BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-88-1230
       ENTRY:: April 24, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Specification and Verification of Concurrent Programs by
               For-All Automata
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: November 1988
       PAGES:: 44
    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.
       NOTES:: [Adminitrivia V1/Prg/19950424]
         END:: STAN//CS-TR-88-1230