Interpreting logics of knowledge in propositional dynamic logic.

*(English)*Zbl 0634.03012A 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.)

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

##### MSC:

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

##### Keywords:

distributed systems; Propositional Temporal Knowledge Logic; participants; semantics; Kripke model; distributed protocol; Propositional Dynamic Logic; interpretation; satisfiability problem; branching time
PDF
BibTeX
XML
Cite

\textit{M. J. Fischer} and \textit{N. Immerman}, Inf. Process. Lett. 25, 175--181 (1987; Zbl 0634.03012)

Full Text:
DOI

##### References:

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