Arbeitsgemeinschaft Logik und Automaten

Vorträge im Sommersemester 2008

Complementation, Disambiguation, and Determinization of Büchi Automata Unified

Mittwoch, 2. April 2008, 15 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Thomas Wilke
Christian-Albrechts-Universität zu Kiel


We present a uniform approach to (1) complementing Büchi automata, (2) turning Büchi automata into equivalent unambiguous Büchi automata, and (3) turning Büchi automata into equivalent deterministic parity automata. In particular, we present the first solution to (2) which does not make use of McNaughton's theorem (determinization).

Our results are based on Muller and Schupp's procedure for turning alternating tree automata into non-determinstic ones.

Infinite Two-Player Games with Partial Information

Montag, 28.04.2008, 10.15 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Bernd Puchala
RWTH Aachen


In this talk we consider certain aspects of infinite two-player games with partial information. We introduce and discuss a model for such games which generalizes certain other models and we have a look at different possibilities to define partial information in infinite games which are played on finite graphs, especially definability in certain logical systems.

The focus of this talk is on the strategy problem, that means, the following decision problem. Given a two-player game G with partial information and some initial position v, does player 1 have a winning strategy for G from v? We prove upper and lower bounds on the complexity of this problem for omega-regular games as well as upper and lower bounds on the memory which is needed to implement winning strategies. We consider two different ways to define partial information in two-player games which leads to two different notions of strategies. The starting point for these results is a construction which has been presented by John H. Reif in his paper 'The Complexity of Two-Player Games of Incomplete Information" from 1984.

Furthermore we have a look at the connection between games with partial information and alternating tree automata

Controller-synthesis for Markov decision processes and branching time logics

Freitag, 16.5.2008, 11 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Vojtěch Forejt
Masaryk University, Brno


In this talk, we consider the controller-synthesis problem for Markov decision processes (MDP) and PCTL (a probabilistic extension of CTL). The problem is defined as follows: Given an MDP and a PCTL formula, is there a strategy (controller) that ensures satisfying of the formula?

Properties of winning strategies for branching-time formulae are different from the properties of winning strategies for linear-time objectives. In particular, the controller-synthesis problem for PCTL is undecidable in general. In the talk we point out main ideas of the proof. Then we restrict ourselves to the qualitative fragment of PCTL. This fragment is still very strong and allows us to express many interesting properties. We argue that the controller-synthesis problem for this fragment is decidable despite the fact that winning strategies may require infinite memory.

Recognizable vs. Regular Picture Languages

Freitag, 6. Juni 2008, 11 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Oliver Matz
Universität Kiel
Order independence of strategy elimination procedures in strategic games

Montag, 9. Juni 2008, 11 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Krzysztof R. Apt
CWI and University of Amsterdam


In the area of strategic games several strategy elimination procedures have been proposed and their order independence (confluence) has been studied. We show that the appropriate results can be derived in a uniform way using Newman's Lemma and Tarski's Fixpoint Theorem.

Equivalence of Labeled Markov Chains

Dienstag, 10. Juni 2008, 14 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Laurent Doyen
EPFL Lausanne


We consider the equivalence problem for probabilistic machines. Two probabilistic machines are equivalent if every finite sequence of observations has the same probability of occurrence in the two machines. We show that deciding equivalence is polynomial for labeled Markov chains, using a reduction to the equivalence problem for probabilistic automata, which is known to be polynomial. We provide an alternative algorithm to solve the latter problem, which is based on a new definition of bisimulation for probabilistic machines.

Then, we consider the equivalence problem for labeled Markov decision processes (LMDPs) which asks given two LMDPs whether for every way of resolving the decisions in each of the processes, there exists a way of resolving the decisions in the other process such that the resulting probabilistic machines are equivalent. The decidability of this problem remains open. We show that the strategies used to resolve the decisions can be restricted to be observation-based, but may require infinite memory.

This is a joint work with Tom Henzinger and Jean-Francois Raskin.

Topological Properties of Game Tree Languages – Results on Inseparability

Mittwoch, 25. Juni 2008, 16 Uhr, Seminarraum Informatik 1 (Raum 4017)

  Damian Niwinski
University of Warsaw


The game tree languages can be viewed as an automata-theoretic counterpart of parity games on graphs. They play an important role in the complexity analysis of tree automata, as they witness the strictness of the alternating index hierarchy.

We show a topological argument behind the strictness result, by proving that the game languages form a hierarchy in the sense of Wadge.

We also consider a game tree language of the first non-trivial level, where Eve wins if 1 occurs only finitely often, and its ``twin'', obtained by interchanging Eve with Adam, and 0 with 1. Both these sets (which amount to one up to a renaming) are complete in the class of co-analytic sets, and recognizable by a non-deterministic automaton with co-Buchi condition. We show that they cannot be separated by any Borel set.

This settles a case left open in the paper by A.Arnold and L.Santocanale (2005), who studied separation of the Mu-calculus terms (or equivalent automata) by composition of terms of lower level. They showed that separation property fails in general for non-deterministic automata of type Sigma (Mu Nu Mu...), starting from level n=3, and our result settles the missing case n=2.

Joint work with Szczepan Hummel and Henryk Michalewski.

MSO-Model-Checking over Infinite Graphs — Taking Caucal to the Limit

Donnerstag, 7. August 2008, 11:30 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Basile Morcrette
ENS Cachan


We review the background results on MSO-model-checking which lead to the Caucal hierarchy. We propose "Unfolding-MSO-schemes" that yield graphs outside the Caucal hierarchy. We show that the "branching" version of these schemes generates graphs with undecidable MSO-theory, and we finally discuss the more restricted case of "linear" schemes.

The Caucal Hierarchy

Montag, 11. August 2008, 13:30 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Achim Blumensath
TU Darmstadt


A standard problem in algorithmic model theory consists in giving algebraic characterisations of the structures in a given class of finitely presented structures. That is, one would like to develop methods to determine whether a given structure can be presented in a certain way. In this talk I will focus on the Caucal-Hierarchy. After recalling its definition and some of its characterisations, I will present two techniques to prove that some structures do not belong to a given level of this hierarchy. The first one is a result giving a bound of the outdegree of definable relations. The second one is a pumping lemma for higher-order pushdown automata.

Decidable Continuous time Temporal Logic

Montag, 11. August 2008, 14:30 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Alexander Rabinovich
Tel Aviv University


In this talk we survey expressiveness and complexity results for continuous time Temporal Logic which can specify metric properties.

The compositional method and regular reachability

Montag, 11. August 2008, 15:30 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Ingo Felscher
RWTH Aachen


The compositional method, introduced by Feferman and Vaught in 1959, allows to reduce the model-checking problem for a product structure to the model-checking problem for its factors. It applies to first-order logic, and limitations for its use have recently been revealed by Rabinovich (2007). We sharpen the results of Rabinovich by showing that the composition method is applicable to the asynchronous product (and the finitely synchronized product) for an extended modal logic in which the reachability modality is enhanced by a (semi-linear) condition on path lengths. We show that a slight extension leads to the failure of the composition theorem. We add comments on extensions of the result and open questions.

Complexity Measures for Directed Graphs

Freitag, 22. August 2008, 10 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Roman Rabinovich
RWTH Aachen