{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:34Z","timestamp":1760202694329,"version":"3.41.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,7,1]],"date-time":"2015-07-01T00:00:00Z","timestamp":1435708800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"IndAM 2013 project &ldquo;Logiche di Gioco Estese,&rdquo;"},{"name":"FP7 European Union project 600958-SHERPA"},{"name":"Embedded System Cup Project B25B09090100007 (POR Campania FSE 2007\/2013, asse IV e asse V)"},{"name":"Italian Ministry of University and Research"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,7,8]]},"abstract":"<jats:p>Many decision problems in formal verification and design can be suitably formulated in game-theoretic terms. This is the case for the model checking of open and closed systems and both controller and reactive synthesis. Interpreted in this context, these problems require one to find a strategy (i.e., a plan) to force the system to fulfill some desired goal, no matter what the opponent (e.g., the environment) does. A strategy essentially constrains the possible behaviors of the system to those that are compatible with the decisions dictated by the plan itself. Therefore, finding a strategy to meet some goal basically reduces to identifying a portion of the model of interest (i.e., one of its substructures) that satisfies that goal. In this view, the ability to reason about substructures becomes a crucial aspect for several fundamental problems.<\/jats:p>\n          <jats:p>In this article, we present and study a new branching-time temporal logic, called Substructure Temporal Logic (STL * for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. The logic is obtained by adding four new temporal-like operators to CTL *, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL * turns out to be very expressive and allows one to capture in a very natural way many well-known problems, such as module checking, reactive synthesis, and reasoning about games in a wide sense. A formal account of the model-theoretic properties of the new logic and results about (un)decidability and complexity of related decision problems are also provided.<\/jats:p>","DOI":"10.1145\/2757286","type":"journal-article","created":{"date-parts":[[2015,7,6]],"date-time":"2015-07-06T14:04:16Z","timestamp":1436191456000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Reasoning About Substructures and Games"],"prefix":"10.1145","volume":"16","author":[{"given":"Massimo","family":"Benerecetti","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II"}]},{"given":"Fabio","family":"Mogavero","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II"}]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli Federico II"}]}],"member":"320","published-online":{"date-parts":[[2015,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0165-1765(00)00371-2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591370.2591379"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:11)2008"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee T. A. Henzinger and N. Piterman. 2007. Strategy logic. In Concurrency Theory \u201907 (LNCS 4703). Springer 59--73.   K. Chatterjee T. A. Henzinger and N. Piterman. 2007. Strategy logic. In Concurrency Theory \u201907 (LNCS 4703). Springer 59--73.","DOI":"10.1007\/978-3-540-74407-8_5"},{"key":"e_1_2_1_6_1","volume-title":"International Congress of Mathematicians \u201962","author":"Church A.","year":"1963","unstructured":"A. Church . 1963 . Logic, arithmetics, and automata . In International Congress of Mathematicians \u201962 . 23--35. A. Church. 1963. Logic, arithmetics, and automata. In International Congress of Mathematicians \u201962. 23--35."},{"key":"e_1_2_1_7_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 (LNCS 131). 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 (LNCS 131). Springer 52--71.","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_9_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_1_10_1","volume-title":"Graph Theory","author":"Diestel R.","unstructured":"R. Diestel . 2012. Graph Theory ( 4 th ed.). Graduate Texts in Mathematics, Vol. 173 . Springer . R. Diestel. 2012. Graph Theory (4th ed.). Graduate Texts in Mathematics, Vol. 173. Springer.","edition":"4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/22587.22589"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and A. P. Sistla. 1983. Deciding branching time logic: A triple exponential decision procedure for CTL&star;. In Logic of Programs \u201983 (LNCS 164). Springer 176--192.   E. A. Emerson and A. P. Sistla. 1983. Deciding branching time logic: A triple exponential decision procedure for CTL&star;. In Logic of Programs \u201983 (LNCS 164). Springer 176--192.","DOI":"10.1007\/3-540-12896-4_363"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"N. Francez. 1986. Fairness. Springer.   N. Francez. 1986. Fairness. Springer.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008222603071"},{"key":"e_1_2_1_17_1","unstructured":"J. Gutierrez P. Harrenstein and M. Wooldridge. 2014. Reasoning about equilibria in game-like concurrent systems. In Knowledge Representation and Reasoning \u201914. AAAI Press.  J. Gutierrez P. Harrenstein and M. Wooldridge. 2014. Reasoning about equilibria in game-like concurrent systems. In Knowledge Representation and Reasoning \u201914. AAAI Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"T. Hafer and W. Thomas. 1987. Computation tree logic CTL &star; and path quantifiers in the monadic theory of the binary tree. In International Colloquium on Automata Languages and Programming \u201987 (LNCS 267). Springer 269--279.   T. Hafer and W. Thomas. 1987. Computation tree logic CTL &star; and path quantifiers in the monadic theory of the binary tree. In International Colloquium on Automata Languages and Programming \u201987 (LNCS 267). Springer 269--279.","DOI":"10.1007\/3-540-18088-5_22"},{"key":"e_1_2_1_19_1","volume-title":"Logic and Computation Conference \u201984","author":"Harel D.","year":"1984","unstructured":"D. Harel . 1984 . A simple highly undecidable domino problem . In Logic and Computation Conference \u201984 . North-Holland, 177--194. D. Harel. 1984. A simple highly undecidable domino problem. In Logic and Computation Conference \u201984. North-Holland, 177--194."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90039-8"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"B. Khoussainov and A. Nerode. 2001. Automata Theory and Its Applications. Birkhauser.   B. Khoussainov and A. Nerode. 2001. Automata Theory and Its Applications. Birkhauser.","DOI":"10.1007\/978-1-4612-0171-7"},{"key":"e_1_2_1_23_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"},{"volume-title":"Conference on Automated Deduction \u201902 (LNCS 2392)","author":"Kupferman O.","key":"e_1_2_1_24_1","unstructured":"O. Kupferman , U. Sattler , and M. Y. Vardi . 2002. The complexity of the graded muCalculus . In Conference on Automated Deduction \u201902 (LNCS 2392) . Springer, 423--437. O. Kupferman, U. Sattler, and M. Y. Vardi. 2002. The complexity of the graded muCalculus. In Conference on Automated Deduction \u201902 (LNCS 2392). Springer, 423--437."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2893"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567463"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"C. L\u00f6ding and P. Rohde. 2003. Model checking and satisfiability for sabotage modal logic. In Foundations of Software Technology and Theoretical Computer Science \u201903 (LNCS 2914). Springer 302--313.  C. L\u00f6ding and P. Rohde. 2003. Model checking and satisfiability for sabotage modal logic. In Foundations of Software Technology and Theoretical Computer Science \u201903 (LNCS 2914). Springer 302--313.","DOI":"10.1007\/978-3-540-24597-1_26"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02737-6_32"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_15"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2631917"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.32"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"F. Mogavero A. Murano and L. Sauro. 2014. A behavioral hierarchy of strategy logic. In Computational Logic in Multi-Agent Systems \u201914 (LNCS 8624). Springer 148--165.  F. Mogavero A. Murano and L. Sauro. 2014. A behavioral hierarchy of strategy logic. In Computational Logic in Multi-Agent Systems \u201914 (LNCS 8624). Springer 148--165.","DOI":"10.1007\/978-3-319-09764-0_10"},{"key":"e_1_2_1_34_1","unstructured":"F. Mogavero A. Murano and M. Y. Vardi. 2010. Reasoning about strategies. In Foundations of Software Technology and Theoretical Computer Science \u201910 (LIPIcs 8). Leibniz-Zentrum fuer Informatik 133--144.  F. Mogavero A. Murano and M. Y. Vardi. 2010. Reasoning about strategies. In Foundations of Software Technology and Theoretical Computer Science \u201910 (LIPIcs 8). Leibniz-Zentrum fuer Informatik 133--144."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00104-4"},{"key":"e_1_2_1_36_1","unstructured":"M. J. Osborne and A. Rubinstein. 1994. A Course in Game Theory. MIT Press.  M. J. Osborne and A. Rubinstein. 1994. A Course in Game Theory. MIT Press."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-007-9168-7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"volume-title":"Symposium on Programming \u201981 (LNCS 137)","author":"Queille J. P.","key":"e_1_2_1_41_1","unstructured":"J. P. Queille and J. Sifakis . 1981. Specification and verification of concurrent programs in Cesar . In Symposium on Programming \u201981 (LNCS 137) . Springer, 337--351. J. P. Queille and J. Sifakis. 1981. Specification and verification of concurrent programs in Cesar. In Symposium on Programming \u201981 (LNCS 137). Springer, 337--351."},{"key":"e_1_2_1_42_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 . Transactions of the American Mathematics Society 141 (1969), 1 -- 35 . M. O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematics Society 141 (1969), 1--35.","journal-title":"Transactions of the American Mathematics Society"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516510"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82604-0"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/800125.804029"},{"volume-title":"Mechanizing Mathematical Reasoning \u201905 (LNCS 2605)","author":"van Benthem J.","key":"e_1_2_1_48_1","unstructured":"J. van Benthem . 2005. An essay on sabotage and obstruction . In Mechanizing Mathematical Reasoning \u201905 (LNCS 2605) . Springer , 268--276. J. van Benthem. 2005. An essay on sabotage and obstruction. In Mechanizing Mathematical Reasoning \u201905 (LNCS 2605). Springer, 268--276."},{"volume-title":"Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models \u201996","author":"Vardi M. Y.","key":"e_1_2_1_49_1","unstructured":"M. Y. Vardi . 1996. Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models \u201996 . American Mathematical Society , 149--184. M. Y. Vardi. 1996. Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models \u201996. American Mathematical Society, 149--184."},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"S. Vester. 2013. Alternating-time temporal logic with finite-memory strategies. In Games Automata Logics and Formal Verification \u201913 (EPTCS 119). 194--207.  S. Vester. 2013. Alternating-time temporal logic with finite-memory strategies. In Games Automata Logics and Formal Verification \u201913 (EPTCS 119). 194--207.","DOI":"10.4204\/EPTCS.119.17"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1961.tb03975.x"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2757286","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2757286","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:27Z","timestamp":1750227387000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2757286"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,7,8]]}},"alternative-id":["10.1145\/2757286"],"URL":"https:\/\/doi.org\/10.1145\/2757286","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2015,7]]},"assertion":[{"value":"2014-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}