Document Open Access Logo

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

Authors Agnieszka M. Zbrzezny, Andrzej Zbrzezny

PDF
Thumbnail PDF

File

OASIcs.ICCSW.2015.78.pdf
  • Filesize: 0.61 MB
  • 9 pages

Document Identifiers

Author Details

Agnieszka M. Zbrzezny
Andrzej Zbrzezny

Cite As Get 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) https://doi.org/10.4230/OASIcs.ICCSW.2015.78

Abstract

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.

Subject Classification

Keywords
  • SMT
  • Timed Real-Weighted Interpreted Systems
  • Bounded Model Checking

Metrics

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

References

  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
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact