We propose an automated procedure to prove polyhedral abstractions for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In …
This paper takes you behind the scenes of the Model Checking Contest (MCC), an annual competition focusing on the behavioral analysis of asynchronous systems using state-space exploration and model checking techniques. The MCC is part of a thriving …
The concurrent places of a Petri net are all pairs of places that may simultaneously have a token in some reachable marking. Concurrent places generalize the usual notion of dead places and are particularly useful for decomposing a Petri net into …
We propose a new method that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. Our approach relies on a state space abstraction, called polyhedral abstraction, which involves a …
We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability property …