Conference paper
Operational semantics for knowledge bases
Ronald Fagin, Yoram Moses, et al.
aaai 1994
An automata-theoretic approach to automatic verification of concurrent finite-state programs by model checking is described. The basic idea underlying this approach is that for any temporal formula we can construct an automation that accepts precisely the computations that satisfy the formula. The model-checking algorithm that results from this approach is much simpler and cleaner than tableau-based algorithms. This approach is used to extend model checking to probabilistic concurrent finite-state programs.
Ronald Fagin, Yoram Moses, et al.
aaai 1994
Ronald Fagin, Moshe Y. Vardi
STOC 1984
Ronald Fagin, Joseph Y. Halpern, et al.
PODC 1995
A.K. Chandra, Moshe Y. Vardi
SIAM Journal on Computing