1 Search Results for "Zbrzezny, Agnieszka M."

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-dev.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}
}
  • Refine by Author
  • 1 Zbrzezny, Agnieszka M.
  • 1 Zbrzezny, Andrzej

  • Refine by Classification

  • Refine by Keyword
  • 1 Bounded Model Checking
  • 1 SMT
  • 1 Timed Real-Weighted Interpreted Systems

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2015

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 Imprint Privacy Contact