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 …
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 an automated procedure to prove polyhedral abstractions for Petri nets. Polyhedral abstraction is a new type of state-space equivalence based on the use of linear integer constraints. Our approach relies on an encoding into a set of SMT …
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 …
Kong, the Koncurrent places Grinder, is a tool designed to compute the concurrency relation of a Petri net by taking advantage of structural reductions. The specificity of Kong is to rely on a state space abstraction, called polyhedral abstraction in …
We define a method for taking advantage of net reductions in combination with a SMT-based model checker. We prove the correctness of this method using a new notion of equivalence between nets that we call polyhedral abstraction. Our approach has been …