DROPS

Document

DOI: 10.4230/OASIcs.ICCSW.2012.88

Bounded Model Checking for Linear Time Temporal-Epistemic Logic

Authors: Artur Meski, Wojciech Penczek, and Maciej Szreter

Published in: OASIcs, Volume 28, 2012 Imperial College Computing Student Workshop

Abstract

We present a novel approach to the verification of multi-agent systems using bounded model checking for specifications in LTLK, a linear time temporal-epistemic logic. The method is based on binary decision diagrams rather than the standard conversion to Boolean satisfiability. We apply the approach to two classes of interpreted systems: the standard, synchronous semantics and the interleaved semantics. We provide a symbolic algorithm for the verification of LTLK over models of multi-agent systems and evaluate its implementation against MCK, a competing model checker for knowledge. Our evaluation indicates that the interleaved semantics can often be preferable in the verification of LTLK.

Cite as

Artur Meski, Wojciech Penczek, and Maciej Szreter. Bounded Model Checking for Linear Time Temporal-Epistemic Logic. In 2012 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 28, pp. 88-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{meski_et_al:OASIcs.ICCSW.2012.88,
  author =	{Meski, Artur and Penczek, Wojciech and Szreter, Maciej},
  title =	{{Bounded Model Checking for Linear Time Temporal-Epistemic Logic}},
  booktitle =	{2012 Imperial College Computing Student Workshop},
  pages =	{88--94},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-48-4},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{28},
  editor =	{Jones, Andrew V.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2012.88},
  URN =		{urn:nbn:de:0030-drops-37705},
  doi =		{10.4230/OASIcs.ICCSW.2012.88},
  annote =	{Keywords: model checking, multi-agent systems, temporal-epistemic logic, verification, interpreted systems}
}

Search Results

Documents authored by Szreter, Maciej

Bounded Model Checking for Linear Time Temporal-Epistemic Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message