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 propose a new method for accelerating the computation of a concurrency relation, that is all pairs of places in a Petri net that can be marked together. Our approach relies on a state space abstraction, that involves a mix between structural …