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 ChristianAlbrechtsUniversität zu Kiel Zusammenfassung:
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 nondeterminstic ones.
 Infinite TwoPlayer Games with Partial Information

Montag, 28.04.2008, 10.15 Uhr, Seminarraum Informatik 7 (Raum 4116)
Bernd Puchala RWTH Aachen Zusammenfassung:
In this talk we consider certain aspects of infinite twoplayer 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 twoplayer 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 omegaregular 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 twoplayer 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 TwoPlayer Games of Incomplete Information" from 1984.
Furthermore we have a look at the connection between games with partial information and alternating tree automata
 Controllersynthesis 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 Zusammenfassung:
In this talk, we consider the controllersynthesis 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 branchingtime formulae are different from the properties of winning strategies for lineartime objectives. In particular, the controllersynthesis 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 controllersynthesis 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 Zusammenfassung:
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 Zusammenfassung:
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 observationbased, but may require infinite memory.
This is a joint work with Tom Henzinger and JeanFrancois 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 Zusammenfassung:
The game tree languages can be viewed as an automatatheoretic 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 nontrivial 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 coanalytic sets, and recognizable by a nondeterministic automaton with coBuchi 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 Mucalculus terms (or equivalent automata) by composition of terms of lower level. They showed that separation property fails in general for nondeterministic 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.
 MSOModelChecking over Infinite Graphs — Taking Caucal to the Limit

Donnerstag, 7. August 2008, 11:30 Uhr, Seminarraum Informatik 7 (Raum 4116)
Basile Morcrette ENS Cachan Zusammenfassung:
We review the background results on MSOmodelchecking which lead to the Caucal hierarchy. We propose "UnfoldingMSOschemes" that yield graphs outside the Caucal hierarchy. We show that the "branching" version of these schemes generates graphs with undecidable MSOtheory, 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 Zusammenfassung:
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 CaucalHierarchy. 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 higherorder pushdown automata.
 Decidable Continuous time Temporal Logic

Montag, 11. August 2008, 14:30 Uhr, Seminarraum Informatik 7 (Raum 4116)
Alexander Rabinovich Tel Aviv University Zusammenfassung:
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 Zusammenfassung:
The compositional method, introduced by Feferman and Vaught in 1959, allows to reduce the modelchecking problem for a product structure to the modelchecking problem for its factors. It applies to firstorder 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 (semilinear) 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