zbMATH — the first resource for mathematics

Interpreting logics of knowledge in propositional dynamic logic. (English) Zbl 0634.03012
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.)
Reviewer: J.Sefránek

03B45 Modal logic (including the logic of norms)
68N25 Theory of operating systems
68T99 Artificial intelligence
03B70 Logic in computer science
03B25 Decidability of theories and sets of sentences
68Q25 Analysis of algorithms and problem complexity
03D15 Complexity of computation (including implicit computational complexity)
Full Text: DOI
[1] Emerson, E.A.; Halpern, J.Y., Decision procedures and expressiveness in the temporal logic of brancing time, J. comput. system sci., 30, 1-24, (1985) · Zbl 0559.68051
[2] Fischer, M.J.; Immerman, N.; Fischer, M.J.; Immerman, N., Foundations of knowledge for distributed systems, (), 171-185, also in
[3] Fischer, M.J.; Ladner, R.E., Propositional dynamic logic of regular programs, J. comput. system sci., 18, 2, 194-211, (1979) · Zbl 0408.03014
[4] Halpern, J.Y.; Moses, Y., Knowledge and common knowledge in a distributed environment, (), 50-61 · Zbl 0699.68115
[5] Halpern, J.Y.; Vardi, M., The complexity of reasoning about knowledge and time, (), 304-315
[6] Parikh, R., Logics of knowledge, games and dynamic logic, foundations of software technology and theoretical computer science, (), 202-222
[7] Pratt, V.R., A decidable μ-calculus: preliminary report, (), 421-427
[8] Streett, R.S., Propositional dynamic logic of looping and converse, () · Zbl 0515.68062
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.