On the Expressiveness and Complexity of ATL

DOI10.1007/978-3-540-71389-0_18zbMath1142.68438OpenAlexW1589868478MaRDI QIDQ5758039

Nicolas Markey, François Laroussinie, Ghassan Oreiby

Publication date: 7 September 2007

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71389-0_18

zbMATH Keywords

model checkingtemporal logicmulti-agent systemsconcurrent game structuresalternating bisimulationalternating transition systems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items

Automatic verification of competitive stochastic systems, Model checking abilities of agents: a closer look, ATL with Strategy Contexts and Bounded Memory, Easy Yet Hard: Model Checking Strategies of Agents, Constructive knowledge: what agents can achieve under imperfect information