Propositional dynamic logic of nonregular programs

摘要

The 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) one-letter program L ⊆ A such that the validity problem for PDL with the single additional program L is ∏11-complete. Undecidability and ∏11-completeness of a less restricted version of PDL than the one in (a) are proved separately using different techniques.