Jobs/PHD 2019 LDL

From LRDE

Traduction de logique dynamique linéaire en ω-automates
Reference id

PHD_2019_LDL

Dates

2019

Research field

Automates et vérification

Related project

Spot

Advisor

Alexandre Duret-Lutz, Adrien Pommellet

General presentation of the field

Différentes techniques de vérification formelle utilisent des formules de logique temporelle pour spécifier des comportements attendus. Par exemple la logique temporelle à temps linéaire (LTL) augmente la logique booléenne classique en y ajoutant des opérateurs temporels tels que F(x) (dans le futur x sera vrai), G(x) (x est toujours vrai), ou x U y (x est vrai jusqu'à ce que y le soit). De telles formules sont ensuite traduites sous forme d'ω-automates, typiquement des automates de Büchi, avant de réaliser un processus de vérification. Les applications d'une telle transformation sont nombreuses: model checking, synthèse de contrôleur, génération de tests, etc.

Prerequisites

C++

Objectives

L'objectif de ce projet est de s'intéresser, non pas à la logique LTL, mais à des logiques un peu plus expressives : LDL (linear dynamic logique) et la partie linéaire de PSL (property specification language). Dans les deux cas, la logique est augmentée avec des expressions ω-régulières. Par ailleurs, on souhaite produire des ω-automates qui ne soient pas nécessairement des automates de Büchi ; par exemple certaines applications préfèrent travailler avec des automates à parité déterministes.

On souhaite développer les algorithmes pour effectuer ces traductions, et les implémenter dans la bibliothèque Spot. Aujourd'hui, Spot est une bibliothèque C++ mature pour la manipulation d'ω-automates et de formules de logique, on y trouve des algorithmes de traductions de LTL en ω-automates réputés, ainsi qu'un support partiel de la logique PSL.

Benefit for the candidate
References
Place LRDE: How to get to us
Compensation

environ 1750 euros nets/mois pendant 36 mois

Future work opportunities
Contact

adl@lrde.epita.fr