Arbeitsgemeinschaft Logik und Automaten
Vorträge im Wintersemester 2003
- Concurrent Parity Games
7.11.2002, 14 Uhr
Marcin Jurdzinski, University of California
Behavioral properties of open systems can be formalized as objectives in two-player games. Turn-based games model asynchronous interaction between the players (the system and its environment) by interleaving their moves. Concurrent games model synchronous interaction: the players always move simultaneously. We consider infinitary parity winning conditions for concurrent games played on finite graphs.
A generalization of determinacy to concurrent parity games demands probabilistic (mixed) strategies: either player 1 has a mixed strategy to win with probability 1 (almost-sure winning), or player 2 has a mixed strategy to win with positive probability.
This work provides efficient reductions of concurrent probabilistic Buchi and co-Buchi games to turn-based games with Buchi condition and parity winning condition with three priorities, respectively. The reductions improve understanding of concurrent games and provide an alternative simple proof of determinacy of concurrent Buchi and co-Buchi games. From a practical point of view, the reductions turn solvers of turn-based games into solvers of concurrent probabilistic games. Thus improvements in the well-studied algorithms for the former carry over immediately to the latter. In particular, a recent improvement in the complexity of solving turn-based parity games yields an improvement in time complexity of solving concurrent probabilistic co-Buchi games from cubic to quadratic.
- n-iterated Pushdown Automata, Application in Arithmetic
28.11.2002, 14 Uhr
Séverine Fratani, Université Bordeaux 1
We study n-iterated automata. The class of languages accepted by these automata, called level-n languages, constitute a strict hierarchy, for which the first terms are rational languages while the second are context-free languages. We first show the already know results on decidability by using an extension of the Rabin's theorem on tree structure due to Muchnik, then we prove that the second order monadic theory of computation graphs of these automata is decidable. We present next some class of languages of different levels. Finally the study of these languages permit us to show a class of unary predicates P for which the structure < N ,succ, P > admit a decidable second order monadic theory.
- Ein "Gittersatz" für die Cliquenweite - auf dem Weg zur Vermutung von Seese?
05.12.2002, 14 Uhr
Achim Blumensath, RWTH Aachen
- Parity Games played on BPA graphs
12.12.2002, 14 Uhr
Olivier Serre, Université Paris 7
A BPA is a special case of pushdown process that only have one state. As for pushdown, we associate with a BPA a graph whose nodes are the set of configurations of the BPA (i.e. the words on the BPA's alphabet) and whose edges are induced by the rewriting rules. We first assume that the rewriting rules of the BPA only depend on the top symbol and we partition the nodes between two players and we color them depending on their top letter: this defines a two players parity game on an infinite graph that we call a local parity BPA game. We show that for such a game, the winning strategy only depends on the top stack symbol and therefore, deciding the winner is in NP ∩ co-NP. Then we give an algorithm to decide the winner in a local parity BPA game in exponential time in the number of colors. For this, we use a Turing reduction to parity games on finite graphs. Then we consider a natural generalization of local BPA games: global BPA games.
For this, the set of configuration is partitioned into two regular languages and colored according to a partition of the set of configurations into regular languages. Moreover, rewriting rules do not only depend on the top symbol but also on the color of the configuration. We give an exponential reduction to local BPA game that leads to a DEXPTIME algorithm to decide the winner in a global parity BPA game. As a by product we show that the set of winning positions for a given player is regular. Finally, we show that deciding the winner in a global parity BPA game is a DEXPTIME-hard problem.
- Eine Erweiterung des Satzes von Muchnik
09.01.2003, 14 Uhr
Achim Blumensath, RWTH Aachen
- Remarks on the Improvement Algorithm for Soving Parity Games
Mariane Riss, RWTH Aachen
The complexity of the improvement algorithm (due to J. Vöge and M. Jurdzinski) is still unknown. I will try to show the reason why the computation of this complexity is so difficult. I will present different approaches which all failed. However these failures point out the core problem.
- On a Hierarchy of Graph Families
23.01.2003, 14 Uhr
Didier Caucal, IRISA Rennes
Starting from the finite graphs and using the unfolding followed by the inverse rational mapping, we present an infinite hierarchy of families of graphs having a decidable monadic theory. The first level of this hierarchy is the family of prefix-recognizable graphs, which are the graphs obtained by transitive closure of the pushdown transition graphs, and are also the graphs obtained by monadic second order interpretations from the binary tree. For each family of this hierarchy, we give closure properties and a tree generator. We show also that this hierarchy contains the transition graphs of multi level stack automata, and the solutions of higher order recursive schemes.
- Synthesizing a Discrete Controller
30.01.2003, 14 Uhr
Igor Walukiewicz, Université Bordeaux 1
We put the synthesis of controllers for discrete event systems, as introduced by Ramadge and Wonham, into the game framework. We show that in this framework it is possible to extend the specifications of the supervised systems as well as the constraints on the controllers by expressing them in the modal μ-calculus.
In order to express unobservability constraints, we propose an extension of the modal μ-calculus in which one can specify whether an edge of a graph is a loop. This extended μ-calculus still has the interesting properties of the classical one. In particular it is equivalent to automata with loop testing. The problems such as emptiness testing and elimination of alternation are solvable for such automata.
The proposed method relies on a simple construction of the quotient of automata with loop testing by a deterministic transition system. This is enough to deal with the centralized control problems. The solution of the decentralized control problems uses a more involved construction of the quotient of two automata.
This work extends the framework of Ramadge and Wonham in two directions. We consider infinite behaviours and arbitrary regular specifications, while the standard framework deals only with specifications on the set of finite paths of processes. We also allow dynamic changes of the set of observable and controllable events.
- Context-sensitive Traces of Infinite Graphs
Antoine Meyer, Université Paris 7
The well-known Chomsky hierarchy of formal languages can be extended to a hierarchy of (infinite) graphs by considering the trace languages of graphs. For example, the rational languages are the traces of finite graphs, and the recursively enumerable languages are the traces of the transition graphs of Turing machines.
Recently, Morvan introduced the family of rational graphs, and showed that their traces are the context-sensitive languages. This result was later extended by Rispal to the smaller family of synchronized (rational) graphs. However, neither of these results was able to provide any insight on the case of deterministic context-sensitive languages.
In this talk, we will try to present families of graphs whose traces are the deterministic context-sensitive languages. In a first part, we bring some modifications to the proof techniques used in the work of Morvan and Rispal, which enable us to consider the deterministic case. Then, after drawing conclusions from this first construction, we will present a different approach of the same problem by introducing the transition graphs of linearly-bounded Turing machines.
- Graphen mit entscheidbarer monadischer Theorie 2. Stufe und Anwendungen für Cayley-Graphen
13.02.2003, 14 Uhr
Markus Lohrey, Universität Stuttgart
(gemeinsame Arbeit mit Dietrich Kuske)
Monadische Logik 2. Stufe (kurz MSO-Logik) nimmt innerhalb der Theoretischen Informatik eine herausragende Rolle ein: Sie ist einerseits extrem ausdrucksstark, andererseits lassen sich noch Entscheidbarkeitsresultate zeigen.
In dem Vortrag wird für eine Teilklasse von (unendlichen) Graphen eine Charakterisierung der Graphen mit einer entscheidbaren MSO-Theorie vorgestellt. Genauer wird gezeigt, dass für einen zusammenhängenden Graphen G mit beschränktem Grad, der außerdem nur endlich viele Orbits unter seiner Automorphismengruppe besitzt, die folgenden Aussagen äquivalent sind:
- G hat eine entscheidbare MSO-Theorie.
- G ist kontextfrei im Sinne von Muller/Schupp.
- G hat endliche Baumweite.
Als Korollar folgt, dass eine endlich erzeugte Gruppe genau dann einen Cayley-Graphen mit einer entscheidbaren MSO-Theorie hat, wenn die Gruppe kontextfrei ist. Ähnliche Resultate für Logik 1.Stufe sowie Cayley-Graphen von Monoiden werden ebenfalls vorgestellt.
- Numeration Systems and Recognizability: From Integer Base Systems to Abstract Systems Built on a Regular Language
20.02.2003, 14 Uhr Raum 5052
Michel Rigo, Université de Liège
For a given numeration system, for instance when considering the binary system, an important question related to formal languages theory is the following one: let X be a subset of integers, is the language made up of the representations of the elements in X regular ? In the affirmative case, the set is said to be recognizable.
In the first part of this talk, we will survey various results concerning recognizable sets of integers with respect to positional numeration systems. As an example, recognizable sets can be defined by first order formulas of the Presburger arithmetic extended with some function related to the considered numeration system. This characterization also holds for linear systems built upon a Pisot number (so, in particular, for integer base systems or for the Fibonacci system). These latter systems have two important properties: the language of all the representations is regular and the function mapping an integer onto its representation is strictly increasing (with respect to the genealogical ordering).
This observation leads to the following generalization. Consider an arbitrary infinite regular language L over the totally ordered alphabet (A,<). Ordering the words of L with respect to the genealogical order induced by the ordering of A leads to a one-to-one correspondence between N and L. Therefore, we can be interested in the corresponding recognizable sets of integers. Observe that an abstract system defined by a triple (L,A,<) is generally not a positional system. We will show for instance that any arithmetic progression is always recognizable in any abstract system. Next, we will show that in a general setting, multiplication by a constant does not preserve recognizability (here the results are related to the complexity function, or growth function, of the language L).
Finally, we will present an extension of these abstract systems to be able to represent not only integers but also real numbers. In this latter case, the representations are infinite words which are limit of finite words in L. Moreover in this setting, a real number can have one, a finite number or even an infinite number of representations and the situation is completely determined from the automaton accepting L.
- WS1S erweitert mit Kardinalitätsvergleichen
Dienstag,25.02.2003, 14 Uhr
Felix Klaedtke, Universität Freiburg
(gemeinsame Arbeit mit Harald Ruess)
Ich stelle eine Erweiterung der monadischen Logik zweiter Stufe (MSO) ueber (endlichen) Wörter vor, die es erlaubt, Kardinalitäten von MSO Variablen durch atomare Formeln der Form |X_1| + ... + |X_r| < |Y_1| + ... + |Y_s| zu vergleichen. Die klassische Beziehung zwischen endlichen Automaten und der MSO Logik über Wörter ueberträgt sich auf gewichtete Automaten mit linearen arithmetischen Bedingungen und dem existentiellen Fragment der Logik. Basierend auf dieser Charakterisierung durch Automaten lassen sich mehrere (Un-)Entscheidbarkeitsresultate über Fragmente der MSO Logik über Woerter mit Kardinalitätsvergleichen zeigen, die die Grenze des Entscheidbaren abstecken. Die benutzten Techniken lassen sich (mindestens) auf Bäume verallgemeinern.
- Remarks on Positive Games and Persistent Strategies
27.02.2003, 14 Uhr
Jacques Duparc, RWTH Aachen
At CSL 2002, as well as at the GAMES kickoff meeting, Jerzy Marcinkowsi introduced the notions of positive game and persistent strategy.
Given any finite or infinite run played on a game graph, a strategy is persistent if each time the player visits some vertex already encountered, this player repeats the decision made when visiting this vertex for the first time.
Such strategies require at least some memory, but once a choice is made, it is made for ever. So, in some way, persistency extends somewhere between the two notions of memoryless and LAR.
In "Optimal Complexity Bounds for Positive LTL Games", Jerzy Marcinkowsi and Tomasz Truderung showed that in games with positive winning condition the opponent has a winning strategy if and only if he has a persistent winning strategy. Here, ``positive game'' means a game such that for any two infinite sequences (of vertices) x and y, where x is a subsequence of y, whenever the game x is won, the game y is won as well. We will show how close to persistent strategy, the notion of positive game is. And since the latter is a reliable criterion to discriminate between persistent and non persistent strategies, we will bring out its topological complexity:
- When restricted to finite game graphs, positive games are simple objects. They are all countable intersections of open sets. We will refine this analysis to point out the Wadge classes involved.
- To the contrary, when dealing with infinite game graphs, we will show that the topological complexity of positive games may be really awful, and lead to non determined games.
To conclude, we'll discuss the role of positive games defined in terms of Muller winning conditions, and the one of persistent winning strategies for such games.