Erich Grädel

CSL Conference 2026 Conference Paper

Compactness in Semiring Semantics

• Sophie Brinke
• Anuj Dawar
• Erich Grädel
• Lovro Mrkonjic
• Matthias Naaf

Semiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query. To this end, logical statements are not just evaluated to true or false but 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. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This raises the question to what extent model-theoretic results can be generalised to semiring semantics and how this relates to the algebraic properties of the underlying semiring. Here we investigate the availability of compactness in semiring semantics. The appropriate setting for this is based on absorptive semirings with well-defined infinitary products. Compactness can be stated either in terms of satisfiability or in terms of entailment, and these two variants are trivially equivalent in Boolean semantics. However, this is no longer the case in semiring semantics. Compactness in terms of satisfiability, defined as the existence of non-zero valuations, indeed generalises to every infinitary absorptive semiring. For compactness in terms of entailment the situation is different. The entailment relation naturally extends to semiring semantics (via the natural order on the semiring) but this yields a stronger variant of compactness, which fails for certain important semirings, including the tropical semiring and the Łukasiewicz semiring. Our main positive results show that strong compactness does indeed hold for all finite semirings and all lattice semirings.

MFCS Conference 2025 Conference Paper

Symmetric Proofs in the Ideal Proof System

• Anuj Dawar
• Erich Grädel
• Leon Kullmann
• Benedikt Pago

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.

CSL Conference 2024 Conference Paper

Ehrenfeucht-Fraïssé Games in Semiring Semantics

• Sophie Brinke
• Erich Grädel
• Lovro Mrkonjic

Ehrenfeucht-Fraïssé games provide a fundamental method for proving elementary equivalence (and equivalence up to a certain quantifier rank) of relational structures. We investigate the soundness and completeness of this method in the more general context of semiring semantics. Motivated originally by provenance analysis of database queries, semiring semantics evaluates logical statements not just by true or false, but by values in some commutative semiring; this can provide much more detailed information, for instance concerning the combinations of atomic facts that imply the truth of a statement, or practical information about evaluation costs, confidence scores, access levels or the number of successful evaluation strategies. There is a wide variety of different semirings that are relevant for provenance analysis, and the applicability of classical logical methods in semiring semantics may strongly depend on the algebraic properties of the underlying semiring. While Ehrenfeucht-Fraïssé games are sound and complete for logical equivalences in classical semantics, and thus on the Boolean semiring, this is in general not the case for other semirings. We provide a detailed analysis of the soundness and completeness of model comparison games on specific semirings, not just for classical Ehrenfeucht-Fraïssé games but also for other variants based on bijections or counting. Finally we propose a new kind of games, called homomorphism games, based on the fact that there exist locally very different semiring interpretations that can be proved to be elementarily equivalent via separating sets of homomorphisms. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite lattice semirings.

MFCS Conference 2023 Conference Paper

Locality Theorems in Semiring Semantics

• Clotilde Bizière
• Erich Grädel
• Matthias Naaf

Semiring semantics of first-order logic generalises classical Boolean semantics by permitting truth values from a commutative semiring, which can model information such as costs or access restrictions. This raises the question to what extent classical model-theoretic properties still apply, and how this depends on the algebraic properties of the semiring. In this paper, we study this question for the classical locality theorems due to Hanf and Gaifman. We prove that Hanf’s locality theorem generalises to all semirings with idempotent operations, but fails for many non-idempotent semirings. We then consider Gaifman normal forms and show that for formulae with free variables, Gaifman’s theorem does not generalise beyond the Boolean semiring. Also for sentences, it fails in the natural semiring and the tropical semiring. Our main result, however, is a constructive proof of the existence of Gaifman normal forms for min-max and lattice semirings. The proof implies a stronger version of Gaifman’s classical theorem in Boolean semantics: every sentence has a Gaifman normal form which does not add negations.

GandALF Workshop 2021 Workshop Paper

Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials

• Erich Grädel
• Niels Lücking
• Matthias Naaf

This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in Büchi 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üchi 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.

CSL Conference 2021 Conference Paper

Semiring Provenance for Fixed-Point Logic

• Katrin M. Dannert
• Erich Grädel
• Matthias Naaf
• Val Tannen

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.

Highlights Conference 2021 Conference Abstract

Semiring Provenance for LFP and Strategy Analysis in Büchi Game

• Erich Grädel

We present a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in Büchi games. Semiring semantics generalises 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. The case of Büchi games is of special interest for this approach, 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 further applications such as game synthesis or determining minimal modifications to the game needed to change its outcome.

CSL Conference 2020 Conference Paper

Guarded Teams: The Horizontally Guarded Case

• Erich Grädel
• Martin Otto 0001

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.

MFCS Conference 2019 Conference Paper

Choiceless Logarithmic Space

• Erich Grädel
• Svenja Schalthöfer

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.

CSL Conference 2018 Conference Paper

Dependency Concepts up to Equivalence

• Erich Grädel
• Matthias Hoelzel

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.

CSL Conference 2017 Conference Paper

Advice Automatic Structures and Uniformly Automatic Classes

• Faried Abu Zaid
• Erich Grädel
• Frederic Reinhardt

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.

CSL Conference 2017 Conference Paper

The Model-Theoretic Expressiveness of Propositional Proof Systems

• Erich Grädel
• Benedikt Pago
• Wied Pakusa

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 polynomial 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 (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.

CSL Conference 2016 Conference Paper

Counting in Team Semantics

• Erich Grädel
• Stefan Hegselmann

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.

CSL Conference 2015 Conference Paper

Rank Logic is Dead, Long Live Rank Logic!

• Erich Grädel
• Wied Pakusa

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. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power. In our first main result we show that the extensions of FPC by 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 FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR. One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by 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.

TCS Journal 2014 Journal Article

The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs

• Felix Canavoi
• Erich Grädel
• Roman Rabinovich

The problem whether winning regions and wining strategies for parity games can be computed in polynomial time is a major open problem in the field of infinite games, which is relevant for many applications in logic and formal verification. For some time the discrete strategy improvement algorithm due to Jurdziński and Vöge had been considered to be a candidate for solving parity games in polynomial time. However, it has recently been proved by Oliver Friedmann that this algorithm requires super-polynomially many iteration steps, for all popular local improvements rules, including switch-all (also with Fearnley's snare memorisation), switch-best, random-facet, random-edge, switch-half, least-recently-considered, and Zadeh's Pivoting rule. We analyse the examples provided by Friedmann in terms of complexity measures for directed graphs such as treewidth, DAG-width, Kelly-width, entanglement, directed pathwidth, and cliquewidth. It is known that for every class of parity games on which one of these parameters is bounded, the winning regions can be efficiently computed. It turns out that with respect to almost all of these measures, the complexity of Friedmann's counterexamples is bounded, and indeed in most cases by very small numbers. This analysis strengthens in some sense Friedmann's results and shows that the discrete strategy improvement algorithm is even more limited than one might have thought. Not only does it require super-polynomial running time in the general case, where the problem of polynomial-time solvability is open, it even has super-polynomial time lower bounds on natural classes of parity games on which efficient algorithms are known.

Highlights Conference 2013 Conference Abstract

Invited talk: Linear Algebra and the quest for a logic for PTIME

• Erich Grädel

The quest for a logic for PTIME is one of the central open problems in both finite model theory and database theory. It asks whether there is a logic in which a property of finite structures is definable if, and only if, it is decidable in polynomial time. Much of the research in this area has focused on the logic FPC, the extension of least or inflationary fixed-point logic by counting terms. In fact, FPC has been shown to capture PTIME on many natural classes of structures. On the other side, already in 1992, a graph query has been constructed that can be decided in PTIME but is not definable in FPC. But while this CFI query, as it is now called, is very elegant and has led to new insights in many different areas, it can hardly be called a natural problem in polynomial time. Therefore it was often remarked that possibly all natural polynomial-time properties of finite structures could be expressed in FPC. However, this hope was eventually refuted in a strong sense by Atserias, Bulatov and Dawar who proved that the important problem of solvability of linear equation systems (over any finite Abelian group) is not definable in FPC and that, indeed, the CFI query reduces to this problem. This motivates the study of the relationship between finite model theory and linear algebra, and suggests that operators from linear algebra, such as matrix ranks or solvability operators, could be a source of new extensions to fixed-point logic, in an attempt to find a logical characterisation of PTIME. We will discuss such approaches and study the relations between different polynomial-time computable problems over (finite) rings, fields and Abelian groups in the context of logical many-to-one and Turing reductions, i. e. , interpretations and generalised quantiers. In this context, we will also discuss an alternative approach towards a logic for PTIME, proposed by Blass, Gurevich and Shelah, based on choiceless computations operating directly on structures. 09: 50 10: 00 Break

TCS Journal 2013 Journal Article

Model-checking games for logics of imperfect information

• Erich Grädel

Logics of dependence and independence have semantics that, unlike Tarski semantics, are not based on single assignments (mapping variables to elements of a structure) but on sets of assignments. Sets of assignments are called teams and the semantics is called team semantics. We design model-checking games for logics with team semantics in a general and systematic way. The construction works for any extension of first-order logic by atomic formulae on teams, as long as certain natural conditions are observed which are satisfied by all team properties considered so far in the literature, including dependence, independence, constancy, inclusion, and exclusion. The second-order features of team semantics are reflected by the notion of a consistent winning strategy which is also a second-order notion in the sense that it depends not on single plays but on the space of all plays that are compatible with the strategy. Beyond the application to logics with team semantics, we isolate an abstract, purely combinatorial definition of such games, which may be viewed as second-order reachability games, and study their algorithmic properties. A number of examples are provided that show how logics with team semantics express familiar combinatorial problems in a somewhat unexpected way. Based on our games, we provide a complexity analysis of logics with team semantics.

CSL Conference 2012 Conference Paper

Banach-Mazur Games with Simple Winning Strategies

• Erich Grädel
• Simon Leßenich

We discuss several notions of "simple" winning strategies for Banach-Mazur games on graphs, such as positional strategies, move-counting or length-counting strategies, and strategies with a memory based on finite appearance records (FAR). We investigate classes of Banach-Mazur games that are determined via these kinds of winning strategies. Banach-Mazur games admit stronger determinacy results than classical graph games. For instance, all Banach-Mazur games with omega-regular winning conditions are positionally determined. Beyond the omega-regular winning conditions, we focus here on Muller conditions with infinitely many colours. We investigate the infinitary Muller conditions that guarantee positional determinacy for Banach-Mazur games. Further, we determine classes of such conditions that require infinite memory but guarantee determinacy via move-counting strategies, length-counting strategies, and FAR-strategies. We also discuss the relationships between these different notions of determinacy.

CSL Conference 2012 Conference Paper

Definability of linear equation systems over groups and rings

• Anuj Dawar
• Erich Grädel
• Bjarki Holm
• Eryk Kopczynski
• Wied Pakusa

Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Further, we prove closure properties for classes of queries that reduce to solvability over rings. As an application, these closure properties provide normal forms for logics extended with solvability operators.

TCS Journal 2012 Journal Article

Entanglement and the complexity of directed graphs

• Dietmar Berwanger
• Erich Grädel
• Łukasz Kaiser
• Roman Rabinovich

Entanglement is a parameter for the complexity of finite directed graphs that measures to what extent the cycles of the graph are intertwined. It is defined by way of a game similar in spirit to the cops and robber games used to describe treewidth, directed treewidth, and hypertree width. Nevertheless, on many classes of graphs, there are significant differences between entanglement and the various incarnations of treewidth. Entanglement is intimately related with the computational and descriptive complexity of the modal μ -calculus. The number of fixed-point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. This plays a crucial role in the proof that the variable hierarchy of the μ -calculus is strict. We study complexity issues for entanglement and compare it to other structural parameters of directed graphs. One of our main results is that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of subgames induced by a winning strategy. Furthermore, we discuss the case of graphs of entanglement two. While graphs of entanglement zero and one are very simple, graphs of entanglement two allow arbitrary nesting of cycles, and they form a sufficiently rich class for modelling relevant classes of structured systems. We provide characterisations of this class, and propose decomposition notions similar to the ones for treewidth, DAG-width, and Kelly-width.

GandALF Workshop 2012 Workshop Paper

The discrete strategy improvement algorithm for parity games and complexity measures for directed graphs

• Felix Canavoi
• Erich Grädel
• Roman Rabinovich

For some time the discrete strategy improvement algorithm due to Jurdzinski and Voge had been considered as a candidate for solving parity games in polynomial time. However, it has recently been proved by Oliver Friedmann that the strategy improvement algorithm requires super-polynomially many iteration steps, for all popular local improvements rules, including switch-all (also with Fearnley's snare memorisation), switch-best, random-facet, random-edge, switch-half, least-recently-considered, and Zadeh's Pivoting rule. We analyse the examples provided by Friedmann in terms of complexity measures for directed graphs such as treewidth, DAG-width, Kelly-width, entanglement, directed pathwidth, and cliquewidth. It is known that for every class of parity games on which one of these parameters is bounded, the winning regions can be efficiently computed. It turns out that with respect to almost all of these measures, the complexity of Friedmann's counterexamples is bounded, and indeed in most cases by very small numbers. This analysis strengthens in some sense Friedmann's results and shows that the discrete strategy improvement algorithm is even more limited than one might have thought. Not only does it require super-polynomial running time in the general case, where the problem of polynomial-time solvability is open, it even has super-polynomial lower time bounds on natural classes of parity games on which efficient algorithms are known.

CSL Conference 2010 Invited Paper

Definability in Games

• Erich Grädel

Abstract We shall present a survey on definability questions for graph games. Infinite games on graphs, where two players move a token along the edges of a directed graph tracing out a finite or infinite path, are intimately connected with fundamental questions in logic and have numerous applications in different areas of mathematics and computer science.

CSL Conference 2008 Conference Paper

The Descriptive Complexity of Parity Games

• Anuj Dawar
• Erich Grädel

Abstract We study the logical definablity of the winning regions of parity games. For games with a bounded number of priorities, it is well-known that the winning regions are definable in the modal μ -calculus. Here we investigate the case of an unbounded number of priorities, both for finite game graphs and for arbitrary ones. In the general case, winning regions are definable in guarded second-order logic (GSO), but not in least-fixed point logic (LFP). On finite game graphs, winning regions are LFP-definable if, and only if, they are computable in polynomial time, and this result extends to any class of finite games that is closed under taking bisimulation quotients.

TCS Journal 2006 Journal Article

Backtracking games and inflationary fixed points

• Anuj Dawar
• Erich Grädel
• Stephan Kreutzer

We define a new class of games, called backtracking games. Backtracking games are essentially parity games with an additional rule allowing players, under certain conditions, to return to an earlier position in the play and revise a choice or to force a countback of the number of moves. This new feature makes backtracking games more powerful than parity games. As a consequence, winning strategies become more complex objects and computationally harder. The corresponding increase in expressiveness allows us to use backtracking games as model-checking games for inflationary fixed-point logics such as IFP or MIC. We identify a natural subclass of backtracking games, the simple games, and show that these are the “right” model-checking games for IFP by (a) giving a translation of formulae φ and structures A into simple games such that A ⊨ φ if, and only if, Player 0 wins the corresponding game and (b) showing that the winner of simple backtracking games can again be defined in IFP.

CSL Conference 2006 Conference Paper

The Ackermann Award 2006

• Samson Abramsky
• Erich Grädel
• Johann A. Makowsky

Abstract The second Ackermann Award is presented at this CSL’06. Eligible for the 2006 Ackermann Award were PhD dissertations in topics specified by the EACSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1. 1. 2004 and 31. 12. 2005. The jury received 14 nominations for the Ackermann Award 2006. The candidates came from 10 different nationalities from Europe, the Middle East and India, and received their PhDs in 9 different countries in Europe, Israel and North America.

CSL Conference 2005 Conference Paper

The Ackermann Award 2005

• Erich Grädel
• Johann A. Makowsky
• Alexander A. Razborov

Abstract At the annual conference of the EACSL, CSL’04, it was suggested to the newly elected president of EACSL that steps be taken to make the Annual Conference of EACSL even more attractive for young researchers in Logic and Computer Science. In response to this suggestion, the EACSL Board decided in November 2004 to launch the Ackermann Award, the EACSL Outstanding Dissertation Award for Logic in Computer Science.

LPAR Conference 2004 Conference Paper

Entanglement - A Measure for the Complexity of Directed Graphs with Applications to Logic and Games

• Dietmar Berwanger
• Erich Grädel

Abstract We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. This measure, called entanglement, is defined by way of a game that is somewhat similar in spirit to the robber and cops games used to describe tree width, directed tree width, and hypertree width. Nevertheless, on many classes of graphs, there are significant differences between entanglement and the various incarnations of tree width. Entanglement is intimately connected to the computational and descriptive complexity of the modal μ -calculus. On the one hand, the number of fixed point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. This plays a crucial role in the proof that the variable hierarchy of the μ -calculus is strict. In addition to this, we prove that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of a subgame induced by a winning strategy.

LPAR Conference 2003 Conference Paper

Once upon a Time in a West - Determinacy, Definability, and Complexity of Path Games

• Dietmar Berwanger
• Erich Grädel
• Stephan Kreutzer

We study determinacy, definability and complexity issues of path games on finite and infinite graphs. Compared to the usual format of infinite games on graphs (such as Gale-Stewart games) we consider here a different variant where the players select in each move a path of arbitrary finite length, rather than just an edge. The outcome of a play is an infinite path, the winning condition hence is a set of infinite paths, possibly given by a formula from S1S, LTL, or first-order logic. Such games have a long tradition in descriptive set theory (in the form of Banach-Mazur games) and have recently been shown to have interesting application for planning in nondeterministic domains. It turns out that path games behave quite differently than classical graph games. For instance, path games with Muller conditions always admit positional winning strategies which are computable in polynomial time. With any logic on infinite paths (defining a winning condition) we can associate a logic on graphs, defining the winning regions of the associated path games. We explore the relationships between these logics. For instance, the winning regions of path games with an S1S-winning condition are definable in the modal mu-calculus. Further, if the winning condition is first-order (on paths), then the winning regions are definable in monadic path logic, or, for a large class of games, even in first-order logic. As a consequence, winning regions of LTL path games are definable in CTL.

TCS Journal 2002 Journal Article

Guarded fixed point logics and the monadic theory of countable trees

• Erich Grädel

Different variants of guarded logics (a powerful generalization of modal logics) are surveyed and an elementary proof for the decidability of guarded fixed point logics is presented. In a joint paper with Igor Walukiewicz, we proved that the satisfiability problems for guarded fixed point logics are decidable and complete for deterministic double exponential time (E. Grädel and I. Walukiewicz, Proc. 14th IEEE Symp. on Logic in Computer Science, 1999, pp. 45–54). That proof relies on alternating automata on trees and on a forgetful determinacy theorem for games on graphs with unbounded branching. The exposition given here emphasizes the tree model property of guarded logics: every satisfiable sentence has a model of bounded tree width. Based on the tree model property, we show that the satisfiability problem for guarded fixed point formulae can be reduced to the monadic theory of countable trees (SωS), or to the μ-calculus with backwards modalities.

CSL Conference 2002 Conference Paper

On the Variable Hierarchy of the Modal µ-Calculus

• Dietmar Berwanger
• Erich Grädel
• Giacomo Lenzi

Abstract We investigate the structure of the modal μ-calculus L μ with respect to the question of how many different fixed point variables are necessary to define a given property. Most of the logics commonly used in verification, such as CTL, LTL, CTL *, PDL, etc. can in fact be embedded into the two-variable fragment of the μ-calculus. It is also known that the two-variable fragment can express properties that occur at arbitrarily high levels of the alternation hierarchy. However, it is an open problem whether the variable hierarchy is strict. Here we study this problem with a game-based approach and establish the strictness of the hierarchy for the case of existential (i. e. ,□-free) formulae. It is known that these characterize precisely the L μ -definable properties that are closed under extensions. We also relate the strictness of the variable hierarchy to the question whether the finite variable fragments satisfy the existential preservation theorem.

LPAR Conference 2001 Conference Paper

Games and Model Checking for Guarded Logics

• Dietmar Berwanger
• Erich Grädel

Abstract We investigate the model checking problems for guarded first-order and fixed point logics byreducing them to paritygames. This approach is known to provide good results for the modal μ-calculus and is verycloselyrelated to automata-based methods. To obtain good results also for guarded logics, optimized constructions of games have to be provided. Further, we studythe structure of paritygames, isolate ‘easy’ cases that admit efficient algorithmic solutions, and determine their relationship to specific fragments of guarded fixed point logics.

CSL Conference 2001 Conference Paper

Inflationary Fixed Points in Modal Logic

• Anuj Dawar
• Erich Grädel
• Stephan Kreutzer

Abstract 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.

LPAR Conference 2000 Conference Paper

Efficient Evaluation Methods for Guarded Logics and Datalog LITE

• Erich Grädel

Abstract Guarded logics are fragments of first-order logic, fixed point logic or second-order logic in which all quantifiers are relativised by guard formulae in an appropriate way. Semantically, this means that such logics can simultaneously refer to a collection of elements only if all these elements are ‘close together’ (e. g. coexist in some atomic fact). Guarded logics are powerful generalizations of modal logics (such as propositional multi-modal logic or the modal μ-calculus) that retain and, to a certain extent, explain their good algorithmic and model-theoretic properties. In this talk, I will survey the recent research on guarded logics. I will also present a guarded variant of Datalog, called Datalog LITE, which is semantically equivalent to the alternation-free portion of guarded fixed point logic. The main focus of the talk will be on model checking (or equivalently, query evaluation) algorithms for guarded logics. While the complexity of evaluating arbitrary guarded fixed point formulae is closely related to the model checking problem for the modal μ-calculus (for which no polynomial-time algorithms are known up to now), there are interesting fragments that admit efficient, in fact linear time, evaluation algorithms. In particular this is the case for the guarded fragment of first-order logic and for Datalog LITE.

CSL Conference 1999 Conference Paper

Descriptive Complexity Theory for Constraint Databases

• Erich Grädel
• Stephan Kreutzer

Abstract We consider the data complexity of various logics on two important classes of constraint databases: dense order and linear constraint databases. For dense order databases, we present a general result allowing us to lift results on logics capturing complexity classes from the class of finite ordered databases to dense order constraint databases. Considering linear constraints, we show that there is a significant gap between the data complexity of first-order queries on linear constraint databases over the real and the natural numbers. This is done by proving that for arbitrary high levels of the Presburger arithmetic there are complete first-order queries on databases over (ℕ, <, +). The proof of the theorem demonstrates a simple argument for the translating complexity results for prefix classes in logical theories to results on the complexity of query evaluation in contraint boundary databases.

TCS Journal 1999 Journal Article

On logics with two variables

• Erich Grädel
• Martin Otto

This paper is a survey and systematic presentation of decidability and complexity issues for modal and non-modal two-variable logics. A classical result due to Mortimer says that the two-variable fragment of first-order logic, denoted FO2, has the finite model property and is therefore decidable for satisfiability. One of the reasons for the significance of this result is that many propositional modal logics can be embedded into FO2. Logics that are of interest for knowledge representation, for the specification and verification of concurrent systems and for other areas of computer science are often defined (or can be viewed) as extensions of modal logics by features like counting constructs, path quantifiers, transitive closure operators, least and greatest fixed points, etc. Examples of such logics are computation tree logic CTL, the modal μ-calculus L μ, or popular description logics used in artificial intelligence. Although the additional features are usually not first-order constructs, the resulting logics can still be seen as two-variable logics that are embedded in suitable extensions of FO2. Typically, the applications call for an analysis of the satisfiability and model checking problems of the logics employed. The decidability and complexity issues for modal and non-modal two-variables logics have been studied quite intensively in the last years. It has turned out that the satisfiability problems for two-variable logics with full first-order quantification are usually much harder (and indeed highly undecidable in many cases) than the satisfiability problems for corresponding modal logics. On the other side, the situation is different for model checking problems. The model checking problem of a modal logic has essentially the same complexity as the model checking problem of the corresponding two variable logic with full quantification.

I&C Journal 1998 Journal Article

Metafinite Model Theory

• Erich Grädel
• Yuri Gurevich

Motivated by computer science challenges, we suggest to extend the approach and methods of finite model theory beyond finite structures. We study definability issues and their relation to complexity onmetafinite structureswhich typically consist of (i) a primary part, which is a finite structure, (ii) a secondary part, which is a (usually infinite) structure that can be viewed as a structured domain of numerical objects, and (iii) a set of “weight” functions from the first part into the second. We discuss model-theoretic properties of metafinite structures, present results on descriptive complexity, and sketch some potential applications.

STOC Conference 1995 Conference Paper

Descriptive complexity theory over the real numbers

• Erich Grädel
• Klaus Meer

CSL Conference 1994 Conference Paper

Approximable Minimization Problems and Optimal Solutions on Random Inputs

• Erich Grädel
• Anders Malmström

Abstract In this paper we extend recent work about logical criteria for approximation properties of optimization problems. We focus on the relationship between logical expressibility and expected asymptotic growth of optimal solutions on random inputs. This further develops a probabilistic approach due to Behrendt, Compton and Grädel showing that expected optimal solutions for any problem in the class Max ⌆ 1 grows essentially like a polynomial. We show that there is a similar result for Min F + II 1, a syntactic class of minimization problems which provides a logical criterion for approximability. As a consequence, we show that some important problems do not belong to Min F + II 1.

CSL Conference 1993 Conference Paper

Inductive Definability with Counting on Finite Structures

• Erich Grädel
• Martin Otto 0001

CSL Conference 1993 Conference Paper

Optimization Problems: Expressibility, Approximation Properties and Expected Asymptotic Growth of Optimal Solutions

• Thomas Behrendt
• Kevin J. Compton
• Erich Grädel

TCS Journal 1992 Journal Article

Capturing complexity classes by fragments of second-order logic

• Erich Grädel

We investigate the expressive power of certain fragments of second-order logic on finite structures. The fragments are second-order Horn logic, second-order Krom logic as well as a symmetric and a deterministic version of the latter. It is shown that all these logics collapse to their existential fragments. In the presence of successor relation they provide characterizations of polynomial time, deterministic and nondeterministic logspace and of the complement of symmetric logspace. Without successor relation these logics still can express certain problems that are complete in the corresponding complexity classes, but on the other hand they are strictly weaker than previously known logics for these classes and fail to express some very simple properties.

FOCS Conference 1992 Conference Paper

Hierarchies in Transitive Closure Logic, Stratified Datalog and Infinitary Logic

• Erich Grädel
• Gregory L. McColm

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. >

CSL Conference 1992 Conference Paper

On Transitive Closure Logic

• Erich Grädel

Abstract We present Ehrenfeucht-Fraïssé games for transitive closure logic (FO + TC) and for quantifier classes in (FO + TC). With this method we investigate the fine structure of positive transitive closure logic (FO + pos TC), and identify an infinite quantifier hierarchy inside (FO + pos TC), formed by interleaving universal quantifiers and TC-operators. It is also shown that transitive closure logic (and its fragments) have the same expressive power as the linear programs in certain extensions of Datalog.

I&C Journal 1991 Journal Article

Simple sentences that are hard to decide

• Erich Grädel

It was considered to be “typical for first order theories” that a restriction to sentences with only a limited number of quantifier alternations leads to an exponential decrease of complexity. Using domino games, which were treated in a previous paper to describe computations of alternating Turing machines, we prove that this is not always true. We present a list of theories, all of them decidable in ⌣ c>0 ATIME(2cn, n), for which the subclasses with bounded quantifier alternations still have alternating exponential time complexity. In particular this yields non-deterministic exponential time lower bounds for very simple prefix classes (with 2 or 3 alternations). Theories with such behaviour are the theory of Boolean algebras, the theory of polynomial rings over finite fields, the theory of idempotent rings, the theory of finite sets with inclusion, the theory of semilattices, the theory of Stone algebras, the theory of distributive p-algebras in the Lee-class B n, and the theories of natural numbers with divisibility or coprimeness.

CSL Conference 1990 Conference Paper

On Logical Descriptions of Some Concepts in Structural Complexity Theory

• Erich Grädel

Abstract A logical framework is introduced which captures the behaviour of oracle machines and gives logical descriptions of complexity classes that are defined by oracle machines. Using this technique the notion of first-order selfreducibility is investigated and applied to obtain a structural result about non-uniform complexity classes below P.

CSL Conference 1989 Conference Paper

Size of Models versus Length of Computations: On Inseparability by Nondeterministic Time Complexity Classes

• Erich Grädel

Abstract Starting from the classification of prefix vocabulary classes in first order logic (with functions) with respect to decidability/undecidability and from Trakhtenbrots Inseparability Theorem we prove NTIME-lower bounds for every set that separates (in a certain class) the formulas with a model of bounded size (depending on the length of the formula) from the invalid formulas. The results are optimal when the lower time bound is the the same function that bounds the size of the models. We prove that his can be reached for most undecidable prefix vocabulary classes. However, for some formula classes the size of the models is larger than the length of the computations that they can describe. For these classes the inseparability results are weaker. The proofs use reductions from bounded domino problems and interpretations among different formula classes. In the last section we use such a result to prove a nondeterministic exponential time lower bound for a simple prefix class in Presburger arithmetic.

TCS Journal 1988 Journal Article

Subclasses of presburger arithmetic and the polynomial-time hierarchy

• Erich Grädel

We investigate the complexity of subclasses of Presburger arithmetic, i. e. , the first-order theory of natural numbers with addition. The subclasses are defined by restricting the quantifier prefix to finite lists Q 1…Qs. For allm⩾ 2 we find formula classes, defined by prefixes with m+1 alternations and m+5 quantifiers, which are Σ p m - respectively Π p m -complete. For m=1, the class of ∃∀∀-formulas is shown to be NP-complete. For m=0 and for all natural numbers t, the class of ∃ t -formulas is known to be in P. Thus we have a nice characterisation of the polynomial-time hierarchy by classes of Presburger formulas. Finally, the NP-completeness of the ∃∀∀-class is used to prove that for certain formulas there exist no equivalent quantifier-free formulas of polynomial length.