LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Synthesis of Recursive Programs
- Date
- Tuesday, March 24 2015 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.