Verification of concurrent programs: The automata-theoretic framework (Q2277249)

An effective version of Wolper's temporal logic IPTL, recursive infinitary temporal logic (RITL) is introduced, and it is proved that the properties expressed in RITL can be captured by recursive automata on infinite trees. Three types of acceptance conditions (Wolper acceptance, Büchi acceptance, and Streett acceptance) for these automata are considered and shown to be of the same power. This enables to define effective equivalent transformations of recursive trees with complicated correctness conditions to trees with simpler ones (nondeterministic programs are naturally associated to their computational trees, which are recursive). This transformation technique is then applied to verification of concurrent and nondeterministic programs. Proof methods for two approaches to fair termination are developed: the method of explicit schedulers, and the method of helpful directions. The idea is that, given a computation tree of a program and a correctness condition, both defined via recursive automata, one constructs new automata which terminate iff the program is correct. If, for example, the correctness is formulated in RITL, we can express it in terms of recursive automata. Hence correctness is reduced to termination.