Checking WECTLK Properties of TRWISs via SMT-based Bounded Model Checking

Authors Agnieszka M. Zbrzezny, Andrzej Zbrzezny

Thumbnail PDF


  • Filesize: 0.61 MB
  • 9 pages

Document Identifiers

Author Details

Agnieszka M. Zbrzezny
Andrzej Zbrzezny

Cite AsGet BibTex

Agnieszka M. Zbrzezny and Andrzej Zbrzezny. Checking WECTLK Properties of TRWISs via SMT-based Bounded Model Checking. In 2015 Imperial College Computing Student Workshop (ICCSW 2015). Open Access Series in Informatics (OASIcs), Volume 49, pp. 78-86, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


In this paper, we present a Satisfiability Modulo Theory based (SMT-based) bounded model checking (BMC) method for Timed Real-Weighted Interpreted Systems and for the existential fragment of the Weighted Epistemic Computation Tree Logic. SMT-based bounded model checking consists in translating the existential model checking problem for a modal logic and for a model to the satisfiability problem of a quantifier-free first-order formula. We have implemented the SMT-BMC method and performed the BMC algorithm on Timed Weighted Generic Pipeline Paradigm benchmark. The preliminary experimental results demonstrate the feasibility of the method. To perform the experiments, we used the state of the art SMT-solver Z3.
  • SMT
  • Timed Real-Weighted Interpreted Systems
  • Bounded Model Checking


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995. Google Scholar
  2. P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In Proceedings of CAV'04, volume 3114 of LNCS, pages 479-483. Springer-Verlag, 2004. Google Scholar
  3. M. Kacprzak, W. Nabialek, A. Niewiadomski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae, 85(1-4):313-328, 2008. Google Scholar
  4. A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: A model checker for the verification of multi-agent systems. In Proceedings of CAV'09, volume 5643 of LNCS, pages 682-688. Springer-Verlag, 2009. Google Scholar
  5. L. De Moura and N. Bjørner. Z3: an efficient SMT solver. In Proceedings of TACAS'08, volume 4963 of LNCS, pages 337-340. Springer-Verlag, 2008. Google Scholar
  6. M. Wooldridge. An introduction to multi-agent systems - Second Edition. John Wiley &Sons, 2009. Google Scholar
  7. B. Woźna-Szcześniak. SAT-based bounded model checking for weighted deontic interpreted systems. In Proceedings of EPIA'13, volume 8154 of LNAI, pages 444-455. Springer-Verlag, 2013. Google Scholar
  8. B. Woźna-Szcześniak. Checking EMTLK properties of timed interpreted systems via bounded model checking. In Proceedings of AAMAS'14, pages 1477-1478. IFAAMAS/ACM, 2014. Google Scholar
  9. B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. SAT-based bounded model checking for weighted interpreted systems and weighted linear temporal logic. In Proceedings of PRIMA'13, volume 8291 of LNAI, pages 355-371. Springer-Verlag, 2013. Google Scholar
  10. A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1-4):513-531, 2008. Google Scholar