Arbeitsgemeinschaft Logik und Automaten

Vorträge im Wintersemester 2008/2009

Solving Infinite Games with Parameters

Freitag, 21st November 2008, 10.00

  Paul Hänsch
RWTH Aachen
Automaton-definable tree relations with cardinality constraints

Freitag, 21. November 2008, 10.45

  Nils Jansen
RWTH Aachen
Undecidability of the monadic theory of the real order: Ideas

Freitag, 21. November 2008, 11.45

  Ulrich Loup
RWTH Aachen
Formalsprachliche Lösungen für das Church'sche Problem der Controller-Synthese

Mittwoch, 3. Dezember 2008, 11.00

  Jörg Olschewski
RWTH Aachen
Das Komplementierungsproblem für Büchi-Automaten: Algorithmen und Implementierung

Mittwoch, 3. Dezember 2008, 11.45

  Andreas Roell
RWTH Aachen
Time-optimal Winning Strategies in Infinite Games

Mittwoch, 14. Januar 2009, 11:45 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Martin Zimmermann
RWTH Aachen


Infinite Games are an important tool in the synthesis of finite-state controllers for reactive systems. While classical optimization of synthesized controllers focused on the size of the automaton implementing a finite-state winning strategy, we investigate a different quality measure. Many winning conditions allow a natural definition of waiting times that reflect periods of waiting in the original system. We investigate time-optimal strategies for Request-Response Games, Poset Games - a novel type of infinite games that extend Request-Response Games, and games with winning conditions in Parametric Linear Temporal Logic. Here, the temporal operators of classical Temporal Logics can be subscribed with free variables, that represent bounds on the satisfaction. Then, one is interested in winning strategies with respect to optimal valuations of the free variables.

For Request-Response Games and Poset Games, we prove the existence of time-optimal finite-state winning strategies. For games with winning conditions in Parametric Linear Temporal Logic, we prove that optimal winning strategies are computable for solitary games.

The Computational Complexity of Probabilistic Networks

Donnerstag, 12. März 2009, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Johan Kwisthout
Universiteit Utrecht


Probabilistic networks (also called Bayesian or belief networks) represent a joint probability distribution on a set of statistical variables. A probabilistic network is often described by a directed acyclic graph and a set of conditional probabilities. The nodes represent the statistical variables, the arcs (or lack of them) represent (in)dependencies induced by the joint probability distribution. These networks are interesting also from a complexity-theoretical point of view: many problems related to these networks are complete for complexity classes that have few, if any, known "real world" complete problems.

In my thesis research, I investigated the complexity of a number of these problems. In my talk, I will present some background and sketch some of these complexity proofs. Furthermore, I will discuss my most recent work, which aims to establish lower bounds on the running time of inference algorithms for probabilistic networks, and which builds on Daniel Marx' Can you beat treewidth-paper (Foundations of Computer Science, 2007). Finally, I will place my results in a broader perspective: many problems, for example in AI, combine some sort of "selecting", "verifying", "enumerating" and "stochastic reasoning". These problems - inasmuch as their computational complexity has been studied - tend to be complete for classes in the Counting Hierarchy, like NP^PP, co-NP^PP, and P^PP^PP. An interesting question is, whether we can also characterize the power of such classes with other methods, like stochastic automata or stochastic parity games.

Lösung des Church'schen Problems mit kontextfreien Spezifikationen

Freitag, 20. März 2009, 12:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Wladimir Fridman
RWTH Aachen


Das Church'sche Problem der Kontrollersynthese fragt nach der Existenz und Konstruktion eines Automaten mit Output, der zu jeder Eingabefolge X eine Ausgabe Y produziert, so dass das Paar (X,Y) eine gegebene Spezifikation erfüllt. Wir befassen uns mit Spezifikationen, die durch kontextfreie omega-Sprachen gegeben sind. Hierzu werden verschiedene Modelle von Pushdown-Automaten betrachtet. Wir zeigen, dass das Church'sche Problem für Spezifikationen L in omega-DCFL (deterministische kontextfreie omega-Sprachen) und L in omega-VPL (Visibly Pushdown omega-Sprachen) entscheidbar ist und dass die Lösungen in DCFL und für die letzteren auch in VPL liegen. Für nichtdeterministische kontextfreie omega-Sprachen (L in omega-CFL) ist das Church'sche Problem unentscheidbar.