CTL.STIT: enhancing ATL to express important multi-agent system verification properties

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. Categories and Subject Descriptors I.2.11 [Artificial Intelligence]: Distributed Artificial Intelligence-Multiagent systems; I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods--Modal logic General Terms Theory, Verification Keywords Log...

• Type: Conference
• Year: 2010
• Where: ATAL
• Authors: Jan Broersen
• Keywords: ATAL 2010, Intelligent Agents, Logics, Multi-agent System Verification, Strategic Stit-logic Variant