{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:21Z","timestamp":1760202561152,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,5,15]],"date-time":"2008-05-15T00:00:00Z","timestamp":1210809600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>ATL is a temporal logic geared towards the specification and verification of\nproperties in multi-agents systems. It allows to reason on the existence of\nstrategies for coalitions of agents in order to enforce a given property. In\nthis paper, we first precisely characterize the complexity of ATL\nmodel-checking over Alternating Transition Systems and Concurrent Game\nStructures when the number of agents is not fixed. We prove that it is\n\\Delta^P_2 - and \\Delta^P_?_3-complete, depending on the underlying multi-agent\nmodel (ATS and CGS resp.). We also consider the same problems for some\nextensions of ATL. We then consider expressiveness issues. We show how ATS and\nCGS are related and provide translations between these models w.r.t.\nalternating bisimulation. We also prove that the standard definition of ATL\n(built on modalities \"Next\", \"Always\" and \"Until\") cannot express the duals of\nits modalities: it is necessary to explicitely add the modality \"Release\".<\/jats:p>","DOI":"10.2168\/lmcs-4(2:7)2008","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T13:30:40Z","timestamp":1212499840000},"source":"Crossref","is-referenced-by-count":13,"title":["On the Expressiveness and Complexity of ATL"],"prefix":"10.46298","volume":"Volume 4, Issue 2","author":[{"given":"Francois","family":"Laroussinie","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1977-7525","authenticated-orcid":false,"given":"Nicolas","family":"Markey","sequence":"additional","affiliation":[]},{"given":"Ghassan","family":"Oreiby","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,5,15]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/826\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/826\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:57:04Z","timestamp":1681243024000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,15]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(2:7)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0804.2435","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0804.2435","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"arxiv","id":"1708.05849","asserted-by":"subject"},{"id-type":"doi","id":"10.1007\/s00224-019-09926-y","asserted-by":"subject"},{"id-type":"doi","id":"10.4230\/lipics.stacs.2018.34","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arxiv.1708.05849","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2008,5,15]]},"article-number":"826"}}