OASIcs.ICCSW.2012.88.pdf
- Filesize: 0.6 MB
- 7 pages
Document
Bounded Model Checking for Linear Time Temporal-Epistemic Logic
Authors
-
Part of:
Volume:
2012 Imperial College Computing Student Workshop
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication date: 2012-11-09
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
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)
0PDF Downloads