Arbeitsgemeinschaft Logik und Automaten

Vorträge im Sommersemester 2010

Two-Variable Logic with Two Order Relations

Dienstag, 22. Juni 2010, 16:30 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Thomas Schwentick
TU Dortmund


The finite satisfiability problem for two-variable logic over structures with unary relations and two order relations is investigated. Firstly, decidability is shown for structures with one total preorder relation and one linear order relation. More specifically, we show that this problem is complete for EXPSPACE. As a consequence, the same upper bound applies to the case of two linear orders. Secondly, we prove undecidability for structures with two total preorder relations as well as for structures with one total preorder and two linear order relations. Further, we point out connections to other logics. We conclude (and that was the main motivation of this work), that decidability is shown for two-variable logic on data words with orders on both positions and data values, but without a successor relation. Also "partial models" of compass and interval temporal logic are considered and decidability for some of their fragments is shown.

Besides presenting the technical results, the talk will give a short introduction to recent research on data words.

Game Theoretic Analysis of Dynamic Networks

Dienstag, 7. September 2010, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Sten Grüner
RWTH Aachen University


Dynamic network games are a flexible framework for simulation and verification of fault-tolerant systems. Rather than playing on a fixed Kripke structure, two players modify the game graph. One player deleting nodes of the game graph faces an opponent who modifies the graph by application of predefined rules. In general, these rules may include relabeling, movement and creation of vertices in the game graph. We are mainly interested in reachability and safety games respective connectivity as the winning condition. In other words, a play ends if a connected resp. a disconnected graph is reached. In our talk we introduce and discuss dynamic network games. We show that determining the winner in a dynamic network game is undecidable in both the reachability and the safety setting for the general case. In some cases where only a subset of rules are allowed the game problem becomes decidable. Finally, we will introduce further topics of our research including dynamic network games with LTL winning conditions and games in a probabilistic setting.

Unendliche Zweipersonenspiele mit Verzögerter Information

Mittwoch, 15. September 2010, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Frank Pöttgen
RWTH Aachen University


Unendliche Spiele sind wichtige Werkzeuge zum Design von reaktiven Systemen. In dieser Arbeit werden Varianten von unendlichen Zweipersonenspielen untersucht, bei denen die Information über die Spielzüge des Gegners verzögert wird. Damit kann man verteilte Systeme modellieren, bei denen die Signalübertragung zwischen Komponenten verzögert ist. Verzögerungen führen leicht zur Nichtdeterminiertheit von Spielen. Für reguläre Spiele kann man entscheiden, ob solche Verzögerungen existieren. Falls solche Verzögerungen existieren, kann eine obere Schranke der konstanten Verzögerungen mit Determiniertheit angegeben werden. Für jeden Spieler kann man au├čerdem entscheiden, ob er ein gegebenes reguläres Spiel mit festen konstanten Verzögerungen gewinnt. Auf diese Weise wird der komplette Bereich der konstanten Verzögerungen abgedeckt. Beide Entscheidungsverfahren sind für nicht reguläre Spiele nicht möglich, z.B. wenn die Gewinnbedingung durch eine kontextfreie omega-Sprache gegeben ist.

Mean-Payoff Parity Games and Permissive Strategies

Donnerstag, 16. September 2010, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Jörg Olschewski
RWTH Aachen University


Two-player turn-based games are commonly used as a model for the verification and synthesis of controllers. Usually, a player's behaviour in such a game is given by a deterministic strategy, which selects a single move for every controllable history. By allowing several moves to be selected, we obtain the notion of a multi-strategy. In this setting, the player playing according to a multi-strategy permits several different outcomes of the game, and thus allows more behaviours. Intuitively, a multi-strategy is more permissive if it allows more moves to be selected. Formally, we assign a penalty to each move, which is incurred by a multi-strategy if it blocks this move; the penalty of the strategy is the average penalty that is incurred in the limit. Consequently, we define the value of the game as the least penalty that a winning strategy can incur (in the limit). In order to decide this value, we reduce the value problem to the value problem for games whose objective is a combination of a parity objective and a mean-payoff objective. Finally, we show that, even though the resulting game is exponentially larger, we can decide the value problem for both kinds of games in coNP.

Classifying Regular Languages via Cascade Products of Automata

Freitag, 24. September 2010, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Marcus Gelderie
RWTH Aachen University


In the structure theory of finite automata there are few prominent results on decomposing automata into prime factors. One example of such a decomposition is the Krohn-Rhodes theorem, which states that every finite automaton is covered by a cascade product of two-state reset automata and permutation automata. We investigate how classes of regular languages can be characterized in terms of the decomposition of minimal automata for languages in that class. More specifically we consider the case of piecewise testable, R-trivial and commutative languages. Considering R-trivial and piecewise testable languages we introduce the notion of a biased reset automaton. We show that language is R-trivial if and only if its minimal automaton is covered by a cascade product of biased two-state resets. In the case of piecewise testable languages we need to further restrict how the automata in the cascade react to the states of the automata preceding them in order to obtain a characterization. This leads us to the notion of locally i-triggered cascade products, which we use to characterize piecewise testable languages. Commutative languages are characterized as a direct product of cascade products of biased resets and cascade products of simple cyclic grouplike automata. Finally, we introduce the scope of a cascade product as a measure of locality in the cascade. We show that every R-trivial language can be recognized by a cascade product of scope 1.

Iterierte Regret-Minimierung in Spielen auf Graphen

Donnerstag, 30. September 2010, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Daniel Franzen
RWTH Aachen University


Am Donnerstag 30.September, 11 Uhr im Seminarraum i7, wird Daniel Franzen seine Bachelor-Arbeit "Iterierte Regret-Minimierung in Spielen auf Graphen" vorstellen.

In der Arbeit wollen wir uns mit einem Lösungskonzept für Spiele beschäftigen: mit der Regret-Minimierungen. Dieses Konzept ist auf Normalformspielen schon eingeführt und untersucht. Auf die Definitionen in Normalformspielen gehen wir kurz ein. Der Hauptteil wird sich aber mit der Erweiterung dieses Konzeptes auf Graphspiele beschäftigen. Wir betrachten vor Allem Erreichbarkeitsspiele auf Graphen. Dort definieren wir den Regret, weisen die Wohldefiniertheit und die Existenz von Strategien mit minimalem Regret nach und geben einen Algorithmus an um den Regret zu berechnen. Ein weiterer Algorithmus wird diese Regret-Minimierung iterieren. Andere kurz betrachtete Spiele sind Spiele mit qualitativer Gewinnbedingung und Sicherheitsspiele. Für diese steht der Nutzen und die konsistente Definierbarkeit des Konzeptes im Vordergrund.