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. |
We propose and study a method to accelerate the verification of reachability problems in Petri nets based on structural reductions. This approach, that we call polyhedral reduction, relies on a state space abstraction that combines structural reductions and linear arithmetic constraints on the marking of places.
The correctness of this method is based on a new notion of equivalence between nets. Combined with an SMT-based model checker, one can transform a reachability problem about some Petri net, into the verification of an equivalent reachability property on a reduced version of this net. We also propose an automated procedure to prove that such an abstraction is correct, exploiting a connection with a class of Petri nets with Presburger-definable reachability sets.
In addition, we present a data structure, called Token Flow Graph (TFG), that captures the particular structure of constraints stemming from structural reductions. We leverage TFGs to efficiently solve two problems. First, to eliminate quantifiers that appear during our transformation, in the updated formula to be checked on the reduced net. Second, to compute the concurrency relation of a net, that is all pairs of places that can be marked simultaneously in some reachable marking.
We apply our approach to several symbolic model checking procedures and introduce a new semi-decision procedure for checking reachability properties in Petri nets based on the Property Directed Reachability (PDR) method. A distinctive feature of this PDR method is its ability to generate verdict certificates that can be verified using an external SMT solver.
Our approach and algorithms are implemented in four open-source tools: SMPT for checking reachability properties; Kong for accelerating the computation of concurrent places; Octant for eliminating quantifiers; and Reductron for automatically proving the correctness of polyhedral reductions. We give experimental results about their effectiveness, both for bounded and unbounded nets, using a large benchmark provided by the Model Checking Contest. We focus on the reproducibility of our results and provide an accompanying artifact that covers all our experiments. |