  When verifying liveness properties on a transition system, it is often
necessary to discard spurious violating paths by making assumptions on which
paths represent realistic executions. Capturing that some property holds under
such an assumption in a logical formula is challenging and error-prone,
particularly in the modal $\mu$-calculus. In this paper, we present template
formulae in the modal $\mu$-calculus that can be instantiated to a broad range
of liveness properties. We consider the following assumptions: progress,
justness, weak fairness, strong fairness, and hyperfairness, each with respect
to actions. The correctness of these formulae has been proven.
