{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,22]],"date-time":"2026-02-22T07:23:41Z","timestamp":1771745021878,"version":"3.50.1"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,8,1]],"date-time":"2014-08-01T00:00:00Z","timestamp":1406851200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Embedded System Cup Project, B25B09090100007 (POR Campania FS 2007\/2013, asse IV e asse V)"},{"name":"FP7 European Union project 600958-SHERPA"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,8]]},"abstract":"<jats:p>In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multiagent games, such as A<jats:sc>tl<\/jats:sc>, A<jats:sc>tl<\/jats:sc>*, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced<jats:italic>Strategy Logic<\/jats:italic>, which we denote here by CHP-S<jats:sc>l<\/jats:sc>, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-S<jats:sc>l<\/jats:sc>is obtained by using first-order quantifications over strategies and has been investigated in the very specific setting of two-agents turned-based games, where a nonelementary model-checking algorithm has been provided. While CHP-S<jats:sc>l<\/jats:sc>is a very expressive logic, we claim that it does not fully capture the strategic aspects of multiagent systems.<\/jats:p><jats:p>In this article, we introduce and study a more general strategy logic, denoted S<jats:sc>l<\/jats:sc>, for reasoning about strategies in multiagent concurrent games. As a key aspect, strategies in S<jats:sc>l<\/jats:sc>are not intrinsically glued to a specific agent, but an explicit binding operator allows an agent to bind to a strategy variable. This allows agents to share strategies or reuse one previously adopted. We prove that S<jats:sc>l<\/jats:sc>strictly includes CHP-S<jats:sc>l<\/jats:sc>, while maintaining a decidable model-checking problem. In particular, the algorithm we propose is computationally not harder than the best one known for CHP-S<jats:sc>l<\/jats:sc>. Moreover, we prove that such a problem for S<jats:sc>l<\/jats:sc>is N<jats:sc>on<\/jats:sc>E<jats:sc>lementary<\/jats:sc>. This negative result has spurred us to investigate syntactic fragments of S<jats:sc>l<\/jats:sc>, strictly subsuming A<jats:sc>tl<\/jats:sc>*, with the hope of obtaining an elementary model-checking problem. Among others, we introduce and study the sublogics S<jats:sc>l<\/jats:sc>[<jats:sc>ng<\/jats:sc>], S<jats:sc>l<\/jats:sc>[<jats:sc>bg<\/jats:sc>], and S<jats:sc>l<\/jats:sc>[1<jats:sc>g<\/jats:sc>]. They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean combinations of goals, and, a single goal at a time. Intuitively, for a goal, we mean a sequence of bindings, one for each agent, followed by an L<jats:sc>tl<\/jats:sc>formula. We prove that the model-checking problem for S<jats:sc>l<\/jats:sc>[1<jats:sc>g<\/jats:sc>] is 2E<jats:sc>xp<\/jats:sc>T<jats:sc>ime<\/jats:sc>-<jats:sc>complete<\/jats:sc>, thus not harder than the one for A<jats:sc>tl<\/jats:sc>*. In contrast, S<jats:sc>l<\/jats:sc>[<jats:sc>ng<\/jats:sc>] turns out to be N<jats:sc>on<\/jats:sc>E<jats:sc>lementary<\/jats:sc>-hard, strengthening the corresponding result for S<jats:sc>l<\/jats:sc>. Regarding S<jats:sc>l<\/jats:sc>[<jats:sc>bg<\/jats:sc>], we show that it includes CHP-S<jats:sc>l<\/jats:sc>and its model-checking is decidable with a 2E<jats:sc>xp<\/jats:sc>T<jats:sc>ime<\/jats:sc>lower-bound.<\/jats:p><jats:p>It is worth enlightening that to achieve the positive results about S<jats:sc>l<\/jats:sc>[1<jats:sc>g<\/jats:sc>], we introduce a fundamental property of the semantics of this logic, called<jats:italic>behavioral<\/jats:italic>, which allows to strongly simplify the reasoning about strategies. Indeed, in a nonbehavioral logic such as S<jats:sc>l<\/jats:sc>[<jats:sc>bg<\/jats:sc>] and the subsuming ones, to satisfy a formula, one has to take into account that a move of an agent, at a given moment of a play, may depend on the moves taken by any agent in another counterfactual play.<\/jats:p>","DOI":"10.1145\/2631917","type":"journal-article","created":{"date-parts":[[2014,11,24]],"date-time":"2014-11-24T15:29:41Z","timestamp":1416842981000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":97,"title":["Reasoning About Strategies"],"prefix":"10.1145","volume":"15","author":[{"given":"Fabio","family":"Mogavero","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II, Napoli, Italy"}]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II, Napoli, Italy"}]},{"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II, Napoli, Italy"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"Rice University, Houston, Texas"}]}],"member":"320","published-online":{"date-parts":[[2014,11,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1324249.1324256"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(84)90073-8"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.11.005"},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"F. Belardinelli. 2014. Reasoning about knowledge and strategies: Epistemic strategy logic. In SR. 27--33. F. Belardinelli. 2014. Reasoning about knowledge and strategies: Epistemic strategy logic. In SR. 27--33.","DOI":"10.4204\/EPTCS.146.4"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591370.2591379"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.28"},{"key":"e_1_2_2_8_1","volume-title":"EACSL Annual Conference on Computer Science Logic\u201910","author":"Bianco A.","unstructured":"A. Bianco , F. Mogavero , and A. Murano . 2010. Graded computation tree logic with binary coding . In EACSL Annual Conference on Computer Science Logic\u201910 . Springer, 125--139. A. Bianco, F. Mogavero, and A. Murano. 2010. Graded computation tree logic with binary coding. In EACSL Annual Conference on Computer Science Logic\u201910. Springer, 125--139."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2287718.2287725"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:11)2008"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92687-0_7"},{"key":"e_1_2_2_12_1","volume-title":"International Congress on Logic, Methodology, and Philosophy of Science\u201962","author":"B\u00fcchi J. R.","year":"1962","unstructured":"J. R. B\u00fcchi . 1962 . On a decision method in restricted second-order arithmetic . In International Congress on Logic, Methodology, and Philosophy of Science\u201962 . Stanford University Press, 1--11. J. R. B\u00fcchi. 1962. On a decision method in restricted second-order arithmetic. In International Congress on Logic, Methodology, and Philosophy of Science\u201962. Stanford University Press, 1--11."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-013-9231-3"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9110-4"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"P. \u010cerm\u00e1k A. Lomuscio F. Mogavero and A. Murano. 2014. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In Computer Aided Verification\u201914. Springer 524--531. P. \u010cerm\u00e1k A. Lomuscio F. Mogavero and A. Murano. 2014. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In Computer Aided Verification\u201914. Springer 524--531.","DOI":"10.1007\/978-3-319-08867-9_34"},{"key":"e_1_2_2_16_1","volume-title":"Proceedings 1st International Workshop on Strategic Reasoning (SR\u201913)","author":"Chareton C.","unstructured":"C. Chareton , J. Brunel , and D. Chemouil . 2013. Towards an updatable strategy logic . In Proceedings 1st International Workshop on Strategic Reasoning (SR\u201913) , F. Mogavero, A. Murano, and M. Y. Vardi (Eds.). 91--98. C. Chareton, J. Brunel, and D. Chemouil. 2013. Towards an updatable strategy logic. In Proceedings 1st International Workshop on Strategic Reasoning (SR\u201913), F. Mogavero, A. Murano, and M. Y. Vardi (Eds.). 91--98."},{"key":"e_1_2_2_17_1","volume-title":"VMCAI","author":"Chatterjee K.","year":"2014","unstructured":"K. Chatterjee , L. Doyen , E. Filiot , and J. F. Raskin . 2014. Doomsday equilibria for omega-regular games . In VMCAI 2014 . Springer, 78--97. K. Chatterjee, L. Doyen, E. Filiot, and J. F. Raskin. 2014. Doomsday equilibria for omega-regular games. In VMCAI 2014. Springer, 78--97."},{"key":"e_1_2_2_18_1","volume-title":"International Conference on Concurrency Theory\u201907","author":"Chatterjee K.","unstructured":"K. Chatterjee , T. A. Henzinger , and N. Piterman . 2007. Strategy logic . In International Conference on Concurrency Theory\u201907 . Springer, 59--73. K. Chatterjee, T. A. Henzinger, and N. Piterman. 2007. Strategy logic. In International Conference on Concurrency Theory\u201907. Springer, 59--73."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.07.004"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and E. A. Emerson. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs\u201981. Springer 52--71. E. M. Clarke and E. A. Emerson. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs\u201981. Springer 52--71.","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_2_21_1","unstructured":"E. M. Clarke O. Grumberg and D. A. Peled. 2002. Model Checking. MIT Press. E. M. Clarke O. Grumberg and D. A. Peled. 2002. Model Checking. MIT Press."},{"key":"e_1_2_2_22_1","volume-title":"IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science\u201910","author":"Da Costa A.","unstructured":"A. Da Costa , F. Laroussinie , and N. Markey . 2010a. ATL with strategy contexts: Expressiveness and model checking . In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science\u201910 . 120--132. A. Da Costa, F. Laroussinie, and N. Markey. 2010a. ATL with strategy contexts: Expressiveness and model checking. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science\u201910. 120--132."},{"key":"e_1_2_2_23_1","unstructured":"A. Da Costa F. Laroussinie and N. Markey. 2010b. Personal communication. A. Da Costa F. Laroussinie and N. Markey. 2010b. Personal communication."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_14"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"H. D. Ebbinghaus and J. Flum. 1995. Finite Model Theory. Springer-Verlag. H. D. Ebbinghaus and J. Flum. 1995. Finite Model Theory. Springer-Verlag.","DOI":"10.1007\/3-540-28788-4"},{"key":"e_1_2_2_26_1","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E. A.","unstructured":"E. A. Emerson . 1990. Temporal and modal logic . In Handbook of Theoretical Computer Science , vol. B. MIT Press, 995-- 1072 . E. A. Emerson. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, vol. B. MIT Press, 995--1072."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"R. Fagin J. Y. Halpern Y. Moses and M. Y. Vardi. 1995. Reasoning About Knowledge. MIT Press. R. Fagin J. Y. Halpern Y. Moses and M. Y. Vardi. 1995. Reasoning About Knowledge. MIT Press.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"A. Ferrante A. Murano and M. Parente. 2008. Enriched &mu;-calculi module checking. Logical Methods Comput. Sci. 4 3 (2008). A. Ferrante A. Murano and M. Parente. 2008. Enriched &mu;-calculi module checking. Logical Methods Comput. Sci. 4 3 (2008).","DOI":"10.2168\/LMCS-4(3:1)2008"},{"key":"e_1_2_2_30_1","volume-title":"EACSL Annual Conference on Computer Science Logic\u201910","author":"Finkbeiner B.","unstructured":"B. Finkbeiner and S. Schewe . 2010. Coordination logic . In EACSL Annual Conference on Computer Science Logic\u201910 . Springer, 305--319. B. Finkbeiner and S. Schewe. 2010. Coordination logic. In EACSL Annual Conference on Computer Science Logic\u201910. Springer, 305--319."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_16"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"E. Gr\u00e4del W. Thomas and T. Wilke. 2002. Automata Logics and Infinite Games: A Guide to Current Research. Springer-Verlag. E. Gr\u00e4del W. Thomas and T. Wilke. 2002. Automata Logics and Infinite Games: A Guide to Current Research. Springer-Verlag.","DOI":"10.1007\/3-540-36387-4"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"A. Herzig E. Lorini and D. Walther. 2013. Reasoning about actions meets strategic logics. In Logic Rationality and Interaction. Springer 162--175. A. Herzig E. Lorini and D. Walther. 2013. Reasoning about actions meets strategic logics. In Logic Rationality and Interaction. Springer 162--175.","DOI":"10.1007\/978-3-642-40948-6_13"},{"key":"e_1_2_2_34_1","volume-title":"Model Theory","author":"Hodges W.","unstructured":"W. Hodges . 1993. Model Theory . Cambridge University Press . W. Hodges. 1993. Model Theory. Cambridge University Press."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9833-0_1"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_11"},{"key":"e_1_2_2_37_1","unstructured":"W. Jamroga and A. Murano. 2014. On module checking and strategies. In AAMAS. IFAAMAS 701--708. W. Jamroga and A. Murano. 2014. On module checking and strategies. In AAMAS. IFAAMAS 701--708."},{"key":"e_1_2_2_38_1","first-page":"2","article-title":"Agents that know how to play","volume":"63","author":"Jamroga W.","year":"2004","unstructured":"W. Jamroga and W. van der Hoek . 2004 . Agents that know how to play . Fundamenta Informaticae 63 , 2 -- 3 (2004), 185--219. W. Jamroga and W. van der Hoek. 2004. Agents that know how to play. Fundamenta Informaticae 63, 2--3 (2004), 185--219.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_2_2_40_1","volume-title":"Handbook of Model-Theoretic Logics","author":"Kolaitis F.","unstructured":"F. Kolaitis . 1985. Game quantification . In Handbook of Model-Theoretic Logics , J. Barwise and S. Feferman (Eds.). SpringerVerlag , 365--421. F. Kolaitis. 1985. Game quantification. In Handbook of Model-Theoretic Logics, J. Barwise and S. Feferman (Eds.). SpringerVerlag, 365--421."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_2_42_1","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"Kripke S. A.","year":"1963","unstructured":"S. A. Kripke . 1963 . Semantical considerations on modal logic . Acta Philosophica Fennica 16 (1963), 83 -- 94 . S. A. Kripke. 1963. Semantical considerations on modal logic. Acta Philosophica Fennica 16 (1963), 83--94.","journal-title":"Acta Philosophica Fennica"},{"key":"e_1_2_2_43_1","volume-title":"Conference on Automated Deduction\u201902","author":"Kupferman O.","unstructured":"O. Kupferman , U. Sattler , and M. Y. Vardi . 2002. The complexity of the graded &mu;-calculus . In Conference on Automated Deduction\u201902 . Springer, 423--437. O. Kupferman, U. Sattler, and M. Y. Vardi. 2002. The complexity of the graded &mu;-calculus. In Conference on Automated Deduction\u201902. Springer, 423--437."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/276698.276748"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2893"},{"key":"e_1_2_2_47_1","first-page":"208","article-title":"Satisfiability of ATL with strategy contexts","volume":"119","author":"Laroussinie F.","year":"2013","unstructured":"F. Laroussinie and N. Markey . 2013 . Satisfiability of ATL with strategy contexts . In GandALF (EPTCS) , Vol. 119. 208 -- 223 . F. Laroussinie and N. Markey. 2013. Satisfiability of ATL with strategy contexts. In GandALF (EPTCS), Vol. 119. 208--223.","journal-title":"GandALF (EPTCS)"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.2307\/1971035"},{"key":"e_1_2_2_49_1","volume-title":"Symposia in Pure Mathematics\u201982 (Recursion Theory)","author":"Martin A. D.","unstructured":"A. D. Martin . 1985. A purely inductive proof of Borel determinacy . In Symposia in Pure Mathematics\u201982 (Recursion Theory) . American Mathematical Society and Association for Symbolic Logic , 303--308. A. D. Martin. 1985. A purely inductive proof of Borel determinacy. In Symposia in Pure Mathematics\u201982 (Recursion Theory). American Mathematical Society and Association for Symbolic Logic, 303--308."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_15"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.32"},{"key":"e_1_2_2_52_1","doi-asserted-by":"crossref","unstructured":"F. Mogavero A. Murano and L. Sauro. 2014a. A behavioral hierarchy of strategy logic. In CLIMA XV. Springer 148--165. F. Mogavero A. Murano and L. Sauro. 2014a. A behavioral hierarchy of strategy logic. In CLIMA XV. Springer 148--165.","DOI":"10.1007\/978-3-319-09764-0_10"},{"key":"e_1_2_2_53_1","unstructured":"F. Mogavero A. Murano and L. Sauro. 2014b. Strategy games: A renewed framework. In AAMAS. IFAAMAS 869--876. F. Mogavero A. Murano and L. Sauro. 2014b. Strategy games: A renewed framework. In AAMAS. IFAAMAS 869--876."},{"key":"e_1_2_2_54_1","volume-title":"IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science\u201910","author":"Mogavero F.","unstructured":"F. Mogavero , A. Murano , and M. Y. Vardi . 2010a. Reasoning about strategies . In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science\u201910 . 133--144. F. Mogavero, A. Murano, and M. Y. Vardi. 2010a. Reasoning about strategies. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science\u201910. 133--144."},{"key":"e_1_2_2_55_1","volume-title":"International Conference on Logic for Programming Artificial Intelligence and Reasoning\u201910","author":"Mogavero F.","unstructured":"F. Mogavero , A. Murano , and M. Y. Vardi . 2010b. Relentful strategic reasoning in alternating-time temporal logic . In International Conference on Logic for Programming Artificial Intelligence and Reasoning\u201910 . Springer, 371--387. F. Mogavero, A. Murano, and M. Y. Vardi. 2010b. Relentful strategic reasoning in alternating-time temporal logic. In International Conference on Logic for Programming Artificial Intelligence and Reasoning\u201910. Springer, 371--387."},{"key":"e_1_2_2_56_1","volume-title":"IEEE Symposium on Logic in Computer Science\u201988","author":"Muller D. E.","unstructured":"D. E. Muller , A. Saoudi , and P. E. Schupp . 1988. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time . In IEEE Symposium on Logic in Computer Science\u201988 . IEEE Computer Society, 422--427. D. E. Muller, A. Saoudi, and P. E. Schupp. 1988. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In IEEE Symposium on Logic in Computer Science\u201988. IEEE Computer Society, 422--427."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90133-2"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00214-4"},{"key":"e_1_2_2_59_1","volume-title":"Game Theory: Analysis of Conflict","author":"Myerson R. B.","year":"1997","unstructured":"R. B. Myerson . 1997 . Game Theory: Analysis of Conflict . Harvard University Press . R. B. Myerson. 1997. Game Theory: Analysis of Conflict. Harvard University Press."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.1.149"},{"key":"e_1_2_2_61_1","volume-title":"Infinite Words. Pure and Applied Mathematics","volume":"141","author":"Perrin D.","unstructured":"D. Perrin and J. Pin . 2004 . Infinite Words. Pure and Applied Mathematics , Vol. 141 . Elsevier. D. Perrin and J. Pin. 2004. Infinite Words. Pure and Applied Mathematics, Vol. 141. Elsevier."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779046.1779067"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_64_1","volume-title":"International Symposium on Programming\u201981","author":"Queille J. P.","unstructured":"J. P. Queille and J. Sifakis . 1981. Specification and verification of concurrent programs in CESAR . In International Symposium on Programming\u201981 . Springer, 337--351. J. P. Queille and J. Sifakis. 1981. Specification and verification of concurrent programs in CESAR. In International Symposium on Programming\u201981. Springer, 337--351."},{"key":"e_1_2_2_65_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin M. O.","year":"1969","unstructured":"M. O. Rabin . 1969 . Decidability of second-order theories and automata on infinite trees . Trans. Am. Math. Soc. 141 (1969), 1 -- 35 . M. O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141 (1969), 1--35.","journal-title":"Trans. Am. Math. Soc."},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_31"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_2_2_69_1","volume-title":"Handbook of Theoretical Computer Science","author":"Thomas W.","unstructured":"W. Thomas . 1990. Automata on infinite objects . In Handbook of Theoretical Computer Science , vol. B. MIT Press, 133-- 191 . W. Thomas. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, vol. B. MIT Press, 133--191."},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73582"},{"key":"e_1_2_2_71_1","volume-title":"Why is modal logic so robustly decidable&quest","author":"Vardi M. Y.","unstructured":"M. Y. Vardi . 1996. Why is modal logic so robustly decidable&quest ; In Descriptive Complexity and Finite Models\u201996. American Mathematical Society , 149--184. M. Y. Vardi. 1996. Why is modal logic so robustly decidable&quest; In Descriptive Complexity and Finite Models\u201996. American Mathematical Society, 149--184."},{"key":"e_1_2_2_72_1","volume-title":"IEEE Symposium on Logic in Computer Science\u201986","author":"Vardi M. Y.","unstructured":"M. Y. Vardi and P. Wolper . 1986. An automata-theoretic approach to automatic program verification . In IEEE Symposium on Logic in Computer Science\u201986 . IEEE Computer Society, 332--344. M. Y. Vardi and P. Wolper. 1986. An automata-theoretic approach to automatic program verification. In IEEE Symposium on Logic in Computer Science\u201986. IEEE Computer Society, 332--344."},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1324249.1324285"},{"key":"e_1_2_2_74_1","volume-title":"CONCUR","author":"Wang F.","year":"2011","unstructured":"F. Wang , C. Huang , and F. Yu . 2011. A temporal logic for the interaction of strategies . In CONCUR 2011 . Springer, 466--481. F. Wang, C. Huang, and F. Yu. 2011. A temporal logic for the interaction of strategies. In CONCUR 2011. Springer, 466--481."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631917","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2631917","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:13Z","timestamp":1750231153000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631917"}},"subtitle":["On the Model-Checking Problem"],"short-title":[],"issued":{"date-parts":[[2014,8]]},"references-count":73,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["10.1145\/2631917"],"URL":"https:\/\/doi.org\/10.1145\/2631917","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8]]},"assertion":[{"value":"2012-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-11-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}