Concurrent Game Structures for Temporal STIT Logic
Joseph Boudou, Emiliano Lorini · 2018
The paper introduces a new semantics for temporal STIT logic (the logic of seeing to it that ) based on concurrent game structures (CGSs), thereby strengthening the connection between temporal STIT and existing logics for MAS including coalition logic, alternating-time temporal logic and strategy logic whose language are usually interpreted over CGSs. Moreover, it provides a complexity result for a rich temporal STIT language interpreted over these structures. The language extends that of full computation tree logic (CTL*) by individual agency operators, allowing to express sentences of the form "agent i sees to it that $\varphi$ is true, as a consequence of her choice''.