Progress, Justness and Fairness in Modal $\mu$-Calculus Formulae
Logic in Computer Science
2024-07-12 v1
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 -calculus. In this paper, we present template formulae in the modal -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.
Keywords
Cite
@article{arxiv.2407.08060,
title = {Progress, Justness and Fairness in Modal $\mu$-Calculus Formulae},
author = {Myrthe Spronck and Bas Luttik and Tim Willemse},
journal= {arXiv preprint arXiv:2407.08060},
year = {2024}
}