Interpreting logics of knowledge in propositional dynamic logic
type: Item
instance of: scholarly article
title: Interpreting logics of knowledge in propositional dynamic logic
zbMATH Open document ID: 0634.03012
DOI: 10.1016/0020-0190(87)90129-3
author: Michael Fischer
author: Neil Immerman
published in: Information Processing Letters
publication date: 1987-01-01T00:00:00Z
review text: A language of Propositional Temporal Knowledge Logic (PTKL) over a set of propositional symbols PROP and a finite set \(PART=\{1,...,n\}\) of participants with operators Y, G, U and \(C_ H\) is specified. The semantics of PTKL is defined using a kind of Kripke model called a distributed protocol. The protocol is a tuple \({\mathcal P}=<n,Q,I,\tau,\pi >\) for n participants, where Q is a set of local states, \(I\subseteq Q\) n is a set of initial global states, \(\pi\) : Q \(n\times PROP\to \{0,1\}\), \(\tau\subseteq Q\) \(n\times Q\) n is the next move relation on global states, \(\tau\) * is its reflexive transitive closure. Reachable global states are defined using I and \(\tau\) *. The satisfaction relation \(<{\mathcal P},q>\vDash \alpha\) is defined for a protocol \({\mathcal P}\), global state q and a PTKL formula \(\alpha\). The definition covers the following intuition: \(Y\alpha\) means that \(\alpha\) holds at every next step (in branching time), \(G\alpha\) means that \(\alpha\) holds at all points in the future, \(\alpha\) \(U\beta\) means that \(\alpha\) is true and remains true until \(\beta\) becomes true, and \(C_ H\alpha\) means that it is common knowledge among the members of a set H of participants that \(\alpha\). Main results of the paper are: 1. Interpretation of PTKL in Propositional Dynamic Logic with Converse (PDLC). Let \(\Phi\) (PTKL), \(\Phi\) (PDLC) be the sets of all formulas of PTKL, PDLC. There is an interpretation \(f: \Phi\) (PTKL)\(\to \Phi (PDLC)\) such that for all \(\alpha\), \(\alpha\) is satisfiable iff f(\(\alpha)\) is satisfiable. The mapping f is simultaneously log-space and O(n 2) time computable. 2. The satisfiability problem for PTKL is decidable in EXPTIME. (The satisfiability problem for PTKL is EXPTIME complete even with only one participant and no occurrences of \(C_ H:\) satisfiability for propositional logic of branching time remains EXPTIME complete with addition of any combination of knowledge operators.)
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 68N25
Mathematics Subject Classification ID: 68T99
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 03D15
zbMATH DE Number: 4031636
zbMATH Keywords: distributed systems
zbMATH Keywords: Propositional Temporal Knowledge Logic
zbMATH Keywords: participants
zbMATH Keywords: semantics
zbMATH Keywords: Kripke model
zbMATH Keywords: distributed protocol
zbMATH Keywords: Propositional Dynamic Logic
zbMATH Keywords: interpretation
zbMATH Keywords: satisfiability problem
zbMATH Keywords: branching time
reviewed by: Jan Šefránek
MaRDI profile type: Publication
full work available at URL: 0020-0190(87)90129-3
OpenAlex ID: W2086062372
cites work: Decision procedures and expressiveness in the temporal logic of branching time
cites work: Propositional dynamic logic of regular programs
cites work: Knowledge and common knowledge in a distributed environment
cites work: Q3218103
cites work: Propositional dynamic logic of looping and converse is elementarily decidable
description: scientific article; zbMATH DE number 4031636