Arbeitsgemeinschaft Logik und Automaten

Vorträge im Sommersemester 2004

Different Automatic Presentations of Certain String Structures.

30.9.2004 14 Uhr
Vince Bárány, RWTH Aachen

Zusammenfassung:

Proving non-automaticity of structures is a delicate art. Alternatively, one may find a form of self-expression in the act of constructing ever new automatic presentations of a given structure. In doing this, one is only limited by the so called intrinsic properties of the structure: those invariant under any automatic representation. The three aforementioned disciplines: proving non-automaticity, constructing different automatic presen- tations, and identifying intrinsic properties are not surprisingly strongly interconnected, as I will demonstrate on a few examples.

As to the automatic presentations of the binary tree with prefix and equal length relations, a complete and simple characterisation will be given.

I will also exhibit a slightly more unexpected connection to proving decidability of the MSO theory of word structures involved, and relate it to that of the morphic words.

A Hierarchy for Automatic Structures

23.9.2004 14 Uhr
Thomas Colcombet, IRISA Rennes

Zusammenfassung:

The Caucal hierarchy defines classes of structures of decidable monadic theory in a natural way. The level zero is the one of finite structures; level one contains prefix-recognizable structures; and by induction, more and more structures are introduced in each level. For structures having a decidable first-order theory, one knows the classes of [omega-][tree-]automatic structures. However, those families do not capture the Caucal hierarchy. And this from the second level. Hence, it is natural to try to describe families of automatic-like structures that would capture all the expresivity of the Caucal Hierachy.

We answer to this question in a simple way: one provides a family of structure transformations, called MSO-to-FO interpretations, which transform a structure of decidable monadic-theory into a structure of decidable first-order theory. Those transformations send exactly the class of prefix-recognizable structures to the class of omega-tree-automatic structures. By some refinement, one can also capture the other variants of automatic-like structures. When applied to a level n of the Caucal hierarchy, one describes by this way more complex families. It can be understood as constructing "automatic-like-structures of level n".

We then establish various simple results on those families of structures. We study their complexity, and deduce from this various strictness of the inclusions. We also provide a representation of those structures by means of equational systems. Finally, we show how, for each level of those families, a generator can be produced; i.e. a structure, in which any structure of the level can be interpreted in first-order.

Visibly Pushdown Games

6.8.2004 11.30 Uhr
Christof Löding, RWTH Aachen

Zusammenfassung:

The class of visibly pushdown languages has been recently defined by Alur and Madhusudan as a subclass of context-free languages with desirable closure properties and tractable decision problems. In their definition the input alphabet is partitioned into calls, internal actions, and returns. This partition determines whether the visibly pushdown automaton (VPA) reading an input letter pushes a symbol onto the stack (for a call), leaves the stack unchanged (for an internal action), or removes a symbol from the stack (for a return).

In this talk we consider visibly pushdown games, which are games played on visibly pushdown systems where the winning condition is given by a visibly pushdown language. We show that, unlike pushdown games with general pushdown winning conditions, visibly pushdown games are decidable. Furthermore, we establish the topological complexity of visibly pushdown languages by showing that they are a subclass of the Boolean closure of the third level of the Borel hierarchy.

I'm happy if you're happy!

8.7.2004 14 Uhr
Dietmar Berwanger, RWTH Aachen

Zusammenfassung:

Auf einer Klasse von Pfadspielen für mehrere Spieler mit LTL-Zielen untersuchen wir parasitäre Strategien. Eine solche Strategie bringt einen Spieler, der seinen Gewinn nicht selbständig sichern kann, doch noch an sein Ziel, unter der Annahme, dass die (Haupt-)Gewinner gemäß ihrer Gewinnstrategien spielen.

Dazu führen wir ein allgemeines Modell ein, in dem Spielverläufe aus elementaren Aktionen - Transitionen in einem Graphen - nach einem Flussdiagramm zusammengesetzt werden; das Flussdiagramm, wir nennen es Spektrum, spezifiziert also das Verhalten der Spieler unabhängig von dem Aktionsgraphen. Jede Partie erzeugt schliesslich einen unendlichen Pfad durch diesen Graphen und die Spieler, deren LTL-Ziel auf dem Pfad erfüllt wird, gewinnen.

Für Spiele mit endlichen Spektra auf endlichen Graphen zeigen wir zunächst, dass die zwei-Spieler Variante mit widersprüchlichen Gewinnbedingungen durch automatische Strategien determiniert ist. Anhand der automatentheoretischen Charakterisierung von Gewinnstrategien entwickeln wir dann ein Berechnungsverfahren für parasitäre Strategien.

Der Vortrag berichtet über eine gemeinsame Arbeit mit Christof Löding.

FO und MSO über hierarchisch definierten Graphen

1.7.2004 14 Uhr
Markus Lohrey, RWTH Aachen

Zusammenfassung:

Hierarchische Graphdefinitionen erlauben die modulare Beschreibung von Graphen mittels Modulen, welche wiederholt auftretende Teilstrukturen spezifizieren. Neben dieser Modularität können durch hierarchische Graphdefinitionen exponentielle Kompressionsraten erzielt werden. In vielen Fällen führt jedoch diese Datenkompression zu einer Zunahme der Berechnungskomplexität, wenn Eingabegraphen hierarchisch spezifiziert werden. Hierarchische Graphdefinitionen haben Anwendungen in vielen Bereichen der Informatik, wie z. B. Verifikation, Datenbanken, VLSI Design, etc.

In diesem Vortrag wird das model-checking Problem für Logik 1. Stufe (FO) und monadische Logik 2. Stufe auf hierarchisch definierten Eingabegraphen untersucht. Wir zeigen, dass im Allgemeinen diese Probleme exponentiell schwerer als die entsprechenden model-checking Probleme für explizit repräsentierte Graphen sind. Als Konsequenz erhalten wir neue vollständige Probleme für die Levels der Polynomialzeithierarchie und Exponentialzeithierarchie. Basierend auf klassischen Resultaten von Gaifman und Courcelle zeigen wir außerdem, dass unter gewissen strukturellen Einschränkungen effizientere Algorithmen möglich sind.

Die Ausdrucksstärke kommunizierender Automaten

24.6.2004 14 Uhr
Benedikt Bollig, RWTH Aachen

Zusammenfassung:

Ein kommunizierender Automat besteht aus einigen endlichen Automaten, die über unbeschränkte FIFO-Kanäle Nachrichten austauschen und auf diese Weise eine Menge von Kommunikationsszenarien bzw. Message Sequence Charts (MSCs) definieren. Wir zeigen, dass die Ausdrucksstärke kommunizierender Automaten dem existentiellen Fragment der MSO-Logik über MSCs entspricht. Außerdem wird sich herausstellen, dass die Alternierung der Quantoren zweiter Ordnung in der MSO-Logik über MSCs eine unendliche Hierarchie bildet. Wir können also schließen, dass die Klasse der von kommunizierenden Automaten erkannten MSC-Sprachen nicht unter Komplement abgeschlossen ist.

MSO-definierbare lokale temporale Logiken für Mazurkiewicz-Spuren

Mi, 12.5.2004 15 Uhr
Dietrich Kuske, TU Dresden

Zusammenfassung:

Temporale Logiken für Mazurkiewicz-Spuren sind in den vergangenen 15 Jahren ausführlich untersucht worden. Um für die Verifikation nutzbar zu sein, muss hierbei sichergestellt werden, dass das Erfüllbarkeits- und das Model Checking Problem in vertretbarer Komplexität gelöst werden können. Bisher wurden für alle neu eingeführten lokalen temporalen Logiken neue Beweise dafür angegeben, dass diese Probleme in PSPACE lösbar sind. Im Vortrag werde ich ein allgemeines Resultat herleiten, das auf alle bekannten (und viele weitere) lokale temporale Logiken anwendbar ist. Hierbei wird ein Zusammenhang zwischen der Komplexität der genannten Probleme und der Form der verwandten Modalitäten hergestellt werden.

Diese Ergebnisse wurden zusammen mit Paul Gastin (Paris) erreicht und z.T. auf CONCUR 2003 vorgestellt.

μ-Calculus Model Checking Algorithms for Low Alternation Depth

29.4.2004, 14 Uhr
Rafal Somla, Uppsala University

Zusammenfassung:

All known algorithms for checking whether a μ-calculus formula is true in a given transition system have complexity exponential in the alternation depth of the formula. However, it can be argued that we do not need more than two levels of alternation to express all properties we would ever like to verify. In particular, it is well known that logics LTL and CTL* can be encoded using μ-calculus formulas with at most one level of alternation. Hence it is interesting to develop efficient model checking algorithms for μ-calculus with bounded (and low) alternation depth.

We present model checking algorithms for the alternation free fragment of the μ-calculus and for the fragment with one level of alternation. The algorithms use the game based approach that is, they determine the winner of the corresponding model checking game. They exploit the special structure of the game graph for formulas with no or just one level of alternation. The algorithms were designed so that it is easy to distribute them among several processors to increase capacity of a model checker.

The time and space complexities of our algorithms are the same as for the best known general μ-calculus model checkers (when restricted to bounded alternation depth formulae). We will try to argue that exploiting the structure of the alternation bounded formulae in our algorithms in many cases may lead to improved performance.

Order Invariant Properties and Bounded Tree-width

22.4.2004, 14 Uhr
Luc Segoufin, INRIA France

Zusammenfassung:

On relational structures we consider properties definable in inv-FO(<). A linear order is available but the overall property should be independant from the linear order used.
Gurevich showed that it is possible to express this way strictly more properties than in pure FO. We conjecture that this is no longer the case over structures with bounded tree-width. As a first step towards this conjecture we will show that for ranked trees inv-FO(<) does collapse to FO.