Difference between revisions of "Jobs/PHD 2019 LDL"
From LRDE
m |
|||
| (5 intermediate revisions by one other user not shown) | |||
| Line 2: | Line 2: | ||
|Reference id=PHD_2019_LDL |
|Reference id=PHD_2019_LDL |
||
|Title=Traduction de logique dynamique linéaire en ω-automates |
|Title=Traduction de logique dynamique linéaire en ω-automates |
||
| + | |Dates=2019 |
||
| − | |Research field=automates, logique temporelle, model checking, vérification formelle |
||
| + | |Research field=Automates et vérification |
||
|Related project=Spot |
|Related project=Spot |
||
| − | |Advisor=Alexandre Duret-Lutz, Adrien Pommellet |
+ | |Advisor=[https://www.lrde.epita.fr/~adl Alexandre Duret-Lutz], [https://www.lrde.epita.fr/~adrien Adrien Pommellet] |
|General presentation of the field=Différentes techniques de vérification formelle utilisent des formules |
|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 |
de logique temporelle pour spécifier des comportements attendus. Par |
||
| Line 15: | Line 16: | ||
Les applications d'une telle transformation sont nombreuses: model |
Les applications d'une telle transformation sont nombreuses: model |
||
checking, synthèse de contrôleur, génération de tests, etc. |
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, |
|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 |
mais à des logiques un peu plus expressives : LDL (linear dynamic |
||
| Line 30: | Line 32: | ||
en ω-automates réputés, ainsi qu'un support partiel de la logique PSL. |
en ω-automates réputés, ainsi qu'un support partiel de la logique PSL. |
||
|References=* Spot: https://spot.lrde.epita.fr/ |
|References=* Spot: https://spot.lrde.epita.fr/ |
||
| − | + | * LDL: https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf (attention, la sémantique de LDL y est donnée sur des mots finis, alors que nous travaillerons sur des mots infinis). |
|
| − | + | * PSL: https://fr.wikipedia.org/wiki/Property_Specification_Language |
|
|Contact=adl@lrde.epita.fr |
|Contact=adl@lrde.epita.fr |
||
|Compensation=environ 1750 euros nets/mois pendant 36 mois |
|Compensation=environ 1750 euros nets/mois pendant 36 mois |
||
|Type=PhD position |
|Type=PhD position |
||
| − | |Language= |
+ | |Language=en |
|Published=Yes |
|Published=Yes |
||
}} |
}} |
||
Latest revision as of 15:38, 5 July 2019
| 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 |