Preservation and Decomposition Theorems for Bounded Degree Structures

This talk is based on the CSL-LICS '14 paper Preservation and decomposition theorems for bounded degree structures co-authored by Frederik Harwath, Lucas Heimberg, and Nicole Schweikardt (Goethe-University Frankfurt am Main) [link]. In this paper, we provide elementary algorithms for two preservation theorems for first-order sentences with modulo m counting quantifiers (FO+mod m ) on the class C d of all finite structures of degree at most d: For each FO+mod m -sentence that is preserved under extensions (homomorphisms) on C d, a C d -equivalent existential (existential-positive) FO-sentence can be constructed in 6-fold (4-fold) exponential time. For FO-sentences, the algorithm has 5-fold (4-fold) exponential time complexity. This is complemented by lower bounds showing that for FO-sentences a 3-fold exponential blow-up of the computed existential (existential-positive) sentence is unavoidable. In this talk, I will focus on a third contribution of our paper, concerning Feferman-Vaught decompositions. The classical Feferman-Vaught theorem states that for certain forms of compositions of structures (like disjoint unions and cartesian products), the theory of a structure composed from simpler structures is determined by the theories of the simpler structures. Algorithmic versions of such decomposition theorems are typically of the following form: A given FO-sentence that shall be evaluated in a composition of structures can be transformed into a decomposition, that is, a Boolean combination of FO-sentences that each are evaluated in only one component structure. It is known that even when restricted to disjoint unions of tree structures, a non-elementary complexity for such an algorithmen is unavoidable (Dawar, Grohe, Kreutzer, Schweikardt 2007). Here, we restrict our attention to the classes C d for d ≥ 2. We provide an algorithm that computes decompositions, that are equivalent to the input FO-formula on disjoint unions of a finite number of structures from C d for d ≥ 3 ( d ≥ 2). The algorithm’s running time is 3-fold (2-fold) exponential in the size of the input formula. This is achieved by employing an elementary construction for Hanf normal forms (Bollig, Kuske 2012) and decomposing the resulting Hanf-formulas. Our algorithm is optimal in the following sense: Even on binary forests (unions of labeled chains), that is, classes of structures of degree at most 3 (respectively, 2), a 3-fold (2-fold) exponential blow-up of the size of decompositions in terms of the size of the input formula is unavoidable. 11: 45 12: 00 Break

Authors

• Lucas Heimberg

Keywords

No keywords are indexed for this paper.