Francois Laroussinie ; Nicolas Markey ; Ghassan Oreiby - On the Expressiveness and Complexity of ATL

lmcs:826 - Logical Methods in Computer Science, May 15, 2008, Volume 4, Issue 2 - https://doi.org/10.2168/LMCS-4(2:7)2008
On the Expressiveness and Complexity of ATL

Authors: Francois Laroussinie ; Nicolas Markey ; Ghassan Oreiby

    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. In this paper, we first precisely characterize the complexity of ATL model-checking over Alternating Transition Systems and Concurrent Game Structures when the number of agents is not fixed. We prove that it is \Delta^P_2 - and \Delta^P_?_3-complete, depending on the underlying multi-agent model (ATS and CGS resp.). We also consider the same problems for some extensions of ATL. We then consider expressiveness issues. We show how ATS and CGS are related and provide translations between these models w.r.t. alternating bisimulation. We also prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") cannot express the duals of its modalities: it is necessary to explicitely add the modality "Release".


    Volume: Volume 4, Issue 2
    Published on: May 15, 2008
    Accepted on: June 25, 2015
    Submitted on: September 20, 2007
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computer Science and Game Theory,Computer Science - Multiagent Systems,F.1.1,F.3.1

    Linked data

    Source : ScholeXplorer IsReferencedBy ARXIV 1708.05849
    Source : ScholeXplorer IsReferencedBy DOI 10.1007/s00224-019-09926-y
    Source : ScholeXplorer IsReferencedBy DOI 10.4230/lipics.stacs.2018.34
    Source : ScholeXplorer IsReferencedBy DOI 10.48550/arxiv.1708.05849
    • 10.4230/lipics.stacs.2018.34
    • 10.1007/s00224-019-09926-y
    • 10.1007/s00224-019-09926-y
    • 10.1007/s00224-019-09926-y
    • 1708.05849
    • 10.48550/arxiv.1708.05849
    Dependences in Strategy Logic
    Gardy, Patrick ; Bouyer, Patricia ; Markey, Nicolas ;

    13 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 365 times.
    This article's PDF has been downloaded 199 times.