A New Translation from ECTL* to SAT*

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

Abstrakty

EN

In this paper we present a new translation from ECTL* to SAT and show that the proposed translation substantially increases the efficiency of verifying temporal properties using the Bounded Model Checking method. We have implemented our new translation and made experimental results, which demonstrate the efficiency of the method.

Słowa kluczowe

EN

ECTL; translation to SAT; bounded model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 120, nr 3/4
• Strony: 375--395
• Opis fizyczny: Bibliogr. 14 poz., tab.

Twórcy

autor

Zbrzezny A.

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

Bibliografia

• [1] Abdulla, P. A., Bjesse, P., Eén, N.: Symbolic Reachability Analysis Based on SAT-Solvers, Proc. of the 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), 1785, Springer-Verlag, 2000.
• [2] Baier, C., Katoen, J.-P.: Principles of model checking, MIT Press, 2008, ISBN 978-0-262-02649-9.
• [3] Biere, A., Cimatti, A., Clarke, E., M.Fujita, Zhu, Y.: Symbolic Model Checking Using SAT Procedures Instead of BDDs, Proc. of the ACM=IEEE Design Automation Conference (DAC'99), 1999.
• [4] Biere, A., Heljanko, K., Junttila, T. A., Latvala, T., Schuppan, V.: Linear Encodings of Bounded LTL Model Checking, Logical Methods in Computer Science, 2(5), 2006.
• [5] Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, 19(1), 2001, 7-34.
• [6] Clarke, E. M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and Complexity of Bounded Model Checking, VMCAI (B. Steffen, G. Levi, Eds.), 2937, Springer, 2004.
• [7] Dijkstra, E.: Hierarchical Ordering of Sequential Processes, Acta Inf., 1, 1971, 115-138.
• [8] Eén, N., Sörensson, N.: MiniSat Page, http://minisat.se/MiniSat.html.
• [9] Emerson, E. A., Halpern, J. Y.: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time, J. Comput. Syst. Sci., 30(1), 1985, 1-24.
• [10] Hoare, C.: Communicating sequential processes, Prentice Hall, 1985.
• [11] Latvala, T., Biere, A., Heljanko, K., Junttila, T. A.: Simple Bounded LTL Model Checking, FMCAD (A. J. Hu, A. K. Martin, Eds.), 3312, Springer, 2004, ISBN 3-540-23738-0.
• [12] Penczek, W., Wo´zna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL, Fundamenta Informaticae, 51(1-2), 2002, 135-156.
• [13] Woźna, B.: ACTL_ Properties and Bounded Model Checking, Fundamenta Informaticae, 63(1), 2004, 65-87.
• [14] Zbrzezny, A.: Improving the Translation from ECTL to SAT, Fundamenta Informaticae, 85(1-4), 2008, 513-531.