Comparing sat-based bounded model checking rtectl and ectl properties
Agnieszka M. Zbrzezny
Abstract
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.
Keywords:
SAT, bounded model checking, ECTL, RTECTL, translationReferences
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.
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.
Zbrzezny, A. M. (2017). Comparing sat-based bounded model checking rtectl and ectl properties. Technical Sciences, 20(2), 131–147. https://doi.org/10.31648/ts.5147
Agnieszka M. Zbrzezny
