Arbeitsgemeinschaft Logik und Automaten

Vorträge im Sommersemester 2007

Optimal Strategies in Request-Response Games

Tuesday, 10th April 2007, 15.00

  Nico Wallmeier
RWTH Aachen


Die klassischen Spieltheorie-Algorithmen liefern nur eine qualitative Aussage über eine Partie, d.h. es wird nur der Gewinner ermittelt. Die Frage, wie gut oder schlecht eine Partie gewonnen bzw. verloren wird, wird dabei nicht beantwortet.

Die Request-Response-Gewinnbedingung fordert nur irgendwann den Besuch der passenden Antwortmenge, wenn die Anforderungsmenge besucht worden ist. Oftmals ist aber eine optimale Strategie gefordert. Dabei ist in diesem Kontext optimal nicht im Sinne der Speichergröße des Controllers gemeint, sondern Optimalität im Bezug auf die Qualität des Gewinnens. Dazu werden in diesem Vortrag verschiedene Qualitätsmaße für Partien in Request-Response-Spielen eingeführt und diskutiert. Es wird ein Algorithmus zur Berechnung optimaler Strategien vorgestellt, der eine Reduktion auf Mean-Payoff-Spiele enthält und zugleich zeigt, dass optimale Strategien durch endliche Automaten implementierbar sind.

Order-invariant MSO is stronger than Counting MSO in the finite

Thursday, 24 May 2007, 14.00

  Tobias Ganzow
RWTH Aachen


We review the concept of order-invariance and present some classes of structures on which the "order-invariant fragment" of FO, resp. MSO, is known to be more expressive than the plain logic itself. The easiest examples of order-invariantly definable properties of structures in those classes are modulo-counting properties, e.g., that the universe contains an even number of elements.

By explicitly adding the possibility of stating things like "the number of elements in X is even" (or divisible by k, for some arbitrary but fixed integer k) to MSO, we obtain a logic called "Counting MSO" (CMSO). It is not hard to see that such statements about the cardinality of sets can be translated into order-invariant MSO sentences. On the other hand, it has not yet been clear whether, in general, order-invariant formulae can express more than just modulo-counting properties. Courcelle proved that on the class of forests order-invariant MSO collapses to CMSO, but he conjectured that order-invariant MSO is more expressive than CMSO in general.

We present an Ehrenfeucht-Fraisse game capturing the expressiveness of CMSO and a class of grid-like structures that is order-invariantly definable in MSO but not in CMSO, thus proving Courcelle's conjecture.

Two-Player Graph Games with Partial Information

Thursday, 21 June 2007, 14:00

  Bernd Puchala
RWTH Aachen


We consider a model for two-player graph games with partial information that originally has been suggested by John H. Reif in 1979 in his paper "Universal Games of Incomplete Information". We will have a look at the properties of this model and how information evolves over time in a particular play of such a game.

The major issue is the complexity of the outcome problem for these games which is the following decision problem. Given a game G and an initial position v, does player 1 have a winning strategy for G from v? We consider two different notions of strategies and we will show for both outcome-problems, that they are complete for the class EXPTIME. To prove the membership in the class we will use a powerset construction which turns a game with partial information into a game with full information. This construction also shows that the games we are considering allow finite memory strategies. For the EXPTIME-hardness we use the concept of private alternating Turing-machines which are a generalizaton of usual alternating Turing-machines.

Finally we want to have a look at further questions concerning such games, especially logical definability of the indistinguishability of positions.

Unranked Tree Automata with Sibling Equalities and Disequalities

Friday, 6 July 2007, 11 a.m.

  Wong Karianto
RWTH Aachen


This is a joint work with Christof Löding.

We propose an extension of the tree automata with constraints between direct subtrees (Bogaert and Tison, 1992) to unranked trees. Our approach uses MSO-formulas to capture the possibility of comparing unboundedly many direct subtrees. Our main result is that the nonemptiness problem for the deterministic automata, as in the ranked setting, is decidable. Furthermore, we show that the nondeterministic automata are more expressive than the deterministic ones.

Memory Reduction for Strategies in Infinite Games

Friday, 6 July 2007, 11:35 a.m.

  Michael Holtmann
RWTH Aachen


We deal with the problem of reducing the memory necessary for implementing winning strategies in infinite games. We present an algorithm that is based on the notion of game reduction. The key idea of a game reduction is to reduce the problem of computing a solution for a given game to the problem of computing a solution for a new game which has an extended game graph but a simpler winning condition. The new game graph contains the memory to solve the original game. Our algorithm computes an equivalence relation on the vertices of the extended game graph and from that deduces equivalent memory contents. We apply our algorithm to Request-Response and Staiger-Wagner games where in both cases we obtain a running time polynomial in the size of the extended game graph. We compare our method to the technique of minimising strategy automata and present an example for which our approach yields a substantially better result.

Modelchecking über Produktstrukturen

Montag, 16. Juli 2007, 14.00 Uhr

  Ingo Felscher
RWTH Aachen


Feferman und Vaught haben 1959 ein Verfahren entwickelt, mit dem Aussagen über einem Produkt von Strukturen auf Aussagen über die Komponenten des Produkts zurückgeführt werden können.

In diesem Vortrag wird gezeigt, wie die Feferman-Vaught-Technik für das Modelchecking-Problem genutzt werden kann, um eine Formel der Modallogik, die über einem Produkt von Transitionssystemen interpretiert wird, auf Formeln der Modallogik zurückzuführen, die in den einzelnen Transitionssystemen interpretiert werden. Statt das Modelchecking-Problem im Produkt zu lösen, können somit Modelchecking-Probleme der so entstandenen Formeln in den Komponenten gelöst werden.

Ausgehend von den Spezialfällen des asynchronen und direkten Produkts, wird gezeigt, in wie weit die Produkte und die Logik verallgemeinert werden können, so dass die Technik noch angewendet werden kann.

Dazu wird ein Verfahren vorgestellt mit dem bewiesen werden kann, dass für eine Logik, die eine bestimmte Formel ausdrücken kann, der Feferman-Vaught-Satz nicht gilt. Dieses Verfahren wird verwendet, um zu zeigen, dass für Erweiterungen der Modallogik durch verschiedene Erreichbarkeitsaussagen die Feferman-Vaught-Technik im asynchronen bzw. im direkten Produkt nicht anwendbar sind.

Infinite Games over Higher-Order Pushdown Systems

Thursday, 2 August 2007, 11.00

  Michaela Slaats
RWTH Aachen


In this talk we deal with games on pushdown graphs with regular winning conditions. For these games it is known that the winning regions are regular sets of configurations.

We extend this result to games over higher-order pushdown systems. They work over higher-order pushdown stacks which are stacks of stacks of stacks etc.. We concentrate in this talk just on level 2 stacks that are stacks that contain a sequence of level 1 stacks; the results can easily be lifted to level n. For the definition of regularity over higher-order stacks we use a technique recently developed by Carayol.

We will present an optimal algorithm (w.r.t. time complexity) to compute the winning region of reachability games and of parity games over higher-order pushdown graphs. For the treatment of parity games we use a method of Vardi (reduction of two-way to one-way tree automata).

Model Checking Games for the Quantitative mu-Calculus

Tuesday, 28 August 2007, 14.00

  Diana Fischer
RWTH Aachen


In this talk, we introduce the quantitative mu-calculus, an extension of the classical modal mu-calculus. In this logic, propositions can take values in the non-negative reals with infinity and we can discount values. This logic is interpreted over transition systems, in which states and transitions are labelled with quantities.
To get a better understanding of the quantitative mu-calculus, we look at the connection between the classical mu-calculus and parity games and generalise it to the quantitative setting.
We introduce an appropriate game model of quantitative parity games, where terminal positions are labelled with values and moves are labelled with discounts. In this model finite plays have an outcome in the non-negative reals with infinity, whereas the outcome of infinite plays is either 0 or infinity, depending on the lowest priority seen infinitely often in the play. These games do not enjoy the same properties as classical parity games, as even in simple cases, optimal strategies need not exist and epsilon-optimal strategies may require an unbounded amount of memory.
Following the method of unfolding parity games, we show that these games are determined and can be used for model checking the quantitative mu-calculus.

Operations Preserving Recognizable Languages

Tuesday, 4 September 2007, 14.00

  Jean-Éric Pin
LIAFA, Université Paris VII and CNRS


Given a subset S of N, filtering a word a0a1 ... an by S consists in deleting the letters ai such that i is not in S. By a natural generalization, denote by L[S], where L is a language, the set of all words of L filtered by S. The filtering problem is to characterize the filters S such that, for every recognizable language L, L[S] is recognizable. In this paper, the filtering problem is solved, and a unified approach is provided to solve similar questions, including the removal problem considered by Seiferas and McNaughton. There are two main ingredients on our approach: the first one is the notion of residually ultimately periodic sequences, and the second one is the notion of representable transductions.