Generalized Verification Diagrams combine deductive and algorithmic verification to establish general temporal properties of finite- and infinite-state reactive systems. The diagram serves as an abstraction of the system. This abstraction is deductively justified and algorithmically model checked. We present a new simple class of verification diagrams, using Muller acceptance conditions, and show how they can be used to verify general temporal properties of reactive systems.
In AMAST'98, Vol 1548 of LNCS, pp 28-41, Springer-Verlag, 1998.
Postscript, PDF. © 1998, Springer Verlag.