Verification diagrams are a succinct and intuitive way of representing proofs that reactive systems satisfy a given temporal property. We present a generalized verification diagram that allows representation of a proof of any property expressible by a temporal formula. We show that representation of a proof by generalized verification diagram is sound and complete.
Proceedings 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Bangalore, India (December 1995).
Postscript, PDF. © 1995, Springer Verlag.