@inproceedings{20ba2d5b873a4619a4efaf0f48f87390,
title = "Progress, Justness and Fairness in Modal µ-Calculus Formulae",
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 = "Completeness criteria, Fairness, Justness, Liveness properties, Modal µ-calculus, Progress, Property specification",
author = "Spronck, \{Myrthe S.C.\} and Bas Luttik and Willemse, \{Tim A.C.\}",
year = "2024",
month = aug,
day = "29",
doi = "10.4230/LIPIcs.CONCUR.2024.38",
language = "English",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
pages = "38:1--38:22",
editor = "Rupak Majumdar and Alexandra Silva",
booktitle = "35th International Conference on Concurrency Theory (CONCUR 2024)",
note = "35th International Conference on Concurrency Theory, CONCUR 2024 ; Conference date: 09-09-2024 Through 13-09-2024",
}