Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Progress, Justness and Fairness in Modal $μ$-Calculus Formulae

Myrthe Spronck, Bas Luttik, Tim Willemse

TL;DR

This work addresses spurious liveness counterexamples by combining liveness properties with completeness criteria via template formulae in the modal $\mu$-calculus. It builds a general, blocking-action–parameterised framework that unifies progress, justness, weak/strong fairness, and hyperfairness with a general PSP-based property, backed by formal correctness proofs. A central result (mucalc:gen) establishes feasibility-based applicability to finitely realisable predicates, enabling instantiations to WFA, WHFA and JA (and, with higher cost, SFA and SHFA). The approach yields practical, verifiable translations of common liveness patterns into $\mu$-calculus formulae and is demonstrated through an application to a Dekker-like starvation-freedom scenario, with avenues for extending the method to broader criteria and real-time or probabilistic settings.

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.

Progress, Justness and Fairness in Modal $μ$-Calculus Formulae

TL;DR

This work addresses spurious liveness counterexamples by combining liveness properties with completeness criteria via template formulae in the modal -calculus. It builds a general, blocking-action–parameterised framework that unifies progress, justness, weak/strong fairness, and hyperfairness with a general PSP-based property, backed by formal correctness proofs. A central result (mucalc:gen) establishes feasibility-based applicability to finitely realisable predicates, enabling instantiations to WFA, WHFA and JA (and, with higher cost, SFA and SHFA). The approach yields practical, verifiable translations of common liveness patterns into -calculus formulae and is demonstrated through an application to a Dekker-like starvation-freedom scenario, with avenues for extending the method to broader criteria and real-time or probabilistic settings.

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.
Paper Structure (30 sections, 49 theorems, 25 equations, 2 figures, 1 table)

This paper contains 30 sections, 49 theorems, 25 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Labelled Transition Systems
  4. Modal mu-Calculus
  5. Motivation
  6. Completeness Criteria
  7. Progress with Blocking Actions
  8. Justness
  9. Fairness
  10. A Generalisation of the Property Specification Liveness Patterns
  11. Template Formulae
  12. Progress
  13. Weak Fairness, Weak Hyperfairness and Justness
  14. Strong Fairness and Strong Hyperfairness
  15. Application Example
  16. ...and 15 more sections

Key Result

Theorem 16

A state in an LTS satisfies mucalc:unfair if, and only if, it does not admit $\mathcal{B}$-progressing paths that are $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

Figures (2)

  • Figure 1: The LTS for the running example.
  • Figure 2: The four types of $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating paths: finite or infinite, and without or with $\alpha_{\mathit{e}}$. Always, it has a prefix matching $\rho$ and is $\alpha_{\mathit{f}}$-free up until the first occurrence of an action in $\alpha_{\mathit{e}}$.

Theorems & Definitions (77)

  • Definition 1
  • Definition 2
  • Definition 3
  • Example 4
  • Definition 5
  • Example 6
  • Definition 7
  • Definition 7
  • Example 8
  • Definition 8
  • ...and 67 more