{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T04:17:55Z","timestamp":1751948275296,"version":"3.41.2"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T00:00:00Z","timestamp":1532995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Union's Horizon 2020 research and innovation programme","award":["EPS313360"],"award-info":[{"award-number":["EPS313360"]}]},{"name":"ANR for the project EQINOCS","award":["ANR-11-BS02-004"],"award-info":[{"award-number":["ANR-11-BS02-004"]}]},{"name":"European Research Council"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,7,31]]},"abstract":"<jats:p>We revisit Janin and Walukiewicz\u2019s classic result on the expressive completeness of the modal mu-calculus with respect to Monadic Second Order Logic (MSO), which is where the mu-calculus corresponds precisely to the fragment of MSO that is invariant under bisimulation. We show that adding binary relations over finite paths in the picture may alter the situation. We consider a general setting where finite paths of transition systems are linked by means of a fixed binary relation. This setting gives rise to natural extensions of MSO and the mu-calculus, that we call the MSO<jats:italic>with paths relation<\/jats:italic>and the<jats:italic>jumping mu-calculus<\/jats:italic>, the expressivities of which we aim at comparing. We first show that \u201cbounded-memory\u201d binary relations bring about no additional expressivity to either of the two logics, and thus preserve expressive completeness. In contrast, we show that for a natural, classic \u201cinfinite-memory\u201d binary relation stemming from games with imperfect information, the existence of a winning strategy in such games, though expressible in the bisimulation-invariant fragment of MSO with paths relation, cannot be expressed in the jumping mu-calculus. Expressive completeness thus fails for this relation. These results crucially rely on our observation that the jumping mu-calculus has a tree automata counterpart: the<jats:italic>jumping tree automata<\/jats:italic>, hence the name of the jumping mu-calculus. We also prove that for<jats:italic>observable<\/jats:italic>winning conditions, the existence of winning strategies in games with imperfect information is expressible in the jumping mu-calculus. Finally, we derive from our main theorem that jumping automata cannot be projected, and ATL with imperfect information does not admit expansion laws.<\/jats:p>","DOI":"10.1145\/3231596","type":"journal-article","created":{"date-parts":[[2018,9,19]],"date-time":"2018-09-19T11:58:41Z","timestamp":1537358321000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Relating Paths in Transition Systems"],"prefix":"10.1145","volume":"19","author":[{"given":"Catalin","family":"Dima","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris-Est, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9081-2920","authenticated-orcid":false,"given":"Bastien","family":"Maubert","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli \u201cFederico II\u201d, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sophie","family":"Pinchinat","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Rennes 1, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,9,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"R. Alur P. \u010cern\u00fd and S. Chaudhuri. 2007. Model checking on trees with path equivalences. In TACAS\u201907. Springer 664--678. R. Alur P. \u010cern\u00fd and S. Chaudhuri. 2007. Model checking on trees with path equivalences. In TACAS\u201907. Springer 664--678.","DOI":"10.1007\/978-3-540-71209-1_51"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"volume-title":"Transductions and Context-Free Languages","author":"Berstel J.","key":"e_1_2_1_3_1","unstructured":"J. Berstel . 1979. Transductions and Context-Free Languages , Vol. 4 . Teubner Stuttgart . J. Berstel. 1979. Transductions and Context-Free Languages, Vol. 4. Teubner Stuttgart."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.09.006"},{"key":"e_1_2_1_5_1","unstructured":"D. Berwanger and L. Doyen. 2008. On the power of imperfect information. In FSTTCS. 73--82. D. Berwanger and L. Doyen. 2008. On the power of imperfect information. In FSTTCS. 73--82."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-009-9115-8"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.014"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"N. Bulling J. Dix and W. Jamroga. 2010. Model checking logics of strategic ability: Complexity. In Specification and Verification of Multi-Agent Systems M. Dastani K. V. Hindriks and J.-J. C. Meyer (Eds.). Springer 125--160. N. Bulling J. Dix and W. Jamroga. 2010. Model checking logics of strategic ability: Complexity. In Specification and Verification of Multi-Agent Systems M. Dastani K. V. Hindriks and J.-J. C. Meyer (Eds.). Springer 125--160.","DOI":"10.1007\/978-1-4419-6984-2_5"},{"volume-title":"Proceedings of IJCAI \u201911","author":"Bulling N.","key":"e_1_2_1_9_1","unstructured":"N. Bulling and W. Jamroga . 2011. Alternating epistemic mu-calculus . In Proceedings of IJCAI \u201911 . IJCAI\/AAAI, 109--114. N. Bulling and W. Jamroga. 2011. Alternating epistemic mu-calculus. In Proceedings of IJCAI \u201911. IJCAI\/AAAI, 109--114."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 21st European Conference on Artificial Intelligence (ECAI\u201914)","author":"Bulling Nils","year":"2014","unstructured":"Nils Bulling , Wojciech Jamroga , and Matei Popovici . 2014 . ATL* with truly perfect recall: Expressivity and validities . In Proceedings of the 21st European Conference on Artificial Intelligence (ECAI\u201914) , 18-22 August 2014, Prague, Czech Republic\u2014Including Prestigious Applications of Intelligent Systems (PAIS\u201914). 177--182. Nils Bulling, Wojciech Jamroga, and Matei Popovici. 2014. ATL* with truly perfect recall: Expressivity and validities. In Proceedings of the 21st European Conference on Artificial Intelligence (ECAI\u201914), 18-22 August 2014, Prague, Czech Republic\u2014Including Prestigious Applications of Intelligent Systems (PAIS\u201914). 177--182."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00089-5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee and L. Doyen. 2010. The complexity of partial-observation parity games. In LPAR 17. Springer 1--14. K. Chatterjee and L. Doyen. 2010. The complexity of partial-observation parity games. In LPAR 17. Springer 1--14.","DOI":"10.1007\/978-3-642-16242-8_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579821"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2011.07.001"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"B. Courcelle and J. Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic\u2014A Language-Theoretic Approach. Cambridge University Press. http:\/\/www.cambridge.org\/fr\/knowledge\/isbn\/item5758776\/?site_locale&equals;fr_FR. B. Courcelle and J. Engelfriet. 2012. Graph Structure and Monadic Second-Order Logic\u2014A Language-Theoretic Approach. Cambridge University Press. http:\/\/www.cambridge.org\/fr\/knowledge\/isbn\/item5758776\/?site_locale&equals;fr_FR.","DOI":"10.1017\/CBO9780511977619"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_26"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48057-1_14"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"S. Dziembowski M. Jurdzinski and I. Walukiewicz. 1997. How much memory is needed to win infinite games? In LICS. IEEE 99--110. S. Dziembowski M. Jurdzinski and I. Walukiewicz. 1997. How much memory is needed to win infinite games? In LICS. IEEE 99--110.","DOI":"10.1109\/LICS.1997.614939"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269808"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793304741"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"R. Fagin J. Halpern Y. Moses and M. Vardi. 2004. Reasoning About Knowledge. The MIT Press. R. Fagin J. Halpern Y. Moses and M. Vardi. 2004. Reasoning About Knowledge. The MIT Press.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/938135"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539797320906"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90039-1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.17.423-475"},{"volume-title":"Proceedings of CONCUR\u201996","author":"Janin D.","key":"e_1_2_1_27_1","unstructured":"D. Janin and I. Walukiewicz . 1996. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic . In Proceedings of CONCUR\u201996 . Springer, 263--277. D. Janin and I. Walukiewicz. 1996. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In Proceedings of CONCUR\u201996. Springer, 263--277."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.12.020"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.193.4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273878"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_31"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.2955"},{"volume-title":"Proceedings of FSTTCS\u201913","author":"Maubert B.","key":"e_1_2_1_35_1","unstructured":"B. Maubert and S. Pinchinat . 2013. Jumping automata for uniform strategies . In Proceedings of FSTTCS\u201913 . 287--298. B. Maubert and S. Pinchinat. 2013. Jumping automata for uniform strategies. In Proceedings of FSTTCS\u201913. 287--298."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00214-4"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647210.720030"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1885577.1885629"},{"key":"e_1_2_1_40_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. Amer. Math. Soc. 141 (1969), 1 -- 35 . M. O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141 (1969), 1--35.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_1_41_1","first-page":"287","article-title":"Algorithms for omega-regular games with imperfect information","volume":"3","author":"Raskin Jean-Fran\u00e7ois","year":"2007","unstructured":"Jean-Fran\u00e7ois Raskin , Krishnendu Chatterjee , Laurent Doyen , and Thomas A. Henzinger . 2007 . Algorithms for omega-regular games with imperfect information . LMCS 3 , 3 (2007), 287 -- 302 . Jean-Fran\u00e7ois Raskin, Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. 2007. Algorithms for omega-regular games with imperfect information. LMCS 3, 3 (2007), 287--302.","journal-title":"LMCS"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90034-5"},{"key":"e_1_2_1_43_1","volume-title":"Distributed graph automata. CoRR abs\/1404.6503","author":"Reiter F.","year":"2014","unstructured":"F. Reiter . 2014. Distributed graph automata. CoRR abs\/1404.6503 ( 2014 ). http:\/\/arxiv.org\/abs\/1404.6503 F. Reiter. 2014. Distributed graph automata. CoRR abs\/1404.6503 (2014). http:\/\/arxiv.org\/abs\/1404.6503"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00168-5"},{"key":"e_1_2_1_45_1","unstructured":"N. V. Shilov and N. O. Garanina. 2002. Combining Knowledge and Fixpoints. Technical Report Preprint n.98 http:\/\/www.iis.nsk.su\/files\/preprints\/098.pdf. A.P. Ershov Institute of Informatics Systems Novosibirsk. N. V. Shilov and N. O. Garanina. 2002. Combining Knowledge and Fixpoints. Technical Report Preprint n.98 http:\/\/www.iis.nsk.su\/files\/preprints\/098.pdf. A.P. Ershov Institute of Informatics Systems Novosibirsk."},{"key":"e_1_2_1_46_1","first-page":"1","article-title":"Update and abstraction in model checking of knowledge and branching time","volume":"72","author":"Shilov Nikolay V.","year":"2006","unstructured":"Nikolay V. Shilov , Natalya Olegovna Garanina , and K.-M. Choe . 2006 . Update and abstraction in model checking of knowledge and branching time . Fundam. Inform. 72 , 1 -- 3 (2006), 347--361. Nikolay V. Shilov, Natalya Olegovna Garanina, and K.-M. Choe. 2006. Update and abstraction in model checking of knowledge and branching time. Fundam. Inform. 72, 1--3 (2006), 347--361.","journal-title":"Fundam. Inform."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1134\/S036176881604006X"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90090-3"},{"volume-title":"Handbook of Formal Languages, Beyond Words","author":"Thomas W.","key":"e_1_2_1_49_1","unstructured":"W. Thomas . 1997. Languages , automata, and logic . In Handbook of Formal Languages, Beyond Words , Vol. 3 , G. Rozenberg and A. Salomaa (Eds.). Springer Verlag , 389--455. W. Thomas. 1997. Languages, automata, and logic. In Handbook of Formal Languages, Beyond Words, Vol. 3, G. Rozenberg and A. Salomaa (Eds.). Springer Verlag, 389--455."},{"volume-title":"Handbook of Philosophical Logic","author":"Benthem Johan Van","key":"e_1_2_1_50_1","unstructured":"Johan Van Benthem . 1984. Correspondence theory . In Handbook of Philosophical Logic . Springer , 167--247. Johan Van Benthem. 1984. Correspondence theory. In Handbook of Philosophical Logic. Springer, 167--247."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of FSTTCS\u201999 (LNCS)","volume":"1738","author":"van der Meyden R.","unstructured":"R. van der Meyden and N. Shilov . 1999. Model checking knowledge and time in systems with perfect recall (extended abstract) . In Proceedings of FSTTCS\u201999 (LNCS) , Vol. 1738 . 432--445. R. van der Meyden and N. Shilov. 1999. Model checking knowledge and time in systems with perfect recall (extended abstract). In Proceedings of FSTTCS\u201999 (LNCS), Vol. 1738. 432--445."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/646252.685998"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00185-2"},{"key":"e_1_2_1_54_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\/3231596","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3231596","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,7]],"date-time":"2025-07-07T21:35:11Z","timestamp":1751924111000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3231596"}},"subtitle":["The Fall of the Modal Mu-Calculus"],"short-title":[],"issued":{"date-parts":[[2018,7,31]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,7,31]]}},"alternative-id":["10.1145\/3231596"],"URL":"https:\/\/doi.org\/10.1145\/3231596","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,7,31]]},"assertion":[{"value":"2017-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-09-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}