Title :
Deciding properties of nonregular programs
Author :
Harel, David ; Raz, Danny
Author_Institution :
Dept. of Appl. Math. & Comput. Sci., Weizmann Inst. of Sci. Rehovot, Israel
Abstract :
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
Keywords :
decidability; finite automata; formal languages; formal logic; PDAs; decidability; decision procedures; infinite trees; nonregular languages; nonregular programs; propositional dynamic logic; stack automata; validity; Automata; Calculus; Computer science; Logic; Mathematics; Page description languages; Personal digital assistants;
Conference_Titel :
Foundations of Computer Science, 1990. Proceedings., 31st Annual Symposium on
Conference_Location :
St. Louis, MO
Print_ISBN :
0-8186-2082-X
DOI :
10.1109/FSCS.1990.89587