Model Checking Temporal Logics of Knowledge Via OBDDs

There are no files associated with this record.

Title Model Checking Temporal Logics of Knowledge Via OBDDs
Author Su, Kaile; Sattar, Abdul; Luo, Xiangyu
Journal Name The Computer Journal
Year Published 2007
Place of publication Oxford
Publisher Oxford University Press
Abstract Model checking is a promising approach to automatic verification, which has concentrated on specification expressed in temporal logics. Comparatively little attention has been given to temporal logics of knowledge, although such logics have been proven to be very useful in the specifications of protocols for distributed systems. In this paper, we addressed the model checking problem for a temporal logic of knowledge (Halpern and Vardi's logic of CKLn). Based on the semantics of interpreted systems with local propositions, we developed an approach to symbolic CKLn model checking via Ordered Binary decision diagrams and implemented the corresponding symbolic model checker MCTK. In our approach to model checking specifications involving agents' knowledge, the knowledge modalities are eliminated via quantifiers over agents' non-observable variables. We then modelled the Dining Cryptographers protocol and the five-hands protocol for Russian Cards problem in MCTK. Via these two examples, we compare MCTK's empirical performance with two different state-of-the-art epistemic model checkers, MCK and MCMAS.
Peer Reviewed Yes
Published Yes
Publisher URI
Alternative URI
Volume 50
Issue Number 4
Page from 403
Page to 420
ISSN 0010-4620
Date Accessioned 2008-03-06
Language en_AU
Research Centre Institute for Integrated and Intelligent Systems
Faculty Faculty of Science, Environment, Engineering and Technology
Subject PRE2009-Analysis of Algorithms and Complexity
Publication Type Journal Articles (Refereed Article)
Publication Type Code c1

Show simple item record

Griffith University copyright notice