Shashanka Ubaru, Lior Horesh, et al.
Journal of Biomedical Informatics
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.
Shashanka Ubaru, Lior Horesh, et al.
Journal of Biomedical Informatics
Joseph Y. Halpern, Moshe Y. Vardi
STOC 1988
R.A. Brualdi, A.J. Hoffman
Linear Algebra and Its Applications
Jaione Tirapu Azpiroz, Alan E. Rosenbluth, et al.
SPIE Photomask Technology + EUV Lithography 2009