Arbeitsgemeinschaft Logik und Automaten
Vorträge im Sommersemester 2003
- Winning Strategies for Infinite Games: From Large Cardinals to Effective Cases
17.7.2003, 14 Uhr
Jean Pierre Ressayre, Université Paris VII
Martin proved the existence of a winning strategy for one of the players in every infinite game of perfect information between two players, if the winning set of one of the players happens to be an analytic one. But Martin's proof uses a large cardinal axiom: the "axiom of sharps". And Harrington proved that this axiom is in a sense requiered to have the result. This underlies the fact that the winning strategy proved to exists is in the general case of the most extremely noneffective kind. Nevertheless we modify and supplement Martin's proof so that it yields again the Rabin, Buechi-Landweber, Gurevich-Harrington theorem - of existence of finite state winning strategies when the player's winning sets are themselves finite state accepted. This is for us only a first part of the effectivization of Martin's proof, which only gets a known result. But a second part with new applications should follow.
- On the Bisimulation Invariant Fragment of MSO over the Finite
David Janin, Université Bordeaux 1
Over arbitrary graph (finite and infinite), it is known that the bisimulation invariant fragment of monadic seconc order logic (MSO) is as expressive as the modal μ-calcul. If a similar result holds when restricting bisimulation invariance to finite graphs is essentially an open problem. Eric Rosen proved that the bisimulation invariant fragment of first order logic (FO) over the finite equals modal logic. With Anuj Dawar, we recently prove that the bisimulation invariant fragment of existential MSO (EMSO) over the finite equals the extention of modal logic by greatest fixed point construction, i.e. the ν-fragment of the μ-calculus. After reviewing some background notions about this topic I will essentially give a sketch of the proof of this last result.
- Planar Invariant Properties of Cycle Matchings
Christof Löding, RWTH Aachen
A labeled cycle matching (LCM) is a structure over a universe U of even cardinality with unary predicates for the labels, a binary successor relation S such that the graph (U,S) is a cycle, a ternary between-ness predicate B, and a binary relation M that is a maximal matching on U. An LCM is called planar if the graph with edges corresponding to S and M is planar. A first order sentence is planar invariant if it cannot distinguish planar LCMs that only differ in the matching M.
We show that planar invariant FO properties over LCMs can be expressed without use of the matching M. This answers a conjecture by Michael Benedikt and Jan van den Bussche that came up in connection with planar invariant queries on closed semi algebraic sets over the real plane (this connection will not be discussed in the talk). The core of the proof is an automata-theoretic characterization of FO-definable languages of words of even length.
- Infinite Graphs, Representations and Manipulations
5.6.2003, 14 Uhr
Thomas Colcombet, IRISA Rennes
We focus on the equational representation of infinite graphs (or structures) which amounts to the "evaluation" of infinite terms. Following the theory known over finite terms, we develop the idea of "top down deterministic tree transducer" (TDDTT) and its extension with "rational lookahead". We show that this tool is a convenient alternative to "a la Courcelle" MS-transductions for manipulating equational systems.
We then illustrate this technique by considering successively the prefix recognizable graphs, the Caucal hierarchy, the automatic graphs, the ground tree rewriting graphs and the tree automatic graphs. We show that different equivalence results for those families can be expressed in the framework of TDDTT.
- Confluence of Right Ground Term Rewriting Systems and Related Problems
Lukasz Kaiser, Universität Wroclaw
Term rewriting systems (TRS) are often used as models of programs and mathematical structures. Important properties of TRSes like reachability, joinability, weak confluence and confluence are in general undecidable but are decidable for certain classes of term rewriting systems. We will show how these problems can be analyzed in right ground TRSes. First we will state basic facts about reachability and joinability and sketch the methods used to decide these problems. We will also show a few basic reductions between these problems to show their connections with each other. Later we will reduce confluence of right ground TRSes to simpler problems and give an overview of methods used to solve them. We will also present an undecidability result for common ancestor problem to give a better insight into the presented problems.
- Aspects of mu-arithmetic
21.5.2003, 16.30 Uhr
Michael Möllerfeld, Universität Bonn
The μ-calculus is a system of positive inductive definitions, which is widely spread in computer science. Reals (i.e., sets of natural numbers) definable in the μ-calculus with coding are called μ-arithmetical reals. The class of μ-arithmetical reals extends Π11 and is a proper subclass of Δ12. We present several characterizations of this class using concepts of different areas of logic.
- Strategy Synthesis Without Full Determinisation
15.5.2003, 14 Uhr
Pierre-Yves Schobbens, Université Namur
The usual algorithm for computing strategies in a game where the winning condition is given by an automaton first determinises the automaton. For Buchi automata, this is done by Safra's algorithm, which is known to be inefficient in practice. For automata that are reverse deterministic outside ~ and deterministic inside ~, we propose to use another algorithm that use the usual subset construction which is practically more efficient. This apparently strange condition is naturally satisfied by Buchi automata build from future-time temporal logics. We illustrate it on the logic ATL*, where it yields a simple symbolic algorithm for strategy synthesis.
This is work in progress.
This is common work with Aidan Harding and Mark Ryan.