Bounded Model Checking for Linear Time Temporal-Epistemic Logic

Authors Artur Meski, Wojciech Penczek, Maciej Szreter

Thumbnail 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)


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.
  • model checking
  • multi-agent systems
  • temporal-epistemic logic
  • verification
  • interpreted systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
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