Arbeitsgemeinschaft Logik und Automaten

Vorträge im Sommersemester 2011

State of Buechi Complementation

Montag, 04. April 2011, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Ming-Hsien Tsai
National Taiwan University

Zusammenfassung:

Buechi complementation has been studied for five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. For the performance of these approaches, there have been several complexity analyses but very few experimental results. What especially lacks is a comparative experiment on all the four approaches to see how they perform in practice.

In this talk, I will review the state of Buechi complementation, propose several optimization heuristics, and perform comparative experimentation on the four approaches. The experimental results show that the determinization-based Safra-Piterman construction outperforms the other three and our heuristics substantially improve the Safra-Piterman construction and the slice-based construction.

GOAL for Learning and Researching Omega-Automata and Temporal Logic

Dienstag, 05. April 2011, 16:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Yih-Kuen Tsay
National Taiwan University

Zusammenfassung:

Omega-automata, in particular Buechi automata, and linear temporal logic are closely related and have long served as fundamental building blocks of linear-time model checking. Understanding their relation is instrumental in discovering algorithmic solutions to model checking problems or simply in using those solutions, e.g., specifying a temporal property directly by an automaton rather than a temporal formula so that the property can be verified by an algorithm that operates on automata.

In this talk, I will introduce GOAL (http://goal.im.ntu.edu.tw/), a graphical interactive tool for defining and manipulating Buechi automata and temporal logic formulae. It also partially supports other variants of omega-automata. One main function of the GOAL tool is translation of a temporal formula into an equivalent Buechi automaton that can be further manipulated visually. The tool also provides various standard operations and tests on Buechi automata, in particular the equivalence test. The GOAL tool can be used for educational purposes, helping the user get a better understanding of how Buechi automata work and how they are related to linear temporal logics. It may also be used to construct correct and smaller specification automata, supplementing model checkers such as SPIN that adopt the automata-theoretic approach. GOAL includes a large number of translation and Buechi complementation algorithms. Most functions of GOAL can be accessed by programs or scripts, making it convenient for supporting research. Several use cases will be elaborated in the talk to show how GOAL may be used to facilitate the learning and research of omega-automata and linear temporal logic.

Buechi Store: An Open Repository of Buechi Automata

Dienstag, 05. April 2011, 16:30 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Yih-Kuen Tsay
National Taiwan University

Zusammenfassung:

Buechi automata are finite automata operating on infinite words. In the automata-theoretic approach, model checking boils down to testing emptiness of the intersection of two Buechi automata, the first modeling the system while the second representing all behaviors not permitted by a temporal specification formula. In general, for a given system, the smaller the specification automaton is, the faster the model checking task may be completed.

In this talk, I will introduce the Buechi Store (http://buchi.im.ntu.edu.tw/), an open repository of Buechi automata for model checking practice, research, and education. The repository contains Buechi automata and their complements for common specification patterns and numerous temporal formulae. These automata are made as small as possible by various construction techniques, in view that smaller automata are easier to understand and often help in speeding up the model checking process. The repository is open, allowing the user to add new automata or smaller ones that are equivalent to some existing automaton. Such a collection of Buechi automata is also useful as benchmark cases for evaluating translation or complementation algorithms and as examples for teaching or learning Buechi automata and temporal logic.

On the Impact and Perspectives of Buechi's Work - Some Personal Impressions

Mittwoch, 06. April 2011, 11:30 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Wolfgang Thomas
RWTH Aachen University

Zusammenfassung:

Richard Buechi was one of the most influential pioneers of automata theory. In this talk an outline of his life and work is given, and remarks are added on his writing, opinions, and visions.

Buechi was of Swiss citizenship; after obtaining his doctoral degree he worked in the US. Last week the Swiss Society of Logic and Philosophy of Science organized a colloquium titled "The Posterity of Buechi". A slightly shortened edition of the introductory talk of this colloquium will be presented in the seminar.

Exponential lower bounds for determined game policy iteration and linear program simplex methods

Freitag, 15. April 2011, 11:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Oliver Friedmann
LMU München

Zusammenfassung:

Policy iteration is one of the most important algorithmic schemes for solving problems in the domain of determined game theory such as parity games, stochastic games and Markov decision processes, and many more. It is parameterized by an improvement rule that determines how to proceed in the iteration from one policy to the next. It is a major open problem whether there is an improvement rule that results in a polynomial time algorithm for solving one of the considered (two-player) game classes. Simplex algorithms for solving linear programs are closely related to policy iteration algorithms. Like policy iteration, the simplex algorithm is parameterized by a so-called pivoting rule that describes how to proceed from one basic feasible solution in the linear program to the next. Also, it is a major open problem whether there is a pivoting rule that results in a (strongly) polynomial time algorithm for solving linear programs. We describe our recent construction for parity games that give rise to an exponential lower bounds for the Random Facet improvement rule, and how to extend the lower bound to more expressive game classes like stochastic games. We show that our construction for parity games can be translated to Markov decision processes, transferring our lower bound to their domain, and finally show how the lower bounds for the MDPs can be transferred to the linear programming domain, solving problems that have been open for several decades. We briefly address lower bound constructions for other pivoting rules if we still have time.

Minimal Models and Fixed-Points

Freitag, 13. May 2011, 12:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Francicleber Martins Ferreira
Federal University of Ceará / RWTH Aachen University

Zusammenfassung:

We study model-theoretic properties of logics which use the concepts of minimal models and fixed-points. We give a proof that the Löwenheim-Skolem theorem does not hold for Circumscription. We address a definability problem posed by Doyle and show that, whenever a circumscription is equivalent to an FO theory and implicitly defines the circumscribed predicate, then such circumscription can be replaced by the original theory plus a suitable explicit definition for the circumscribed symbol. We also study the MIN(FO) logic introduced by van Benthem, which is equivalent to LFP. We consider two extensions MIN^i and MIN^u which have operators able to define the intersection and the unions of the minimal models of a formula, respectively. We show that these two logics and SO have the same expressive power. Finally, we extend the proof of the Löwenheim-Skolem theorem for LFP given by Flum and Grädel and show that any infinite LPF theory of cardinality k has a model of cardinality at most k.

Logics with guarded negation

Donnerstag, 18. August 2011, 14:00 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Malte Milatz
RWTH Aachen University

Zusammenfassung:

Guarded logics play a major role in the search of "well-behaved" fragments of first-order logic or least fixed-point logic. Guarded negation logic (GN) is a proper extension of the guarded fragment and has recently been shown to be decidable for satisfiability. A suitable fixed-point extension, µGN, is still decidable for both satisfiability and finite satisfiability. We study the notions of bisimulation that are associated with these logics. Appealing to the game formulation of those bisimulation methods, we show that µGN^m, the set of µGN formulae of width at most m, is the GN^m-bisimulation-invariant fragment of guarded second-order logic.

Komplexität von Logiken mit Teamsemantik

Mittwoch, 14. September 2011, 11:15 Uhr, Seminarraum Informatik 7 (Raum 4116)

  Eugen Stoll
RWTH Aachen University