Comparing SAT- and SMT- based bounded model checking for Ectl properties

• Autorzy: Zbrzezny A. M.

Identyfikatory

DOI

10.16926/m.2017.22.12

• Języki publikacji: EN

Abstrakty

EN

We compare two bounded model checking methods for properties expressed in the existential fragment of Computation Tree Logic (Ectl). To this end we use the generic pipeline paradigm (GPP) and the train controller system (TC), the classic concurrency problems, which we formalise by means of a finite transition system. We consider several properties of the problems that can be expressed in Ectl logic, and we present the performance evaluation of the mentioned bounded model checking methods by means of the running time and the memory used.

Słowa kluczowe

EN

computational tree logic; control system; limited modelling method

PL

logika drzewa obliczeniowego; system sterowania; metoda ograniczonego modelowania

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2017
• Tom: Vol. 22
• Strony: 161--175
• Opis fizyczny: Bibliogr. 12 poz., rys.

Twórcy

autor

Zbrzezny A. M.

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

Bibliografia

• [1] C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008.
• [2] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings 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.
• [3] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. Bounded model checking. Advances in Computers, 58:117–148, 2003.
• [4] N. Eén and N. Sörensson. MiniSat. http://minisat.se/MiniSat.html.
• [5] N. Eén and N. Sörensson. MiniSat - A SAT Solver with Conflict-Clause Minimization. In Proceedings of 8th International Conference on Theory and Applications of Satisfiability Testing(SAT’05), LNCS. Springer-Verlag, 2005.
• [6] E. A. Emerson and E. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241–266, 1982.
• [7] W. van der Hoek and M. Wooldridge. Model checking knowledge and time. In Proceedings of the 9th Int. SPIN Workshop (SPIN’02), volume 2318 of LNCS, pages 95–111. Springer-Verlag, 2002.
• [8] D. Peled. All from one, one for all: On model checking using representatives. In Proceedings of the 5th Int. Conf. on Computer Aided Verification (CAV’93), volume 697 of LNCS, pages 409–423. Springer-Verlag, 1993.
• [9] W. Penczek, B. Wozna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135–156, 2002.
• [10] B. Wozna. ACTL_ properties and bounded model checking. Fundamenta Informaticae, 63(1):65–87, 2004.
• [11] B. Wozna-Szczesniak, A. M. Zbrzezny, and A. Zbrzezny. The BMC method for the existential part of RTCTLK and interleaved interpreted systems. In Proceedings of the 15th Portuguese Conference on Artificial Intelligence (EPIA’2011), volume 7026 of LNAI, pages 551–565. Springer-Verlag, 2011.
• [12] A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1-4):513–531, 2008.