Back and Forth Between Guarded and Modal Logics, with E. Grädel and C. Hirsch
ACM Transactions on Computational Logic , volume 3, 2002, pp. 418-463.
Based on LICS'2000 version.

Abstract Guarded fixed point logic muGF 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 mu-calculus plays within the modal domain. We provide a semantic characterisation of muGF within an appropriate fragment of second-order logic, guarded second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterisation of the modal mu-calculus, due to Janin and Walukiewicz, is lifted from the modal to the guarded domain by means of model theoretic translations. The full proof of this main result comprises the case of formulae with arbitrary tuples of free variables. The proposed model theoretic translations provide a general method and toolkit for using the intuitive analogy between modal and guarded logics in the analysis of the guarded domain. Guarded second-order logic is proposed as a framework for the model theory of guarded logics with a role comparable to that which monadic second-order logic plays in the modal world. Several equivalent characterisations of guarded second-order logic are explored in order to indicate its robustness and naturalness.

An Interpolation Theorem,
Bulletin of Symbolic Logic, volume 6, 2000, pp.447-462.

Abstract A relativized variant of Lyndons's Interpolation Theorem is proved, which gives a tool to focus on existential and universal quantification over designated subdomains -- through positive and negative occurrences of predicates denoting these subdomains in relativized quantifications.
It is shown how this single new interpolation theorem unifies a number of related results: namely, the classical preservation theorems concerning extensions/substructures with those concerning monotonicity, as well as a many-sorted interpolation theorem focusing on existentially/universally quantified sorts.

Back and Forth Between Guarded and Modal Logics, with E. Grädel and C. Hirsch
Proc. of 15th IEEE Symposium on Logic in Computer Science LICS 2000, Santa Barbara, pp. 217-228.

Abstract Guarded fixed point logic muGF 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 mu-calculus plays within the modal domain. We provide a semantic characterisation of muGF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterisation of the modal mu-calculus, due to Janin and Walukiewicz, 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.

Epsilon-Logic is More Expressive Than First-Order Logic over Finite Structures,
Journal of Symbolic Logic, volume 65, 2000, pp. 1749-1757.

Abstract It is shown that there are properties of finite structures that are expressible with the use of Hilbert's epsilon-operator in a manner that does not depend on the actual interpretation for epsilon-terms, but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly enhance the expressive power of first-order logic even as far as deterministic queries are concerned, thereby answering a question raised by Abiteboul and Vianu.

Two-Variable First-Order Logic over Ordered Domains,
Journal of Symbolic Logic, volume 66, 2001, pp. 685-702.

Abstract The satisfiability problem for the two-variable fragment FO² of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations.
It is shown that FO² over ordered, respectively wellordered, domains or in the presence of one wellfounded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO², namely non-deterministic exponential time.
In contrast FO² becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as (even partial) orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO² and computation tree logic.

On logics with two variables, with E. Grädel
Theoretical Computer Science, volume 224, 1999, pp. 73-113.

Abstract Logical languages whose leading feature lies in the restriction to just two element variables play an important role in a number of applications, including the specification of processes or of the temporal or causal behaviour of transition systems, as well as the formalization of epistemological or terminological dependencies. The two-variable nature of many important languages may be attributed to the fact that they contain propositional modal logic as an essential core. Diverse mechanisms for extending basic modal logic have been analyzed with great success within the modal framework, and have lead to interesting, manageable languages, that meet the essential expressive needs for certain applications. For many applications, however, first-order closure properties offer an equally desirable direction for extensions. In this case, the extension of basic modal logic to first-order logic with two variables provides the natural starting point.
This survey presents an overview of recent results pertaining to logics that lift some of the prominent mechanisms of extension from the modal framework to the framework of two-variable first-order logic. Most strikingly, two-variable first-order logic turns out to be not nearly as robust as modal logic with respect to satisfiability; several seemingly weak extensions of two-variable first-oder in important directions turn out to be highly undecidable. One notable exception is the extension by counting quantifiers, which does provide a decidable common extension of graded modal logic and two-variable first order. Some of the resulting other logics, while being undecidable, do provide natural levels of expressiveness for model checking applications, their complexity is generally no worse than for the underlying modal variants.

Bisimulation-Invariant Ptime and Higher-Dimensional mu-Calculus,
Theoretical Computer Science, volume 224, 1999, pp. 237-265.

Abstract Let "bisimilar Ptime" be the class of those monadic queries over finite Kripke structures that are in Ptime and closed under bisimulation equivalence. This class "bisimilar Ptime" has a natural logical characterisation: it is captured, in the sense of descriptive complexity, by the straightforward extension of propositional mu-calculus to arbitrary finite dimension. Here mu-calculus in dimension k is based on modal logic with k-tuples of worlds as the new k-worlds, k different accessibility relations, one for each component, and a mu-operator. It is also shown that even 2-dimensional mu-calculus does not have the finite model property, is undecidable for finite satisfiability, and Sigma^1_1-hard for satisfiability.

Adding FOR-Loops to First-Order Logic, with F. Neven, J. Tyszkiewicz, and J. Van den Bussche,
Information and Computation, volume 168, 2001, pp. 156-186.

Abstract The extension of first-order logic by means of a FOR-loop operator, governing the iteration of some formula in terms of the cardinality of a predicate defined by another formula, is analysed and various separations are proved. One of the results shows that BQL, the query language extending relational algebra with FOR-loops, is strictly weaker than FO(FOR), in contrast to the situation for WHILE-loops. Further results address the role of parameters in FOR-loop operators, the relation of FO(FOR) with fixed-point logics with counting, and phenomena related to the nesting depth of FOR-constructors.

Undecidability Results on Two-Variable Logics, with E. Grädel and E. Rosen,
Archive of Mathematical Logic, volume 38, 1999, 313-354.

Abstract It is a classical result of Mortimer's that L², first-order logic with two variables, is decidable for satisfiability. It is shown that going beyond L² by adding any one of the following leads to an undecidable logic:

• very weak forms of recursion, viz.

transitive closure operations , or
(restricted) monadic fixed-point operations
• weak access to cardinalities, through the Härtig (or equicardinality) quantifier , or
• a choice construct known as Hilbert's epsilon operator.

Bounded-Variable Logics: Two, Three, and More,
Archive for Mathematical Logic, volume 38, 1999, pp. 235-256.

Abstract This study concerns the bounded variable logics L^k (with k variable symbols), and C^k (with k variables in the presence of first-order counting quantifiers). These fragments of infinitary logic are well known to provide an adequate logical framework for some important issues in finite model theory. This paper deals with a translation that associates equivalence of structures in the k-variable fragments with bisimulation equivalence between derived structures. Apart from a uniform and intuitively appealing treatment of these equivalences, this approach relates some interesting issues for the case of an arbitrary number of variables to the case of just three variables. Invertibility of the invariants for C³, in particular, would imply a positive answer to the tempting conjecture that fixed-point logic with counting captures Ptime in the world of bounded variable logic with counting.

Adding FOR-Loops to First-Order Logic, with F. Neven, J. Tyszkiewicz, and J. Van den Bussche,
Proc. of ICDT'99, Lecture Notes in Computer Science No. 1540, Springer 1999, 58-69.

cf. journal version

Eliminating Recursion in the mu-Calculus,
Proc. of STACS'99, Lecture Notes in Computer Science No. 1563, Springer 1999, pp. 531-540.

Abstract The following decision problem is analysed: given a formula of the modal mu-calculus, decide whether there is some formula of basic modal logic equivalent to it. It is shown that this problem is decidable, and indeed Exptime complete. The decidability proof can be given through a purely model theoretic reduction to the monadic second-order theory of the binary tree, or through an analysis of suitably adapted tree automata. The latter analysis also yields a decision procedure in deterministic exponential time.

Beth Definability for the Guarded Fragment, with E. Hoogland and M. Marx,
Proc. of LPAR'99, LNAI, vol. 1705, Springer 1999, pp. 273-285.

See also in: JFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday, J. Gebrandy, M. Marx, M. de Rijke and Y. Venema (ed.), CD-ROM, Amsterdam University Press 1999.

Abstract The guarded fragment (GF) was introduced by Andreka, van Bethem, and Nemeti as a fragment of first order logic which combines a great expressive power with nice modal behavior. It consists of relational first order formulas whose quantifiers are relativized by atoms in a certain way. GF has been established as a particularly well-behaved fragment of first order logic in many respects. As was recently shown by Hoogland and Marx, however, interpolation fails in restriction to GF. In this paper we consider the Beth property of first order logic and show that, despite the failure of interpolation, it is retained in restriction to GF. Being a closure property w.r.t. definability, the Beth property is of independent interest, both theoretically and for typical potential applications of GF, e.g., in the context of description logics. The Beth property for GF is here established on the basis of a limited form of interpolation, which more closely resembles the interpolation property that is usually studied in modal logics. >From this we obtain that, more specifically, even every n-variable guarded fragment with up to n-ary relations has the Beth property.

On the Boundedness Problem for Two-Variable First-Order Logic, with P. Kolaitis,
Proc. of 13th IEEE Symposium on Logic in Computer Science LICS `98, Indianapolis, pp. 513-524.

Abstract A positive first-order formula is bounded if the sequence of its stages converges to the least fixed point of the formula within a fixed finite number of steps independent of the input structure. The boundedness problem for a fragment of first-order logic asks: given a positive formula in the fragment, is it bounded?

We investigate the boundedness problem for two-variable first-order logic, an otherwise very well-behaved and, in particular, decidable fragment of first-order logic. Our main result asserts that the boundedness problem for two-variable first-order logic is undecidable, even when restricted to negation-free and equality-free formulae with a single monadic predicate variable that occurs within the scopes of universal quantifiers only. This contrasts sharply with earlier decidability results for monadic Datalog programs, which amount to the decidability of boundedness for negation-free and equality-free existential first-order formulae with a single monadic predicate variable.

Our main result has certain applications to circumscription, the most well-developed formalism of nonmonotonic reasoning. Specifically, we show that it is an undecidable problem to tell whether the circumscription of a given two-variable first-order formula is equivalent to a first-order formula.

Bounded Variable Logics and Counting - A Study in Finite Models,

Lecture Notes in Logic volume 9, Springer 1997, IX+183 pages.
Now distributed through ASL

Abstract This is a comprehensive treatment of a variety of results on infinitary logics with a bounded number of variables, both with and without counting quantifiers, as well as on related fixed-point logics. The emphasis is on central issues in finite model theory and in particular on descriptive complexity. Despite its character as a research monograph the exposition is largely self-contained. Much room is given to connections with the existing body of work in this area. From the contents:

• An introduction to the relevant notions from logic, model theory, and to the programme of descriptive complexity.
• A systematic treatment of the relevant games and game-theoretic structural invariants.
• The analysis of fixed-point logics, both with and without counting.
• Canonization and inversion problems as an approach to capturing fragments of PTIME.
• Capturing results for the two-variable fragments of PTIME.

Undecidability Results on Two-Variable Logics, with E. Grädel and E. Rosen,
Proc. of 14th Symposium on Theoretical Aspects of Computer Science STACS `97 Lecture Notes in Computer Science No. 1200, Springer 1997, 249-260.

cf. journal version

Two-Variable Logic with Counting is Decidable, with E. Grädel and E. Rosen,
Proc. of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau, pp. 306-317.

Abstract The satisfiability problem for C² is shown to be decidable.
C² is first-order logic with only two variables in the presence of arbitrary counting quantifiers of the form ``there exist at least m''. It considerably extends L², plain first-order with only two variables, which is known to be decidable by a result of Mortimer. Unlike L², C² does not have the finite model property. As C² extends L² by expressive means for counting, significant applications arise from the fact that C² embeds corresponding counting extensions of modal logics.

Canonization for Two Variables and Puzzles on the Square,
Annals of Pure and Applied Logic, volume 85, 1997, pp. 243-282.

Abstract We consider infinitary logic with only two variable symbols, both with and without counting quantifiers, L² and C². The main result is that finite relational structures admit PTIME canonization with respect to L² and C²: there are polynomial time computable functors mapping finite relational structures to unique representatives of their equivalence class with respect to indistinguishability in either of these logics. In fact Ptime inverses are constructed for the natural Ptime invariants that characterize structures up to L²- or C²-equivalence, respectively. This yields a recursive representations of the classes of all Ptime boolean queries that are closed with respect to L²--or C²--equivalence.

Capturing Bisimulation-Invariant Ptime,
Proc. of 4th Symposium on Logical Foundations of Computer Science, LFCS `97, Lecture Notes in Computer Science No. 1234, Springer 1997, 294-305.

see extended version

The Logic of Explicitly Representation-Invariant Circuits,
Selected Papers of CSL `96, D. van Dalen and M. Bezem (ed.), Lecture Notes in Computer Science, volume 1258, Springer 1997, 369-384.

see also extended version

The Expressive Power of Fixed-Point Logic with Counting,
Journal of Symbolic Logic, volume 61, 1996, pp. 147-176.

Abstract This is an investigation in finite model theory concerning the expressive power of the logic FP+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. The analysis is carried out in parallel along two entirely different lines.
- One employs an isomorphism preserving (`generic') model of computation, whose PTIME restriction exactly corresponds to FP+Counting, while its PSPACE restriction corresponds to WHILE+Counting. A normal form gives a clear separation of the relational vs. the arithmetical side of the algorithms involved.
- The other one uses the connection with the infinitary logics C^r, r-variable infinitary logic with counting quantifiers, to apply the corresponding pebble games in the analysis.

The main result involves the concept of an arithmetical invariant. This is a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. A family of arithmetical invariants I^r with the following properties is introduced:

• each I^r can be evaluated in polynomial time.
• a class of finite relational structures is definable in FP+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants.
• I^r classifies all finite relational structures exactly up to equivalence with respect to the logic C^r.

First-Order Queries on Databases Embedded in an Infinite Structure,
with J. Van den Bussche,
Information Processing Letters, volume 60, 1996, pp. 37-41.

Abstract We consider ``generic'' (isomorphism-invariant) queries on relational databases embedded in an infinite background structure. Assume a generic query is expressible by a first-order formula over the embedded domain that may involve both the relations of the database and the relations and functions of the background structure. Then this query is already expressible by a first-order formula involving just an auxiliary linear ordering as background structure. We present an elementary proof of this fact.

Bounded Variable Logics and Counting - A Study in Finite Models,
Habilitationsschrift (English), RWTH Aachen, 1995, 190 pages.

compare monograph

A Note on the Number of Monadic Quantifiers in Monadic Sigma_1^1,
Information Processing Letters, volume 53, 1995, pp. 337-339.

Abstract A simple proof is given, that the number of monadic quantifiers in existential monadic second-order logic gives rise to a strict hierarchy over finite structures. This resolves a problem put forward by R.Fagin.

Ptime Canonization for Two Variables with Counting,
Proc. of 10th IEEE Symposium on Logic in Computer Science LICS `95, San Diego, pp. 342-352.

also see journal version

Abstract Infinitary logic with two variable symbols and counting quantifiers C² and its intersection with PTIME are considered on finite relational structures. A PTIME canonization procedure is presented which provides unique representatives up to equivalence in C² for finite relational structures. As a consequence there is a recursive presentation for the class of all those queries on arbitrary finite relational structures which are both PTIME and definable in C². The proof renders a succinct normal form representation of this non-trivial semantically defined fragment of PTIME. Through specializations of the proof techniques similar results apply with respect to the logic L², infinitary logic with two variable symbols, itself.

Generalized Quantifiers for Simple Properties,
Proc. of 9th IEEE Symposium on Logic in Computer Science LICS `94, Paris, pp. 30-39.

Abstract Extensions of fixed-point logic by means of generalized quantifiers are considered in the context of descriptive complexity. By the well-known theorem of Immerman and Vardi, fixed-point logic captures PTIME over linearly ordered structures. It fails, however, to express even most fundamental structural properties, like simple cardinality properties, in the absence of order.
The present investigation concentrates on extensions by generalized quantifiers which serve to adjoin simple or basic structural properties. An abstract notion of simplicity is put forward which isolates those structural properties, that can be characterized in terms of a concise structural invariant . The key examples are provided by all monadic and cardinality properties in a very general sense.
The main theorem establishes that no extension by any family of such simple quantifiers can cover all of PTIME. These limitations are proved on the basis of the semantically motivated notion of simplicity; in particular there is no implicit bound on the arities of the generalized quantifiers involved. Quite to the contrary, the natural applications concern infinite families of quantifiers adjoining certain structural properties across all arities in a uniform way.

Inductive Definability with Counting on Finite Structures, with E. Grädel
Selected Papers, 6th Workshop on Computer Science Logic CSL `92, San Miniato 1992, Lecture Notes in Computer Science No. 702, Springer 1993, pp. 231-247.

Abstract The properties and the expressive power of logical languages that include both a mechanism for inductive definitions and the ability to count are studied. The most important of these languages is fixed-point logic with counting terms, denoted FP+C.
It is shown that in the presence of counting terms inductive definability on arbitrary finite structures has nice properties that it retains without counting only in the case of ordered structures.
Main issues of the investigation concern:

• equivalent charcterizations and robustness of FP+C: e.g. FP+C is equivalent with DATALOG+C and offers intuitive functional as well as machine theoretic characterizations.
• relations with infinitary logic with bounded number of variables and counting quantifiers.
• relations with partial fixed-point logic with counting, PFP+C.

Automorphism Properties of Stationary Logic,
Journal of Symbolic Logic, volume 57, 1992, pp. 231-237.

EM Functors for a Class of Generalized Quantifiers,
Archive for Mathematical Logic, volume 31, 1992, pp. 355-371.

A Reduction Scheme for Phase Spaces with Almost-Kähler Symmetry -- Regularity Results for Momentum Level Sets,
Journal of Geometry and Physics volume 4 (1987), 101-118.

Ehrenfeucht-Mostowski Konstruktionen in Erweiterungslogiken,
Doctoral dissertation (German), Freiburg University, 1990, 94 pages.

Symmetry and First-Order: Explicitly Representation-Invariant Circuits,
unpublished extended version (32 pages) of CSL paper, 1994.

Abstract Circuit complexity is considered under the additional assumption of full combinatorial symmetry with respect to permutations of the input representation. This approach leads to a very natural and simple characterization of first-order logic and its infinitary variant with bounded numbers of variables over finite structures. Extensions to not necessarily acyclic boolean networks provide corresponding characterizations of partial fixed-point logic (or the relational query language WHILE) and ordinary fixed-point logic.