During the early days of relational database theory it was realized that "acyclic" database schemas possess a number of desirable properties. In fact, three different notions of "acyclicity" were identified and investigated during the 1980s, namely, α-acyclicity, β-acyclicity, and γ-acyclicity. Much more recently, the study of α-acyclicity was extended to annotated relations, where the annotations are values from some positive commutative monoid. The recent results about α-acyclic schemas and annotated relations give rise to results about β-acyclic schemas and annotated relations, since a schema is β-acyclic if and only if every sub-schema of it is α-acyclic. Here, we study γ-acyclic schemas and annotated relations. Our main finding is that the characterization of γ-acyclic schemas in terms of monotone sequential join expression extends to annotated relations, provided the annotations come from a positive commutative monoid that has the inner consistency property. Furthermore, the results reported here shed light on the role of the join of two standard relations. Specifically, our results reveal that the only relevant property of the join of two standard relations is that it is a witness to the consistency of the two relations, provided that these two relations are consistent. For the more abstract setting of annotated relations, this property of the standard join is captured by the notion of a consistency witness function, a notion which we systematically utilize in this work.

We study the status of classical model-theoretic preservation theorems such as the Łoś-Tarski theorem and the homomorphism preservation theorem in the context of semiring semantics. Semiring semantics has its origins in the provenance analysis of database queries but has been extended to a systematic way of evaluating logical statements to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. The systematic development of semiring semantics for first-order logic and other logical systems raises the question to what extent classical model-theoretic results can be generalised to this setting and how such results depend on the underlying semiring. The definitions of semantic properties such as preservation under extensions, substructures, or homomorphisms naturally generalise to the setting of semiring semantics. However, the status of the corresponding preservation theorem strongly depends on the algebraic properties of the particular semirings. We prove that these preservation theorems do indeed hold for all lattice semirings (a quite large class, encompassing practically relevant semirings and in particular all min-max semirings). The proofs combine adaptations of the classical compactness and amalgamation methods with specific reduction methods for logical entailment that have been developed in semiring semantics. On the other side, variants of the existential preservation theorem fail for many other semirings, including the tropical semiring, the Viterbi semiring, the Łukasiewicz semiring, and the natural semirings ℕ and ℕ^∞. Surprisingly, the existential preservation theorem does hold for finite interpretations in a number of semirings, including the three-element min-max semiring, which extends the Boolean by just a single additional truth value. Thus, the situation for these semirings is in sharp contrast to the Boolean case, where the Łoś-Tarski theorem holds in general, but not in the finite.

We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.

This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in B\"uchi games. Semiring semantics generalizes the classical Boolean semantics by permitting multiple truth values from certain semirings. Evaluating the fixed-point formula that defines the winning region in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. This is well-understood for reachability games, where the winning region is definable as a least fixed point. The case of B\"uchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the fixed-point definition involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies -- strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables applications such as game synthesis or determining minimal modifications to the game needed to change its outcome. Lastly, we discuss limitations of our approach and present questions that cannot be immediately answered by semiring semantics.

Abstract This note draws conclusions that arise by combining two recent papers, by Anuj Dawar, Erich Grädel and Wied Pakusa, published at ICALP 2019, and by Moritz Lichter, published at LICS 2021. In both papers, the main technical results rely on the combinatorial and algebraic analysis of the invertible-map equivalences ${\equiv ^{\text {IM}}_{k, Q}}$ on certain variants of Cai–Fürer–Immerman structures (CFI-structures for short). These ${\equiv ^{\text {IM}}_{k, Q}}$-equivalences, for a natural number $k$ and a set of primes $Q$, refine the well-known Weisfeiler–Leman equivalences used in algorithms for graph isomorphism. The intuition is that two graphs $G{\equiv ^{\text {IM}}_{k, Q}}H$ cannot be distinguished by iterative refinements of equivalences on $k$-tuples defined via linear operators on vector spaces over fields of characteristic $p \in Q$. In the first paper it has been shown, using considerable algebraic machinery, that for a prime $q \notin Q$, the ${\equiv ^{\text {IM}}_{k, Q}}$ equivalences are not strong enough to distinguish between non-isomorphic CFI-structures over the field $\mathbb {F}_q$. In the second paper, a similar but not identical construction for CFI-structures over the rings $\mathbb {Z}_{2^i}$ has, again by rather involved combinatorial and algebraic arguments, been shown to be indistinguishable with respect to ${\equiv ^{\text {IM}}_{k, \{2\}}}$. Together with an earlier work on rank logic, this second result suffices to separate rank logic from polynomial time. We show here that the two approaches can be unified to prove that CFI-structures over the rings $\mathbb {Z}_{2^i}$ are in fact indistinguishable with respect to ${\equiv ^{\text {IM}}_{k, {\mathbb {P}}}}$, for the set ${\mathbb {P}}$ of all primes. In particular, this implies the following two results. First, there is no fixed $k$ such that the invertible-map equivalence ${\equiv ^{\text {IM}}_{k, {\mathbb {P}}}}$ coincides with isomorphism on all finite graphs. Second, no extension of fixed-point logic by linear-algebraic operators over fields can capture polynomial time.

Semiring semantics evaluates logical statements by values in some commutative semiring (K, +, ·, 0, 1). Random semiring interpretations, induced by a probability distribution on K, generalise random structures, and we investigate here the question of how classical results on first-order logic on random structures, most importantly the 0-1 laws of Glebskii et al. and Fagin, generalise to semiring semantics. For positive semirings, the classical 0-1 law implies that every first-order sentence is, asymptotically, either almost surely evaluated to 0 by random semiring interpretations, or almost surely takes only values different from 0. However, by means of a more sophisticated analysis, based on appropriate extension properties and on algebraic representations of first-order formulae, we can prove much stronger results.

Team semantics is the mathematical basis of modern logics of dependence and independence. In contrast to classical Tarski semantics, a formula is evaluated not for a single assignment of values to the free variables, but on a set of such assignments, called a team. Team semantics is appropriate for a purely logical understanding of dependency notions, where only the presence or absence of data matters, but being based on sets, it does not take into account multiple occurrences of data values. It is therefore insufficient in scenarios where such multiplicities matter, in particular for reasoning about probabilities and statistical independencies. Therefore, an extension from teams to multiteams (i.e. multisets of assignments) has been proposed by several authors. In this paper we aim at a systematic development of logics of dependence and independence based on multiteam semantics. We study atomic dependency properties of finite multiteams and discuss the appropriate meaning of logical operators to extend the atomic dependencies to full-fledged logics for reasoning about dependence properties in a multiteam setting. We explore properties and expressive power of a wide spectrum of different multiteam logics and compare them to second-order logic and to logics with team semantics. In many cases the results resemble what is known in team semantics, but there are also interesting differences. While in team semantics, the combination of inclusion and exclusion dependencies leads to a logic with the full power of both independence logic and existential second-order logic, independence properties of multiteams are not definable by any combination of properties that are downwards closed or union closed and thus are strictly more powerful than inclusion-exclusion logic. We also study the relationship of logics with multiteam semantics with existential second-order logic for a specific class of metafinite structures. It turns out that inclusion-exclusion logic can be characterised in a precise sense by the Presburger fragment of this logic, but for capturing independence, we need to go beyond it and add some form of multiplication. Finally, we also consider multiteams with weights in the reals and study the expressive power of formulae by means of topological properties.

Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.

We study the first-order axiomatisability of finite semiring interpretations or, equivalently, the question whether elementary equivalence and isomorphism coincide for valuations of atomic facts over a finite universe into a commutative semiring. Contrary to the classical case of Boolean semantics, where every finite structure is axiomatised up to isomorphism by a first-order sentence, the situation in semiring semantics is rather different, and depends on the underlying semiring. We prove that for a number of important semirings, including min-max semirings, and the semirings of positive Boolean expressions, there exist finite semiring interpretations that are elementarily equivalent but not isomorphic. The same is true for the polynomial semirings that are universal for the classes of absorptive, idempotent, and fully idempotent semirings, respectively. On the other side, we prove that for other, practically relevant, semirings such as the Viterby semiring 𝕍, the tropical semiring 𝕋, the natural semiring ℕ and the universal polynomial semiring ℕ[X], all finite semiring interpretations are first-order axiomatisable, and thus elementary equivalence implies isomorphism.

Abstract Modern logics of dependence and independence are based on team semantics, which means that formulae are evaluated not on a single assignment of values to variables, but on a set of such assignments, called a team. This leads to high expressive power, on the level of existential second-order logic. As an alternative, Baltag and van Benthem have proposed a local variant of dependence logic, called logic of functional dependence ($ {\textsf {LFD}}$). While its semantics is also based on a team, the formulae are evaluated locally on just one of its assignments, and the team just serves as the supply of the possible assignments that are taken into account in the evaluation process. This logic thus relies on the modal perspective of generalized assignments semantics and can be seen as a fragment of first-order logic. For the variant of $ {\textsf {LFD}}$ without equality, the satisfiability problem is decidable. We extend the idea of localizing logics of dependence and independence in a systematic way, taking into account local variants of standard atomic dependency properties: besides dependence and independence, also inclusion, exclusion and anonymity. We study model-theoretic and algorithmic questions of the localized logics and also resolve some of the questions that had been left open by Baltag and van Benthem. In particular, we study decidability issues of the local logics and prove that satisfiability of $ {\textsf {LFD}}$ with equality is undecidable. Further, we establish characterization theorems via appropriate notions of bisimulation and study the complexity of model checking problems for these logics.

Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity. We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams. In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.

Automatic structures made their appearance at LICS twenty years ago, at LICS 2000. However, their roots are much older. The idea of automata based decision procedures for logical theories can be traced back to the early days of automata theory and to the work of Büchi, Elgot, Trakhtenbrot and Rabin in the 1960s. The explicit notion of automatic structures has first been proposed in 1976 in the (unfortunately largely unnoticed) PhD thesis of Hodgson, and later been reinvented by Khoussainov and Nerode in 1995.

Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parameterized by a number k and a set Q of primes. The intuition is that two equivalent graphs G equiv^IM_{k, Q} H cannot be distinguished by means of partitioning the set of k-tuples in both graphs with respect to any linear-algebraic operator acting on vector spaces over fields of characteristic p, for any p in Q. These equivalences have first appeared in the study of rank logic, but in fact they can be used to delimit the expressive power of any extension of fixed-point logic with linear-algebraic operators. We define {LA^{k}}(Q), an infinitary logic with k variables and all linear-algebraic operators over finite vector spaces of characteristic p in Q and show that equiv^IM_{k, Q} is the natural notion of elementary equivalence for this logic. The logic LA^{omega}(Q) = Cup_{k in omega} LA^{k}(Q) is then a natural upper bound on the expressive power of any extension of fixed-point logics by means of Q-linear-algebraic operators. By means of a new and much deeper algebraic analysis of a generalized variant, for any prime p, of the CFI-structures due to Cai, Fürer, and Immerman, we prove that, as long as Q is not the set of all primes, there is no k such that equiv^IM_{k, Q} is the same as isomorphism. It follows that there are polynomial-time properties of graphs which are not definable in LA^{omega}(Q), which implies that no extension of fixed-point logic with linear-algebraic operators can capture PTIME, unless it includes such operators for all prime characteristics. Our analysis requires substantial algebraic machinery, including a homogeneity property of CFI-structures and Maschke’s Theorem, an important result from the representation theory of finite groups.

One of the most important open problems in finite model theory is the question whether there is a logic characterising efficient computation. While this question usually concerns Ptime, it can also be applied to other complexity classes, and in particular to Logspace which can be seen as a formalisation of efficient computation for big data. One of the strongest candidates for a logic capturing Ptime is Choiceless Polynomial Time (CPT). It is based on the idea of choiceless algorithms, a general model of symmetric computation over abstract structures (rather than their encodings by finite strings). However, there is currently neither a comparably strong candidate for a logic for Logspace, nor a logic transferring the idea of choiceless computation to Logspace. We propose here a notion of Choiceless Logarithmic Space which overcomes some of the obstacles posed by Logspace as a less robust complexity class. The resulting logic is contained in both Logspace and CPT, and is strictly more expressive than all logics for Logspace that have been known so far. Further, we address the question whether this logic can define all Logspace-queries, and prove that this is not the case.

Abstract Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. WhileFPRcan express most of the known queries that separateFPCfromPtime, almost nothing was known about the limitations of its expressive power. In our first main result we show that the extensions ofFPCby rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic ${\text{FPR}}^{\text{*}}$ with an operator that uniformly expresses the matrix rank over finite fields is more expressive thanFPR. One important step in our proof is to consider solvability logicFPSwhich is the analogous extension ofFPCby quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.

We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded-width resolution, and the monomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded-width resolution captures existential least fixed-point logic, and that the polynomial calculus with bounded degree over the rationals solves precisely the problems definable in fixed-point logic with counting. We also study the bounded-degree polynomial calculus. Over the rationals, it captures fixed-point logic with counting if we restrict the bit-complexity of the coefficients. For unrestricted coefficients, we can only say that the bounded-degree polynomial calculus is at most as powerful as bounded variable infinitary counting logic, but a precise logical characterisation of its power remains an open problem. These connections between logics and proof systems allow us to establish finite-model-theoretic tools for proving lower bounds for the polynomial calculus over the rationals and also over finite fields. This is a corrected version of the paper (arXiv:1802.09377) published originally on January 23, 2019.

Modern logics of dependence and independence are based on different variants of atomic dependency statements (such as dependence, exclusion, inclusion, or independence) and on team semantics: A formula is evaluated not with a single assignment of values to the free variables, but with a set of such assignments, called a team. In this paper we explore logics of dependence and independence where the atomic dependency statements cannot distinguish elements up to equality, but only up to a given equivalence relation (which may model observational indistinguishabilities, for instance between states of a computational process or between values obtained in an experiment). Our main goal is to analyse the power of such logics, by identifying equally expressive fragments of existential second-order logic or greatest fixed-point logic, with relations that are closed under the given equivalence. Using an adaptation of the Ehrenfeucht-Fraïssé method we further study conditions on the given equivalences under which these logics collapse to first-order logic, are equivalent to full existential second-order logic, or are strictly between first-order and existential second-order logic.

In the past decades for more and more graph classes the Graph Isomorphism Problem was shown to be solvable in polynomial time. An interesting family of graph classes arises from intersection graphs of geometric objects. In this work we show that the Graph Isomorphism Problem for unit square graphs, intersection graphs of axis-parallel unit squares in the plane, can be solved in polynomial time. Since the recognition problem for this class of graphs is NP-hard we can not rely on standard techniques for geometric graphs based on constructing a canonical realization. Instead, we develop new techniques which combine structural insights into the class of unit square graphs with understanding of the automorphism group of such graphs. For the latter we introduce a generalization of bounded degree graphs which is used to capture the main structure of unit square graphs. Using group theoretic algorithms we obtain sufficient information to solve the isomorphism problem for unit square graphs.

We study structures that are automatic with advice. These are structures that admit a presentation by finite automata (over finite or infinite words or trees) with access to an additional input,called an advice. Over finite words, a standard example of a structure that is automatic with advice, but not automatic in the classical sense, is the additive group of rational numbers (Q,+). By using a set of advices rather than a single advice, this leads to the new concept of a parameterised automatic presentation as a means to uniformly represent a whole class of structures. The decidability of the first-order theory of such a uniformly automatic class reduces to the decidability of the monadic second-order theory of the set of advices that are used in the presentation. Such decidability results also hold for extensions of first-order logic by regularity preserving quantifiers, such as cardinality quantifiers and Ramsey quantifiers. To investigate the power of this concept, we present examples of structures and classes of structures that are automatic with advice but not without advice, and we prove classification theorems for the structures with an advice automatic presentation for several algebraic domains. In particular, we prove that the class of all torsion-free Abelian groups of rank one is uniformly omega-automatic and that there is a uniform omega-tree-automatic presentation of the class of all Abelian groups up to elementary equivalence and of the class of all countable divisible Abelian groups. On the other hand we show that every uniformly omega-automatic class of Abelian groups must have bounded rank. While for certain domains, such as trees and Abelian groups, it turns out that automatic presentations with advice are capable of presenting significantly more complex structures than ordinary automatic presentations, there are other domains, such as Boolean algebras, where this is provably not the case. Further, advice seems to not be of much help for representing some particularly relevant examples of structures with decidable theories, most notably the field of reals. Finally we study closure properties for several kinds of uniformly automatic classes, and decision problems concerning the number of non-isomorphic models in uniformly automatic classes with the unique representation property.

We study the descriptive complexity of summation problems in Abelian groups and semigroups. In general, an input to the summation problem consists of an Abelian semigroup G, explicitly represented by its multiplication table, and a subset X of G. The task is to determine the sum over all elements of X. Algorithmically this is a very simple problem. If the elements of X come in some order, then we can process these elements along that order and calculate the sum in a trivial way. However, what makes this fundamental problem so interesting for us is that from the viewpoint of logical definability its tractability is much more delicate. If we consider the semigroup G as an abstract structure and X as an abstract set, without a linear order and hence without a canonical way to process the elements one by one, then it is unclear how to define the sum in any logic that does not have the power to quantify over a linear order. Indeed the trivial summation algorithm cannot be expressed in any polynomial-time logic or, in fact, in any computational model which works on abstract mathematical structures in an isomorphism-invariant way without violating polynomial resource bounds. The surprising difficulty, in terms of logical definability, of this basic mathematical problem is the reason why Ben Rossman asked, more than ten years ago, whether it can be expressed in the logic Choiceless Polynomial Time with counting (CPT). Note that, to date, CPT is one of the most powerful known candidates for a logic that might be capable of defining every polynomial-time property of finite structures. In this paper we clarify the status of the definability for the summation problem for Abelian groups and semigroups in important polynomial-time logics. In our first main result we show that the problem can be defined in fixed-point logic with counting (FPC). Since FPC is contained in CPT this settles Rossman's question. Our proof is based on a dynamic programming approach and heavily uses the counting mechanism of FPC. In our second main result we give a matching lower bound and show that the use of counting operators cannot be avoided: the summation problem, even over Abelian groups, cannot be defined in pure fixed-point logic without counting. Our proof is based on a probabilistic argument.

We explore several counting constructs for logics with team semantics. Counting is an important task in numerous applications, but with a somewhat delicate relationship to logic. Team semantics on the other side is the mathematical basis of modern logics of dependence and independence, in which formulae are evaluated not for a single assignment of values to variables, but for a set of such assignments. It is therefore interesting to ask what kind of counting constructs are adequate in this context, and how such constructs influence the expressive power, and the model-theoretic and algorithmic properties of logics with team semantics. Due to the second-order features of team semantics there is a rich variety of potential counting constructs. Here we study variations of two main ideas: forking atoms and counting quantifiers. Forking counts how many different values for a tuple w occur in assignments with coinciding values for v. We call this the forking degree of bar v with respect to bar w. Forking is powerful enough to capture many of the previously studied atomic dependency properties. In particular we exhibit logics with forking atoms that have, respectively, precisely the power of dependence logic and independence logic. Our second approach uses counting quantifiers E^{geq mu} of a similar kind as used in logics with Tarski semantics. The difference is that these quantifiers are now applied to teams of assignments that may give different values to mu. We show that, on finite structures, there is an intimate connection between inclusion logic with counting quantifiers and FPC, fixed-point logic with counting, which is a logic of fundamental importance for descriptive complexity theory. For sentences, the two logics have the same expressive power. Our analysis is based on a new variant of model-checking games, called threshold safety games, on a trap condition for such games, and on game interpretations.

We study definability questions for positional winning strategies in infinite games on graphs. The quest for efficient algorithmic constructions of winning regions and winning strategies in infinite games, in particular parity games, is of importance in many branches of logic and computer science. A closely related, yet different, facet of this problem concerns the definability of winning regions and winning strategies in logical systems such as monadic second-order logic, least fixed-point logic LFP, the modal μ-calculus and some of its fragments. While a number of results concerning definability issues for winning regions have been established, so far almost nothing has been known concerning the definability of winning strategies. We make the notion of logical definability of positional winning strategies precise and study systematically the possibility of translations between definitions of winning regions and definitions of winning strategies. We present explicit LFP-definitions for winning strategies in games with relatively simple objectives, such as safety, reach ability, eventual safety (Co-Büchi) and recurrent reach ability (Büchi), and then prove, based on the Stage Comparison Theorem, that winning strategies for any class of parity games with a bounded number of priorities are LFP-definable. For parity games with an unbounded number of priorities, LFP-definitions of winning strategies are provably impossible on arbitrary (finite and infinite) game graphs. On finite game graphs however, this definability problem turns out to be equivalent to the fundamental open question about the algorithmic complexity of parity games. Indeed, based on a general argument about LFP-translations we prove that LFP definable winning strategies on the class of all finite parity games exist if, and only if, parity games can be solved in polynomial time, despite the fact that LFP is, in general, strictly weaker than polynomial time.

Choice less Polynomial Time (CPT) is one of the candidates in the quest for a logic for polynomial time. It is a strict extension of fixed-point logic with counting, but to date the question is open whether it expresses all polynomial-time properties of finite structures. We present here alternative characterisations of Choice less Polynomial Time (with and without counting) based on iterated first-order interpretations. The fundamental mechanism of Choice less Polynomial Time is the manipulation of hereditarily finite sets over the input structure by means of set-theoretic operations and comprehension terms. While this is very convenient and powerful for the design of abstract computations on structures, it makes the analysis of the expressive power of CPT rather difficult. We aim to reduce this functional framework operating on higher-order objects to an approach that evaluates formulae on less complex objects. We propose a more model-theoretic formalism, called polynomial-time interpretation logic (PIL), that replaces the machinery of hereditarily finite sets and comprehension terms by traditional first-order interpretations, and handles counting by Härtig quantifiers. In our framework, computations on finite structures are captured by iterations of interpretations, and a run is a sequence of states, each of which is a finite structure of a fixed vocabulary. Our main result is that PIL has precisely the same expressive power as Choice less Polynomial Time. We also analyse the structure of PIL and show that many of the logical formalisms or database languages that have been proposed in the quest for a logic for polynomial time reappear as fragments of PIL, obtained by restricting interpretations in a natural way (e.g. By omitting congruences or using only one-dimensional interpretations).

We investigate the logical resources required to maintain knowledge about a property of a finite structure that undergoes an ongoing series of local changes such as insertion or deletion of tuples to basic relations. Our framework is closely related to the Dyn-FO-framework of Patnaik and Immerman and the FOIES-framework of Dong, Libkin, Su and Wong, and also builds on work of Weber and Schwentick. We assume that the dynamic process starts with an arbitrary, nonempty structure, but in contrast to previous work, we assume that, in general, structures are unordered. We show how to modify known dynamic algorithms for symmetric reachability, bipartiteness, k-edge connectivity and more, to work also without an order and with dynamic processes starting at an arbitrary graph. A history independent dynamic system (also called deterministic or memoryless) is one that maintains all auxiliary information independent of the update order. In 1997, Dong and Su posed the problem whether there exist history independent dynamic systems with FO-updates for symmetric reachability or bipartiteness. We give a positive answer to this question. We further show that there is a history independent system for tree isomorphism with FO+C-updates. On the other hand we show that on unordered structures first-order logic is too weak to maintain enough information to answer the equal cardinality query and the tree isomorphism query dynamically.

We investigate structural properties of omega-automatic presentations of infinite structures in order to sharpen our methods to determine whether a given structure is omega-automatic. We apply these methods to show that no field of characteristic 0 admits an injective omega-automatic presentation, and that uncountable fields with a definable linear order cannot be omega-automatic.

We study 0-1 laws for extensions of first-order logic by Lindström quantifiers. We state sufficient conditions on a quantifier Q expressing a graph property, for the logic FO[Q] – the extension of first-order logic by means of the quantifier Q – to have a 0-1 law. We use these conditions to show, in particular, that FO[Rig], where Rig is the quantifier expressing rigidity, has a 0-1 law. We also show that extensions of first-order logic with quantifiers for Hamiltonicity, regularity and self-complementarity of graphs do not have a 0-1 law. Blass and Harary pose the question whether there is a logic which is powerful enough to express Hamiltonicity or rigidity and which has a 0-1 law. It is a consequence of our results that there is no such regular logic (in the sense of abstract model theory) in the case of Hamiltonicity, but there is one in the case of rigidity. We also consider sequences of vectorized quantifiers, and show that the extensions of first-order logic obtained by adding such sequences generated by quantifiers that are closed under substructures have 0-1 laws. The positive results also extend to the infinitary logic with finitely many variables.

We survey determinacy, definability, and complexity issues of Banach-Mazur games on finite and infinite graphs. Infinite games where two players take turns to move a token through a directed graph, thus tracing out an infinite path, have numerous applications in different branches of mathematics and computer science. In the usual format, the possible moves of the players are given by the edges of the graph; in each move a player takes the token from its current position along an edge to a next position. In Banach-Mazur games the players instead select in each move a \emph{path} of arbitrary finite length rather than just an edge. In both cases the outcome of a play is an infinite path. A winning condition is thus given by a set of infinite paths which is often specified by a logical formula, for instance from S1S, LTL, or first-order logic. Banach-Mazur games have a long tradition in descriptive set theory and topology, and they have recently been shown to have interesting applications also in computer science, for instance for planning in nondeterministic domains, for the study of fairness in concurrent systems, and for the semantics of timed automata. It turns out that Banach-Mazur games behave quite differently than the usual graph games. Often they admit simpler winning strategies and more efficient algorithmic solutions. For instance, Banach-Mazur games with $\omega$-regular winning conditions always have positional winning strategies, and winning positions for finite Banach-Mazur games with Muller winning condition are computable in polynomial time.

We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy. The theory of such games is well studied for winning conditions that are defined in terms of a mapping that assigns to each position a priority from a finite set. Specifically, in Muller games the winner of a play is determined by the set of those priorities that have been seen infinitely often; an important special case are parity games where the least (or greatest) priority occurring infinitely often determines the winner. It is well-known that parity games are positionally determined whereas Muller games are determined via finite-memory strategies. In this paper, we extend this theory to the case of games with infinitely many priorities. Such games arise in several application areas, for instance in pushdown games with winning conditions depending on stack contents. For parity games there are several generalisations to the case of infinitely many priorities. While max-parity games over omega or min-parity games over larger ordinals than omega require strategies with infinite memory, we can prove that min-parity games with priorities in omega are positionally determined. Indeed, it turns out that the min-parity condition over omega is the only infinitary Muller condition that guarantees positional determinacy on all game graphs.

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed-point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed-point operators to first-order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC), we introduce has much greater expressive power than the μ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.

We survey logical formalisms based on inflationary and deflationary fixed points, and compare them to the (more familiar) logics based on least and greatest fixed points.

No abstract available.

We present Datalog LITE, a new deductive query language with a linear-time model-checking algorithm, that is, linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable occurrences and a limited form of universal quantification in rule bodies.Despite linear-time evaluation, Datalog LITE is highly expressive: It encompasses popular modal and temporal logics such as CTL or the alternation-free μ-calculus. In fact, these formalisms have natural presentations as fragments of Datalog LITE. Further, Datalog LITE is equivalent to the alternation-free portion of guarded fixed-point logic. Consequently, linear-time model checking algorithms for all mentioned logics are obtained in a unified way.The results are complemented by inexpressibility proofs to the effect that linear-time fragments of stratified Datalog have too limited expressive power.

Guarded fixed-point logic μGF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal μ-calculus plays within the modal domain. We provide a semantic characterization of μGF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterization of the modal μ-calculus, due to Janin and Walukiewicz, is lifted from the modal to the guarded domain by means of model theoretic translations. Guarded second-order logic, the fragment of second-order logic which is introduced in the context of our characterization theorem, captures a natural and robust level of expressiveness with several equivalent characterizations. For a wide range of issues in guarded logics it may take up a role similar to that of monadic second-order in relation to modal logics. At the more general methodological level, the translations between the guarded and modal domains make the intuitive analogy between guarded and modal logics available as a tool in the further analysis of the model theory of guarded logics.

We study definability and complexity issues for automatic and /spl omega/-automatic structures. These are, in general, infinite structures but they can be finitely presented by a collection of automata. Moreover they admit effective (in fact automatic) evaluation of all first-order queries. Therefore, automatic structures provide an interesting framework for extending many algorithmic and logical methods from finite structures to infinite ones. We explain the notion of (/spl omega/-)automatic structures, give examples, and discuss the relationship to automatic groups. We determine the complexity of model checking and query evaluation on automatic structures for fragments of first-order logic. Further we study closure properties and definability issues on automatic structures and present a technique for proving that a structure is not automatic. We give model-theoretic characterisations for automatic structures via interpretations. Finally we discuss the composition theory of automatic structures and prove that they are closed under finitary Feferman-Vaught-like products.

Guarded fixed point logic /spl mu/GF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal /spl mu/-calculus plays within the modal domain. We provide a semantic characterisation of /spl mu/GF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterisation of the modal /spl mu/-calculus, due to D. Janin and I. Walukiewicz (1999), is lifted from the modal to the guarded domain by means of model theoretic translations. At the methodological level, these translations make the intuitive analogy between modal and guarded logics available as a tool in the analysis of the guarded domain.

We prove that the class of all languages that are definable in /spl Sigma//sub 1//sup 1/(FO/sup 2/), that is, in (non-monadic) existential second-order logic with only two first-order variables, coincides with the regular languages. This provides an alternative logical description of regularity to both the traditional one in terms of monadic second-order logic, due to Buchi and Trakhtenbrot, and the more recent ones in terms of prefix fragments of /spl Sigma//sub 1//sup 1/, due to Eiter, Gottlob and Gurevich. Our result extends to more general settings than words. Indeed, definability in /spl Sigma//sub 1//sup 1/(FO/sup 2/) coincides with recognizability by appropriate notions of automata on a large class of objects, including /spl omega/-words, trees, pictures and, more generally, all weakly deterministic, triangle-free transition systems.

Guarded fixed point logics are obtained by adding least and greatest fixed points to the guarded fragments of first-order logic that were recently introduced by H. Andreka et al. (1998). Guarded fixed point logics can also be viewed as the natural common extensions of the modal p-calculus and the guarded fragments. We prove that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time. For guarded fixed point sentences of bounded width, the most important case for applications, the satisfiability problem is EXPTIME-complete.

Abstract Guarded fragments of first-order logic were recently introduced by Andréka, van Benthem and Németi; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable fragments of first-order logic. Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is Exptime-complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment. It is also shown that some natural, modest extensions of the guarded fragments are undecidable.

The reliability of database queries on databases with uncertain information is studied, on the basis of a probabilistic model for unreliable databases. While it was already known that the reliability of quantifierfree queries is computable in polynomial time, we show here that already for conjunctive queries, the reliability may become highly intractable. We exhibit a conjunctive query whose reliability problem is complete for FP #P . We further show, that FP #P is the typical complexity level for the reliability problems of a very large class of queries, including all second-order queries. We study approximation algorithms and prove that the reliabilities of all polynomial-time evaluable queries can be efficiently approximated by randomized algorithms. Finally we discuss the extension of our approach to the more general metafinite database model where finite relational structures are endowed with functions into an infinite interpreted domain; in addition queries may use aggregate ...

We prove that the satisfiability and the finite satisfiability problems for C/sup 2/ are decidable. C/sup 2/ is first-order logic with only two variables in the presence of arbitrary counting quantifiers 3/sup /spl ges/m/,m/spl ges/1. It considerably extends L/sup 2/ plain first-order with only two variables, which is known to be decidable by a result of Mortimer's. Unlike L/sup 2/, C/sup 2/ does not have the finite model property.

We study 0-1 laws for extensions of first-order logic by Lindstrom quantifiers. We state sufficient conditions on a quantifier Q expressing a graph property, for the logic FO[Q]-the extension of first-order logic by means of the quantifier Q-to have a 0-1 law. We use these conditions to show, in particular, that FO[Rig], where Rig is the quantifier expressing rigidity, has a 0-1 law. We also show that FO[Ham], where Ham is the quantifier expressing Hamiltonicity, does not have a 0-1 law. Blass and Harary pose the question whether there is a logic which is powerful enough to express Hamiltonicity or rigidity and which has a 0-1 law. It is a consequence of our results that there is no such regular logic (in the sense of abstract model theory) in the case of Hamiltonicity, but there is one in the case of rigidity. We also consider sequences of vectorized quantifiers, and show that the extensions of first-order logic obtained by adding such sequences generated by quantifiers that are closed under substructures have 0-1 laws.

We present a logical approach to complexity over the real numbers with respect to the model of Blum, Shub and Smale. The logics under consideration are interpreted over a special class of two-sorted structures, called R-structures: They consist of a finite structure together with the ordered field of reals and a finite set of functions from the finite structure into R. They are a special case of the metafinite structures introduced recently by Grädel and Gurevich. We argue that R-structures provide the right class of structures to develop a descriptive complexity theory over R. We substantiate this claim by a number of results that relate logical definability on R-structures with complexity of computations of BSS-machines.

Abstract We design functional algebras that characterize various complexity classes of global functions. For this purpose, classical schemata from recursion theory are tailored for capturing complexity. In particular we present a functional analog of first-order logic and describe algebras of the functions computable in nondeterministic logarithmic space, deterministic and nondeterministic polynomial time, and for the functions computable by AC 1 -circuits.

The authors establish a general hierarchy theorem for quantifier classes in the infinitary logic L/sub infinity omega //sup omega / on finite structures. In particular, it is shown that no infinitary formula with bounded number of universal quantifiers can express the negation of a transitive closure. This implies the solution of several open problems in finite model theory: On finite structures, positive transitive closure logic is not closed under negation. More generally the hierarchy defined by interleaving negation and transitive closure operators is strict. This proves a conjecture of N. Immerman (1987). The authors also separate the expressive power of several extensions of Datalog, giving new insight in the fine structure of stratified Datalog.>

It is shown that transitive closure logic (FO+TC) is strictly more powerful than deterministic transitive closure logic (FO+DTC) on unordered structures. In fact, on certain classes of graphs, such as hypercubes or regular graphs of large degree and girth, every query in (FO+DTC) is first-order expressible. On the other hand, there are simple (FO+pos TC) queries on these classes that cannot be defined by first-order formulas.>

Domino games which describe computations of alternating Turing machines in the same way as dominoes (tiling systems) encode computations of deterministic and nondeterministic Turing machines are considered. The domino games are two-person games in the course of which the players build up domino tilings of a square of prescribed size. Acceptance of an alternating Turing machine corresponds to a winning strategy for one player—the number of moves in the game is the number of alternations of the Turing machine. Let $\operatorname{ATIME}(T(n), m)$ denote the class of all sets that are accepted by some alternating Turing machine in time $T(n)$ with at most m alternations. It is shown that any problem in such a complexity class can be reduced to the strategy problem for some domino game. In particular domino games which are complete in the classes $\Sigma_{m}^{p}$, and $\Pi_{m}^{p}$, of the polynomial time hierarchy are found. This corresponds to the approach of Savelsbergh and van Emde Boas and of Lewis and Papadimitriou, who have shown that the theory of NP-completeness may also be founded on a finite domino problem instead of the satisfiability problem for propositional formulae. Similar generalizations are possible for domino connectability problems: Domino thread games where the players build up a thread of dominoes are introduced; the first player wins if he can ultimately connect two given points. It is shown that a certain class of such games captures deterministic time complexity. In particular, games are found whose strategy problems are P-complete. In the last section applications to the complexity of simple prefix classes in logical theories are briefly discussed.