Order invariance on decomposable structures

DOI10.1145/2933575.2934517MaRDI QIDQ4635897zbMATH OpenOpenAlexFDO

Authors Michael Elberfeld, Marlin Frickenschmidt, Martin Grohe

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1606.06557

zbMATH Keywords

finite model theoryfirst-order logicmonadic second-order logicplanaritybounded tree-widthmodulo-counting logicorder-invariant logic

Mathematics Subject Classification ID

Trees (05C05) Planar graphs; geometric and topological aspects of graph theory (05C10) Model theory of finite structures (03C13) Classical first-order logic (03B10)

Abstract: Order-invariant formulas access an ordering on a structure's universe, but the model relation is independent of the used ordering. Order invariance is frequently used for logic-based approaches in computer science. Order-invariant formulas capture unordered problems of complexity classes and they model the independence of the answer to a database query from low-level aspects of databases. We study the expressive power of order-invariant monadic second-order (MSO) and first-order (FO) logic on restricted classes of structures that admit certain forms of tree decompositions (not necessarily of bounded width). While order-invariant MSO is more expressive than MSO and, even, CMSO (MSO with modulo-counting predicates), we show that order-invariant MSO and CMSO are equally expressive on graphs of bounded tree width and on planar graphs. This extends an earlier result for trees due to Courcelle. Moreover, we show that all properties definable in order-invariant FO are also definable in MSO on these classes. These results are applications of a theorem that shows how to lift up definability results for order-invariant logics from the bags of a graph's tree decomposition to the graph itself.

Recommendations

• Towards a characterization of order-invariant queries over tame graphs
• Computer Science Logic
• Expressivity and succinctness of order-invariant logics on depth-bounded structures
• Succinctness of Order-Invariant Logics on Depth-Bounded Structures
• Order-invariant MSO is stronger than counting MSO in the finite

Cited in

(7)

• On the expressive power of logics with invariant uses of arithmetic predicates
• Order-invariant MSO is stronger than counting MSO in the finite
• Order-invariant types and their applications
• Towards a characterization of order-invariant queries over tame graphs
• Computer Science Logic
• Model-checking on ordered structures
• Expressivity and succinctness of order-invariant logics on depth-bounded structures

This page was built for publication: Order invariance on decomposable structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635897)