Stubborn Sets for Priority Nets

Partial order methods, such as the stubborn set method and the priority method, reduce verification effort by exploiting irrelevant orders of events. We show how the stubborn set method can be applied to priority nets. By applicability we mean that for a given priority net, the stubborn set method constructs a reduced reachability graph that sufficiently represents the full reachability graph of the priority net. This work can also be considered as a combination of the stubborn set method and the priority method, to be used in “complete or moderated incomplete” verification when the original models are unprioritised nets.

• Type: Conference
• Year: 2004
• Where: ISCIS
• Authors: Kimmo Varpaaniemi
• Keywords: ISCIS 2004, Priority Method, Priority Net, Stubborn Set Method