Automata theoretic techniques for modal logics of programs.
01 January 1984
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 automation A(f) for a given formula (f), such that A(f) accepts some tree if and only if (f) is satisfiable. is satisfiable.