A polyhedral framework for reachability problems in Petri Nets

Un cadre polyédrique pour les problèmes d'accessibilité dans les réseaux de Petri Nous proposons une méthode, appelée réduction polyédrique, pour accélérer la vérification de problèmes d'accessibilité sur les réseaux de Petri basée sur des réductions structurelles. Notre approche repose sur une abstraction de l'espace d'état qui combine réductions structurelles et contraintes arithmétiques sur le marquage des places.La correction de cette méthode est basée sur une nouvelle notion d'équivalence entre réseaux. Combinée avec un vérificateur de modèles basé SMT, nous montrons comment transformer un problème d'accessibilité sur un certain réseau de Petri, en la vérification d'une propriété équivalente sur une version réduite de ce réseau. Nous proposons également une procédure automatique pour prouver qu'une telle abstraction est correcte, en exploitant une connexion avec une classe de réseaux de Petri qui ont un ensemble d'accessibilité définissable par l'arithmétique de Presburger.De plus, nous présentons une nouvelle structure de données, appelée Token Flow Graph (TFG), qui capture la structure particulière des contraintes résultant des réductions structurelles. Nous exploitons les TFGs pour résoudre efficacement deux problèmes. Premièrement, pour éliminer les quantificateurs, qui apparaissent lors de notre transformation, dans la formule mise à jour à vérifier sur le réseau réduit. Deuxièmement, pour le calcul de la relation de concurrence d'un réseau, c'est-à-dire énumérer toutes les paires de places qui peuvent être marquées simultanément dans un marquage accessible.Nous appliquons notre approche à plusieurs procédures de vérification symboliques, et nous introduisons une nouvelle procédure de semi-décision pour la vérification des propriétés d'accessibilité sur les réseaux de Petri, basée sur la méthode Property Directed Reachability (PDR). La particularité de cette méthode PDR réside dans sa capacité à générer des certificats de verdict qui peuvent être vérifiés à l'aide d'un résolveur SMT externe.Notre approche et nos algorithmes sont implémentés dans quatre outils open-source : SMPT pour vérifier des propriétés d'accessibilité; Kong pour accélérer le calcul de places concurrentes; Octant pour l'élimination de quantificateurs; et enfin Reductron pour prouver automatiquement la correction de réductions polyédriques. Nous donnons des résultats expérimentaux sur leur efficacité, à la fois pour les réseaux bornés et non bornés, en utilisant les modèles et formules fournis par le Model Checking Contest. Nous mettons l'accent sur la reproductibilité de nos résultats et fournissons un artefact couvrant l'ensemble de nos expérimentations.