Séminaires
Séminaire du 7 Décembre 2012
Lieu
LACL (salle des thèse, bâtiment P, faculté des sciences & Technologie): comment y aller
Programme
14h00-15h00: Emmanuel Fillot, LACL, "Exploiting Structure in LTL Synthesis"
Abstract: 
The aim of program synthesis is to automatically generate a program that satisfies a given specification, in contrast to program verification, for which both the specification and the program are given as input. The underlying goal is to improve program reliability and optimize design constraints, like time and human errors, and to get rid of the low-level programming tasks, by replacing them with the design of high-level specifications. The old dream of automatic synthesis, which among others was shared by Church, is difficult to realize for general-purpose programming languages. However in recent years, there has been a renewed interest in feasible methods for the synthesis of application specific programs, which have been, for instance, applied to reactive systems, distributed systems, programs manipulating arithmetic or concurrent data-structures.
Reactive systems are non-terminating programs that continuously interact with their environment. They arise both as hardware and software, and are usually part of safety-critical systems, for example microprocessors, air traffic controllers, programs to monitor medical devices, or nuclear plants. It is therefore crucial to guarantee their correctness. The temporal logic LTL is a very important abstract formalism to describe properties of reactive systems. As shown by Pnueli and Rosner in 89, the synthesis of reactive systems from LTL specifications is a 2-Exptime complete problem.
In this talk, I will present recent progresses in LTL synthesis based on a bounded synthesis approach inspired by bounded model-checking, and show that the high worst-case time complexity of LTL synthesis does not handicap its practical feasibility. This is achieved by exploiting the structure underlying the automata constructions used to solve the synthesis problem.
15h00-15h30 : Etienne Renault, LIP6/LRDE, "Strength-based decomposition of the property Büchi automaton for faster model-checking"
Abstract: The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton.
When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm.
Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers