Temporal verification by diagram transformations

This paper presents a methodology for the verification of temporal properties of systems based on the gradual construction and algorithmic checking of fairness diagrams. Fairness diagrams correspond to abstractions of the system and its progress properties, and have a simple graphical representation.In the proposed methodology, a proof of a temporal property consists of a chain of diagram transformations, starting from a diagram representing the original system and ending with a diagram that either corresponds directly to the specification, or that can be shown to satisfy it by purely algorithmic methods. Each diagram transformation captures a natural step of the gradual process of system analysis and proof discovery. The structure of fairness diagrams simplifies reasoning about progress properties, and the graphical representation provided by the diagrams enables the user to direct the construction of the proof. The resulting methodology is complete for proving specifications written in first-order lineartime temporal logic, provided no temporal operator appears in the scope of a quantifier.