Model-Checking on Ordered Structures

作     者：Eickmeyer, Kord van den Heuvel, Jan Kawarabayashi, Ken-ichi Kreutzer, Stephan de Mendez, Patrice Ossona Pilipczuk, Michal Quiroz, Daniel A. Rabinovich, Roman Siebertz, Sebastian 

作者机构：Tech Univ Darmstadt Dept Math Schlossgartenstr 7 D-64289 Darmstadt Germany London Sch Econ & Polit Sci Dept Math Houghton St London WC2A 2AE England Natl Inst Informat Hitotsubashi 2-1-2 Tokyo 1018430 Japan Tech Univ Berlin Log & Semant Ernst Reuter Pl 7 D-10587 Berlin Germany CNRS UMR 8557 Ctr Anal & Math Sociales 54 Blvd Raspail F-75006 Paris France Charles Univ Prague Comp Sci Inst IUUK Malostranske Nam 25 Prague 11800 Czech Republic Univ Warsaw Inst Informat Stefana Banacha 2 PL-02097 Warsaw Poland Univ Chile Dept Ingn Matemat Av Beauchef 851 Santiago 851 Chile Univ Chile Ctr Modelamiento Matemat Av Beauchef 851 Santiago 851 Chile Univ Bremen Bremen Germany Humboldt Univ Inst Informat Unter Linden 6 D-10099 Berlin Germany 

出 版 物：《ACM TRANSACTIONS ON COMPUTATIONAL LOGIC》 (美国计算机学会计算逻辑汇刊)

年 卷 期：2020年第21卷第2期

页      面：11-11页

核心收录：

学科分类：08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：European Research Council (ERC) under the European Union CE-ITI European Associated Laboratory "Structures in Combinatorics" (LEA STRUCO) [P202/12/G061] National Science Centre of Poland [UMO-2015/19/P/ST6/03998] European Union CONICYT, PIA/Concurso Apoyo a Centros Cientificos y Tecnologicos de Excelencia con Financiamiento Basal [AFB170001] ERCCZ LL-1201 

主　　题：Model checking order-invariance successor-invariance algorithmic meta-theorems 

摘      要：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.