Progress, Justness and Fairness in Modal $\mu$-Calculus Formulae

TL;DR

This paper introduces template modal $fectu$-calculus formulae for verifying liveness properties under various assumptions like progress, justness, and fairness, ensuring correctness in modeling realistic system behaviors.

Contribution

It presents a novel set of template formulae in the modal $fectu$-calculus for broad applicability to liveness properties with different assumptions, with proven correctness.

Findings

Template formulae cover a wide range of liveness assumptions.

Correctness of the proposed formulae has been formally proven.

Facilitates more accurate verification of realistic system executions.

Abstract

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.