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

• Autorzy: Męski A. , Penczek W. , Półrola A.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

bounded model checking; Petri net; 1-Safe Petri Nets; temporal logics LTL; set-theoretic characterisation of ECTL; binary decision diagrams

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 109, nr 3
• Strony: 305--321
• Opis fizyczny: Bibliogr. 20 poz., tab., wykr.

Twórcy

autor

Męski A.

autor

Penczek W.

autor

Półrola A.

• Institute of Computer Science, Polish Academy of Sciences, Ordona 21, 01-237Warsaw, Poland,

Bibliografia

• [1] P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In Proc. of the 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pages 411-425. Springer-Verlag, 2000.
• [2] N. Amla, R. Kurshan, K. McMillan, and R. Medel. Experimental analysis of different techniques for bounded model checking. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 34-48. Springer-Verlag, 2003.
• [3] B. Berthomieu, P-O. Ribet, and F. Vernadat. The tool TINA - construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research, 42(14), 2004.
• [4] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.
• [5] R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers, 35(8):677-691, 1986.
• [6] J. R. Burch, E. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142-170, 1990.
• [7] G. Cabodi, P. Camurati, and S. Quer. Can BDD compete with SAT solvers on bounded model checking? In Proc. of the 39th Design Automation Conference (DAC'02), pages 117-122, 2002.
• [8] G. Cabodi, S. Nocco, and S. Quer. Mixing forward and backward traversals in guided-prioritized BDD-based verification. In Proc. of the 14th Int. Conf. on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 471-484. Springer-Verlag, 2003.
• [9] G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: An efficient iteration strategy for symbolic state space generation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), volume 2031 of LNCS, pages 328-342. Springer-Verlag, 2001.
• [10] E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Proc. of the 6th Int. Conf. on Computer Aided Verification (CAV'94), volume 818 of LNCS, pages 415-427. Springer-Verlag, 1994.
• [11] F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of bounded model checking at an industrial setting. In Proc. of the 13th Int. Conf. on Computer Aided Verification (CAV'01), volume 2102 of LNCS, pages 436-453. Springer-Verlag, 2001.
• [12] M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2004.
• [13] A. Jones and A. Lomuscio. A BDD-based BMC approach for the verification of multi-agent systems. In L. Czaja, editor, Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'09), volume 1, pages 253-264. Warsaw University, 2009.
• [14] A. Miner and G. Ciardo. Efficient reachability set generation and storage using decision diagrams. In Proc. of the 20th Int. Conf. on Applications and Theory of Petri Nets (ICATPN'99), volume 1639 of LNCS, pages 6-25. Springer-Verlag, 1999.
• [15] J. Møller, J. Lichtenberg, H. Andersen, and H. Hulgaard. Difference Decision Diagrams. In Proc. of the 13th Int. Workshop Computer Science Logic (CSL'99), volume 1683 of LNCS, pages 111-125. Springer-Verlag, 1999.
• [16] W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.
• [17] W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [18] F. Somenzi. CUDD: CU decision diagram package - release 2.3.1. http://vlsi.colorado.edu/∼fabio/CUDD/cuddIntro.html.
• [19] O. Strichman. Tuning SAT checkers for bounded model checking. In Proc. of the 12th Int. Conf. on Computer Aided Verification (CAV'00), volume 1855 of LNCS, pages 480-494. Springer-Verlag, 2000.
• [20] A. J. Yu, G. Ciardo, and G. Luettgen. Decision-diagram-based techniques for bounded reachability checking of asynchronous systems. Software Tools for Technology Transfer, 11(2):117-131,