Arbeitsgemeinschaft Logik und Automaten

Vorträge im Wintersemester 2006/07

Automatendefinierbare Relationen über Bäumen

Montag, 23.10.2006, 13.30 Uhr

  Frank Radmacher
RWTH Aachen

Zusammenfassung:

Automatendefinierbare Relationen über Wörtern sind weitgehend erforscht. Dort bilden erkennbare, automatische, deterministisch rationale und (nichtdeterministisch) rationale Relationen eine wohlbekannte Hierarchie.

Wir übertragen diese Klassen von Relationen auf Bäume. Wir untersuchen, wie wir auf natürliche Weise rationale Baumrelationen definieren können, so dass die von rationalen Wortrelationen vertrauten Eigenschaften erhalten bleiben.

Im Mittelpunkt stehen 'asynchrone Baumautomaten', ein neues Automatenmodell, welches gerade die rationalen Baumrelationen erkennt. Dieses Automatenmodell ermöglicht auch die Definition von deterministischen rationalen Baumrelationen.

Speicherreduktion fuer Strategien in unendlichen Spielen

Montag, 30.10.2006, 13.30 Uhr

  Michael Holtmann
RWTH Aachen

Zusammenfassung:

Unendliche Zwei-Personen-Spiele auf endlichen Graphen sind ein vielfaeltig verwendetes Modell fuer die Verifikation unendlicher Prozesse, z.B. von Protokollen, Controllern oder Betriebssystemen.

Ein Loesungsverfahren fuer diejenigen Spiele, bei denen nicht-positionale Strategien benoetigt werden, ist die sogenannte Spielreduktion. Dabei wird ein Speicher S eingefuehrt. Als neuer Spielgraph dient dann eine endliche Anzahl von Kopien des ursrpuenglichen Spielgraphen, wobei jede Kopie fuer ein Speicherelement steht. Die Gewinnbedingung wird hingegegen einfacher, so dass auf dem erweiterten Spielgraphen positionale Gewinnstrategien ausreichen. Aus der Loesung des resultierenden Spiels kann ein Strategieautomat zur Loesung des Ausgangsspiel konstruiert werden.

Wir stellen einen Algorithmus zur Reduktion des benoetigten Speichers vor. Die Idee ist, vor der Berechnung des Strategieautomaten die Anzahl der Knoten des erweiterten Spielgraphen so zu reduzieren, dass die Eigenschaften einer Spielreduktion erhalten bleiben. Dazu wird eine Aequivalenzrelation auf dem Speicher S mittels der Reduktion von omega- Automaten berechnet.

Unser Verfahren wenden wir auf Request-Response- und Staiger-Wagner Spiele an.

Sociable Interfaces: Theory, Implementation, and Future

Monday, 6th November 2006, 13h30

  Axel Legay
Université de Liège

Zusammenfassung:

Axel Legay, Luca de Alfaro, Marco Faella

Open systems are systems whose behavior is jointly determined by their internal structure, and by the inputs that they receive from their environment. A component of a larger system is, therefore, an open system, as its behavior depends on the inputs it receives from the other system components.

Since the last decades, various models have been introduce to model open systems. Among them one finds game-based models that represent the interaction between the behavior originating within a component, and the behavior originating from the component's environment as a game.

In this talk, I will first recall the basic advantages of using a game-based model for the specification, verification, composition, and refinement of open systems.

I will then introduce sociable interfaces, a recent concrete asynchronous game-based model where components have rich communication primitives that facilitate the modeling of software and distributed systems as well as global resources.

The Sociable Interfaces model has been implemented in a tool called TICC. I will describe the main features of TICC, and explain the difficulties of moving from the theoretical description of the model to its implementation.

Finally, I will discuss the possibility of adding time to the model.

Rewriting Systems over Unranked Trees – Reachability Problems

Monday, 13th November 2006, 13.30

  Alex. Spelten
RWTH Aachen

Zusammenfassung:

Finite graphs constitute an important tool in various fields of computer science. In order to transfer the theory of finite graphs at least partially to infinite systems, a finite representation of infinite systems is needed. Rewriting systems form a practical model for the finite representation of infinite graphs. Among attractive subclasses of rewriting systems is the class of ground tree rewriting systems over ranked trees, which is known to have good algorithmic properties.

We investigate these algorithmic properties for two kinds of rewriting systems over unranked trees.

For the first introduced rewriting formalism, we define a reduction to ranked (binary) trees via an encoding and also to standard ground tree rewriting, and we show that the generated classes of transition graphs coincide.

For the second introduced rewriting formalism over unranked trees using subtree rewriting combined with flat prefix rewriting, we obtain strictly more transition graphs, and we show that the reachability problem over such graphs is still decidable. Here, a flat prefix rewrite rule substitutes a prefix of the word derived from the front of a subtree of height 1.

However, as opposed to standard ground tree rewriting systems, this decidability result fails for both formalisms when the transition graphs are restricted by a deterministic top down tree automaton.

Algebraic Recognizability of Tree Languages

Thursday, 16th November 2006, 10.00

  Pascal Weil
LaBRI (CNRS and Université Bordeaux-1)

Zusammenfassung:

In this talk, trees are finite, ranked and ordered. It has been known since the 1960s that the central results of formal language theory (existence and uniqueness of a minimal automaton, equivalence of recognizability with monadic second-order logical definability) also hold for tree languages. However, the algebraic approach has remained elusive. This approach (which is so successful in the case of word languages) is interesting not only for aesthetic reasons, to unify and mathematize issues related with recognizability, but also because it provides tools to classify recognizable languages, and to decide membership in significant subclasses. First-order definable languages (specifically FO(<)) constitute a case in point. In the word (and the trace) case, this class of languages is decidable, and the decidability algorithm essentially depends on Schuetzenberger's theorem, that is, on the algebraic characterization of these languages. In contrast, FO(<) for tree languages is not yet known to be decidable.

There have been several attempts to algebrize the theory of tree languages, say, with the notions of the syntactic Sigma-algebra or the syntactic tree monoid of a tree language. These notions have however been disappointing. The notion of forest algebras, recently introduced by Bojanczyk and Walukiewicz (with additional contributions by Straubing), looks quite promising to deal with unranked, unordered trees. I will present another approach, developed together with Zoltan Esik (Szeged), based on the algebraic notion notion of preclones. I will show how the syntactic preclone of a recognizable tree language is naturally connected with its minimal automaton, how preclones generalize the notion of Sigma-algebra and tree monoids associated with a language. The main result is an algebraic characterization of FO(<) in terms of preclones. Whether this characterization may lead to a decision procedure is still an open problem.

Faster Algorithms for Finitary Games

Monday, 22nd January 2007, 13.30

  Florian Horn
LIAFA Paris

Zusammenfassung:

Automaten über unendlichen Alphabeten

Monday, 5th March 2007, 13.30

  Jonathan Heinen
RWTH Aachen

Zusammenfassung: