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.

翻译：在验证转移系统的活性属性时，通常需要通过对哪些路径代表实际执行过程做出假设来排除虚假的违规路径。在逻辑公式中捕捉此类假设下属性成立的条件具有挑战性且容易出错，在模态μ演算中尤其如此。本文提出一组模态μ演算模板公式，可实例化为广泛的活性属性。我们考虑以下关于动作的假设：进展性、公正性、弱公平性、强公平性和超公平性。这些公式的正确性已得到证明。