In: Formal Methods in System Design, 2006. 2006. URL: http://dx.doi.org/10.1007/s10703-006-0006-1.
Abstract: This paper presents two stubborn set methods for alleviating the state explosion problem when reasoning about state properties. The first method makes it possible to determine whether a state of the system is reachable in which a given state predicate holds. The second method makes it possible to determine if from all reachable states it is possible to reach a state where a given state predicate holds. The novelty of the two methods is that they rely on so-called up sets and down sets rather than the notion of visible transitions which causes earlier methods to give only limited reduction of the state space, especially when considering state predicates referring to many of the state variables of the system. The suggested stubborn set methods have been implemented in the LoLA tool, and we report on some experimental results obtained with this computer tool together with some general guidance for applying the two question-guided stubborn set methods and their different implementations in verification. The two methods are presented in the context of Petri Nets, but are applicable also to other state and action oriented modelling formalisms for which the basic stubborn set theory is applicable.
Keywords: State space methods; State explosion problem; Stubborn set methods; Partial-order reduction; Petri nets.