Bounded Model Checking for Linear Time Temporal-Epistemic Logic

Meski, Artur; Penczek, Wojciech; Szreter, Maciej

doi:10.4230/OASIcs.ICCSW.2012.88

Document

Bounded Model Checking for Linear Time Temporal-Epistemic Logic

Authors Artur Meski, Wojciech Penczek, Maciej Szreter

Part of: Volume: 2012 Imperial College Computing Student Workshop (ICCSW 2012)
Part of: Series: Open Access Series in Informatics (OASIcs)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2012-11-09

PDF

File

PDF

OASIcs.ICCSW.2012.88.pdf

Filesize: 0.6 MB
7 pages

Document Identifiers

DOI: 10.4230/OASIcs.ICCSW.2012.88
URN: urn:nbn:de:0030-drops-37705

Subject Classification

Keywords

model checking
multi-agent systems
temporal-epistemic logic
verification
interpreted systems

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/OASIcs.ICCSW.2012.88

Author Details

Artur Meski

Wojciech Penczek

Maciej Szreter

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail