{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T09:13:09Z","timestamp":1772356389134,"version":"3.50.1"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,1,5]],"date-time":"2021-01-05T00:00:00Z","timestamp":1609804800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["IIS-1527668, CCF-1704883, and IIS-1830549"],"award-info":[{"award-number":["IIS-1527668, CCF-1704883, and IIS-1830549"]}]},{"name":"Maryland Procurement Office"},{"name":"European Union's Horizon 2020 research and innovation programme"},{"name":"Marie Sklodowska-Curie","award":["709188"],"award-info":[{"award-number":["709188"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,1,31]]},"abstract":"<jats:p>\n            We introduce an extension of Strategy Logic for the imperfect-information setting, called SL\n            <jats:sub>ii<\/jats:sub>\n            and study its model-checking problem. As this logic naturally captures multi-player games with imperfect information, this problem is undecidable; but we introduce a syntactical class of \u201chierarchical instances\u201d for which, intuitively, as one goes down the syntactic tree of the formula, strategy quantifications are concerned with finer observations of the model, and we prove that model-checking SL\n            <jats:sub>ii<\/jats:sub>\n            restricted to hierarchical instances is decidable. This result, because it allows for complex patterns of existential and universal quantification on strategies, greatly generalises the decidability of distributed synthesis for systems with hierarchical information. It allows us to easily derive new decidability results concerning strategic problems under imperfect information such as the existence of Nash equilibria or rational synthesis.\n          <\/jats:p>\n          <jats:p>\n            To establish this result, we go through an intermediary, \u201clow-level\u201d logic much more adapted to automata techniques. QCTL\n            <jats:sup>*<\/jats:sup>\n            is an extension of CTL\n            <jats:sup>*<\/jats:sup>\n            with second-order quantification over atomic propositions that has been used to study strategic logics with perfect information. We extend it to the imperfect information setting by parameterising second-order quantifiers with observations. The simple syntax of the resulting logic, QCTL\n            <jats:sup>*<\/jats:sup>\n            <jats:sub>ii<\/jats:sub>\n            , allows us to provide a conceptually neat reduction of SL\n            <jats:sub>ii<\/jats:sub>\n            to QCTL\n            <jats:sup>*<\/jats:sup>\n            <jats:sub>ii<\/jats:sub>\n            that separates concerns, allowing one to forget about strategies and players and focus solely on second-order quantification. While the model-checking problem of QCTL\n            <jats:sup>*<\/jats:sup>\n            <jats:sub>ii<\/jats:sub>\n            is, in general, undecidable, we identify a syntactic fragment of hierarchical formulas and prove, using an automata-theoretic approach, that it is decidable.\n          <\/jats:p>","DOI":"10.1145\/3427955","type":"journal-article","created":{"date-parts":[[2021,1,5]],"date-time":"2021-01-05T18:14:11Z","timestamp":1609870451000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Strategy Logic with Imperfect Information"],"prefix":"10.1145","volume":"22","author":[{"given":"Rapha\u00ebl","family":"Berthon","sequence":"first","affiliation":[{"name":"Universit\u00e9 libre de Bruxelles 8 University of Antwerp, Triomphe, Ixelles, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bastien","family":"Maubert","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli \u201cFederico II,\u201d, Napoli, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli \u201cFederico II,\u201d, Napoli, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasha","family":"Rubin","sequence":"additional","affiliation":[{"name":"University of Sydney, Darlington NSW, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Rice University, Houston, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"#cr-split#-e_1_2_1_2_1.1","doi-asserted-by":"crossref","unstructured":"Francesco Belardinelli. 2014. Reasoning about knowledge and strategies: Epistemic strategy logic. In SR'14. 27--33. DOI:https:\/\/doi.org\/10.4204\/EPTCS.146.4 10.4204\/EPTCS.146.4","DOI":"10.4204\/EPTCS.146.4"},{"key":"#cr-split#-e_1_2_1_2_1.2","doi-asserted-by":"crossref","unstructured":"Francesco Belardinelli. 2014. Reasoning about knowledge and strategies: Epistemic strategy logic. In SR'14. 27--33. DOI:https:\/\/doi.org\/10.4204\/EPTCS.146.4","DOI":"10.4204\/EPTCS.146.4"},{"key":"e_1_2_1_3_1","unstructured":"Francesco Belardinelli. 2015. A logic of knowledge and strategies with imperfect information. In LAMAS\u201915. 1--15.  Francesco Belardinelli. 2015. A logic of knowledge and strategies with imperfect information. In LAMAS\u201915. 1--15."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Francesco Belardinelli Alessio Lomuscio Aniello Murano and Sasha Rubin. 2017. Verification of broadcasting multi-agent systems against an epistemic strategy logic. In IJCAI\u201917. 91--97. DOI:https:\/\/doi.org\/10.24963\/ijcai.2017\/14    10.24963\/ijcai.2017\nFrancesco Belardinelli Alessio Lomuscio Aniello Murano and Sasha Rubin. 2017. Verification of broadcasting multi-agent systems against an epistemic strategy logic. In IJCAI\u201917. 91--97. DOI:https:\/\/doi.org\/10.24963\/ijcai.2017\/14","DOI":"10.24963\/ijcai.2017\/14"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103302"},{"key":"e_1_2_1_6_1","unstructured":"Rapha\u00ebl Berthon Bastien Maubert and Aniello Murano. 2017. Decidability results for ATL* with imperfect information and perfect recall. In AAMAS\u201917. 1250--1258. Retrieved from http:\/\/arxiv.org\/abs\/1805.12582.  Rapha\u00ebl Berthon Bastien Maubert and Aniello Murano. 2017. Decidability results for ATL* with imperfect information and perfect recall. In AAMAS\u201917. 1250--1258. Retrieved from http:\/\/arxiv.org\/abs\/1805.12582."},{"key":"e_1_2_1_7_1","volume-title":"Vardi","author":"Berthon Raphael","year":"2017","unstructured":"Raphael Berthon , Bastien Maubert , Aniello Murano , Sasha Rubin , and Moshe Y . Vardi . 2017 . Strategy logic with imperfect information. In LICS\u201917. IEEE , 1--12. DOI:https:\/\/doi.org\/10.1109\/LICS.2017.8005136 10.1109\/LICS.2017.8005136 Raphael Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, and Moshe Y. Vardi. 2017. Strategy logic with imperfect information. In LICS\u201917. IEEE, 1--12. DOI:https:\/\/doi.org\/10.1109\/LICS.2017.8005136"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.09.006"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0306-5"},{"key":"e_1_2_1_10_1","unstructured":"Benjamin Bittner Marco Bozzano Alessandro Cimatti and Xavier Olive. 2012. Symbolic synthesis of observability requirements for diagnosability. In AAAI\u201912.  Benjamin Bittner Marco Bozzano Alessandro Cimatti and Xavier Olive. 2012. Symbolic synthesis of observability requirements for diagnosability. In AAAI\u201912."},{"key":"e_1_2_1_11_1","volume-title":"FOSSACS\u201918","author":"Bouyer Patricia","unstructured":"Patricia Bouyer . 2018. Games on graphs with a public signal monitoring . In FOSSACS\u201918 . Springer , 530--547. Retrieved from http:\/\/arxiv.org\/abs\/1710.07163. Patricia Bouyer. 2018. Games on graphs with a public signal monitoring. In FOSSACS\u201918. Springer, 530--547. Retrieved from http:\/\/arxiv.org\/abs\/1710.07163."},{"key":"e_1_2_1_12_1","volume-title":"Pure Nash equilibria in concurrent deterministic games. Log. Methods Comput. Sci. 11, 2","author":"Bouyer Patricia","year":"2015","unstructured":"Patricia Bouyer , Romain Brenguier , Nicolas Markey , and Michael Ummels . 2015. Pure Nash equilibria in concurrent deterministic games. Log. Methods Comput. Sci. 11, 2 ( 2015 ). DOI:https:\/\/doi.org\/10.2168\/LMCS-11(2:9)2015 10.2168\/LMCS-11(2:9)2015 Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. 2015. Pure Nash equilibria in concurrent deterministic games. Log. Methods Comput. Sci. 11, 2 (2015). DOI:https:\/\/doi.org\/10.2168\/LMCS-11(2:9)2015"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.10.010"},{"key":"e_1_2_1_14_1","volume-title":"CONCUR\u201917","volume":"85","author":"Brenguier Romain","year":"2017","unstructured":"Romain Brenguier , Arno Pauly , Jean-Fran\u00e7ois Raskin , and Ocan Sankur . 2017 . Admissibility in games with imperfect information . In CONCUR\u201917 , Vol. 85 . Romain Brenguier, Arno Pauly, Jean-Fran\u00e7ois Raskin, and Ocan Sankur. 2017. Admissibility in games with imperfect information. In CONCUR\u201917, Vol. 85."},{"key":"e_1_2_1_15_1","volume-title":"AAMAS\u201914 28, 3","author":"Bulling Nils","year":"2014","unstructured":"Nils Bulling and Wojciech Jamroga . 2014. Comparing variants of strategic ability: How uncertainty and memory influence general properties of games . In AAMAS\u201914 28, 3 ( 2014 ), 474--518. Nils Bulling and Wojciech Jamroga. 2014. Comparing variants of strategic ability: How uncertainty and memory influence general properties of games. In AAMAS\u201914 28, 3 (2014), 474--518."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.09.011"},{"key":"e_1_2_1_17_1","volume-title":"LPAR\u201910","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee and Laurent Doyen . 2010. The complexity of partial-observation parity games . In LPAR\u201910 . Springer , 1--14. Krishnendu Chatterjee and Laurent Doyen. 2010. The complexity of partial-observation parity games. In LPAR\u201910. Springer, 1--14."},{"key":"#cr-split#-e_1_2_1_18_1.1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee and Laurent Doyen. 2014. Games with a weak adversary. In ICALP'14. 110--121. DOI:https:\/\/doi.org\/10.1007\/978-3-662-43951-7_10 10.1007\/978-3-662-43951-7_10","DOI":"10.1007\/978-3-662-43951-7_10"},{"key":"#cr-split#-e_1_2_1_18_1.2","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee and Laurent Doyen. 2014. Games with a weak adversary. In ICALP'14. 110--121. DOI:https:\/\/doi.org\/10.1007\/978-3-662-43951-7_10","DOI":"10.1007\/978-3-662-43951-7_10"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579821"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.10.012"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.07.004"},{"key":"e_1_2_1_22_1","unstructured":"Edmund M. Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. The MIT Press.  Edmund M. Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. The MIT Press."},{"key":"#cr-split#-e_1_2_1_23_1.1","unstructured":"Rodica Condurache Emmanuel Filiot Raffaella Gentilini and Jean-Fran\u00e7ois Raskin. 2016. The complexity of rational synthesis. In ICALP'16. 121:1--121:15. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.121 10.4230\/LIPIcs.ICALP.2016.121"},{"key":"#cr-split#-e_1_2_1_23_1.2","unstructured":"Rodica Condurache Emmanuel Filiot Raffaella Gentilini and Jean-Fran\u00e7ois Raskin. 2016. The complexity of rational synthesis. In ICALP'16. 121:1--121:15. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.121"},{"key":"e_1_2_1_24_1","volume-title":"CSL\u201910","author":"Degorre Aldric","unstructured":"Aldric Degorre , Laurent Doyen , Raffaella Gentilini , Jean-Fran\u00e7ois Raskin , and Szymon Toru\u0144czyk . 2010. Energy and mean-payoff games with imperfect information . In CSL\u201910 . Springer , 260--274. Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-Fran\u00e7ois Raskin, and Szymon Toru\u0144czyk. 2010. Energy and mean-payoff games with imperfect information. In CSL\u201910. Springer, 260--274."},{"key":"e_1_2_1_25_1","volume-title":"Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR","author":"Dima Catalin","year":"2011","unstructured":"Catalin Dima and Ferucio Laurentiu Tiplea . 2011. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR ( 2011 ). arXiv:1102.4225 Catalin Dima and Ferucio Laurentiu Tiplea. 2011. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR (2011). arXiv:1102.4225"},{"key":"e_1_2_1_26_1","volume-title":"Lectures in Game Theory for Computer Scientists","author":"Doyen Laurent","unstructured":"Laurent Doyen and Jean-Fran\u00e7ois Raskin . 2011. Games with imperfect information: Theory and algorithms . In Lectures in Game Theory for Computer Scientists . Cambridge University Press , Cambridge, UK , 185--212. Laurent Doyen and Jean-Fran\u00e7ois Raskin. 2011. Games with imperfect information: Theory and algorithms. In Lectures in Game Theory for Computer Scientists. Cambridge University Press, Cambridge, UK, 185--212."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269808"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_29_1","volume-title":"Vardi","author":"Fagin Ronald","year":"1995","unstructured":"Ronald Fagin , Joseph Y. Halpern , Yoram Moses , and Moshe Y . Vardi . 1995 . Reasoning about Knowledge. Vol. 4 . The MIT Press , Cambridge, MA. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. 1995. Reasoning about Knowledge. Vol. 4. The MIT Press, Cambridge, MA."},{"key":"e_1_2_1_30_1","unstructured":"Emmanuel Filiot Raffaella Gentilini and Jean-Fran\u00e7ois Raskin. 2018. Rational synthesis under imperfect information. In LICS\u201918. ACM 422--431.  Emmanuel Filiot Raffaella Gentilini and Jean-Fran\u00e7ois Raskin. 2018. Rational synthesis under imperfect information. In LICS\u201918. ACM 422--431."},{"key":"#cr-split#-e_1_2_1_31_1.1","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner and Sven Schewe. 2005. Uniform distributed synthesis. In LICS'05. 321--330. DOI:https:\/\/doi.org\/10.1109\/LICS.2005.53 10.1109\/LICS.2005.53","DOI":"10.1109\/LICS.2005.53"},{"key":"#cr-split#-e_1_2_1_31_1.2","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner and Sven Schewe. 2005. Uniform distributed synthesis. In LICS'05. 321--330. DOI:https:\/\/doi.org\/10.1109\/LICS.2005.53","DOI":"10.1109\/LICS.2005.53"},{"key":"#cr-split#-e_1_2_1_32_1.1","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner and Sven Schewe. 2010. Coordination logic. In CSL'10. 305--319. DOI:https:\/\/doi.org\/10.1007\/978-3-642-15205-4_25 10.1007\/978-3-642-15205-4_25","DOI":"10.1007\/978-3-642-15205-4_25"},{"key":"#cr-split#-e_1_2_1_32_1.2","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner and Sven Schewe. 2010. Coordination logic. In CSL'10. 305--319. DOI:https:\/\/doi.org\/10.1007\/978-3-642-15205-4_25","DOI":"10.1007\/978-3-642-15205-4_25"},{"key":"e_1_2_1_33_1","volume-title":"TACAS\u201910","author":"Fisman Dana","unstructured":"Dana Fisman , Orna Kupferman , and Yoad Lustig . 2010. Rational synthesis . In TACAS\u201910 . Springer , 190--204. DOI:https:\/\/doi.org\/10.1007\/978-3-642-12002-2_16 10.1007\/978-3-642-12002-2_16 Dana Fisman, Orna Kupferman, and Yoad Lustig. 2010. Rational synthesis. In TACAS\u201910. Springer, 190--204. DOI:https:\/\/doi.org\/10.1007\/978-3-642-12002-2_16"},{"key":"#cr-split#-e_1_2_1_34_1.1","doi-asserted-by":"crossref","unstructured":"Tim French. 2001. Decidability of quantifed propositional branching time logics. In AJCAI'01. 165--176. DOI:https:\/\/doi.org\/10.1007\/3-540-45656-2_15 10.1007\/3-540-45656-2_15","DOI":"10.1007\/3-540-45656-2_15"},{"key":"#cr-split#-e_1_2_1_34_1.2","doi-asserted-by":"crossref","unstructured":"Tim French. 2001. Decidability of quantifed propositional branching time logics. In AJCAI'01. 165--176. DOI:https:\/\/doi.org\/10.1007\/3-540-45656-2_15","DOI":"10.1007\/3-540-45656-2_15"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0064-7"},{"key":"e_1_2_1_36_1","volume-title":"FoSSaCS\u201915","author":"Genest Blaise","unstructured":"Blaise Genest , Doron Peled , and Sven Schewe . 2015. Knowledge&equals; observation+ memory+ computation. In FoSSaCS\u201915 . Springer , 215--229. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46678-014 10.1007\/978-3-662-46678-014 Blaise Genest, Doron Peled, and Sven Schewe. 2015. Knowledge&equals; observation+ memory+ computation. In FoSSaCS\u201915. Springer, 215--229. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46678-014"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.21.93-131"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2018.02.023"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90039-1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3233769"},{"key":"e_1_2_1_41_1","volume-title":"IJCAI\u201911","author":"Jamroga Wojciech","unstructured":"Wojciech Jamroga and Nils Bulling . 2011. Comparing variants of strategic ability . In IJCAI\u201911 . AAAI Press , 252--257. DOI:https:\/\/doi.org\/10.1023\/A:1026171312755 10.1023\/A:1026171312755 Wojciech Jamroga and Nils Bulling. 2011. Comparing variants of strategic ability. In IJCAI\u201911. AAAI Press, 252--257. DOI:https:\/\/doi.org\/10.1023\/A:1026171312755"},{"key":"e_1_2_1_42_1","unstructured":"Wojciech Jamroga Vadim Malvone and Aniello Murano. 2019. Natural strategic ability under imperfect information. In AAMAS\u201919. 962--970.  Wojciech Jamroga Vadim Malvone and Aniello Murano. 2019. Natural strategic ability under imperfect information. In AAMAS\u201919. 962--970."},{"key":"e_1_2_1_43_1","unstructured":"Wojciech Jamroga and Aniello Murano. 2014. On module checking and strategies. In AAMAS\u201914. 701--708.  Wojciech Jamroga and Aniello Murano. 2014. On module checking and strategies. In AAMAS\u201914. 701--708."},{"key":"e_1_2_1_44_1","unstructured":"Wojciech Jamroga and Aniello Murano. 2015. Module checking of strategic ability. In AAMAS\u201915. 227--235.  Wojciech Jamroga and Aniello Murano. 2015. Module checking of strategic ability. In AAMAS\u201915. 227--235."},{"key":"e_1_2_1_45_1","first-page":"2","article-title":"Agents that know how to play","volume":"63","author":"Jamroga Wojciech","year":"2004","unstructured":"Wojciech Jamroga and Wiebe van der Hoek . 2004 . Agents that know how to play . Fundam. Inform. 63 , 2 -- 3 (2004), 185--219. Wojciech Jamroga and Wiebe van der Hoek. 2004. Agents that know how to play. Fundam. Inform. 63, 2--3 (2004), 185--219.","journal-title":"Fundam. Inform."},{"key":"e_1_2_1_46_1","unstructured":"Sophia Knight and Bastien Maubert. 2019. Dealing with imperfect information in strategy logic. In SR\u201915. arxiv:1908.02488.  Sophia Knight and Bastien Maubert. 2019. Dealing with imperfect information in strategy logic. In SR\u201915. arxiv:1908.02488."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.2.135"},{"key":"e_1_2_1_48_1","volume-title":"Pazhamaneri Subramaniam Thiagarajan, and Moshe Y. Vardi","author":"Kupferman Orna","year":"2000","unstructured":"Orna Kupferman , Parthasarathy Madhusudan , Pazhamaneri Subramaniam Thiagarajan, and Moshe Y. Vardi . 2000 . Open systems in reactive environments: Control and synthesis. In CONCUR\u2019 00. 92--107. Orna Kupferman, Parthasarathy Madhusudan, Pazhamaneri Subramaniam Thiagarajan, and Moshe Y. Vardi. 2000. Open systems in reactive environments: Control and synthesis. In CONCUR\u201900. 92--107."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-016-9508-8"},{"key":"e_1_2_1_50_1","volume-title":"Vardi","author":"Kupferman Orna","year":"1997","unstructured":"Orna Kupferman and Moshe Y . Vardi . 1997 . Module checking revisited. In CAV\u201997. Springer , 36--47. Orna Kupferman and Moshe Y. Vardi. 1997. Module checking revisited. In CAV\u201997. Springer, 36--47."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.2307\/421091"},{"key":"e_1_2_1_52_1","volume-title":"Vardi","author":"Kupferman Orna","year":"2001","unstructured":"Orna Kupferman and Moshe Y . Vardi . 2001 . Synthesizing distributed systems. In LICS\u2019 01. 389--398. DOI:https:\/\/doi.org\/10.1109\/LICS.2001.932514 10.1109\/LICS.2001.932514 Orna Kupferman and Moshe Y. Vardi. 2001. Synthesizing distributed systems. In LICS\u201901. 389--398. DOI:https:\/\/doi.org\/10.1109\/LICS.2001.932514"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2893"},{"key":"e_1_2_1_55_1","volume-title":"Quantified CTL: Expressiveness and complexity. Log. Methods Comput. Sci. 10, 4","author":"Laroussinie Fran\u00e7ois","year":"2014","unstructured":"Fran\u00e7ois Laroussinie and Nicolas Markey . 2014. Quantified CTL: Expressiveness and complexity. Log. Methods Comput. Sci. 10, 4 ( 2014 ). DOI:https:\/\/doi.org\/10.2168\/LMCS-10(4:17)2014 10.2168\/LMCS-10(4:17)2014 Fran\u00e7ois Laroussinie and Nicolas Markey. 2014. Quantified CTL: Expressiveness and complexity. Log. Methods Comput. Sci. 10, 4 (2014). DOI:https:\/\/doi.org\/10.2168\/LMCS-10(4:17)2014"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.12.020"},{"key":"#cr-split#-e_1_2_1_57_1.1","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Laroussinie Nicolas Markey and Arnaud Sangnier. 2015. ATLsc with partial observation. In GandALF'15. 43--57. DOI:https:\/\/doi.org\/10.4204\/EPTCS.193.4 10.4204\/EPTCS.193.4","DOI":"10.4204\/EPTCS.193.4"},{"key":"#cr-split#-e_1_2_1_57_1.2","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Laroussinie Nicolas Markey and Arnaud Sangnier. 2015. ATLsc with partial observation. In GandALF'15. 43--57. DOI:https:\/\/doi.org\/10.4204\/EPTCS.193.4","DOI":"10.4204\/EPTCS.193.4"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273878"},{"key":"e_1_2_1_59_1","unstructured":"Christof L\u00f6ding. 2011. Automata on infinite trees. In Preliminary Version for the Handbook Automata: From Mathematics to Applications Jean-Eric Pin (Ed.). Available online from author.  Christof L\u00f6ding. 2011. Automata on infinite trees. In Preliminary Version for the Handbook Automata: From Mathematics to Applications Jean-Eric Pin (Ed.). Available online from author."},{"key":"e_1_2_1_60_1","unstructured":"Bastien Maubert and Aniello Murano. 2018. Reasoning about knowledge and strategies under hierarchical information. In KR\u201918. Retrieved from http:\/\/arxiv.org\/abs\/1806.00028.  Bastien Maubert and Aniello Murano. 2018. Reasoning about knowledge and strategies under hierarchical information. In KR\u201918. Retrieved from http:\/\/arxiv.org\/abs\/1806.00028."},{"key":"e_1_2_1_61_1","article-title":"Reasoning about strategies: On the model-checking problem","volume":"15","author":"Mogavero Fabio","year":"2014","unstructured":"Fabio Mogavero , Aniello Murano , Giuseppe Perelli , and Moshe Y. Vardi . 2014 . Reasoning about strategies: On the model-checking problem . ACM Trans. Comput. Log. 15 , 4 (2014), 34:1--34:47. DOI:https:\/\/doi.org\/10.1145\/2631917 10.1145\/2631917 Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. 2014. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log. 15, 4 (2014), 34:1--34:47. DOI:https:\/\/doi.org\/10.1145\/2631917","journal-title":"ACM Trans. Comput. Log."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00214-4"},{"key":"e_1_2_1_63_1","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/j.ipl.2016.10.005","article-title":"The fixed initial credit problem for partial-observation energy games is Ack-complete","volume":"118","author":"P\u00e9rez Guillermo A.","year":"2017","unstructured":"Guillermo A. P\u00e9rez . 2017 . The fixed initial credit problem for partial-observation energy games is Ack-complete . Inf. Process. Lett. 118 (2017), 91 -- 99 . Guillermo A. P\u00e9rez. 2017. The fixed initial credit problem for partial-observation energy games is Ack-complete. Inf. Process. Lett. 118 (2017), 91--99.","journal-title":"Inf. Process. Lett."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0898-1221(00)00333-3"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0898-1221(01)00282-6"},{"key":"e_1_2_1_66_1","volume-title":"Reif","author":"Peterson Gary L.","year":"1979","unstructured":"Gary L. Peterson and John H . Reif . 1979 . Multiple-person alternation. In SFCS\u2019 79. 348--363. DOI:https:\/\/doi.org\/10.1109\/SFCS.1979.25 10.1109\/SFCS.1979.25 Gary L. Peterson and John H. Reif. 1979. Multiple-person alternation. In SFCS\u201979. 348--363. DOI:https:\/\/doi.org\/10.1109\/SFCS.1979.25"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2005.04.011"},{"key":"e_1_2_1_68_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. 1977. The temporal logic of programs. In FOCS\u201977. 46--57.  Amir Pnueli. 1977. The temporal logic of programs. In FOCS\u201977. 46--57.","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_69_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli and Roni Rosner. 1989. On the synthesis of a reactive module. In POPL\u201989. 179--190.  Amir Pnueli and Roni Rosner. 1989. On the synthesis of a reactive module. In POPL\u201989. 179--190.","DOI":"10.1145\/75277.75293"},{"key":"#cr-split#-e_1_2_1_70_1.1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli and Roni Rosner. 1990. Distributed reactive systems are hard to synthesize. In FOCS'90. 746--757. DOI:https:\/\/doi.org\/10.1109\/FSCS.1990.89597 10.1109\/FSCS.1990.89597","DOI":"10.1109\/FSCS.1990.89597"},{"key":"#cr-split#-e_1_2_1_70_1.2","doi-asserted-by":"crossref","unstructured":"Amir Pnueli and Roni Rosner. 1990. Distributed reactive systems are hard to synthesize. In FOCS'90. 746--757. DOI:https:\/\/doi.org\/10.1109\/FSCS.1990.89597","DOI":"10.1109\/FSCS.1990.89597"},{"key":"e_1_2_1_71_1","doi-asserted-by":"crossref","unstructured":"Bernd Puchala. 2010. Asynchronous omega-regular games with partial information. In MFCS\u201910. 592--603.  Bernd Puchala. 2010. Asynchronous omega-regular games with partial information. In MFCS\u201910. 592--603.","DOI":"10.1007\/978-3-642-15155-2_52"},{"key":"e_1_2_1_72_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin Michael O.","year":"1969","unstructured":"Michael O. Rabin . 1969 . Decidability of second-order theories and automata on infinite trees . Trans. Amer. Math. Soc. 141 (1969), 1 -- 35 . DOI:https:\/\/doi.org\/10.1090\/S0002-9947-1969-0246760-1 10.1090\/S0002-9947-1969-0246760-1 Michael O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141 (1969), 1--35. DOI:https:\/\/doi.org\/10.1090\/S0002-9947-1969-0246760-1","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_1_73_1","volume-title":"CONCUR\u201910","author":"Ramanujam Ramaswamy","unstructured":"Ramaswamy Ramanujam and Sunil Simon . 2010. A communication based model for games of imperfect information . In CONCUR\u201910 . Springer , 509--523. Ramaswamy Ramanujam and Sunil Simon. 2010. A communication based model for games of imperfect information. In CONCUR\u201910. Springer, 509--523."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90034-5"},{"key":"#cr-split#-e_1_2_1_75_1.1","doi-asserted-by":"crossref","unstructured":"Sven Schewe and Bernd Finkbeiner. 2007. Distributed synthesis for alternating-time logics. In ATVA'07. 268--283. DOI:https:\/\/doi.org\/10.1007\/978-3-540-75596-8_20 10.1007\/978-3-540-75596-8_20","DOI":"10.1007\/978-3-540-75596-8_20"},{"key":"#cr-split#-e_1_2_1_75_1.2","doi-asserted-by":"crossref","unstructured":"Sven Schewe and Bernd Finkbeiner. 2007. Distributed synthesis for alternating-time logics. In ATVA'07. 268--283. DOI:https:\/\/doi.org\/10.1007\/978-3-540-75596-8_20","DOI":"10.1007\/978-3-540-75596-8_20"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82604-0"},{"key":"e_1_2_1_77_1","first-page":"301","article-title":"Spieltheoretische behandlung eines oligopolmodells mit nachfragetr\u00e4gheit: Teil i: Bestimmung des dynamischen preisgleichgewichts","volume":"2","author":"Selten Reinhard","year":"1965","unstructured":"Reinhard Selten . 1965 . Spieltheoretische behandlung eines oligopolmodells mit nachfragetr\u00e4gheit: Teil i: Bestimmung des dynamischen preisgleichgewichts . Zeitschrift gesamte Staatswissenschaft\/J. Instit. Theor. Econ. H. 2 (1965), 301 -- 324 . Reinhard Selten. 1965. Spieltheoretische behandlung eines oligopolmodells mit nachfragetr\u00e4gheit: Teil i: Bestimmung des dynamischen preisgleichgewichts. Zeitschrift gesamte Staatswissenschaft\/J. Instit. Theor. Econ. H. 2 (1965), 301--324.","journal-title":"Zeitschrift gesamte Staatswissenschaft\/J. Instit. Theor. Econ. H."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90090-3"},{"key":"e_1_2_1_80_1","volume-title":"Vardi","author":"van der Meyden Ron","year":"1998","unstructured":"Ron van der Meyden and Moshe Y . Vardi . 1998 . Synthesis from knowledge-based specifications. In CONCUR\u201998. Springer , 34--49. Ron van der Meyden and Moshe Y. Vardi. 1998. Synthesis from knowledge-based specifications. In CONCUR\u201998. Springer, 34--49."},{"key":"e_1_2_1_81_1","doi-asserted-by":"crossref","unstructured":"Ron van der Meyden and Thomas Wilke. 2005. Synthesis of distributed systems from knowledge-based specifications. In CONCUR\u201905. 562--576.  Ron van der Meyden and Thomas Wilke. 2005. Synthesis of distributed systems from knowledge-based specifications. In CONCUR\u201905. 562--576.","DOI":"10.1007\/11539452_42"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1092"},{"key":"#cr-split#-e_1_2_1_83_1.1","doi-asserted-by":"crossref","unstructured":"Steen Vester. 2013. Alternating-time temporal logic with finite-memory strategies. In GandALF'13. 19--207. DOI:https:\/\/doi.org\/10.4204\/EPTCS.119.17 10.4204\/EPTCS.119.17","DOI":"10.4204\/EPTCS.119.17"},{"key":"#cr-split#-e_1_2_1_83_1.2","doi-asserted-by":"crossref","unstructured":"Steen Vester. 2013. Alternating-time temporal logic with finite-memory strategies. In GandALF'13. 19--207. DOI:https:\/\/doi.org\/10.4204\/EPTCS.119.17","DOI":"10.4204\/EPTCS.119.17"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00009-7"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427955","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3427955","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:23Z","timestamp":1750195463000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427955"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,5]]},"references-count":93,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1,31]]}},"alternative-id":["10.1145\/3427955"],"URL":"https:\/\/doi.org\/10.1145\/3427955","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,5]]},"assertion":[{"value":"2018-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}