BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets

摘要

In the paper we present a bounded model checking for 1 -safe Petri nets and properties expressed in LTL and the universal fragment of CTL, based on binary decision diagrams. The presented experimental results show that we have obtained a technique which performs better in some of the considered cases, in comparison with the existing SAT-based implementation. The results are also compared with standard BDD-based symbolic method.