Skip to main content

Synthesis From Temporal Specifications

Nir Piterman ( University of Leicester )

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 efficiently. Finally, we survey recent applications in model-driven development and robot control.

Speaker bio

Nir Piterman is a Reader in the department of computer science in the university of Leicester. He completed his PhD in 2005 in the Weizmann Institute of Science under the supervision of Amir Pnueli. He was a postdoc in Tom Henzinger's group in the Ecoloe Polytechnique Federal de Lausanne between 2005-2007 and a research fellow in Imperial College London working with Michael Huth between 2007-2010. His research interests include formal verification and automata theory. He is working on model checking of various types of systems, different aspects of temporal logic, as well as synthesis and game solving. He is also working on applications of formal methods to biological modeling.

Share this: