DOI
10.9781/ijimai.2015.354
Abstract
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.
Source Publication
International Journal of Interactive Multimedia and Artificial Intelligence
Recommended Citation
Zbrzezny, Agnieszka and Zbrzezny, Andrzej
(2015)
"Checking RTECTL properties of STSs via SMT-based Bounded Model Checking,"
International Journal of Interactive Multimedia and Artificial Intelligence: Vol. 3:
Iss.
5, Article 9.
DOI: 10.9781/ijimai.2015.354
Available at:
https://ijimai.researchcommons.org/ijimai/vol3/iss5/9
