Arbeitsgemeinschaft Logik und Automaten

Vorträge im Wintersemester 2007/08

Conjunctive Query Containment over Trees

Monday, 5 November 2007, 13.00

  Wim Martens
Universität Dortmund

Zusammenfassung:

The complexity of containment and satisfiability of conjunctive queries over finite, unranked, labeled trees is studied with respect to the axes Child, NextSibling, their transitive and reflexive closures, and Following. When studying such queries over trees instead of general relations, the problem is quite different from what we are used to from traditional database theory. For the containment problem a trichotomy is presented, classifying the problems as in PTIME, coNP-complete, or Pi_2^P-complete. For the satisfiability problem most problems are classified as either in PTIME or NP-complete.

Modelchecking über Produktstrukturen

Dienstag, 20. November 2007, 15.00 Uhr

  Ingo Felscher
RWTH Aachen

Zusammenfassung:

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.

On the Descriptive Complexity of Linear Algebra

Monday, 17 December 2007, 14.00

  Anuj Dawar
University of Cambridge
Das Erreichbarkeitsproblem in randomisierten Sabotagespielen ist PSPACE-vollständig

Dienstag, 25. März 2008, 13:30 Uhr

Vortragender:   Dominik Klein
RWTH Aachen

Zusammenfassung:

Sabotagespiele sind Spielmodelle, die es ermöglichen, fehlerhafte, sich dynamisch verändernde Systeme zu modellieren. Ein Spieler ("Runner") zieht von Knoten zu Knoten in einem Multigraph. Sein Gegner ("Blocker") kann dabei nach jedem Zug eine Kante aus dem Graph löschen. Die Theorie dieser Spiele wurde am Lehrstuhl I7 von Christoph Löding und Philipp Rohde entwickelt; dort wurde u.a. auch die PSPACE-Vollständigkeit des Erreichbarkeitsproblems gezeigt.

Im Mittelpunkt des Interesses steht hier eine randomisierte Variante des Sabotagespiels, bei der der Spieler ("Runner") nicht mehr gegen einen zweiten Spieler spielt, sondern sich in einem zufällig verändernden Graph bewegt. Dort wird nach jedem Zug zufällig eine Kante mit gleicher Wahrscheinlichkeit ausgewählt und entfernt. Motiviert ist dieses Modell durch eine realistischere Abbildung von möglichen praktischen Szenarien.

Die Ergebnisse bezüglich des Sabotagespiels lassen sich größtenteils auf die randomisierte Variante übertragen; auch hier ist das Erreichbarkeitsproblem PSPACE-vollständig. Damit lässt sich das randomisierte Modell in die Komplexitätsklasse SAPTIME einordnen, wobei SAPTIME eine von Christos Papadimitriou definierte Charakterisierung von PSPACE ist, die auf der Analyse von Spielen gegen den Zufall (oder "gegen die Natur") basiert.