The method of Invisible Invariants was developed originally in order to verify safety properties of parameterized systems in a fully automatic manner. The method is based on (1) a project-and-generalizege heuristic to generate auxiliary constructs for parameterized systems, and (2) a small model theorem implying that it is sufficient to check the validity of logical assertions of certain syntactic form on small instantiations of a parameterized system. The approach can be generalized to any deductive proof rule that (1) requires auxiliary constructs that can be generated by prject-and-generalize, and (2) the premises resulting when using the constructs are of the form covered by the small model theorem.
The method of invisible ranking, presented here, generalizes the approach to liveness properties of parameterized systems. Starting with a proof rule and cases where the method can be applied almost "as is," the paper progresses to develop deductive proof rules for liveness and extend the small model theorem to cover many intricate families of parameterized systems.