Mefosyloma
Le savoir est une arme !
Vendredi 7 juin 2024Yann THIERRY-MIEG (LIP6)
Nous abordons le problème de la vérification d'une nouvelle formule LTL phi sur un système S, phi |= S, "sachant que" K, où K est une connaissance a priori sur les comportements du système, e.g. une autre formule LTL déjà prouvée. Après une présentation sur le sens à donner aux "connaissances" au niveau langage sur des mots infinis, nous plongerons dans de nouvelles opérations permettant étant donné deux automates A_!phi et A_K de construire un automate B = A_phi |_K (se lit "sachant que", comme une proba conditionnelle), où B est plus "simple" que A_!phi (diverses métriques considérées) mais peut être utilisé pour le model-checking en lieu et place de A_!phi. Ces opérations sont implantées dans Spot, un outil de manipulation d'automates, et sont comparées sur un large benchmark issu du Model Checking Contest. Pour l'acquisition de connaissances nous proposons des approches pragmatiques basées sur une diversité de procédures de décision moins coûteuse que LTL (typiquement structurelles, exploitant du SMT) implantées au sein d'ITS-Tools, un model-checker portfolio, qui a remporté en 2023 la compétition (en partie) grâce à ces techniques. Présentation Yann thierry-Mieg, travail en commun avec Alexandre Duret-Lutz (LRE), Denis Poitrenaud (LIP6), Emmanuel Paviot-Adet (LIP6).
nathalie.sznajder (at) nulllip6.fr