Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Exploiting Structure in LTL Synthesis

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Emmanuel Filiot
Date
Le mardi 06 mars 2012 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Emmanuel Filiot (Université Libre de Bruxelles)

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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents