Publikationen

Noch nicht erschienen

A. Dawar and E. Grädel. The Descriptive Complexity of Parity Games. In Proceedings of the 17th Annual Conference on Computer Science Logic, CSL 2008. To appear.

Abstract BibTeX

We study the logical definablity of the winning regions of parity games. For games with a bounded number of priorities, it is wellknown that the winning regions are definable in the modal mu-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.

@inproceedings{DG08,
     author = {Anuj Dawar and Erich Grädel},
     title = {The Descriptive Complexity of Parity Games},
     booktitle = {Proceedings of the 17th Annual Conference on Computer Science Logic, CSL 2008},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/csl08.pdf},
     optyear = {2008},
     note = {to appear},
}
E. Grädel and M. Ummels. Solution Concepts and Algorithms for Infinite Multiplayer Games. In New Perspectives on Games and Interaction (K. Apt and R. van Rooij, Eds.), vol. 5 of Texts in Logic and Games. Amsterdam University Press. To appear.

Abstract BibTeX

We survey and discuss several solution concepts for infinite turn-based multiplayer games with qualitative (i.e. win-lose) objectives of the players. These games generalise in a natural way the common model of games in verification which are two-player, zero-sum games with $\omega$-regular winning conditions. The generalisation is in two directions: our games may have more than two players, and the objectives of the players need not be completely antagonistic. The notion of a Nash equilibrium is the classical solution concept in game theory. However, for games that extend over time, in particular for games of infinite duration, Nash equilibria are not always satisfactory as a notion of rational behaviour. We therefore discuss variants of Nash equilibria such as subgame perfect equilibria and secure equilibria. We present criteria for the existence of Nash equilibria and subgame perfect equilibria in the case of arbitrary many players and for the existence of secure equilibria in the two-player case. In the second part of this paper, we turn to algorithmic questions: For each of the solution concepts that we discuss, we present algorithms that decide the existence of a solution with certain requirements in a game with parity winning conditions. Since arbitrary $\omega$-regular winning conditions can be reduced to parity conditions, our algorithms are also applicable to games with arbitrary $\omega$-regular winning conditions.

@inproceedings{GU08,
     author = {Erich Grädel and Michael Ummels},
     title = {Solution Concepts and Algorithms for Infinite Multiplayer Games},
     booktitle = {New Perspectives on Games and Interaction},
     editor = {Krzysztof Apt and Robert van Rooij},
     series = {Texts in Logic and Games},
     volume = {5},
     publisher = {Amsterdam University Press},
     url = {http://www.logic.rwth-aachen.de/~ummels/knaw07.pdf},
     note = {To appear},
}

2008

V. Bárány. A Hierarchy of Automatic $\omega$-Words having a Decidable MSO Theory. RAIRO - Theor. Inf. Appl., vol. 42, pp. 417-450, 2008.

Abstract BibTeX

We investigate automatic presentations of omega-words. Starting points of our study are the works of Rigo and Maes, Caucal, and Carton and Thomas concerning lexicographic presentation, MSO-interpretability in algebraic trees, and the decidability of the MSO theory of morphic words. Refining their techniques we observe that the lexicographic presentation of a (morphic) word is in a certain sense canonical. We then generalize our techniques to a hierarchy of classes of omega-words enjoying the above mentioned definability and decidability properties. We introduce k-lexicographic presentations, and morphisms of level k stacks and show that these are inter-translatable, thus giving rise to the same classes of k-lexicographic or level k morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every k-lexicographic word as well as closure of these classes under MSO-definable recolorings, e.g. closure under deterministic sequential mappings. The classes of k-lexicographic words are shown to constitute an infinite hierarchy.

@article{Bar08ITA,
     author = {Vince Bárány},
     title = {A Hierarchy of Automatic $\omega$-Words having a Decidable MSO Theory},
     journal = {RAIRO - Theor. Inf. Appl.},
     volume = {42},
     pages = {417-450},
     year = {2008},
     doi = {10.1051/ita:2008008},
     url = {http://www.logic.rwth-aachen.de/~vbarany/hom_ITA.pdf},
}
D. Fischer, E. Grädel, and Ł. Kaiser. Model Checking Games for the Quantitative $\mu$-Calculus. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 301–312, 2008.

Abstract BibTeX

We investigate quantitative extensions of modal logic and the modal $\mu$-calculus, and study the question whether the tight connection between logic and games can be lifted from the qualitative logics to their quantitative counterparts. It turns out that, if the quantitative $\mu$-calculus is defined in an appropriate way respecting the duality properties between the logical operators, then its model checking problem can indeed be characterised by a quantitative variant of parity games. However, these quantitative games have quite different properties than their classical counterparts, in particular they are, in general, not positionally determined. The correspondence between the logic and the games goes both ways: the value of a formula on a quantitative transition system coincides with the value of the associated quantitative game, and conversely, the values of quantitative parity games are definable in the quantitative $\mu$-calculus.

@inproceedings{FGK08,
     author = {Diana Fischer and Erich Grädel and Łukasz Kaiser},
     title = {Model Checking Games for the Quantitative $\mu$-Calculus},
     booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
     editor = {Susanne Albers and Pascal Weil},
     url = {http://www.logic.rwth-aachen.de/~kaiser/quantitative_games.pdf},
     pages = {301–312},
     year = {2008},
}
T. Ganzow and S. Rubin. Order-Invariant MSO is Stronger than Counting MSO in the Finite. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 313–324, 2008.

BibTeX

@inproceedings{GR08,
     author = {Tobias Ganzow and Sasha Rubin},
     title = {Order-Invariant MSO is Stronger than Counting MSO in the Finite},
     booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
     editor = {Susanne Albers and Pascal Weil},
     pages = {313–324},
     year = {2008},
}
Ł. Kaiser, S. Rubin, and V. Bárány. Cardinality and counting quantifiers on omega-automatic structures. In Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008 (S. Albers and P. Weil, Eds.), pp. 385–396, 2008.

Abstract BibTeX

We investigate structures that can be represented by omega-automata, so called omega-automatic structures, and prove that relations defined over such structures in first-order logic expanded by the first-order quantifiers `there exist at most $\aleph_0$ many', 'there exist finitely many' and 'there exist $k$ modulo $m$ many' are omega-regular. The proof identifies certain algebraic properties of omega-semigroups. As a consequence an omega-regular equivalence relation of countable index has an omega-regular set of representatives. This implies Blumensath's conjecture that a countable structure with an $\omega$-automatic presentation can be represented using automata on finite words. This also complements a very recent result of Hjörth, Khoussainov, Montalban and Nies showing that there is an omega-automatic structure which has no injective presentation.

@inproceedings{BKR08,
     author = {Łukasz Kaiser and Sasha Rubin and Vince Bárány},
     title = {Cardinality and counting quantifiers on omega-automatic structures},
     booktitle = {Proceedings of the 25th International Symposium on Theoretical Aspects of Computer Science, STACS 2008},
     editor = {Susanne Albers and Pascal Weil},
     url = {http://www.logic.rwth-aachen.de/~kaiser/cardinality_automatic.pdf},
     pages = {385–396},
     year = {2008},
}
M. Ummels. The Complexity of Nash Equilibria in Infinite Multiplayer Games. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2008 (R. Amadio, Ed.), vol. 4962 of LNCS, pp. 20–34. Springer-Verlag, 2008.

Abstract BibTeX

We study the complexity of Nash equilibria in infinite (turn-based, qualitative) multiplayer games. Chatterjee et al. showed the existence of a Nash equilibrium in any such game with $\omega$-regular winning conditions, and they devised an algorithm for computing one. We argue that in applications it is often insufficient to compute just some Nash equilibrium. Instead, we enrich the problem by allowing to put (qualitative) constraints on the payoff of the desired equilibrium. Our main result is that the resulting decision problem is NP-complete for games with co-Büchi, parity or Streett winning conditions but fixed-parameter tractable for many natural restricted classes of games with parity winning conditions. For games with Büchi winning conditions we show that the problem is, in fact, decidable in polynomial time. We also analyse the complexity of strategies realising a Nash equilibrium. In particular, we show that pure finite-state strategies as opposed to arbitrary mixed strategies suffice to realise any Nash equilibrium of a game with $\omega$-regular winning conditions with a qualitative constraint on the payoff.

@inproceedings{Ummels08,
     author = {Michael Ummels},
     title = {The Complexity of Nash Equilibria in Infinite Multiplayer Games},
     booktitle = {Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2008},
     editor = {Roberto Amadio},
     publisher = {Springer-Verlag},
     series = {LNCS},
     volume = {4962},
     pages = {20–34},
     year = {2008},
     url = {http://www.logic.rwth-aachen.de/~ummels/fossacs08.pdf},
}

2007

D. Berwanger, E. Grädel, and G. Lenzi. The variable hierarchy of the $\mu$-calculus is strict. Theory of Computing Systems, vol. 40, pp. 437–466, 2007.

Abstract BibTeX

Most of the logics commonly used in verification, such as LTL, CTL, CTL*, and PDL can be embedded into the two-variable fragment of the mu-calculus. It is also known that properties occurring at arbitrarily high levels of the alternation hierarchy can be formalised using only two variables. This raises the question whether the number of fixedpoint variables in mu-formulae can be bounded in general.

We answer this question negatively, and prove that the variable-hierarchy of the mu-calculus is semantically strict. For any k, we provide examples of formulae with k variables that are not equivalent to any formula with fewer variables. In particular, this implies that Parikh's Game Logic is less expressive than the mu-calculus, thus resolving an open issue raised by Parikh in 1983.

@article{BGL07,
     author = {Dietmar Berwanger and Erich Grädel and Giacomo Lenzi},
     title = {The variable hierarchy of the $\mu$-calculus is strict},
     journal = {Theory of Computing Systems},
     volume = {40},
     pages = {437–466},
     year = {2007},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGrLe-tocs07.pdf},
}
D. Berwanger. Admissibility in infinite games. In Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2007 (W. Thomas and P. Weil, Eds.), vol. 4393 of LNCS, pp. 188–199. Springer-Verlag, 2007.

BibTeX

@inproceedings{Berwanger07,
     author = {Dietmar Berwanger},
     title = {Admissibility in infinite games},
     booktitle = {Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2007},
     editor = {Wolfgang Thomas and Pascal Weil},
     publisher = {Springer-Verlag},
     series = {LNCS},
     volume = {4393},
     pages = {188–199},
     year = {2007},
     url = {http://www.logic.rwth-aachen.de/~dwb/admissibility.pdf},
}
V. Bárány. Automatic Presentations of Infinite Structures. PhD thesis, RWTH Aachen, 2007.

BibTeX

@phdthesis{Bar07diss,
     author = {V. Bárány},
     title = {Automatic Presentations of Infinite Structures},
     school = {RWTH Aachen},
     type = {Dissertation},
     year = {2007},
     url = {http://www.logic.rwth-aachen.de/~vbarany/diss.pdf},
}
J. Flum, E. Grädel, and T. Wilke (Eds.). Logic and Automata: History and Perspectives. Amsterdam University Press, 2007.

BibTeX

@book{FlumGraWil07,
     editor = {J. Flum and E. Grädel and T. Wilke},
     title = {Logic and Automata: History and Perspectives},
     publisher = {Amsterdam University Press},
     year = {2007},
     series = {Texts in Logic and Games},
     volume = {2},
     url = {http://www.logic.rwth-aachen.de/Books/},
}
E. Grädel. Finite Model Theory and Descriptive Complexity. In Finite Model Theory and Its Applications, pp. 125–230. Springer-Verlag, 2007.

BibTeX

@incollection{Graedel03,
     author = {E. Grädel},
     title = {Finite Model Theory and Descriptive Complexity},
     booktitle = {Finite Model Theory and Its Applications},
     publisher = {Springer-Verlag},
     year = {2007},
     pages = {125–230},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/FMTbook-Chapter3.pdf},
}
E. Grädel and Ł. Kaiser. What kind of memory is needed to win infinitary Muller games? In Interactive Logic (J. van Benthem, B. Löwe, and D. Gabbay, Eds.), vol. 1 of Texts in Logic and Games. Amsterdam University Press, 2007.

Abstract BibTeX

In an influential paper entitled ``How much memory is needed to win infinite games'', Dziembowski, Jurdziński, and Walukiewicz have shown that there are Muller games of size $O(n)$ whose winning strategies require memory of size at least $n!$. This shows that the LAR-memory, based on the latest appearance records introduced by Gurevich and Harrington, is optimal for solving Muller games. We review these results and reexamine the situation for the case of infinitary Muller games, i.e. Muller games with infinitely many priorities. We introduce a new, infinite, memory structure, based on finite appearance records (FAR) and investigate classes of Muller games that can be solved with FAR-memory.

@inproceedings{GK07,
     author = {Erich Grädel and Łukasz Kaiser},
     title = {What kind of memory is needed to win infinitary Muller games?},
     editor = {Johan van Benthem and Benedikt Löwe and Dov Gabbay},
     booktitle = {Interactive Logic},
     series = {Texts in Logic and Games},
     volume = {1},
     publisher = {Amsterdam University Press},
     year = {2007},
     url = {http://www.logic.rwth-aachen.de/pub/kaiser/memory_kinds.pdf},
}
E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S.Weinstein. Finite Model Theory and Its Applications. Springer-Verlag, 2007.

BibTeX

@book{FMT07,
     author = {E. Grädel and Ph. G. Kolaitis and L. Libkin and M. Marx and J. Spencer and M. Y. Vardi and Y. Venema and S.Weinstein},
     title = {Finite Model Theory and Its Applications},
     publisher = {Springer-Verlag},
     year = {2007},
     series = {Texts in Theoretical Computer Science},
     url = {http://www.logic.rwth-aachen.de/Books/},
}

2006

D. Berwanger, A. Dawar, P. Hunter, and S. Kreutzer. DAG-width and parity games. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006, vol. 3884 of LNCS, pp. 524–536. Springer-Verlag, 2006.

BibTeX

@inproceedings{BDHK06,
     author = {Dietmar Berwanger and Anuj Dawar and Paul Hunter and Stephan Kreutzer},
     title = {DAG-width and parity games},
     booktitle = {Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science, STACS 2006},
     publisher = {Springer-Verlag},
     series = {LNCS},
     volume = {3884},
     year = {2006},
     pages = {524–536},
     url = {http://www.logic.rwth-aachen.de/~dwb/pub/dagwidth.pdf},
}
D. Berwanger and D. Janin. Automata on Directed Graphs: Vertex versus Edge Marking. In Proceedings of the 3rd International Conference on Graph Transformation, ICGT 2006, vol. 4179 of LNCS, pp. 46–60. Springer-Verlag, 2006.

BibTeX

@inproceedings{BerwangerJan06,
     author = {Dietmar Berwanger and David Janin},
     title = {Automata on Directed Graphs: Vertex versus Edge Marking},
     booktitle = {Proceedings of the 3rd International Conference on Graph Transformation, ICGT 2006},
     url = {http://www.logic.rwth-aachen.de/~dwb/pub/acc.pdf},
     publisher = {Springer-Verlag},
     series = {LNCS},
     volume = {4179},
     pages = {46–60},
     year = {2006},
}
V. Bárány. A Hierarchy of Automatic Words having a Decidable MSO Theory. In Online Proceedings of the 11th Journées Montoises, Rennes (D. Caucal, Ed.), 2006.

Abstract BibTeX

We investigate automatic presentations of infinite words. Starting points of our study are the works of Rigo and Maes, and Carton and Thomas concerning the lexicographic presentation, respectively the decidability of the MSO theory of morphic words. Refining their techniques we observe that the lexicographic presentation of a (morphic) word is canonical in a certain sense. We then go on to generalize our techniques to a hierarchy of classes of infinite words enjoying the above mentioned properties. We introduce $k$-lexicographic presentations, and morphisms of level $k$ stacks and show that these are inter-translatable, thus giving rise to the same classes of $k$-lexicographic or level $k$ morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every $k$-lexicographic word as well as closure of these classes under restricted MSO interpretations, e.g. closure under deterministic sequential mappings. The classes of $k$-lexicographic words are shown to form an infinite hierarchy.

@inproceedings{Bar06JM,
     author = {Vince Bárány},
     title = {A Hierarchy of Automatic Words having a Decidable MSO Theory},
     year = {2006},
     booktitle = {Online Proceedings of the 11th Journées Montoises, Rennes},
     editor = {D. Caucal},
     url = {http://www.logic.rwth-aachen.de/~vbarany/jm06.pdf},
}
V. Bárány, C. Löding, and O. Serre. Regularity Problems for Visibly Pushdown Languages. In Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006 (B. Durand and W. Thomas, Eds.), vol. 3884 of LNCS, pp. 420–431. Springer, 2006.

Abstract BibTeX

Visibly pushdown automata are special pushdown automata whose stack behavior is driven by the input symbols according to a partition of the alphabet. We show that it is decidable for a given visibly pushdown automaton whether it is equivalent to a visibly counter automaton, i.e. an automaton that uses its stack only as counter. In particular, this allows to decide whether a given visibly pushdown language is a regular restriction of the set of well-matched words, meaning that the language can be accepted by a finite automaton if only well-matched words are considered as input.

@inproceedings{BLS06STACS,
     author = {Vince Bárány and Christof Löding and Olivier Serre},
     title = {Regularity Problems for Visibly Pushdown Languages},
     year = {2006},
     booktitle = {Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006},
     editor = {B. Durand and W. Thomas},
     series = {LNCS},
     volume = {3884},
     pages = {420–431},
     publisher = {Springer},
     url = {http://www.logic.rwth-aachen.de/~vbarany/BLS_stacs06_withAppendix.pdf},
}
V. Bárány. Invariants of Automatic Presentations and Semi-Synchronous Transductions. In Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006 (B. Durand and W. Thomas, Eds.), vol. 3884 of LNCS, pp. 289–300. Springer, 2006.

Abstract BibTeX

Automatic structures are countable structures finitely presentable by a collection of automata. We study questions related to properties invariant with respect to the choice of an automatic presentation. We give a negative answer to a question of Rubin concerning definability of intrinsically regular relations by showing that order-invariant first-order logic can be stronger than first-order logic with counting on automatic structures. We introduce a notion of equivalence of automatic presentations, define semi-synchronous transductions, and show how these concepts correspond. Our main result is that a one-to-one function on words preserves regularity as well as non-regularity of all relations iff it is a semi-synchronous transduction. We also characterize automatic presentations of the complete structures of Blumensath and Grädel.

@inproceedings{Bar06STACS,
     author = {Vince Bárány},
     title = {Invariants of Automatic Presentations and Semi-Synchronous Transductions},
     year = {2006},
     booktitle = {Proceedings of the 23rd Annual Symposioum on Theoretical Aspects of Computer Science, STACS 2006},
     editor = {B. Durand and W. Thomas},
     series = {LNCS},
     volume = {3884},
     pages = {289–300},
     publisher = {Springer},
     url = {http://www.logic.rwth-aachen.de/~vbarany/stacs06_88_appendix.pdf},
}
A. Dawar, E. Grädel, and S. Kreutzer. Backtracking Games and Inflationary Fixed Points. Theoretical Computer Science, vol. 350, pp. 174–187, 2006.

Abstract BibTeX

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 $\phi$ and structures $A$ into simple games such that $A |= \phi$ 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.

@article{DGK06,
     author = {Anuj Dawar and Erich Grädel and Stephan Kreutzer},
     title = {Backtracking Games and Inflationary Fixed Points},
     journal = {Theoretical Computer Science},
     year = {2006},
     volume = {350},
     pages = {174–187},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/DaGrKr-tcs05.ps},
}
E. Grädel and I. Walukiewicz. Positional Determinacy of Games with Infinitely Many Priorities. Logical Methods in Computer Science, 2006.

Abstract BibTeX

We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy.

The theory of such games is well studied for winning conditions that are defined in terms of a mapping that assigns to each position a priority from a finite set C. Specifically, in Muller games the winner of a play is determined by the set of those priorities that have been seen infinitely often; an important special case are parity games where the least (or greatest) priority occurring infinitely often determines the winner. It is well-known that parity games are positionally determined whereas Muller games are determined via finite-memory strategies.

In this paper, we extend this theory to the case of games with infinitely many priorities. Such games arise in several application areas, for instance in pushdown games with winning conditions depending on stack contents.

For parity games there are several generalisations to the case of infinitely many priorities. While max-parity games over $\omega$ or min-parity games over larger ordinals than $\omega$ require strategies with infinite memory, we can prove that min-parity games with priorities in $\omega$ are positionally determined. Indeed, it turns out that the min-parity condition over $\omega$ is the only infinitary Muller condition that guarantees positional determinacy on all game graphs.

@article{GraedelWal06,
     author = {E. Grädel and I. Walukiewicz},
     title = {Positional Determinacy of Games with Infinitely Many Priorities},
     journal = {Logical Methods in Computer Science},
     year = {2006},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/GrWa-lmcs06.pdf},
}
Ł. Kaiser. Game Quantification on Automatic Structures and Hierarchical Model Checking Games. In Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006 (Z. Esik, Ed.), vol. 4207 of LNCS, pp. 411–425. Springer-Verlag, 2006.

Abstract BibTeX

Game quantification is an expressive concept and has been studied in model theory and descriptive set theory, especially in relation to infinitary logics. Automatic structures on the other hand appear very often in computer science, especially in program verification. We extend first-order logic on structures on words by allowing to use an infinite string of alternating quantifiers on letters of a word, the game quantifier. This extended logic is decidable and preserves regularity on automatic structures, but can be undecidable on other structures even with decidable first-order theory. We show that in the presence of game quantifier any relation that allows to distinguish successors is enough to define all regular relations and therefore the game quantifier is strictly more expressive than first-order logic in such cases. Conversely, if there is an automorphism of atomic relations that swaps some successors then we prove that it can be extended to any relations definable with game quantifier. After investigating it's expressiveness, we use game quantification to introduce a new type of combinatorial games with multiple players and imperfect information exchanged with respect to a hierarchical constraint. It is shown that these games on finite arenas exactly capture the logic with game quantifier when players alternate their moves but are undecidable and not necessarily determined in the other case. In this way we define the first model checking games with finite arenas that can be used for model checking first-order logic on automatic structures.

@inproceedings{K06,
     author = {Łukasz Kaiser},
     title = {Game Quantification on Automatic Structures and Hierarchical Model Checking Games},
     booktitle = {Proceedings of the 15th Annual Conference on Computer Science Logic, CSL 2006},
     publisher = {Springer-Verlag},
     series = {LNCS},
     editor = {Zoltan Esik},
     volume = {4207},
     pages = {411–425},
     year = {2006},
     url = {http://www.logic.rwth-aachen.de/pub/kaiser/game_quantifier_logic.pdf},
}
M. Ummels. Rational Behaviour and Strategy Construction in Infinite Multiplayer Games. In Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006 (S. Arun-Kumar and N. Garg, Eds.), vol. 4337 of LNCS, pp. 212–223. Springer-Verlag, 2006.

Abstract BibTeX

We study infinite games played by arbitrarily many players on a directed graph. Equilibrium states capture rational behaviour in these games. Instead of the well-known notion of a Nash equilibrium, we focus on the notion of a subgame perfect equilibrium. We argue that the latter one is more appropriate for the kind of games we study, and we show the existence of a subgame perfect equilibrium in any infinite game with $\omega$-regular winning conditions. As, in general, equilibria are not unique, it is appealing to compute one with a maximal payoff. This problem corresponds naturally to the problem of deciding given a game and two payoff vectors whether the game has an equilibrium with a payoff in between the given thresholds. We show that this problem is decidable for games with $\omega$-regular winning conditions played on a finite graph and analyse its complexity. Moreover, we establish that any subgame perfect equilibrium of a game with $\omega$-regular winning conditions played on a finite graph can be implemented by finite-state strategies. Finally, we consider logical definability. We state that if we fix the number of players together with an $\omega$-regular winning condition for each of them and two payoff vectors the property that a game has a subgame perfect equilibrium with a payoff in between the given thresholds is definable in the modal $\mu$-calculus.

@inproceedings{Ummels06,
     author = {Michael Ummels},
     title = {Rational Behaviour and Strategy Construction in Infinite Multiplayer Games},
     year = {2006},
     booktitle = {Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006},
     publisher = {Springer-Verlag},
     editor = {S. Arun-Kumar and Naveen Garg},
     series = {LNCS},
     volume = {4337},
     pages = {212–223},
     url = {http://www.logic.rwth-aachen.de/~ummels/fsttcs06.pdf},
}

2005

D. Berwanger. Games and Logical Expressiveness. PhD thesis, RWTH Aachen, 2005.

Abstract BibTeX

We investigat the inner structure of process logics, in particular of the mu-calculus $L_\mu$, from the viewpoint of games over graphs. First, we show that Parikh's Game Logic, a two-variable sublogic of the mu-calculus, is expressive enough to capture parity games and, hence, to reach arbitrarily high levels of the $L_\mu$ alternation hierarchy. Further, we devise a game that captures relevant issues of descriptive and computational complexity of the mu-calculus. As a first application, we show that, for the model-checking problem of $L_\mu$, our game naturally leads to instances that can be solved in polynomial time. On the basis of this game, we also derive a parameter that captures the number of variables required to specify the behaviour of a given transition system in the mu-calculus. As a consequence, it follows that the expressive power of the mu-calculus strictly increases with the number of variables used in formulae. Already a particular case of this result, that three variables can express more than two, allows us to separate the expressive power of Parikh's Game Logic and the mu-calculus, a question that was open since 1983.

@phdthesis{BerwangerThesis,
     author = {Dietmar Berwanger},
     title = {Games and Logical Expressiveness},
     school = {RWTH Aachen},
     year = {2005},
     task = {2,7},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/express.pdf},
}
D. Berwanger and E. Grädel. Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. In Proceedings of LPAR 2004, Montevideo, Uruguay, vol. 3452 of LNCS, pp. 209–223. Springer-Verlag, 2005.

Abstract BibTeX

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

As we will show, entanglement is intimately related to the descriptive complexity of the modal $\mu$-calculus. Particular, if we view the syntax of a formula as a tree with back edges leading from fixed-point variables to their definition, the block width of this syntax graph is bounded by the number of distinct variables used in the formula. On the one hand, the entanglement of a finite transition system provides an upper bound for the number of fixed point variables needed to describe it up to bisimulation.

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 subgames induced by winning strategies.

@inproceedings{BerwangerGraLPAR04,
     author = {Dietmar Berwanger and Erich Grädel},
     title = {Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games},
     pages = {209–223},
     booktitle = {Proceedings of LPAR 2004, Montevideo, Uruguay},
     publisher = {Springer-Verlag},
     series = {LNCS},
     volume = {3452},
     year = {2005},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/BG_lpar04.pdf},
     task = {2},
}
D. Berwanger and G. Lenzi. The variable hierarchy of the $\mu$-calculus is strict. In STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science, vol. 3404 of LNCS, pp. 97–109. Springer-Verlag, 2005.

Abstract BibTeX

The modal $\mu$-calculus $\Lmu$ attains high expressive power by extending basic modal logic with monadic variables and binding them to extremal fixed points of definable operators. The number of variables occurring in a formula provides a relevant measure of its conceptual complexity. In a previous paper with Erich Grädel we have shown, for the existential fragment of $\Lmu$, that this conceptual complexity is also reflected in an increase of semantic complexity, by providing examples of existential formulae with $k$ variables that are not equivalent to any existential formula with fewer than $k$ variables.

In this paper, we prove an existential preservation theorem for the family of $\Lmu$-formulae over at most $k$ variables that define simulation closures of finite strongly connected structures. Since hard formulae for the level $k$ of the existential hierarchy belong to this family, it follows that the bounded variable fragments of the full modal $\mu$-calculus form a hierarchy of strictly increasing expressive power.

@inproceedings{BerwangerLen05,
     author = {Dietmar Berwanger and Giacomo Lenzi},
     title = {The variable hierarchy of the $\mu$-calculus is strict},
     booktitle = {STACS 2005, Proceedings of the 22nd Symposium on Theoretical Aspects of Computer Science},
     publisher = {Springer-Verlag},
     series = {LNCS},
     volume = {3404},
     year = {2005},
     pages = {97–109},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/hierarchy.ps},
     task = {7},
}
Ł. Kaiser. Confluence of Right Ground Term Rewriting Systems is Decidable. In FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (V. Sassone, Ed.), vol. 3441 of LNCS. Springer-Verlag, 2005.

Abstract BibTeX

Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper we prove that confluence of a fairly large class of systems, namely right ground term rewriting systems, is decidable. We introduce a labelling of variables with colours and constrain substitutions according to these colours. We show how right ground rewriting systems can be reduced to simple systems with coloured variables. Such systems can be analysed using reduction-automata techniques which leads to an interesting decision procedure for confluence.

@inproceedings{KaiserFossacs05,
     author = {Łukasz Kaiser},
     title = {Confluence of Right Ground Term Rewriting Systems is Decidable},
     booktitle = {FOSSACS 2005, Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures},
     publisher = {Springer-Verlag},
     series = {LNCS},
     editor = {Vladimiro Sassone},
     volume = {3441},
     year = {2005},
     url = {http://www.logic.rwth-aachen.de/pub/kaiser/rgtrs.pdf},
}
M. Ummels. Rational Behaviour and Strategy Construction in Infinite Multiplayer Games. Diploma thesis, RWTH Aachen, 2005.

BibTeX

@misc{Ummels05,
     author = {Michael Ummels},
     title = {Rational Behaviour and Strategy Construction in Infinite Multiplayer Games},
     howpublished = {Diploma thesis, RWTH Aachen},
     year = {2005},
     url = {http://www.logic.rwth-aachen.de/~ummels/diplom.pdf},
}

2004

D. Berwanger and E. Grädel. Fixed-Point Logics and Solitaire Games. Theory of Computing Systems, vol. 37, pp. 675–694, 2004.

Abstract BibTeX

The model checking games associated with fixed-point logics are parity games, and it is currently not known whether the strategy problem for parity games can be solved in polynomial time. We study $\SolLFP$, a fragment of least fixed-point logic, whose evaluation games are nested soltaire games. This means that on each strongly connected component of the game, only one player can make non-trivial moves. Winning sets of nested solitaire games can be computed efficiently.

The model checking problem for $\SolLFP$ is \sc Pspace-complete in general and \sc Ptime-complete for formulae of bounded width. On finite structures (but not on infinite ones), $\SolLFP$ is equivalent to transitive closure logic.

We also consider the solitaire fragment of guarded fixed-point logics. Due to the restricted quantification pattern of these logics, the associated games are small and therefore admit more efficient model checking algorithms.

@article{BerwangerGra04,
     author = {Dietmar Berwanger and Erich Grädel},
     title = {Fixed-Point Logics and Solitaire Games},
     journal = {Theory of Computing Systems},
     publisher = {Springer-Verlag},
     year = {2004},
     volume = {37},
     pages = {675–694},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/BeGr_tocs.pdf},
     task = {2,7},
}
A. Blumensath and E. Grädel. Finite Presentations of Infinite Structures: Automata and Interpretations. Theory of Computing Systems, vol. 37, pp. 641 – 674, 2004.

BibTeX

@article{BlumensathGra04,
     author = {Achim Blumensath and Erich Grädel},
     title = {Finite Presentations of Infinite Structures: Automata and Interpretations},
     journal = {Theory of Computing Systems},
     publisher = {Springer-Verlag},
     year = {2004},
     volume = {37},
     pages = {641 – 674},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/BlGr_tocs.pdf},
}
A. Dawar, E. Grädel, and S. Kreutzer. Inflationary fixed points in modal logic. ACM Transations on Computational Logic, vol. 5, pp. 282 – 315, 2004.

BibTeX

@article{DawarGraKre02,
     author = {Anuj Dawar and Erich Grädel and Stephan Kreutzer},
     title = {Inflationary fixed points in modal logic},
     journal = {ACM Transations on Computational Logic},
     volume = {5},
     year = {2004},
     pages = {282 – 315},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/DGK-tocl.ps},
}
A. Dawar, S. Kreutzer, and E. Grädel. Backtracking Games and Inflationary Fixed Points. In Proc. 31st International Colloquium on Automata, Languages and Programming – ICALP'04. Springer-Verlag, 2004.

BibTeX

@inproceedings{DawarKreGra04,
     author = {Anuj Dawar and Stephan Kreutzer and Erich Grädel},
     title = {Backtracking Games and Inflationary Fixed Points},
     booktitle = {Proc. 31st International Colloquium on Automata, Languages and Programming – ICALP'04},
     publisher = {Springer-Verlag},
     year = {2004},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/DaGrKr-icalp04.ps},
}
E. Grädel. Positional Determinacy of Infinite Games. In Proceedings of STACS 2004: 21st Annual Symposium on Theoretical Aspects of Computer Science, vol. 2996 of LNCS, pp. 2 – 18. Springer-Verlag, 2004.

BibTeX

@inproceedings{Graedel04,
     author = {Erich Grädel},
     title = {Positional Determinacy of Infinite Games},
     booktitle = {Proceedings of STACS 2004: 21st Annual Symposium on Theoretical Aspects of Computer Science},
     publisher = {Springer-Verlag},
     series = {LNCS},
     volume = {2996},
     year = {2004},
     pages = {2 – 18},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-stacs04.ps},
}
A. Nowack. Slicing Abstract State Machines. In Abstract State Machines – Advances in Theory and Practice, vol. 3052 of LNCS. Springer-Verlag, 2004.

Abstract BibTeX

In this work, we introduce slicing for Abstract State Machines (ASMs). The idea of this concept is analogous to the one of program slicing which is an established technique for extracting statements from a program that are relevant for its behaviour at a given point of interest. These statements form again a syntactically correct program called a slice. Previous work has focused on programming languages that differ substantially from ASMs. Although the concept of program slicing does not directly extend to ASMs, it is possible to find an analogous concept for ASMs. We present such an approach.

In spite of the fact that a minimal slice is not computable in the general case, we identify an expressive class of ASMs for which a minimal (static) slice is computable (and prove the computability). This basic result can be extended in several ways. We present some extensions to larger classes of ASMs and other variants for the notion of slicing.

@inproceedings{Nowack04a,
     author = {Antje Nowack},
     title = {Slicing Abstract State Machines},
     booktitle = {Abstract State Machines – Advances in Theory and Practice},
     series = {LNCS},
     volume = {3052},
     year = {2004},
     publisher = {Springer-Verlag},
     url = {http://www.logic.rwth-aachen.de/pub/nowack/asm04.ps},
}
A. Nowack. A Guarded Fragment for Abstract State Machines. In Proceedings of the ESSLLI 2004 Workshop on Guarded Fragments, 2004.

Abstract BibTeX

Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods.

Applications motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results.

In this work, we introduce such a class of ASMs. The idea of this class is the same as for the guarded fragment of first-order logic. We analyse the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works.

@inproceedings{Nowack04b,
     author = {Antje Nowack},
     title = {A Guarded Fragment for Abstract State Machines},
     booktitle = {Proceedings of the ESSLLI 2004 Workshop on Guarded Fragments},
     year = {2004},
     url = {http://www.logic.rwth-aachen.de/pub/nowack/GuardedASMs.ps},
}

2003

D. Berwanger. Game Logic is Strong Enough for Parity Games. Studia Logica, vol. 75(2), pp. 205–219, 2003.

Abstract BibTeX

We investigate the expressive power of Parikh's Game Logic interpreted in Kripke structures, and show that the syntactical alternation hierarchy of this logic is strict. This is done by encoding the winning condition for parity games of rank $n$. It follows that Game Logic is not captured by any finite level of the modal $\mu$-calculus alternation hierarchy. Moreover, we can conclude that model checking for the $\mu$-calculus is efficiently solvable iff this is possible for Game Logic.

@article{Ber03,
     author = {Dietmar Berwanger},
     title = {Game Logic is Strong Enough for Parity Games},
     journal = {Studia Logica},
     publisher = {Kluwer},
     year = {2003},
     volume = {75},
     number = {2},
     pages = {205–219},
     note = {Special issue on Game Logic and Game Algebra edited by M. Pauly and R. Parikh},
     url = {http://journals.kluweronline.com/article.asp?PIPS=5253758},
}
D. Berwanger, E. Grädel, and S. Kreutzer. Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games. In Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning, vol. 2850 of LNCS, pp. 226–240. Springer-Verlag, 2003.

Abstract BibTeX

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*

@inproceedings{BGK03,
     author = {Dietmar Berwanger and Erich Grädel and Sthephan Kreutzer},
     title = {Once Upon a Time in the West. Determinacy, Complexity and Definability of Path Games.},
     booktitle = {Proceedings of the 10th International Conference on Logic for Programming and Automated Reasoning},
     year = {2003},
     series = {LNCS},
     volume = {2850},
     pages = {226–240},
     publisher = {Springer-Verlag},
     copyright = {(c) Springer-Verlag},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar03.ps},
     task = {7},
}
A. Blumensath. Structures of Bounded Partition Width. PhD thesis, RWTH Aachen, 2003.

BibTeX

@phdthesis{Blumensath03,
     author = {A. Blumensath},
     title = {Structures of Bounded Partition Width},
     year = {2003},
     school = {RWTH Aachen},
     address = {Aachen},
     type = {Ph.D. Thesis},
     url = {http://www.logic.rwth-aachen.de/pub/blume/Partition.ps.gz},
}
E. Grädel. Decidable fragments of first-order and fixed-point logic. From prefix-vocabulary classes to guarded logics. In Proceedings of Kalmár Workshop on Logic and Computer Science, Szeged, 2003.

BibTeX

@inproceedings{Graedel03a,
     author = {E. Grädel},
     title = {Decidable fragments of first-order and fixed-point logic. From prefix-vocabulary classes to guarded logics.},
     booktitle = {Proceedings of Kalmár Workshop on Logic and Computer Science, Szeged},
     year = {2003},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-kalmar03.ps},
}
E. Grädel and S. Kreutzer. Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions. In Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 158 – 167, 2003.

BibTeX

@inproceedings{GraedelKr03,
     author = {Erich Grädel and Stephan Kreutzer},
     title = {Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions.},
     booktitle = {Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS)},
     year = {2003},
     pages = {158 – 167},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/GrKr-lics03.ps},
}
E. Grädel and A. Nowack. Quantum Computing and Abstract State Machines. In Abstract State Machines – Advances in Theory and Applications, vol. 2589 of LNCS, pp. 309 – 323. Springer-Verlag, 2003.

BibTeX

@inproceedings{GraedelNo03,
     author = {Erich Grädel and Antje Nowack},
     title = {Quantum Computing and Abstract State Machines},
     booktitle = {Abstract State Machines – Advances in Theory and Applications},
     series = {LNCS},
     volume = {2589},
     pages = {309 – 323},
     year = {2003},
     publisher = {Springer-Verlag},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/GrNo-asm03.ps},
}
S. Kreutzer. Pure and Applied Fixed-Point Logics. In Ausgezeichnete Informatikdissertationen 2002 (D. Wagner et al., Eds.), vol. D-3 of Lecture Notes in Informatics – Dissertations, pp. 59–68. German Informatics Society, 2003.

BibTeX

@incollection{Kre03d,
     author = {Stephan Kreutzer},
     title = {Pure and Applied Fixed-Point Logics},
     booktitle = {Ausgezeichnete Informatikdissertationen 2002},
     pages = {59–68},
     publisher = {German Informatics Society},
     year = {2003},
     editor = {Dorothea Wagner and Others},
     volume = {D-3},
     series = {Lecture Notes in Informatics – Dissertations},
}
A. Nowack. Deciding the Verification Problem for Abstract State Machines. In Abstract State Machines – Advances in Theory and Applications, vol. 2589 of LNCS. Springer-Verlag, 2003.

Abstract BibTeX

We study the decdability of general verification problems for ASMs. This corresponds to the question whether all computations of an ASM satisfy a property (usually expressed in some temporal logic). Because of undecidability in the general case, one has to identify classes of ASMs and classes of properties in order to receive positive decidability results. One idea for this could be to put simple restrictions on the ASMs as forbidding certain advanced constructs. But it turns out that this does not help much. Additionally, the restrictions in those cases are very strong. Consequently, one has to look for others. Such restrictions may result from techniques which are intended to be used in the proofs of decidability. One proof technique is the reduction to a decidable reasoning problem in logic. M. Spielmann has applied it to receive some positive decidability results.

In this paper, we identify further classes of ASMs and classes of properties for which the general verification problem is decidable. Each proof is a reduction to the satisfiability problem of a fragment of linear temporal first-order logic which has respectively been proved to be decidable by I. Hodkinson, F. Wolter and M. Zakharyaschev.

@inproceedings{Nowack03,
     author = {Antje Nowack},
     title = {Deciding the Verification Problem for Abstract State Machines},
     booktitle = {Abstract State Machines – Advances in Theory and Applications},
     series = {LNCS},
     volume = {2589},
     year = {2003},
     publisher = {Springer-Verlag},
     url = {http://www.logic.rwth-aachen.de/pub/nowack/asm03.ps},
}

2002

D. Berwanger and A. Blumensath. Automata for Guarded Fixed Point Logics. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), LNCS, pp. 343-355. Springer Verlag, 2002.

BibTeX

@incollection{BerwangerBl02,
     author = {Dietmar Berwanger and Achim Blumensath},
     title = {Automata for Guarded Fixed Point Logics},
     booktitle = {Automata, Logics, and Infinite Games},
     pages = {343-355},
     publisher = {Springer Verlag},
     year = {2002},
     editor = {E. Grädel and W. Thomas and T. Wilke},
     number = {2500},
     series = {LNCS},
     chapter = {19},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/guarded.ps},
}
D. Berwanger and A. Blumensath. The Monadic Theory of Tree-like Structures. In Automata, Logics, and Infinite Games (E. Grädel, W. Thomas, and T. Wilke, Eds.), LNCS, pp. 285-301. Springer Verlag, 2002.

BibTeX

@incollection{BlumensathBe02,
     author = {Dietmar Berwanger and Achim Blumensath},
     title = {The Monadic Theory of Tree-like Structures},
     booktitle = {Automata, Logics, and Infinite Games},
     pages = {285-301},
     publisher = {Springer Verlag},
     year = {2002},
     editor = {E. Grädel and W. Thomas and T. Wilke},
     number = {2500},
     series = {LNCS},
     chapter = {16},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/muchnik.ps},
}
D. Berwanger and E. Grädel. Fixed point formulae and solitaire games. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.

Abstract BibTeX

The model checking games associated with fixed point logics are parity games, and it is currently not known whether the strategy problem for parity games can be solved in polynomial time. We study , a fragment of least fixed point logic, whose model checking games are nested soltaire games. This means that on each strongly connected component of the game, only one player can make non-trivial moves. Winning sets of nested solitaire games can be efficiently computed. The model checking problem for is Pspace-complete in general and Ptime-complete for formulae of bounded width. On finite structures (but not on infinite ones), is equivalent to transitive closure logic.

@inproceedings{BerwangerGra02,
     author = {Dietmar Berwanger and Erich Grädel},
     title = {Fixed point formulae and solitaire games},
     booktitle = {Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002},
     year = {2002},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/ciad02.ps},
     task = {7},
}
D. Berwanger, E. Grädel, and G. Lenzi. On the variable hierarchy of the modal mu-calculus. In Computer Science Logic, CSL 2002 (J. Bradfield, Ed.), vol. 2471 of LNCS, pp. 352–366. Springer-Verlag, 2002.

Abstract BibTeX

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 mu-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., Box-free) formulae. It is known that these characterize precisely the L_\mu-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.

@inproceedings{BerwangerGraLen02,
     author = {Dietmar Berwanger and Erich Grädel and Giacomo Lenzi},
     title = {On the variable hierarchy of the modal mu-calculus},
     booktitle = {Computer Science Logic, CSL 2002},
     editor = {Julian Bradfield},
     year = {2002},
     series = {LNCS},
     volume = {2471},
     pages = {352–366},
     publisher = {Springer-Verlag},
     copyright = {(c) Springer-Verlag},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/csl02.ps},
}
A. Blumensath. Axiomatising Tree-interpretable Structures. In Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science, vol. 2285 of LNCS, pp. 596–607. Springer-Verlag, 2002.

Abstract BibTeX

Generalising the notion of a prefix-recognisable graph to arbitrary relational structures we introduce the class of tree-interpretable structures. We prove that every tree-interpretable structure is finitely axiomatisable in guarded second-order logic with cardinality quantifiers.

@inproceedings{Bl02,
     author = {A. Blumensath},
     title = {Axiomatising Tree-interpretable Structures},
     booktitle = {Proceedings of 19th International Symposium on Theoretical Aspects of Computer Science},
     year = {2002},
     series = {LNCS},
     publisher = {Springer-Verlag},
     copyright = {(c) Springer-Verlag},
     volume = {2285},
     pages = {596–607},
     url = {http://www.logic.rwth-aachen.de/pub/blume/stacs02.ps.gz},
}
A. Blumensath and E. Grädel. Finite Presentations of Infinite Structures. In Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002, 2002.

Abstract BibTeX

We study definability problems and algorithmic issues for infinite structures that are finitely presented. After a brief overview over different classes of finitely presentable structures, we focus on structures presented by automata or by model-theoretic interpretations. These two ways of presenting a structure are related. Indeed, a structure is automatic if, and only if, it is first-order interpretable in an appropriate expansion of Presburger arithmetic or, equivalently, in the infinite binary tree with prefix order and equal length predicate. Similar results hold for $\omega$-automatic structures and appropriate expansions of the real ordered group. We also discuss the relationship to automatic groups. The model checking problem for $\FO(\exists^\omega)$, first-order logic extended by the quantifier ``there are infinitely many'', is proved to be decidable for automatic and $\omega$-automatic structures. Further, the complexity for various fragments of first-order logic is determined. On the other hand, several important properties not expressible in $\FO$, such as isomorphism or connectedness, turn out to be undecidable for automatic structures. Finally, we investigate methods for proving that a structure does not admit an automatic presentation, and we establish that the class of automatic structures is closed under Feferman-Vaught like products

@inproceedings{BlumensathGra02,
     author = {Achim Blumensath and Erich Grädel},
     title = {Finite Presentations of Infinite Structures},
     booktitle = {Proceedings of the 2nd International Workshop on Complexity in Automated Deduction, CiAD 2002},
     year = {2002},
     note = {Submitted to ACM Theory of Computing Systems},
     url = {http://www.logic.rwth-aachen.de/pub/blume/tocs-2002-ciad.ps},
}
A. Dawar and S. Kreutzer. Generalising Automaticity to Modal Properties of Finite Structures. In Foundations of Software Technology and Theoretical Computer Science, 2002.

Abstract BibTeX

We introduce a complexity measure of modal properties of finite structures which generalises the automaticity of languages. It is based on graph-automata like devices called labelling systems. We define a measure of the size of a structure that we call rank, and show that any modal property of structures can be approximated up to any fixed rank n by a labelling system. The function that takes n to the size of the smallest labelling system doing this is called the labelling index of the property. We demonstrate that this is a useful and fine-grained measure of complexity and show that it is especially well suited to characterise the expressive power of modal fixed-point logics. From this we derive several separation results of modal and non-modal fixed-point logics, some of which are already known whereas others are new.

@inproceedings{KreutzerDaw02,
     author = {Anuj Dawar and Stephan Kreutzer},
     title = {Generalising Automaticity to Modal Properties of Finite Structures},
     booktitle = {Foundations of Software Technology and Theoretical Computer Science},
     year = {2002},
     url = {http://www.logic.rwth-aachen.de/pub/kreutzer/fsttcs.ps},
}
G. Gottlob, E. Grädel, and H. Veith. Datalog LITE: A deductive query language with linear time model checking. ACM Transactions on Computational Logic, vol. 3(1), pp. 1–35, 2002.

BibTeX

@article{GoGrVe99,
     author = {G. Gottlob and E. Grädel and H. Veith},
     title = {Datalog LITE: A deductive query language with linear time model checking},
     journal = {ACM Transactions on Computational Logic},
     year = {2002},
     volume = {3},
     number = {1},
     pages = {1–35},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/GoGrVe-tocl02.ps},
}
E. Grädel. Guarded fixed point logic and the monadic theory of trees. Theoretical Computer Science, vol. 288, pp. 129–152, 2002.

BibTeX

@article{Gr02,
     author = {E. Grädel},
     title = {Guarded fixed point logic and the monadic theory of trees},
     journal = {Theoretical Computer Science},
     volume = {288},
     year = {2002},
     pages = {129–152},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-tcs01.ps},
}
E. Grädel. Model Checking Games. In Proceedings of WOLLIC 02, vol. 67 of Electronic Notes in Theoretical Computer Science. Elsevier, 2002.

Abstract BibTeX

We survey evaluation algorithms for first-order logic and least fixed point logics, and discuss their algorithmic complexity

@inproceedings{GrWollic02,
     author = {E. Grädel},
     title = {Model Checking Games},
     booktitle = {Proceedings of WOLLIC 02},
     series = {Electronic Notes in Theoretical Computer Science},
     publisher = {Elsevier},
     volume = {67},
     year = {2002},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/Gr-wollic02.ps},
}
E. Grädel, C. Hirsch, and M. Otto. Back and Forth Between Guarded and Modal Logics. ACM Transactions on Computational Logics, vol. 3(3), pp. 418 – 463, 2002.

Abstract BibTeX

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

@article{GrHiOt00a,
     author = {E. Grädel and C. Hirsch and M. Otto},
     title = {Back and Forth Between Guarded and Modal Logics},
     journal = {ACM Transactions on Computational Logics},
     pages = {418 – 463},
     volume = {3},
     number = {3},
     year = {2002},
     note = {See also: conference version \citeGrHiOt00},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/GrHiOt-tocl02.ps},
}
E. Grädel, W. Thomas, and T. Wilke (Eds.). Automata, Logics, and Infinite Games. Springer-Verlag, 2002.

BibTeX

@book{GraedelThoWil02,
     editor = {E. Grädel and W. Thomas and T. Wilke},
     title = {Automata, Logics, and Infinite Games},
     publisher = {Springer-Verlag},
     year = {2002},
     series = {Lecture Notes in Compter Science},
     number = {2500},
     url = {http://www.logic.rwth-aachen.de/Books/},
}
C. Hirsch. Guarded Logics: Algorithms and Bisimulation. PhD thesis, RWTH Aachen, 2002.

BibTeX

@phdthesis{HirschThesis,
     author = {Colin Hirsch},
     title = {Guarded Logics: Algorithms and Bisimulation},
     school = {RWTH Aachen},
     year = {2002},
     url = {http://www.logic.rwth-aachen.de/pub/hirsch/hirsch.pdf},
}
S. Kreutzer. Expressive Equivalence of Least and Inflationary Fixed-Point Logic. In Proceedings of the 17th IEEE Symp. on Logic in Computer Science (LICS), 2002.

Abstract BibTeX

We study the relationship between least and inflationary fixed-point logic. By results of Gurevich and Shelah from 1986, it has been known that on finite structures both logics have the same expressive power. On infinite structures however, the question whether there is a formula in $\IFP$ not equivalent to any $\LFP$-formula was still open. In this paper, we settle the question by showing that both logics are equally expressive on arbitrary structures. The proof will also establish the strictness of the nesting-depth hierarchy for $\IFP$ on some infinite structures. Finally, we show that the alternation hierarchy for $\IFP$ collapses to the first level on all structures, i.e. the complement of an inflationary fixed-point is an inflationary fixed-point itself.

@inproceedings{Kreutzer02,
     author = {S. Kreutzer},
     title = {Expressive Equivalence of Least and Inflationary Fixed-Point Logic},
     booktitle = {Proceedings of the 17th IEEE Symp. on Logic in Computer Science (LICS)},
     year = {2002},
     url = {http://www.logic.rwth-aachen.de/pub/kreutzer/ifp.ps},
}
S. Kreutzer. Partial Fixed-Point Logic on Infinite Structures. In Annual Conference of the European Association for Computer Science Logic (CSL), vol. 2471 of Lecture Notes in Computer Science (LNCS). Springer, 2002.

Abstract BibTeX

We consider an alternative semantics for partial fixed-point logic (PFP) To define the fixed point of a formula in this semantics, the sequence of stages induced by the formula is considered. As soon as this sequence becomes cyclic, the set of elements contained in every stage of the cycle is taken as the fixed point. It is shown that on finite structures, this fixed-point semantics and the standard semantics for PFP as considered in finite model theory are equivalent, although arguably the formalisation of properties might even become simpler and more intuitive. Contrary to the standard PFP semantics which is only defined on finite structures the new semantics generalises easily to infinite structures and transfinite inductions. In this generality we compare – in terms of expressive power – partial with other known fixed-point logics. The main result of the paper is that on arbitrary structures, PFP is strictly more expressive than inflationary fixed-point logic (IFP). A separation of these logics on finite structures would prove PTIME different from PSPACE.

@inproceedings{Kreutzer02b,
     author = {S. Kreutzer},
     title = {Partial Fixed-Point Logic on Infinite Structures},
     booktitle = {Annual Conference of the European Association for Computer Science Logic (CSL)},
     year = {2002},
     volume = {2471},
     series = {Lecture Notes in Computer Science (LNCS)},
     publisher = {Springer},
}
S. Kreutzer. Pure and Applied Fixed-Point Logics. PhD thesis, RWTH Aachen, 2002.

BibTeX

@phdthesis{KreutzerThesis,
     author = {Stephan Kreutzer},
     title = {Pure and Applied Fixed-Point Logics},
     school = {RWTH Aachen},
     year = {2002},
     url = {http://www.logic.rwth-aachen.de/pub/kreutzer/kreutzer.pdf},
}
E. Rosen. Some aspects of model theory and finite structures. Bulletin of Symbolic Logic, vol. 8(3), pp. 380 – 403, 2002.

BibTeX

@article{Rosen02,
     author = {Eric Rosen},
     title = {Some aspects of model theory and finite structures},
     journal = {Bulletin of Symbolic Logic},
     year = {2002},
     volume = {8},
     number = {3},
     pages = {380 – 403},
     url = {http://www.logic.rwth-aachen.de/pub/rosen/Rosen02.ps},
}

2001

D. Berwanger and E. Grädel. Games and Model Checking for Guarded Logics. In Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana (R. Nieuwenhuis and A. Voronkov, Eds.), vol. 2250 of LNCS. Springer-Verlag, 2001.

Abstract BibTeX

We investigate the model checking problems for guarded first-order and fixed point logics by reducing them to parity games. This approach is known to provide good results for the modal $\mu$-calculus and is very closely related to automata-based methods. To obtain good results also for guarded logics, optimized constructions of games have to be provided.

Further, we study the structure of parity games, isolate èasy' cases that admit efficient algorithmic solutions, and determine their relationship to specific fragments of guarded fixed point logics.

@inproceedings{BeGr01,
     author = {D. Berwanger and E. Grädel},
     title = {Games and Model Checking for Guarded Logics},
     booktitle = {Proceedings of the 8th International Conference on Logic for Programming and Automated Reasoning, LPAR 2001, Havana},
     editor = {R. Nieuwenhuis and A. Voronkov},
     year = {2001},
     series = {LNCS},
     volume = {2250},
     publisher = {Springer-Verlag},
     copyright = {(c) Springer-Verlag},
     url = {http://www.logic.rwth-aachen.de/pub/graedel/lpar.ps},
}
D. Berwanger. Game Logic is Strong Enough for Parity Games. In Proceedings of the ESSLLI 2001 Workshop on Logic and Games (M. Pauly and G. Sandu, Eds.), Helsinki, 2001.

Abstract BibTeX

This paper is concerned with the expressive power of Parikh's Game Logic interpreted in Kripke structures. We show that the syntactical alternation hierarchy of this logic is strict, by expressing the winning condition for parity games with $n$ priorities. Moreover, it follows that Game Logic is not captured by any finite level of the $\mu$-calculus alternation hierarchy. We can further conclude that model checking for the $\mu$-calculus is efficiently solvable iff this is possible for Game Logic.

@inproceedings{Ber01,
     author = {D. Berwanger},
     title = {Game Logic is Strong Enough for Parity Games},
     booktitle = {Proceedings of the ESSLLI 2001 Workshop on Logic and Games},
     editor = {M. Pauly and G. Sandu},
     year = {2001},
     address = {Helsinki},
     note = {Conference version of \citeBer03},
     url = {http://www.logic.rwth-aachen.de/pub/dwb/helsinki.ps},
}
A. Blumensath. Prefix-Recognisable Graphs and Monadic Second-Order Logic. RWTH Aachen, 2001.

Abstract BibTeX

We present several characterisations of the class of prefix-recognisable graphs including representations via graph-grammars and MSO-interpretations. The former implies that prefix-recognisable graphs have bounded clique-width; the latter is used to extend this class to arbitrary relational structures. We prove that the prefix-recognisable groups are exactly the context-free groups. Finally, we develop methods to prove that certain structures are not prefix-recognisable and apply them to well-ordered structures.

@techreport{Bl01,
     author = {Achim Blumensath},
     title = {Prefix-Recognisable Graphs and Monadic Second-Order Logic},
     institution = {RWTH Aachen},
     year = {2001},
     number = {AIB-06-2001},
     month = {May},
     url = {http://www.logic.rwth-aachen.de/pub/blume/aib-2001-06.ps.gz},
}
A. Dawar, E. Grädel, and S. Kreutzer. Inflationary Fixed Points in Modal Logic. In Proceedings of 15th Annual Conference of the European Association for Computer Science Logic CSL 2001, LNCS. Springer-Verlag, 2001.

Abstract BibTeX

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal $\mu$-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 ha

Mathematische Grundlagen der Informatik

Prof. Dr. Erich Grädel

Publikationen

Noch nicht erschienen

2008

2007

2006

2005

2004

2003

2002

2001