Design and verification of concurrent switching sequences with Petri nets

The authors show how dynamical and structural properties of Petri nets can be used in proving important assertions about integrated control systems with the aid of computers. Methods of reducing complexity with Petri-net specifications are illustrated. To exploit analysis features, precise meanings must be given to the net entities, which leads to the choice of conditions/events (C/E) nets. Boundness is the first decidable property that allows proof of liveness and also the C/E nature for the nets. However, because this property demands an exponential algorithm, previous reduction must be done to preserve meaning. This preservation allows interpretation of the structural relations which can be proved for Petri nets. A tightly coupled set of automatic switching sequences is modeled and verified with Petri nets, specifying nontrivial bus and transformer operations in distribution substations