Visual Abstractions for Temporal Verification

摘要

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 Miiller acceptance conditions, and show how they can be used to verify general temporal properties of reactive systems.