Visual abstractions for temporal verification

Abstract

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 algorithmi-cally model checked. We present a new simple class of verification diagrams, using Mu¨ller acceptance conditions, and show how they can be used to verify general temporal properties of reactive systems.