Monotone monadic SNP and constraint satisfaction
Tomás Feder, Moshe Y. Vardi
STOC 1993
Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 (1991) 79-98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if a program PA, obtained by combining P and A, terminates. We formalize this idea in a framework of ω-automata with a recursive set of states. This unifies previous works on verification of fair termination and verification of temporal properties. © 1991.
Tomás Feder, Moshe Y. Vardi
STOC 1993
Ronald Fagin, Joseph Y. Halpern, et al.
Journal of the ACM
Stavros S. Cosmadakis, Paris C. Kanellakis, et al.
STOC 1988
Ronald Fagin, Joseph Y. Halpern, et al.
Artificial Intelligence