When verifying liveness properties on transition systems, it is often necessary to discard spurious counterexamples. This can be done through the application of completeness criteria: assumptions on which paths represent realistic executions of the modelled system. To support verification of properties under completeness criteria, we have developed template modal mu-calculus formulae that can be instantiated to capture a broad range of liveness properties under the following completeness criteria: progress, justness, weak fairness, strong fairness and hyperfairness. In this talk, I will present the formulae instantiated for the starvation freedom property of mutual exclusion algorithms, and show how the completeness criteria have been represented.

This is joint work with Bas Luttik and Tim Willemse