Comparing sat-based bounded model checking rtectl and ectl properties

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

Abstrakty

EN

We compare two SAT-based bounded model checking algorithms for the properties expressed in the existential fragment of a soft real-time computation tree logic (RTECTL) and 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 both RTECTL and ECTL, 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

SAT; bounded model checking; ECTL; RTECTL; translation

• Wydawca: Wydawnictwo Uniwersytetu Warmińsko-Mazurskiego w Olsztynie
• Czasopismo: Technical Sciences / University of Warmia and Mazury in Olsztyn
• Rocznik: 2017
• Tom: nr 20(2)
• Strony: 131--147
• Opis fizyczny: Bibliogr. 14 poz., rys., wykr.

Twórcy

autor

Zbrzezny A. M.

• Instytut Matematyki i Informatyki, Wydział Matematyczno-Przyrodniczy, Akademia im. Jana Długosza, 42-200 Częstochowa, al. Armii Krajowej 13/15, phone: [phone]

Bibliografia

• BAIER C., KATOEN J.-P. 2008. Principles of model checking. MIT Press.
• BIERE A., CIMATTI A., CLARKE E., ZHU Y. 1999. Symbolic Model Checking without BDDs. Proceedings of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS;99), LNCS. Springer-Verlag, p. 193-207.
• BRYANT R., 1986. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comput, 35(8): 677-691.
• CAMPOS S.V.A. 1996. A quantitative approach to the formal verification of real-time systems. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA.
• CLARKE E., EMERSON E.A., SISTLA A.P. 1986. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. ACM Trans. Program. Lang. Syst., 8(2): 244-263.
• CLARKE E., GRUMBERG O., PELED D. 1999. Model Checking. MIT Press.
• EMERSON E.A., MOK A.K., SISTLA A.P., SRINIVASAN J. 1992. Quantitative Temporal Reasoning. Real-Time Syst., 4: 331-352.
• LOMUSCIO A., PENCZEK W., QU H. 2010. Partial order reduction for model checking interleaved multi-agent systems. Proceedings of the 9th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS;2010). IFAAMAS Press, p. 659-666.
• MCMILLAN K.L. 1993. Symbolic Model Checking. Kluwer Academic Publishers.
• PENCZEK W., LOMUSCIO A. 2003. Verifying Epistemic Properties of Multi-Agent Systems via Bounded Model Checking. Fundam. Informaticae, 55: 167-185.
• PENCZEK W., WOŹNA B., ZBRZEZNY A. 2002. Bounded Model Checking for the Universal Fragment of CTL. Fundam. Informaticae, 51(1-2): 135-156.
• WOŹNA B., ZBRZEZNY A. 2004. Checking ACTL* Properties of Discrete Timed Automata via Bounded Model Checking. Proceedings of the 1st Int. Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS’03), LNCS. Springer-Verlag, p. 18-33.
• WOŹNA-SZCZEŚNIAK B., ZBRZEZNY A.M., ZBRZEZNY A. 2011. The BMC method for the existential part of RTCTLK and interleaved interpreted systems. Proceedings of the 15th Portuguese Conference on Artificial Intelligence (EPIA;2011), LNAI. Springer-Verlag, p. 551-565.
• ZBRZEZNY A. 2008. Improving the Translation from ECTL to SAT. Fundam. Informaticae 85(1-4): 513-531.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).