In this paper we present a visual approach to proving progress properties of parameterized systems using induction on verification diagrams. The inductive hypothesis is represented by an automaton and is based on a state-dependent order on process indices, for increased flexibility. This approach yields more intuitive proofs for progress properties and simpler verification conditions that are more likely to be proved automatically.
Appeared in CAV'99, pp 25-43, LNCS 1633, Springer-Verlag, 1999.
Corrected version: Postscript, PDF. © 1999, Springer Verlag.