Accession Number:

ADA165487

Title:

Interpreting Logics of Knowledge in Propositional Dynamic Logic with Converse.

Descriptive Note:

Technical rept.,

Corporate Author:

YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1986-03-01

Pagination or Media Count:

14.0

Abstract:

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.

Subject Categories:

  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE