Difference between revisions of "Jobs/PHD 2019 LDL"

From LRDE

m
m
Line 5: Line 5:
 
|Research field=Automates et vérification
 
|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 34: Line 34:
 
* 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).
 
* 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
 
* PSL: https://fr.wikipedia.org/wiki/Property_Specification_Language
|Contact=adl@lrde.epita.fr
+
|Contact=[mailto:adl@lrde.epita.fr 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

Revision as of 14:36, 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

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

[mailto:adl@lrde.epita.fr adl@lrde.epita.fr]