Rüdiger Ehlers

Rüdiger Ehlers (Ph.D. Student) Reactive Systems Group Universität des Saarlandes Phone: +49 681 302 5606 Fax: +49 681 302 5636 eMail: ehlers at cs.uni-saarland.de Building: E 1.3 Room: 532

I am a Ph.D. student in the Reactive Systems Group at the Computer Science Department at Saarland University. My research interests are applied automata theory and in particular the automatic synthesis of finite-state systems.

Research

Automatic synthesis of finite state systems from specifications stated in some sort of temporal logic is an ambitious challenge. Despite the high complexities of the numerous variations of this problem, recent advances in its algorithmic solution have shown the potential of this approach. Two main lines of research can be identified in this context:

How can we make the approach scale better?

In [Ehl10a], generalized Rabin(1) synthesis is described, which is an extension to generalized reactivity(1) synthesis, originally developed by Piterman, Pnueli and Sa’ar. This extension allows the efficient encoding of the synthesis problem for specificiations with assumptions and guarantees having a Rabin index of one into five-colour parity games.

In [Ehl10d], a SAT-based technique for (fully) minimizing deterministic Büchi automata is presented. This allows the reduction of specification automata prior to their application in the generalized reactivity(1) context. The technique is easily extendable to Rabin automata and thus also useful for generalized Rabin(1) synthesis.

For some applications, the full power of linear-time temporal logic is required for stating the specification of the system to be constructed. One particularly interesting approach in this context if bounded synthesis, which in turn builds upon Safraless synthesis. In [Ehl10c], techniques for enabling this approach to work well with symbolic data structures are presented.

Which extensions to the problem that are useful in practice can be done without sacrificing the efficiency of synthesis procedures?

The value of synthesis tools is even higher if they do not only solve the basic synthesis problem, but also guarantee optimality of the solution with respect to some quality measure. One typical such measure is the number of states in a synthesized finite state machine (FSM). In [Ehl10b], it is shown that the size of a smallest FSM satisfying some specification is NP-hard to approximate within any polynomial even in case of closed synthesis, i.e., for systems without external non-determinism. This result even holds for pure safety objectives.

Publications

2012

2011

2010

Some suggestions for student projects

• Efficient symbolic representation of safety automata for synthesis and model checking