Undecidability of PDL with L=\a^2^ i| i 0\

Modal logic (including the logic of norms) (03B45) Complexity of computation (including implicit computational complexity) (03D15) Undecidability and degrees of sets of sentences (03D35) Abstract data types; algebraic specification (68Q65)

Review text

The validity problem of regular PDL (Propositional Dynamic Logic) was shown to be decidable in deterministic exponential time by \textit{M. J. Fischer} and \textit{R. E. Ladner} [J. Comput. Syst. Sci. 18, 194-211 (1979; Zbl 0408.03014)]. The same problem can become \(\Pi^ 1_ 1\)-complete with the addition of a bit of context-free programs. Indeed, \textit{D. Harel, A. Pnueli} and \textit{J. Stavi} [J. Comput. Syst. Sci. 26, 222-243 (1983; Zbl 0536.68041)] have given some simple classes of such a bad behavior. This paper gives another nonregular PDL of a very bad kind, showing that the validity problem for PDL with the addition of \(L=\{a^{2^ i}| i\geq 0\}\) is \(\Pi^ 1_ 1\)-complete.

Recommendations

Cites work

Cited in

(7)

This page was built for publication: Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q801901)