Interpreting logics of knowledge in propositional dynamic logic (Q1096609)

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.)