Aiming at extremely efficient algorithms for big data sets, we introduce property testing of relational databases of bounded degree. Our model generalises the bounded degree model for graphs (Goldreich and Ron, STOC 1997). We prove that in this model, if the databases have bounded tree-width, then every query definable in monadic second-order logic with modulo counting is testable with a constant number of oracle queries and polylogarithmic running time. This is the first logical meta-theorem in property testing of sparse models. Furthermore, we discuss conditions for the existence of uniform and non-uniform testers.

We study the expressive power and succinctness of order-invariant sentences of first-order (FO) and monadic second-order (MSO) logic on structures of bounded tree-depth. Order-invariance is undecidable in general and, thus, one strives for logics with a decidable syntax that have the same expressive power as order-invariant sentences. We show that on structures of bounded tree-depth, order-invariant FO has the same expressive power as FO. Our proof technique allows for a fine-grained analysis of the succinctness of this translation. We show that for every order-invariant FO sentence there exists an FO sentence whose size is elementary in the size of the original sentence, and whose number of quantifier alternations is linear in the tree-depth. We obtain similar results for MSO. It is known that the expressive power of MSO and FO coincide on structures of bounded tree-depth. We provide a translation from MSO to FO and we show that this translation is essentially optimal regarding the formula size. As a further result, we show that order-invariant MSO has the same expressive power as FO with modulo-counting quantifiers on bounded tree-depth structures.

It is shown that order-invariance of two-variable first-logic is decidable in the finite. This is an immediate consequence of a decision procedure obtained for the finite satisfiability problem for existential second-order logic with two first-order variables (ESO2) on structures with two linear orders and one induced successor. We also show that finite satisfiability is decidable on structures with two successors and one induced linear order. In both cases, so far only decidability for monadic ESO2 has been known. In addition, the finite satisfiability problem for ESO2 on structures with one linear order and its induced successor relation is shown to be decidable in non-deterministic exponential time.

We study Gaifman and Hanf locality of an extension of first-order logic with modulo p counting quantifiers (FO+MODp, for short) with arbitrary numerical predicates. We require that the validity of formulas is independent of the particular interpretation of the numerical predicates and refer to such formulas as arb-invariant formulas. This paper gives a detailed picture of locality and non-locality properties of arb-invariant FO+MODp. For example, on the class of all finite structures, for any p >= 2, arb-invariant FO+MODp is neither Hanf nor Gaifman local with respect to a sublinear locality radius. However, in case that p is an odd prime power, it is weakly Gaifman local with a polylogarithmic locality radius. And when restricting attention to the class of string structures, for odd prime powers p, arb-invariant FO+MODp is both Hanf and Gaifman local with a polylogarithmic locality radius. Our negative results build on examples of order-invariant FO+MODp formulas presented in Niemistö's PhD thesis. Our positive results make use of the close connection between FO+MODp and Boolean circuits built from NOT-gates and AND-, OR-, and MODp-gates of arbitrary fan-in.

This paper considers the logic FOcard, i.e., first-order logic with cardinality predicates that can specify the size of a structure modulo some number. We study the expressive power of FOcard on the class of languages of ranked, finite, labelled trees with successor relations. Our first main result characterises the class of FOcard-definable tree languages in terms of algebraic closure properties of the tree languages. As it can be effectively checked whether the language of a given tree automaton satisfies these closure properties, we obtain a decidable characterisation of the class of regular tree languages definable in FOcard. Our second main result considers first-order logic with unary relations, successor relations, and two additional designated symbols < and + that must be interpreted as a linear order and its associated addition. Such a formula is called addition-invariant if, for each fixed interpretation of the unary relations and successor relations, its result is independent of the particular interpretation of < and +. We show that the FOcard-definable tree languages are exactly the regular tree languages definable in addition-invariant first-order logic. Our proof techniques involve tools from algebraic automata theory, reasoning with locality arguments, and the use of logical interpretations. We combine and extend methods developed by Benedikt and Segoufin (ACM ToCL, 2009) and Schweikardt and Segoufin (LICS, 2010).