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 | |
| Advisor | |
| 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 |