Checking RTECTL properties of STSs via SMT-based Bounded Model Checking
DOI:
https://doi.org/10.9781/ijimai.2015.354Keywords:
RTECTL, STS, SMTAbstract
We present an SMT-based bounded model checking (BMC) method for Simply-Timed Systems (STSs) and for the existential fragment of the Real-time Computation Tree Logic. We implemented the SMT-based BMC algorithm and compared it with the SAT-based BMC method for the same systems and the same property language on several benchmarks for STSs. For the SAT- based BMC we used the PicoSAT solver and for the SMT-based BMC we used the Z3 solver. The experimental results show that the SMT-based BMC performs quite well and is, in fact, sometimes significantly faster than the tested SAT-based BMC.Downloads
References
[1] R. Alur. Timed Automata. In Proceedings of CAV’99, volume 1633 of LNCS, pages 8-22. Springer-Verlag, 1999.
[2] R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(1):2-34, 1993.
[3] Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 26, pages 825-885. IOS Press, 2009.
[4] A. Biere. PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 4:75-97, 2008.
[5] N. Markey and Ph. Schnoebelen. Symbolic model checking of simply-timed systems. In Proceedings of FORMATS’04 and FTRTFT’04, volume 3253 of LNCS, pages 102-117. Springer, 2004.
[6] L. De Moura and N. Bjørner. Z3: an efficient SMT solver. In Proceedings of TACAS’2008, volume 4963 of LNCS, pages 337-340. Springer-Verlag, 2008.
[7] D. Peled. All from one, one for all: On model checking using representatives. In Proceedings of CAV’93, volume 697 of LNCS, pages 409-423. Springer-Verlag, 1993.
[8] Elizabeth Early Cook Saul X. Levmore. Super Strategies for Puzzles and Games. Doubleday, Garden City, N.Y., 1981.
[9] B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. The BMC method for the existential part of RTCTLK and interleaved
interpreted systems. In Proceedings of EPIA’2011, volume 7026 of LNAI, pages 551-565. Springer-Verlag, 2011.
[10] B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. SAT-based bounded model checking for RTECTL and simply-timed systems. In Proceedings of EPEW 2013, volume 8168 of LNCS, pages 337-349. Springer-Verlag, 2013.
[11] A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1-4):513-531, 2008.
[12] A. Zbrzezny and A. Pólrola. SAT-based reachability checking for timed automata with discrete data. Fundamenta Informaticae, 79(3-4):579-593, 2007.
Downloads
Published
-
Abstract32
-
PDF24
Submit Article
Information
