Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


Synthesis From Temporal Specifications

  • Speaker:   Dr  Nir Piterman  (Imperial College London)
  • Host:   Andrei Voronkov
  • 12th May 2010 at 14:15 in Lecture Theatre 1.4, Kilburn Building
In this talk we 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. 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 efficiently. We discuss how to extend our approach to handle more general properties and mention future direction. Finally, we give a few examples of applications from hardware design, model-driven development, and robot control.
▲ Up to the top