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

Synthesis of Recursive Programs

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

 Martin Lange
Date
Le mardi 24 mars 2015 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Martin Lange (University of Kassel)

Temporal logics are widely used in the specification and verification of reactive and concurrent systems for the purpose of building correct systems. Verification through model checking for instance is used to prove that a system, constructed in a possibly faulty way, satisfies a formal specification. Synthesis aims at eliminating errors in the construction phase already: a system (model) should automatically be derived from the formal specification such that satisfaction is guaranteed. Synthesis is therefore closely related to a logic's satisfiability problem: apart from deciding whether a formula has a model, such a model should also be returned.

In this talk we will present a generic game-theoretic approach to the satisfiability problems for various temporal logics. Typical known logics that can be embedded into MSO have the finite model property though, i.e. synthesis for these logics is restricted to finite models only. In order to create the theoretical foundations for synthesis of infinite-state systems like recursive programs for instance it is necessary to consider temporal logics beyond MSO that do not have the finite model property. There is only a narrow gap between the finite model property on one side and undecidability on the other. A family of temporal specification languages in this corridor - therefore suitable for such synthesis purposes - is obtained by enriching classical temporal logics with visibly pushdown languages.


À 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