Une approche polyédrique pour la vérification SMT de réseaux de Petri

Abstract

Nous définissons une méthode pour tirer parti des réductions de réseaux de Petri en combinaison avec des méthodes de vérification SMT. Nous prouvons la correction de cette méthode en utilisant une nouvelle notion d’équivalence entre les réseaux que nous appelons abstraction polyédrique. Notre approche a été implantée dans un outil, nommé SMPT, qui fournit deux procédures principales : Bounded Model Checking (BMC) et Property Directed Reachability (PDR). Chaque procédure a été adaptée afin d’utiliser des réductions et de travailler avec des réseaux de Petri généraux. Nous avons testé SMPT sur un ensemble d’instances issues de l’édition 2020 du Model Checking Contest. Nos résultats expérimentaux montrent que notre approche fonctionne bien, même lorsque nous n’avons qu’une quantité modérée de réductions.