Automata-Theoretic Techniques for Modal Logics of Programs

We present a new technique for obtaining decision procedures for modal logics of programs. The technique centers around a new class of finite automata on infinite trees for which the emptiness problem can be solved in polynomial time. The decision procedures then consist of constructing an automaton Af, for a given formula f, such that Af, accepts some tree if and only if f is satisfiable. We illustrate our technique by giving exponential decision procedures for several variants of deterministic propositional dynamic logic