On Symbolic Model Checking in Petri Nets

概要

論文の詳細を見る
The symbolic model checking algorithm was proposed for the efficient verification of sequential circuits. In this paper, we show 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 enumerating each state, the problem of state space explosion can be avoided in many cases.
社団法人電子情報通信学会の論文
1995-11-25