BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets
Artur Męski, Wojciech Penczek, Agata Półrola · Fundamenta Informaticae · 2011
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 whi