AbstractThe borderline between decidable and undecidable propositional dynamic Logic (PDL) is sought when iterative programs represented by regular expressions are augmented with increasingly more complex recursive programs represented by nonregular languages. The results in this paper indicate that this line is extremely close to the original regular PDL. Moreover, the versions of PDL which we show to be beyond this borderline are shown to be actually very highly undecidable. The main results of the paper are: (a) The validity problem for PDL with the single additional context-free program AΔ (B)AΔ, for atomic programs A, B, defined as ⋃i⩾0Ai;B;Ai, is ∏11-complete. (b) There exists a recursive (but nonregular, and hence noncontext-free) on...