In: IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science, Vol. E78-A, No. 11, pages 1479-1486. 1995.
Abstract: The symbolic model checking algorithm was proposed for the efficient verification of sequential circuits. This paper shows that this algorithm is applicable to the verification of concurrent systems described by finite capacity Petri nets. In this algorithm, specifications of the system are given in the form of temporal logic formulas, and the algorithm checks whether these formulas hold in the state space. All logical operations are performed on binary decision diagrams. Since the algorithm does not enumerate each state, the problem of the state space explosion can be avided in many cases.
Keywords: concurrent systems, discrete event systems, symbolic model checking, system verification.