c^{\prime}Tc\implies\forall[C_{i}]^{n}_{i}\in\mathbb{E}_{c}^{R}.\leavevmode\nobreak\
\exists\,[C^{\prime}_{j}]^{m}_{j}\in\mathbb{E}_{c^{\prime}}^{R^{\prime}}.\leavevmode\nobreak\
\\\ \exists\bigl{[}h_{k}\bigr{]}_{k}^{n}.\leavevmode\nobreak\ (\forall
k<n.\leavevmode\nobreak\ \forall k^{\prime}\leq k.\leavevmode\nobreak\
h_{k^{\prime}}\leq h_{k})\leavevmode\nobreak\ \land\\\ \forall
n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}=h_{n^{\prime}}<m.\leavevmode\nobreak\
O(C_{n^{\prime}})=O^{\prime}(C^{\prime}_{m^{\prime}})$

  1. 1.

_New:_ $c^{\prime}\in\mathrm{dom}(T)$.

  2. 2.

_New:_ $c$ _s.t._ $c^{\prime}Tc$.

  3. 3.

_New:_ $\bigl{[}C_{i}\bigr{]}_{i}^{n}\in\mathbb{E}_{c}^{R}$.

  4. 4.

_Pick:_
$\bigl{[}C^{\prime}_{j}\bigr{]}_{j}^{m}\in\mathbb{E}_{c^{\prime}}^{R^{\prime}}$
_s.t._

    1. (a)

$\forall n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}<m.\leavevmode\nobreak\
O(C_{n^{\prime}})=O^{\prime}(C^{\prime}_{m^{\prime}})$

      1. $\triangleright$

_Proof:_ Exists by the assumption.

  5. 5.

_Pick:_ $\bigl{[}h_{k}\bigr{]}_{k}^{n}$ _s.t._

    1. (a)

$\forall k^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}<m.\leavevmode\nobreak\
O(C_{k^{\prime}})=O^{\prime}(C^{\prime}_{m^{\prime}})\land
h_{k^{\prime}}=m^{\prime}$

      1. $\triangleright$

_Proof:_ Such $m^{\prime}$ exists by step 4a, and thus we can construct the
sequence with $h_{k^{\prime}}=m^{\prime}$.

    2. (b)

$\forall k^{\prime}<n.\forall k^{\prime\prime}\leq
k^{\prime}.\leavevmode\nobreak\
O(C_{k^{\prime}})=O(C_{k^{\prime\prime}})\implies
h_{k^{\prime\prime}}=h_{k^{\prime}}$

      1. $\triangleright$

_Proof:_ If two $k^{\prime}$ and $k^{\prime\prime}$ have the same observation,
then we can pick the same $m^{\prime}$ for both.

  6. 6.

_Suffices:_

    1. (a)

$\forall k<n.\leavevmode\nobreak\ \forall k^{\prime}\leq
k.\leavevmode\nobreak\ h_{k^{\prime}}\leq h_{k}$

    2. (b)

$\forall n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}=h_{n^{\prime}}<m.\leavevmode\nobreak\
O(C_{n^{\prime}})=O^{\prime}(C^{\prime}_{m^{\prime}})$

  7. 7.

$\forall k<n.\leavevmode\nobreak\ \forall k^{\prime}\leq
k.\leavevmode\nobreak\ h_{k^{\prime}}\leq h_{k}$

    1. (a)

$\forall k<n.\leavevmode\nobreak\ \forall k^{\prime}\leq
k.\leavevmode\nobreak\ O(C_{k^{\prime}})\leq_{O}O(C_{k})$

    2. (b)

$\forall l<m.\leavevmode\nobreak\ \forall l^{\prime}\leq
l.\leavevmode\nobreak\
O^{\prime}(C_{l^{\prime}})\leq_{O^{\prime}}O^{\prime}(C_{l})$

      1. $\triangleright$

_Proof:_ By the definition of the monotonicity of $O$ and $O^{\prime}$.

    3. (c)

_New:_ $k<n$.

    4. (d)

_New:_ $k^{\prime}\leq k$.

    5. (e)

$O(C_{k^{\prime}})\leq_{O}O(C_{k})$

      1. $\triangleright$

_Proof:_ By step 7a

    6. (f)

$O^{\prime}(C_{h_{k^{\prime}}})\leq_{O^{\prime}}O^{\prime}(C_{h_{k}})$

      1. $\triangleright$

_Proof:_ Follows from previous step by the equality of observations $O$ and
$O^{\prime}$ in step 5a.

    7. (g)

_Case:_ $O^{\prime}(C_{h_{k^{\prime}}})=_{O^{\prime}}O^{\prime}(C_{h_{k}})$

      1. i.

$O(C_{k^{\prime}})=_{O}O(C_{k})$

      2. ii.

$h_{k^{\prime}}=h_{k}$

        1. $\triangleright$

_Proof:_ Follows step 5b applied to previous step.

      3. iii.

$h_{k^{\prime}}\leq h_{k}$

    8. (h)

_Case:_ $O^{\prime}(C_{h_{k^{\prime}}})<_{O^{\prime}}O^{\prime}(C_{h_{k}})$

      1. i.

$h_{k^{\prime}}<h_{k}$

        1. $\triangleright$

_Proof:_ Follows from the definition of monotonicity of $O^{\prime}$.

      2. ii.

$h_{k^{\prime}}\leq h_{k}$

    9. (i)

_QED_

  8. 8.

$\forall n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}=h_{n^{\prime}}<m.\leavevmode\nobreak\
O(C_{n^{\prime}})=O^{\prime}(C^{\prime}_{m^{\prime}})$

    1. (a)

_New:_ $n^{\prime}<n$.

    2. (b)

_Pick:_ $m^{\prime}=h_{n^{\prime}}<m$.

    3. (c)

$O(C_{n^{\prime}})=O^{\prime}(C^{\prime}_{m^{\prime}})$

      1. $\triangleright$

_Proof:_ By construction of the sequence in step 5a with $n^{\prime}$ in place
of $k^{\prime}$.

    4. (d)

_QED_

  9. 9.

_QED_

See 5.9

######  Proof B.2.

_Assume:_

  1. 1.

$R\leavevmode\nobreak\
\,^{O}\negmedspace\xrightleftharpoons{T}\\!^{O^{\prime}}\,R^{\prime}$

  2. 2.

$R^{\prime}\leavevmode\nobreak\
\,{}^{O^{\prime}}\negmedspace\xrightleftharpoons{T^{\prime}}\\!^{O^{\prime\prime}}\,R^{\prime\prime}$

_Prove:_

  1. $\triangleright$

$R\leavevmode\nobreak\ \,^{O}\negmedspace\xrightleftharpoons{T\circ
T^{\prime}}\\!^{O^{\prime\prime}}\,R^{\prime\prime}$

_Suffices:_

  1. $\triangleright$

$\forall\,c^{\prime\prime}\in\mathrm{dom}(T^{\prime}).\leavevmode\nobreak\
\forall c.\leavevmode\nobreak\ c^{\prime\prime}(T\circ
T^{\prime})c\implies\forall[C_{i}]^{n}_{i}\in\mathbb{E}_{c}^{R}.\leavevmode\nobreak\
\exists\,[C^{\prime\prime}_{j}]^{m}_{j}\in\mathbb{E}_{c^{\prime\prime}}^{R^{\prime\prime}}.\leavevmode\nobreak\
\\\ \forall n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}<m.\leavevmode\nobreak\
O(C_{n^{\prime}})=O^{\prime}(C^{\prime\prime}_{m^{\prime}})$

  1. 1.

_New:_ $c^{\prime\prime}\in dom(T^{\prime})$.

  2. 2.

_New:_ $c^{\prime}$ _s.t._ $c^{\prime\prime}T^{\prime}c^{\prime}$.

  3. 3.

_New:_ $c$ _s.t._ $c^{\prime}Tc$.

    1. $\triangleright$

_Note:_ $c^{\prime\prime}T^{\prime}c^{\prime}\land c^{\prime}Tc$ therefore
$c^{\prime\prime}(T\circ T^{\prime})c$.

  4. 4.

_New:_
$\bigl{[}C_{k}^{\prime}\bigr{]}_{k}^{l}\in\mathbb{E}_{c^{\prime}}^{R^{\prime}}$.

  5. 5.

_New:_ $\bigl{[}C_{i}\bigr{]}_{i}^{n}\in\mathbb{E}_{c}^{R}$.

  6. 6.

_Pick:_
$\bigl{[}C_{j}^{\prime\prime}\bigr{]}_{j}^{m}\in\mathbb{E}_{c^{\prime\prime}}^{R^{\prime\prime}}$
_s.t._ $\forall k^{\prime}<l.\leavevmode\nobreak\ \exists
m^{\prime}<m.\leavevmode\nobreak\
O^{\prime}(C_{k^{\prime}})=O^{\prime\prime}(C^{\prime\prime}_{m^{\prime}})$

    1. $\triangleright$

_Proof:_ Exists by expanded definition of assumption 2.

  7. 7.

_Suffices:_ $\forall n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}<m.\leavevmode\nobreak\
O(C_{n^{\prime}})=O^{\prime}(C^{\prime\prime}_{m^{\prime}})$

    1. $\triangleright$

_Proof:_ By definition after elimination of quantifiers.

  8. 8.

_New:_ $n^{\prime}<n$.

  9. 9.

_Pick:_ $k^{\prime}<l$ _s.t._

    1. (a)

$O(C_{n^{\prime}})=O^{\prime}(C^{\prime}_{k^{\prime}})$

  10. $\triangleright$_Proof:_ Exists by assumption 1.

  11. 10.

_Pick:_ $m^{\prime}$ _s.t._

    1. (a)

$m^{\prime}<m$

    2. (b)

$O^{\prime}(C_{k^{\prime}})=O^{\prime\prime}(C^{\prime\prime}_{m^{\prime}})$

  12. $\triangleright$_Proof:_ Exists by step 6.

  13. 11.

_Suffices:_ $O(C_{n^{\prime}})=O^{\prime}(C^{\prime\prime}_{m^{\prime}})$.

    1. $\triangleright$

_Proof:_ By definition after elimination of quantifiers.

  14. 12.

$O(C_{n^{\prime}})=O^{\prime}(C^{\prime}_{k^{\prime}})=O^{\prime\prime}(C^{\prime\prime}_{m^{\prime}})$.

    1. $\triangleright$

_Proof:_ Follows from steps 9a and 10b.

  15. 13.

_QED_

See 5.11

######  Proof B.3.

  1. 1.

_New:_ $O^{\prime\prime}$

  2. 2.

_New:_ $R,O,T,O^{\prime},R^{\prime}$ _s.t._ $R\leavevmode\nobreak\
\,^{O}\negmedspace\xrightleftharpoons{T}\\!^{O^{\prime}}\,R^{\prime}$

    1. (a)

_Expanded:_ $\forall c\in\mathrm{dom}(T).\leavevmode\nobreak\ \forall
c^{\prime}.c^{\prime}Tc\implies\forall[C_{i}]^{n}_{i}\in\mathbb{E}_{c}^{R}.\leavevmode\nobreak\
\exists[C_{j}^{\prime}]^{m}_{j}\in\mathbb{E}_{c^{\prime}}^{R^{\prime}}.\leavevmode\nobreak\
\forall n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}<m.\leavevmode\nobreak\
\hbox{\pagecolor{lipicsLightGray}$O(C_{n^{\prime}})=O^{\prime}(C_{m^{\prime}})$}$

  3. 3.

_Suffices:_ $R\leavevmode\nobreak\ \,^{O^{\prime\prime}\circ
O}\negmedspace\xrightleftharpoons{T}\\!^{O^{\prime\prime}\circ
O^{\prime}}\,R^{\prime}$

    1. (a)

_Expanded:_ $\forall c\in\mathrm{dom}(T).\leavevmode\nobreak\ \forall
c^{\prime}.c^{\prime}Tc\implies\forall[C_{i}]^{n}_{i}\in\mathbb{E}_{c}^{R}.\leavevmode\nobreak\
\exists[C_{j}^{\prime}]^{m}_{j}\in\mathbb{E}_{c^{\prime}}^{R^{\prime}}.\leavevmode\nobreak\
\forall n^{\prime}<n.\leavevmode\nobreak\ \exists
m^{\prime}<m.\leavevmode\nobreak\
\hbox{\pagecolor{lipicsLightGray}$O^{\prime\prime}(O(C_{n^{\prime}}))=O^{\prime\prime}(O^{\prime}(C_{m^{\prime}}))$}$

      1. $\triangleright$

_Note:_ This expanded form differs only by the highlighted regions to step 2a.

  4. 4.

$\forall C,C^{\prime}.\leavevmode\nobreak\ O(C)=O^{\prime}(C^{\prime})\implies
O^{\prime\prime}(O(C))=O^{\prime\prime}(O^{\prime}(C^{\prime}))$

  5. 5.

$R\leavevmode\nobreak\
\,^{O}\negmedspace\xrightleftharpoons{T}\\!^{O^{\prime}}\,R^{\prime}\implies
R\leavevmode\nobreak\ \,^{O^{\prime\prime}\circ
O}\negmedspace\xrightleftharpoons{T}\\!^{O^{\prime\prime}\circ
O^{\prime}}\,R^{\prime}$

    1. $\triangleright$

_Proof:_ By expansion of the definitions, it follows directly by application
of step 4 to the highlighted regions.

  6. 6.

_QED_

###  B.2 Properties of Traces and Causality

In this section we will define traces and how they relate to executions, and
further define a causal order relation on traces, with the goal to show that
any causal-order preserving permutation of a trace is a valid trace. In
addition to the material presented in the main body of the paper (Section
6.1), this section presents the definitions in more detail.

See 6.1

######  Definition B.4 (Trace Application (Extended Definition)).

A trace $Z$ of length $n$ applied to a configuration $c$ results in a sequence
of configurations $C$ of length $n+1$, $Z(c)=C$, if $\forall i<n$:

$\begin{array}[]{r@{~}l@{~}l@{~}c@{~}r@{\,}l}\leavevmode\nobreak\ &(\exists
p,N_{p},X.\nobreak\leavevmode\hfil\leavevmode\nobreak\
&Z_{i}=\langle{\textsc{I-Event}},p,N_{p},X\rangle\hfil\leavevmode\nobreak\
&\land\hfil\leavevmode\nobreak\
&\\{{\textsc{I-Event}},{\textsc{S-Step}}\\}&\vdash
C_{i}\xRightarrow[p]{N_{p},X}C_{i+1})\\\ \lor\leavevmode\nobreak\ &(\exists
p,N_{p},X.\nobreak\leavevmode\hfil\leavevmode\nobreak\
&Z_{i}=\langle{\textsc{I-Border}},p,N_{p},X\rangle\hfil\leavevmode\nobreak\
&\land\hfil\leavevmode\nobreak\
&\\{{\textsc{I-Border}},{\textsc{S-Step}}\\}&\vdash
C_{i}\xRightarrow[p]{N_{p},X}C_{i+1})\\\ \lor\leavevmode\nobreak\ &(\exists
p.\nobreak\leavevmode\hfil\leavevmode\nobreak\
&Z_{i}=\langle{\textsc{F-Fail}},p\rangle\hfil\leavevmode\nobreak\
&\land\hfil\leavevmode\nobreak\
&\\{{\textsc{F-Fail}},{\textsc{S-AbsX}},{\textsc{S-Step}}\\}&\vdash
C_{i}\xRightarrow[p]{\phantom{N_{p},X}}C_{i+1})\\\ \lor\leavevmode\nobreak\
&(\hfil\leavevmode\nobreak\
&Z_{i}=\langle{\textsc{F-Recover}}\rangle\hfil\leavevmode\nobreak\
&\land\hfil\leavevmode\nobreak\ &\\{{\textsc{F-Recover}}\\}&\vdash
C_{i}\xRightarrow{\phantom{N_{p},X}}C_{i+1})\end{array}$

See 6.3

Note, that by definition of execution and trace application, any sequence of
configurations produced by a trace application is an execution.

It is easy to show that any prefix of a valid trace is also a valid trace.
Still, this is a useful property, so we state it as a lemma.

######  Lemma B.5 (Validity of Prefix).

All prefixes of a valid trace from $c$ are valid traces from $c$.

######  Proof B.6.

This property follows directly from the definition of a valid trace. Given a
valid trace $Z$ from $c$, there exists an execution $C$ starting from $c$ such
that $Z(c)=C$, then we can simply construct an execution $C^{\prime}$ and
trace $Z^{\prime}$ as prefixes from $C$ and $Z^{\prime}$ respectively, such
that $Z^{\prime}(c)=C^{\prime}$.

Using the notion of traces, we can define a causal order relation on trace
steps similar to the happens-before relation [34].

######  Definition B.7 (Causal Order (Extended Definition)).

A step $Z_{i}$ happens before $Z_{j}$ with $i<j$ if one of the four cases
apply:

$Z_{i}={\textsc{F-Recover}}\lor Z_{j}={\textsc{F-Recover}}$ then $Z_{i}$
happens before $Z_{j}$, by total order on the recovery steps.

if they are not recovery steps, _i.e.,_ for some $p$ and $p^{\prime}$,
$N_{p},N_{p}^{\prime},X,X^{\prime}$:

$Z_{i}=\langle{\textsc{I-Event}},p,N_{p},X\rangle\lor
Z_{i}=\langle{\textsc{I-Border}},p,N_{p},X\rangle\lor
Z_{i}=\langle{\textsc{F-Fail}},p\rangle,\text{\leavevmode\nobreak\ and}$
$Z_{j}=\langle{\textsc{I-Event}},p^{\prime},N_{p}^{\prime},X^{\prime}\rangle\lor
Z_{j}=\langle{\textsc{I-Border}},p^{\prime},N_{p}^{\prime},X^{\prime}\rangle\lor
Z_{j}=\langle{\textsc{F-Fail}},p^{\prime}\rangle$

and $p=p^{\prime}$ then $Z_{i}$ happens before $Z_{j}$, by intraprocessor
order.

if they are action-producing steps, _i.e.,_ for some $p$ and $p^{\prime}$,
$N_{p}$ and $N_{p}^{\prime}$, $X$ and $X^{\prime}$:

$Z_{i}=\langle{\textsc{I-Event}},p,N_{p},X\rangle\lor
Z_{i}=\langle{\textsc{I-Border}},p,N_{p},X\rangle,\text{\leavevmode\nobreak\
and}$
$Z_{j}=\langle{\textsc{I-Event}},p^{\prime},N_{p}^{\prime},X^{\prime}\rangle\lor
Z_{j}=\langle{\textsc{I-Border}},p^{\prime},N_{p}^{\prime},X^{\prime}\rangle$

and there is a message $m$ produced by $Z_{i}$, that is

$\exists M,M^{\prime\prime},N_{p}^{\prime\prime}.\leavevmode\nobreak\
X(N_{p},M)=(N_{p}^{\prime\prime},M^{\prime\prime})\land
m\in(M^{\prime\prime}\setminus M^{\prime})$

which is consumed by $Z_{j}$, that is

$\forall M^{\prime}.\leavevmode\nobreak\ m\notin
M^{\prime}\implies(X^{\prime}(N_{p}^{\prime},M^{\prime})\leavevmode\nobreak\
\text{is undefined})$

then $Z_{i}$ happens before $Z_{j}$, by interprocessor order.

if there exists a step $Z_{k}$ such that $Z_{i}$ happens before $Z_{k}$ and
$Z_{k}$ happens before $Z_{j}$, then $Z_{i}$ happens before $Z_{j}$, by
transitivity.

Reorderings of traces are captured as permutations. We will want to show that
permutations that preserve the causal order relation are valid in the sense
that they produce valid traces.

######  Definition B.8 (Trace Permutation).

A trace $Z^{\prime}$ of length $n$ is a permutation of another trace $Z$ of
length $n$ if there is a bijection $f$ from $\mathrm{dom}(Z)$ to itself such
that $\forall i\in\mathrm{dom}(Z).\leavevmode\nobreak\
Z_{i}=Z^{\prime}_{f(i)}$.

######  Definition B.9 (Trace Permutation Preserving a Relation).

A trace $Z^{\prime}$ of length $n$ is a permutation of another trace $Z$ of
length $n$ preserving relation $R$ if, for a bijection $f$ defining the
permutation, $\forall i,j.\leavevmode\nobreak\ R(Z_{i},Z_{j})\implies
R(Z_{f(i)},Z_{f(j)})$.

Finally, we state a lemma about the validity and similarity of permutations
preserving causal order. Intuitively, it follows from the fact that causally
unrelated steps should not influence each other.

See 6.5

######  Proof B.10.

The proof is done by first (1) proving the validity; and then (2) proving the
similarity of causality-preserving permutations.

Validity. Given a trace $Z$ valid from $c$, and any causality-preserving
permutation $Z^{\prime}$ thereof such that $Z_{i}=Z^{\prime}_{f(i)}$, to show
is that: $Z^{\prime}$ is valid from $c$. We show this by induction over the
length of prefixes of $Z^{\prime}$.

  1. 1.

Induction base: $\bigl{[}Z^{\prime}_{i}\bigr{]}_{i}^{0}$ is valid from $c$.

    1. (a)

$\bigl{[}Z^{\prime}_{i}\bigr{]}_{i}^{0}=\varepsilon=\bigl{[}Z_{i}\bigr{]}_{i}^{0}$
which is a prefix of $Z$, and, by Lemma B.5, is therefore valid from $c$.

  2. 2.

Induction step: assuming $\bigl{[}Z^{\prime}_{i}\bigr{]}_{i}^{j}$ is valid
from $c$, to show is that $\bigl{[}Z^{\prime}_{i}\bigr{]}_{i}^{j+1}$ is valid
from $c$.

    1. (a)

By assumption, $\bigl{[}Z^{\prime}_{i}\bigr{]}_{i}^{j}$ is a valid trace from
$c$, thereby there exists an execution $C^{\prime}$ such that
$\bigl{[}Z^{\prime}_{i}\bigr{]}_{i}^{j}(c)=C^{\prime}$.

    2. (b)

Let’s proceed by case-analysis on the $(j+1)$’th step $Z^{\prime}_{j}$. It
suffices to show that $Z^{\prime}_{j}$ can be applied to configuration
$C^{\prime}_{j}$.

      1. i.

case $Z^{\prime}_{j}=\langle{\textsc{I-Event}},p,N_{p},X\rangle$

        1. A.

By assumption, $Z^{\prime}$ is a causality-preserving permutation of $Z$. By
rule (3) of the causal order relation for step $Z^{\prime}_{j}$, any of the
consumed messages in $X$ have been produced by previous steps and are thus
available for consumption in $C_{j}$. By rule (2) of the causal order
relation, all steps $Z_{k}$ with $k<f(j)$ on the same processor $p$ as
$Z^{\prime}_{j}$, appear once in the prefix of $Z^{\prime}$ before
$Z^{\prime}_{k}$. That is, the intraprocessor order has been preserved. For
this reason, the state $\Sigma_{p}$ of $p$ in configuration $C^{\prime}_{j}$
is the same as the state of $\Sigma_{p}$ in $C_{f(j)}$ (for some $C$ with
$Z(c)=C$). For these reasons, the step $Z^{\prime}_{j}$ can be applied to
configuration $C^{\prime}_{j}$ for actions $X$ on processor $p$, as the
consumed messages are available in $C^{\prime}_{j}$.

      2. ii.

case $Z^{\prime}_{j}=\langle{\textsc{I-Border}},p,X\rangle$, follows
analogously.

      3. iii.

case $Z^{\prime}_{j}=\langle{\textsc{F-Fail}},p\rangle$

        1. A.

The rule F-Fail is always applicable as can be seen by its definition; it does
not depend on the configuration. For this reason the step $Z^{\prime}_{j}$ can
be applied to $C^{\prime}_{j}$.

      4. iv.

case $Z^{\prime}_{j}=\langle{\textsc{F-Recover}}\rangle$

        1. A.

By assumption, $Z^{\prime}$ is a causality-preserving permutation of $Z$. By
rule (1) of the causal order relation for step $Z^{\prime}_{j}$, for all other
steps $Z^{\prime}_{k}$ with $f(k)<f(j)$, we have that $k<j$. As the step was
enabled in the trace $Z$, we know that some fail step
$\langle{\textsc{F-Fail}},p\rangle$ must occur in one of these other steps
before the recovery step. For this reason, the recovery step is enabled and
$Z^{\prime}_{j}$ can be applied to $C^{\prime}_{j}$.

Similarity. It suffices to show that, given any trace $Z$ of length $n$ valid
from $c$, for which the second to last step is not causally ordered with
respect to the last step, swapping these two steps will result in the same
final configuration when applied to $c$. That is, given
$Z=Z_{prefix}:[Z_{n-2}]:[Z_{n-1}]$, we need to show that for
$Z^{\prime}=Z_{prefix}:[Z_{n-1}]:[Z_{n-2}]$ we have that
$Z(c)_{n}=Z^{\prime}(c)_{n}$. In simpler terms, it suffices to show that
$[Z_{n-2}]:[Z_{n-1}](Z_{prefix}(c))=[Z_{n-1}]:[Z_{n-2}](Z_{prefix}(c))$. The
proof is done by case analysis on the last two steps. By assumption, $Z_{n-2}$
and $Z_{n-1}$ are not causally ordered, therefore, by rule (1) neither of them
can be an F-Recover step, by rule (2) the steps cannot be on the same
processor, by rule (3) one of the steps may not be consuming messages produced
by the other step, or by rule (4) there are no transitive causal dependencies
between the steps. This leaves the following two cases. (Case 1) If one of
them is an F-Fail step, then reordering the two steps will not affect the
final configuration. This is the case because the steps are on different
processors, therefore the steps will not be influenced by the local state
effect of either step, further, the F-Fail step does not consume or produce
any messages, therefore it cannot influence the other step. For this reason,
the application of these two steps will produce the same final configuration.
(Case 2) If the steps are either a I-Event or I-Border step on different
processors. As the steps are on different processors, they do not influence
each other in terms of the local processor state. However, a step on one
processor may produce a message which is consumed later by another processor.
Fortunately, this case is ruled out by rules (3) and (4). For this reason,
either step will be enabled regardless of their order, and consume and produce
the same messages. Thus, resulting in the same final configuration.

###  B.3 Properties of the Implementation Model

This section presents some lemmas about the implementation model which are
later used in the proof of failure transparency.

Many of the lemmas center around border steps, in particular, the committing
border step, and the non-committing border step. The committing border step is
the last border step for a given epoch, it occurs when all processors have
executed the border step for the epoch. Formally, we capture this step as:
$(\\{{\textsc{S-Step}},{\textsc{I-Border}}\\}\vdash c\Rightarrow
c^{\prime})\land\mathrm{gce}(c)\neq\mathrm{gce}(c^{\prime})$, that is, it is a
border step in which the greatest common epoch number is increased. A non-
committing border step, on the other hand, does not change the greatest common
epoch number.

######  Lemma B.11.

All execution steps derivable in $I$, except for the committing border step,
do not affect the observed output.

######  Proof B.12.

The proof is done by case analysis of the rules in $\mathrm{I}$ given the
configurations $c=\langle\,\Pi,\,\Sigma,\,N,\,M,\,M_{0}\,\rangle$ and
$c^{\prime}=\langle\,\Pi^{\prime},\,\Sigma^{\prime},\,N^{\prime},\,M^{\prime},\,M_{0}^{\prime}\,\rangle$.

To show is that:
$(\\{{\textsc{S-Step}},{\textsc{I-Event}},{\textsc{F-Fail}},{\textsc{F-Recover}}\\}\vdash
c\Rightarrow c^{\prime})\implies\mathrm{out}(c)=\mathrm{out}(c^{\prime})$ and
$(\\{{\textsc{S-Step}},{\textsc{I-Border}}\\}\vdash c\Rightarrow
c^{\prime})\land\mathrm{gce}(c)=\mathrm{gce}(c^{\prime})\implies\mathrm{out}(c)=\mathrm{out}(c^{\prime})$.

Failure Step. The F-Fail rule does not introduce any change of output, since
it does not change the epoch number nor the messages, and the output cannot be
changed without changing the epoch number or the messages. Our goal is to show
that:

$(\\{{\textsc{S-Step}},{\textsc{F-Fail}}\\}\vdash c\Rightarrow
c^{\prime})\implies\mathrm{out}(c)=\mathrm{out}(c^{\prime})$

First, let’s show that:

$(\\{{\textsc{S-Step}},{\textsc{F-Fail}}\\}\vdash c\Rightarrow
c^{\prime})\implies\mathrm{gce}(c)=\mathrm{gce}(c^{\prime})\land M=M^{\prime}$

Since the only local step is F-Fail, the only possible execution step is:

$\infer*{\Pi_{p}=\texttt{TK}\langle\,f,S,o\,\rangle\\\
\Sigma_{p}=\langle\,a,\,\sigma_{\mathrm{V}}\,\rangle\\\ \\\ X=\varepsilon\\\
\Sigma_{p}^{\prime}=\langle\,a,\,\texttt{fl}\,\rangle\\\
(N^{\prime}_{p},\,M^{\prime})=X(N_{p},\,M)}{\langle\,\Pi,\,\Sigma,\,N,\,M,\,D\,\rangle\Rightarrow\langle\,\Pi,\,\Sigma\bigl{[}p\mapsto\Sigma_{p}^{\prime}\bigr{]},\,N\bigl{[}p\mapsto
N^{\prime}_{p}\bigr{]},\,M^{\prime},\,D\,\rangle}$

By the definition of action application, $\varepsilon(N_{p},\,M)=(N_{p},\,M)$,
therefore $M=M^{\prime}$.
$\Sigma^{\prime}=\Sigma\bigl{[}p\mapsto\langle\,a,\,\texttt{fl}\,\rangle\bigr{]}$
where $\Sigma_{p}=\langle\,a,\,\sigma_{\mathrm{V}}\,\rangle$. From this
follows that:

$\forall
q,a,a^{\prime},\sigma_{\mathrm{V}},\sigma_{\mathrm{V}}^{\prime}.\leavevmode\nobreak\
\Sigma_{p}=\langle\,a,\,\sigma_{\mathrm{V}}\,\rangle\land\Sigma_{p}^{\prime}=\langle\,a^{\prime},\,\sigma_{\mathrm{V}}^{\prime}\,\rangle\implies
a=a^{\prime}$

Further, by expanding the definitions, we can show that the $\mathrm{gce}$ is
not changed:

$\displaystyle\mathrm{gce}(c)$
$\displaystyle=\mathrm{min}\bigl{\\{}\mathrm{max}(\mathrm{dom}(a))\ \big{|}\
\Sigma_{p}=\langle\,a,\,\sigma_{\mathrm{V}}\,\rangle\bigr{\\}}$
$\displaystyle=\mathrm{min}\bigl{\\{}\mathrm{max}(\mathrm{dom}(a))\ \big{|}\
\Sigma_{p}^{\prime}=\langle\,a,\,\sigma_{\mathrm{V}}\,\rangle\bigr{\\}}$
$\displaystyle=\mathrm{gce}(c^{\prime})$

From which follows our intended result:

$(\\{{\textsc{S-Step}},{\textsc{F-Fail}}\\}\vdash c\Rightarrow
c^{\prime})\implies\mathrm{gce}(c)=\mathrm{gce}(c^{\prime})\land M=M^{\prime}$

Next, it suffices to show that the observable output is not changed given that
the $\mathrm{gce}$ and the messages are not changed:

$\mathrm{gce}(c)=\mathrm{gce}(c^{\prime})\land
M=M^{\prime}\implies\mathrm{out}(c)=\mathrm{out}(c^{\prime})$

The conclusion follows directly from the premises and the definition of
$\mathrm{out}$:

$\displaystyle\mathrm{out}(c)=\bigl{\\{}n\,s\,\langle\,e,\,d\,\rangle\
\big{|}\ (n\,s\,\langle\,e,\,d\,\rangle)\in M\land
e\leq\mathrm{gce}(c)\bigr{\\}}$ $\displaystyle=$
$\displaystyle\bigl{\\{}n\,s\,\langle\,e,\,d\,\rangle\ \big{|}\
(n\,s\,\langle\,e,\,d\,\rangle)\in M^{\prime}\land
e\leq\mathrm{gce}(c^{\prime})\bigr{\\}}$
$\displaystyle=\mathrm{out}(c^{\prime})$

Event Step. The I-Event rule does not affect the greatest common epoch number
(gce), nor does it produce any messages with an epoch number lower than the
gce. For this reason, by the definition of $\mathrm{out}$, the output is not
changed.

Non-Committing Border Step. A non-committing (local) border step, _i.e.,_ an
execution step for which $(\\{{\textsc{S-Step}},{\textsc{I-Border}}\\}\vdash
c\Rightarrow c^{\prime})\land\mathrm{gce}(c)=\mathrm{gce}(c^{\prime})$, does
not affect the observable output. By assumption, the $\mathrm{gce}$ is not
changed. Further, no new messages with $e\leq\mathrm{gce}(c)$ can be produced,
since all processors have epoch number $e>\mathrm{gce}(c)$ by definition of
$\mathrm{gce}$, therefore these messages are not included in $\mathrm{out}$.

Recovery Step. The recovery rule does not change the observed output. Here we
should reason about the latest common snapshot ($\mathrm{lcs}$), in
particular, that it preserves the output messages. Our goal is to show that:

$(\\{{\textsc{F-Recover}}\\}\vdash c\Rightarrow
c^{\prime})\implies\mathrm{out}(c)=\mathrm{out}(c^{\prime})$

By applying the recovery rule, we get that:

$c^{\prime}=\mathrm{lcs}(c)$

By the definition of $\mathrm{lcs}$, it the $\mathrm{gce}$ is not changed,
_i.e.,_ $\mathrm{gce}(c^{\prime})=\mathrm{gce}(lcs(c))=\mathrm{gce}(c)$, since
$\forall\langle
a^{\prime},\sigma_{\mathrm{V}}^{\prime}\rangle\in\Sigma^{\prime}.\leavevmode\nobreak\
\mathrm{dom}(a^{\prime})=\bigl{\\{}\mathrm{gce}(c)\bigr{\\}}$. Further,
$M^{\prime}=M_{0}\cup out(c)$, leaving the events with epoch number
$e\leq\mathrm{gce}(c)$ unchanged. Therefore, the observed output is not
changed, _i.e.,_ $\mathrm{out}(c)=\mathrm{out}(c^{\prime})$.

######  Lemma B.13.

If a trace $Z$ consists of a sequence of S-Steps (_i.e.,_ excluding F-Recover
steps) valid from a configuration $c$, then a trace step $Z_{i}$ with epoch
number $e$ cannot happen before a trace step $Z_{j}$ with epoch number
$e^{\prime}$ for which $e^{\prime}<e$.

######  Proof B.14.

By the definition of local steps in $I$, the epoch number of a processor can
only grow. In particular, for event steps and failure steps it stays the same,
and for border steps it is incremented. Therefore, if the steps are on the
same processor, by case (2) of Definition B.7, for epoch numbers $e^{\prime}$
and $e$ such that $e^{\prime}<e$, any $e^{\prime}$ step happens before all $e$
steps on the same processor. Further, if the steps are on different
processors, by (3, 4) of Definition B.7, if $e^{\prime}<e$ then $Z_{i}$ cannot
happen before $Z_{j}$, as: (a) any messages emitted by $Z_{i}$ cannot be
received by $Z_{j}$ as $e^{\prime}\neq e$; and (b) nor can there exist a
transitive causal dependency, as neither of the rules (2, 3) allow a direct
dependency such that a higher epoch-numbered step happens before a lower
epoch-numbered step.

######  Lemma B.15.

If a trace $Z$ is valid from a configuration $c$, and $Z^{\prime}$ is a
causality-preserving permutation of $Z$, such that the permutation preserves
the total order of all trace steps with an epoch number less than $e$, then
the observable outputs obtained by the committing border steps of all epochs
below $e$ are equal for $Z$ and $Z^{\prime}$.

######  Proof B.16.

Consider one of the committing border steps for epoch $e^{\prime}$ with
$e^{\prime}<e$. We can reorder the trace by moving all trace steps for epochs
larger than $e^{\prime}$ that occur before the committing border step directly
after the committing border step. By Lemma B.13, this is a causality-
preserving permutation, as none of the moved trace steps can happen before the
committing border step nor any other step for epochs less than or equal to
$e^{\prime}$. By Lemma 6.5, we know that the configuration obtained (i) after
the committing border step before the reordering; and (ii) after the last
moved step after the reordering, are the same. Furthermore, by Lemma B.11 we
know that output function is not affected by non-committing (non-global)
border steps. As none of the moved steps can be global committing border
steps, we know that the output function’s result must be the same (after the
reordering) for the committing border step and the last moved step. And
therefore we know that the output function at the committing border step for
$e^{\prime}$ must be the same after the reordering as before the reordering.
This procedure can be repeated for every committing border step up the
$e^{\prime}$, and therefore each committing border step will have the same
observable output before as after the reordering.

######  Lemma B.17.

The latest common snapshot is only changed by committing border steps.

######  Proof B.18.

By definition of the latest common snapshot ($\mathrm{lcs}$), it is only
affected by changes to $N$ and $\Sigma$ in $c$, as well as by
$\mathrm{out}(c)$. With respect to the sequence numbers $N$, the computed
$\mathrm{lcs}$ solely depends on the domain of $N$, which remains the same for
all steps as it is a map from processors to sequence numbers. With respect to
the states $\Sigma$, the computed $\mathrm{lcs}$ solely depends on the
archives $a$ of the states for epochs less than the $\mathrm{gce}$. The
archives of epochs less than $\mathrm{gce}$ are never changed, as no processor
can have an epoch number less than $\mathrm{gce}$. Further, as was shown in
the proof of Lemma B.11, the only steps changing the greatest common epoch are
the committing border steps. Therefore, changes to $\Sigma$ do not affect the
latest common snapshot. Lastly, $\mathrm{out}(c)$ is only changed by the
committing border steps (Lemma B.11). Therefore, the latest common snapshot is
only changed by the committing border steps.

######  Lemma B.19.

If a trace $Z$ of S-Steps is valid from a configuration $c$, such that the
last trace step is a committing border step with epoch number $e$, and epoch
numbers of all trace steps are less than or equal to $e$, then the last
configuration of the execution $\bigl{[}C\bigr{]}_{i}^{n}=Z(c)$ is equal to
its latest common snapshot, _i.e.,_ $C_{n-1}=\mathrm{lcs}(C_{n-1})$.

######  Proof B.20.

By inspection of the definition of $\mathrm{lcs}$, it suffices to show that
the state ($\Sigma$), the sequence numbers ($N$), and the messages ($M$) of
the last configuration $C_{n-1}$ are the same as obtained by the latest common
snapshot. ($\Sigma$) The last trace step for each processor in $Z$ must have
been a border step for epoch $e$. This border step saves the current state to
the archive for $e$, and increments the epoch number on the processor to
$e+1$. As can be seen by the definition of $\mathrm{lcs}$, the $\mathrm{lcs}$
computes the same archive and same local state, as we know that
$e=\mathrm{gce}(C_{n-1})$. ($N$) The sequence numbers for each processor are
incremented by one for every consumed or produced message. As can be seen in
the definition of $\mathrm{lcs}$, the computed sequence numbers correspond to
the number of output messages on each stream. As a stream has at most one
producer, the computed sequence number corresponds to the number of produced
messages. For consumed messages, we know that all messages of epochs smaller
than the $\mathrm{gce}$ must have been consumed, therefore the computed
sequence number is also equal. ($M$) The $\mathrm{lcs}$ computes the new set
of messages from the observed output messages $\mathrm{out}$. As all produced
messages in $Z$ have epoch numbers less than or equal to $e$, all produced
messages are included in the observed output $\mathrm{out}(C_{n-1})$.
Therefore, the computed messages are the same as the messages in the
configuration $C_{n-1}$.

######  Lemma B.21.

If a trace $Z$ of S-Steps is valid from $c$ with $Z(c)=C$, such that the first
$n$ trace steps have epoch numbers less than or equal to
$\mathrm{gce(C_{\left|C\right|-1})}$, and all later trace steps have epoch
numbers greater than $\mathrm{gce(C_{\left|C\right|-1})}$, then
$\mathrm{lcs}(C_{n})=\mathrm{lcs}(C_{\left|C\right|-1})$.

######  Proof B.22.

The proof is done by induction on the length of the prefix of $Z$ starting
from index $n$.

Induction base: the length the prefix $[Z_{i}]^{n}_{i}$ is $n$. In this case,
for the sequence of configurations $C^{\prime}=[Z_{i}]^{n}_{i}(c)$, we have
that $n=\left|C^{\prime}\right|-1$ and thus
$C^{\prime}_{n}=C^{\prime}_{\left|C^{\prime}\right|-1}$, and therefore
$\mathrm{lcs}(C^{\prime}_{n})=\mathrm{C^{\prime}_{\left|C^{\prime}\right|-1}}$.

Induction step: for some prefix $Z^{\prime}=[Z_{i}]^{n^{\prime}}_{i}$ of size
$n^{\prime}>n$ for which $C^{\prime}=Z^{\prime}(c)$, we have to show that
$\mathrm{lcs}(C^{\prime}_{n})=\mathrm{lcs}(C^{\prime}_{\left|C^{\prime}\right|-1})$,
under the assumption that
$\mathrm{lcs}(C^{\prime}_{n})=\mathrm{lcs}(C^{\prime}_{\left|C^{\prime}\right|-2})$.
By its definition, the latest common snapshot is only affected by all trace
steps except for non-committing border steps with an epoch number less than or
equal to the greatest common epoch number. As the new step has an epoch number
greater than the greatest common epoch number, and it is known to not be a
committing border step (as otherwise the $\mathrm{gce}$ would be increased),
it does not affect the latest common snapshot, thus
$\mathrm{lcs}(C^{\prime}_{\left|C^{\prime}\right|-1})=\mathrm{lcs}(C^{\prime}_{\left|C^{\prime}\right|-2})$.
For this reason, following the induction hypothesis,
$\mathrm{lcs}(C^{\prime}_{n})=\mathrm{lcs}(C^{\prime}_{\left|C^{\prime}\right|-2})=\mathrm{lcs}(C^{\prime}_{\left|C^{\prime}\right|-1})$.

######  Definition B.23 (Fair Execution).

An execution $C$ is fair if it is maximal (_i.e.,_ it is not a prefix of
another execution), has a finite amount of failures, and eventually executes
any step which is eventually always enabled. That is, $\mathrm{fair}(C)$ iff:

$\displaystyle(\nexists C^{\prime}.\leavevmode\nobreak\
(C:C^{\prime})\in\mathbb{E}_{C_{0}}^{\mathrm{I}})\leavevmode\nobreak\ \land$
$\displaystyle(\exists C^{\prime},C^{\prime\prime}.\leavevmode\nobreak\
C=(C^{\prime}:C^{\prime\prime})\land\left|C^{\prime}\right|\in\mathbb{N}\land\forall\langle\Pi^{\prime\prime},\Sigma^{\prime\prime},M^{\prime\prime},N^{\prime\prime},D^{\prime\prime}\rangle\in
C^{\prime\prime}.\leavevmode\nobreak\ \nexists\langle
a,\mathtt{fl}\rangle\in\Sigma^{\prime\prime})\leavevmode\nobreak\ \land$
$\displaystyle(\forall C^{\prime},C^{\prime\prime}.\leavevmode\nobreak\
C=(C^{\prime}:C^{\prime\prime})\land\left|C^{\prime\prime}\right|=\infty\implies\nexists
z.\leavevmode\nobreak\ (\forall c^{\prime\prime}\in
C^{\prime\prime}.\leavevmode\nobreak\ z(c^{\prime\prime}))\land\nexists
i.\leavevmode\nobreak\ z(C^{\prime\prime}_{i})=C^{\prime\prime}_{i+1})$

Proving liveness typically involves fairness assumptions. Specifically, for
our proof of liveness in Theorem 6.12, we assume that executions are maximal,
_i.e.,_ we exclude executions which are prefixes of other executions. This is
necessary as our definition of the set of executions is prefix-closed, that
is, even the execution consisting solely of the initial state is included in
it. It would be difficult to reason about the liveness of an execution which
takes no execution steps. Instead, all executions are restricted to either be
terminated or infinite. Further, we assume that the execution has at most a
finite amount of failures. Formally, this means that any fair execution must
be decomposable into a finite prefix and a suffix for which the suffix
contains no failures. If this was not the case, then we may have a situation
in which the execution always fails and aborts an epoch before it has
completed. Lastly, a fair execution must eventually execute any step which is
eventually always enabled. Formally, we describe this by negation: a step
cannot eventually always be enabled but not eventually taken. We use this last
property to ensure that execution steps which are enabled to eventually be
taken. If we would not make such an assumption, it would be possible for the
execution to always execute one of the processors, but never the others, thus
making it difficult to argue about the liveness. However, with the assumption,
we know that, once a step is enabled, and if it remains enabled, then
eventually it will be taken. Using this, we can then show through a chain of
eventual steps that the system eventually produces an output.

See 6.12

######  Proof B.24.

Given an arbitrary initial configuration $k$ and some epoch $e$ which is
present in the initial configuration, to show is that eventually the epoch $e$
appears in the output of a fair execution. To show this, we proceed by the
following definitions and statements.

(Def0) A configuration is well-formed if the messages on the streams have
contiguous sequence numbers and are divided into epochs, and the processors
have sequence numbers which correspond with the number of consumed/produced
messages.

(Def1) A configuration is failed if there is a processor in a failed state.

(Def2) An epoch is produced if there is a message for that epoch visible in
the output as defined by the output function $\mathrm{out}$.

(S0) Any valid initial configuration is well-formed, _i.e.,_ it maintains
Def0. Proof. This follows from the definition of valid initial configuration.

(S1) Any execution step of $\mathrm{I}$ applied to a well-formed configuration
results in a well-formed configuration. Proof. This follows from inspection on
the rules when applied to an arbitrary well-formed configuration.

(S2) Any execution of $\mathrm{I}$ starting from a well-formed configuration
contains only well-formed configurations. Proof. This follows directly from S0
and S1.

(S3) If an execution step is enabled in $\mathrm{I}$, then it will remain
enabled at least until a recovery step is taken. Proof. This follows from
inspection on the rules in $\mathrm{I}$.

(S4) It is not possible that there _always_ _eventually_ is a failure. Proof.
This follows from the fair execution assumption which states that there is a
“finite amount of failures”. In other words, failures do not occur infinitely
often, which implies that failures do not always eventually occur.

(S5) Starting from any arbitrary configuration $c$ from an execution starting
from $k$, for which $c$ is not failed and the epoch $e$ is not yet produced.
If there are no failures in the execution continuing from $c$, then eventually
the epoch $e$ is produced.

Proof. We proceed by induction on the structure of the processing graph as
defined by $\Pi$. To show is that: (IH) for each stream in the processing
graph, eventually a border event for the epoch $e$ is produced. That is,
eventually there is some configuration for which the border events for $e$
exist on all streams, and snapshots for $e$ exist on all processors. Note that
IH implies S5, as by definition of the output function, the epoch is produced
once there is a configuration for which all processors have a snapshot of the
epoch.

Base case. The base case consists of the empty processing graph with no
processors, but with the set of input streams to the graph. IH follows from
the well-formedness of the initial configuration on the input streams.

Induction step. By the induction hypothesis, we have that IH holds for some
processing graph $\Pi^{\prime}$ which is a subgraph of $\Pi$. The induction
step is to show that IH holds for the processing graph $\Pi^{\prime\prime}$,
which adds one of the processors to $\Pi^{\prime}$ for which all inputs to the
processor are either inputs to the graph or are outputs of other processors in
$\Pi^{\prime}$. This way, all possible allowed acyclic graph structures can be
constructed. We know that all inputs to the new processor will eventually
contain the border message for epoch $e$ by IH on $\Pi^{\prime}$. Further, we
know that these streams are well-formed by S2. To show is that the processor
eventually consumes the epoch border message for $e$ on every one of its input
streams, and thus produces a corresponding epoch border message on its output
stream.

By construction of the rules $\mathrm{I}$, we know that the processor
processes one epoch from its inputs until completion, before starting the next
epoch. Further, by well-formedness on the initial configuration, we know that
the epochs are finite in size. From the well-formedness on its inputs, we know
that there exists a sequence of execution steps for the processor such that it
can process all input steps that are available to it. We know that at least
one such step will be enabled until all inputs have been processed. Further,
we know that any enabled step remains enabled until taken (S3). Thus, by the
fairness assumption, we know that such steps will eventually be taken, and
therefore all inputs to the processor will eventually be processed.
Consequently, eventually the border message for epoch $e$ will have been
consumed, and a corresponding border message for epoch $e$ produced.

(S6) It is _always_ the case that: _eventually_ there is a failure; or
_eventually_ the epoch is produced. In other terms, starting from any
configuration in an execution, eventually there is a failure or eventually the
epoch is produced.

Proof. Given an arbitrary configuration $c$ from an execution starting from
$k$. We show that, starting from $c$, eventually there is a failure or
eventually the epoch $e$ is produced. Let us assume that the epoch has not yet
been produced in any configuration leading up to $c$, otherwise we would be
done. Further, let us consider the case in which there is a failed processor
in the configuration $c$. In this case, there is a failure, and thus we are
done. Then, let us consider the case in which there is no failed processor in
the configuration $c$. If the execution continuing from configuration $c$
eventually contains a failure, then we are done. Therefore, the last case to
consider is the execution starting from configuration $c$ contains no failures
and for which $e$ has not yet been produced. This last case is handled by S5.

(S7) Eventually the epoch $e$ appears in the output of a fail execution. More
precisely, starting from any configuration in an execution, eventually the
epoch is produced.

Proof. This follows from S4 and S6 by the following temporal reasoning:
(_always_ ((_eventually_ A) or (_eventually_ B))) and (_not_ (_always_
(_eventually_ A))) implies (_always_(_eventually_ B)). That is, we have shown
that _always_ _eventually_ the epoch is produced.


11institutetext: University of Tartu, Tartu, Estonia
11email<EMAIL_ADDRESS>
# Why am I Waiting? Data-Driven Analysis of Waiting Times in Business
Processes††thanks: Work funded by the European Research Council (PIX Project)

Katsiaryna Lashkevich  0000-0003-4426-7738 Fredrik Milani  0000-0002-1322-915X
David Chapela-Campa  0000-0002-4711-9653 Ihar Suvorau  0000-0002-1862-2604
Marlon Dumas  0000-0002-9247-7476

###### Abstract

Waiting times in a business process often arise when a case transitions from
one activity to another. Accordingly, analyzing the causes of waiting times of
activity transitions can help to identify opportunities for reducing the cycle
time of a process. This paper proposes a process mining approach to decompose
the waiting time observed in each activity transition in a process into
multiple direct causes and to analyze the impact of each identified cause on
the cycle time efficiency of the process. An empirical evaluation shows that
the proposed approach is able to discover different direct causes of waiting
times. The applicability of the proposed approach is demonstrated on a real-
life process.

###### Keywords:

Process mining Waiting time Cycle time efficiency.

##  1 Introduction

Waiting time is a common source of waste in business processes [6]. Although
it is impractical to completely eliminate waiting times in business processes,
there are various approaches to reduce them [11]. Waiting times typically
arise during transitions between activities, i.e., when the execution of a
case moves from one activity to another. There are different reasons why
waiting times occur during activity transitions. For instance, when two
consecutive activities in a case are executed by different resources (a.k.a. a
handoff [23]), the processing of the case is put on hold until the next
resource becomes available to execute it. In this scenario, the cause of the
waiting time is resource contention, i.e. a resource is not available to
execute an activity instance because they are busy executing other activity
instances [7]. Waiting times may also be caused by data exchanges [18],
coordination issues [19], or synchronization points [19].

Process mining techniques allow us to analyze data generated by business
process executions, a.k.a.  _event logs_ , to unveil performance and
conformance issues, and associated improvement opportunities [1]. In
particular, process mining techniques support the discovery of sources of
waste, including waiting times [1]. However, while existing process mining
techniques enable analysts to visualize activity transitions with high waiting
time (i.e., bottlenecks), they provide limited support for identifying the
causes of waiting times and how to reduce them.

To tackle this gap, this paper addresses the following research questions
(RQ): (1) “What causes of waiting times between pairs of activity instances
can be identified from event logs?”, (2) “How can these causes of waiting time
be identified from event logs?”, and (3) “How can improvement opportunities,
expressed as inefficiencies due to waiting times, be identified from event
logs?”

The contribution of the paper is two-fold. First, we conceptualize the causes
of waiting time arising from activity transitions. Second, we propose a
process mining approach to (1) discover waiting times associated with activity
transitions; (2) identify their causes; and (3) analyze their impact w.r.t. a
well known measure of temporal efficiency called Cycle Time Efficiency (CTE):
the ratio of processing time to cycle time in a process [7].

The proposed approach has been implemented as a software tool and empirically
evaluated to verify its ability to discover different causes of waiting time
using synthetic event logs. In addition, the applicability of the approach has
been tested by applying it to a real-life event log.

The rest of the paper is structured as follows. Section 2 introduces
background and related work. Section 3 presents the proposed approach. Section
4 describes the empirical evaluation, and Section 5 concludes the paper.

##  2 Background and Related Work

In this section, we introduce relevant conceptual foundations and notations
from the fields of business process management and process mining, and
position our contribution w.r.t. existing approaches to discover and analyze
waiting times.

###  2.1 Business Processes and Temporal Performance Measures

A business process is a collection of events, activities, and decisions that
lead from a customer need to an outcome that is of value to this customer [7].
Each execution of a business process is called a _case_. A common measure of
temporal performance of a business process is its _cycle time_ : The time
between the moment a case of the process starts, and the case ends, aggregated
to the level of the set of cases of a process observed during a period of
time. The cycle time of a process consists of _processing time_ (i.e., the
time during which a case is being processed) and _waiting time_ (i.e., the
time when a case waits to be processed) [7].

Waiting time may be caused by resource contention, i.e., no suitable resource
is available to execute an activity instance [11]. Other causes of waiting
time include: synchronization between resources within a process [19] or
across multiple processes [7], coordination between resources executing
different activities [19], data transfer [7], batching [12], handoffs [19],
and external inputs [2].

As stated earlier, the temporal efficiency of a process can be measured by its
CTE: the ratio of processing time to cycle time. When CTE is close to 1, there
is relatively little waiting time. Conversely, if the CTE is close to 0, the
waiting times are longer relative to processing times and there are
opportunities to improve the CTE by reducing waiting times [7].

###  2.2 Event Logs and Activity Instance Logs

Modern IT systems record and store process execution data in _event logs_ ,
i.e., sets of timestamped events capturing the execution of the activities in
a process [7]. An event log contains information about state changes of each
activity instance (e.g. enablement, start, end, or cancellations of activity
instances). In this paper, we use the concept of _activity instance log_ to
represent the execution of a set of cases in a process. An activity instance
log is an event log in which each entry contains information about the start
time and end time of an activity instance [16]. Below, we introduce several
notations used in the paper, leading to a definition of an activity instance
log.

We consider a business process that involves a set of _activities_ $A$. We
denote each of these activities with $\alpha$. An _activity instance_
$\varepsilon=(\varphi,\alpha,\tau_{e},\tau_{s},\tau_{c},\rho)$ denotes one
execution of activity $\alpha$, where $\varphi$ identifies the case
(represented by a _process trace_) to which this execution belongs to,
$\tau_{e}$, $\tau_{s}$, and $\tau_{c}$ denote, respectively, the instants in
time in which this activity instance was _enabled_ , _started_ , and
_completed_ , and $\rho$ identifies the _resource_ that processed the
activity. Accordingly, we use $\varphi(\varepsilon_{i})$,
$\alpha(\varepsilon_{i})$, $\tau_{e}(\varepsilon_{i})$,
$\tau_{s}(\varepsilon_{i})$, $\tau_{c}(\varepsilon_{i})$ and
$\rho(\varepsilon_{i})$ to denote, respectively, the process trace, the
activity, the enablement time, the start time, the completion time, and the
resource associated with the activity instance $\varepsilon_{i}$. We use
$(\tau_{i},\tau_{j})$ to denote the interval of time starting in $\tau_{i}$
and ending in $\tau_{j}$. In this way,
$\omega(\varepsilon_{i})=(\tau_{e}(\varepsilon_{i}),\tau_{s}(\varepsilon_{i}))$
denotes the waiting time of $\varepsilon_{i}$, representing the interval since
$\varepsilon_{i}$ became available for processing
($\tau_{e}(\varepsilon_{i})$), until its recorded start
($\tau_{s}(\varepsilon_{i})$). Accordingly, the processing time of
$\varepsilon_{i}$ is
$pt(\varepsilon_{i})=(\tau_{s}(\varepsilon_{i}),\tau_{c}(\varepsilon_{i}))$.
We use $(\tau_{i},\tau_{j})\in(\tau_{k},\tau_{l})$ to denote that the interval
$(\tau_{i},\tau_{j})$ is contained in $(\tau_{k},\tau_{l})$, i.e.
$\tau_{i}\geq\tau_{k}$ and $\tau_{j}\leq\tau_{l}$. With
$(\tau_{i},\tau_{j})\perp(\tau_{k},\tau_{l})$ we denote that both intervals
(partially or fully) overlap, i.e.,
$\exists(\tau_{m},\tau_{n})\in(\tau_{i},\tau_{j})\mid(\tau_{m},\tau_{n})\in(\tau_{k},\tau_{l})$.

Given the above, an activity instance log $L$ is a collection of activity
instances recording the data of the execution of a set of traces of a business
process.

###  2.3 Related Work

Process mining is a research field that encompasses a wide range of techniques
that enable process discovery and efficiency, quality, compliance, predictive,
and prescriptive analysis [17]. Some techniques address the question of how to
discover and analyze waiting times in specific application domains. For
instance, Uysal et al. [22] present a case study where process mining is used
to identify bottlenecks and reduce the cycle time in a production process.
Similarly, Erdogan et al. [8] apply process mining techniques to identify
waiting times in a hospital emergency process, while Yampaka & Chongstitvatana
[25] describe an application of process mining combined with a queuing system
to analyze and improve temporal performance in a healthcare process.
Similarly, Antunes et al. [3] combine process mining with discrete event
simulation to optimize waiting time in an emergency department. However, none
of these domain-specific studies considers the question of how to attribute
waiting times to their causes, which is the focus of this paper.

Ferreira & Vasilyev [9] present a technique to identify why some cases in a
process take longer time to complete. They identify case characteristics
correlating with higher delays, e.g., when a given activity occurs in a case,
or when a given resource is involved, the case is likely to have higher
waiting time. Likewise, De Leoni & van der Aalst [5] combine some of the
existing correlation analysis techniques to identify how different process
characteristics correlate with the process performance, e.g., if process
deviations cause delays. Similarly, Hompes et al. [10] propose an approach
based on time series analysis to detect cause-effect relations between process
characteristics and performance indicators, e.g., if the waiting time for the
receipt of a payment depends on the time of day. Toosinezhad et al. [21]
introduce an approach to detect event patterns that frequently precede, i.e.
lead to, dynamic bottlenecks. While these studies take a correlation-based
approach to analyze waiting times, we classify the causes of waiting times and
consider their impact on process performance.

Some process mining techniques support the identification of waiting times
caused by queuing effects, i.e., when activity instances wait in a queue until
a resource becomes available [20]. Similarly, in [12], the authors present an
approach to discover waiting times caused by batch processing. However, these
techniques focus on identifying a singular cause of waiting time. In contrast,
in the present paper we seek to decompose the observed waiting time into
multiple causes.

##  3 Waiting Time Discovery and Analysis

In this section, we describe our approach to discover and analyze waiting
times in a business process. The approach takes an event log as input and, as
a result, produces a report comprising the causes of waiting times in a
business process and their impact on the CTE. Figure 1 depicts an overview of
the three main steps of the proposed approach.

Figure 1: Overview of the proposed approach.

In the first step, we discover the transitions between activities and their
characteristics – total frequency, case frequency, and total waiting time –
from the event log. In the second step, we identify the causes of waiting time
of each transition. In the third and final step, we analyze the impact of each
cause on the temporal efficiency of the process.

###  3.1 Activity Transition Discovery

The first step of our approach is to discover transitions between activities
and their waiting times. To do this, we define an activity transition instance
as a pair of activity instances $\langle a_{1},b_{1}\rangle$ in a single case,
such that the completion of $a_{1}$ enables $b_{1}$, i.e., $b_{1}$ cannot be
executed before $a_{1}$ is completed. In a sequential process, each activity
instance of a case is enabled by the completion of the preceding activity
instance. However, concurrency is common in real-life processes. Figure 2
shows an example of the execution of a sub-process formed by four activities
with concurrency between two of them. In this case, even though the order of
the activity instances is $a_{1}$, $b_{1}$, $c_{1}$, and $d_{1}$, both $b_{1}$
and $c_{1}$ are enabled when the activity instance $a_{1}$ completes. In the
same way, the activity instance $d_{1}$ is enabled only when $c_{1}$ is
completed. Thus, there are only three activity transitions in this example,
namely $\langle a_{1},b_{1}\rangle$, $\langle a_{1},c_{1}\rangle$, and
$\langle c_{1},d_{1}\rangle$.

Figure 2: Waiting time in a case fragment with concurrent activity instances.

To detect the concurrency relations, e.g., when the activities $b$ and $c$ are
concurrent (see Figure 2), we use the concurrency oracle from the Heuristics
Miner [24]. This method computes, for each observed relation between two
activities, a degree of confidence whether it is a concurrent or directly-
follows relation, based on the percentage of occurrences in each order – $b$
followed by $c$, or $c$ followed by $b$. Then, based on a set of defined
thresholds, it retrieves the concurrent relations of the process. In this way,
we consider each activity instance being enabled by its closest non-concurrent
preceding activity instance. We assume that once an activity instance is
enabled, it remains enabled until its processing starts.

We call the first element of an activity transition instance the _source
activity instance_ , while the latter is the _target activity instance_. An
_activity transition_ is a set of activity transition instances with the same
source and target activities, where the _source activity_ is the activity
executed in all its source activity instances, and the _target activity_ is
the activity executed in all its target activity instances. For example, the
activity transition $\langle a,b\rangle$ is composed of the set of activity
transition instances $\\{\langle a_{1},b_{1}\rangle,\langle
a_{2},b_{2}\rangle,...,\langle a_{n},b_{n}\rangle\\}$ in the event log. For
the sake of simplicity, we will refer to activity transitions as _transitions_
, and to activity transition instances as _transition instances_.

Once the transition instances are discovered, we calculate their _duration_ ,
i.e., the waiting times they induce. The waiting time of a target activity
instance in a transition instance is the interval between its enablement and
its start time. For example, in Figure 2, the waiting time in the transition
$\langle c_{1},d_{1}\rangle$ corresponds to the interval
$(t_{enabled\\_d1},t_{start\\_d1})$. In this way, we identify the waiting time
of each target activity instance per transition.

Finally, for each identified transition (composed of all its transition
instances), we compute the following characteristics. _Case frequency_
illustrates the proportion of process cases from total number of cases where
this transition is observed. _Total frequency_ indicates the number of
occurrences of this transition in the process. _Total duration_ is the sum of
the waiting times of all transition instances. The output of this step is a
report depicting all identified transitions and their characteristics, sorted
by total duration in descending order. Based on this information, the analysts
can see what transitions cause the highest waiting times and how frequently
they are executed.

###  3.2 Waiting Time Cause Discovery

Once the activity transitions and their characteristics are discovered, we
analyze the waiting time of each transition instance and identify their
causes. We target five causes of waiting time (WT): WT due to batching,
resource contention, prioritization, resource unavailability, and extraneous
factors. In this section, we define these five causes of waiting times (RQ1)
and describe how they can be identified from an event log (RQ2).

Within a single transition instance, waiting time can be explained by one or
several causes –e.g. the resource was working in another activity half of the
waiting time, and out of their working hours the other half. If there are
several waiting time causes in a transition, we propose to classify them in
non-overlapping time intervals by identifying them in strict order using the
dichotomies’ classification illustrated in Figure 3. Thus, when an interval of
the waiting time is classified as a certain cause, it cannot be classified as
any other.

We first identify if any intervals of the transition duration are caused by
batching. Then we seek intervals of waiting time caused by resource contention
and prioritization, followed by resource unavailability and extraneous factors
(see Figure 3). The order of identification is based on the dominance of a
certain cause over the others, i.e., although several phenomena might be
observed for the same interval, only the cause with the highest dominance is
considered. For instance, if during the same waiting time interval, both
batching and resource unavailability exist, we consider the primary cause for
the instance waiting, i.e., batching in this case. Although the resource might
be unavailable, the processing cannot start until the batch is accumulated.
Therefore, when multiple causes are observed, only one is considered as the
direct cause of waiting time. In addition, this approach ensures the addition
property of the waiting time for each transition instance – i.e. the sum of
the waiting time causes is equal to the total waiting time of the transition
instance.

Figure 3: Overview of the waiting time cause discovery process and their
definitions.

Waiting time due to Batching. The first cause that we identify is _waiting
time due to batching_. Batch processing occurs when a set of instances of the
same activity are accumulated to be processed together (either simultaneously
or one after the other) [12]. In this context, a batch is a set of activity
instances $\mathcal{E}_{b}\subseteq L$, such that all
$\varepsilon_{i}\in\mathcal{E}_{b}$ record the execution of the same activity,
performed by the same resource, and processed as a batch (i.e. all of them
were enabled before any of them started, and they were processed as a group).
We use the technique proposed in [12] to identify batch processing. In batch
processing, when an activity instance is enabled and ready to be processed, it
can wait for other instances of the same activity until the batch is
accumulated, i.e., until all instances that are a part of a batch are
collected.

Accordingly, when the target activity instance of a transition instance is
detected as part of a batch, the waiting time interval from its enablement
time to the batch accumulation time is classified as _waiting time due to
batching_ (see Figure 4). The waiting time due to batching of an activity
instance is then defined as follows:

######  Definition 1 (Waiting Time Due to Batching).

Given an activity instance log $L$, a batch $\mathcal{E}_{b}\subseteq L$, and
an activity instance $\varepsilon_{i}\in\mathcal{E}_{b}$. The WT due to
batching of $\varepsilon_{i}$ is
$\omega_{ba}(\varepsilon_{i})=(\tau_{e}(\varepsilon_{i}),\tau_{bc})\mid\tau_{bc}=max(\\{\tau_{e}(\varepsilon_{j})\mid\varepsilon_{j}\in\mathcal{E}_{b}\\})$,
i.e. the interval of time between the enablement of $\varepsilon_{i}$ and the
last enablement of the activities in the batch.

Following with the example in Figure 4, the activity $B$ is a batch processed
activity where the resource accumulates instances and then processes them one
by one (sequential batch processing) [16]. The batch is accumulated until the
activity instance $b_{3}$ is enabled (case C3 is ready to be processed
($t_{enabled\\_b3}$). Therefore, if we analyze the transition instance
$\langle a_{1},b_{1}\rangle$ of case C1, its WT due to batching corresponds to
the interval of the waiting time between $t_{enabled\\_b1}$ and
$t_{enabled\\_b3}$.

Figure 4: Waiting time due to batching.

Waiting time due to resource contention. There are situations where the
resources that have to process a certain activity are busy processing another
activity instances that were enabled earlier than the waiting one and, thus,
it’s understood that they start processing them before the current one
(following a first-in-first-out order).111 We assume that resources work only
on one activity at a time, i.e., there is no multitasking. Thus, we foresee
that the proposed estimation technique will not be suitable for event logs
with a high proportion of multitask activity instances.  When this situation
occurs, we classify as _waiting time due to resource contention_ those
intervals in which the resource that performed the activity instance was
working in other activity instances enabled before it (see Figure 5).
Therefore, the waiting time due to resource contention of an activity instance
is defined as follows:

######  Definition 2 (Waiting Time Due to Resource Contention).

Given an activity instance log $L$, and an activity instance
$\varepsilon_{i}\in L$. The WT due to resource contention of $\varepsilon_{i}$
is $\Omega_{rc}(\varepsilon_{i})=\\{(\tau_{i},\tau_{j})\mid\
\tau_{i}=max(\tau_{e}(\varepsilon_{i}),\tau_{s}(\varepsilon_{j}))\wedge\tau_{j}=min(\tau_{s}(\varepsilon_{i}),\tau_{c}(\varepsilon_{j}))\wedge\varepsilon_{j}\in
L\wedge\varepsilon_{j}\neq\varepsilon_{i}\wedge\rho(\varepsilon_{j})=\rho(\varepsilon_{i})\wedge\tau_{e}(\varepsilon_{j})\leq\tau_{e}(\varepsilon_{i})\wedge
pt(\varepsilon_{j})\perp\omega(\varepsilon_{i})\\}$, i.e., the set of
intervals of processing time of all $\varepsilon_{j}$ of $L$ (executed by the
same resource as $\varepsilon_{i}$, and enabled before it) overlapping with
the WT of $\varepsilon_{i}$.

Waiting time due to prioritization. However, the resources might not always
follow the FIFO policy. In some situations, the resources might give priority
to certain activity instances over others. We call this behavior
_prioritization_ , meaning that an activity instance is processed out of turn
w.r.t. a FIFO policy, thus causing other activity instances to wait longer.
When this situation occurs, we classify as _waiting time due to
prioritization_ those intervals in which the resource that performed the
activity instance was working in other activity instances enabled after it
(see Figure 5). Therefore, the waiting time due to prioritization of an
activity instance is defined as follows:

######  Definition 3 (Waiting Time Due to Prioritization).

Given an activity instance log $L$, and an activity instance
$\varepsilon_{i}\in L$. The WT due to prioritization of $\varepsilon_{i}$ is
$\Omega_{prior}(\varepsilon_{i})=\\{(\tau_{i},\tau_{j})\mid\
\tau_{i}=\tau_{s}(\varepsilon_{j})\wedge\tau_{j}=min(\tau_{s}(\varepsilon_{i}),\tau_{c}(\varepsilon_{j}))\wedge\varepsilon_{j}\in
L\ \wedge\
\varepsilon_{j}\neq\varepsilon_{i}\wedge\rho(\varepsilon_{j})=\rho(\varepsilon_{i})\
\wedge\ \tau_{e}(\varepsilon_{j})>\tau_{e}(\varepsilon_{i})\ \wedge\
pt(\varepsilon_{j})\perp\omega(\varepsilon_{i})\\}$, i.e., the set of
intervals of processing time of all $\varepsilon_{j}$ of $L$ (executed by the
same resource as $\varepsilon_{i}$, and enabled after it) overlapping with the
WT of $\varepsilon_{i}$.

Figure 5: Waiting time due to resource contention and due to prioritization.

Waiting time due to resource unavailability. The fourth cause of waiting time
that we propose to consider is resource unavailability, which corresponds to
the intervals in time in which the resource is not available to work due to
their working schedules. To identify this waiting time, we need to first
discover the working schedules of the resources. We propose to use the
technique presented in [14] to discover calendars over time granules not fully
described by the input data. This technique analyzes the instants in time when
each resource interacted with the system (i.e. the start and end of each
activity instance) to build a weekly working calendar composed of time
intervals in which there was enough evidence, based on given support and
confidence values, that the resource is working.222Although we use this
resource calendar discovery algorithm, the approach can be applied with other
calendar discovery algorithms or with manually defined calendars. Given the
weekly calendars of each resource, we transform them to absolute time
intervals to compare them with the waiting times observed in the log. Then, we
classify as _waiting time due to resource unavailability_ those intervals
where the resource is not available for working. Therefore, the waiting time
due to resource unavailability of an activity instance is defined as follows:

######  Definition 4 (Waiting Time Due to Resource Unavailability).

Given an activity instance log $L$, an activity instance $\varepsilon_{i}\in
L$, and being $cal_{av}(\rho)=\\{(\tau_{avs},\tau_{avc})\\}$ a resource
availability calendar with the set of time intervals in which the resource is
available to work. The WT due to resource unavailability of $\varepsilon_{i}$
is $\Omega_{unav}(\varepsilon_{i})=\\{(\tau_{i},\tau_{j})\mid\
(\tau_{i},\tau_{j})\in\omega(\varepsilon_{i})\wedge\nexists(\tau_{k},\tau_{l})\in
cal_{av}(\rho(\varepsilon_{i}))\mid(\tau_{i},\tau_{j})\perp(\tau_{k},\tau_{l})\\}$,
i.e., the set of intervals of the waiting time of $\varepsilon_{i}$ that do
not overlap with the availability calendar of the resource
$\rho(\varepsilon_{i})$ that executed $\varepsilon_{i}$.

Figure 6: Waiting time due to resource unavailability.

Waiting time due to extraneous factors. The last cause of waiting time that we
propose to consider is “extraneous factors”. We propose to classify as
_waiting time due to extraneous factors_ the waiting time intervals caused by
the external effects that cannot be identified from the event log – e.g. the
resource is working on another process, the activity instance cannot start
until some unrecorded event has occurred, fatigue effects, or context switch.
Thus, the waiting time of an activity instance due to extraneous factors is
defined as follows.

######  Definition 5 (Waiting Time Due to Extraneous Factors).

Given an activity instance log $L$ and an activity instance
$\varepsilon_{i}\in L$. The WT due to extraneous factors of $\varepsilon_{i}$
is $\Omega_{extr}(\varepsilon_{i})=\\{(\tau_{i},\tau_{j})\mid\
(\tau_{i},\tau_{j})\in\omega(\varepsilon_{i})\wedge\nexists(\tau_{k},\tau_{l})\in(\\{\omega_{ba}(\varepsilon_{i})\\}\bigcup\Omega_{rc}(\varepsilon_{i})\bigcup\Omega_{prior}(\varepsilon_{i})\bigcup\Omega_{unav}(\varepsilon_{i}))\mid(\tau_{i},\tau_{j})\perp(\tau_{k},\tau_{l})\\}$,
i.e., the set of intervals within the WT of $\varepsilon_{i}$ that does not
overlap with waiting times due to batching, resource contention,
prioritization, or resource unavailability.

Therefore, the second step of the approach results in a report discovering and
measuring the total waiting time for each transition according to their
causes. These results reveal the cause of each waiting times and by how much.

###  3.3 Waiting Time Analysis

The final step is to analyze how much each waiting time cause contributes to
the temporal performance of the process and their impact to the CTE. With that
purpose, we propose to compute the percentage of time that each cause induces
in the CTE of the process. In this context, we measure the CTE as the
processing time (PT) divided by the sum of the processing and the waiting time
(PT $+$ WT), where PT is the sum of the processing time of all activity
instances in the process, and WT is the sum of their waiting time. The impact
of waiting times per cause is calculated as the difference between the
original process CTE and the CTE if a particular waiting time is eliminated.
In this way, we can measure (1) the impact that each waiting time cause has on
the process CTE, (2) the impact that each transition has on the process CTE,
and (3) the impact that each waiting time cause has in each transition. This
metrics can indicate the potential CTE improvement if a particular cause of
waiting time is addressed.

As a result of the proposed analysis, we can analyze the discovered waiting
time causes and their impact on CTE. With this information, process analysts
can identify where the inefficiencies due to waiting times are localized,
choose which transitions and/or waiting time causes to address, and which
redesign alternatives to apply.

##  4 Evaluation

In this section, we present the evaluation of our approach. We evaluate the
approach by addressing two evaluation questions (EQ): (1) To which extent is
the technique able to detect the presence or absence of certain waiting time
causes?, (2) To what extent is the technique able to correctly quantify the
amount of waiting time waste per each cause? In this experimentation we use
synthetic data to validate the ability of the technique to accurately discover
transitions, their waiting times, and the waiting time causes known to be
present in the event logs. Then, we demonstrate the approach’s applicability
on a real-life event log. The approach implementation, the event logs and
experiment results, are all available on
GitHub.333https://github.com/AutomatedProcessImprovement/waiting-time-
analysis/tree/caise2023

###  4.1 Evaluation on Synthetic Data

To answer EQ1, we used a business process simulation model (BPS model) of a
loan application process to simulate a set of event logs with different
combinations of waiting time causes. To simulate WT due to resource
contention, we set a low number of available resources in the BPS model, so
that in some cases there were no resources available to process an enabled
activity instance. To create WT due to resource unavailability, we set
resource working calendars so that some resources worked from Monday to
Wednesday, and others from Thursday to Friday. To simulate WT due to
extraneous factors, we added timer events before some of the activities in the
BPS model, thus delaying their start. WT due to batching and prioritization
cannot be injected by modifying the simulation parameters, as current BPS
engines do not support them. Therefore, in case of batching, we added a set of
new traces delaying the start of some activity instances so that they are
processed as a batch. To simulate prioritization, we added a set of new traces
changing the order of execution of some activity instances, so they are
processed following a prioritization order. Combining these modifications, we
simulated a set of 32 event logs with all the combinations of causes of
waiting time and measured the performance using precision and recall. True
positives and false positives stand for the discovery of a waiting time cause
that, respectively, was and was not injected in the event log. True and false
negatives denote an undiscovered waiting time cause that, respectively, was
not and was injected.

Table 1: Results for the simulated event logs with all waiting time causes,
depicting the true positives with ’✓‘, the false positives with ’✗‘, and the
true negatives with an empty cell (there are no false negatives).

| S01 | S02 | S03 | S04 | S05 | S06 | S07 | S08 | S09 | S10 | S11 | S12 | S13 | S14 | S15 | S16
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
Batching |  | ✓ |  |  |  |  | ✓ | ✓ | ✓ | ✓ |  |  |  | ✗ |  |
Prioritization |  |  | ✓ |  |  |  | ✓ |  |  |  | ✓ | ✓ | ✓ | ✗ | ✗ |
Res. Contention |  |  |  | ✓ |  |  |  | ✓ |  |  | ✓ |  |  | ✓ | ✓ |
Res. Unavailability |  |  |  |  | ✓ | ✗ |  |  | ✓ | ✗ |  | ✓ | ✗ | ✓ | ✗ | ✓
Extraneous factors |  |  |  |  |  | ✓ |  |  |  | ✓ |  |  | ✓ |  | ✓ | ✓
| S17 | S18 | S19 | S20 | S21 | S22 | S23 | S24 | S25 | S26 | S27 | S28 | S29 | S30 | S31 | S32
Batching | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✗ |  |  | ✗ | ✓ | ✓ | ✓ | ✓ | ✗ | ✓
Prioritization | ✓ | ✓ | ✓ |  | ✗ |  | ✓ | ✓ | ✓ | ✗ | ✓ | ✓ | ✓ | ✗ | ✓ | ✓
Res. Contention | ✓ |  |  | ✓ | ✓ |  | ✓ | ✓ |  | ✓ | ✓ | ✓ |  | ✓ | ✓ | ✓
Res. Unavailability |  | ✓ | ✗ | ✓ | ✗ | ✓ | ✓ | ✗ | ✓ | ✓ | ✓ | ✗ | ✓ | ✓ | ✓ | ✓
Extraneous factors |  |  | ✓ |  | ✓ | ✓ |  | ✓ | ✓ | ✓ |  | ✓ | ✓ | ✓ | ✓ | ✓

Table 1 depicts the results for the simulated event logs used to evaluate EQ1.
Our approach discovered the injected waiting time causes in all the event logs
(no false negatives) resulting in a recall of 100%. However, due to the
influence that some waiting time causes have between them, the results contain
17 false positives (precision of 83%). False positives in WT due to resource
unavailability (S06, S10, S13, S15, S19, S21, S24, and S28) are caused by the
presence of extraneous waiting time, combined with limited data for the
discovery of resources’ working calendars. To simulate these logs, we set 24/7
working calendar for all resources (high availability). However, when a
resource has low occupation (executes few events), there is not enough data
for the calendar discovery to identify a 24/7 calendar and some intervals are
interpreted as non-working time. When these non-working intervals overlap with
extraneous waiting time, the tool classifies them as WT due to resource
unavailability. This limitation is inherent to the discovery of the resource
calendar, if there is no data showing that a resource was active during a
period of time, it cannot be assumed that they were working.

The injection of WT due to extraneous factors also induced false positives of
prioritization (S15, S21, S26, S30). When an activity instance is enabled but
waiting due to extraneous factors, the resource might execute other activities
enabled after the waiting one, being detected as WT due to prioritization.
These false positives are due to the absence of an explicit indicator of the
WT due to extraneous factors (i.e. extraneous waiting time is only detected
when no other causes are identified).

False positives due to batching (S14, S23, S26, S31) are caused by the
appearance of a batch processing behavior that was not intentionally added. To
create WT due to resource contention and unavailability, in some scenarios we
assigned working calendars that produced low resource availability. In such
cases, while instances were waiting until the resource became available, they
were collected and then, executed by the same resource. This resulted in an
unassigned but correctly discovered batch processing behavior.

EQ2 aimed at assessing if our approach is able to correctly identify waiting
time intervals and their causes. We could not use the set of event logs used
for EQ1 to answer EQ2, as the logs were created through stochastic business
process simulation – we know we have introduced a certain cause of waiting
time, but we don’t know to what extent. Therefore, we manually created a set
of 5 event logs (with up to 15 traces) with activity transitions having
different waiting time causes. Due to the low number of events per resource,
we manually defined the resource working calendars for this experiment. We ran
our technique over these logs and obtained accurate waiting time intervals and
their causes.

###  4.2 Evaluation on a Real-Life Log

To evaluate the applicability of the proposed approach in a real-life
scenario, we used an event log of a manufacturing production process [13]. The
event log has 225 traces (cases), recording the execution of 24 activities in
a total of 4,503 activity instances, executed by 46 resources.

First, we discovered activity transition instances and their characteristics:
91 transitions with 3421 transition instances (i.e., executions of each
transition). For each transition, we identified its characteristics (case
frequency, total frequency and total duration, i.e., total waiting time).

Second, we discovered the causes of waiting times. As a result, we obtained a
report that captures how much of the waiting time is induced by each cause in
every activity transition. The highest waiting times originated from the self-
loop transitions, i.e., when the same activity is executed for the case twice
in a row. For instance, transitions between two activity instances of “Turning
& Milling Q.C.” induced a total waiting time of 1101d 5h 34m. This made it the
greatest contributor to the total waiting time in the process. The largest
portion of the waiting time in this transition (54.74%) was caused by resource
unavailability and equaled 602d 18h 59m.

Finally, we analyzed the waiting times by calculating how much each cause
contributed to the total WT of the process and how they affected the CTE.
Thus, resource unavailability was the major source of WT as it caused 57% of
the total WT. It is followed by batching (22%), prioritization (9%),
extraneous (8%) and resource contention (4%). Then, we measured the impact of
the waiting times by cause on the process CTE (CTE = 6.81%). The highest CTE
increase (up to 14.62%) can be achieved if the WT due to resource
unavailability is eliminated. From the transition perspective, the highest
improvement opportunity lies in addressing the “Turning & Milling Q.C” self-
loop transition. If the WT is this transition is addressed, the CTE could
increase to 7.69%.

##  5 Conclusion

This paper outlines a process mining-based approach for identifying causes of
waiting times and their impact. To address research question RQ1, we propose a
method to attribute the waiting time of activity transitions to one of five
causes: batching, resource contention, prioritization, resource
unavailability, and extraneous factors. To address RQ2, we outline how these
five causes of waiting time can be discovered, for each activity transition,
from an event log. Finally, we propose to measure the impact of each waiting
time cause on the CTE of a process, to help analysts to prioritize
opportunities to reduce these waiting times (RQ3). The empirical evaluation
shows that our approach can accurately classify the waiting times in a process
into the five causes, in (synthetic) event logs where the causes of waiting
time are known. Finally, we illustrated the applicability of our approach
using an event log of a production process.

In its current form, the proposed approach only considers waiting times
associated with transitions between activity instances. Yet waiting times may
also arise in at least two other settings: (i) between case creation and start
of the first activity instance; and (ii) within an activity instance due to
interruptions (e.g. the resource interrupts their work and resumes it later).
The first of these waiting times could be analyzed by applying methods that
estimate the inter-arrival time of each trace [15, 4]. The second approach
requires new methods for modeling and inferring interruptions, possibly using
additional attributes in an event log or other additional data.

Another limitation of the approach is that it does not consider multitasking.
This could be addressed by inferring multitasking patterns from the log, and
using this information to estimate at what point in time a resource would
normally have started an activity instance, given their past multitasking
behavior.

In future work, we plan to develop a method for discovering business process
simulation models from event logs, which takes into account the causes of
waiting times considered in this paper. Such simulation models could be used
to support analysts in identifying combinations of redesign options to
optimize CTE, while also considering other performance dimensions (e.g. cost).

## References

  * [1] van der Aalst, W.M.P.: Process Mining: Data Science in Action. Springer, Heidelberg, 2nd edn. (2016)
  * [2] Andrews, R., Wynn, M.T.: Shelf time analysis in CTP insurance claims processing. In: Workshops on Trends and Applications in Knowledge Discovery and Data Mining (PAKDD 2017). pp. 151–162. Springer (2017)
  * [3] Antunes, B.B., Manresa, A., Bastos, L.S., Marchesi, J.F., Hamacher, S.: A solution framework based on process mining, optimization, and discrete-event simulation to improve queue performance in an emergency department. In: BPM. pp. 583–594. Springer (2019)
  * [4] Berkenstadt, G., Gal, A., Senderovich, A., Shraga, R., Weidlich, M.: Queueing inference for process performance analysis with missing life-cycle data. In: Proceedings of the 2nd International Conference on Process Mining (ICPM 2020). pp. 57–64. IEEE (2020)
  * [5] De Leoni, M., van der Aalst, W.M., Dees, M.: A general process mining framework for correlating, predicting and clustering dynamic behavior based on event logs. Information Systems 56, 235–257 (2016)
  * [6] Delias, P.: A positive deviance approach to eliminate wastes in business processes: The case of a public organization. Ind. Manag. Data Syst. (2017)
  * [7] Dumas, M., La Rosa, M., Mendling, J., Reijers, H.A., et al.: Fundamentals of business process management. Springer, 2nd edn. (2018)
  * [8] Erdogan, T.G., Tarhan, A.K.: Multi-perspective process mining for emergency process. Health Informatics Journal 28(1), 14604582221077195 (2022)
  * [9] Ferreira, D.R., Vasilyev, E.: Using logical decision trees to discover the cause of process delays from event logs. Computers in Industry 70, 194–207 (2015)
  * [10] Hompes, B.F., Maaradji, A., La Rosa, M., Dumas, M., Buijs, J.C., van der Aalst, W.M.: Discovering causal factors explaining business process performance variation. In: CAiSE. pp. 177–192. Springer (2017)
  * [11] Jansen-Vullers, M., Reijers, H.: Business process redesign in healthcare: towards a structured approach. INFOR 43(4), 321–339 (2005)
  * [12] Lashkevich, K., Milani, F., Chapela-Campa, D., Dumas, M.: Data-driven analysis of batch processing inefficiencies in business processes. In: RCIS. pp. 231–247. Springer (2022)
  * [13] Levy, D.: Production analysis with process mining technology (2014). https://doi.org/10.4121/uuid:68726926-5ac5-4fab-b873-ee76ea412399
  * [14] López-Pintado, O., Dumas, M.: Business process simulation with differentiated resources: Does it make a difference? In: BPM. pp. 361–378. Springer (2022)
  * [15] Martin, N., Depaire, B., Caris, A.: Using event logs to model interarrival times in business process simulation. In: Workshops of the 13th Intl. Conf. on BPM. pp. 255–267. Springer (2015)
  * [16] Martin, N., Pufahl, L., Mannhardt, F.: Detection of batch activities from event logs. Inf. Syst. 95, 101642 (2021)
  * [17] Milani, F., Lashkevich, K., Maggi, F.M., Di Francescomarino, C.: Process mining: A guide for practitioners. In: RCIS. pp. 265–282. Springer (2022)
  * [18] Ramakrishnan, S., Kumaran, S., Chang, H., Kulkarni, N., Srihari, K.: Defining and categorizing handoff points for the service domain. In: Proceedings of the 29th Annual Conf. of ASEM. pp. 12–15 (2008)
  * [19] Rummel, J.L., Walter, Z., Dewan, R., Seidmann, A.: Activity consolidation to improve responsiveness. Eur J Oper Res 161(3), 683–703 (2005)
  * [20] Senderovich, A., Weidlich, M., Gal, A., Mandelbaum, A.: Queue mining for delay prediction in multi-class service processes. Information Systems 53, 278–295 (2015)
  * [21] Toosinezhad, Z., Fahland, D., Köroğlu, Ö., Van Der Aalst, W.M.: Detecting system-level behavior leading to dynamic bottlenecks. In: 2020 2nd ICPM. pp. 17–24. IEEE (2020)
  * [22] Uysal, M.S., van Zelst, S.J., Brockhoff, T., Ghahfarokhi, A.F., Pourbafrani, M., Schumacher, R., Junglas, S., Schuh, G., van der Aalst, W.: Process mining for production processes in the automotive industry. In: Industry Forum at BPM. vol. 20 (2020)
  * [23] Van Der Aalst, W.M., Reijers, H.A., Weijters, A.J., van Dongen, B.F., De Medeiros, A.A., Song, M., Verbeek, H.: Business process mining: An industrial application. Information Systems 32(5), 713–732 (2007)
  * [24] Weijters, A.J.M.M., Ribeiro, J.T.S.: Flexible heuristics miner (FHM). In: Proceedings of the IEEE Symposium on CIDM. IEEE (2011)
  * [25] Yampaka, T., Chongstitvatana, P.: An application of process mining for queueing system in health service. In: 13th Intl. JCSSE. pp. 1–6. IEEE (2016)