Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract)

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 A f for a given formula f , such that A f accepts some tree if and only if f is satisfiable. We illustrate our technique by giving an exponential decision procedure for deterministic propositional dynamic logic and a variant of the μ-calculus of Kozen.

Authors

• Moshe Y. Vardi
• Pierre Wolper

Keywords

No keywords are indexed for this paper.