Bounded Model Checking Approaches for Verification of Distributed Time Petri Nets.
Artur Męski, Agata Półrola, Wojciech Penczek, Bożena Woźna-Szcześniak, Andrzej Zbrzezny · 2011
We consider two symbolic approaches to bounded model checking (BMC) of distributed time Petri nets (DTPNs). We focus on the properties expressed in Linear Temporal Logic without the neXt-time operator (LTL−X) and the existential fragment of Computation Tree Logic without the neXt-time operator (ECTL−X). We give a translation of BMC to SAT and describe a BDD-based BMC for both LTL−X and ECTL−X. The two translations have been implemented, tested, and compared with each other on two standard benchmarks. Our experimental results reveal the advantages and disadvantages of both the approaches.