Bounded Model Checking for Linear Time Temporal-Epistemic Logic

Authors Artur Meski, Wojciech Penczek, Maciej Szreter



PDF
Thumbnail PDF

File

OASIcs.ICCSW.2012.88.pdf
  • Filesize: 0.6 MB
  • 7 pages

Document Identifiers

Author Details

Artur Meski
Wojciech Penczek
Maciej Szreter

Cite AsGet 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

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.
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
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