Eindhoven University of Technology, The
Netherlandsm.s.c.spronck@tue.nlhttps://orcid.org/0000-0003-2909-7515Eindhoven
University of Technology, The
Netherlandss.p.luttik@tue.nlhttps://orcid.org/0000-0001-6710-8436 Eindhoven
University of Technology, The
Netherlandst.a.c.willemse@tue.nlhttps://orcid.org/0000-0003-3049-7962 Myrthe
S.C. Spronck, Bas Luttik and Tim A.C. Willemse [500]Theory of computation
Modal and temporal logics

###### Acknowledgements.

We thank an anonymous reviewer for the observation that weak and strong
hyperfairness must be distinguished.Rupak Majumdar and Alexandra Silva 2 35th
International Conference on Concurrency Theory (CONCUR 2024) CONCUR 2024
CONCUR 2024 September 9–13, 2024 Calgary, Canada 311 25

# Progress, Justness and Fairness in Modal $\mu$-Calculus Formulae

Myrthe S. C. Spronck  Bas Luttik  Tim A. C. Willemse

###### 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 $\mu$-calculus. In this paper, we present template
formulae in the modal $\mu$-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:

Modal $\mu$-calculus, Property specification, Completeness criteria, Progress,
Justness, Fairness, Liveness properties

##  1 Introduction

Formal verification through model checking requires a formalisation of the
properties of the modelled system as formulae in some logic, such as LTL [33],
CTL [18] or the modal $\mu$-calculus [30]. In this paper, we focus on the
modal $\mu$-calculus, a highly expressive logic used in established model
checkers such as mCLR2 [11] and CADP [20].

A frequently encountered problem when checking liveness properties is that
spurious violations are found, such as paths on which some components never
make progress. Often, such paths do not represent realistic executions of the
system. It is then a challenge to restrict verification to those paths that do
represent realistic system executions. For this, we use completeness criteria
[22, 23]: predicates on paths that say which paths are to be regarded as
realistic runs of the system. These runs are called complete runs. Examples of
completeness criteria are progress, justness and fairness.

It turns out that writing a modal $\mu$-calculus formula for a property being
satisfied under a completeness criterion is non-trivial. Since the
$\mu$-calculus is a branching-time logic, we cannot separately formalise when
a path is complete and when it satisfies the property, and then combine the
two formalisations with an implication. Instead, a more intricate integration
of both aspects of a path is needed. Our aim is to achieve such an integration
for a broad spectrum of liveness properties and establish the correctness of
the resulting formulae. To this end, we shall consider a template property
that can be instantiated to a plethora of liveness properties and, in
particular, covers all liveness property patterns of [17]. Then, we present
modal $\mu$-calculus formulae integrating the completeness criteria of
progress, justness, weak fairness, strong fairness, and hyperfairness with
this template property.

As discussed in [24], for the formulation of realistic completeness criteria
it is sometimes necessary to give special treatment to a set of blocking
actions, i.e., actions that require cooperation of the environment in which
the modelled system operates. Our template formulae are therefore
parameterised with a set of blocking actions. We shall see that, given a set
of blocking actions, there are two different interpretations of hyperfairness;
we call these weak and strong hyperfairness.

Regarding our presented formulae, the progress formula is similar to those
commonly used for liveness properties even when completeness is not explicitly
considered. Our formulae for justness, weak fairness and weak hyperfairness
only subtly differ from each other. We characterise the similarities these
three share and give a generic formula that can be adapted to represent all
completeness criteria that meet these conditions. Lastly, we observe that
strong fairness and strong hyperfairness do not meet these conditions. We give
alternative formulae that are significantly more complex. Whether more
efficient formulae for these completeness criteria exist remains an open
problem.

Modal $\mu$-calculus formulae are often hard to interpret. Accordingly, it is
not trivial to see that our formulae indeed express the integration of
liveness properties with completeness criteria. We have therefore included
elaborate correctness proofs in the appendices.

Our work is essentially a generalisation along two dimensions (viz., the
completeness criterion and the liveness property) of the works of [35] and [7,
37]. In [35], the tool PASS is presented for automatically translating common
property patterns into modal $\mu$-calculus formulae. Some of those patterns
integrate an assumption that excludes paths deemed unrealistic, but since the
exact assumption is not stated separately, we cannot make a formal comparison
with our approach. In [7], a formula for justness is presented, covering one
of the properties we cover. This formula forms the basis for our justness,
weak fairness and weak hyperfairness formulae. Our formulae for strong
fairness and strong hyperfairness are in part inspired by the formula for
termination under strong fairness presented in [37].

The organisation of this paper is as follows. In section 2 we recap the
relevant definitions on labelled transition systems, as well as the syntax and
semantics of the modal $\mu$-calculus. In section 3, we motive our work with
an example, and in section 4 we give the completeness criteria we cover in
this paper. In section 5, we formally identify the class of liveness
properties we study and relate it to a popular class of properties. Our
template formulae are presented in section 6, combining the completeness
criteria from section 4 with the property template from section 5. We give a
small application example in section 7 and discuss the scope of our work in
section 8. Finally, we give our conclusions in section 9.

##  2 Preliminaries

We represent models as labelled transition systems (LTSs). In this section, we
briefly introduce the relevant definitions on LTSs, as well as the modal
$\mu$-calculus.

###  2.1 Labelled Transition Systems

######  Definition 2.1.

An LTS is a tuple
$M=(\mathcal{S},s_{\mathit{init}},\mathit{Act},\mathit{Trans})$ where

  * •

$\mathcal{S}$ is a set of states,

  * •

$s_{\mathit{init}}\in\mathcal{S}$ is the initial state,

  * •

$\mathit{Act}$ is a set of action labels, also referred to as the alphabet of
the LTS, and

  * •

$\mathit{Trans}\subseteq\mathcal{S}\times\mathit{Act}\times\mathcal{S}$ is a
transition relation.

In this paper, we only consider finite LTSs, such as the kind used in finite-
state model checking. In particular, our formulae are proven correct under the
assumption that $\mathit{Act}$ is finite. We write
$s\xrightarrow{a}s^{\prime}$ as shorthand for
$(s,a,s^{\prime})\in\mathit{Trans}$, and for a given transition
$t=(s,a,s^{\prime})$ we write $\mathit{src}(\mathit{t})=s$,
$\mathit{act}(\mathit{t})=a$ and $\mathit{trgt}(\mathit{t})=s^{\prime}$.

For the definitions below, we fix an LTS
$M=(\mathcal{S},s_{\mathit{init}},\mathit{Act},\mathit{Trans})$.

######  Definition 2.2.

A _path_ is an $($alternating$)$ sequence $\pi=s_{0}t_{1}s_{1}t_{2}\ldots$ of
states $s_{0},s_{1},\ldots\in\mathcal{S}$ and transitions
$t_{1},t_{2},\ldots\in\mathit{Trans}$. A path must start with a state, and
must be either infinite, or end in a state. In the latter case, the end of the
path is referred to as the _final state_. For all $i\geq 0$, $t_{i+1}$ must
satisfy $\mathit{src}(\mathit{t_{i+1}})=s_{i}$ and
$\mathit{trgt}(\mathit{t_{i+1}})=s_{i+1}$.

We sometimes refer to transitions on a path as steps. We say an action occurs
on a path if a transition labelled with that action is on the path. We call a
path on which no action in some set $\alpha$ occurs an _$\alpha$ -free_ path.
One path can be appended to another: let
$\pi^{\prime}=s_{0}^{\prime}t_{1}^{\prime}s_{1}^{\prime}\ldots
t_{n}^{\prime}s_{n}^{\prime}$ and
$\pi^{\prime\prime}=s_{0}^{\prime\prime}t_{1}^{\prime\prime}s_{1}^{\prime\prime}\ldots$,
where $\pi^{\prime}$ must be finite and $\pi^{\prime\prime}$ may be finite or
infinite. Then the path $\pi$ defined as $\pi^{\prime\prime}$ appended to
$\pi^{\prime}$ is written as
$\pi=\pi^{\prime}\cdot\pi^{\prime\prime}=s_{0}^{\prime}t_{1}^{\prime}s_{1}^{\prime}\ldots
t_{n}^{\prime}s_{n}^{\prime}t_{1}^{\prime\prime}s_{1}^{\prime\prime}\ldots$.
This is only allowed when $s_{n}^{\prime}=s_{0}^{\prime\prime}$.

######  Definition 2.3.

We say that:

  * •

A transition $t\in\mathit{Trans}$ is _enabled_ in a state $s\in\mathcal{S}$
if, and only if, $\mathit{src}(\mathit{t})=s$.

  * •

An action $a\in\mathit{Act}$ is _enabled_ in a state $s\in\mathcal{S}$ if, and
only if, there exists a transition $t\in\mathit{Trans}$ with
$\mathit{act}(\mathit{t})=a$ that is enabled in $s$.

  * •

An action $a\in\mathit{Act}$ is _perpetually enabled_ on a path $\pi$ if $a$
is enabled in every state of $\pi$.

  * •

An action $a\in\mathit{Act}$ is _relentlessly enabled_ on a path $\pi$ if
every suffix of $\pi$ contains a state in which $a$ is enabled.

  * •

A state without enabled actions is called a _deadlock state_.

Every action that is perpetually enabled on a path is also relentlessly
enabled on that path.

###  2.2 Modal $\mu$-Calculus

The modal $\mu$-calculus is given in [30]. Our presentation of the logic is
based on [8, 9, 10, 27].

The syntax of the modal $\mu$-calculus is described by the following grammar,
in which $a$ ranges over the set of actions $\mathit{Act}$, and $X$ ranges
over a set of formal variables $\mathit{Var}$.

$\phi,\psi::=\mathit{ff}\mid
X\mid\neg\phi\mid\phi\lor\psi\mid\langle\mathit{a}\rangle\phi\mid\mu\mathit{X}.\mathit{\phi}$

Here $\mathit{ff}$ is false; $\neg$ represents negation; $\lor$ is
disjunction; $\langle\mathit{\leavevmode\nobreak\ }\rangle$ is the diamond
operator; and $\mu$ is the least fixpoint operator. We say that
$\mu\mathit{X}.\mathit{\phi}$ binds $X$ in $\phi$. Variables that are unbound
in a formula are free, and a formula without free variables is closed.

A modal $\mu$-calculus formula $\phi$ must both adhere to this grammar and be
_syntactically monotonic_ , meaning that for every occurrence of $\mu X.\psi$
in $\phi$, every free occurrence of $X$ in $\psi$ must always be preceded by
an even number of negations.

We give the semantics of a modal $\mu$-calculus formula $\phi$ with respect to
an arbitrary LTS
$M=(\mathcal{S},s_{\mathit{init}},\mathit{Act},\mathit{Trans})$ and
environment $\mathit{e}:\mathit{Var}\to 2^{\mathcal{S}}$.

$\displaystyle\llbracket\mathit{ff}\rrbracket_{\mathit{e}}^{M}=\emptyset$
$\displaystyle\llbracket\phi\lor\psi\rrbracket_{\mathit{e}}^{M}=\llbracket\phi\rrbracket_{\mathit{e}}^{M}\cup\llbracket\psi\rrbracket_{\mathit{e}}^{M}$
$\displaystyle\llbracket X\rrbracket_{\mathit{e}}^{M}=\mathit{e}(X)$
$\displaystyle\llbracket\langle\mathit{a}\rangle\phi\rrbracket_{\mathit{e}}^{M}=\left\\{s\in\mathcal{S}\mid\exists_{s^{\prime}\in\mathcal{S}}.s\xrightarrow{a}s^{\prime}\land
s^{\prime}\in\llbracket\phi\rrbracket_{\mathit{e}}^{M}\right\\}$
$\displaystyle\llbracket\neg\phi\rrbracket_{\mathit{e}}^{M}=\mathcal{S}\setminus\llbracket\phi\rrbracket_{\mathit{e}}^{M}$
$\displaystyle\llbracket\mu\mathit{X}.\mathit{\phi}\rrbracket_{\mathit{e}}^{M}=\bigcap\left\\{\mathcal{S}^{\prime}\subseteq\mathcal{S}\mid\mathcal{S}^{\prime}\supseteq\llbracket\phi\rrbracket_{\mathit{e}[X:=\mathcal{S}^{\prime}]}^{M}\right\\}$

In contexts where the model is fixed, we drop the $M$ from
$\llbracket\phi\rrbracket_{\mathit{e}}^{M}$. Additionally, we drop
$\mathit{e}$ when the environment does not affect the semantics of the
formula, e.g. with closed formulae.

We use conjunction, $\land$, and implication, $\Rightarrow$, as the usual
abbreviations. We also add several abbreviations:
$\mathit{tt}=\neg\mathit{ff}$ for true;
$[\mathit{a}]\phi=\neg\langle\mathit{a}\rangle\neg\phi$ for the box operator;
and $\nu X.\phi=\neg\mu X.(\neg\phi[X:=\neg X])$ for the greatest fixpoint.

To express formulae more compactly, we extend our syntax to allow regular
expressions over finite sets of actions to be used in the box and diamond
operators. Since we limit this to finite sets of actions, the syntactical
extension does not increase the expressivity of the logic, it merely
simplifies the presentation. This is a common extension of the $\mu$-calculus
syntax, for instance shown in [27], based on the operators defined for PDL
[19]. We overload the symbol for a single action to also represent the
singleton set containing that action. We use union, intersection, set
difference, and set complement to describe sets of actions as usual. Regular
expressions over sets of actions, henceforth referred to as _regular formulae_
, are defined by the following grammar:

$R,Q::=\varepsilon\mid\alpha\mid R\cdot Q\mid R+Q\mid\mathit{R}^{\star}$

The empty sequence is represented by $\varepsilon$, and $\alpha$ ranges over
sets of actions. The symbol $\cdot$ represents concatenation, $+$ the union of
formulae, and $\mathit{}^{\star}$ is closure under repetition.

We define the meaning of the diamond operator over the new regular formulae as
abbreviations of standard modal $\mu$-calculus formulae:

$\displaystyle\langle\mathit{\varepsilon}\rangle\phi$ $\displaystyle=\phi$
$\displaystyle\langle\mathit{\alpha}\rangle\phi$
$\displaystyle=\bigvee_{a\in\alpha}\langle\mathit{a}\rangle\phi$
$\displaystyle\langle\mathit{R\cdot Q}\rangle\phi$
$\displaystyle=\langle\mathit{R}\rangle\langle\mathit{Q}\rangle\phi$
$\displaystyle\langle\mathit{R+Q}\rangle\phi$
$\displaystyle=\langle\mathit{R}\rangle\phi\lor\langle\mathit{Q}\rangle\phi$
$\displaystyle\langle\mathit{\mathit{R}^{\star}}\rangle\phi$
$\displaystyle=\mu\mathit{X}.(\mathit{\langle\mathit{R}\rangle X\lor\phi})$

The box operator is defined dually. We say a path $\pi$ _matches_ a regular
formula $R$ if the sequence of actions on $\pi$ is in the language of $R$.

##  3 Motivation

When analysing algorithms and systems, there are many different properties
which may need to be checked. For instance, when model checking mutual
exclusion algorithms we want to check linear properties such as mutual
exclusion and starvation freedom, but also branching properties such as
invariant reachability of the critical section. The modal $\mu$-calculus,
which subsumes even CTL⋆, is able to express all these properties and more,
and is therefore used in toolsets such as mCLR2 [11] and CADP [20].

An issue that is frequently encountered when checking liveness properties in
particular, is that the model admits executions that violate the property but
do not represent realistic executions of the real system. For example, models
of algorithms that contain a busy waiting loop usually admit executions where
processes do nothing except wait. Infinite loops can also be introduced by
abstractions of reality, such as modelling a loop to represent an event that
occurs an arbitrary, but finite, number of times. Counterexamples that are due
to such modelling artefacts obscure whether the property is satisfied on all
realistic executions. The problem we address in this paper is how to avoid
such counterexamples and check properties only on realistic executions. We
illustrate the problem with an example, which we also employ as a running
example throughout this paper.

######  Example 3.1.

Consider the coffee machine modelled in Figure 1. When a user places an
$\mathit{order}$ for one or more cups of coffee, they are required to scan
their payment $\mathit{card}$. If the user prefers using coinage, they switch
the machine to its alternate mode ($\mathit{to\\_cash}$), and then pay in
$\mathit{cash}$. In the alternate mode, the machine can be switched back using
$\mathit{to\\_card}$. After payment, the machine will $\mathit{brew}$ the
cup(s) of coffee. This is modelled as a non-deterministic choice between a
looping and a final $\mathit{brew}$ action, since at least one cup was
ordered. Finally, the coffee is $\mathit{deliver}$ed and the machine awaits
the next order.

We consider three example properties.

  1. 1.

_Single order_ : whenever an $\mathit{order}$ is made, there may not be a
second $\mathit{order}$ until a $\mathit{deliver}$ has taken place,
$[\mathit{\mathit{\mathit{Act}}^{\star}\cdot\mathit{order}\cdot\mathit{\overline{\mathit{\mathit{deliver}}}}^{\star}\cdot\mathit{order}}]\mathit{ff}$.

  2. 2.

_Inevitable delivery_ : whenever an $\mathit{order}$ is made, there will
inevitably be an occurrence of $\mathit{deliver}$,
$[\mathit{\mathit{\mathit{Act}}^{\star}\cdot\mathit{order}}]\mu
X.(\langle\mathit{\mathit{Act}}\rangle\mathit{tt}\land[\mathit{\overline{\mathit{\mathit{deliver}}}}]X)$.

  3. 3.

_Possible delivery_ : it is invariantly possible to eventually execute the
$\mathit{deliver}$ action,
$[\mathit{\mathit{\mathit{Act}}^{\star}}]\langle\mathit{\mathit{\mathit{Act}}^{\star}\cdot\mathit{deliver}}\rangle\mathit{tt}$.

The described problem occurs with _inevitable delivery_ :
$s_{0}t_{1}s_{1}t_{4}(s_{3}t_{6})^{\omega}$ is a violating path, on which
infinitely many cups are part of the same order. Similarly,
$s_{0}t_{1}(s_{1}t_{2}s_{2}t_{3})^{\omega}$ violates the property because the
user never decides on a payment method. The first counterexample represents an
impossible scenario, and the second gives information on problematic user
behaviour but tells us little about the machine itself.

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$s_{4}$$t_{1}$:$\mathit{order}$$t_{2}$:$\mathit{to\\_cash}$$t_{3}$:$\mathit{to\\_card}$$t_{4}$:$\mathit{card}$$t_{5}$:$\mathit{cash}$$t_{6}$:$\mathit{brew}$$t_{7}$:$\mathit{brew}$$t_{8}$:$\mathit{deliver}$
Figure 1: The LTS for the running example.

The kind of spurious counterexamples discussed in the example above primarily
occur when checking liveness properties. We therefore focus on liveness
properties, such as _inevitable delivery_ , in this paper. We will briefly
discuss safety properties in section 8.

There are ad-hoc solutions to exclude unrealistic counterexamples, e.g.
altering the model to remove the unrealistic executions, or tailoring the
formula to exclude specific problematic counterexamples [26]. Such ad-hoc
solutions are undesirable because they clutter the model or the formula, and
are therefore error-prone. We aim for a more generic solution, of which the
correctness can be established once and for all. Such a generic solution
requires, on the one hand, a general method to distinguish between realistic
and unrealistic executions, and, on the other hand, a general class of
liveness properties.

A general method to distinguish between realistic and unrealistic executions
is provided by _completeness criteria_ [22, 23], i.e., predicates on paths
that label some as complete and all others as incomplete. If a property is
satisfied on all complete paths, it is satisfied under the given completeness
criterion. Completeness criteria give us a model-independent way to determine
which paths are unrealistic, and therefore a generic solution to the stated
problem. Depending on the property and the model, we may prefer a different
completeness criterion. We therefore consider several criteria instead of
fixing one specific criterion. These completeness criteria are discussed in
section 4.

To find a general class of liveness properties, we take the _property
specification patterns_ (PSP) of [17] as a starting point. Since the modal
$\mu$-calculus as presented in Section 2.2 supports references to action
occurrences but not state information, we specifically interpret these
patterns on action occurrences. Our first contribution, in section 5, will be
to characterise a class of liveness properties that subsumes all liveness
properties expressible in PSP. Our second and main contribution is then
presented in section 6, where we combine the identified completeness criteria
with our class of liveness properties, yielding template formulae for each
combination.

##  4 Completeness Criteria

It is often assumed, sometimes implicitly, that as long as a system is capable
of executing actions, it will continue to do so [25]. One could consider this
the “default” completeness criterion, also known as _progress_ [22]; it says
that only paths that are infinite or end in a deadlock state model complete
runs and are hence complete paths. We first present a modified version of the
progress assumption that allows some actions to be blocked by the environment.
We then define the other completeness criteria considered in this paper. As
already remarked in the previous section, the modal $\mu$-calculus is most
suited to reasoning about action occurrences. Hence, we focus on completeness
criteria defined on action labels. For more general definitions on sets of
transitions, see [25].

###  4.1 Progress with Blocking Actions

In [24], it is argued that it is useful to consider some actions of an LTS as
blocking. A blocking action is an action that depends on participation by the
environment of the modelled system. Consequently, even when such an action is
enabled in a state because the system is willing to perform it, it may not be
possible for the action to occur because the environment is uncooperative. In
this paper, we refer to the set of blocking actions as
$\mathcal{B}\subseteq\mathit{Act}$, and the set of non-blocking actions as
$\overline{\mathit{\mathcal{B}}}=\mathit{Act}\setminus\mathcal{B}$. Which
actions are in $\mathcal{B}$ is a modelling choice.

The default progress assumption can be adapted to account for blocking actions
[21, 25].

######  Definition 4.1.

A state $s\in\mathcal{S}$ is a _$\mathcal{B}$ -locked state_ if, and only if,
all actions enabled in $s$ are in $\mathcal{B}$. A path $\pi$ is
_$\mathcal{B}$ -progressing_ if, and only if, it is infinite or ends in a
$\mathcal{B}$-locked state.

We refer to the assumption that only $\mathcal{B}$-progressing paths represent
complete executions as $\mathcal{B}$-progress. The “default” completeness
criterion is equivalent to $\emptyset$-progress.

######  Example 4.2.

Consider Figure 1. Here, $\mathit{order}$ is an environment action, since it
involves the user. If we do not assume that there will always be a next user,
we should add $\mathit{order}$ to $\mathcal{B}$. In some cases, we may want to
consider the possibility that the machine is broken and not capable of
producing coffee. In those cases, we should add $\mathit{brew}$ to
$\mathcal{B}$. Our choice of $\mathcal{B}$ affects which paths are
progressing: $s_{0}t_{1}s_{1}t_{4}s_{3}$ is not $\emptyset$-progressing, but
it is $\\{\mathit{brew}\\}$-progressing.

All completeness criteria we discuss in this paper are parameterised with a
set of blocking actions. The justness and fairness assumptions discussed in
the remainder of this section label paths as incomplete if certain actions do
not occur. Since it can never be assumed that the environment supports the
occurrence of blocking actions, we do not want justness and fairness to label
paths as incomplete due to the non-occurrence of blocking actions.

For readability the prefix $\mathcal{B}$\- will sometimes be dropped from the
names of the completeness criteria and their acronyms. From this point, we
will always discuss completeness criteria with respect to a set of blocking
actions.

###  4.2 Justness

Justness [21, 25] is a natural extension of progress to exclude infinite paths
instead of finite paths. The idea is that in addition to the system as a whole
progressing, individual components in that system should also be able to make
progress unless they are prevented from doing so by other components. It is a
weaker, and hence frequently more justifiable, assumption than the fairness
assumptions we cover in the next section. In its original presentation,
justness is defined with respect to sets of transitions. Which components
contribute to a transition and how they contribute to them determines which
transitions interfere with each other. We here consider justness defined with
respect to actions instead, based on [7]. We do not go into how it is
determined which actions interfere with each other here. For discussions on
this topic and when the two definitions coincide, see [6, 7, 21].

Intuitively, justness of actions says that if an action $a$ is enabled at some
point of a path, then eventually some action that can interfere with the
occurrence of $a$ must occur in that path. That action may be $a$ itself. In
order to formalise the concept of interference, we require the concept of a
_concurrency relation on actions_ ,
$\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$.

######  Definition 4.3.

Relation
$\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}\subseteq\mathit{Act}\times\mathit{Act}$
is a _concurrency relation on actions_ if, and only if:

  1. 1.

$\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$ is irreflexive, and

  2. 2.

for all $a\in\mathit{Act}$, if $\pi$ is a path from a state $s$ in which $a$
is enabled to a state $s^{\prime}\in\mathcal{S}$ such that
$a\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}b$ for all actions
$b$ occurring in $\pi$, then $a$ is enabled in $s^{\prime}$.

We write
$\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}$ for the
complement of $\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$. Note
that $\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$ may be
asymmetric.

Read $a\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}b$ as “$a$ is
concurrent with $b$”, and
$a\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}b$ as
“$b$ interferes with $a$” or “$b$ eliminates $a$”. A labelled transition
system can be extended with a concurrency relation on actions, which produces
a _labelled transition system with concurrency_ (LTSC).

We here present the definition for justness of actions with blocking actions.

######  Definition 4.4.

A path $\pi$ satisfies _$\mathcal{B}$ -justness of actions_ _(
$\mathcal{B}$-JA)_ if, and only if, for each action
$a\in\overline{\mathit{\mathcal{B}}}$ that is enabled in some state $s$ in
$\pi$, an action $a^{\prime}\in\mathit{Act}$ occurs in the suffix
$\pi^{\prime}$ of $\pi$ starting in $s$ such that
$a\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}a^{\prime}$.

######  Example 4.5.

Consider Figure 1, specifically the path
$s_{0}t_{1}(s_{1}t_{2}s_{2}t_{3})^{\omega}$. On this path the user keeps
switching the mode of the machine, without paying. To see if this path
satisfies $\emptyset$-JA, we need a concrete
$\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$. Consider a
$\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$ such that
$\mathit{card}\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}\mathit{to\\_cash}$,
$\mathit{cash}\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}\mathit{to\\_card}$,
and $a\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}a$
for all action labels $a$. These are all required for
$\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$ to be a valid
concurrency relation. This is because by 4.3,
$\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$ must be
irreflexive, and when an action is enabled it must remain enabled on any path
on which no interfering action occurs. Since $\mathit{card}$ is enabled in
$s_{1}$ but not $s_{2}$, it must be the case that
$\mathit{card}\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}\mathit{to\\_cash}$.
Similarly, we must have
$\mathit{cash}\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}\mathit{to\\_card}$.
With such a concurrency relation, the path satisfies $\emptyset$-JA since
every action that is enabled is subsequently eliminated. In this LTS, there is
no valid choice of $\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$
that makes this path violate $\emptyset$-JA. However, if we modify Figure 1 by
replacing both $\mathit{card}$ and $\mathit{cash}$ with the action
$\mathit{pay}$, then 4.3 does not enforce that $\mathit{to\\_cash}$ and
$\mathit{to\\_card}$ interfere with the actions on $t_{4}$ and $t_{5}$, since
$\mathit{pay}$ is enabled in both $s_{1}$ and $s_{2}$. We can choose whether
$\mathit{pay}\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}\mathit{to\\_cash}$
and
$\mathit{pay}\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}\mathit{to\\_card}$.
If $\mathit{pay}$ is concurrent with both, then the path
$s_{0}t_{1}(s_{1}t_{2}s_{2}t_{3})^{\omega}$ violates $\emptyset$-JA. If either
interferes with $\mathit{pay}$, then the path satisfies $\emptyset$-JA.

###  4.3 Fairness

There are situations where we want to exclude a larger set of infinite paths
than those excluded by justness, or where we do not have a concurrency
relation. For this, we can use what are called _fairness assumptions_ in the
literature. These are a class of predicates on paths that distinguish between
_fair_ and _unfair_ infinite paths. It is assumed that only the fair paths are
complete. For an overview of many common fairness assumptions, see [25]. In
this paper, we consider weak fairness of actions, strong fairness of actions,
and (weak and strong) hyperfairness of actions. Each of the assumptions we
discuss has the general shape, adapted from [3], “if it is sufficiently often
possible for an action to occur, it will occur sufficiently often”. What it
means for an action to be “sufficiently often possible” and “occur
sufficiently often” depends on the exact assumption.

We first discuss _weak fairness of actions_ , which says that actions that are
always enabled must eventually occur. It is one of the most commonly discussed
fairness assumptions. We define weak fairness of actions formally, with
respect to a set of blocking actions $\mathcal{B}$.

######  Definition 4.6.

A path $\pi$ satisfies _$\mathcal{B}$ -weak fairness of actions_ _(
$\mathcal{B}$-WFA)_ if, and only if, for every suffix $\pi^{\prime}$ of $\pi$,
every action $a\in\overline{\mathit{\mathcal{B}}}$ that is perpetually enabled
in $\pi^{\prime}$ occurs in $\pi^{\prime}$.

######  Example 4.7.

Consider again Figure 1, with $\mathit{card}$ and $\mathit{cash}$ both
replaced by $\mathit{pay}$. Then the path
$s_{0}t_{1}(s_{1}t_{2}s_{2}t_{3})^{\omega}$ violates $\emptyset$-WFA, since
$\mathit{pay}$ is perpetually enabled in a suffix of this path without
occurring. If there are two separate actions for paying with cash or card, the
path satisfies $\emptyset$-WFA because no actions are perpetually enabled in
any suffix.

Next, _strong fairness of actions_ says that on a path, all actions that are
enabled infinitely often, must occur infinitely often. Formally, we define
strong fairness of actions as:

######  Definition 4.8.

A path $\pi$ satisfies _$\mathcal{B}$ -strong fairness of actions_ _(
$\mathcal{B}$-SFA)_ if, and only if, for every suffix $\pi^{\prime}$ of $\pi$,
every action $a\in\overline{\mathit{\mathcal{B}}}$ that is relentlessly
enabled in $\pi^{\prime}$ occurs in $\pi^{\prime}$.

Strong fairness is a stronger assumption than weak fairness, since it
classifies more paths as incomplete. This follows from perpetual enabledness
implying relentless enabledness.

######  Example 4.9.

The path $s_{0}t_{1}(s_{1}t_{2}s_{2}t_{3})^{\omega}$ in Figure 1 satisfies
$\emptyset$-WFA since there are no perpetually enabled actions in any suffix
of the path. However, $\mathit{cash}$ is relentlessly enabled in suffixes of
this path, and yet does not occur. Hence, this path violates $\emptyset$-SFA.

Finally, we discuss _hyperfairness of actions_. Informally, it says that on
all fair paths, every action that can always become enabled must occur
infinitely often. The idea is that if there is always a reachable future where
the action occurs, then it is merely unlucky if the action does not occur
infinitely often. The concept of hyperfairness is introduced and named in [4].
For our presentation of hyperfairness, we use the generalisation from [31]. We
first formalise what it means that an action “can become” enabled, by defining
_reachability_.

######  Definition 4.10.

We say that:

  * •

A state $s\in\mathcal{S}$ is _$\mathcal{B}$ -reachable_ from some state
$s^{\prime}\in\mathcal{S}$ if, and only if, there exists a $\mathcal{B}$-free
path starting in $s^{\prime}$ that ends in $s$.

  * •

An action $a\in\mathit{Act}$ is _$\mathcal{B}$ -reachable_ from some state
$s\in\mathcal{S}$ if, and only if, there exists a state
$s^{\prime}\in\mathcal{S}$ that is $\mathcal{B}$-reachable from $s$ and in
which $a$ is enabled.

  * •

A state $s\in\mathcal{S}$ or action $a\in\mathit{Act}$ is _perpetually
$\mathcal{B}$-reachable_ on a path $\pi$ if, and only if, it is
$\mathcal{B}$-reachable from every state of $\pi$.

  * •

A state $s\in\mathcal{S}$ or action $a\in\mathit{Act}$ is _relentlessly
$\mathcal{B}$-reachable_ on a path $\pi$ if, and only if, every suffix of
$\pi$ contains a state from which it is $\mathcal{B}$-reachable.

From the intuitive description of hyperfairness, it is clear it is a variant
of weak or strong fairness with reachability instead of enabledness, giving us
two possible definitions of hyperfairness. We name the two interpretations
weak hyperfairness and strong hyperfairness respectively. Both interpretations
of hyperfairness are reasonable, and in fact when not considering blocking
actions, they coincide [31]. However, this is not the case when blocking
actions are included in the definitions. We therefore consider both variants.

######  Definition 4.11.

A path $\pi$ satisfies _weak $\mathcal{B}$-hyperfairness of actions_ _(
$\mathcal{B}$-WHFA)_ if, and only if, for every suffix $\pi^{\prime}$ of
$\pi$, every action $a\in\overline{\mathit{\mathcal{B}}}$ that is perpetually
$\mathcal{B}$-reachable in $\pi^{\prime}$ occurs in $\pi^{\prime}$.

######  Definition 4.12.

A path $\pi$ satisfies _strong $\mathcal{B}$-hyperfairness of actions_ _(
$\mathcal{B}$-SHFA)_ if, and only if, for every suffix $\pi^{\prime}$ of
$\pi$, every action $a\in\overline{\mathit{\mathcal{B}}}$ that is relentlessly
$\mathcal{B}$-reachable in $\pi^{\prime}$ occurs in $\pi^{\prime}$.

Since enabledness implies reachability, WHFA is stronger than WFA, and SHFA is
stronger than SFA. Perpetually reachability implies relentless reachability,
so SHFA is also stronger than WHFA. However, as the next examples will show,
SFA and WHFA are incomparable.

######  Example 4.13.

The impact of hyperfairness can clearly be seen when non-determinism is used.
Consider the path $s_{0}t_{1}s_{1}t_{4}(s_{3}t_{6})^{\omega}$ in Figure 1.
This path satisfies $\emptyset$-SFA, since the only action that is
relentlessly enabled on this path, $\mathit{brew}$, also occurs infinitely
often. However, as long as $\mathit{deliver}\not\in\mathcal{B}$ and
$\mathit{brew}\not\in\mathcal{B}$, this path does not satisfy
$\mathcal{B}$-WHFA or $\mathcal{B}$-SHFA: $\mathit{deliver}$ is
$\mathcal{B}$-reachable from $s_{3}$, and therefore is perpetually and
relentlessly $\mathcal{B}$-reachable in a suffix of this path, but does not
occur. We here see $\mathcal{B}$-SFA does not imply $\mathcal{B}$-WHFA.

######  Example 4.14.

In Figure 1, consider $s_{0}t_{1}(s_{1}t_{2}s_{2}t_{3})^{\omega}$ with
$\mathcal{B}=\\{\mathit{order},\mathit{to\\_cash},\mathit{to\\_card}\\}$. This
path satisfies $\mathcal{B}$-WHFA because $\mathit{card}$ and $\mathit{cash}$
are only $\mathcal{B}$-reachable from $s_{1}$ and $s_{2}$ respectively. They
are not perpetually $\mathcal{B}$-reachable in any suffix of this path,
therefore $\mathcal{B}$-WHFA is satisfied. However, they are relentlessly
$\mathcal{B}$-reachable, so $\mathcal{B}$-SHFA is violated. This demonstrates
that $\mathcal{B}$-WHFA and $\mathcal{B}$-SFHA do not coincide when blocking
actions are considered. The actions $\mathit{card}$ and $\mathit{cash}$ are
also relentlessly $\mathcal{B}$-enabled, so $\mathcal{B}$-SFA is also
violated. Hence, $\mathcal{B}$-WHFA does not imply $\mathcal{B}$-SFA.

##  5 A Generalisation of the Property Specification Liveness Patterns

Dwyer, Avrunin and Corbett observed that a significant majority of properties
that are used in practice can be fit into a set of property specification
patterns [17]. These patterns consist of a _behaviour_ that must be satisfied
and a _scope_ within a path that delimits where the behaviour must be
satisfied. We recall the behaviours and scopes presented in [17] in Appendix
A. We focus on expressing properties that are captured by PSP.

Of all behaviours considered in [17], only existence, existence at least,
response and chain response represent pure liveness properties. The global and
after scopes, when combined with any of these four behaviours, give liveness
properties. We argue why only these patters of PSP represent pure liveness
properties in Appendix A. All other scopes result in safety properties or
properties that combine safety and liveness. Of those, we cover the until and
after-until scopes, since we can incorporate those into our formulae with
little difficulty.

For behaviours, existence at least says some action in a set $S_{r}$ must
occur at least $k$ times in the scope; when $k=1$ we call this existence. The
response behaviour requires that whenever an action in a set $S_{q}$ occurs,
it must be followed by the occurrence of an action in $S_{r}$. When chains of
action occurrences are used instead of individual action occurrences, this is
called chain response. For the scopes, global refers to the full path and
after to the path after the first occurrence of an action in a set $S_{a}$.
The until scope refers to the path before the first occurrence of an action in
a set $S_{b}$, or the full path if no such action occurs. Finally, after-until
combines after and until, referring to every subpath of the path that starts
after any occurrence of an action in $S_{a}$ and ends before the following
occurrence of an action in $S_{b}$. If no action in $S_{b}$ occurs, the
behaviour must still be satisfied after $S_{a}$.

######  Example 5.1.

Consider again the properties we presented in 3.1. _Single order_ is absence
after-until, with $S_{a}=\\{\mathit{order}\\}$, $S_{b}=\\{\mathit{deliver}\\}$
and $S_{r}=\\{\mathit{order}\\}$. _Inevitable delivery_ is global response
with $S_{q}=\\{\mathit{order}\\}$ and $S_{r}=\\{\mathit{deliver}\\}$.
_Possible delivery_ does not fit into the patterns on occurrences of actions,
since it contains a requirement on states, specifically that the state admits
a path on which $\mathit{delivery}$ occurs.

We want to create formulae for all 16 combinations of the selected behaviours
and scopes. To make our results more compact and generic, we first generalise
these 16 patterns into a single template property. This template works by
describing the shape of a violating path for a property that fits one of these
patterns. Intuitively, this shape is: “after the occurrence of $\rho$, there
are no occurrences of $\alpha_{\mathit{f}}$ up until the (optional) occurrence
of $\alpha_{\mathit{e}}$”. For our template formulae to be syntactically
correct, it is important that $\rho$ is a regular formula, describing the
prefix that a violating path must have, whereas $\alpha_{\mathit{f}}$ and
$\alpha_{\mathit{e}}$ are sets of actions. The actions in
$\alpha_{\mathit{f}}$ are those that are forbidden from occurring after $\rho$
on a violating path, whereas the actions in $\alpha_{\mathit{e}}$ indicate the
end of the scope in which $\alpha_{\mathit{f}}$ may not occur.

We formalise this template as follows:

######  Definition 5.2.

A path $\pi$ is _$(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$ -violating_
if, and only if, there exist $\pi_{\mathit{pre}}$ and $\pi_{\mathit{suf}}$
such that:

  1. 1.

$\pi=\pi_{\mathit{pre}}\cdot\pi_{\mathit{suf}}$, and

  2. 2.

$\pi_{\mathit{pre}}$ matches $\rho$, and

  3. 3.

$\pi_{\mathit{suf}}$ satisfies at least one of the following conditions:

    1. (a)

$\pi_{\mathit{suf}}$ is $\alpha_{\mathit{f}}$-free, or

    2. (b)

$\pi_{\mathit{suf}}$ contains an occurrence of an action in
$\alpha_{\mathit{e}}$, and the prefix of $\pi_{\mathit{suf}}$ before the first
occurrence of an action in $\alpha_{\mathit{e}}$ is
$\alpha_{\mathit{f}}$-free.

For readability, we frequently refer to
$(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating paths as violating
paths. We sometimes summarise condition 3 as “$\pi_{\mathit{suf}}$ is
$\alpha_{\mathit{f}}$-free up until the first occurrence of
$\alpha_{\mathit{e}}$”. See Figure 2 for an illustration of what types of
paths are considered violating.

$\rho$$\alpha_{\mathit{f}}$-free$\rho$$\alpha_{\mathit{f}}$-free$\rho$$\alpha_{\mathit{f}}$-free$\rho$$\alpha_{\mathit{f}}$-free$\alpha_{\mathit{e}}$$\alpha_{\mathit{e}}$
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}}$.

All 16 patterns can indeed be represented by the non-existence of
$(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating paths, albeit some
more directly than others. It turns out that $\rho$, $\alpha_{\mathit{f}}$ and
$\alpha_{\mathit{e}}$ can mostly be determined separately for behaviour and
scope. For these patterns, $\alpha_{\mathit{f}}$ is only affected by behaviour
and $\alpha_{\mathit{e}}$ only by scope. However, we must split up the regular
formula $\rho$ into a behaviour component, $\rho_{\mathit{b}}$, and scope
component, $\rho_{\mathit{s}}$, such that
$\rho=\rho_{\mathit{s}}\cdot\rho_{\mathit{b}}$. See 1(a) and 1(b) for how the
variables should be instantiated for the four scopes and three of the four
behaviours. For a compact representation, we use $\sum$ to generalise the
union operator on regular formulae ($+$). We also use $x^{i}$ to represent $i$
concatenations of $x$, where $x^{0}=\varepsilon$.

We do not include chain response in 1(b), since it does not fit into a single
formula. However, it is possible to represent chain response as several
response formulae placed in conjunction with each other. We include an example
of this in Appendix B.

Table 1: Variable instantiation for templates.

(a) For scopes. Scope | $\rho_{\mathit{s}}$ | $\alpha_{\mathit{e}}$
---|---|---
Global | $\varepsilon$ | $\emptyset$
Until | $\varepsilon$ | $S_{b}$
After | $\mathit{\overline{\mathit{S_{a}}}}^{\star}\cdot S_{a}$ | $\emptyset$
After-until | $\mathit{\mathit{Act}}^{\star}\cdot S_{a}$ | $S_{b}$

(b) For behaviours. Behaviour | $\rho_{\mathit{b}}$ | $\alpha_{\mathit{f}}$
---|---|---
Existence | $\varepsilon$ | $S_{r}$
Existence at least $k$ | $\sum_{0\leq i<k}(\mathit{\overline{\mathit{\alpha_{\mathit{e}}\cup S_{r}}}}^{\star}\cdot S_{r})^{i}$ | $S_{r}$
Response | $\mathit{\overline{\mathit{\alpha_{\mathit{e}}}}}^{\star}\cdot S_{q}$ | $S_{r}$
Chain response | See Appendix B |

##  6 Template Formulae

In this section, we present the modal $\mu$-calculus formulae representing the
non-existence of a violating path, as defined in section 5, that satisfies one
of the completeness criteria from section 4. We express the non-existence of
such a path, rather than expressing the equivalent notion that all complete
paths satisfy the property, because we find the resulting formulae to be more
intuitive. We first present a formula for $\mathcal{B}$-progress only.
Subsequently, we give the formulae for weak fairness, weak hyperfairness and
justness using a common structure all three share. Finally, we present the
formulae for strong fairness and strong hyperfairness. In the justness and
fairness formulae, $\mathcal{B}$-progress is also included: these assumptions
eliminate unrealistic infinite paths, but we still need progress to discard
unrealistic finite paths.

The proofs of all theorems in this section are included in Appendix D.

###  6.1 Progress

A formula for the non-existence of a violating path without progress is
uninteresting. If progress is not assumed then all finite paths are complete,
and therefore a path consisting of just $\rho$ is a violating path whenever
$\alpha_{\mathit{f}}\neq\emptyset$. The non-existence of a violating path
would then be captured by $\neg\langle\mathit{\rho}\rangle\mathit{tt}$. This
is why we include progress in all our formulae.

To represent progress, we must capture that as long as non-blocking actions
are enabled, some transitions must still be executed. The following formula
captures the non-existence of violating paths under $\mathcal{B}$-progress:

$\neg\langle\mathit{\rho}\rangle\nu
X.(\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle
X)$ (1)

Intuitively, this formula says that there is no path that starts with a prefix
matching $\rho$, after which infinitely often a transition can be taken that
is not labelled with an action in $\alpha_{\mathit{f}}$, or such transitions
can be taken finitely often before a state is reached that is
$\mathcal{B}$-locked or in which $\alpha_{\mathit{e}}$ is enabled. In the
former case there is a $\mathcal{B}$-progressing path on which no actions in
$\alpha_{\mathit{f}}$ occur after $\rho$. If a state in which
$\alpha_{\mathit{e}}$ is enabled is reached, then it is guaranteed a violating
and $\mathcal{B}$-progressing path exists: by arbitrarily extending the path
as long as non-blocking actions are still enabled, a $\mathcal{B}$-progressing
and violating path can be constructed.

######  Theorem 6.1.

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

Since representing a liveness pattern without progress leads to uninteresting
formulae, it is unsurprising that previous translations of PSP to the
$\mu$-calculus have also implicitly included progress. For instance, the
translations from [32] for the liveness patterns of PSP are very similar to
Formula 1, albeit in positive form and without blocking actions.

###  6.2 Weak Fairness, Weak Hyperfairness and Justness

For weak fairness, weak hyperfairness and justness, we employ a trick inspired
by the formula for justness presented in [7] (which was in turn inspired by
[12]): we translate a requirement on a full path into an invariant that can be
evaluated within finitely many steps from every state of the path. We
illustrate this using weak fairness.

On every suffix of a weakly fair path, every perpetually enabled non-blocking
action occurs. To turn this into an invariant, we observe that we can evaluate
a property on all suffixes of a path by evaluating it from every state of the
path instead. Next we must determine, within finitely many steps, if an action
is perpetually enabled on a possibly infinite path. We do this by observing
that if an action is not perpetually enabled, it must become disabled within
finitely many steps. An equivalent definition of WFA therefore is: a path
$\pi$ satisfies WFA if, and only if, for every state $s$ in $\pi$, every
action $a\in\overline{\mathit{\mathcal{B}}}$ that is enabled in $s$ occurs or
becomes disabled within finitely many steps on the suffix of $\pi$ starting in
$s$. This translation of WFA determines three things for every non-blocking
action $a$. First, which actions may need to occur because of $a$; in the case
of WFA this is $a$ itself. Second, when those actions need to occur; for WFA
this is when $a$ is enabled. We refer to this as the action being “on”.
Finally, when those actions do not need to occur; for WFA this is when $a$
becomes disabled. We refer to this as the action being “off”. When an action
that was previously on becomes off, or one of the required actions occurs, we
say the action is “eliminated”. By choosing different definitions for an
action being on or off, and when an action is eliminated, we can also
represent justness and weak hyperfairness in the same way.

We find that completeness criteria for which such a translation can be made
can be represented using the same generalised formula. We will present this
formula and how to instantiate it for WFA, WHFA and JA. However, we must first
formalise what it means for a predicate on paths to be translatable to an
invariant that can be evaluated within finitely many steps. We introduce the
term _finitely realisable (path) predicates_ for this purpose.

######  Definition 6.2.

A path predicate $P$ is _finitely realisable_ if, and only if, there exist
mappings $\phi_{\mathit{on}}$ and $\phi_{\mathit{of}}$ from non-blocking
actions to closed modal $\mu$-calculus formulae, and a mapping
$\alpha_{\mathit{el}}$ from non-blocking actions to sets of actions, such
that:

  1. 1.

A path $\pi$ satisfies predicate $P$ if, and only if, all states $s$ on $\pi$
satisfy the following: for all $a\in\overline{\mathit{\mathcal{B}}}$, if $s$
satisfies $\phi_{\mathit{on}}(a)$ then the suffix $\pi^{\prime}$ of $\pi$
starting in $s$ must contain an occurrence of some action in
$\alpha_{\mathit{el}}(a)$ or a state that satisfies $\phi_{\mathit{of}}(a)$.

  2. 2.

A state $s$ is a $\mathcal{B}$-locked state if, and only if,
$s\not\in\llbracket\phi_{\mathit{on}}(a)\rrbracket$ for all
$a\in\overline{\mathit{\mathcal{B}}}$.

  3. 3.

For every state $s$ and for all $a\in\overline{\mathit{\mathcal{B}}}$,
$s\in\llbracket\phi_{\mathit{on}}(a)\rrbracket$ implies
$s\not\in\llbracket\phi_{\mathit{of}}(a)\rrbracket$.

  4. 4.

For all states $s$ and all $a\in\overline{\mathit{\mathcal{B}}}$ such that
$s\in\llbracket\phi_{\mathit{on}}(a)\rrbracket$, if there exists a finite path
$\pi$ from $s$ to a state $s^{\prime}$ such that there is no occurrence of an
action in $\alpha_{\mathit{el}}(a)$ on $\pi$ and there is no state on $\pi$
that satisfies $\phi_{\mathit{of}}(a)$, then
$s^{\prime}\in\llbracket\phi_{\mathit{on}}(a)\rrbracket$.

We refer to these four properties as the _invariant property_ , the _locking
property_ , the _exclusive property_ and the _persistent property_ ,
respectively.

The general formula for finitely realisable predicates is as follows:

$\neg\langle\mathit{\rho}\rangle\nu
X.(\bigwedge_{a\in\overline{\mathit{\mathcal{B}}}}(\phi_{\mathit{on}}(a)\Rightarrow\langle\mathit{\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}^{\star}}\rangle(\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor(\phi_{\mathit{of}}(a)\land
X)\lor\langle\mathit{\alpha_{\mathit{el}}(a)\setminus\alpha_{\mathit{f}}}\rangle
X)))$ (2)

This formula has similarities to Formula 1, particularly how $\rho$ and
$\alpha_{\mathit{e}}$ are integrated. The important part is that after $\rho$,
it must invariantly hold that all non-blocking actions for which
$\phi_{\mathit{on}}(a)$ is satisfied are later eliminated. An action $a$ is
eliminated if, within finitely many steps, $\phi_{\mathit{of}}(a)$ is
satisfied or an action in $\alpha_{\mathit{el}}(a)$ occurs. In both cases, the
invariant must once again hold. After $\rho$, no actions in
$\alpha_{\mathit{f}}$ may occur. The formula works correctly for finite paths
as well as infinite ones: if it is possible to reach a $\mathcal{B}$-locked
state after $\rho$ without taking actions in $\alpha_{\mathit{f}}$, then $X$
is satisfied due to the locking property, and a violating path is found.

Formula 2 is a template formula in two ways: $\rho$, $\alpha_{\mathit{f}}$ and
$\alpha_{\mathit{e}}$ determine what property is captured, and
$\phi_{\mathit{on}}$, $\phi_{\mathit{of}}$ and $\alpha_{\mathit{el}}$
determine the completeness criterion. In this paper, we only cover how to
instantiate the formula for WFA, WHFA and JA, but it can also be used for
other finitely realisable predicates. However, the correctness proof of the
formula depends on the criterion being _feasible_. Feasibility on paths [3] is
defined as follows.

######  Definition 6.3.

A predicate on paths $P$ is _feasible_ if, and only if, for every LTS $M$,
every finite path $\pi$ in $M$ can be extended to a path $\pi^{\prime}$ that
satisfies $P$ and is still a valid path in $M$.

That WFA, WHFA and JA are feasible for finite LTSs is proven in Appendix C.

######  Theorem 6.4.

For all feasible and finitely realisable path predicates $P$, it holds that an
LTSC satisfies Formula 2 if, and only if, its initial state does not admit
$\mathcal{B}$-progressing paths that satisfy $P$ and are
$(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

By instantiating the theorem for each completeness criterion, we derive the
following:

######  Corollary 6.5.

A state in an LTS satisfies Formula 2 with
$\phi_{\mathit{on}}(a)=\langle\mathit{a}\rangle\mathit{tt}$,
$\phi_{\mathit{of}}(a)=[\mathit{a}]\mathit{ff}$ and
$\alpha_{\mathit{el}}(a)=\\{a\\}$ for all
$a\in\overline{\mathit{\mathcal{B}}}$ if, and only if, it does not admit
$\mathcal{B}$-progressing paths that satisfy $\mathcal{B}$-weak fairness of
actions and are $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

######  Corollary 6.6.

A state in an LTS satisfies Formula 2 with
$\phi_{\mathit{on}}(a)=\langle\mathit{\mathit{\overline{\mathit{\mathcal{B}}}}^{\star}\cdot
a}\rangle\mathit{tt}$,
$\phi_{\mathit{of}}(a)=[\mathit{\mathit{\overline{\mathit{\mathcal{B}}}}^{\star}\cdot
a}]\mathit{ff}$ and $\alpha_{\mathit{el}}(a)=\\{a\\}$ for all
$a\in\overline{\mathit{\mathcal{B}}}$ if, and only if, it does not admit
$\mathcal{B}$-progressing paths that satisfy weak $\mathcal{B}$-hyperfairness
of actions and are $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

######  Corollary 6.7.

A state in an LTSC satisfies Formula 2 with
$\phi_{\mathit{on}}(a)=\langle\mathit{a}\rangle\mathit{tt}$,
$\phi_{\mathit{of}}(a)=\mathit{ff}$ and
$\alpha_{\mathit{el}}(a)=\\{b\in\mathit{Act}\mid
a\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}b\\}$ for
all $a\in\overline{\mathit{\mathcal{B}}}$ if, and only if, it does not admit
$\mathcal{B}$-progressing paths that satisfy $\mathcal{B}$-justness of actions
and are $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

###  6.3 Strong Fairness and Strong Hyperfairness

SFA is not finitely realisable because we cannot observe within finitely many
steps whether an action is relentlessly enabled: even if we observe several
times that it is disabled, it may still be infinitely often enabled along the
whole path. Hence, we cannot use Formula 2.

Instead we observe that, on a path, actions that are not relentlessly enabled
must eventually become perpetually disabled. If the path is strongly fair,
then all relentlessly enabled non-blocking actions occur infinitely often. We
can therefore say that a path is strongly fair if we can divide all non-
blocking actions into two disjoint sets: those that occur infinitely often and
those that eventually become perpetually disabled. This observation is also
made in [37], where a $\mu$-calculus formula for termination under strong
fairness is given.

Using this idea, we give the following template formula for SFA:

$\neg\langle\mathit{\rho\cdot\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}^{\star}}\rangle(\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\bigvee_{\emptyset\neq
F\subseteq\overline{\mathit{\mathcal{B}}}}\nu X.(\bigwedge_{a\in F}\mu
W.((\bigwedge_{b\in\overline{\mathit{\mathcal{B}}}\setminus
F}[\mathit{b}]\mathit{ff})\land(\langle\mathit{a\setminus\alpha_{\mathit{f}}}\rangle
X\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle W))))$ (3)

The use of negation, the exclusion of $\alpha_{\mathit{f}}$, and $\rho$ in the
diamond operator at the start of this formula are the same as in Formula 1. We
explain the start of the formula after addressing the part starting with
$\bigvee_{\emptyset\neq F\subseteq\overline{\mathit{\mathcal{B}}}}$. Here, we
use that on a strongly fair path, all non-blocking actions can be divided into
those that occur infinitely often and those that become perpetually disabled.
The disjunction over subsets considers all possible ways of selecting some
non-empty subset $F$ of $\overline{\mathit{\mathcal{B}}}$ that should occur
infinitely often. The greatest fixpoint states that infinitely often, all
those actions must indeed occur within finitely many steps. Additionally, at
no point may a non-blocking action not in $F$ be enabled. We exclude
$F=\emptyset$ because the logic of the greatest fixed point formula we give
relies on there being at least one $a$ in $F$. The special case that $F$ is
empty and therefore a $\mathcal{B}$-locked state should be reached, is instead
covered by explicitly considering
$[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}$ earlier in the
formula. Returning to the start of the formula, we allow a finite
$\alpha_{\mathit{f}}$-free path before the greatest fixpoint is satisfied. The
reason is that it may take several steps before all the non-blocking actions
that are only finitely often enabled become perpetually disabled. Since we
include a finite prefix already, we also add the cases that an action in
$\alpha_{\mathit{e}}$ becomes enabled or that a $\mathcal{B}$-locked state is
reached here, rather than deeper into the formula like in Formula 2.

######  Theorem 6.8.

An LTS satisfies Formula 3 if, and only if, its initial state does not admit
$\mathcal{B}$-progressing paths that satisfy $\mathcal{B}$-strong fairness of
actions and are $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

Due to the quantification over subsets, the formula is exponential in the
number of actions in $\overline{\mathit{\mathcal{B}}}$. Beyond small models,
it is therefore not practical. However, it can serve as a basis for future
work. For instance, if fairness is applied to sets of actions rather than
individual actions, the formula is exponential in the number of sets instead,
which may be smaller depending on how the sets are formed [36].

We can adapt the formula for strong fairness to a formula for strong
hyperfairness, by replacing perpetual disabledness of non-blocking actions not
in $F$ with perpetual unreachability.

$\neg\langle\mathit{\rho\cdot\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}^{\star}}\rangle(\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\bigvee_{\emptyset\neq
F\subseteq\overline{\mathit{\mathcal{B}}}}\nu X.(\bigwedge_{a\in F}\mu
W.((\bigwedge_{b\in\overline{\mathit{\mathcal{B}}}\setminus
F}[\mathit{\mathit{\overline{\mathit{\mathcal{B}}}}^{\star}\cdot
b}]\mathit{ff})\land(\langle\mathit{a\setminus\alpha_{\mathit{f}}}\rangle
X\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle W))))$ (4)

######  Theorem 6.9.

An LTS satisfies Formula 4 if, and only if, its initial state does not admit a
$\mathcal{B}$-progressing path that satisfies strong
$\mathcal{B}$-hyperfairness of actions and is
$(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

Since we are not aware of other completeness criteria that fit the same
structure, we do not provide a generalised formula here like we did with
Formula 2, although we do prove a more general theorem in Section D.4.

##  7 Application Example

We here give an example of an application of the template formulae. In [26],
several mutual exclusion algorithms are analysed using the mCRL2 toolset.
Their analysis of Dekker’s algorithm [15] presents the following modal
$\mu$-calculus formula for starvation freedom of processes with id’s 0 and 1.
For clarity, the notation has been adjusted to match the previous sections and
action names have been simplified.

$[\mathit{\mathit{\mathit{Act}}^{\star}}]\bigwedge_{i\in\\{0,1\\}}[\mathit{\\{\mathit{wish\\_flag}(i,b)\mid
b\in\mathbb{B}\\}}]\mu
X.([\mathit{\overline{\mathit{\mathit{enter}(i)}}}]X\land\langle\mathit{\mathit{Act}}\rangle\mathit{tt})$
(5)

Starvation freedom is a global response property. In this case, the starvation
freedom of a process $i$ is represented as an instantiation of the pattern
with $S_{q}=\\{\mathit{wish\\_flag}(i,b)\mid b\in\mathbb{B}\\}$ and
$S_{r}=\\{\mathit{enter}(i)\\}$. Indeed, the above formula is equivalent to:

$\bigwedge_{i\in\\{0,1\\}}\neg\langle\mathit{\mathit{\mathit{Act}}^{\star}\cdot\\{\mathit{wish\\_flag}(i,b)\mid
b\in\mathbb{B}\\}}\rangle\nu
X.(\langle\mathit{\emptyset}\rangle\mathit{tt}\lor[\mathit{\mathit{Act}}]\mathit{ff}\lor\langle\mathit{\overline{\mathit{\mathit{enter}(i)}}}\rangle
X)$ (6)

Observe that, when taking $\mathcal{B}=\emptyset$, the above matches a
conjunction of two instances of Formula 1, taking $\rho$,
$\alpha_{\mathit{e}}$ and $\alpha_{\mathit{f}}$ as suggested in Table 1 for
global response. Thus, this formula captures starvation freedom under
$\emptyset$-progress. In [26], it is reported that mCRL2 finds a violating
path for this formula; a path which the authors note is unfair. The exact
fairness assumption considered is not made concrete. As an ad-hoc solution,
the modal $\mu$-calculus formula is adjusted to specifically ignore that
counterexample. Subsequently, mCRL2 finds another counterexample, which the
authors again claim is unfair. Instead of creating yet another formula, they
move on to Peterson’s algorithm, which is deemed easier to analyse. Using our
template formulae, we can easily produce a formula for starvation freedom
under several different completeness criteria. We give the formula for
$\emptyset$-WFA, as an example.

$\bigwedge_{i\in\\{0,1\\}}\neg\langle\mathit{\mathit{\mathit{Act}}^{\star}\cdot\\{\mathit{wish\\_flag}(i,b)\mid
b\in\mathbb{B}\\}}\rangle\\\ \nu
X.(\bigwedge_{a\in\mathit{Act}}(\langle\mathit{a}\rangle\mathit{tt}\Rightarrow\langle\mathit{\mathit{\overline{\mathit{\mathit{enter}(i)}}}^{\star}}\rangle(\langle\mathit{\emptyset}\rangle\mathit{tt}\lor([\mathit{a}]\mathit{ff}\land
X)\lor\langle\mathit{a\setminus\mathit{enter}(i)}\rangle X)))$ (7)

We check this formula on the model from [26] using mCRL2. Since mCRL2 only
supports quantification over data parameters and not over actions, the
conjunction over $\mathit{Act}$ must be written out explicitly. The tool
reports that the formula is violated. Examining the counterexample reveals
this is because actions in the model do not show which process performs the
action. Therefore, process $i$ reading value $v$ from a register $r$ is
labelled with the same action as process $j$ reading $v$ from $r$. We add the
responsible process to each action label, and also define
$\mathcal{B}=\\{\mathit{wish\\_flag}(i,i,b)\mid
i\in\\{0,1\\},b\in\mathbb{B}\\}$, to capture that processes are allowed to
remain in their non-critical section indefinitely. This was not considered in
Formula 5, but it is part of the mutual exclusion problem [16, 23]. The tool
reports that the modified formula is satisfied. We can therefore conclude that
Dekker’s algorithm satisfies starvation freedom when assuming weak fairness of
actions, as long as it is taken into account for each action which process is
responsible for it.

Our other formulae can be used in similar ways. An example of how to use the
justness formula in mCRL2, including a method for encoding the concurrency
relation, is given in [7].

##  8 Discussion

In this section, we briefly reflect on the coverage of the properties we
consider, and our choice in focusing on the modal $\mu$-calculus.

Firstly, we have exclusively addressed liveness properties in this paper thus
far. As indicated previously, the problem we are considering primarily crops
up for these properties. This is because, as pointed out in [23], when a
completeness criterion is feasible, assuming the criterion holds true or not
has no impact on whether a safety property is satisfied or not. The reason is
that for safety properties on paths, any path that violates the property must
contain a finite prefix such that any extension of that prefix also violates
the property [1]. Therefore, if a completeness criterion is feasible, then
whenever a model contains incomplete paths that violate a safety property it
also contains complete paths that violate the property. All completeness
criteria discussed in section 4 are feasible with respect to finite LTSs, and
hence we do not need to consider patterns that capture safety properties. For
modal $\mu$-calculus formulae for the safety properties of PSP, without
integrated completeness criteria, we refer to [32] and [35]. For properties
that are a combination of safety and liveness, the components can be turned
into separate formulae and checked separately.

Readers may also wonder about alternative methods of representing properties
under completeness criteria, such as using LTL. As indicated in section 3,
there are many contexts where we also want to consider non-linear properties,
and hence the modal $\mu$-calculus is preferred. Automatic translations from
LTL to the modal $\mu$-calculus exist, but can be exponential in complexity
[14] and it is unclear at this time if this blow-up is avoided in this case.
Anecdotal evidence [34] suggests this is not the case for existing
translations. In [23] several completeness criteria are represented in LTL,
but it is noted that this translation requires introducing new atomic
propositions which hides the complexity of this translation. The
representation of hyperfairness in particular may be expensive, since atomic
propositions for all reachable actions are required. It is also unclear how to
combine LTL-based translations effectively with symbolic model checking
approaches. For these reasons, a direct representation in the modal
$\mu$-calculus is preferable.

##  9 Conclusion

In this paper, we have presented formulae for liveness properties under
several completeness criteria. As part of this, we defined a property template
that generalises the liveness properties of PSP, which has been estimated to
cover a majority of properties found in the literature [17]. The completeness
criteria covered are progress, justness, weak fairness, strong fairness, and
hyperfairness, all defined with respect to actions and parameterised with a
set of blocking actions. The formulae have all been manually proven to be
correct.

For future work, one goal is to formalise the proofs in the appendices using a
proof assistant. Another avenue for future work is extending our formulae to
cover a wider range of completeness criteria and properties. We suggest some
potential extensions here.

One of our contributions is the identification of a shared common structure
underlying justness, weak fairness and weak hyperfairness: they are finitely
realisable path predicates. Our formula for such predicates can be adapted to
arbitrary feasible finitely realisable path predicates. While we do not have
such a generic formula for other completeness criteria, our characterisation
of $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating paths can be
used as a basis to express the non-existence of complete paths violating many
common properties for different notions of completeness as well, as we
demonstrate with strong fairness and strong hyperfairness. We are especially
interested in extending our formulae to allow fairness over sets of actions,
rather than individual actions, similar to the task-based definitions from
[25].

In terms of properties, we can look at proposed extensions of PSP, such as
those suggested in [13]. There is also the constrained chain behaviour, which
is a modification of precedence chain and response chain given in [17]. There
are extensions of PSP to real-time [5, 29] and probabilistic [28] contexts as
well. Finally, in [6] the formula from [7] that formed the basis of Formula 2
is extended to also include state information.

There are therefore many potentially useful extensions of the formulae
presented in this paper. However, the presented template formulae already
cover many completeness criteria and liveness properties, making them useful
for model checking in practice.

## References

  * [1] Mack W. Alford, Leslie Lamport, and Geoff P. Mullery.  Basic concepts.  In Mack W. Alford, Jean-Pierre Ansart, Günter Hommel, Leslie Lamport, Barbara Liskov, Geoff P. Mullery, and Fred B. Schneider, editors, Distributed Systems: Methods and Tools for Specification, An Advanced Course, April 3-12, 1984 and April 16-25, 1985, Munich, Germany, volume 190 of Lecture Notes in Computer Science, pages 7–43. Springer, 1984.  doi:10.1007/3-540-15216-4\\_12.
  * [2] Bowen Alpern and Fred B. Schneider.  Defining liveness.  Inf. Process. Lett., 21(4):181–185, 1985.  doi:10.1016/0020-0190(85)90056-0.
  * [3] Krzysztof R. Apt, Nissim Francez, and Shmuel Katz.  Appraising fairness in languages for distributed programming.  Distributed Comput., 2(4):226–241, 1988.  doi:10.1007/BF01872848.
  * [4] Paul C. Attie, Nissim Francez, and Orna Grumberg.  Fairness and hyperfairness in multi-party interactions.  In Frances E. Allen, editor, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990, pages 292–305. ACM Press, 1990.  doi:10.1145/96709.96739.
  * [5] Pierfrancesco Bellini, Paolo Nesi, and Davide Rogai.  Expressing and organizing real-time specification patterns via temporal logics.  J. Syst. Softw., 82(2):183–196, 2009.  doi:10.1016/j.jss.2008.06.041.
  * [6] Mark S. Bouwman.  Supporting Railway Standardisation with Formal Verification.  Phd Thesis 1 (Research TU/e / Graduation TU/e), Mathematics and Computer Science, Eindhoven University of Technology, 2023.  https://pure.tue.nl/ws/portalfiles/portal/307965423/20231023_Bouwman_hf.pdf.
  * [7] Mark S. Bouwman, Bas Luttik, and Tim A. C. Willemse.  Off-the-shelf automated analysis of liveness properties for just paths.  Acta Informatica, 57(3-5):551–590, 2020.  doi:10.1007/s00236-020-00371-w.
  * [8] Julian C. Bradfield and Colin Stirling.  Modal logics and mu-calculi: an introduction.  In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 293–330. Elsevier Science, 2001.  doi:10.1016/b978-044482830-9/50022-9.
  * [9] Julian C. Bradfield and Colin Stirling.  Modal mu-calculi.  In Patrick Blackburn, Johan Van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721–756. Elsevier, 2007.  doi:10.1016/s1570-2464(07)80015-2.
  * [10] Julian C. Bradfield and Igor Walukiewicz.  The mu-calculus and model checking.  In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871–919. Springer, 2018.  doi:10.1007/978-3-319-10575-8\\_26.
  * [11] Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse.  The mCRL2 toolset for analysing concurrent systems.  In Tomáš Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, volume 11428 of Lecture Notes in Computer Science, pages 21–39. Springer, 2019.  doi:10.1007/978-3-030-17465-1\\_2.
  * [12] Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, and Xudong Zhao.  Efficient generation of counterexamples and witnesses in symbolic model checking.  In Bryan Preas, editor, Proceedings of the 32st Conference on Design Automation, San Francisco, California, USA, Moscone Center, June 12-16, 1995, pages 427–432. ACM Press, 1995.  doi:10.1145/217474.217565.
  * [13] Rachel L. Cobleigh, George S. Avrunin, and Lori A. Clarke.  User guidance for creating precise and accessible property specifications.  In Michal Young and Premkumar T. Devanbu, editors, Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, November 5-11, 2006, pages 208–218. ACM, 2006.  doi:10.1145/1181775.1181801.
  * [14] Sjoerd Cranen, Jan Friso Groote, and Michel A. Reniers.  A linear translation from CTL⋆ to the first-order modal $\mu$-calculus.  Theor. Comput. Sci., 412(28):3129–3139, 2011.  doi:10.1016/j.tcs.2011.02.034.
  * [15] Edsger W Dijkstra.  Over de sequentialiteit van procesbeschrijvingen (EWD-35). EW dijkstra archive.  Center for American History, University of Texas at Austin, 1962.  URL: https://www.cs.utexas.edu/~EWD/ewd00xx/EWD35.PDF.
  * [16] Edsger W. Dijkstra.  Solution of a problem in concurrent programming control.  Commun. ACM, 8(9):569, 1965.  doi:10.1145/365559.365617.
  * [17] Matthew B. Dwyer, George S. Avrunin, and James C. Corbett.  Patterns in property specifications for finite-state verification.  In Barry W. Boehm, David Garlan, and Jeff Kramer, editors, Proceedings of the 1999 International Conference on Software Engineering, ICSE’ 99, Los Angeles, CA, USA, May 16-22, 1999, pages 411–420. ACM, 1999.  doi:10.1145/302405.302672.
  * [18] E. Allen Emerson and Edmund M. Clarke.  Using branching time temporal logic to synthesize synchronization skeletons.  Sci. Comput. Program., 2(3):241–266, 1982.  doi:10.1016/0167-6423(83)90017-5.
  * [19] Michael J. Fischer and Richard E. Ladner.  Propositional dynamic logic of regular programs.  J. Comput. Syst. Sci., 18(2):194–211, 1979.  doi:10.1016/0022-0000(79)90046-1.
  * [20] Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe.  CADP 2011: a toolbox for the construction and analysis of distributed processes.  Int. J. Softw. Tools Technol. Transf., 15(2):89–107, 2013.  doi:10.1007/s10009-012-0244-z.
  * [21] Rob J. van Glabbeek.  Justness - A completeness criterion for capturing liveness properties (extended abstract).  In Mikołaj ojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 505–522. Springer, 2019.  doi:10.1007/978-3-030-17127-8\\_29.
  * [22] Rob J. van Glabbeek.  Reactive temporal logic.  In Ornela Dardha and Jurriaan Rot, editors, Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020, and 17th Workshop on Structural Operational SemanticsOnline, 31 August 2020, volume 322 of EPTCS, pages 51–68. Open Publishing Association, 2020.  doi:10.4204/EPTCS.322.6.
  * [23] Rob J. van Glabbeek.  Modelling mutual exclusion in a process algebra with time-outs.  Inf. Comput., 294:105079, 2023.  doi:10.1016/j.ic.2023.105079.
  * [24] Rob J. van Glabbeek and Peter Höfner.  CCS: It’s not fair! fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions.  Acta Informatica, 52(2-3):175–205, 2015.  doi:10.1007/s00236-015-0221-6.
  * [25] Rob J. van Glabbeek and Peter Höfner.  Progress, Justness, and Fairness.  ACM Comput. Surv., 52(4):69:1–69:38, 2019.  doi:10.1145/3329125.
  * [26] Jan Friso Groote and Jeroen J. A. Keiren.  Tutorial: designing distributed software in mCRL2.  In Kirstin Peters and Tim A. C. Willemse, editors, Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, volume 12719 of Lecture Notes in Computer Science, pages 226–243. Springer, 2021.  doi:10.1007/978-3-030-78089-0\\_15.
  * [27] Jan Friso Groote and Mohammad Reza Mousavi.  Modeling and Analysis of Communicating Systems.  MIT Press, 08 2014.  URL: https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems.
  * [28] Lars Grunske.  Specification patterns for probabilistic quality properties.  In Wilhelm Schäfer, Matthew B. Dwyer, and Volker Gruhn, editors, 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, pages 31–40. ACM, 2008.  doi:10.1145/1368088.1368094.
  * [29] Sascha Konrad and Betty H. C. Cheng.  Real-time specification patterns.  In Gruia-Catalin Roman, William G. Griswold, and Bashar Nuseibeh, editors, 27th International Conference on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, pages 372–381. ACM, 2005.  doi:10.1145/1062455.1062526.
  * [30] Dexter Kozen.  Results on the propositional $\mu$-calculus.  Theor. Comput. Sci., 27(3):333–354, 1983.  doi:10.1016/0304-3975(82)90125-6.
  * [31] Leslie Lamport.  Fairness and hyperfairness.  Distributed Comput., 13(4):239–245, 2000.  doi:10.1007/PL00008921.
  * [32] Radu Mateescu.  Property Pattern Mappings for RAFMC, 2019.  Available at: https://cadp.inria.fr/resources/evaluator/rafmc.html (Accessed: 26 January 2024).
  * [33] Amir Pnueli.  The temporal logic of programs.  In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46–57. IEEE Computer Society, 1977.  doi:10.1109/SFCS.1977.32.
  * [34] Jaco van de Pol and Michael Weber.  A multi-core solver for parity games.  Electronic Notes in Theoretical Computer Science, 220(2):19–34, 2008.  Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2008).  doi:10.1016/j.entcs.2008.11.011.
  * [35] Daniela Remenska.  Bringing Model Checking Closer To Practical Software Engineering.  PhD thesis, Vrije U., Amsterdam, 2016.  PhD Thesis, available at: https://hdl.handle.net/1871/53958.
  * [36] Myrthe S. C. Spronck.  Fairness assumptions in the modal $\mu$-calculus, 2023.  Master’s thesis, Eindhoven University of Technology, available at https://research.tue.nl/en/studentTheses/fairness-assumptions-in-the-modal-%C2%B5-calculus.
  * [37] Frank A. Stomp, Willem-Paul de Roever, and Rob T. Gerth.  The $\mu$-calculus as an assertion-language for fairness arguments.  Inf. Comput., 82(3):278–322, 1989.  doi:10.1016/0890-5401(89)90004-7.

##  Appendix A Property Patterns

Here we recall the behaviours and scopes presented in [17]. The original
presentation is not restricted to a particular logic and the patterns allow
behaviour and scopes to be defined based on both states and actions. We give
the definitions specifically with respect to occurrences of actions, since
those are the properties we consider in this paper. We use $S_{a}$ (“after”),
$S_{b}$ (“before”), $S_{q}$ (“query”) and $S_{r}$ (“required”/“response”) as
placeholder names for property-specific sets of actions. We use $k$ for an
arbitrary natural number.

The following behaviours are given:

  * •

Absence: no action in $S_{r}$ may occur.

  * •

Existence: some action in $S_{r}$ must occur.

    * –

Existence at least/at most/exactly: there must be at least/at most/exactly $k$
occurrences of actions in $S_{r}$. The existence pattern is an instantiation
of existence at least with $k=1$.

  * •

Universality: only actions in $S_{r}$ occur.

  * •

Precedence: an occurrence of an action in $S_{r}$ must always be preceded by
an occurrence of an action in $S_{q}$.

    * –

Chain precedence: if actions from the sets $S_{r_{0}}$, $S_{r_{1}}$, $\ldots$,
$S_{r_{n}}$ occur in that order (potentially with other actions in-between),
then they must have been preceded by occurrences of actions from the sets
$S_{q_{0}}$, $S_{q_{1}}$, $\ldots$, $S_{q_{m}}$, in that order.

  * •

Response: an occurrence of an action in $S_{q}$ must be followed by the
occurrence of an action from $S_{r}$.

    * –

Chain response: if actions from the sets $S_{q_{0}}$, $S_{q_{1}}$, $\ldots$,
$S_{q_{n}}$ occur in that order (potentially with other actions in between),
then they must be followed by occurrences of actions from the sets
$S_{r_{0}}$, $S_{r_{1}}$, $\ldots$, $S_{r_{m}}$, in that order.

All of the behaviours only need to hold within the chosen scope. The following
scopes are given:

  * •

Global: the full path.

  * •

Before: the prefix of the path before the first occurrence of an action in
$S_{b}$. If no action in $S_{b}$ occurs on the path, then the behaviour does
not need to be satisfied anywhere.

    * –

Until: same as before, except that if no action in $S_{b}$ occurs, then the
behaviour needs to hold on the full path.

  * •

After: the suffix of the path after the first occurrence of an action in
$S_{a}$. If no action in $S_{a}$ occurs on the path, then the behaviour does
not need to be satisfied anywhere.

  * •

Between: every subpath of the path that starts after an occurrence of an
action in $S_{a}$ and ends before the first following occurrence of an action
in $S_{b}$. If there is an occurrence of an action in $S_{a}$ that is not
eventually followed by an action in $S_{b}$, the behaviour does not need to be
satisfied after that $S_{a}$. This combines after and before, but unlike the
default after scope considers any occurrence of $S_{a}$, not merely the first.

    * –

After-until: same as between, except that if there is an occurrence of an
action in $S_{a}$ that is not eventually followed by an action in $S_{b}$, the
behaviour still needs to be satisfied after that occurrence of $S_{a}$. This
combines after and until.

The until scope does not appear in [17], but after-until does. We include the
until scope from [35], there called before-variant, because it can be seen as
a simpler form of after-until.

We only consider liveness properties, so we must ask which combinations of
behaviour and scope result in liveness properties. To make this judgement, we
need a formal definition of what makes a property a safety or liveness
property. For the purposes of this paper, since all the properties we consider
are defined on occurrences of actions, we can use the following definition of
a property:

######  Definition A.1.

A _property_ is a set of sequences of actions. A path $\pi$ _satisfies_ the
property if its sequence of actions is in the set, otherwise it _violates_ the
property.

We adapt the formal definitions of safety and liveness properties from [1] and
[2] respectively to this definition of properties.

######  Definition A.2.

A property $P$ is a _safety_ property if, and only if, every infinite sequence
of actions not in $P$ has a finite prefix that is not in $P$.

The consequence of this is that an infinite path that violates a safety
property always has a finite prefix that violates it as well.

######  Definition A.3.

A property $P$ is a _liveness_ property if, and only if, for every finite
sequence of actions $\mathit{f}$ there exists some infinite sequence of
actions $\mathit{f}^{\prime}$ such that $\mathit{f}\mathit{f}^{\prime}$ is in
$P$.

In terms of paths, this means that for every finite path $\pi$ that violates a
liveness property, there exists an infinite path $\pi^{\prime}$ of which $\pi$
is a prefix that satisfies the property. Note that it is not required for an
LTS that admits $\pi$ to also admit $\pi^{\prime}$, only that such an
extension could be made. We now discuss which patterns form liveness
properties.

First, we note that the before and between scopes will turn every behaviour
into a safety property: whenever an action in $S_{b}$ occurs the behaviour
should be satisfied before that occurrence, hence every path that violates the
property will have a finite prefix, ending with the first occurrence of an
action in $S_{b}$, that also violates the property. The global, until, after
and after-until scopes remain relevant. Under these four scopes, the
behaviours absence, existence at most, universality, precedence and chain
precedence will always result in safety properties as well. For each of these
behaviours, some actions may not occur under certain circumstances (be it at
all, after there have already been a number of occurrence of those actions, or
when some other actions have not yet occurred), therefore every violating path
has a finite prefix, ending with the occurrence of such an action, that also
violates the path. This leaves us with existence, existence at least,
existence exactly, response and chain response.

We further drop existence exactly since it is merely a conjunction of
existence at least and existence at most. Both parts of the pattern can be
expressed separately, so a separate formula for existence exactly is
superfluous.

We could apply a similar argument to the until scope: it is merely a
combination of global and before. Saying that an action in $S_{r}$ has to
occur until $S_{b}$ (existence until), for instance, is the same as saying
that an action in $S_{r}$ has to occur at all (global existence) and that if
there is an occurrence of $S_{b}$, there must be an occurrence of $S_{r}$
before it (existence before). This extends to after-until as well, although it
requires a bit more care than simply combining after and between, since after
always applies to the first occurrence of an action in $S_{a}$, whereas after-
until refers to every occurrence. This could be achieved with minor
modifications to the patterns. However, it turns out we can relatively easily
incorporate the until and after-until scopes into our formulae, so we include
them for convenience.

##  Appendix B Representing Chain Response

We here illustrate how the chain response behaviour can be represented using
our template formulae by combining several response formulae.

Consider, for example, sequences of two sets each: if an occurrence of
$S_{q_{0}}$ is eventually followed by an occurrence of $S_{q_{1}}$, then there
must subsequently be an occurrence of $S_{r_{0}}$ followed by $S_{r_{1}}$.
There are two possible violating paths here: either $S_{q_{0}},S_{q_{1}}$ is
not followed by $S_{r_{0}}$, or $S_{q_{0}},S_{q_{1}},S_{r_{0}}$ is not
followed by $S_{r_{1}}$. These two violations cannot be slotted directly into
the form of a single
$(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating path. Instead, we
have two different $(\rho,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating
paths. In general, if we have chain response with $S_{q_{0}}$ to $S_{q_{n}}$
and $S_{r_{0}}$ to $S_{r_{m}}$ then we get $m$ different violating paths.
Specifically, for all $0\leq i\leq m$, we get a violating path that consists
of a sequence $S_{q_{0}}$, $\ldots$, $S_{q_{n}}$, $S_{r_{0}}$, $\ldots$,
$S_{r_{i-1}}$ that may not be followed by an occurrence of $S_{r_{i}}$. For
convenience, we write such violating paths as a sequence $S_{0}$, $S_{1}$,
$\ldots$, $S_{n}$ that may not be followed by $S_{n+1}$.

Such violating paths can be expressed through
$\rho_{\mathit{b}}=\mathit{\overline{\mathit{\alpha_{\mathit{e}}}}}^{\star}\cdot
S_{0}\cdot\mathit{\overline{\mathit{\alpha_{\mathit{e}}\cup
S_{1}}}}^{\star}\cdot
S_{1}\cdot\mathit{\overline{\mathit{\alpha_{\mathit{e}}\cup
S_{2}}}}^{\star}\cdot
S_{2}\ldots\cdot\mathit{\overline{\mathit{\alpha_{\mathit{e}}\cup
S_{n}}}}^{\star}\cdot S_{n}$, and $\alpha_{\mathit{f}}=S_{n+1}$. Each
violating path must be given its own formula, where 1(a) is still used for the
scope, and all resulting formulae placed in conjunction. This way chain-
response can be represented.

######  Example B.1.

Say we want to express chain response with the scope after-until under WFA,
and we take the chain that an occurrence of an action in $S_{q_{0}}$, if
followed by an action in $S_{q_{1}}$, needs to be followed by an action in
$S_{r_{0}}$ and then by an action in $S_{r_{1}}$. The violating paths are
occurrences of an actions in $S_{q_{0}},S_{q_{1}}$ not followed by an action
$S_{r_{0}}$, and occurrences of actions in $S_{q_{0}},S_{q_{1}},S_{r_{0}}$
with no subsequent occurrence of an action in $S_{r_{1}}$. Both must be after
the first occurrence of an action in $S_{a}$, and before the next occurrence
of an action in $S_{b}$. The formula we need is then:

$\displaystyle\neg(\langle\mathit{\mathit{\mathit{Act}}^{\star}\cdot
S_{a}\cdot\mathit{\overline{\mathit{S_{b}}}}^{\star}\cdot
S_{q_{0}}\cdot\mathit{\overline{\mathit{S_{b}\cup S_{q_{1}}}}}^{\star}\cdot
S_{q_{1}}}\rangle$ $\displaystyle\quad\nu
X.(\bigwedge_{a\in\overline{\mathit{\mathcal{B}}}}(\langle\mathit{a}\rangle\mathit{tt}\Rightarrow\langle\mathit{\mathit{\overline{\mathit{S_{r_{0}}}}}^{\star}}\rangle(\langle\mathit{S_{b}}\rangle\mathit{tt}\lor([\mathit{a}]\mathit{ff}\land
X)\lor\langle\mathit{a\setminus S_{r_{0}}}\rangle X))))$ $\displaystyle\land$
$\displaystyle\neg(\langle\mathit{\mathit{\mathit{Act}}^{\star}\cdot
S_{a}\cdot\mathit{\overline{\mathit{S_{b}}}}^{\star}\cdot
S_{q_{0}}\cdot\mathit{\overline{\mathit{S_{b}\cup S_{q_{1}}}}}^{\star}\cdot
S_{q_{1}}\cdot\mathit{\overline{\mathit{S_{b}\cup S_{r_{0}}}}}^{\star}\cdot
S_{r_{0}}}\rangle$ $\displaystyle\quad\nu
X.(\bigwedge_{a\in\overline{\mathit{\mathcal{B}}}}(\langle\mathit{a}\rangle\mathit{tt}\Rightarrow\langle\mathit{\mathit{\overline{\mathit{S_{r_{1}}}}}^{\star}}\rangle(\langle\mathit{S_{b}}\rangle\mathit{tt}\lor([\mathit{a}]\mathit{ff}\land
X)\lor\langle\mathit{a\setminus S_{r_{1}}}\rangle X))))$

##  Appendix C Proofs of Feasibility

In Section 6.2 we claimed WFA, WHFA and JA are feasible with respect to finite
LTSs. In the proof of the SFA and SHFA formulae, we will need feasibility of
SFA and SHFA as well. In this appendix, we give those proofs.

All our proofs assume a fixed LTSC
$M=(\mathcal{S},s_{\mathit{init}},\mathit{Act},\mathit{Trans},\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}})$,
although the $\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$ is
only relevant for JA. We also refer to an arbitrary environment $\mathit{e}$,
and set of blocking actions $\mathcal{B}\subseteq\mathit{Act}$. When we refer
to an arbitrary state or transition in a path in our proofs, it should be
understood that we are referring to specific occurrences of those states and
transitions unless explicitly stated otherwise.

Recall 6.3: See 6.3

######  Proposition C.1.

$\mathcal{B}$-weak fairness of actions is feasible.

######  Proof C.2.

It is proven in [25, Theorem 6.1] that if only countably many actions are
enabled in each state of a transition system, then weak fairness of actions
with $\mathcal{B}=\emptyset$ is feasible. We have assumed a finite set
$\mathit{Act}$, hence this theorem applies in our case. This means that every
finite path can be extended to a path that is $\emptyset$-weakly fair. A path
that satisfies $\emptyset$-WFA also satisfies $\mathcal{B}$-WFA for arbitrary
$\mathcal{B}$, since $\emptyset$-WFA requires all actions in $\mathit{Act}$ to
occur in suffixes that they are perpetually enabled in, and $\mathit{Act}$ is
a superset of $\overline{\mathit{\mathcal{B}}}$. We conclude that
$\mathcal{B}$-weak fairness of actions is feasible.

######  Proposition C.3.

$\mathcal{B}$-strong fairness of actions is feasible.

######  Proof C.4.

It is proven in [25, Theorem 6.1] that if only countably many actions are
enabled in each state of a transition system, then strong fairness of actions
with $\mathcal{B}=\emptyset$ is feasible. We have assumed a finite set
$\mathit{Act}$, hence this theorem applies. Similarly to WFA, as argued in
C.1, $\emptyset$-SFA implies $\mathcal{B}$-SFA for arbitrary $\mathcal{B}$
because $\mathcal{B}$-SFA requires only actions in
$\overline{\mathit{\mathcal{B}}}$ to occur when they are relentlessly enabled.
We conclude $\mathcal{B}$-strong fairness of actions is feasible.

For the two forms of hyperfairness, we first prove a supporting lemma.

######  Lemma C.5.

Every finite path $\pi$ can be extended to a path $\pi^{\prime}$ that
satisfies weak $\mathcal{B}$-hyperfairness of actions, such that all
occurrences of blocking actions in $\pi^{\prime}$ are part of $\pi$.

######  Proof C.6.

Let $\pi$ be an arbitrary finite path. We prove that $\pi$ can be extended to
path $\pi^{\prime}$ that satisfies weak $\mathcal{B}$-hyperfairness of
actions, such that there are no occurrences of blocking actions in the
extension. We do this through construction of the path $\pi^{\prime}$. We will
construct $\pi^{\prime}$ in steps. Let $\pi_{i}$ with $i\geq 0$ be the path
constructed in the $i$’th iteration, with $\pi_{0}=\pi$. Let $s_{i}$ be the
last state of $\pi_{i}$. For this construction, we use a queue $Q$ containing
non-blocking actions. At the start of the construction, $Q$ is initialised
with exactly one copy all non-blocking actions $\mathcal{B}$-reachable from
$s_{0}$, the final state of $\pi$, in some arbitrary order. The construction
has the following invariants: $Q$ contains exactly one copy of every non-
blocking action $\mathcal{B}$-reachable in the final state of the path
constructed so far. It may contain zero or one copies of non-blocking actions
not $\mathcal{B}$-reachable from this state. It contains no blocking actions.
Additionally, the only occurrences of blocking actions in the path constructed
thus far are in $\pi$.

At each step $i>0$, we do the following: first, we determine if $Q$ is empty
or not. If it is empty, we take $\pi_{i}=\pi_{i-1}$ and the construction
terminates. If $Q$ is not empty, we pop the head $a$ from $Q$. If $a$ is not
$\mathcal{B}$-reachable from $s_{i-1}$, then we let $\pi_{i}=\pi_{i-1}$ and go
to step $i+1$. The invariants are maintained because we only removed $a$ from
$Q$, and $a$ was not $\mathcal{B}$-reachable from $s_{i-1}=s_{i}$. If $a$ is
$\mathcal{B}$-reachable from $s_{i-1}$, then there exists some path
$\pi_{i}^{\prime}$ consisting of only non-blocking actions starting in
$s_{i-1}$ and ending in a state $s_{i-1}^{\prime}$ such that some transition
$t_{a}$ with $\mathit{act}(\mathit{t_{a}})=a$ is enabled in
$s_{i-1}^{\prime}$. Let
$\pi_{i}=\pi_{i-1}\cdot\pi_{i-1}^{\prime}t_{a}\mathit{trgt}(\mathit{t_{a}})$
and append $a$ back to the end of $Q$. Then continue to step $i+1$. The
invariants are maintained in this case as well. This is because every action
$\mathcal{B}$-reachable in $s_{i}$ must also have been $\mathcal{B}$-reachable
from $s_{i-1}$, since $s_{i}$ is $\mathcal{B}$-reachable from $s_{i-1}$. Since
$Q$ at the start of this step contains the same actions as at the end of this
step, and by the invariant it contained all actions at the start that are
$\mathcal{B}$-reachable from $s_{i-1}$, it also contains all actions that are
$\mathcal{B}$-reachable from $s_{i}$ at the end of the step. Finally, the
segment we added did not contain any blocking actions, and $a$ itself is non-
blocking because all actions in $Q$ are non-blocking.

There are two potential outcomes to this construction: either $Q$ becomes
empty and the construction terminates, or $Q$ never becomes empty and the
construction continues infinitely. We prove that in either case, the path
$\pi^{\prime}$ that is ultimately constructed is weakly
$\mathcal{B}$-hyperfair of actions and does not contain occurrences of
blocking actions beyond those already present in $\pi$.

  * •

If $Q$ becomes empty and the construction terminates, then the final path
$\pi^{\prime}$ is $\pi_{i}$ for the $i$ on which $Q$ was determined to be
empty. The final state of $\pi^{\prime}$, $s^{\prime}$ is then a state in
which no non-blocking actions are $\mathcal{B}$-reachable. Hence, there are no
non-blocking actions perpetually $\mathcal{B}$-reachable on any suffix of
$\pi^{\prime}$ and so $\pi^{\prime}$ is trivially $\mathcal{B}$-WHFA.

  * •

If $Q$ never becomes empty then the construction continues forever. Let
$\pi^{\prime}$ be the infinite path $\pi_{\infty}$. Let $\pi^{\prime\prime}$
be an arbitrary suffix of $\pi^{\prime}$, and let $a$ be an arbitrary action
in $\overline{\mathit{\mathcal{B}}}$ that is perpetually
$\mathcal{B}$-reachable on $\pi^{\prime\prime}$. We prove $a$ occurs in
$\pi^{\prime\prime}$. Consider that if $a$ is perpetually
$\mathcal{B}$-reachable on $\pi^{\prime\prime}$, then it is
$\mathcal{B}$-reachable in every state of $\pi^{\prime\prime}$. Consider also
that, since $\pi^{\prime\prime}$ is a suffix of the infinite path
$\pi^{\prime}$, $\pi^{\prime\prime}$ is also infinite. In our construction, we
add only a finite number of steps to the path in every iteration. Therefore,
$\pi^{\prime\prime}$ was created as a part of $\pi^{\prime}$ over infinitely
many iterations. Since $a$ is enabled in every state of $\pi^{\prime\prime}$,
by the invariants $a$ must be in $Q$ at the start of all iterations of the
construction that contributed to $\pi^{\prime\prime}$, with possible exception
of the first. Since $Q$ is a queue and $\mathit{Act}$ is finite, $a$ will be
at the head of the queue during the construction of $\pi^{\prime\prime}$
infinitely many times. Whenever $a$ was at the head of the queue during the
construction, a finite number of steps were added to the path that ended with
a transion labelled with $a$. Hence, $a$ occurs in $\pi^{\prime\prime}$, and
so $\pi^{\prime}$ is $\mathcal{B}$-WHFA.

In both cases, that no new occurrences of blocking actions are added to the
path comes directly from the invariants.

######  Proposition C.7.

Weak $\mathcal{B}$-hyperfairness of actions is feasible.

######  Proof C.8.

This follows from C.5, which is a stronger property.

######  Proposition C.9.

Strong $\mathcal{B}$-hyperfairness of actions in feasible.

######  Proof C.10.

We prove that every finite path $\pi$ can be extended to a path $\pi^{\prime}$
that satisfies strong $\mathcal{B}$-hyperfairness of actions. Let $\pi$ be an
arbitrary finite path, then by C.5 we know that there exists a path
$\pi^{\prime}$ that extends $\pi$ and satisfies weak
$\mathcal{B}$-hyperfairness of actions, and has no occurrences of blocking
actions save those already present in $\pi$. We will use $\pi^{\prime}$ to
witness that there exists a strongly $\mathcal{B}$-hyperfair extension of
$\pi$, by proving $\pi^{\prime}$ satisfies strong $\mathcal{B}$-hyperfairness
as well as weak $\mathcal{B}$-hyperfairness.

Towards a contradiction, assume that $\pi^{\prime}$ does not satisfy strong
$\mathcal{B}$-hyperfairness of actions. Then $\pi^{\prime}$ must have a suffix
$\pi^{\prime\prime}$ such that there is an action
$a\in\overline{\mathit{\mathcal{B}}}$ that is relentlessly
$\mathcal{B}$-reachable in $\pi^{\prime\prime}$ and yet does not occur in
$\pi^{\prime\prime}$. If $a$ is relentlessly $\mathcal{B}$-reachable in
$\pi^{\prime\prime}$, it is also relentlessly $\mathcal{B}$-reachable in every
suffix of $\pi^{\prime\prime}$. Let $\pi^{\prime\prime\prime}$ be a suffix of
$\pi^{\prime\prime}$ such that $\pi^{\prime\prime\prime}$ does not contain any
occurrences of blocking actions. That such a suffix exists follows from
$\pi^{\prime}$ only having occurrences of blocking actions in the finite
prefix $\pi$. We now have the path $\pi^{\prime\prime\prime}$ on which $a$ is
relentlessly $\mathcal{B}$-reachable and that does not contain occurrences of
blocking actions. Let $s$ be an arbitrary state on $\pi^{\prime\prime\prime}$.
Since $a$ is relentlessly $\mathcal{B}$-reachable, there must be a state
$s^{\prime}$ on $\pi^{\prime\prime\prime}$ past $s$ such that $a$ is
$\mathcal{B}$-reachable from $s^{\prime}$. And since there are no occurrences
of blocking actions on $\pi^{\prime\prime\prime}$, $a$ is also
$\mathcal{B}$-reachable from $s$. Hence, $a$ is $\mathcal{B}$-reachable from
every state of $\pi^{\prime\prime\prime}$ and is therefore perpetually
$\mathcal{B}$-reachable on $\pi^{\prime\prime\prime}$.

We constructed $\pi^{\prime\prime\prime}$ as a suffix of $\pi^{\prime\prime}$
which is a suffix of $\pi^{\prime}$, so $\pi^{\prime\prime\prime}$ is a suffix
of $\pi^{\prime}$ as well. We know that $\pi^{\prime}$ satisfies weak
$\mathcal{B}$-hyperfairness, so since $a$ is perpetually
$\mathcal{B}$-reachable on $\pi^{\prime\prime\prime}$, a suffix of
$\pi^{\prime}$, $a$ also occurs in $\pi^{\prime\prime\prime}$. Since
$\pi^{\prime\prime\prime}$ is a suffix of $\pi^{\prime\prime}$, we know that
$a$ occurs on $\pi^{\prime}$. However, we assumed previously that $a$ does not
occur on $\pi^{\prime\prime}$. We have reached a contradiction and therefore
conclude that $\pi^{\prime}$ satisfies strong $\mathcal{B}$-hyperfairness as
well as weak $\mathcal{B}$-hyperfairness.

######  Proposition C.11.

$\mathcal{B}$-justness of actions is feasible.

######  Proof C.12.

Let $\pi$ be an arbitrary finite path. We prove $\pi$ can be extended to a
path $\pi^{\prime}$ satisfying $\mathcal{B}$-justness of actions. We do this
through construction of such a path $\pi^{\prime}$. We do this in steps, where
$\pi_{i}$ with $i\geq 0$ represents the path constructed in step $i$. Let
$\pi_{0}=\pi$. Let $s_{i}$ be the last state of $\pi_{i}$ for all $i\geq 0$.
For this construction we use a queue $Q$.

The initial contents of $Q$ are determined by $\pi_{0}$: it contains exactly
one copy of every non-blocking action that is enabled in some state of
$\pi_{0}$ but has not been subsequently eliminated. The order of these actions
is arbitrary. The construction has the following invariant: $Q$ contains
exactly one copy of every non-blocking action that is enabled in some state of
the path constructed so far, but has not been subsequently eliminated.
Trivially, this invariant holds at initialisation.

The construction proceeds as follows: in step $i$, with $i>0$, we construct
$\pi_{i}$ from $\pi_{i-1}$ using $Q$. At this point, $Q$ contains exactly one
copy of every non-blocking action that was enabled in some state of
$\pi_{i-1}$ but has not subsequently been eliminated. If $Q$ is empty, let
$\pi_{i}=\pi_{i-1}$ and the construction terminates. Otherwise, we pop the
head of $Q$, let this action be $a$. The action $a$ must have been enabled in
some state $s_{a}$ of $\pi_{i-1}$ such that the subpath $\pi_{a}$ of
$\pi_{i-1}$ from $s_{a}$ to $s_{i-1}$ does not contain an occurrence of an
action that eliminates $a$. By the second property of concurrency relations on
actions, $a$ must still be enabled in $s_{i-1}$. Let $t_{a}$ be a transition
enabled in $s_{i-1}$ with $\mathit{act}(\mathit{t_{a}})=a$, let
$\pi_{i}=\pi_{i-1}t_{a}\mathit{trgt}(\mathit{t_{a}})$. We modify $Q$ in two
steps: firstly, every action $b$ that is in $Q$ such that
$b\mathbin{{\centernot\smile}^{\raisebox{-1.20552pt}{\tiny$\bullet$}}}a$ is
removed from $Q$. Secondly, every non-blocking action that is enabled in
$\mathit{trgt}(\mathit{t_{a}})=s_{i}$ that is not yet in $Q$ gets appended to
$Q$ in some arbitrary order. At this point, the invariant is again satisfied:
by removing all actions that are eliminated by $a$ from $Q$, we ensure that
$Q$ no longer contains those actions that were not eliminated in $\pi_{i-1}$
but are eliminated in $\pi_{i}$. By afterwards adding those actions that are
enabled in $s_{i}$, we include those actions that are newly enabled without
being eliminated yet. We proceed to the next iteration.

This construction either terminates after finitely many steps, or continues
forever, the latter case results in an infinite path. We show that in either
case, the constructed path $\pi^{\prime}$ satisfies $\mathcal{B}$-justness of
actions.

  * •

If the construction terminates during step $i$, then $\pi^{\prime}=\pi_{i}$.
By the invariant, $Q$ contains exactly those non-blocking actions that are
enabled in $\pi^{\prime}$ without being subsequently eliminated, and $Q$ must
be empty because the construction terminated. Let $s^{\prime}$ be the final
state of $\pi^{\prime}$. If there are non-blocking actions enabled in
$s^{\prime}$, then those actions are enabled in $\pi^{\prime}$ without being
subsequently eliminated, since there are no further transitions in
$\pi^{\prime}$. Since no such actions can exist, we know $s^{\prime}$ is a
$\mathcal{B}$-locked state. If there were a non-blocking action enabled on
$\pi^{\prime}$ that has not subsequently been eliminated through the
occurrence of an interfering action, then by the second property of
concurrency relations on actions that non-blocking action should still be
enabled on $s^{\prime}$. Since $s^{\prime}$ is a $\mathcal{B}$-locked state,
this is impossible and hence $\pi^{\prime}$ is $\mathcal{B}$-JA.

  * •

If the construction never terminates, then we construct an infinite path
$\pi_{\infty}=\pi^{\prime}$. Let $s$ be some arbitrary state of $\pi^{\prime}$
and let $a$ be an arbitrary non-blocking action that is enabled in $s$. We
prove that $a$ is eliminated in the suffix $\pi_{a}^{\prime}$ of
$\pi^{\prime}$ starting in $s$. Towards a contradiction, assume that $a$ is
not eliminated in $\pi^{\prime}_{a}$. Let $i>0$ be the first iteration of the
construction such that $s_{i-1}$ is in $\pi_{a}^{\prime}$. Since $s_{i-1}$ is
in $\pi_{a}^{\prime}$, it either is $s$ or comes after $s$, and since $a$ is
not eliminated in $\pi_{a}^{\prime}$ it must be the case, by the second
property of concurrency relations on actions, that $a$ is enabled in
$s_{i-1}$. Hence, by the invariant, $Q$ must have contained $a$ at the start
of iteration $i$. Since $Q$ contains at most one copy of every non-blocking
action and $\mathit{Act}$ is finite, there are finitely many actions before
$a$ in the queue. Every iteration, at least one action gets removed from $Q$
and new actions get appended. Hence, $a$ is either removed early or eventually
becomes the head of the queue. If $a$ is removed early, this is because an
action occurred that eliminates $a$, hence $a$ is eliminated in
$\pi_{a}^{\prime}$. If $a$ becomes the head of the queue, then we ensure $a$
itself occurs. By the first property of concurrency relations on actions, $a$
eliminates itself. In this case too, $a$ is eliminated in $\pi_{a}^{\prime}$.
This contradicts our assumption that $a$ was not eliminated. We conclude that
all non-blocking actions that are enabled in some state of $\pi^{\prime}$ are
subsequently eliminated. Hence, $\pi^{\prime}$ satisfies
$\mathcal{B}$-justness of actions.

In either case, the finite path $\pi$ can be extended to a path $\pi^{\prime}$
that satisfies $\mathcal{B}$-JA. We conclude $\mathcal{B}$-justness of actions
is feasible.

##  Appendix D Correctness of Formulae

In this appendix, we provide the correctness proofs for the presented
formulae. First, there is a supporting proposition we use repeatedly
throughout the different proofs.

All our proofs assume a fixed LTSC
$M=(\mathcal{S},s_{\mathit{init}},\mathit{Act},\mathit{Trans},\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}})$,
although the $\mathbin{\smile^{\raisebox{-0.60275pt}{\tiny$\bullet$}}}$ is
only relevant for JA. We also refer to an arbitrary environment $\mathit{e}$
and set of blocking actions $\mathcal{B}\subseteq\mathit{Act}$. We define the
length of a finite path to be the number of transitions occurring in it. A
path of length $0$ contains only a single state and is called the empty path.

###  D.1 Supporting Proposition

The following proposition gives the semantics of a least fixed point formula
that occurs in several of our presented formulae.

######  Proposition D.1.

For all states $s\in\mathcal{S}$, formal variables $Y$, modal $\mu$-calculus
formulae $\phi_{1}$ and $\phi_{2}$ that do not depend on $Y$, and set of
actions $\alpha$, it is the case that $s$ is in
$\llbracket\mu\mathit{Y}.(\mathit{\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)})\rrbracket$ if, and only if, $s$ admits a finite path $\pi$ satisfying the
following requirements:

  1. 1.

all actions occurring in $\pi$ are in $\alpha$, and

  2. 2.

all states in $\pi$ are in $\llbracket\phi_{1}\rrbracket$, and

  3. 3.

the final state of $\pi$ is in $\llbracket\phi_{2}\rrbracket$.

We first need to prove a supporting lemma. To prove this lemma, we use an
alternate characterisation of the semantics of least fixpoints to the one we
presented in Section 2.2. We only give the definitions that we require for our
proofs. The following presentation can be found in [8, 9], amongst others.

Let $Y$ be an arbitrary formal variable, $\phi$ be an arbitrary modal
$\mu$-calculus formula and $\mathit{e}$ an arbitrary environment. Let $T$ be
the transformer associated with $\mu Y.\phi$, defined as

$T(\mathcal{F})=\\{s\in\mathcal{S}\mid
s\in\llbracket\phi\rrbracket_{\mathit{e}[Y:=\mathcal{F}]}\\}$

And define

$\displaystyle T^{0}(\mathcal{F})$ $\displaystyle=\mathcal{F}$ $\displaystyle
T^{i+1}(\mathcal{F})$ $\displaystyle=T(T^{i}(\mathcal{F}))$

Then we can calculate the semantics of $\mu\mathit{Y}.\mathit{\phi}$ under
$\mathit{e}$ as:

$\displaystyle\llbracket\mu\mathit{Y}.\mathit{\phi}\rrbracket_{\mathit{e}}$
$\displaystyle=\bigcup_{0\leq i\leq|\mathcal{S}|}T^{i}(\emptyset)$

Note that this definition only works for finite systems, since it uses
$|\mathcal{S}|$. A version exists for infinite systems, but is not relevant
here. We call $T^{i}(\emptyset)$ the $i$’th approximation of $\phi$.

For the subsequent lemmas, we fix formal variable $Y$.

######  Lemma D.2.

For all environments $\mathit{e}$, states $s\in\mathcal{S}$, modal
$\mu$-calculus formulae $\phi_{1}$ and $\phi_{2}$ that do not depend on $Y$,
sets of actions $\alpha$, and natural numbers $0\leq i\leq|\mathcal{S}|$, it
holds that: $s$ is in the $i$’th approximation of
$\mu\mathit{Y}.(\mathit{\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)})$ under $\mathit{e}$ if, and only if, $s$ admits a finite path $\pi$
meeting the following conditions:

  1. 1.

$\pi$ has length at most $i-1$, and

  2. 2.

only actions in $\alpha$ occur in $\pi$, and

  3. 3.

all states in $\pi$ are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and

  4. 4.

the final state of $\pi$ is in $\llbracket\phi_{2}\rrbracket_{\mathit{e}}$.

######  Proof D.3.

Let $T$ be the transformer of
$\mu\mathit{Y}.(\mathit{\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)})$. We prove that $s$ is in $T^{i}(\emptyset)$ if, and only if, $s$ admits
a finite path $\pi$ of length at most $i-1$ on which only actions in $\alpha$
occur, all states are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and
which ends in a state
$s^{\prime}\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. We do this by
induction on $i$.

For the first _base_ , take $i=0$. Note that $s$ is in the $i$’th
approximation if $s\in T^{0}(\emptyset)$. However,
$T^{0}(\emptyset)=\emptyset$, so $s$ cannot be in the $0$’th approximation.
Indeed, we cannot have a path of length at most $-1$. So in both directions of
the bi-implication, the left side of the implication does not hold.

For the second _base_ , take $i=1$. We prove the bi-implication.

  * •

First, assume $s$ is in the first approximation. Then $s\in
T^{1}(\emptyset)=\\{s\in\mathcal{S}\mid
s\in\llbracket\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)\rrbracket_{\mathit{e}[Y:=\emptyset]}\\}$. Hence,
$s\in\llbracket\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)\rrbracket_{\mathit{e}[Y:=\emptyset]}$. Through the semantics of the modal
$\mu$-calculus, and using that $\phi_{1}$ and $\phi_{2}$ do not depend on $Y$,
this becomes
$s\in(\llbracket\phi_{1}\rrbracket_{\mathit{e}}\cap(\llbracket\phi_{2}\rrbracket_{\mathit{e}}\cup\llbracket\langle\mathit{\alpha}\rangle
Y\rrbracket_{\mathit{e}[Y:=\emptyset]})$. Therefore,
$s\in\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and $s$ is in
$\llbracket\phi_{2}\rrbracket_{\mathit{e}}$ or
$s\in\\{s\in\mathcal{S}\mid\exists_{s^{\prime}\in\mathcal{S}}.s\xrightarrow{\alpha}s^{\prime}\land
s^{\prime}\in\emptyset\\}$. It is not possible for a state $s^{\prime}$ to
exist that is in $\emptyset$, hence
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. Let $\pi$ be the empty path
from $s$. No actions occur on $\pi$, so trivially all occurring actions are in
$\alpha$. Since $s$ satisfies both $\phi_{1}$ and $\phi_{2}$ under
$\mathit{e}$, the other conditions are met as well. We conclude that $s$
admits a finite path of length at most 0 on which only actions in $\alpha$
occur, all states are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and
which ends in a state in $\llbracket\phi_{2}\rrbracket_{\mathit{e}}$.

  * •

Second, assume $s$ admits a path of length at most $0$ on which only actions
on $\alpha$ occur, all states are in
$\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and which ends in a state in
$\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. The only path starting in $s$ of
length at most $0$ is the path consisting of only $s$. Hence,
$s\in\llbracket\phi_{1}\rrbracket_{\mathit{e}}$ and
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. Since $\phi_{1}$ and
$\phi_{2}$ do not depend on $Y$, we also have
$s\in\llbracket\phi_{1}\rrbracket_{\mathit{e}[Y:=\emptyset]}$ and
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}[Y:=\emptyset]}$. If
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}[Y:=\emptyset]}$, it is also in
the superset
$\llbracket\phi_{2}\rrbracket_{\mathit{e}[Y:=\emptyset]}\cup\llbracket\langle\mathit{\alpha}\rangle
Y\rrbracket_{\mathit{e}[Y:=\emptyset]}$. We conclude that
$s\in\\{s\in\mathcal{S}\mid
s\in\llbracket\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)\rrbracket_{\mathit{e}[Y:=\emptyset]}\\}=T^{1}(\emptyset)$ and hence $s$ is
in the first approximation.

The _induction hypothesis_ we use is that a state $s^{\prime}$ is in the
$k$’th approximation of $\mu
Y.(\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle Y))$ if, and only
if, $s^{\prime}$ admits a finite path of length at most $k-1$ on which only
actions in $\alpha$ occur, all states are in
$\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and which ends in a state in
$\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. This is for all $k\geq 1$.

For the _step_ case, we prove the claim for $k+1$. Let $S$ be the set of
states that admit finite paths of length at most $k-1$ on which only actions
in $\alpha$ occur, all states are in
$\llbracket\phi_{1}\rrbracket_{\mathit{e}}$ and which end in a state in
$\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. By the induction hypothesis,
$S=T^{k}(\emptyset)$. Since this lemma is a bi-implication, we prove both
directions separately.

  * •

We assume $s\in T^{k+1}(\emptyset)$. We need to prove $s$ admits a path $\pi$
that is of length at most $k+1-1=k$, on which only actions in $\alpha$ occur,
all states are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and which ends
in a state in $\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. We have $s\in
T^{k+1}(\emptyset)=T(T^{k}(\emptyset))=T(S)$ Hence,
$s\in\\{s\in\mathcal{S}\mid
s\in\llbracket\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)\rrbracket_{\mathit{e}[Y:=S]}\\}$. This reduces to
$s\in\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}\lor
s\in\\{s\in\mathcal{S}\mid\exists_{s^{\prime}\in\mathcal{S}}.s\xrightarrow{\alpha}s^{\prime}\land
s^{\prime}\in S\\}$, because $\phi_{1}$ and $\phi_{2}$ do not depend on $Y$.
We do a case distinction on whether
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}$.

    * –

If $s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}$, then the path $\pi$
consisting of only $s$ is a path of length 0 on which only actions in $\alpha$
occur, and all states are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and
which ends in a state in $\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. Since we
assumed $k\geq 1$, we know $0\leq k$, hence $s$ admits a path meeting the
requirements of length at most $k$.

    * –

If $s\not\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}$, then
$s\in\\{s\in\mathcal{S}\mid\exists_{s^{\prime}\in\mathcal{S}}.s\xrightarrow{\alpha}s^{\prime}\land
s^{\prime}\in S\\}$. Hence, there exists a state $s^{\prime}$ such that that
there exists an $\alpha$-transition $t$ from $s$ to $s^{\prime}$ and
$s^{\prime}$ is in $S$. Since $s^{\prime}\in S$, we know $s^{\prime}$ admits a
path $\pi^{\prime}$ of length at most $k-1$, on which only actions in $\alpha$
occur, all states are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and
which ends in a state satisfying $\llbracket\phi_{2}\rrbracket_{\mathit{e}}$.
Let $\pi=st\pi^{\prime}$. Since $\pi^{\prime}$ has length at most $k-1$ and we
added one transition, $\pi$ has length at most $k$. Additionally, $t$ is an
$\alpha$-transition, as are all transitions in $\pi^{\prime}$, so all
transitions in $\pi$ are labelled with actions in $\alpha$. Since
$s\in\llbracket\phi_{1}\rrbracket_{\mathit{e}}$ and all states in
$\pi^{\prime}$ are as well, all states on $\pi$ meet this requirement.
Finally, since $\pi^{\prime}$ ends in a state satisfying
$\llbracket\phi_{2}\rrbracket_{\mathit{e}}$, so does $\pi$. Hence, $\pi$ is a
witness that $s$ admits a path meeting all requirements.

In both cases $s$ admits such a path $\pi$ of length at most $k$.

  * •

We assume $s$ admits a path $\pi$ of length at most $k$ such that all
transitions on $\pi$ are labelled with actions in $\alpha$, all states are in
$\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and $\pi$ ends in a state
satisfying $\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. We prove $s\in
T^{k+1}(\emptyset)=T(T^{k}(\emptyset))=T(S)=\\{s\in\mathcal{S}\mid
s\in\llbracket\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)\rrbracket_{\mathit{e}[Y:=S]}\\}$. We do a case distinction on whether the
length of $\pi$ is zero.

    * –

If the length of $\pi$ is zero, then $\pi=s$ and
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. Additionally, since all
states on $\pi$ are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, so is $s$.
Since $\phi_{1}$ and $\phi_{2}$ do not depend on $Y$, we also have
$s\in\llbracket\phi_{1}\rrbracket_{\mathit{e}[Y:=S]}$ and
$s\in\llbracket\phi_{2}\rrbracket_{\mathit{e}[Y:=S]}$, and hence also
$s\in\llbracket\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)\rrbracket_{\mathit{e}[Y:=S]}$. Thus, $s\in T(S)=T^{k+1}(\emptyset)$.

    * –

If the length of $\pi$ is greater than zero, then there is at least one
transition in $\pi$. Let $t$ be the first transition of $\pi$. Since there are
only $\alpha$-transitions in $\pi$, $t$ is an $\alpha$-transition. Let
$s^{\prime}$ be the target of $t$, and let $\pi^{\prime}$ be the suffix of
$\pi$ starting in $s^{\prime}$. Then since the length of $\pi$ is at most $k$,
the length of $\pi^{\prime}$ is at most $k-1$. Hence, $\pi^{\prime}$ witnesses
that $s^{\prime}$ admits a path of length at most $k-1$ on which only
$\alpha$-transitions occur, all states are in
$\llbracket\phi_{1}\rrbracket_{\mathit{e}}$, and which ends in a state
satisfying $\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. Hence, $s\in S$. So
$s$ admits an $\alpha$-transition, namely $t$, to a state in $S$, namely
$s^{\prime}$. Therefore $s\in\llbracket\langle\mathit{\alpha}\rangle
Y\rrbracket_{\mathit{e}[Y:=S]}$ and hence also
$s\in\llbracket\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)\rrbracket_{\mathit{e}[Y:=S]}$. We conclude that $s\in
T(S)=T^{k+1}(\emptyset)$.

In both cases we demonstrate that $s$ is in the $k+1$’th approximation.

We have proven both sides of the bi-implication that $s$ is in the $k+1$’th
approximation of $\mu
Y.(\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle Y))$ if, and only
if, $s$ admits a finite path of length at most $k$ on which only $\alpha$
actions occur, all states are in $\llbracket\phi_{1}\rrbracket_{\mathit{e}}$,
and which ends in a state satisfying
$\llbracket\phi_{2}\rrbracket_{\mathit{e}}$. This proves the step case.

By induction, we have proven the claim holds for all $i\geq 0$. Therefore it
also holds for all $0\leq i\leq|\mathcal{S}|$. We conclude the lemma holds.

We can now prove the main claim, D.1: See D.1

######  Proof D.4.

This claim is a bi-implication, so we prove both directions.

  * •

If $s$ is in the semantics of
$\mu\mathit{Y}.(\mathit{\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)})$, then $s$ is in the least fixed point of the transformer $T$ matching
this formula. Hence, there are one or more natural numbers $0\leq
i\leq|\mathcal{S}|$ such that $s\in T^{i}(\emptyset)$. Let $i$ be the smallest
such number, then by D.2, $s$ admits a path of length at most $i-1$ that meets
all three conditions. This path witnesses that $s$ indeed admits a path
meeting all three conditions.

  * •

Assume $s$ admits at least one finite path that satisfies all three
conditions. Let $\pi$ be the shortest such path that $s$ admits. Let $k$ be
the length of $\pi$. We first prove that $0\leq k+1\leq|\mathcal{S}|$.
Trivially, a path has length at least $0$, so $0\leq k+1$. Towards a
contradiction, assume $k+1>|\mathcal{S}|$. A path of length $j$ contains $j+1$
individual instances of states: the initial state of the path and the target
of every transition on the path. The path $\pi$ has length $k$, and so
contains at least $k+1$ individual occurrences of states, and
$k+1>|\mathcal{S}|$. Hence, $\pi$ contains strictly more than $|\mathcal{S}|$
individual instances of states. Considering there are exactly $|\mathcal{S}|$
states in the LTS, by the pigeonhole principle there must be at least one
state $s^{\prime}$ that is visited at least twice on $\pi$. Let $\pi_{1}$ be
the prefix of $\pi$ up until the first occurrence of $s^{\prime}$, and let
$\pi_{2}$ be the suffix of $\pi$ starting in the last occurrence of
$s^{\prime}$. Now let $\pi^{\prime}=\pi_{1}\cdot\pi_{2}$. This is a valid
path, since $\pi_{1}$ ends in state $s^{\prime}$ and $\pi_{2}$ starts in this
state. $\pi^{\prime}$ contains a subset of the actions and states of $\pi$,
and has the same final state as $\pi$, so it satisfies all three conditions.
Since we chose $s^{\prime}$ to be a state that occurred more than once on
$\pi$, $\pi^{\prime}$ contains at least one transition less than $\pi$ and
hence $\pi\neq\pi^{\prime}$. In fact, $\pi^{\prime}$ is shorter than $\pi$.
However, we chose $\pi$ to be the shortest path that meets all three
conditions starting in $s$. We have reached a contradiction. Hence, we
conclude that $k+1\leq|\mathcal{S}|$. This means that $s$ admits a path of
length at most $k$ with $0\leq k+1\leq|\mathcal{S}|$ that meets the three
conditions. By D.2, this means that $s$ is in the $k+1$’th approximation of
$\mu\mathit{Y}.(\mathit{\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)})$. Since the semantics of the formula are the union of all approximations,
we conclude $s$ is in
$\llbracket\mu\mathit{Y}.(\mathit{\phi_{1}\land(\phi_{2}\lor\langle\mathit{\alpha}\rangle
Y)})\rrbracket$.

We have proven both directions of the bi-implication.

###  D.2 Proof of Progress Formula

We prove Theorem 6.1: See 6.1

Formula 1 is:

$\neg\langle\mathit{\rho}\rangle\nu
X.(\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle
X)$

We fix arbitrary $\mathcal{B}$, $\rho$, $\alpha_{\mathit{f}}$ and
$\alpha_{\mathit{e}}$ for this proof. We first prove the formula without the
$\neg\langle\mathit{\rho}\rangle$ at the start. For this, let $S_{P}$ be the
set of states that admit $\mathcal{B}$-progressing paths that are
$(\varepsilon,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating. In other
words, these are the states that admit paths that are
$\mathcal{B}$-progressing and that are $\alpha_{\mathit{f}}$-free up until an
occurrence of an action in $\alpha_{\mathit{e}}$.

We first prove that $S_{P}$ is a fixed point of $\nu
X.(\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle
X)$, and then that it is the greatest fixed point.

######  Lemma D.5.

$S_{P}$ is a fixed point of the transformer $T_{P}$ defined by:

$T_{P}(\mathcal{F})=\bigcap_{a\in\overline{\mathit{\mathcal{B}}}}\\{s\in\mathcal{S}\mid
s\in\llbracket\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle
X\rrbracket_{\mathit{e}[X:=\mathcal{F}]}\\}$

######  Proof D.6.

To prove $S_{P}$ is a fixed point of $T_{P}$, we prove $T_{P}(S_{P})=S_{P}$.
We do this through mutual set inclusion.

  * •

Let $s$ be an arbitrary state in $T_{P}(S_{P})$. We therefore know that
$s\in\llbracket\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle
X\rrbracket_{\mathit{e}[X:=S_{P}]}$. We do a case distinction on which of
those conditions $s$ satisfies.

    * –

If $s$ satisfies $\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}$, then
there is a transition $t$ enabled in $s$ that is labelled with an action in
$\alpha_{\mathit{e}}$. Let $\pi=st\mathit{trgt}(\mathit{t})$. This is a path
that is $\alpha_{\mathit{f}}$-free up until the first occurrence of an action
in $\alpha_{\mathit{e}}$. We now extend $\pi$ arbitrarily, either until a
$\mathcal{B}$-locked state is reached or infinitely. This is always possible:
as long we are not in a $\mathcal{B}$-locked state there is always a non-
blocking action enabled that can be appended to the path we are constructing.
This way, a $\mathcal{B}$-progressing path that is
$(\varepsilon,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating is
constructed.

    * –

If $s$ satisfies $[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}$, then
$s$ is a $\mathcal{B}$-locked state. Hence, the empty path is a path that $s$
admits that is $\mathcal{B}$-progressing and on which, trivially, no actions
in $\alpha_{\mathit{f}}$ occur. Hence, $s$ admits a $\mathcal{B}$-progressing
path that is
$(\varepsilon,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

    * –

If $s$ satisfies
$\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle X$ with
$X=S_{P}$, then $s$ admits a transition labelled with an action not in
$\alpha_{\mathit{f}}$ to a state in $S_{P}$. Let $t$ be such a transition and
$s^{\prime}=\mathit{trgt}(\mathit{t})$. Then since $s^{\prime}\in S_{P}$,
$s^{\prime}$ admits a path $\pi^{\prime}$ that is $\mathcal{B}$-progressing
and $\alpha_{\mathit{f}}$-free up until the first occurrence of an action in
$\alpha_{\mathit{e}}$. Let $\pi=st\pi^{\prime}$: this path too is
$\mathcal{B}$-progressing and $\alpha_{\mathit{f}}$-free up until the first
occurrence of an action in $\alpha_{\mathit{e}}$. Hence, $\pi$ witnesses that
$s$ admits a $\mathcal{B}$-progressing path that is
$(\varepsilon,\alpha_{\mathit{f}},\alpha_{\mathit{e}})$-violating.

Therefore $s\in T_{P}(S_{P})\Rightarrow s\in S_{P}$.

  * •

Let $s$ be an arbitrary state in $S_{P}$, then $s$ admits a path $\pi$ that is
$\mathcal{B}$-progressing and $\alpha_{\mathit{f}}$-free up until the first
occurrence of $\alpha_{\mathit{e}}$. We prove
$s\in\llbracket\langle\mathit{\alpha_{\mathit{e}}}\rangle\mathit{tt}\lor[\mathit{\overline{\mathit{\mathcal{B}}}}]\mathit{ff}\lor\langle\mathit{\overline{\mathit{\alpha_{\mathit{f}}}}}\rangle
X\rrbracket_{\mathit{e}[X:=S_{P}]}$. First, we do a case distinction on
whether $\pi$ is the empty path.

    * –