Generalized Verification Diagrams combine deductive and algorithmic verification to establish general temporal properties of finiteand 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 Müller acceptance conditions, and show how they
can be used to verify general temporal properties of reactive systems.
This research was supported in part by the National Science Foundation under grants CCR-95-27927 and CCR-9804100, the Defense
Advanced Research Projects Agency under NASA grant NAG2-892, ARO under grants DAAH04-95-1-0317, DAAH04-96-1-0122 and DAAG55-98-1-0471,
ARO under MURI grant DAAH04-96-1-0341, and by Army contract DABT63-96-C-0096 (DARPA).