AUTOMATA-THEORETIC APPROACH TO AUTOMATIC PROGRAM VERIFICATION.
Moshe Y. Vardi, Pierre Wolper
LICS 1986
This article addresses the problem of designing memory-efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are modeled as automata on infinite words (Büchi automata). Verification is then reduced to checking the emptiness of the automaton resulting from the product of the program and the property. This problem is usually solved by computing the strongly connected components of the graph representing the product automaton. Here, we present algorithms that solve the emptiness problem without explicitly constructing the strongly connected components of the product graph. By allowing the algorithms to err with some probability, we can implement them with a randomly accessed memory of size O(n) bits, where n is the number of states of the graph, instead of O(n log n) bits that the presently known algorithms require. © 1992 Kluwer Academic Publishers.
Moshe Y. Vardi, Pierre Wolper
LICS 1986
Ronald Fagin, Joseph Y. Halpern, et al.
PODC 1995
Ronald Fagin, Moshe Y. Vardi
STOC 1984
Ronald Fagin, Yoram Moses, et al.
aaai 1994