What Can Machines Know? On the Epistemic Properties of Machines
Ronald Fagin, Joseph Y. Halpern, et al.
AAAI 1986
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.
Ronald Fagin, Joseph Y. Halpern, et al.
AAAI 1986
Ronald Fagin, Joseph Y. Halpern, et al.
Journal of the ACM
Marc H. Graham, Moshe Y. Vardi
SIGMOD/PODS 1984
Moshe Y. Vardi
IEEE Software