Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\) (Q801901)

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.