Efficient approach to symbolic state exploration of complex parallel controllers

In this paper a method based on the use of zero-suppressed BDDs (0-Sup-BDDs) to symbolic state space exploration of parallel controllers is presented. Unlike traditional methods, the new approach is based on the implicit manipulation of sets of states instead of the manipulation of their characteristic functions. A formal specification of the parallel controller is given in the form of an interpreted Petri net. Experimental results demonstrate that the proposed approach can successfully compete against the state of the art methods of state space exploration.