{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:38:12Z","timestamp":1759639092509},"reference-count":32,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.256.19","type":"journal-article","created":{"date-parts":[[2017,9,6]],"date-time":"2017-09-06T21:26:47Z","timestamp":1504733207000},"page":"268-282","source":"Crossref","is-referenced-by-count":0,"title":["On the Complexity of  ATL  and  ATL* Module Checking"],"prefix":"10.4204","volume":"256","author":[{"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[]}],"member":"2720","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"AGJ07","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/1324249.1324256","article-title":"Alternating-time temporal logics with irrevocable strategies","volume-title":"TARK'07","author":"\u00c5gotnes","year":"2007"},{"key":"Alfaro04three","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/LICS.2004.1319611","article-title":"Three-Valued Abstractions of Games: Uncertainty, but with Precision","volume-title":"LICS'04","author":"de Alfaro","year":"2004"},{"issue":"5","key":"AlurHK02","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","article-title":"Alternating-time temporal logic","volume":"49","author":"Alur","year":"2002","journal-title":"Journal of the ACM"},{"issue":"1","key":"Aminof13pushdown-jc","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2012.11.005","article-title":"Pushdown module checking with imperfect information","volume":"223","author":"Aminof","year":"2013","journal-title":"Inf. Comput."},{"issue":"2","key":"Basu07local","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.entcs.2006.02.035","article-title":"Local Module Checking for CTL Specifications","author":"Basu","year":"2007","journal-title":"ENTCS 176"},{"key":"Bozzelli11newpushown","series-title":"EPTCS 54","doi-asserted-by":"publisher","first-page":"162","DOI":"10.4204\/EPTCS.54.12","article-title":"New results on pushdown module checking with imperfect information","volume-title":"GandALF'11","author":"Bozzelli","year":"2011"},{"issue":"1","key":"Bozzelli10pushdown","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10703-010-0093-x","article-title":"Pushdown Module Checking","volume":"36","author":"Bozzelli","year":"2010","journal-title":"Formal Methods in System Design"},{"key":"CKS81","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","article-title":"Alternation","volume":"28(1)","author":"Chandra","year":"1981","journal-title":"Journal of the ACM"},{"issue":"6","key":"CHP10","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1016\/j.ic.2009.07.004","article-title":"Strategy logic","volume":"208","author":"Chatterjee","year":"2010","journal-title":"Inf. Comput."},{"key":"Clarke81ctl","series-title":"LNCS 131","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","article-title":"Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic","volume-title":"LP'81","author":"Clarke","year":"1981"},{"issue":"1","key":"EmersonH86","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"\"Sometimes\" and \"Not Never\" revisited: on branching versus linear time temporal logic","volume":"33","author":"Emerson","year":"1986","journal-title":"Journal of the ACM"},{"key":"EJ88","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1109\/SFCS.1988.21949","article-title":"The Complexity of Tree Automata and Logics of Programs","volume-title":"FOCS'88","author":"Emerson","year":"1988"},{"key":"Ferrante08enriched","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-4(3:1)2008","article-title":"Enriched \u03bc-Calculi Module Checking","volume":"4","author":"Ferrante","year":"2008","journal-title":"Logical Methods in Computer Science"},{"key":"Godefroid03open","series-title":"LNCS 2855","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45212-6_15","article-title":"Reasoning about Abstract Open Systems with Generalized Module Checking","volume-title":"EMSOFT'03","author":"Godefroid","year":"2003"},{"key":"JamrogaM14","first-page":"701","article-title":"On module checking and strategies","volume-title":"AAMAS'14","author":"Jamroga","year":"2014"},{"key":"JamrogaM15","first-page":"227","article-title":"Module Checking of Strategic Ability","volume-title":"AAMAS'15","author":"Jamroga","year":"2015"},{"key":"KupfermanV98","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1145\/276698.276748","article-title":"Weak Alternating Automata and Tree Automata Emptiness","volume-title":"STOC'98","author":"Kupferman","year":"1998"},{"key":"KV96","series-title":"LNCS 1102","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-61474-5_59","article-title":"Module Checking","volume-title":"CAV'96","author":"Kupferman","year":"1996"},{"key":"Kupferman97revisited","series-title":"LNCS 1254","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-63166-6_7","article-title":"Module Checking Revisited","volume-title":"CAV'97","author":"Kupferman","year":"1997"},{"issue":"2","key":"KVW00","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","article-title":"An Automata-Theoretic Approach to Branching-Time Model Checking","volume":"47","author":"Kupferman","year":"2000","journal-title":"Journal of the ACM"},{"issue":"4","key":"LaroussinieM14","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:17)2014","article-title":"Quantified CTL: Expressiveness and Complexity","volume":"10","author":"Laroussinie","year":"2014","journal-title":"Logical Methods in Computer Science"},{"key":"LaroussinieM15","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.ic.2014.12.020","article-title":"Augmenting ATL with strategy contexts","volume":"245","author":"Laroussinie","year":"2015","journal-title":"Inf. Comput."},{"key":"Martinelli07specification","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.entcs.2006.12.003","article-title":"An Approach for the Specification, Verification and Synthesis of Secure Systems","author":"Martinelli","year":"2007","journal-title":"ENTCS 168"},{"issue":"4","key":"MMPV14","doi-asserted-by":"publisher","DOI":"10.1145\/2631917","article-title":"Reasoning About Strategies: On the Model-Checking Problem","volume":"15","author":"Mogavero","year":"2014","journal-title":"ACM Trans. Comput. Log."},{"key":"Murano08hierarchical","series-title":"LNCS 5330","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-89439-1_23","article-title":"Program Complexity in Hierarchical Module Checking","volume-title":"LPAR'08","author":"Murano","year":"2008"},{"key":"Pnueli77","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/SFCS.1977.32","article-title":"The Temporal Logic of Programs","volume-title":"FOCS'77","author":"Pnueli","year":"1977"},{"key":"Queille81verification","series-title":"LNCS 137","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","article-title":"Specification and verification of concurrent programs in Cesar","volume-title":"SP'82","author":"Queille","year":"1982"},{"key":"Safra88","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1109\/SFCS.1988.21948","article-title":"On the Complexity of \u03c9-Automata","volume-title":"FOCS'88","author":"Safra","year":"1988"},{"key":"Schewe08","series-title":"LNCS 5126","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-540-70583-3_31","article-title":"ATL* Satisfiability Is 2EXPTIME-Complete","volume-title":"ICALP'08","author":"Schewe","year":"2008"},{"key":"ScheweF06","series-title":"LNCS 4207","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/11874683_39","article-title":"Satisfiability and Finite Model Property for the Alternating-Time mu-Calculus","volume-title":"CSL'06","author":"Schewe","year":"2006"},{"issue":"1","key":"VardiW94","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning About Infinite Computations","volume":"115","author":"Vardi","year":"1994","journal-title":"Inf. Comput."},{"key":"Var98","series-title":"LNCS 1443","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BFb0055090","article-title":"Reasoning about the past with two-way automata","volume-title":"ICALP'98","author":"Vardi","year":"1998"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T08:21:58Z","timestamp":1505290918000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1709.02107v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,6]]},"references-count":32,"URL":"https:\/\/doi.org\/10.4204\/eptcs.256.19","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,6]]}}}