Querying the guarded fragment,
with Vince Barany and Georg Gottlob.
LICS 2010.
Abstract
Evaluating a boolean conjunctive query q over a
guarded first-order theory phi is equivalent to checking
whether phi & not q is unsatisfiable.
This problem is relevant to the areas of database theory
and description logic.
Since q may not be guarded, well known results about
the decidability, complexity, and finite-model property
of the guarded fragment do not obviously carry over to
conjunctive query answering over guarded theories,
and had been left open in general.
By investigating finite guarded bisimilar covers of hypergraphs
and relational structures, and by substantially generalising
Rosati's finite chase, we prove for guarded theories phi
and (unions of) conjunctive queries q that
(i) phi implies q iff phi implies q over all finite structures
and
(ii) that this problem is complete for 2EXPTIME.
We further show the following results:
(iii) the existence of polynomial-size conformal covers
of arbitrary hypergraphs;
(iv) a new proof of the finite model property of the
clique-guarded fragment;
(v) the small model property of the guarded fragment
with optimal bounds;
(vi) a polynomial-time solution to the canonisation problem
modulo guarded bisimulation, which yields
(vii) a capturing result for guarded-bisimulation-invariant PTIME.
Highly Acyclic Groups, Hypergraph Covers and the Guarded Fragment,
preprint, revised 2011, 45 pages.
Abstract We construct finite groups whose Cayley graphs have large girth even w.r.t. a discounted distance measure that contracts arbitrarily long sequences of edges from the same colour class, and only counts transitions between colour classes. These groups are shown to be useful in the construction of finite bisimilar hypergraph covers that avoid any small cyclic configurations. We present two applications to the finite model theory of the guarded fragment: a strengthening of the known finite model property for GF and the characterisation of GF as the guarded bisimulation invariant fragment of FO in the sense of finite model theory.
Avoiding Incidental Homomorphisms Into Guarded Covers,
TUD online preprint no.2600,
technical report, 2009, 10 pages.
Abstract
For a given finite relational structure,
we construct a finite guarded-bisimilar companion structure
(a guarded cover) that avoids all avoidable homomorphic images of
other structures.
`Avoidable' turns out to mean that the given homomorphism does not
lift to guarded unravellings of the original structure, hence can at
least be eliminated in infinite guarded-bisimilar companion
structures. We thus get the finite model property for an extension of
the guarded fragment by `forbidden homomorphic images.'
This note is based on material first presented at a finite model
theory workshop in Cambridge, 2001, and revised in 2008/09.
A Lindström Characterisation of the Guarded Fragment
and of Modal Logic With a Global Modality,
with Robert Piro.
in: Advances in Modal Logic 7, C. Areces, R. Goldblatt (eds),
2008, pp. 273-288.
Abstract We establish a Lindström type characterisation of the extension of basic modal logic by a global modality and of the guarded fragment of first-order logic as maximal among compact logics with the corresponding bisimulation invariance and the Tarski Union Property.
Modal Characterisation Theorems over Special Classes of Frames,
with A. Dawar
Annals of Pure and Applied Logic, volume 161, 2009, pp. 1-42.
Considerably extended and revised journal version of LICS 2005 paper
Abstract We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van~Benthem's theorem which says that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes - for instance, rooted frames, finite rooted frames, finite transitive frames, well-founded transitive frames, finite equivalence frames - as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraisse versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes. Over most of the classes considered we obtain finite model theory analogues of the classically expected characterisations, with new proofs also for the classical setting. The class of transitive frames is a notable exception, with a marked difference between the classical and the finite model theory of bisimulation invariant first-order properties. Over the class of all finite transitive frames in particular, we find that monadic second-order logic is no more expressive than first-order as far as bisimulation invariant properties are concerned - though both are more expressive here than basic modal logic. We obtain ramifications of the de Jongh-Sambin theorem and a new and specific analogue of the Janin-Walukiewicz characterisation of bisimulation invariant monadic second-order for finite transitive frames.
Boundedness of Monadic Second-Order Formulae Over Finite Words,
with A. Blumensath and M. Weyer.
ICALP'09, LNCS, volume 5556, 2009, pp. 67-78.
Abstract It is shown that the boundedness problem for monadic least fixed points in monadic second-order logic is decidable over the class of all finite word structures.
Decidability results for the boundedness problem,
with A. Blumensath and M. Weyer.
Preprint of extended journal version based on results in the
ICALP'09 paper, 2011, 43 pages.
Abstract We prove decidability of the boundedness problem for monadic least fixed-point recursion based on positive monadic second-order (MSO) formulae over trees. Given an MSO-formula that is positive in X, it is decidable whether the fixed-point recursion based on this formula is spurious over the class of all trees in the sense that there is some uniform finite bound for the number of iterations it takes to reach its least fixed point, uniformly across all trees. We also identify the exact complexity of this problem. The proof uses automata-theoretic techniques. This key result extends, by means of model-theoretic interpretations, to show decidability of the boundedness problem for MSO and guarded second-order logic (GSO) over the classes of structures of fixed finite tree-width. Further model-theoretic transfer arguments allow us to derive major known decidability results for boundedness for fragments of first-order logic as well as new ones.
Boundedness of Monadic FO Over Acyclic Structures,
with S. Kreutzer and N. Schweikardt.
ICALP'07, LNCS, volume 4596, 2007, pp. 571 - 582.
Abstract We study the boundedness problem for monadic least fixed points as a decision problem. While this problem is known to be undecidable in general and even for syntactically very restricted classes of underlying first-order formulae, we here obtain a decidability result for the boundedness issue for monadic fixed points over arbitrary first-order formulae in restriction to acyclic structures.
The Boundedness Problem for Monadic Universal First-Order Logic
Proceedings of 21th IEEE Symposium on Logic in Computer
Science LICS 2006, pp 37-46.
Abstract Consider the monadic boundedness problem for least fixed points over FO formulae as a decision problem: Given a formula that is positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on this formula. Few fragments of FO are known to have a decidable boundedness problem; boundedness is known to be undecidable for many fragments. We here show that monadic boundedness is decidable for purely universal FO formulae without equality in which each non-recursive predicate occurs in just one polarity (e.g., only negatively). The restrictions are shown to be essential: waving either the polarity constraint or allowing positive occurrences of equality, the monadic boundedness problem for universal formulae becomes undecidable. The main result is based on a model theoretic analysis involving ideas from modal and guarded logics and a reduction to the monadic second-order theory of trees.
Boundedness of Monadic FO over Acyclic Structures,
with S. Kreutzer and N. Schweikardt.
Proceedings of 34th International Colloquium
on Automata, Languages and Programming
ICALP 2007, LNCS 4596, pp 571-582.
Abstract The boundedness problem for monadic least fixed points is studied as a decision problem. While this problem is known to be undecidable in general and even for syntactically very restricted classes of underlying first-order formulae, we here obtain a decidability result for the boundedness issue for monadic fixed points over arbitrary first-order formulae in restriction to acyclic structures. This is meant to provide a first significant step towards a shift emphasis of the boundedness problem from fragments of first-order logic to full (monadic) first-order logic over suitably restricted classes of structures; and thus part of recent efforts towards an algorithmic model theory for `well-behaved' classes of structures.
Modal Characterisation Theorems over Special Classes of Frames,
with A. Dawar
Proceedings of 20th IEEE Symposium on Logic in Computer
Science LICS 2005, pp 21-30.
Abstract
We investigate model theoretic characterisations of
the expressive power of modal logics in terms of bisimulation
invariance. The paradigmatic result of this kind is van Benthem's theorem
which says that a first-order formula is invariant under bisimulation if,
and only if,
it is equivalent to a formula of basic modal logic. The present investigation
primarily concerns ramifications for specific classes of structures.
We study in particular model classes defined through
conditions on the underlying frames, with a focus on frame classes that play
a major role in modal correspondence theory and often correspond to typical
application domains of modal logics. Classical model theoretic arguments
do not apply to many of the most interesting classes - for instance,
rooted connected frames, well-founded frames, finite rooted connected frames,
finite transitive frames,
finite equivalence frames - as these are not
elementary. Instead we develop and extend the game-based analysis
(first-order Ehrenfeucht-Fraisse versus bisimulation games)
over such classes and provide bisimulation preserving model
constructions within these classes.
Note: An erroneous claim concerning the characterisation
of bisimulation invariance over the class of all finite (rooted)
transitive frames will be corrected in the forthcomming
journal version.
Small Substructures and Decidability Issues
for Two-Variable First-Order Logic,
with E. Kieronski
Proceedings of 20th IEEE Symposium on Logic in Computer
Science LICS 2005, pp 448-457.
Abstract We study first-order logic with two variables FO2 and establish a small substructure property. Similar to the small model property for FO2 we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO2 under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO2 has the finite model property and is complete for non-deterministic exponential time, just as for plain FO2. With two equivalence relations, FO2 does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO2 is undecidable.
Modal and Guarded Characterisation Theorems over Finite
Transition Systems
,
Annals of Pure and Applied Logic,
volume 130, 2004, pp. 173-205.
Journal version of LICS 2002 paper.
Abstract
This paper explores the characterisation theorems
for modal and guarded logics -
characterising them as the bisimulation invariant fragments
of first-order logic under appropriate notions of bisimulation -
over transition systems and relational structures of width 2,
especially in the context of finite model theory.
Van Benthem's classical characterisation of basic modal logic
has been shown to be valid also in the sense of finite model theory,
with a completely different proof, by Rosen. This paper also
gives a simplified proof of that result.
Corresponding characterisations are proved for the extension of basic
modal logic by universal and by inverse modalities (as the fragment
invariant under global two-way bisimulations) and
of the width two guarded fragment (as the fragment invariant under
guarded bisimulation). The proofs exploit Gaifman's locality theorem for
first-order logic together with a natural construction of finite, locally
acyclic, bisimilar covers for finite transition systems.
All proofs not only apply in finite model theory but also carry over
to yield new proofs in the classical setting.
It remains open whether the charactersation of the guarded fragment
as the guarded bisimulation invariant fragment of first-order logic which is
here only shown over structures of width 2, extends to relational
vocabularies in general.
Elementary Proof of the van Benthem - Rosen Characterisation Theorem,
revised 2004,
TUD online preprint, 10 pages.
Abstract
This note presents an elementary proof of the well-known
characterisation theorem that associates propositional modal logic
with the bisimulation invariant fragment of first-order logic.
The classical version of this theorem is due to Johann van Benthem,
its finite model theory analogue to Eric Rosen.
The present proof of the van Benthem - Rosen characterisation theorem
is uniformly applicable in both the classical and in the finite model
theory scenario. While it is broadly based on Rosen's proof, it
reduces the technical input from classical logic and the model theory of
modal logics strictly to the use of Ehrenfeucht-Fraisse games
(for first-order, and for the modal variant). Furthermore the proof
is constructive and the model constructions and accompanying
analysis of games in the expressive completeness argument
yield an optimal bound on the modal nesting depth
in terms of the first-order quantifier rank. Despite this strengthening,
the material becomes presentable in a highly self-contained manner,
and can be covered even at the level of an introductory undergraduate
course on logic and semantic games that covers the basic
Ehrenfeucht-Fraisse techniques.
Bisimulation Invariance and Finite Models
,
in: Lecture Notes in Logic,
Logic Colloquium 02, 2006, pp. 276-298.
Abstract We study bisimulation invariance over finite structures. This investigation leads to a new, quite elementary proof of the van Benthem-Rosen characterisation of basic modal logic as the bisimulation invariant fragment of first-order logic. The ramification of this characterisation for the finer notion of global two-way bisimulation equivalence is based on bisimulation respecting constructions of models that recover in finite models some of the desirable properties of the usually infinite bisimilar unravellings.
Finite Conformal Hypergraph Covers
and
Gaifman Cliques in Finite Structures,
with I. Hodkinson
Bulletin of Symbolic Logic, volume 9, 2003, pp. 387-405.
Abstract
Every finite hypergraph is shown to admit a cover
by a finite conformal hypergraph. The notion of a hypergraph cover
is based on homomorphisms that induce a bisimulation like back-and-forth
system of local bijections between hyperedges. It is here introduced
to capture
the essential features of guarded bisimulations in the hypergraph setting.
The classical hypergraph notion of conformality, defined by the requirement
that all induced cliques be contained within hyperedges,
thus corresponds to the collapse of clique guardedness to plain guardedness.
As far as conformality is concerned, our construction can serve as a
substitute in finite model theory for the straightforward but
generally infinite unravelling of hypergraphs or relational structures.
Two immediate applications to the finite model theory of relational
structures are presented:
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^{2}
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^{2} 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^{2}, namely non-deterministic exponential time.
In contrast FO^{2} 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^{2}
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^{2}, first-order logic with two variables, is decidable for satisfiability. It is shown that going beyond L^{2} by adding any one of the following leads to an undecidable logic:
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^{3}, 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:
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^{2} is shown to be decidable.
C^{2} 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^{2}, plain first-order with
only two variables, which is known to be decidable by a result of Mortimer.
Unlike L^{2}, C^{2} does not have the finite model property.
As C^{2} extends L^{2} by expressive means for counting,
significant applications arise from the fact that C^{2} 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^{2} and C^{2}. The main result is that finite relational structures admit PTIME canonization with respect to L^{2} and C^{2}: 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^{2}- or C^{2}-equivalence, respectively. This yields a recursive representations of the classes of all Ptime boolean queries that are closed with respect to L^{2}--or C^{2}--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:
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^{2} 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^{2} 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^{2}. 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^{2}, 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:
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.
M. Otto