Safety slicing Petri nets

Abstract

We define a safety slice as a subnet of a marked Petri net ∑ that approximates ∑'s temporal behavior with respect to a set of interesting places Crit. This safety slice can be used to verify and falsify stutter-invariant linear-time safety properties when Crit is the set of places referred to by the safety property. By construction it is guaranteed that the safety slice's state space is at most as big as that of the original net. Results on a benchmark set demonstrate effective reductions on several net instances. Therefore safety slicing as a net preprocessing step may achieve an acceleration for model checking stutter-invariant linear-time safety properties. © 2012 Springer-Verlag.