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