ON SYMBOLIC MODEL CHECKING IN PETRI NETS

The symbolic model checking algorithm was proposed for the efficient v erification of sequential circuits. In this paper, we show that this a lgorithm is applicable to the verification of concurrent systems descr ibed by finite capacity Petri nets. In this algorithm, specifications of the system are given in the form of temporal logic formulas, and th e algorithm checks whether these formulas hold in the state space. All logical operations are performed on Binary Decision Diagrams, Since t he algorithm does not enumerating each state, the problem of state spa ce explosion can be avoided in many cases.