Improving the Translation from ECTL to SAT

• Autorzy: Zbrzezny, A.
• Języki publikacji: EN

Abstrakty

EN

The objective of this paper is to offer an improvement to the translation from ECTL to SAT introduced in [14] and show that the improvement proposed substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made preliminary experimental results, which demonstrate the efficiency of the method.

Słowa kluczowe

EN

ECTL; Existential Computation Tree Logic ECTL; bounded model checking; translation to SAT

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 513-531
• Opis fizyczny: bibliogr. 20 poz., tab.

Twórcy

autor

Zbrzezny, A.

• Institute of Mathematics and Computer Science, Jan Długosz University in Czestochowa,Armii Krajowej 13/15, 42-200 Częstochowa, Poland l,

Bibliografia

• [1] A. Biere, A. Cimatti, E. Clarke, M.Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of the ACM/IEEE Design Automation Conference (DAC'99), pages 317-320, 1999.
• [2] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [3] E.M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. Completeness and complexity of bounded model checking. In B. Steffen and G. Levi, editors, VMCAI, volume 2937 of Lecture Notes in Computer Science, pages 85-96. Springer, 2004.
• [4] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Wo´zna, and A. Zbrzezny. VerICS: A tool for verifying timed automata and Estelle specifications. 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 278-283. Springer-Verlag, 2003.
• [5] E.W. Dijkstra. Hierarchical ordering of sequential processes. Acta Informatica, 1:115-138, 1971.
• [6] N. Eén and N. Sörensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, SAT, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003.
• [7] E. A. Emerson and E. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982.
• [8] C.A.R. Hoare. Communicating sequential processes. Prentice Hall, 1985.
• [9] T. Latvala, A. Biere, K. Heljanko, and T. A. Junttila. Simple bounded LTL model checking. In A. J. Hu and A. K. Martin, editors, FMCAD, volume 3312 of Lecture Notes in Computer Science, pages 186-200. Springer, 2004.
• [10] MiniSat. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat, 2006. A. Zbrzezny / Improving the Translation from ECTL to SAT 531
• [11] Kedar S. Namjoshi. Certifying model checkers. In Gérard Berry, Hubert Comon, and Alain Finkel, editors, CAV, volume 2102 of Lecture Notes in Computer Science, pages 2-13. Springer, 2001.
• [12] Rotem Oshman and Orna Grumberg. A new approach to bounded model checking for branching time logics. In Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura, editors, ATVA, volume 4762 of Lecture Notes in Computer Science, pages 410-424. Springer, 2007.
• [13] W. Penczek and A. Półrola. Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach, volume 20 of Studies in Computational Intelligence. Springer-Verlag, 2006.
• [14] W. Penczek, B. Wo´zna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.
• [15] W. Penczek, B. Wo´zna, 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.
• [16] B. Wo´zna. ACTL_ properties and bounded model checking. Fundamenta Informaticae, 63(1):65-87, 2004.
• [17] B. Wo´zna and A. Zbrzezny. Checking ACTL_ properties of discrete timed automata via bounded model checking. In Proc. of the 1st Int. Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS'03), volume 2791 of LNCS, pages 18-33. Springer-Verlag, 2004.
• [18] B. Woźna and A. Zbrzezny. Bounded model checking for the existential fragment of TCTL-G and diagonal timed automata. Fundamenta Informaticae, 79(1-2):229-256, 2007.
• [19] A. Zbrzezny. Improvements in SAT-based reachability analysis for timed automata. Fundamenta Informaticae, 60(1-4):417-434, 2004.
• [20] A. Zbrzezny and A. Półrola. Sat-based reachability checking for timed automata with discrete data. Fundamenta Informaticae, 79(3-4) : 579-593, 2007.