Institution: Stanford University, Department of Computer Science

Title: Specification and Verification of Concurrent Programs by For-All Automata

Author: Manna, Z ohar

Author: Pnueli, Amir

Date: November 1988

Abstract: For-all automata are non-deterministic finite-state automata over infinite sequences. They differ from conventional automata in that a sequence is accepted if all runs of the automaton over the sequence are accepting. These automata are suggested as a formalism for the specification and verification of temporal properties of concurrent programs. It is shown that they are as expressive as extended temporal logic (ETL), and, in some cases, provide a more compact representation of properties than temporal logic. A structured diagram notation is suggested for the graphical representation of these automata. A single sound and complete proof rule is presented for proving that all computations of a program have the property specified by a for-all automaton.

http://i.stanford.edu/pub/cstr/reports/cs/tr/88/1230/CS-TR-88-1230.pdf