DROPS

Document

DOI: 10.4230/OASIcs.ICCSW.2015.78

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

Authors: Agnieszka M. Zbrzezny and Andrzej Zbrzezny

Published in: OASIcs, Volume 49, 2015 Imperial College Computing Student Workshop (ICCSW 2015)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{zbrzezny_et_al:OASIcs.ICCSW.2015.78,
  author =	{Zbrzezny, Agnieszka M. and Zbrzezny, Andrzej},
  title =	{{Checking WECTLK Properties of TRWISs via SMT-based Bounded Model Checking}},
  booktitle =	{2015 Imperial College Computing Student Workshop (ICCSW 2015)},
  pages =	{78--86},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-000-2},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{49},
  editor =	{Schulz, Claudia and Liew, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2015.78},
  URN =		{urn:nbn:de:0030-drops-54848},
  doi =		{10.4230/OASIcs.ICCSW.2015.78},
  annote =	{Keywords: SMT, Timed Real-Weighted Interpreted Systems, Bounded Model Checking}
}

Search Results

Documents authored by Zbrzezny, Andrzej

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

Abstract

Cite as

Thanks for your feedback!

Could not send message