2026-08-03T14:40:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20810 2024-08-29T05:40:58Z ddc:004 open_access

Progress, Justness and Fairness in Modal μ-Calculus Formulae Spronck, Myrthe S. C. Luttik, Bas Willemse, Tim A. C. Modal μ-calculus Property specification Completeness criteria Progress Justness Fairness Liveness properties 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Myrthe S. C. Spronck and Bas Luttik and Tim A. C. Willemse 2024 Is Part Of LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2024.38 urn:nbn:de:0030-drops-208102 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.38 eng https://creativecommons.org/licenses/by/4.0/legalcode