Publicado em: 05/08/2010

Palestra sobre Síntese a partir de Especificações Temporais

Título: Synthesis From Temporal Specifications
Palestrante: Nir Piterman (http://www.doc.ic.ac.uk/~npiterma/)
Data: 6 de agosto
Hora: 14h
Local: Sala 109 do prédio 67 do INF

Abstract:
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.

Short-bio:

Nir Piterman completed his PhD at the Weizmann Institute of Science in 2005 working with Turing award winner Amir Pneuli. As a postdoctoral researcher in the Ecole Polytechnique Federal de Lausanne in Switzerland he improved the construction for determinization of automata on infinite words, the most fundamental construction for such automata, as well as other foundational results on two-player games and reactive systems’ synthesis. Recently, as a research associate in the department of computing in Imperial College London he worked on abstraction of probabilistic systems, suggesting the new framework of p-automata, a complete abstraction framework for model-checking discrete-time Markov chains. Dr Piterman is the author of more than 50 papers in formal verification, automata theory, model checking, temporal logic, design synthesis, two-player games, and the application of formal methods to biological modelling.

and mention future direction. Finally, we give a few examples of applications from hardware design, model-driven development, and robot control.

Joint work mostly with Amir Pnueli and Yaniv Sa’ar.