LIP6, salle 25-26/105. Instructions pour venir ici.
Abstract : 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).
Abstract : We study networks of processes that all execute the same finite protocol and communicate synchronously in two different ways: a process can broadcast one message to all other processes or send it to at most one other process. In both cases, if no process can receive the message, it will still be sent. We establish a precise complexity class for two coverability problems with a parameterised number of processes: the state coverability problem and the configuration coverability problem. It is already known that these problems are Ackermann-hard (but decidable) in the general case. We show that when the protocol is Wait-Only, i.e., it has no state from which a process can send and receive messages, the complexity drops to P and PSpace, respectively.