Finding a witness path for non-liveness in free-choice nets

Abstract

One of the disablers of structural Petri net verification techniques is the lack of diagnosis information that is easily understandable. In this article, we improve this situation for a particular technique: the siphon and trap based verification of liveness in free-choice nets. Instead of the information "there is a siphon without included marked trap", we exhibit an execution path that leads from the initial marking to a marking m* and a set of transitions that mutually block each other and are thus dead at m*. The latter information can be much more easily comprehended by non-experts in Petri net theory. We provide experimental results suggesting that our method is competitive to related state space techniques. © 2011 Springer-Verlag.