Report Number: CS-TR-88-1230
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.