Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
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
Wydawca
Czasopismo
Rocznik
Tom
Strony
375--395
Opis fizyczny
Bibliogr. 14 poz., tab.
Twórcy
autor
- Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa Armii Krajowej 13/15, 42-200 Częstochowa, Poland, a.zbrzezny@ajd.czest.pl
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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS8-0029-0034