{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:28:13Z","timestamp":1750220893016,"version":"3.41.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2020,3,2]],"date-time":"2020-03-02T00:00:00Z","timestamp":1583107200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"CE-ITI"},{"name":"CONICYT, PIA\/Concurso Apoyo a Centros Cient\u00edficos y Tecnol\u00f3gicos de Excelencia con Financiamiento Basal","award":["AFB170001"],"award-info":[{"award-number":["AFB170001"]}]},{"name":"LEA STRUCO","award":["P202\/12\/G061"],"award-info":[{"award-number":["P202\/12\/G061"]}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["648527, ERCCZ LL-1201, 665778"],"award-info":[{"award-number":["648527, ERCCZ LL-1201, 665778"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["UMO-2015\/19\/P\/ST6\/03998"],"award-info":[{"award-number":["UMO-2015\/19\/P\/ST6\/03998"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2020,4,30]]},"abstract":"<jats:p>We study the model-checking problem for first- and monadic second-order logic on finite relational structures. The problem of verifying whether a formula of these logics is true on a given structure is considered intractable in general, but it does become tractable on interesting classes of structures, such as on classes whose Gaifman graphs have bounded treewidth. In this article, we continue this line of research and study model-checking for first- and monadic second-order logic in the presence of an ordering on the input structure. We do so in two settings: the general ordered case, where the input structures are equipped with a fixed order or successor relation, and the order-invariant case, where the formulas may resort to an ordering, but their truth must be independent of the particular choice of order. In the first setting we show very strong intractability results for most interesting classes of structures. In contrast, in the order-invariant case we obtain tractability results for order-invariant monadic second-order formulas on the same classes of graphs as in the unordered case. For first-order logic, we obtain tractability of successor-invariant formulas on classes whose Gaifman graphs have bounded expansion. Furthermore, we show that model-checking for order-invariant first-order formulas is tractable on coloured posets of bounded width.<\/jats:p>","DOI":"10.1145\/3360011","type":"journal-article","created":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T06:51:02Z","timestamp":1583218262000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Model-Checking on Ordered Structures"],"prefix":"10.1145","volume":"21","author":[{"given":"Kord","family":"Eickmeyer","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt, Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan van den","family":"Heuvel","sequence":"additional","affiliation":[{"name":"London School of Economics and Political Science, Houghton Street, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ken-Ichi","family":"Kawarabayashi","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Hitotsubashi, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Kreutzer","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrice Ossona De","family":"Mendez","sequence":"additional","affiliation":[{"name":"Centre d\u2019Analyse et de Math\u00e9matiques Sociales (CNRS, UMR 8557), France and Charles University, Prague, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micha\u0142","family":"Pilipczuk","sequence":"additional","affiliation":[{"name":"University of Warsaw, Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel A.","family":"Quiroz","sequence":"additional","affiliation":[{"name":"Universidad de Chile, Santiago, Chile"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roman","family":"Rabinovich","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Siebertz","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Bremen, Berlin, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,3,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1231082307"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793251219"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0895480195282550"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814937"},{"volume-title":"Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC\u201977)","author":"Ashok","key":"e_1_2_1_5_1","unstructured":"Ashok K. Chandra and Philip M. Merlin. 1977. Optimal implementation of conjunctive queries in relational data bases . In Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC\u201977) . ACM, 77--90. Ashok K. Chandra and Philip M. Merlin. 1977. Optimal implementation of conjunctive queries in relational data bases. In Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC\u201977). ACM, 77--90."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.33"},{"volume-title":"Handbook of Theoretical Computer Science","author":"Courcelle Bruno","key":"e_1_2_1_7_1","unstructured":"Bruno Courcelle . 1990. Graph rewriting: An algebraic and logic approach . In Handbook of Theoretical Computer Science , Vol. B, Jan van Leeuwen (Ed.). Elsevier, 194-- 242 . Bruno Courcelle. 1990. Graph rewriting: An algebraic and logic approach. In Handbook of Theoretical Computer Science, Vol. B, Jan van Leeuwen (Ed.). Elsevier, 194--242."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00083-6"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002249910009"},{"volume-title":"Parameterized Algorithms","author":"Cygan Marek","key":"e_1_2_1_10_1","unstructured":"Marek Cygan , Fedor V. Fomin , \u0141ukasz Kowalik , Daniel Lokshtanov , D\u00e1niel Marx , Marcin Pilipczuk , Micha\u0142 Pilipczuk , and Saket Saurabh . 2015. Parameterized Algorithms . Springer . Marek Cygan, Fedor V. Fomin, \u0141ukasz Kowalik, Daniel Lokshtanov, D\u00e1niel Marx, Marcin Pilipczuk, Micha\u0142 Pilipczuk, and Saket Saurabh. 2015. Parameterized Algorithms. Springer."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.31"},{"key":"e_1_2_1_12_1","volume-title":"Graph Theory","author":"Diestel Reinhard","unstructured":"Reinhard Diestel . 2010. Graph Theory ( 4 th ed.). Graduate Texts in Mathematics, Vol. 173 . Springer . Reinhard Diestel. 2010. Graph Theory (4th ed.). Graduate Texts in Mathematics, Vol. 173. Springer.","edition":"4"},{"key":"e_1_2_1_13_1","volume-title":"Fellows","author":"Downey Rodney G.","year":"1999","unstructured":"Rodney G. Downey and Michael R . Fellows . 1999 . Parameterized Complexity. Springer . Rodney G. Downey and Michael R. Fellows. 1999. Parameterized Complexity. Springer."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejc.2012.12.004"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499483"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_22"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the Annual Conference on Computer Science Logic (CSL\u201916)","volume":"62","author":"Eickmeyer Kord","year":"2016","unstructured":"Kord Eickmeyer and Ken-ichi Kawarabayashi. 2016 . Successor-invariant first-order logic on graphs with excluded topological subgraphs . In Proceedings of the Annual Conference on Computer Science Logic (CSL\u201916) . LIPIcs. Leibniz Int. Proc. Inform. , Vol. 62 . Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 18:1--18:15. Kord Eickmeyer and Ken-ichi Kawarabayashi. 2016. Successor-invariant first-order logic on graphs with excluded topological subgraphs. In Proceedings of the Annual Conference on Computer Science Logic (CSL\u201916). LIPIcs. Leibniz Int. Proc. Inform., Vol. 62. Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 18:1--18:15."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.19"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934517"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.38"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:ORDE.0000034609.99940.fb"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/602220.602222"},{"volume-title":"Parameterized Complexity Theory","author":"Flum J\u00f6rg","key":"e_1_2_1_23_1","unstructured":"J\u00f6rg Flum and Martin Grohe . 2006. Parameterized Complexity Theory . Springer . J\u00f6rg Flum and Martin Grohe. 2006. Parameterized Complexity Theory. Springer."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/504794.504798"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Herbrand Symposium, J. Stern (Ed.). Stud. Logic Found. Math.","volume":"107","author":"Gaifman Haim","year":"1982","unstructured":"Haim Gaifman . 1982 . On local and nonlocal properties . In Proceedings of the Herbrand Symposium, J. Stern (Ed.). Stud. Logic Found. Math. , Vol. 107 . North-Holland, 105--135. Haim Gaifman. 1982. On local and nonlocal properties. In Proceedings of the Herbrand Symposium, J. Stern (Ed.). Stud. Logic Found. Math., Vol. 107. North-Holland, 105--135."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2015.63"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP\u201918). LIPIcs. Leibniz Int. Proc. Inform.","volume":"107","author":"Gajarsk\u00fd Jakub","year":"2018","unstructured":"Jakub Gajarsk\u00fd , Stephan Kreutzer , Jaroslav Ne\u0161et\u0159il , Patrice Ossona de Mendez , Micha\u0142 Pilipczuk , Sebastian Siebertz , and Szymon Toru\u0144czyk . 2018 . First-order interpretations of bounded expansion classes . In Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP\u201918). LIPIcs. Leibniz Int. Proc. Inform. , Vol. 107 . Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 126:1--126:14. Jakub Gajarsk\u00fd, Stephan Kreutzer, Jaroslav Ne\u0161et\u0159il, Patrice Ossona de Mendez, Micha\u0142 Pilipczuk, Sebastian Siebertz, and Szymon Toru\u0144czyk. 2018. First-order interpretations of bounded expansion classes. In Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP\u201918). LIPIcs. Leibniz Int. Proc. Inform., Vol. 107. Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 126:1--126:14."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS\u201908). LIPIcs. Leibniz Int. Proc. Inform.","volume":"1","author":"Ganzow Tobias","year":"2008","unstructured":"Tobias Ganzow and Sasha Rubin . 2008 . Order-invariant MSO is stronger than counting MSO in the finite . In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS\u201908). LIPIcs. Leibniz Int. Proc. Inform. , Vol. 1 . Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 313--324. Tobias Ganzow and Sasha Rubin. 2008. Order-invariant MSO is stronger than counting MSO in the finite. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science (STACS\u201908). LIPIcs. Leibniz Int. Proc. Inform., Vol. 1. Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 313--324."},{"volume-title":"Model Theoretic Methods in Finite Combinatorics, Martin Grohe and Johann A","author":"Grohe Martin","key":"e_1_2_1_29_1","unstructured":"Martin Grohe and Stephan Kreutzer . 2011. Methods for algorithmic meta theorems . In Model Theoretic Methods in Finite Combinatorics, Martin Grohe and Johann A . Makowsky (Eds.). Contemp. Math., Vol. 558 . AMS , 181--205. Martin Grohe and Stephan Kreutzer. 2011. Methods for algorithmic meta theorems. In Model Theoretic Methods in Finite Combinatorics, Martin Grohe and Johann A. Makowsky (Eds.). Contemp. Math., Vol. 558. AMS, 181--205."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 41st International Workshop on Graph-Theoretic Concepts in Computer Science (WG\u201915)","volume":"9224","author":"Grohe Martin","year":"2015","unstructured":"Martin Grohe , Stephan Kreutzer , Roman Rabinovich , Sebastian Siebertz , and Konstantinos Stavropoulos . 2015 . Colouring and covering nowhere dense graphs . In Proceedings of the 41st International Workshop on Graph-Theoretic Concepts in Computer Science (WG\u201915) . Lecture Notes in Comput. Sci. , Vol. 9224 . Springer, 325--338. Martin Grohe, Stephan Kreutzer, Roman Rabinovich, Sebastian Siebertz, and Konstantinos Stavropoulos. 2015. Colouring and covering nowhere dense graphs. In Proceedings of the 41st International Workshop on Graph-Theoretic Concepts in Computer Science (WG\u201915). Lecture Notes in Comput. Sci., Vol. 9224. Springer, 325--338."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3051095"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1137\/16M1079336"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330050"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1137\/070685920"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4153\/CMB-1968-037-0"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:ORDE.0000026489.93166.cb"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.disopt.2011.06.001"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science (MFCS\u201916). LIPIcs. Leibniz Int. Proc. Inform.","volume":"58","author":"Kreutzer Stephan","year":"2016","unstructured":"Stephan Kreutzer , Micha\u0142 Pilipczuk , Roman Rabinovich , and Sebastian Siebertz . 2016 . The generalised colouring numbers on classes of bounded expansion . In Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science (MFCS\u201916). LIPIcs. Leibniz Int. Proc. Inform. , Vol. 58 . Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 85:1--85:13. Stephan Kreutzer, Micha\u0142 Pilipczuk, Roman Rabinovich, and Sebastian Siebertz. 2016. The generalised colouring numbers on classes of bounded expansion. In Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science (MFCS\u201916). LIPIcs. Leibniz Int. Proc. Inform., Vol. 58. Schloss Dagstuhl--Leibniz-Zentrum f\u00fcr Informatik, 85:1--85:13."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.39"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1873601.1873631"},{"volume-title":"Elements of Finite Model Theory","author":"Libkin Leonid","key":"e_1_2_1_41_1","unstructured":"Leonid Libkin . 2004. Elements of Finite Model Theory . Springer . Leonid Libkin. 2004. Elements of Finite Model Theory. Springer."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1137\/S089548019120016X"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1056106.1704958"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejc.2006.07.013"},{"volume-title":"Algorithms and Combinatorics","author":"Ne\u0161et\u0159il Jaroslav","key":"e_1_2_1_45_1","unstructured":"Jaroslav Ne\u0161et\u0159il and Patrice Ossona de Mendez . 2012. Sparsity\u2014Graphs, Structures, and Algorithms. Algorithms and Combinatorics , Vol. 28 . Springer . Jaroslav Ne\u0161et\u0159il and Patrice Ossona de Mendez. 2012. Sparsity\u2014Graphs, Structures, and Algorithms. Algorithms and Combinatorics, Vol. 28. Springer."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.32"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695073"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2005.10.006"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209136"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210054"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1185803625"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(89)90161-0"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070079"},{"key":"e_1_2_1_56_1","first-page":"265","article-title":"On an ordering of the vertices of a graph. \u010casopis P\u011bst","volume":"88","author":"Sekanina Milan","year":"1963","unstructured":"Milan Sekanina . 1963 . On an ordering of the vertices of a graph. \u010casopis P\u011bst . Mat. 88 , 3 (1963), 265 -- 282 . Milan Sekanina. 1963. On an ordering of the vertices of a graph. \u010casopis P\u011bst. Mat. 88, 3 (1963), 265--282.","journal-title":"Mat."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90061-X"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC\u201982)","author":"Vardi Moshe Y.","year":"1982","unstructured":"Moshe Y. Vardi . 1982 . The complexity of relational query languages . In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC\u201982) . ACM, 137--146. Moshe Y. Vardi. 1982. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC\u201982). ACM, 137--146."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2008.03.024"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360011","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360011","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:32Z","timestamp":1750203872000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360011"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3,2]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4,30]]}},"alternative-id":["10.1145\/3360011"],"URL":"https:\/\/doi.org\/10.1145\/3360011","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2020,3,2]]},"assertion":[{"value":"2018-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}