DECIDING PROPERTIES OF NONREGULAR PROGRAMS

Extensions of propositional dynamic logic (PDL) with nonregular progra ms are considered. Three classes of nonregular languages are defined, and for each of them it is shown that for any language L in the class, PDL, with L added to the set of regular programs as a new program, is decidable. The first class consists of the languages accepted by push down automata that act only on the basis of their input symbol, except when determining whether they reject or continue. The second class (w hich contains even noncontext-free languages) consists of the language s accepted by deterministic stack machines, but which have a unique ne w symbol prefixing each word. The third class represents a certain del icate combination of these, and, in particular, it serves to prove the 1983 conjecture that PDL with the addition of the language {a(i)b(i)c (i)!i greater-than-or-equal-to 0} is decidable.