ML Anthology

Model Checking Temporal Logics of Knowledge in Distributed Systems

Kaile Su
AAAI 2004 pp. 98-103
/aaai/2004/su2004aaai-model/

Abstract

Model checking is a promising approach to automatic veri-cation, which has concentrated on specication expressed in temporal logic. Comparatively little attention has been given to temporal logics of knowledge, although such logics have been proven to be very useful in the specications of proto-cols for distributed systems. In this paper, we address our-selves to 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 develop an approach to symbolic CKLn model checking via OBDDs. In our approach to model checking specications involving agents ' knowledge, the knowledge modalities are eliminated via quantiers over agents ' non-observable vari-ables.

PDF AAAI Semantic Scholar

Cite

Text

Su. "Model Checking Temporal Logics of Knowledge in Distributed Systems." AAAI Conference on Artificial Intelligence, 2004.

Markdown

[Su. "Model Checking Temporal Logics of Knowledge in Distributed Systems." AAAI Conference on Artificial Intelligence, 2004.](https://mlanthology.org/aaai/2004/su2004aaai-model/)

BibTeX

@inproceedings{su2004aaai-model,
  title     = {{Model Checking Temporal Logics of Knowledge in Distributed Systems}},
  author    = {Su, Kaile},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2004},
  pages     = {98-103},
  url       = {https://mlanthology.org/aaai/2004/su2004aaai-model/}
}