Interpreting Logics of Knowledge in Propositional Dynamic Logic with Converse.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1986
Accession Number
ADA165487

Entities

People

  • Michael J. Fischer
  • Neil Immerman

Organizations

  • Yale University

Tags

Communities of Interest

  • Ground and Sea Platforms
  • Human Systems

DTIC Thesaurus Topics

  • Automata
  • Computations
  • Computer Science
  • Computers
  • Contracts
  • Distributed Computing
  • Information Systems
  • Language
  • Marine Corps
  • Mathematics
  • Military Research
  • New York
  • Numbers
  • Program Management
  • Reasoning
  • Technical Information Centers
  • Universities

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.