Affiliations: Institute of Computer Science, Polish Academy of Sciences, Ordona 21, 01-237 Warsaw, Poland. {meski,penczek}@ipipan.waw.pl | University of Łódź, FMCS, Banacha 22, 90-238 Łódź, Poland. polrola@wmi.uni.lodz.pl
Note: [] Address for correspondence: Institute of Computer Science, Polish Academy of Sciences, Ordona 21, 01-237 Warsaw, Poland Also affiliated with: University of Łódź, FMCS, Banacha 22, 90-238 Łódź, Poland
Note: [] Also affiliated with: Institute of Informatics, University of Natural Sciences and Humanities, 3 Maja 54, 08-110 Siedlce, Poland
Abstract: 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.
