Model Checking Temporal Logics of Knowledge in Distributed Systems
Author(s)
Su, Kaile
Griffith University Author(s)
Year published
2004
Metadata
Show full item recordAbstract
Model checking is a promising approach to automatic verification, which has concentrated on specification 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 specifications of protocols for distributed systems. In this paper, we address ourselves to the model checking problem for a temporal logic of knowledge (Halpern and Vardi's logic of $CKL_n$). Based on the semantics of {/it interpreted systems} with {/it local propositions}, we develop an approach to symbolic $CKL_n$ model checking via OBDDs. In our ...
View more >Model checking is a promising approach to automatic verification, which has concentrated on specification 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 specifications of protocols for distributed systems. In this paper, we address ourselves to the model checking problem for a temporal logic of knowledge (Halpern and Vardi's logic of $CKL_n$). Based on the semantics of {/it interpreted systems} with {/it local propositions}, we develop an approach to symbolic $CKL_n$ model checking via OBDDs. In our approach to model checking specifications involving agents' knowledge, the knowledge modalities are eliminated via quantifiers over agents' non-observable variables.
View less >
View more >Model checking is a promising approach to automatic verification, which has concentrated on specification 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 specifications of protocols for distributed systems. In this paper, we address ourselves to the model checking problem for a temporal logic of knowledge (Halpern and Vardi's logic of $CKL_n$). Based on the semantics of {/it interpreted systems} with {/it local propositions}, we develop an approach to symbolic $CKL_n$ model checking via OBDDs. In our approach to model checking specifications involving agents' knowledge, the knowledge modalities are eliminated via quantifiers over agents' non-observable variables.
View less >
Conference Title
Nineteenth National Conference on Artificial Intelligence: Sixteenth Conference on Innovative Applications of Artificial Intelligence