Tong Zhang, G.H. Golub, et al.
Linear Algebra and Its Applications
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. © 1986.
Tong Zhang, G.H. Golub, et al.
Linear Algebra and Its Applications
Minghong Fang, Zifan Zhang, et al.
CCS 2024
Richard M. Karp, Raymond E. Miller
Journal of Computer and System Sciences
Da-Ke He, Ashish Jagmohan, et al.
ISIT 2007