Nir Piterman (University of Leicester)
Thursday, 29.12.2011, 09:30
In this talk I give a short introduction to the process of synthesis,
the automatic production of designs from their specifications.
We are interested in reactive systems, systems that continuously
interact with other programs, users, or their
environment and specifications in linear temporal logic.
Classical solutions to synthesis use either two player
games or tree automata.
We give a short introduction to the technique of using two player
games for synthesis and how to solve such games.
The classical solution to synthesis requires the usage of
deterministic automata. This solution is 2EXPTIME-complete, is quite
complicated, and does not work well in practice.
We suggest a syntactic approach that restricts the kind of
properties users are allowed to write.
We claim that this approach is general enough and can be extended to
cover most properties written in practice.
The main advantage of our approach is that it is tailored to the use of
BDDs and uses the structure of given properties to handle them more
We discuss how to extend our approach to handle more general properties
and mention future directions.
Finally, we give a few examples of applications from hardware design,
model-driven development, and robot control.