Concurrent Game Structures for Temporal STIT Logic

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 φ is true, as a consequence of her choice".