Bonjour,
nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE.
Il aura lieu le mercredi 24 janvier 2018 à partir de 14h00 en L7 au LRDE (KB).
Les étudiants ING3 présenteront le résultat de leurs travaux des derniers
mois.
Au programme :
SPOT — BIBLIOTHEQUE DE MODEL CHECKING
14h00 : Traduction efficace de formules
LTL d’équité en automates déterministes – LAURENT XU
En vérification formelle de la logique temporelle linéaire (LTL)
à l’aide d’!-automates, la négation d’une formule LTL est traduite
en !-automate. La construction d’un automate plus petit
réduit beaucoup le temps d’exécution et la consommation mémoire
des opérations suivantes de la chaîne de traitement de
la vérification formelle. Müller et Sickert ont présenté une méthode
efficace pour traduire n’importe quelle formule LTL en
un petit automate déterministe. Cette méthode consiste à découper
la formule en trois ensembles de sous-formules qui appartiennent
respectivement au fragment de sureté ou de garantie,
au fragment d’équité et au reste. Ils traduisent ensuite individuellement
ces ensembles de sous-formules en automates
déterministes qu’ils combinent par la suite. Spot peut déjà traduire
les formules d’obligation en automates déterministes minimaux.
Les formules d’obligation étant un surensemble des
formules de sureté et de garantie, on généralise la traduction
de Müller et Sickert en remplaçant le fragment de sureté ou
de garantie par le fragment d’obligation. En ce qui concerne
le fragment d’équité, ils ont présenté un algorithme de traduction
efficace qui produit de petits automates déterministes. Ils
ont également présenté comment construire efficacement un
produit de ces automates avec d’autres automates. Nous présentons
comment nous implémentons ces deux méthodes dans
Spot.
14h30 : Tester l’appartenance à Persistence
ou Récurrence dans Spot – ALEXANDRE GBAGUIDI AÏSSE
Il existe une hiérarchie de propriétés temporelles, définie par
Manna et Pnueli (1990). Cette hiérarchie contient entre autres
les classes de récurrence et persistence. Savoir si une formule
de logique temporelle à temps linéaire (LTL) f est récurrente
(respectivement persistente) est intéressant car cela guarantit
que f peut être traduit en un automate de Büchi déterministe
(respectivement en un automate de co-Büchi). Auparavant,
Spot, une bibliothèque de manipulation de formules LTL
avait une unique façon de tester l’appartenance d’une formule
aux classes de persistence ou récurrence. Grâce à nos précédents
travaux présentés dans A co-Büching Toolbox, Spot a désormais
deux façons de procéder. Nous avons comparé et amélioré
ces deux méthodes en matière de temps d’exécution.
15h00 : Approches incrémentales pour la
synthèse de contrôleur – THIBAUD MICHAUD
Nous proposons deux approches incrémentales pour le problème
de la synthèse de contrôleur à partir de spécifications en
logique temporelle. Dans un travail antérieur, nous avons decrit
notre implémentation d’un outil de synthèse de contrôleur
reposant sur la réductibilité du problème à la résolution d’un
jeu à parité, et avons établi que l’étape la plus coûteuse était
la déterminisation d’un !-automate. Nous décrivons maintenant
deux approches pour mitiger le problème : l’une est basée
sur les automates good-for-games, et l’autre restreint les actions
du contrôleur afin de simplifier la déterminisation. Nos expérimentations
montrent que la deuxième approche est bien plus
prometteuse que la première.
Attention : le LRDE a déménagé, il se trouve au 24 rue Pasteur, 2e étage,
au fond de la cour Pasteur (
https://www.lrde.epita.fr/wiki/Contact).
--
Daniela Becker
Responsable administrative du LRDE