CTL.STIT: enhancing ATL to express important multi-agent system verification properties
Jan Broersen · 2010
We present the logic CTL.STIT, which is the join of the logic CTL with a multi-agent strategic stit-logic variant. CTL.STIT subsumes ATL, and adds expressivity to it that we claim is very important for using the formalism for multi-agent system verification. We argue extensively that the extra expressivity is important for extending ATL to a language for reasoning about norms, strategic games, knowledge games, conditional strategies, etc. Also we compare the logic's suitability for multi-agent system verification with verification formalisms based on dynamic logic. We will give a number of arguments in favor of stit-formalisms. But, which paradigm to use ultimately depends on what kind of properties we want to verify.