License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.ICCSW.2015.78
URN: urn:nbn:de:0030-drops-54848
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5484/
Go to the corresponding OASIcs Volume Portal

Zbrzezny, Agnieszka M. ; Zbrzezny, Andrzej

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

pdf-format:
13.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{zbrzezny_et_al:OASIcs:2015:5484,
  author =	{Agnieszka M. Zbrzezny and Andrzej Zbrzezny},
  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 =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-000-2},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{49},
  editor =	{Claudia Schulz and Daniel Liew},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5484},
  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}
}

Keywords: SMT, Timed Real-Weighted Interpreted Systems, Bounded Model Checking
Collection: 2015 Imperial College Computing Student Workshop (ICCSW 2015)
Issue Date: 2015
Date of publication: 23.09.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI