Checking RTECTL Properties of STSs via SMT-Based Bounded Model Checking

  • Agnieszka M. ZbrzeznyEmail author
  • Andrzej Zbrzezny
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 373)


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.


Model Check Discrete Data Atomic Proposition Symbolic State Bound Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real-time. Information and Computation 104(1), 2–34 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, ch. 26, pp. 825–885. IOS Press (2009)Google Scholar
  4. 4.
    Biere, A.: PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 4, 75–97 (2008)zbMATHGoogle Scholar
  5. 5.
    Markey, N., Schnoebelen, P.: Symbolic model checking for simply-timed systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 102–117. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  8. 8.
    Cook, E.E., Levmore, S.X.: Super Strategies for Puzzles and Games. Doubleday, Garden City (1981)Google Scholar
  9. 9.
    Woźna-Szcześniak, B., Zbrzezny, A., Zbrzezny, A.: The BMC method for the existential part of RTCTLK and interleaved interpreted systems. In: Antunes, L., Pinto, H.S. (eds.) EPIA 2011. LNCS, vol. 7026, pp. 551–565. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  10. 10.
    Woźna-Szcześniak, B., Zbrzezny, A.M., Zbrzezny, A.: SAT-based bounded model checking for RTECTL and simply-timed systems. In: Balsamo, M.S., Knottenbelt, W.J., Marin, A. (eds.) EPEW 2013. LNCS, vol. 8168, pp. 337–349. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  11. 11.
    Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1-4), 513–531 (2008)zbMATHMathSciNetGoogle Scholar
  12. 12.
    Zbrzezny, A., Pólrola, A.: SAT-based reachability checking for timed automata with discrete data. Fundamenta Informaticae 79(3-4), 579–593 (2007)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.IMCSJan Długosz UniversityCzęstochowaPoland

Personalised recommendations