My first contact with Prof. Schneider was during my doctoral
work at the University of Karlsruhe, which lasted from 2000 to
2005. During that time, he showed constant interest in my work,
which lead to several joint publications.
Being aware of my research results, Prof. Schneider invited me
to join the Reactive Systems Group from the 1st of March to
the 31st of August, 2006. During this period, I collaborated in
the excellence cluster Dependable Adaptive Systems and
Mathematical Modeling. Shortly before, Prof. Schneider and
Andreas Morgenstern had introduced
quantifying operators into the μ-calculus, and were asking
themselves whether their extensions could help in the synthesis of
controllers for Quartz programs. I was able to help them by
clarifying many aspects related to the translation of Mealy
automata into Kripke structures, as well as by describing the
interface between the controller and the system to be controlled.
I also realized that there was not only a single synthesis problem
involved, but actually there were three of them. The main result of
my work was to identify and to classify these problems, as well as to
present a solution to one of them, which can be computed using
the Averest tools developed
by the group.
