Sciweavers

ATAL
2010
Springer

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

13 years 4 months ago
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...
Jan Broersen
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where ATAL
Authors Jan Broersen
Comments (0)