Authors: H.P. van Ditmarsch, J. Ruan, and W. van der Hoek
Abstract: We give a relation between a logic of knowledge and change, with a semantics on Kripke models, and a logic of knowledge and time, with a semantics on interpreted systems. More in particular, given an epistemic state (pointed multi-agent Kripke model where all accessibility relations are equivalence relations) and a formula in action model logic (a logic describing the consequences of epistemic events), we construct an interpreted system relative to that epistemic state and that formula that satisfies the translation of the formula into branching temporal epistemic logic. The construction involves that the protocol that is implicit in the dynamic epistemic formula, i.e. the set of sequences of events being executed to evaluate the formula, is made explicit. For presentation reasons, we focus on the logic of knowledge and change that is known as public announcement logic, which can be seen as a specific action model logic. The interpreted system that is constructed in the process is minimal in the sense that it precisely contains all the event structure present in the dynamic epistemic formula. Different approaches to this correspondence can be considered syntactic or semantic sugar. That observation brings applications of our insights closer, because some such approaches originate in the model checking community.
Keywords: modal logic, interpreted system, model checking, action logic, protocol, temporal logic
Download this paper in pdf.
BibTex:
@inproceedings{hvd.jr.wvdh.2007,
author = {H. van Ditmarsch and J. Ruan and W. van der Hoek},
title = {Model Checking Dynamic Epistemics in Branching Time},
booktitle = {Proceedings of Workshop on Formal Approaches to Multi-Agent Systems},
address = {Durham, UK},
month= September,
year = 2007}
Related posts:
- My Coming talk in Liverpool: Connecting Dynamic Epistemic and Temporal Epistemic Logics For Multi-Agent Systems Title: Connecting Dynamic Epistemic and Temporal Epistemic Logics For Multi-Agent...
- Private: Submission on Healthcare (protected due to review process) \begin{abstract} Healthcare systems are essential in maintaining the well-being of...
Related posts brought to you by Yet Another Related Posts Plugin.
