Interpreting Logics of Knowledge in Propositional Dynamic Logic with Converse.
YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
A natural propositional logic of knowledge, common knowledge, and branching time appropriate for reasoning about distributed systems is presented. This logic may be interpreted in Propositional Dynamic Logic with Converse PDLC making the relationship between protocol models and general Kripke models precise and showing that PDLC already suffices for a certain amount of reasoning about knowledge in distributed systems. It follows that satisfiability for propositional logic of branching time remains EMPTIME complete with the addition of any combination of knowledge and common knowledge operators. Finally, the validity or satisfiability of a formula involving two or more participants is not affected by restricting attention to protocol involving just those participants explicitly mentioned in the formula. Keywords Logic of knowledge Distributed system Modal logic Propositional dynamic logic.
- Computer Systems