Myrthe Spronck: Fairness Assumptions in the Modal mu-Calculus


Event Details


The modal μ-calculus is a highly expressive logic, but its formulae are often hard to understand. We have tools for testing if a model satisfies a model μ-calculus formula, but if we are unsure of what the formula expresses we cannot draw definite conclusions from the results. To mitigate the difficulties in designing μ-calculus formulae, property specification patterns have been designed to help researchers express common properties in the μ-calculus. However, existing translations of these patterns to the modal μ-calculus only allow for the inclusion fairness assumptions to a very limited degree, even though fairness assumptions are very useful when model checking. Fairness assumptions allow the researcher to specify that certain types of property violations that may exist in the model are unrealistic and should not be considered when determining if the property is satisfied. This is often required because most of the time, when researchers model systems they abstract away from certain details such as the way scheduling is done, which then results in scenarios being represented in the model that would never occur in reality. There exists, therefore, a need for a standard and proven way of including a variety of fairness assumptions in modal μ-calculus formulae for properties. We extend the existing translations from the property specification patterns to the modal μ-calculus with ways to incorporate three common fairness assumptions: weak fairness, strong fairness and fair reachability (also known as ∞-fairness or hyperfairness) of the actions in a model. We also discuss other fairness assumptions to a lesser extend, including unconditional fairness of actions and weak fairness, strong fairness and fair reachability of parts of a model other than actions. When it comes to the patterns, we start with a detailed discussion on the global response pattern, which is one of the most commonly occurring ones. We then generalise our approach to cover other patterns as well. Correctness proofs are included for both the global response formulae and the generalised formulae. We conclude we a brief discussion of how the formulae we have presented in this thesis can be used in the model checking toolset mCRL2.