Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
On the Expressiveness and Complexity of ATL
verfasst von : François Laroussinie, Nicolas Markey, Ghassan Oreiby
Erschienen in: Foundations of Software Science and Computational Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
ATL
is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of
ATL
(built on modalities “Next”, “Always” and “Until”) has to be completed in order to express the duals of its modalities: it is necessary to add the modality “Release”. We then precisely characterize the complexity of
ATL
model-checking when the number of agents is not fixed. We prove that it is
$\bf \Delta_{\rm 2}^{\sf P}$
- and
$\bf \Delta_{\rm 3}^{\sf P}$
-complete, depending on the underlying multi-agent model (
ATS
and
CGS
resp.). We also prove that
ATL
+ model-checking is
$\bf \Delta_{\rm 3}^{\sf P}$
-complete over both models, even with a fixed number of agents.