Deciding properties of nonregular programs

The problem of deciding the validity of formulas in extensions of propositional dynamic logic (PDL) is considered. The extensions are obtained by adding programs defined by nonregular languages. In the past, a number of very simple languages were shown to render this problem highly undecidable, whereas other very similar-looking languages were shown to retain decidability. Understanding this rather strange phenomenon and generalizing the isolated extensions have remained elusive. The authors provide decision procedures for two wide classes of extensions, thus shedding light on the general problem. The proofs are novel, in that they explicitly consider the machines that accept the languages, in this case special classes of PDAs and stack automata. It is shown that the emptiness problem for stack automata on infinite trees is decidable, a result of independent interest, and the result is combined with the construction of certain tree models for the corresponding formulas.<>