Authors
Moshe Y Vardi, Pierre Wolper
Publication date
1984/12/1
Book
Proceedings of the sixteenth annual acm symposium on theory of computing
Pages
446-456
Description
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 an exponential decision procedure for deterministic propositional dynamic logic and a variant of the μ-calculus of Kozen.
Total citations
Scholar articles
MY Vardi, P Wolper - Proceedings of the sixteenth annual acm symposium …, 1984