<figure><img src="image_156.png" /></figure>

This method has the downside of increasing the size of the forbidden region exponentially in the number of loops in parallel. As Algorithm 4.1.17 scales quadratically with its size [19], it is in our best interest to reduce the number of unfolding. For the next part we will switch back to the Algorithm 1.4.33 as it gives much more tractable results, especially for the unsafe and doomed regions. Following the idea explained in this section we will first extend the notion of unfolding to the syntactic models of program. Then we will deepen the projection to work on the cubes of the underlying posets. Lastly we will prove that using our method we require only to unfold the program twice to get the doomed and unsafe regions.

### 4.1.2 Slight adjustment to the syntactic model

In this section, we go back to the syntactic models of programs of Chapter 3 and define a similar notion of unfolding for those. We use the same grammar for programs as in Definition 3.1.1, but change how we represent the positions in a loop. In Chapter 3, we used the contextual equivalence of Remark 1.1.26 to remove the looping paths and enforce a partial order on the states. This was done at the cost of losing the finiteness of the states in the presence of loops. In the following sections of this chapter, we will go back to considering loops as a pre-order where the terminal and initial positions have been identified.

As we are much more concerned with loops in this chapter, we will first define a few subsets of the programs in **NPIMP**. First let us give a quick reminder of **NPIMP**.

**Definition 3.1.1.** Let $\mathcal{R}$ be a fixed, finite set of resources. Let $a \in \mathcal{R}$. The language **NPIMP** is generated by the following syntactic expressions, defined by their grammar:

* the set $\mathcal{X}$ of actions:

$$A ::= P_a | V_a | \mathbf{skip} | \dots$$

* the set $\mathcal{C}$ of commands, or programs:

$$P, Q ::= A | P; Q | P^* | P+Q | P \parallel Q$$

We will define three subsets of **NPIMP** that will be of particular interest for this section: the processes $\mathbf{Prcs}$, consisting of sequential and conditional branchings, the looping processes $\mathbf{Prcs}^*$ which are loops of processes, and the simple loop programs $\mathbf{Pgrm}$, which are the parallel composition of multiple processes. Formally,
**Definition 4.1.19.** We define, on the language **NPIMP**, with its set of actions $\mathcal{X}$, three sub-languages:

* The set of loop-free processes **Prcs**:

$$S, T ::= A \in \mathcal{X} \mid S;T \mid S+T$$

* The set of process and single loops on them **Prcs**\*:

$$R ::= S \mid S^*$$

* The set of simple loop programs **Pgrm**:

$$P, Q ::= P \parallel Q \mid R$$

### 4.1.2.1 Looped semantics

In the following, we redefine the semantics of syntactic models to take this modification into account. In order to define the semantics, we will first need to redefine the evaluation/consumption $\llbracket - \rrbracket$, the states (positions of Definition 3.1.4) and the reduction relation between states (Definition 3.1.9) starting with the Definition 3.1.4. As the actions of the language have not changed, $\llbracket - \rrbracket_{\mathcal{X}}$ remains unchanged. We will then start to redefine the core notions with the new states of the syntactic model, following the presentation of Chapter 3.

**Definition 4.1.20.** Given a program $P$, pre-positions $p$ are generated by the following grammar:

$$p, q ::= \bot \mid \top \mid p; q \mid p^* \mid p+q \mid p \parallel q$$

Where we identify $\bot^*$ and $\top^*$ (i.e. $\bot^* = \top^*$).

Then as in Definition 3.1.7, we extract from the pre-positions, the effective positions (or states) of the program.

**Definition 4.1.21.** Given a program $P$, we write $P \models p$ to indicate that a pre-position $p$ is a (valid) *position* of a program $P$, this predicate being defined inductively by the following rules:

$$\begin{array}{l@{\qquad}l@{\qquad}l@{\qquad}l}
\frac{P \neq Q \parallel R}{P \models \bot} & \frac{P \models p}{P; Q \models p; \bot} & \frac{P \models p}{P+Q \models p+\emptyset} & \frac{P \models p}{P^* \models p^*} \\
\frac{P \neq Q \parallel R}{P \models \top} & \frac{Q \models q}{P; Q \models \top; q} & \frac{Q \models q}{P+Q \models \emptyset+q} & \frac{P \models p}{P \parallel Q \models p \parallel q}
\end{array}$$

for any pair of programs $Q, R$. We write $\mathcal{P}(P)$ for the set of positions of a program $P$. When there might be confusion we will write $\bot_P$ (resp. $\top_P$) to indicate $P \models \bot$ (resp. $P \models \top$). We write $\bot_{P \parallel Q}$ (resp. $\top_{P \parallel Q}$) for $P \parallel Q \models \bot \parallel \bot$ (resp. $P \parallel Q \models \top \parallel \top$)

Now we redefine the reduction relation between the states of Definition 3.1.9 and prove that it preserves the properties we care about (reachability, equivalence with a pre-order)
**Definition 4.1.22.** The *reduction relation* is defined inductively by the following rules. All the rules not concerning loops remain the same as Definition 3.1.9.

$$ \overline{P+Q \models \bot \rightarrow \emptyset+\bot} $$

$$ \overline{P+Q \models \bot \rightarrow \bot+\emptyset} $$

$$ \overline{P;Q \models \bot \rightarrow \bot;\bot} $$

$$ P \models p \rightarrow p' $$

$$ \overline{P+Q \models p+\emptyset \rightarrow p'+\emptyset} $$

$$ P \models p \rightarrow p' $$

$$ \overline{P;Q \models p;\bot \rightarrow p';\bot} $$

$$ P \models p \rightarrow p' \qquad Q \models q $$

$$ \overline{P \parallel Q \models p \parallel q \rightarrow p';q} $$

$$ Q \models q \rightarrow q' $$

$$ \overline{P+Q \models \emptyset+q \rightarrow \emptyset+q'} $$

$$ Q \models q \rightarrow q' $$

$$ \overline{P;Q \models \top; q \rightarrow \top; q'} $$

$$ P \models p \qquad Q \models q \rightarrow q' $$

$$ \overline{P \parallel Q \models p \parallel q \rightarrow p \parallel q'} $$

$$ \overline{P+Q \models \emptyset+\top \rightarrow \top} $$

$$ \overline{P+Q \models \top+\emptyset \rightarrow \top} $$

$$ \overline{P;Q \models \top;\top \rightarrow \top} $$

$$ \overline{\alpha \models \bot \rightarrow \top} $$

While reductions between positions of loops are replaced by the following rules.

$$ \overline{P^* \models \bot \rightarrow \bot} $$

$$ P \models \bot \rightarrow p' $$

$$ \overline{P^* \models \bot' \rightarrow p'^*} $$

$$ P \models p \rightarrow \top $$

$$ \overline{P^* \models p^* \rightarrow \top^*} $$

$$ \overline{P^* \models \bot^* \rightarrow \top} $$

$$ P \models p \rightarrow p' \qquad p, p' \notin \{\bot, \top\} $$

$$ \overline{P^* \models p^* \rightarrow p'^*} $$

**Lemma 4.1.23.** If $P \models p \rightarrow p'$ holds then both $P \models p$ and $P \models p'$ hold.

*Proof.* We refer to the proof of Lemma 3.1.11. The new reductions for loops do not change the core argument of the proof. □

Our model is no longer a partial order (because of the identification of $\bot^*$ and $\top^*$), but it still keeps the properties of being a well-quasi-order, although it is no longer useful, as we are dealing with finite sets and thus always finitely complemented (Definition 3.2.25).

**Definition 4.1.24.** Given a program $P$, the state space $G_P$ of this program is the graph whose vertices are the positions of $P$ (Definition 3.1.7) and edges are the reductions (Definition 3.1.9).

**Definition 4.1.25.** Given a program $P$, a path on $G_P$ is a sequence of reduction $\pi = (P \models p_i \rightarrow p_{i+1})_{0 \le i < n}$ also written $P \models \pi : p \rightarrow p_0^* p_n$ or $\pi : p_0 \rightarrow p^* p_n$. With the following constructions:

* Given two paths $\pi : p \rightarrow p^*$ and $\pi' : q \rightarrow p'^*$ we write $\pi' \cdot \pi : p \rightarrow p'^*$ for their concatenation.

* The empty path on a state $p$ is written $\varepsilon_p : p \rightarrow p^*$.

Furthermore, we say that

* An execution trace $\pi$ of $P$ is a path $P \models \pi : \bot \rightarrow p^*_P p$. When $p = \top_P$, i.e. $P \models \pi : \bot \rightarrow \top_P \top_P$, we say that $\pi$ is total.

* An execution trace $\pi$ of $P$ is maximal when it cannot be extended.

* An execution is *elementary* when it consists of one reduction step.
* A position $p$ is reachable when there exists an execution trace $\pi$ with $p$ as target i.e. $P \models \pi : \perp \rightarrow_P^* p$.

**Lemma 4.1.26.** Every position $p$ of $P$ is reachable for $\rightarrow^*$

*Proof.* See the proof of Corollary 3.1.26. □

As customary, we also write $P \models p \rightarrow^* p'$ (or sometimes simply $p \rightarrow^* p'$) when there exists a path $P \models \pi : p \rightarrow^* p'$. As before, consumption is equal to evaluation and is defined in the exact same way as for our previous model in Definition 3.1.14.

**Definition 4.1.27.** Given an execution $P \models \pi : p \rightarrow^* p'$, we write $[[P \models \pi : p \rightarrow^* p')] : \Sigma \rightarrow \Sigma$ (or sometimes simply $[[\pi]]$) for its evaluation or consumption of mutexes. This function is defined for elementary executions on each state $\sigma \in \Sigma$ by:

* For $a \in \mathcal{R}$, $[[P_a \models \pi : \perp \rightarrow \top]](\sigma) = [[P_a]]_\mathcal{R} = \delta_a^+(\sigma)$,

$$ \delta_a^+(\sigma)(b) = \begin{cases} \sigma(a) + 1 & \text{if } b = a \\ \sigma(a) & \text{otherwise} \end{cases} $$

* For $a \in \mathcal{R}$, $[[V_a \models \pi : \perp \rightarrow \top]] = [[V_a]]_\mathcal{R} = \delta_a^+(\sigma)$,

$$ \delta_a^+(\sigma)(b) = \begin{cases} \sigma(a) - 1 & \text{if } b = a \\ \sigma(a) & \text{otherwise} \end{cases} $$

* for each reduction $\pi$, different from the two above, deduced with a rule of Definition 4.1.22 with no premise we have $[[\pi]](\sigma) = \sigma$,

* for each reduction $\pi$ deduced with a rule of Definition 4.1.22 with one reduction $\pi'$ as premise, we have $[[\pi]] = [[\pi']]$,

and extended as a morphism of the category of executions on the monoid of consumptions, i.e. $[[\varepsilon]] = \text{id}$ and $[[\pi \cdot \pi']]] = [[\pi']]] + [[\pi]]$.

The notion of conservative program remains unchanged.

**Definition 3.1.15.** A program $P$ is conservative when for any pair of paths $\pi, \tau : x \rightarrow^* y$ in $G_P$ with same source and target we have for any state $\sigma \in \Sigma$ and any resource $a \in \mathcal{R}$:

$$ [[\pi]](\sigma)(a) = [[\tau]](\sigma)(a) $$

As before this implies that we can define consumption on positions instead of paths.

**Definition 4.1.28.** Given a conservative program $P$ and a position $p$ in $P(P)$, we define the consumption of $p$, written $[[p]] : \mathcal{R} \rightarrow \mathbb{Z}$ as follows:

$$ [[p]] = [[\pi]](\sigma_0) $$

for some path $\pi : \perp_P \rightarrow p$ and $\sigma_0$ the initial state of $P$ from Definition 3.1.2.

The consumption of a program stays the same as in Chapter 3.
**Definition 4.1.29.** The consumption of a program *P* is the partial function $\Delta(P) : \mathcal{R} \to \mathbb{Z}$ defined by induction on *P* by

$$ \Delta(\mathbf{P}_a) = \delta_a $$

$$ \Delta(\mathbf{V}_a) = -\delta_a $$

$$ \Delta(A) = \underline{0} $$

$$ \begin{align*} \Delta(P;Q) &= \Delta(P \parallel Q) = \Delta(P) + \Delta(Q) \\ \Delta(P+Q) &= \Delta(P) \quad \text{if } \Delta(P) = \Delta(Q) \\ \Delta(P^*) &= \underline{0} \quad \text{if } \Delta(P) = \underline{0} \end{align*} $$

where $\underline{0}$ is the constant function equal to 0 and $\delta_a$ the indicator function of a.

And the following proposition still holds

**Proposition 4.1.30.** The function $\Delta$ is only partially defined on programs. A program *P* is conservative if and only if $\Delta(P)$ is well-defined.

### 4.1.2.2 Properties of the state space

As we have loops in our state space, we can no longer hope to have a partial order. But, the state space $\mathcal{P}(P)$ of a program *P* still retains a pre-order relation that is equivalent to the reduction relation.

**Definition 4.1.31.** We write $\le$ for the smallest reflexive relation on the positions of *P* such that

$$ \begin{array}{c} \frac{P \neq Q \parallel R}{\perp \leq p} \\ \frac{P \neq Q \parallel R}{p \leq \top} \end{array} \qquad \frac{\begin{array}{c} p \leq p' \qquad q \leq q' \\ p; q \leq p'; q' \end{array}}{p+\emptyset \leq p'+\emptyset} \qquad \frac{\begin{array}{c} p \leq p' \qquad q \leq q' \\ p \parallel q \leq p' \parallel q' \end{array}}{\emptyset+q \leq \emptyset+q'} \qquad \frac{p^* \leq p'^*}{\phantom{p^* \leq p'^*}} $$

for any pair of programs *Q*, *R*.

**Proposition 4.1.32.** Given a program *P* and a position *p* of *P*, we have $\perp \le p$ (resp. $p \le \top$)

*Proof.* Given a program *P* and a position *p* of *P*, let us prove that $\perp \le p$ by induction on the program *P*.

* $P = Q \parallel R$. Then $\perp$ is a shorthand for $\perp \parallel \perp$ (Definition 3.1.7). And by Definition 3.1.7, $p = q \parallel r$ with $Q \models q$, $R \models r$. By induction hypothesis, $\perp \le q$ and $\perp \le r$. Thus, by the inference rules of Definition 3.1.23, we have

$$ \frac{\perp \leq q \quad \perp \leq r}{\perp \parallel \perp \leq q \parallel r} $$

Thus $\perp = \perp \parallel \perp \le q \parallel r = p$.

* Otherwise, the property is immediate by the rule $\frac{P \neq Q \parallel R}{\perp \le p}$ from Definition 3.1.23.
The property $p \leq \top$ is proved in the same way.

□

**Proposition 4.1.33.** *Given two positions *p* and *p'* of *P*, we have *p* ≤ *p'* if and only if *p* →* p'*.□

*Proof.* This is proved by induction on *P*.

* P is not of the form $L^*$. We can refer to the proof of Proposition 3.1.25, as for this case, the reduction relation and induction rules for $\leq$ remain the same.

* $P = L^*$. Let us suppose $p, p' \notin \{\perp, \top\}$, i.e. $p = l^* \leq l'^* = p'$. Then the inference rules for $\leq$ give:

$$ \overline{l^* \leq l'^*} $$

This implies that $p \leq p'$ always hold. Let us show that it is similar for $p \to^* p'$. By inference rules $l \leq_L \top$ and $\perp \leq_L l'$, i.e. $l \to^* \top$ and $\perp \to^* l'$. Then from the following inference rules

$$ \frac{L \models p \to^* \top}{L^* \models p^* \to^* \top^*} \qquad \frac{L \models p \to p' \qquad p, p' \notin \{\perp, \top\}}{L^* \models p^* \to p'^*} \qquad \frac{L \models \perp \to^* p'}{L^* \models \perp^* \to^* p'^*} $$

we can deduce:

$$ \frac{L \models p \to^* \top}{L^* \models p^* \to^* \top^*} \qquad \frac{L \models \perp \to^* p'}{L^* \models \perp^* \to^* p'^*} $$

Thus, for $p, p' \notin \{\perp, \top\}$, we have

$$ L^* \models p \to^* p' $$

Now if $p = \top$, by inference rules, $p \leq p'$ or $p \to^* p'$ implies $p = p' = \top$. Dually, $p' = \perp$ implies $p = p' = \perp$. The remaining cases can be treated similarly to the case $p, p' \notin \{\perp, \top\}$ above, remarking that $p \leq p'$ always holds, adding the following rules in the construction of the path:

$$ \overline{P^* \models \perp \to \perp^*} \qquad \overline{P^* \models \perp^* \to \top} $$

□

**Proposition 4.1.34.** *Let *P* be a program, then its set of positions (*P*(*P*), $\leq$) is a bounded preorder, with $\perp$ (resp. $\top$) as minimal (resp. maximal) element. Furthermore, if $P \in \mathbf{Prcs}$ is a program without loops, then its set of positions *P*(*P*) is a well-ordered lattice.*

*Proof.* By definition of $\to^*$ as a reflexive and transitive closure, and Proposition 4.1.33. When *P* is loop-free, we can fall back to the proof of Proposition 3.1.32 to prove that it is indeed a lattice. By Proposition 4.1.32 and the fact that there are no reduction with $\perp$ as a target, we have that $\perp$ is the minimal element. The property for $\top$ is proved dually. □
### 4.1.3 2-unfolding of programs: syntactic version

Following the method in [17] presented in Section 4.1.1.2, we define what it means to unfold the syntactic model of a program. As previously stated we will show that a 2-unfolding is enough to compute the doomed and unsafe regions. In [17], the n-unfolding of a program $L^*$ is given by sequentially composing n copies $L$; ...; $L$ of a program. Thus, a 2-unfolding of $L^*$ correspond to the sequential constructor $L$; $L$. For more complex programs, the unfolding is defined inductively as follows:

**Definition 4.1.35.** The 2-unfolding $\mathcal{U}: \mathbf{Pgrm} \to \mathbf{Pgrm}$ of programs is defined inductively as follows:

$$ \begin{array}{l} \mathcal{U}(P \parallel Q) = \mathcal{U}(P) \parallel \mathcal{U}(Q) \qquad \mathcal{U}(P;Q) = \mathcal{U}(P);\mathcal{U}(Q) \qquad \mathcal{U}(\alpha) = \alpha \\ \mathcal{U}(P^*) = \mathcal{U}(P);\mathcal{U}(P) \qquad \mathcal{U}(P+Q) = \mathcal{U}(P)+\mathcal{U}(Q) \end{array} $$

*Remark 4.1.36.* $\mathcal{U}$ is the identity for all programs in $\mathbf{Pgrm}$ without loops.

By definition, the positions of $L$; $L$ project naturally onto the positions of $L$. Indeed, by the inference rules in Definition 4.1.21, a position of $L$; $L$ is either $\perp$, $\top$, $l$; $\perp$ or $\top$; $l$ with $l \in L$. Similarly, the positions of $L^*$, are either $\perp$, $\top$ or $l^*$.

From this remark we can define a very natural function, mapping positions of a 2-unfolding $L$; $L$ onto its base program $L^*$ by sending $l$; $\perp$ and $\top$; $l$ to $l^*$.

**Definition 4.1.37.** Given a program $P$, we define its folding projection $\Phi_P: \mathcal{P}(\mathcal{U}(P)) \to \mathcal{P}(P)$ as follows

$$ \begin{array}{l} \Phi_P(\perp_{\mathcal{U}(P)}) = \perp_P \qquad \Phi_{P^*}(p; \perp) = \Phi_P(p)^* \qquad \Phi_{P+Q}(p+\emptyset) = \Phi_P(p)+\emptyset \\ \Phi_P(\top_{\mathcal{U}(P)}) = \top_P \qquad \Phi_{P^*}(\top; p) = \Phi_P(p)^* \qquad \Phi_{P+Q}(\emptyset+q) = \emptyset+\Phi_Q(q) \\ \Phi_{P \parallel Q}(p \parallel q) = \Phi_P(p) \parallel \Phi_Q(q) \qquad \Phi_{P;Q}(p; q) = \Phi_P(p); \Phi_Q(q) \end{array} $$

*Remark 4.1.38.* By a simple albeit tedious proof by induction, $\Phi_P: \mathcal{P}(\mathcal{U}(P)) \to \mathcal{P}(P)$ is surjective.

One very nice property of the folding projection is that, for conservative programs, it will preserve the consumption of resources of a given position (Definition 4.1.28). Meaning that if we can compute the forbidden/authorized region in the 2-unfolding of a program (which is loop-free), its pointwise image by the projection $\Phi$ will be the forbidden/authorized region of the base program.

**Proposition 4.1.39.** Given a program $P$ and a position in its 2-unfolding $p \in \mathcal{P}(\mathcal{U}(P))$, then

$$ [[p]] = [[\Phi_P(p)]] $$

where $[[\cdot]]$ is the resource consumption of a position defined in Definition 4.1.28.

*Proof.* Let $P \in \mathbf{Pgrm}$. Let us prove by induction on $p$ that

$$ \forall p \in \mathcal{P}(P), [[p]] = [[\Phi(p)]] $$

First let us remark that by Definition 4.1.27 $[[\perp_P]] = 0 = [[\perp_{\mathcal{U}(P)}]] = [[\Phi_P(\perp_P)]]$.
• Let $P = \alpha$, then $\mathcal{U}(P) = P$ and $\Phi = \text{id}$.

• Let $P = S+T$.

– $p = s+\emptyset \in \mathcal{P}(\mathcal{U}(P))$, then

$$
\begin{align*}
[\! [p]] &= [\pi : \bot \to^* p] \tag*{Definition 4.1.28} \\
&= [\pi : \bot \to^* s+\emptyset] \\
&= [(\bot+\emptyset \to^* s+\emptyset) \cdot (\bot \to^* \bot+\emptyset)] \tag*{Definition 4.1.27} \\
&= [\bot+\emptyset \to^* s+\emptyset] + [\bot \to^* \bot+\emptyset] \tag*{Definition 4.1.27} \\
&= [\bot \to^* s] + \emptyset \tag*{Definition 4.1.27} \\
&= [s] \tag*{Definition 4.1.28} \\
&= [\Phi_S(s)] \tag*{Induction Hypothesis} \\
&= [\bot \to^* \Phi(s)] \tag*{Definition 4.1.28} \\
&= [\Phi_S(\bot) \to^* \Phi_S(s)] \\
&= [\Phi_P(\bot)+\emptyset \to^* \Phi(s)+\emptyset] \tag*{Definition 4.1.28} \\
&= [\bot \to^* \Phi(s)+\emptyset] \tag*{Definition 4.1.28} \\
&= [\Phi(s)+\emptyset] \tag*{Definition 4.1.28} \\
[\! [p]] &= [\Phi_P(p)]
\end{align*}
$$

– Similarly if $p = \emptyset+t$, then $[p] = [\Phi(p)]$

– $p = \top_{\mathcal{U}(P)}$. Let $\pi : \bot_{\mathcal{U}(P)} \to^* \top_{\mathcal{U}(P)}$,

$$
\begin{align*}
[\top_{\mathcal{U}(P)}] &= [\pi] \tag*{Definition 4.1.28} \\
&= [\bot_{\mathcal{U}(P)} \to^* \top_{\mathcal{U}(S)} + \emptyset] + [\top_{S} + \emptyset \top_{\mathcal{U}(P)}] \\
&= [\top_{\mathcal{U}(S)} + \emptyset] + \emptyset \tag*{Definition 4.1.28} \\
&= [\Phi(\top_{\mathcal{U}(S)} + \emptyset)] \tag*{By the case above} \\
&= [\Phi_S(\top_{\mathcal{U}(S)} + \emptyset)] \\
&= [\top_{S} + \emptyset] \\
&= [\bot_{S+T} \to^* \top_{S+T}] + [\top_{S+T} \to^* \top_{S+T}] \tag*{Definition 4.1.27} \\
&= [\bot_{S+T} \to^* \top_{S+T}] \tag*{Definition 4.1.27} \\
&= [\top_{P}] \tag*{Definition 4.1.28} \\
[\top_{\mathcal{U}(P)}] &= [\Phi_P(\top_{\mathcal{U}(P)})]
\end{align*}
$$

• The case $P = S;T$ is treated in much the same way.
• $P = S \| T$.

<table>
  <tr>
    <td>$[s \| t] = [\pi: \perp_{\mathcal{U}(S)} \| \mathcal{U}(T) \to^* s \| t]$</td>
    <td>Definition 4.1.28</td>
  </tr>
  <tr>
    <td>$=[\pi: \perp \| \perp \to^* s \| t]$</td>
    <td>Definition 4.1.27</td>
  </tr>
  <tr>
    <td>$=[\perp \| \perp s \| \perp \to^* s \| t]$</td>
    <td>by conservativity</td>
  </tr>
  <tr>
    <td>$=[\perp \| \perp \to^* s \| \perp] + [s \| \perp \to^* s \| t]$</td>
    <td></td>
  </tr>
  <tr>
    <td>$=[\perp \to^* s] + [\perp \to^* t]$</td>
    <td>Definition 4.1.27</td>
  </tr>
  <tr>
    <td>$=[s] + [t]$</td>
    <td>Definition 4.1.28</td>
  </tr>
  <tr>
    <td>$=[\Phi(s)] + [\Phi(t)]$</td>
    <td>Induction hypothesis</td>
  </tr>
  <tr>
    <td>$=[\perp \to^* \Phi(s)] + [\perp \to^* \Phi(t)]$</td>
    <td>Definition 4.1.28</td>
  </tr>
  <tr>
    <td>$=[\perp \| \perp \to^* \Phi(s) \| \perp] + [\Phi(s) \| \perp \to^* \Phi(s) \| \Phi(t)]$</td>
    <td></td>
  </tr>
  <tr>
    <td>$=[\perp \| \perp \to^* \Phi(s) \| \Phi(t)]$</td>
    <td>Definition 4.1.27</td>
  </tr>
  <tr>
    <td>$=[\perp_{S \| T} \to^* \Phi(s) \| \Phi(t)]$</td>
    <td>Definition 4.1.27</td>
  </tr>
  <tr>
    <td>$[s \| t] = [\Phi(s) \| \Phi(t)]$</td>
    <td>Definition 4.1.28</td>
  </tr>
</table>

• $P = S^*$. Then $\mathcal{U}(P) = S;S$. First let's remark that for any conservative program $X$, by Proposition 4.1.30

$$ \Delta(X) = [[\top_{X^*}]] = [[\top_{X}]] = 0 \qquad (4.1) $$

– $p = s;\perp$. As we consider conservative programs, the consumption is independent of the path chosen (Definition 4.1.28), so we will choose a cycle-free path $\pi: \perp \to^{\text{lf}} \Phi(p)$ to ensure that we only require the $\frac{P \models p \to p'}{P^* \models p^* \to p'^*}$ rule for reductions in the loop.

<table>
  <tr>
    <td>$[p] = [[\perp_{\mathcal{U}(P)} \to^{\text{lf}} p]]$</td>
    <td>Definition 4.1.28</td>
  </tr>
  <tr>
    <td>$=[\perp \to \perp; \perp] + [[\perp_S; \perp_S \to^{\text{lf}} s; \perp_S]]$</td>
    <td>Definition 4.1.27</td>
  </tr>
  <tr>
    <td>$= \underline{0} + [[\perp_S \to^{\text{lf}} s]]$</td>
    <td>Definition 4.1.27</td>
  </tr>
  <tr>
    <td>$=[\perp^* \to^{\text{lf}} s^*]$</td>
    <td>Induction Hypothesis</td>
  </tr>
  <tr>
    <td>$=[\perp_P \to^{\text{lf}} \perp_S^*] + [[\perp^* \to^{\text{lf}} s^*]]$</td>
    <td>Definition 4.1.27</td>
  </tr>
  <tr>
    <td>$=[\perp_P \to^{\text{lf}} \Phi(p)]$</td>
    <td></td>
  </tr>
  <tr>
    <td>$[p] = [\Phi(p)]$</td>
    <td>Definition 4.1.28</td>
  </tr>
</table>

– $p = \top; s$. As $\Phi(\top; s) = \Phi(s; \perp)$, we will simply prove

$$ [[\top; s]] = [[s; \perp]] $$
Thus

$$ \llbracket \top; s \rrbracket = \llbracket \bot \to^* \bot_S; \bot_S \rrbracket + \llbracket \bot_S; \bot_S \to^* \top_S; \bot_S \rrbracket + \llbracket \top_S; \bot_S \to^* \top_S; s \rrbracket \qquad \text{Definition 4.1.27} $$

$$ = \llbracket \bot_S \to^* \top_S \rrbracket + \llbracket \bot_S \to^* s \rrbracket \qquad \text{Definition 4.1.27} $$

$$ = \llbracket \bot_S \to^* s \rrbracket \qquad \text{Eq. (4.1)} $$

$$ = \llbracket \bot_S; \bot_S \to^* s; \bot_S \rrbracket \qquad \text{Definition 4.1.27} $$

$$ = \llbracket \bot_P \to^* s; \bot_S \rrbracket \qquad \text{Definition 4.1.27} $$

$$ \llbracket \top; s \rrbracket = \llbracket s; \bot_S \rrbracket \qquad \text{Definition 4.1.28} $$

$$ - p = \top_{\mathcal{U}(P)} $$

$$ \llbracket \top_{\mathcal{U}(P)} \rrbracket = \llbracket \pi \rrbracket = \llbracket \bot_{\mathcal{U}(P)} \to^* \top_{\mathcal{U}(S)}; \top_{\mathcal{U}(S)} \rrbracket + \llbracket \top_{\mathcal{U}(S)}; \top_{\mathcal{U}(S)} \to \top_{\mathcal{U}(P)} \rrbracket = \llbracket \top_{\mathcal{U}(S)}; \top_{\mathcal{U}(S)} \rrbracket + \llbracket 0 \rrbracket \qquad \text{Definition 4.1.28} $$

$$ = \llbracket \Phi(\top_{\mathcal{U}(S)}; \top_{\mathcal{U}(S)}) \rrbracket \qquad \text{By the case above} $$

$$ = \llbracket \top_S; \top_S \rrbracket + \llbracket 0 \rrbracket = \llbracket \bot_P \to^* \top_S; \top_S \rrbracket + \llbracket \top_S; \top_S \to^* \top_P \rrbracket \qquad \text{Definition 4.1.27} $$

$$ = \llbracket \bot_P \to^* \top_P \rrbracket \qquad \text{Definition 4.1.27} $$

$$ = \llbracket \top_P \rrbracket \qquad \text{Definition 4.1.28} $$

$$ \llbracket \top_{\mathcal{U}(P)} \rrbracket = \llbracket \Phi(\top_{\mathcal{U}(P)}) \rrbracket $$

□

## 4.2 Syntactic cubical covers for programs with loops

Although we are now dealing with finite syntactic models, the state space might still be large, and we would still like to have a compact representation of the different regions. The simplest way to go about it is to reuse the representation of sets of positions by cubical covers from Chapter 3.

The folding projection $\Phi_P$ already gives a way of going from the unfolding to the base program and back, and if we only wanted to implement Algorithm 4.1.6 we could stop at that, but we hope that we can extend this projection further to make use of the efficient representation given by (syntactic) cubical covers.

Thus, we want to extend the folding projection $\Phi_P$ to a projection $\Psi_P: C(\mathcal{U}(P)) \to C(P)$, sending the cubes of the unfolding to the base program. This projection $\Psi_P$ should, at the very least, send a cube $c$ of $\mathcal{U}(P)$ to a cube $\Psi(c)$ whose underlying support is equal to the projection by $\Phi$ of the support of $c$. That means for any cube $c$, we should have $[\Psi(c)] = \Phi([c])$.

Indeed, using the fact that the folding projection $\Phi: P(\mathcal{U}(P)) \to P(P)$ preserves forbidden positions (Proposition 4.1.39), this would imply that covers of the forbidden (resp. forbidden) regions of the unfolding are sent to covers of the forbidden (resp. forbidden) regions of the base program.
Furthermore, as we are still working with implementability on mind, this projection on cubes should not be too costly to compute.

As cubes are defined by pairs of positions, our first, very natural intuition is that we could use $\Phi \times \Phi : \mathcal{P}(U(P)) \times \mathcal{P}(U(P)) \to \mathcal{P}(P) \times \mathcal{P}(P)$ as our projection on cubes $\Psi_P$.

Unfortunately, this approach does not work, but the fault lies not in our choice of projection but more in the definition of our cubes. Indeed, for preorders, as seen in the Example 4.2.1 and Example 4.2.2, there is no way of separating two equivalent elements from being in the same cube. As all elements of a loop are equivalent, this makes it impossible to project any cube onto the loop without increasing the underlying support. In a first time, we should then try to adapt our definition of cubes so that they work in the more general setting of partially ordered sets.

**Example 4.2.1.** Let us consider the preorder $(\{x, y, z\}, \le)$ where all elements are equivalent, i.e. $x \le y \le z \le x$. Using Definition 3.2.1, $(x, x) = \{b \mid x \le b \le x\} = \{x, y, z\}$. The same is true for all cubes.

**Example 4.2.2.** Let us consider the program $P = (P_a; (V_a; P_a))^* \parallel (P_a; V_a)$ from Example 1.3.34. Its syntactic semantics will give the space below, with the forbidden region in grey.

<figure><img src="image_157.png" /></figure>

As the inference rule $\frac{p^* \le p'^*}{\le}$ for $\le$ has no premises, all elements of the loop are equivalent. This means that taking any pair of positions within the loop results in a cube whose support is the whole loop. This implies that the forbidden region, represented in grey, cannot be described by cubes, as any cube trying to describe the loop will have a support equal to the whole section of the loop.

In this section we first introduce the concept of trivial loops with regard to two positions, corresponding to loops that are a “level (of nested loop) below” the two positions and can in a way be safely ignored. Then, based on this definition we generalize our previous definition of syntactic cubes to give satisfying results in the case of loops, which are defined as set of points cover by paths without any non-trivial loops. Then, we define our cubical refolding projection $\Psi_P$ by separating which cubes can be projected by $\Phi \times \Phi$ and which cubes need more work, proving that $[\Psi(-)] = \Phi([-])$ in Proposition 4.2.44.
## 4.2.1 Generalizing syntactic cubes

In this section we will define a new notion of syntactic cubes suitable for our new state space for looped programs. Indeed, keeping the same definitions we used for syntactic cubes when the state space was partially ordered leads to some strange results as shown in Example 4.2.2. In most cases, it is impossible to cover a region inside the loop by cubes, which is obviously bad.

Ideally, our new definition of syntactic cube/cubes should be the same as the previous one when considering loop-free programs. Thus, we try to generalize our definition of cubes from Definition 3.2.1.

### 4.2.1.1 Paths, loops and problems

One can remark that, given a loop-free program $P$ and two positions $p, q \in P(P)$, the support $[p, q]$ is not only the set of points $\{x \in P(P) \mid p \le x \le q\}$, but also the set of points traversed by a path from $p$ to $q$ (Proposition 3.1.25). This implies that a cube $(p, q)$ can also be defined as the set $\{\pi: p \to^* q\}$ while its support would be defined as the union of the “supports” of those paths. This doesn’t change any of the properties of our cubes.

Unfortunately, it also does not fix any of the problems for pre-orders. This might be due to the fact, that in our partially ordered setting, any path was cycle-free, which for pre-orders is no longer the case. We then give a first attempt at defining our syntactic cubes as set of loop-free paths between two endpoints.

**Definition 4.2.3.** Let $\mathcal{P}$ be a finite set equipped with a binary relation $\to$. Given two elements $p, q \in \mathcal{P}$, a path $\pi$ on $\mathcal{P}$ from $p$ to $q$ is a (possibly empty) finite sequence of reductions $(p_i \to p_{i+1})_{0 \le i \le n}$, such that $p = p_0$ and $q = p_{n+1}$.

We write $\pi: p \to^* q$ for $\pi$ is a path from $p$ to $q$. If $\pi$ is empty, then $p = q$ and $\pi$ is called the empty path on $p$, denoted $\varepsilon_P: p \to^* p$

**Definition 4.2.4.** Let $\mathcal{P}$ be a finite set equipped with a binary relation $\to$. Given a path $\pi = (p_i \to p_{i+1})_{0 \le i \le n}$ on $\mathcal{P}$, we say that $\pi$ is acyclic when for all $0 \le i \ne j \le n+1$, $p_i \ne p_j$.

**Definition 4.2.5.** Let $(\mathcal{P}, \to)$ as in Definition 4.2.4. Given two positions $p, q \in \mathcal{P}$, we define the cube $(p, q)$ as the sets of all acyclic paths from $p$ to $q$:

$$ (p, q) = \{\pi \mid \pi: p \to^* q \text{ with } p, q \in \mathcal{P}, \pi \text{ acyclic}\} $$

The supports of such cubes is defined as the union of the supports of the paths it contains, i.e. the set of points that are visited by a path.

**Definition 4.2.6.** Let $(\mathcal{P}, \le)$ a finite preorder and two elements $p, q \in \mathcal{P}$. Given a path $\pi: p \to^* q = (p_i \to p_{i+1})_{0 \le i \le n}$,

* for $p' \in \mathcal{P}$, we write $p' \in \pi$, when there exists $0 \le i \le n+1$ such that $p' = p'_i$,

* we define the support $[\pi]$ of $\pi$ as $\{p' \in \mathcal{P} \mid p \in \pi\}$
Then the support, i.e. the associated cubical region, of a cube $(p, q)$ from Definition 4.2.5 is defined as $[p, q] = \bigcup_{\pi \in (p, q)} [\pi]$. Once again, this corresponds in the case of loop-free programs, but as shown in Example 4.2.7, the cube $(\perp, \top)$ has some strange behaviour. This suggests that excluding all loops might be a bit too brutal.

*Example 4.2.7.* Let us consider a very simple program $P = (\mathbf{skip}; \mathbf{skip})^*$. Its syntactic semantics is given below, with the support of the cube $(\perp, \top) = \{(\perp \to \perp^* \to \top)\}$ in grey.

<figure><img src="image_158.png" /></figure>

We would expect to be able to describe the whole set of positions simply with the cube $(\perp, \top)$, as in the case of programs without loops. Furthermore, if we were to lift its support with $\Phi^{-1}$ we would expect to get the support of the whole set of positions of the unfolding, which would not be the case here.

### 4.2.1.2 Hierarchy of nested loops

The problem mentioned above comes from the fact that our cubes “see” too much detail in the program. Indeed, in the Example 4.2.7 above, the positions outside (or “above”) the loop, care about information of the path in the loop, and are severely restricted as a consequence.

Using the idea that loops of a “smaller” scale than the edges of the cube can be omitted, we will define a notion of *trivial paths* and define cubes as sets of paths with no non-trivial loops, instead of simply excluding all loops.

*Example 4.2.8.* Let us consider the program $P = ((\mathbf{skip}; \mathbf{skip})^*; \mathbf{skip})^*$, whose semantics is given below. All positions in the loop are equivalent for the preorder relation. Nonetheless, we would like to distinguish between the level of loop-nesting $d$ of the positions.

<figure><img src="image_159.png" /></figure>
We are thus going to equip our preorders with a depth function, to differentiate to which degree positions are equivalent for the preorder relation, this would correspond to checking how many levels of nesting of loops there are for a selected instruction. Sub-paths of a path that only explore positions at a greater depth are said to be trivial. The base path should not concern itself with what happens during these sub-paths.

**Definition 4.2.9.** Given a preorder $\mathcal{P}$ equipped with a function $d: \mathcal{P} \to \mathbb{N}$ called a *depth function*, and a path $\pi: p \to^* q$ on elements of $\mathcal{P}$. We say that a sub-path $\sigma$ of $\pi$ is *d-trivial* in $\pi$ if and only if for all $x \in \sigma$, $d(x) > d(p)$ and $d(x) > d(q)$.

**Definition 4.2.10.** Given a preorder $\mathcal{P}$, we say that a path $\pi$ on $\mathcal{P}$ has a *non-d-trivial cycle* when there exists a non-empty sub-path $\sigma \subseteq \pi$ such that $\sigma$ is not d-trivial and $\sigma$ is a cycle. When a path $\pi: p \to^* q$ has no non d-trivial cycle, we say that $\pi$ is *without trivial cycles* or *cycle-free*, and we write $\pi: p \to^{\text{lf}} q$.

**Definition 4.2.11.** Given a sequential program $P$, we define the *depth* $d_P$ of the position of $P$ as follows.

$$d_P: \mathcal{P}(P^*) \to \mathbb{N} \\ p \mapsto \begin{cases} 1 + d_P(q) & \text{if } p = q^* \\ 0 & \text{otherwise} \end{cases}$$

For all other cases

$$d_{P;Q}(p; \perp) = d_P(p)$$

$$d_{P+Q}(p + \emptyset) = d_P(p)$$

$$d_P(\perp) = 0$$

$$d_{P;Q}(\top; q) = d_Q(q)$$

$$d_{P+Q}(\emptyset + q) = d_Q(q)$$

$$d_P(\top) = 0$$

For looped programs, the depth function $d$ is exactly the greatest depth (level of nesting) of the loop the position is in. And a loop is trivial only if it involves positions of a greater depth than the extremities of the path.

For now, we only consider programs without nested loops, so a path $\pi$ has a non-trivial cycle (Definition 4.2.10) if and only if $\pi: \perp \to^* \top$ and $\pi$ has a cycle.

**Proposition 4.2.12.** *Given a program $P \in \mathbf{Pgrm}$, and a path $\pi: p \to^* q = (p_i \to p_{i+1})_{1 \le i \le n}$ on $\mathcal{P}(P)$, is without non-trivial cycles if and only if $\pi$ is empty or for all $i \ne j$, $p_i = p_j$ implies that $p_i$ is not equivalent to $p$ or $q$.*

*Proof.* By definition of $d_P$ and the inference rule $\overline{p_i^* \le q_j^*}$ two positions $p_i$ of $\mathcal{P}(P^*)$ are equivalent implies that they have the same depth. Thus, by definition of trivial cycles. $\pi$ is without trivial cycles only if $i \ne j$, $p_i = p_j$ implies that $p_i$ is not equivalent to $p$ or $q$. $\square$

Coming back to Example 4.2.7, all cycles are trivial for a path $\pi: \perp \to^* \top$, thus the support of the cube $(\perp, \top)$ will give the whole program as expected.

Before we proceed any further we will remark some few interesting properties for paths on the syntactic semantics of a program. First, paths contained in a single iteration of a loop $L^*$ can be seen as path on the program $L$, with the property of being without non-trivial loops transferring from one path to another.
**Definition 4.2.13.** Let $P \in \mathbf{Prcs}$, $p, q \in \mathcal{P}(P)$, $p \le q$, $p, q \ne \perp, \top$

* Given a path $\pi = (x_i \to x_{i+1})_{i \le n}: p \to^* q$ on positions of $P$, we define the path $\pi^* = (x_i^* \to x_{i+1}^*)_{i \le n}: p^* \to^* q^*$ on positions of $P^*$.

* Given a path $\pi^* = (x_i^* \to x_{i+1}^*)_{i \le n}: p^* \to^* q^*$ such that for all $i \notin \{0, n+1\}$, $x_i^* \ne \top^*$ we associate the path $\pi^{\mathrm{lf}} = (x_i \to x_{i+1})_{i \le n}: p \to^* q$

Furthermore

* If $\pi: p \to^{\mathrm{lf}} q$ then, the associated path $\pi^*: p^* \to^{\mathrm{lf}} q^*$ is also cycle-free

* If $\pi^*: p^* \to^{\mathrm{lf}} q^*$ then, the associated path $\pi^{\mathrm{lf}}: p \to^{\mathrm{lf}} q$ is also cycle-free.

*Proof.* (Proof of Definition 4.2.13) Let $P \in \mathbf{Prcs}$, $p \le q \in \mathcal{P}(P)$, $p, q \ne \perp, \top$. We must prove that the path we construct are indeed valid paths and prove that cycle-free properties are transferred.

* Let $\pi = (x_i \to x_{i+1})_{i \le n}: p \to^{\mathrm{lf}} q$ a cycle-free path. Then by Definition 4.1.22, $\pi^* = (x_i^* \to x_{i+1}^*)_{i \le n}: p^* \to^* q^*$. Let us suppose the existence of $i \ne j$ such that $x_i^* = x_j^*$. As all $x_i, x_j$ are distinct ($\pi$ cycle-free), this implies by Definition 3.1.7, $\{x_i, x_j\} = \{\perp, \top\} \subseteq [\pi]$ This is not compatible with the fact that $p, q \ne \perp, \top$. Thus, $\pi^*$ has no trivial loops.

* Let $\pi^* = (x_i^* \to x_{i+1}^*)_{i \le n}$ such that $\pi^*: p^* \to^{\mathrm{lf}} q^*$. $p \le q$ and for all $i \notin \{0, n+1\}$, $x_i^* \ne \top^*$ implies

$$i \ne 0, x_i \ne \perp \text{ and for all } i \ne n+1, x_i \ne \top$$

This implies that for all $i$, the reduction $x_i^* \to x_{i+1}^*$ is such that $x_i \ne \top$ and $x_{i+1} \ne \perp$. Thus, by Definition 4.1.22, this implies $z_i \to z_{i+1}$. Thus, $\pi = (x_i \to x_{i+1})_{i \le n}: p \to^{\mathrm{lf}} q$. And furthermore, this path is without non-trivial loops as $\mathcal{P}(P)$ is a partial order (Proposition 4.1.34). $\square$

Furthermore, for certain paths of a looping program $P^*$, we have a criterion for easily determining if the core of the loop $\perp^*$ belongs to the support. This criterion will be useful later on to distinguish between the cubes of our preorder.

**Lemma 4.2.14.** Let $P \in \mathbf{Prcs}$. Let $p, q \in \mathcal{P}(P)$ such that $p \le q$, and $\pi^* = (z_i \to z_{i+1})_{i \le n}: p^* \to^{\mathrm{lf}} q^*$ a cycle-free path on $\mathcal{P}(P)$. Then for all $i \notin \{0, n+1\}$, $z_i \ne \top^*$.

*Proof.* First, let us remark that if $p^*$ or $q^*$ equals $\top^*$ then the cycle-free properties conclude the proof. Now let us suppose a path $\pi^* = (z_i \to z_{i+1})_{i \le n}: p^* \to^{\mathrm{lf}} q^*$ that contains no trivial loops such that there exists $0 < j \le n$, $z_j = \top^* \in \pi^*$. Thus, by definition for all $i \ne j$, $z_i \ne \top^*$. Furthermore, by definition of the reduction relation for all $i \in I$, $z_i = x_i^*$. Then splitting as such

$$\pi^* = \underbrace{(x_i^* \to x_{i+1}^*)_{j \le i \le n}: \perp^* \to^{\mathrm{lf}} q^*}_{\mu^*} \circ \underbrace{(x_i^* \to x_{i+1}^*)_{i \le j}: p^* \to^{\mathrm{lf}} \top^*}_{\nu^*}$$

and applying the Definition 4.2.13 to $\mu^*$ and $\nu^*$, we get
• $\nu = (x_i \to x_{i+1})_{i \le j} : p \to^{\text{lf}} \top$

• $\mu = (x_i \to x_{i+1})_{j \le i \le n} : \bot \to^{\text{lf}} q$

• $\sigma : p \to^{\text{lf}} q$ (by Proposition 4.1.33 as $p \le q$)

Let $a$ (resp. $b$) the greatest (resp. smallest) element such that there exists a path from $a$ to $p$ and $a \in \mu$ (resp. from $q$ to $b$ and $b \in \mu$). These exist as we have no loops. We get the following

<figure><img src="image_160.png" /></figure>

By definition, for $P \in \mathbf{Prcs}$ the positions $a$ and $p$ (resp. $b$ and $q$) are the start (resp. end) of a conditional branching. Furthermore, by definition of $a$, (resp. $b$), $a$ and $q$ (resp. $b$ and $p$) are the start and end of the same branching. Hence, we have an inner branching that was opened (at $p$) inside an outer branching (opened at $a$) but closed after that the containing branching was closed. This is impossible by construction of the set of positions. $\square$

### 4.2.1.3 Path-based cubes for preorders

Now, we can finally introduce our new notion of cubes as set of paths without non-trivial loops. Although a great deal of effort was made to reach a satisfying definition, we still need to extend our definition of cubes to consider *composite cubes*. Indeed, even with all our efforts, there are simply too many different cubes in the unfolding to be able to project them all via their endpoints. Composite cubes (and some adjustment to the projection of cubes) are necessary in our model in order to ensure that cubes and their support are projected to the same support, as detailed in Example 4.2.17.

**Definition 4.2.15.** Let $(\mathcal{P}, \le)$ a finite preorder. Let $\mathcal{S} \subseteq \mathcal{P}$.

• We call *simple cube* of $\mathcal{P}$ any non-empty subsets of all paths on $\mathcal{P}$ of the following form $(p, q) = \{\pi \mid \pi : p \to^{\text{lf}} q$ with $p, q \in \mathcal{P}\}$

• For any two cubes $(p, q)$ and $(q, r)$ we call *composite cubes* $(p, q, r) = \{\mu \cdot \nu \mid \nu, \mu \in (p, q) \times (q, r)\}$.

The support $[p, q]$ of the cube $(p, q)$ is defined as

$$[p, q] = \bigcup_{\pi \in (p, q)} [\pi]$$

We write $\mathcal{C}(\mathcal{S})$ the set of all cubes of $\mathcal{P}$ whose support is included in $\mathcal{S}$.

When considering programs, more precisely a looping process $P \in \mathbf{Prcs}^*$ (Definition 4.1.19), we will impose a last restriction on its cubes. For composite cubes, we will only allow composition of cubes of the form $(p, \bot^*)$ and $(\top^*, r)$.
**Definition 4.2.16.** Given a looped process $P \in \mathbf{Prcs}^*$, the cubes of P, written $C(P)$ are a subset of the cubes of the poset $C(\mathcal{P}(P))$ containing only cubes of the form:

$$ \bullet \quad (p, q) = \{\pi \mid \pi : p \to^{\mathrm{lf}} q\} \text{ or} $$

$$ \bullet \quad (p, \perp^*, q) = (p, \top^*, q) = \{\pi \mid \pi = \mu \circ \sigma, \sigma : p \to^{\mathrm{lf}} \top^*, \mu : \perp^* \to^{\mathrm{lf}} q\} $$

with $p, q \in \mathcal{P}(P)$.

*Example 4.2.17.* Let us consider the program $P = (\mathbf{skip} + \mathbf{skip})^*$ and its unfolding $\mathcal{U}(P) = (\mathbf{skip} + \mathbf{skip}); (\mathbf{skip} + \mathbf{skip})$. We need to differentiate between the projections of the two cubes

$$ c = ((\perp + \emptyset); \perp, \top; (\top + \emptyset)) \qquad c' = ((\perp + \emptyset); \perp, (\top + \emptyset); \perp) $$

given in grey below, as they should correspond to the lifting of two different cubes, but with the same endpoints.

<figure><img src="image_161.png" /></figure>

Then $\Phi([c])$ is covered by $((\perp + \emptyset)^*, \perp^*, (\top + \emptyset)^*)$ and $\Phi([c'])$ is covered by $((\perp + \emptyset)^*, (\top + \emptyset)^*)$.

<figure><img src="image_162.png" /></figure>

*Remark 4.2.18.* In Example 4.2.17, one could find a non-composite cube that covers the loop for instance $(\perp^*, (\top + \emptyset)^*)$, but then, it would no longer be obtained as a projection by $\Phi \times \Phi$. Furthermore, the maximal cubes of such a region would be too numerous (three in this case).

*Remark 4.2.19.* Any composition of more than two cubes is by our restriction equivalent to a composition of only two. Indeed, the composition $(p, q) \cdot (q, r) \cdot (r, s)$ implies $q = r = \top^*$. Then $(q, r)$ is the set containing only the trivial paths, such that $(p, q) \cdot (q, r) \cdot (r, s) = (p, \top^*, s)$.

Thankfully most of the composite cubes are actually equivalent to simple cubes as shown in the following Lemma 4.2.20. The actual composite cubes will those of the considered in Example 4.2.17 as well as the cube $(\perp, \top^*, \top)$.
**Lemma 4.2.20.** Let $P \in \mathbf{Prcs}$, let $p, q \in \mathcal{P}(P)$. Then

1. $(\perp, \top^*, q^*) = (\perp, q^*)$

2. $(p^*, \top^*, \top) = (p^*, \top)$

3. $p \leq q$ implies $(p^*, q^*) = (p^*, \top^*, q^*)$

*Proof.* Let $P \in \mathbf{Prcs}$, $p, q \in \mathcal{P}(P)$ such that $p \leq q$

1. Let us prove $(\perp, \top^*, q^*) = (\perp, q^*)$

$P^* \models \perp \rightarrow \perp^*$ is the only reduction possible from $\perp$. Thus, any path $\pi: \perp \rightarrow^{\text{lf}} p^*$ is in fact a path $\pi: \perp \rightarrow^{\text{lf}} \perp^* \rightarrow^{\text{lf}} p^*$ and conversely.

2. Symmetrically, $(p^*, \top^*, \top) = (p^*, \top)$

3. Now let us prove $(p^*, q^*) = (p^*, \top^*) \times (\perp^*, q^*)$.

* Let $\pi^* \in (p^*, q^*)$. Trivially $\pi^* = (z_i^* \rightarrow z_{i+1}^*)_{i \in I}$. Then if $\top^* \notin \pi$, by induction rules, this implies $\pi = (z_i \rightarrow z_{i+1}z)_{i \in I}$ is in fact a path from $p$ to $q$. By Remark 4.2.26 this implies $p \leq q$, which is excluded. Thus, $\top^* \in \pi$, such that $\pi: p^* \rightarrow^{\text{lf}} \top^* \rightarrow q^*$ i.e.

$$ (p^*, q^*) \subseteq (p^*, \top^*) \times (\perp^*, q^*) $$

* Now let us suppose $\sigma \cdot \mu \in (p^*, \top^*) \times (\perp^*, q^*)$. Then if $\sigma \cdot \mu$ contains a non-trivial loop on a point $x^*$ (which by definition must be distinct from $\top^*$), this implies $\mu: p^* \rightarrow^{\text{lf}} x^* \rightarrow^{\text{lf}} \top^*$ and $\sigma: \perp^* \rightarrow^{\text{lf}} x^* \rightarrow^{\text{lf}} q^*$. By the same argument as above, this implies $p \leq x \leq q$, which contradicts our hypothesis. Thus

$$ (p^*, \top^*) \times (\perp^*, q^*) \subseteq (p^*, q^*) $$

□

Now we can also define the cube for the parallel composition of processes. This cannot be defined directly in the same manner as for single processes if we hope to achieve consistent result with regard to unfolding as show in Example 4.2.22 below.

**Definition 4.2.21.** Given a program $P \parallel Q \in \mathbf{Pgrm}$, we define the cubes of $P$ as the product of the cubes of $P$ and $Q$.

$$ \mathcal{C}(P \parallel Q) = \mathcal{C}(P) \times \mathcal{C}(Q) $$

The support of such cube $c \times d \in \mathcal{C}(O \parallel Q)$ is then defined as

$$ [c \times d] = \{p \parallel q \mid p \in [c], q \in [d]\} = [c] \times [d] $$

*Example 4.2.22.* Let us consider the program $P = \mathbf{skip} \parallel (\mathbf{skip}; \mathbf{skip})$, and particularly the cube $c = (\perp \parallel \perp^*, \top \parallel \perp; \perp^*)$

On the left we can see the support of $c$ if we kept the same definition for cubes of parallel processes, and on the right, the support of $c$ with the new definition.
<figure><img src="image_163.png" /></figure>

The loops combined with parallel composition, makes it very hard to restrain the paths that can be taken, leading to the huge supports on the right. This would pose a problem, as all cube of the form $(\perp \parallel p^*, \top \parallel q^*)$ would automatically cover all the loop.

*Remark 4.2.23.* By definition of $\Phi$ and Definition 4.2.21, $\Phi([x] \times [y]) = \Phi([x]) \times \Phi([y])$

*Remark 4.2.24.* If $P$ has no loop, this definition coincides with our previous definition of cubes.

**Proposition 4.2.25.** Let $P \in \mathbf{Prcs}^*$. Let $x, y \in \mathcal{P}(P)$, then $x \le_P y \iff (x, y) \neq \emptyset$ and $(x, \top^*, y) \neq \emptyset$.

*Proof.* First let us remark that there exists a finite path $\pi \models x \to^* y$ if and only if there exists a path $\pi': x \to^{\text{lf}} y$ without non-trivial loops. Indeed, any finite number of loops can be added or removed to the path without changing the fact that it is a path from $x$ to $y$. To do this, replace any loop $\sigma \models p \to^* p \subseteq \pi$ by the trivial loop $\epsilon_p$. Then $(x, y) \neq \emptyset$ if and only if there exists $\pi: x \to^{\text{lf}} y$. By Proposition 4.1.33 and the remark above this is equivalent to $x \le y$. $\square$

*Remark 4.2.26.* For $P \in \mathbf{Prcs}$, $\mathcal{C}(P) = \{(p, q) \mid p, q \in \mathcal{P}(P), p \le q\}$ and correspond to the cubes defined in Chapter 3. Furthermore, a path $\pi = (z_i \to z_{i+1})_{i \le n}: p \to^{\text{lf}} q$ is a strictly increasing sequence $p = z_0 < z_1 < \cdots < z_{n+1} = q$ of positions of $P$.

*Example 4.2.27.* Let $x \in \mathcal{P}(P^*)$ then

• $(x, x) = \{\epsilon_x\}$ and $[x, x] = \{x\}$

• $(\perp, \top)$ is the sets of all paths from $\perp$ to $\top$ and $[\perp, \top] = \mathcal{P}$

#### 4.2.1.4 Order on cubes

As we have changed our definition of cubes, we will also be required to change how we consider the inclusion of such cubes. But in doing so we must ensure that it is coherent with Definition 3.2.4, at the very least, if $i$ is a cube included in $j$, the support of $i$ should be in $j$.

**Definition 4.2.28.** Given a preorder $\mathcal{P}$ and two cubes $i, j \in \mathcal{C}(\mathcal{P})$, we define the relation $\subseteq$ on cubes as follows:

$$i \subseteq j \iff \forall \pi \in i \text{ there exists } \sigma, \mu \text{ such that } \sigma \circ \pi \circ \mu \in j$$

**Proposition 4.2.29.** $(\mathcal{C}(\mathcal{P}), \subseteq)$ is a partial order.
*Proof.* Let $(p, q) \subseteq (s, t) \subseteq (x, y)$ be three cubes of a program $P$.

* Reflexivity: Let $\pi \in (p, q)$, then taking $\epsilon_p$ (resp. $\epsilon_q$) the trivial loop on $p$ (resp. $q$), we have, $\epsilon_q \cdot \pi \cdot \epsilon_p : p \xrightarrow{\text{lf}} q$ i.e. $(p, q) \subseteq (p, q)$.

* Transitivity. Let us suppose $(p, q) \subseteq (s, t) \subseteq (x, y)$. Let $\pi: p \xrightarrow{\text{lf}} q$. Then $(p, q) \subseteq (s, t)$ implies the existence of $\mu, \nu$ such that $\mu \cdot \pi \cdot \nu : s \xrightarrow{\text{lf}} t$. Then $(s, t) \subseteq (x, y)$ implies the existence of $\mu', \nu'$ such that $\mu' \cdot (\mu \cdot \pi \cdot \nu) \cdot \nu' : x \xrightarrow{\text{lf}} y$. This implies $(\mu' \cdot \mu) \cdot \pi \cdot (\nu \cdot \nu') : x \xrightarrow{\text{lf}} y$, i.e. $(p, q) \subseteq (x, y)$

* Anti-symmetry. Let us suppose $(p, q) \subseteq (x, y) \subseteq (p, q)$. Let $\pi: p \xrightarrow{\text{lf}} q$. Then there exists $\mu, \nu, \mu', \nu'$ such that $(\mu' \cdot \mu) \cdot \pi \cdot (\nu \cdot \nu') : p \xrightarrow{\text{lf}} q$. Thus, $\mu' \cdot \mu : q \xrightarrow{\text{lf}} q$ (resp. $\nu \cdot \nu' : p \xrightarrow{\text{lf}} p$) implies $\mu' \cdot \mu = \epsilon_q$ (resp. $\nu \cdot \nu' = \epsilon_p$), such that $\mu = \mu' = \epsilon_y = \epsilon_q$ (resp. $\nu = \nu' = \epsilon_x = \epsilon_p$) i.e. $(p, q) = (x, y)$ □

**Corollary 4.2.30.** Let $i, j \in \mathcal{C}(\mathcal{P})$, $i \subseteq j$ implies $[i] \subseteq [j]$.

**Definition 4.2.31.** Let $\mathcal{P}$ a preorder, we say that a cube $i$ is maximal if it is maximal for the inclusion i.e. $\forall j \in \mathcal{C}(\mathcal{P}), i \not\subseteq j$. Given $X \subseteq \mathcal{P}$, we write $C^{\max}(R)$ for the set of maximal cubes of $X$.

### 4.2.2 Characterizing cubes of the unfolding

Now that we have a satisfying definition of cubes, we can proceed to define the projection $\Psi$ sending the cubes of the unfolding, onto cubes of the base program. We will first address the case of the unfolding of a single loop $P^*$.

As we have seen before in Example 4.2.17, we could not simply define cubes as elements of $\mathcal{P}(P^*) \times \mathcal{P}(P^*)$, introducing the need for composite cubes. We will need to decide when a cube $(x, y)$ of $\mathcal{U}(P)$ should be sent to a simple cube $(\Phi(x), \Phi(y))$ and when it should be sent to a composite cube $(\Phi(x), \top^*, \Phi(y))$ instead.

Of course this projection should satisfy some elementary properties, namely, that the support of a cube $\Psi(c)$ should be equal to the image of its support $\Phi[c]$ (Proposition 4.2.44).

As shown below on the unfolding of $P = (\text{skip} + \text{skip})^*$, most of the cubes of $\mathcal{U}(P) = (\text{skip} + \text{skip}); (\text{skip} + \text{skip})$ do project onto cubes of $P$ via $\Phi \times \Phi$.

The following singletons all project naturally onto cubes of $P^*$

<figure><img src="image_164.png" /></figure>
Then, cubes starting at one of the extremities and ending before $\top;\bot$ are sent to cubes starting at one extremity and ending in the loop. It is important that the cubes end before $\top;\bot$ as otherwise, the support would no longer coincide

<figure><img src="image_165.png" /></figure>

The last type of cubes that are sent via $\Phi \times \Phi$ to simple cubes are the cubes in a single iteration of a loop. These cubes are image of cubes whose endpoints are strictly between $\bot;\bot$ and $\top;\bot$ or strictly between $\top;\bot$ and $\top;\top$.

<figure><img src="image_166.png" /></figure>

As suggested by Example 4.2.17 the cubes of the form $(p;\bot, \top;q)$, where $p \le q$, need to be projected onto composite cube, i.e. to a cube of the form $\Phi(p;\bot) \times \top^* \times \Phi(\top;q)$. When $p \not\le q$, the composite cube is actually a simple cube (in grey in the figures below) by Lemma 4.2.20. Nonetheless, we will regroup both of these types of cubes going forward as they share many properties.

<figure><img src="image_167.png" /></figure>
Some cubes do not have a satisfying way of projecting them, even when considering composite cubes. In the figure below we show such a cube, drawn with the dashed line. Even if we project it on a composite cube, it doesn't cover the projection of its support.

<figure><img src="image_168.png" /></figure>

We could change once more our definition to take these into account, but this is unnecessary in our context. These cubes all verify the property that they cover more than a copy of the content of the loop in the unfolding. As we are studying conservative programs, and more precisely maximal covers of the forbidden/authorized regions, we can safely restrict our projection to ignore those cubes without losing anything.

Indeed, by conservativity, the consumption of the loop is null (Proposition 4.1.30). Thus, if the forbidden region covers more than a copy of a loop in the unfolding, this means that it covers the whole program as $\Phi$ and $\Phi^{-1}$ preserves the consumption of positions.

Thus, we make the choice to not project these cubes, which we can do without loss of generality for the study of programs, and will prove formally in Proposition 4.3.25 that they disappear as we consider maximal covers later on.

We now characterize all cubes of $P^*$ and its unfolding $\mathcal{U}(P^*)$. In a first time it allows us to differentiate between cubes that should be sent by $\Psi$ to simple cubes and those that should be sent to composite cubes. It will also prove useful for the various proofs later on, as each of the different subsets have their own unique quirks.

**Proposition 4.2.32.** Let $P \in \mathbf{Prcs}^*$, then $\mathcal{C}(P^*) = \coprod_{i \in [-1,5]} \mathcal{L}_i$ where the $\mathcal{L}_i$ are defined below

$$ \mathcal{L}_{-1} = \{(\perp, \top^*, \top)\} $$

$$ \mathcal{L}_2 = \{(\perp, p^*) | p \in \mathcal{P}(P) \setminus \{\top\}\} $$

$$ \mathcal{L}_0 = \{(\perp, \perp), (\top, \top), (\top^*, \top^*)\} $$

$$ \mathcal{L}_3 = \{(p^*, \top) | p \in \mathcal{P}(P) \setminus \{\perp\}\} $$

$$ \mathcal{L}_1 = \{(\perp, \top)\} $$

$$ \mathcal{L}_4 = \{(p^*, \top^*, q^*) | p, q \in \mathcal{P}(P) \setminus \{\top, \perp\}\} $$

$$ \mathcal{L}_5 = \{(p^*, q^*) | p \le q, (p, q) \notin \{(\perp, \perp), (\top, \top), (\top, \top)\}\} $$

*Proof.* Given a program $P \in \mathbf{Prcs}$ the positions of $P^*$ can be separated into the following disjoint sets:

$$ \mathcal{P}(P^*) = \underbrace{\{\perp\}}_{=S_1} \coprod \underbrace{\{\top^*\}}_{=S_2} \coprod \underbrace{\{p^* | p \in \mathcal{P}(P) \setminus \{\perp, \top\}\}}_{=S_3} \coprod \underbrace{\{\top\}}_{=S_4} $$
We define

$$S_i^j = \{(x, y) \mid x \in S_i, y \in S_j, x \le y\} \text{ and } L_i^j = \{(x, \top^*, y) \mid x \in S_i, y \in S_j, x \le y\}$$

By Proposition 4.2.25 and Definition 4.2.16, we know that

$$\mathcal{C}(P^*) = \{(p, q) \in \mathcal{P}(P^*) \mid p \le q\} \cup \{(p, \top^*, q) \in \mathcal{P}(P^*) \mid p \le \top^* \le q\}$$

Then by Definition 3.1.23 we have $\perp < p < \top$ and $\perp < q < \top$ for all $p, q \notin \{\perp, \top\}$ such that

$$\mathcal{C}(P^*) = S \cup L$$

where

$$S = \left( \coprod_{i \in [1,4]} S_1^i \right) \coprod \left( \coprod_{i \in [2,4]} S_2^i \right) \coprod \left( \coprod_{i \in [2,4]} S_3^i \right) \coprod S_4^4 \\ L = \left( \coprod_{i \in [2,4]} L_1^i \right) \coprod \left( \coprod_{i \in [2,4]} L_2^i \right) \coprod \left( \coprod_{i \in [2,4]} L_3^i \right)$$

This makes a lot of cubes to check, we will first proceed by reducing the number of sets to check by remarking that by Lemma 4.2.20, all $L_i^j = S_i^j$ except for $L_3^3$ and $L_1^4$, i.e.

$$\mathcal{C}(P^*) = S \cup L_3^3 \cup L_1^4$$

Now we separate $S_3^3 = \{(p^*, q^*) \mid p, q \notin \{\perp, \top\}\}$ and $L_3^3 = \{(p^*, \top^*, q^*) \mid p, q \notin \{\perp, \top\}\}$ in the following sets

$$S_3^{3\le} = \{(p^*, q^*) \mid \perp < p \le q < \top\} \qquad S_3^{3\ge} = \{(p^*, q^*) \mid p, q \notin \{\perp, \top\}, p \le q\} \\ L_3^{3\le} = \{(p^*, \top^*, q^*) \mid \perp < p \le q < \top\} \qquad L_3^{3\ge} = \{(p^*, \top^*, q^*) \mid p, q \notin \{\perp, \top\}, p \ge q\}$$

Such that

$$S_3^3 = S_3^{3\le} \coprod S_3^{3\ge} \qquad L_3^3 = L_3^{3\le} \coprod L_3^{3\ge}$$

By Lemma 4.2.20 $L_3^{3\ge} = S_3^{3\le}$. And by Lemma 4.2.14, every element of $L_3^{3\le}$ contains a loop, which implies that $S \cap L_3^{3\le} = \emptyset$. Furthermore, by comparing the supports of their only cube, $L_1^4 \cap S_1^4 = \emptyset$. Thus, we can reduce $\mathcal{C}(P^*)$ to the disjoint union of the three following sets:

$$\mathcal{C}(P^*) = S \coprod L_3^{3\le} \coprod L_1^4 \qquad (4.2)$$

By reorganizing the cubes, we get back all the $\mathcal{L}_i$, $i \in [-1:8] \setminus \{6\}$.

* $L_1^4 = \mathcal{L}_{-1}$

* $S_1^1 \cup S_4^4 \cup S_2^2 = \{(\perp, \perp), (\top, \top), (\perp^*, \perp^*)\} = \mathcal{L}_0$

* $S_1^4 = \{(\perp, \top)\} = \mathcal{L}_1$
• $S_1^2 \cup S_1^3 = \mathcal{L}_2$. Indeed,

$$
\begin{align*}
S_1^2 \cup S_1^3 &= \{(\perp, \top^*)\} \cup \{(\perp, p^*) \mid p \in \mathcal{P}(P) \setminus \{\perp, \top\}\} \\
&= \{(\perp, p^*) \mid p \in \mathcal{P}(P) \setminus \{\top\}\}
\end{align*}
$$

• Similarly $S_2^4 \amalg S_3^4 = \{(p^*, \top) \mid p \in \mathcal{P}(P) \setminus \{\bot\}\} = \mathcal{L}_3$

• $L_3^{3\le} \cup S_3^{3\le} = \mathcal{L}_4$

• As $\perp \le p \le \top$ for all $p \in \mathcal{P}(P)$ we have

$$
\begin{align*}
S_2^3 \cup S_3^2 \cup S_3^{3\le} &= \{(p^*, \top^*) \mid p \in \mathcal{P}(P) \setminus \{\perp, \top\}\} \\
&\quad \cup \{(p^*, q^*) \mid \perp < p \le q < \top\} \cup \{(\perp^*, q^*) \mid q \in \mathcal{P}(P) \setminus \{\perp, \top\}\} \\
&= \{(p^*, q^*) \mid (p, q) \notin \{\perp, \top\}^2, p \le q\} \\
S_2^3 \cup S_3^2 \cup S_3^{3\le} &= \mathcal{L}_5
\end{align*}
$$

By combining everything in Eq. (4.2), we get $\mathcal{C}(P^*) = \coprod_{i \in [-1,6]} \mathcal{L}_i$ $\square$

**Proposition 4.2.33.** Given a program *P*, then the non-empty cubes of *P*; *P*, can be split
in the following way: $\mathcal{C}(P;P) = \coprod_{i \in [-1,6]} \mathcal{C}_i$ where the $\mathcal{C}_i$ are defined below

$$
\begin{align*}
C_{-1} &= \{(\perp, \top; p) \mid p \in \mathcal{P}(P)\} \cup \{(p; \perp, \top) \mid p \in \mathcal{P}(P)\} \\
&\quad \cup \{(\perp; \perp, \top; \perp), (\top; \perp, \top; \top), (\perp; \perp, \top; \top)\} \\
C_0 &= \{(\perp, \perp), (\top, \top), (\top; \perp, \top; \perp), (\perp; \perp, \perp; \perp), (\top; \top, \top; \top)\}
\end{align*}
$$

$$
\begin{align*}
C_1 &= \{(\perp, \top)\} & C_4 &= \{(p; \perp, \top; q) \mid p, q \in \mathcal{P}(P) \setminus \{\perp, \top\}\} \\
C_2 &= \{(\perp, p; \perp) \mid p \in \mathcal{P}(P) \setminus \{\top\}\} & C_5 &= \{(p; \perp, q; \perp) \mid p \times q \notin \{\perp, \top\}^2, p \le q\} \\
C_3 &= \{(\top; p; \top) \mid p \in \mathcal{P}(P) \setminus \{\perp\}\} & C_6 &= \{(\top; p; \top; q) \mid p \times q \notin \{\perp, \top\}^2, p \le q\}
\end{align*}
$$

*Proof.* Given a program *P*, we define the sets

$$
\begin{array}{llll}
S_1 = \{\bot\} & S_2 = \{\bot; \bot\} & S_3 = \{p; \bot \mid p \in \mathcal{P}(P) \setminus \{\bot, \top\}\} & S_4 = \{\top; \bot\} \\
S_7 = \{\top\} & S_6 = \{\top; \top\} & S_5 = \{\top; p \mid p \in \mathcal{P}(P) \setminus \{\bot, \top\}\}
\end{array}
$$

Such that

$$
\mathcal{P}(P;P) = \coprod_{i \in [1:7]} S_i
$$

We define $S_i^j = \{(x, y) \mid x \in S_i, y \in S_j, x \le y\}$. By Proposition 4.2.25,

$$
\mathcal{C}(P;P) = \{(p,q) \in \mathcal{P}(P;P) \mid p \le q\}
$$

Then by definition of the order on position (Definition 3.1.23)

$$
\mathcal{C}(P;P) = \coprod_{i \le j} S_i^j
$$
* $C_{-1} = (S_1^4 \cup S_1^5 \cup S_1^6) \cup (S_2^7 \cup S_3^7 \cup S_4^7) \cup (S_2^4 \cup S_2^6 \cup S_4^6)$. Indeed,
  - $S_2^4 \cup S_2^6 \cup S_4^6 = \{(\perp; \perp; \top; \perp), (\perp; \perp; \top; \top), (\top; \perp; \top; \top)\}$
  - $S_1^4 \cup S_1^5 \cup S_1^6 = \{(\perp; \top; q) | q \in \mathcal{P}(P)\}$
  - $S_2^7 \cup S_3^7 \cup S_4^7 = \{(p; \perp, \top) | p \in \mathcal{P}(P)\}$

* $C_0 = S_1^1 \cup S_1^7 \cup S_2^2 \cup S_4^4 \cup S_6^6$

* $C_1 = S_1^7$

* $C_2 = S_1^2 \cup S_1^3$. Indeed,

$$ 
\begin{aligned}
S_1^2 \cup S_1^3 &= \{(\perp, \perp; \perp)\} \cup \{(\perp, p; \perp) \mid p \in \mathcal{P}(P) \setminus \{\perp, \top\}\} \\
&= \{(\perp, p; \perp) \mid p \in \mathcal{P}(P) \setminus \{\top\}\}
\end{aligned}
$$

* Similarly, $C_3 = S_5^7 \cup S_6^7$.

* $C_4 = S_3^5$

* $C_5 = S_2^3 \coprod S_3^3 \coprod S_3^4$. Indeed,

$$ 
\begin{aligned}
S_2^3 \cup S_3^3 \cup S_3^4 &= \{(\perp; \perp, q; \perp) \mid q \notin \{\perp, \top\}\} \cup \{(p; \perp, q; \perp) \mid \perp < p \le q < \top\} \\
&\quad \cup \{(p; \perp, \top; \perp) \mid p \notin \{\perp, \top\}\} \\
&= \{(p; \perp, q; \perp) \mid (p, q) \notin \{(\perp, \perp), (\perp, \top), (\top, \top)\}, p \le q\}
\end{aligned}
$$

* Similarly $C_6 = S_4^5 \cup S_5^5 \cup S_5^6$

By combining everything we get $C(P;P) = \coprod_{i \in [-1,7]} C_i$

<figure><img src="image_169.png" /></figure>

Now we properly define the sets $\Pi_P \mathcal{L}_i$ (resp. $\Pi_{\mathcal{U}(P)} \mathcal{C}_i$) which are the sets of cubes of a program $P$ (resp. $\mathcal{U}(P)$) that are built inductively using cubes of $\mathcal{L}_i$ (resp. $\mathcal{C}_i$). These will come up often in proofs and lemmas using the inductive structure of our programs.

**Definition 4.2.34.** Let $P \in \mathbf{Pgrm}$. We define the subsets $\Pi_P \mathcal{L}_i$ of $C(P)$ and $\Pi_{\mathcal{U}(P)} \mathcal{C}_i$ of $\mathcal{CU}(P)$.

$$ \Pi_{\mathcal{U}(P)} \mathcal{C}_i = \begin{cases} \emptyset & \text{if } P \in \mathbf{Prcs} \\ C_i & \text{if } P = Q^* \\ (\mathcal{C}(S) \times \Pi_{\mathcal{U}(T)} \mathcal{C}_i) \cup (\Pi_{\mathcal{U}(S)} \mathcal{C}_i \times \mathcal{C}(T)) & \text{if } P = S \| T \end{cases} $$

$$ \Pi_P \mathcal{L}_i = \begin{cases} \emptyset & \text{if } P \in \mathbf{Prcs} \\ \mathcal{L}_i & \text{if } P = Q^* \\ (\mathcal{C}(S) \times \Pi_T \mathcal{L}_i) \cup (\Pi_S \mathcal{L}_i \times \mathcal{C}(T)) & \text{if } P = S \| T \end{cases} $$
As previously stated, the cubes of $C_{-1} \cap \mathcal{C}(\mathcal{U}(P))$ do not project properly onto cubes of $P$, and cubes of $\mathcal{L}_{-1}$ cannot be the image of a cube of $\mathcal{U}(P)$. Thus, they will be excluded for now, and later on, we will justify this choice.

**Definition 4.2.35.** Let $P \in \mathbf{Prcs}$, we define

$$ \begin{array}{rcl} \Psi_{P^*}: \mathcal{C}(P;P) \setminus C_{-1} & \to & \mathcal{C}(P^*) \setminus \mathcal{L}_{-1} \\ (p,q) & \mapsto & \begin{cases} (\Phi(p), \top^*, \Phi(q)) & \text{if } (p,q) \in C_4 \\ (\Phi(p), \Phi(q)) & \text{otherwise} \end{cases} \\ \Psi_P: \mathcal{C}(P) \setminus \Pi_{\mathcal{U}(P)} C_{-1} & \to & \mathcal{C}(P) \setminus \Pi_P \mathcal{L}_{-1} \\ p & \mapsto & p \end{array} $$

Suppose $P = S \parallel T \in \mathbf{Pgrm}$

$$ \Psi_{S \parallel T}: \mathcal{C}(\mathcal{U}(S \parallel T)) \setminus \Pi_{\mathcal{U}(P)} C_{-1} \to \mathcal{C}(S \parallel T) \setminus \Pi_P \mathcal{L}_{-1} \\ s \times t \mapsto \Psi_S(s) \times \Psi_T(t) $$

By removing the sets $C_{-1}$ (already proven to not have an effect) and $\mathcal{L}_{-1}$, $\Psi$ becomes surjective, and we can further restrain the surjection to be compatible with our partition of $\mathcal{C}(P^*)$ and $\mathcal{C}(\mathcal{U}(P^*))$.

**Proposition 4.2.36.** Let $P \in \mathbf{Prcs}^*$. $\Psi_{P^*}$ is surjective. More precisely,

* $\Psi_{P^*}: C_i \to \mathcal{L}_i$ is a bijection for $i \in [1, 5] \setminus 6$.

* $\Psi_{P^*}: C_6 \to \mathcal{L}_5$ is bijective.

* $\Psi_{P^*}: C_0 \to \mathcal{L}_0$ is surjective.

*Proof.* Let $P \in \mathbf{Prcs}^*$. Let $p, q \in \mathcal{P}(P)$

* $\Psi_{P^*}: C_0 \to \mathcal{L}_0$ is trivially surjective.

* $\Psi_{P^*}: C_1 \to \mathcal{L}_1$ is trivially bijective.

* $\Psi_{P^*}: C_4 \to \mathcal{L}_4$. First let us remark that

$$ p^* = q^* \text{ implies } p = q \text{ or } p, q \in \{\bot, \top\} \qquad (4.3) $$

- Surjectivity: Let $c \in \mathcal{L}_4$, such that $c = (p^*, \top^*, q^*)$, $p, q \notin \{\bot, \top\}$. Then $(p; \bot, \top; q) \in \mathcal{C}_4$ and

$$ \Psi(p; \bot, \top; q) = (\Phi(p; \bot), \top^*, \Phi(\top; q)) = (p^*, \top^*, q^*) = c $$

With $(p; \bot, \top; q) \neq \emptyset$ by the inference rules. Thus, $\Psi_{P^*}: C_4 \to \mathcal{L}_4$ surjective

- Injectivity: Let $c, d \in \mathcal{L}_4$ such that $c = (p; \bot, \top; q)$, $d = (x; \bot, \top; y)$ with $p, q, x, y \notin \{\bot, \top\}$. Now let us suppose $\Psi(c) = \Psi(d)$.

$$ \begin{align} \Psi(c) = \Psi(d) &\implies (p^*, \top^*, q^*) = (x^*, \top^*, y^*) \nonumber \\ &\implies p^* = x^*, q^* = y^* \nonumber \\ &\implies p = x, q = y \tag{4.3} \end{align} $$

$$ \Psi(c) = \Psi(d) \implies c = d $$

Thus $\Psi_{P^*}: C_4 \to \mathcal{L}_4$ injective.
• $\Psi_{P^*}: C_2 \to \mathcal{L}_2$ and $\Psi_{P^*}: C_3 \to \mathcal{L}_3$ follow the same proof.

• $\Psi_{P^*}: C_5 \to \mathcal{L}_5$.

- Surjectivity: Let $c \in \mathcal{L}_5$, such that $c = (p^*, q^*)$, such that $p \le q$ with $p, q \ne \bot, \top$. Then $(p; \bot, q; \bot) \in \mathcal{C}_4$ and

$$ \Psi(p; \bot, q; \bot) = (\Phi(p; \bot), \Phi(q; \bot)) = (p^*, q^*) = c $$

With $(p; \bot, q; \bot) \ne \emptyset$ by the inference rules. Thus, $\Psi_{P^*}: C_5 \to \mathcal{L}_5$ surjective

- Injectivity: Let $c, d \in \mathcal{L}_5$ such that $c = (p; \bot, \top; q)$, $d = (x; \bot, q; \bot)$ with $(p, q), (x, y) \notin \{(\bot, \top), (\bot, \bot), (\top, \top)\}$. Now let us suppose $\Psi(c) = \Psi(d)$.

$$ \begin{align} \Psi(c) = \Psi(d) &\implies (p^*, q^*) = (x^*, y^*) \nonumber \\ &\implies p^* = x^*, q^* = y^* \nonumber \\ &\implies p = x, q = y \tag{4.3} \end{align} $$

Thus $\Psi_{P^*}: C_5 \to \mathcal{L}_5$ injective.

• $\Psi_{P^*}: C_6 \to \mathcal{L}_5$ follows the same proof as previous case, using the fact that $\Phi(p; \bot) = \Phi(\top; p)$ for all $p \in \mathcal{P}(P)$.

□

**Definition 4.2.37.** Given $P \in \mathbf{Pgrm}$, we define the equivalence relation $\approx_P$ on cubes of $\mathcal{U}(P)$, such that for all cubes $c, d \in \mathcal{C}(P)$,

$$ c \approx_P d \iff \Psi_P(c) = \Psi_P(d) $$

In that case, we say that $c, d$ are *unfold-equivalent*.

*Example 4.2.38.* Let us consider the program $P = (\mathbf{skip}+\mathbf{skip})^*$. Below are given the semantics of its unfolding $\mathcal{U}(P)$ and of $P$ respectively on the left and the right. The two cubes $R_1$ and $R_2$ are equivalent, as they project on the same cube of $P$

<figure><img src="image_170.png" /></figure>

The example above is actually the only case of equivalent cubes for a simple loop. This implies that two cubes are equivalent if and only if they are both in the lifting of a cube of the base program as we would expect (counting the singleton cube $(\bot^*, \bot^*)$)
Remark 4.2.39. As a follow-up of the previous remark, proved in Proposition 4.2.40 below, we have that $\Psi$ is a discrete fibration, i.e. the antecedents of a cube by $\Psi$ are either equal or their support is disjoint.

**Proposition 4.2.40.** Given a program $P \in \mathbf{Pgrm}$, and two cubes $c, c' \in \mathcal{C}(\mathcal{U}(P))$, we have

$$c \approx c', c \neq c' \implies [c] \cap [c'] = \emptyset$$

*Proof.* By induction on $P$.

* $P \in \mathbf{Prcs}$. Nothing to do as $\Psi$ is the identity on programs without loops.

* $P = S \parallel T$. Then $d \in \mathcal{C}(P)$ implies $d = d_1 \times d_2$. Let

$$c = c_1 \times c_2 \in \Psi^{-1}(d_1) \times \Psi^{-1}(d_2)$$

$$c' = c'_1 \times c'_2 \in \Psi^{-1}(d_1) \times \Psi^{-1}(d_2)$$

such that $c \neq c'$. By definition of the support of parallel, this implies that

$$c_1 \neq c'_1 \text{ or } c_2 \neq c'_2$$

Let us suppose $c_1 \neq c'_1$. By induction hypothesis, $[c_1] \cap [c'_1] = \emptyset$ i.e. $[c] \cap [c'] = \emptyset$. Similarly, if we suppose $c_2 \neq c'_2$, we have $[c] \cap [c'] = \emptyset$.

* $P = Q^*$. Then for all $c \in \mathcal{C}(P)$, the only cubes that have multiple antecedents by $\Phi$ are the cubes of $\mathcal{L}_5$ or $(\perp^*, \perp^*)$.

- $c = (\perp^*, \perp^*)$ implies $\Psi^{-1}(c) = \{(\perp; \perp, \perp; \perp), (\top; \perp, \top; \perp), (\top; \top, \top; \top)\}$ whose supports are all pairwise disjoint.

- $c \in \mathcal{L}_5$ and $c = (p^*, q^*) \neq (\perp^*, \top^*)$. Then

$$\Psi^{-1}(c) = \{(p; \perp, q; \perp), (\top; p, \top; q)\}$$

As $(p^*, p^*) \neq (\perp^*, \top^*)$, this implies that $p; \perp < \top; \perp < \top; q$ i.e. that the supports of the antecedents of $c$ are disjoints. $\square$

An important property that justifies our choice of projection function $\Psi$ for now is the fact that given a cube $c$ the support of its projection $\Psi(c)$ correspond to the projection by $\Phi$ of all positions in the support $c$. This suggests that we can study the forbidden and authorized region in terms of cubes instead of looking at the set of all positions. We still need to prove that the same holds for $\Psi^{-1}$ and $\Phi^{-1}$, but this is much more complicated.

**Theorem 4.2.41.** Let $P \in \mathbf{Pgrm}$, let $c \in \mathcal{C}(\mathcal{U}(P)) \setminus \Pi_{\mathcal{U}(P)}\mathcal{C}_{-1}$.

$$\Phi[c] = [\Psi(c)]$$

*Proof.* By induction on $P$

* $P \in \mathbf{Prcs}$. All functions are identities.
• $P = P_1 \parallel P_2$. $c \in C(\mathcal{U}(P)) = C(\mathcal{U}(P_1)\parallel\mathcal{U}(P_2))$ implies $c = c_1 \times c_2$. Then by Definition 4.2.21,

$$
\begin{align*}
\Phi([c]) &= \Phi([c_1 \times c_2]) \\
&= \Phi([c_1]) \times \Phi([c_2]) && \text{Remark 4.2.23} \\
&= [\Psi(c_1)] \times [\Psi(c_2)] && \text{Induction hypothesis} \\
\Phi([c]) &= [\Psi(c)]
\end{align*}
$$

• $P = S^*$. Then $\mathcal{U}(P) = S;S$, and using Proposition 4.2.33 we can separate the following cases:

- $c \in C_0$. Trivial.

- $c \in C_1$. Trivial.

- $c \in C_2$. If $x = \perp;\perp$, $\Phi([c]) = \{\perp, \perp;\perp\} = [\Psi(c)]$ and we're done. Now let us suppose $x \neq \perp$

$$
\begin{align*}
\Phi([\perp, x; \perp]) &= \Phi([\perp, \perp; \perp, x; \perp]) \\
&= \Phi(\{\perp, \perp; \perp\}) \cup \Phi([\perp; \perp, x; \perp]) \\
&= \{\perp, \perp^*\} \cup [\Psi(\perp; \perp, x; \perp)] && \text{By the case } C_5 \\
&= [\perp, \perp^*] \cup [\perp^*, x^*] \\
\Phi([c]) &= [\Psi(c)] && \text{Lemma 4.2.20}
\end{align*}
$$

- $c \in C_3$. Dual to the case $C_2$.

- $c \in C_4$. $c = (x; \perp, \top; y)$, $\perp < x, y < \top$.

$$
\begin{align*}
\Phi([x; \perp, \top; y]) &= \Phi([x; \perp, \top; \perp] \cup [\top; \perp, \top; y]) \\
&= \Phi([x; \perp, \top; \perp]) \cup \Phi([\top; \perp, \top; y]) \\
&= [\Psi(x; \perp, \top; \perp)] \cup [\Psi(\top; \perp, \top; y)] && \text{By the cases } C_5, C_6 \\
&= [x^*, \top^*] \cup [\perp^*, y^*] \\
\Phi([c]) &= [\Psi(c)]
\end{align*}
$$

- $c \in C_5$, $c = (x; \perp, y; \perp)$ Then

$$
\begin{align*}
v; \perp \in [c] &\iff \exists \pi: x; \perp \to^{\text{lf}} y; \perp, \quad v; \perp \in \pi \\
&\iff \exists \sigma: x \to^{\text{lf}} y, \quad v \in \sigma && \text{Definition 4.1.22} \\
&\iff \exists \sigma^*: x^* \to^{\text{lf}} y^*, \quad v^* \in \sigma^* && \text{Definition 4.2.13} \\
&\iff v^* \in [x^*, y^*] \\
v; \perp \in [c] &\iff \Phi(v; \perp) \in [\Psi(c)]
\end{align*}
$$

- $c \in C_6$. Similar to the previous case.

□
Now we can proceed to define the covers of a given program P. Not much change in this regard: they can still be defined as sets of cubes, and our modifications of the cubes does not affect their definitions.

The fact that we now have a finite preorder does have some implications, notably, there always exists a normal form.

### 4.2.3 Covers and normal forms

The notion of cover doesn't change from our original definitions. It is still any set of cubes; the order is still as defined in 3.2.13.

**Definition 4.2.42.** Let $\mathcal{P}$ a preorder. We define a cover on $\mathcal{P}$ as a set of cubes of $\mathcal{P}$, and we write $\mathcal{R}(\mathcal{P})$ for the set of all covers of $\mathcal{P}$. The support $[R]$ of a cover $R$ is the union of the support of its cubes i.e. $[R] = \bigcup_{r \in R} [r]$.

We can then naturally extend the definition of the projection $\Psi$ to covers of unfolded program, as well as the equality between support of the projection and projection of the support (Theorem 4.2.41).

**Definition 4.2.43.** Given a program $P \in \mathbf{Pgrm}$, we define the projection on covers of $\mathcal{U}(P)$ as follows:

$$ \Psi_P: \mathcal{R}(\mathcal{U}(P)) \to \mathcal{R}(P) \\ \{r_i \mid i \in I\} \mapsto \{\Psi(r_i) \mid i \in I\} $$

This function is only properly defined for covers $R$ such that $R \cap \Pi_{\mathcal{U}(P)}\mathcal{C}_{-1} = \emptyset$.

**Proposition 4.2.44.** Given a program $P \in \mathbf{Pgrm}$ and a cover $R \subseteq \mathcal{C}(\mathcal{U}(P)) \setminus \Pi_{\mathcal{U}(P)}\mathcal{C}_{-1}$, we have

$$ \Phi[R] = [\Psi(R)] $$

*Proof.* Given a program $P \in \mathbf{Pgrm}$ and a cover $R \subseteq \mathcal{C}(\mathcal{U}(P)) \setminus \Pi_{\mathcal{U}(P)}\mathcal{C}_{-1}$, we have, for all $c \in R$, $c \notin \Pi_{\mathcal{U}(P)}\mathcal{C}_{-1}$. Hence, $\Phi([c]) = [\Psi(c)]$ by Theorem 4.2.41. Thus

$$ \Phi[R] = \bigcup_{c \in R} \Phi([c]) = \bigcup_{c \in R} [\Psi(c)] = [\Psi(R)] $$

□

We now redefine the order on covers as in Definition 3.2.4. The definition stays the same, as the definition is only dependent on the order defined on the cubes.

As a reminder, two covers are equivalent when they describe the same support. These covers correspond to different ways of describing the same set of points. To correctly manipulate covers it is important to determine when they are equivalent and to maximize efficiency, there should be a most compact form of each region. We recall the 3.2.8 and 3.2.13 of the order on regions.

**Definition 4.2.45.** Let $R$ and $S$ be two covers of $X$. The relation $\preceq$ defined as follows is a pre-order on $\mathcal{R}(X)$

$$ R \preceq S \iff \forall R^i \in R, \exists S^j \in S, R^i \subseteq S^j $$

with $\subseteq$ defined in Definition 4.2.28
**Definition 4.2.46.** We can define a partial order $\leq$ on the covers of a partial order $X$ from the preorder $\preceq$ as follows. Given $R, S$ two covers:

$$R \leq S \iff R \preceq S \preceq R \text{ and } S \subseteq R$$

**Proposition 4.2.47.** The relation $\leq$ on covers is a partial order.

*Proof.* Cf proof of 3.2.14. □

<figure><img src="image_171.png" /></figure>

As we are dealing with finite preorders, the normal form Section 3.2.1.3 of a region is always defined. Thus, we no longer need to consider finitely complemented regions (Definition 3.2.27) or normalizable regions as in Chapter 3.

**Proposition 4.2.48.** Let $R$ be a region of a finite preorder $\mathcal{P}$. Then $R$ has a maximal cover $N(R)$ called its normal form and

$$N(R) = \mathcal{C}^{\max}(R) = \{c \in \mathcal{C}(R) \mid \forall d \in \mathcal{C}(R), c \not\in d\}$$

*Proof.* Given a finite preorder $\mathcal{P}$, the set $\mathcal{P} \times \mathcal{P}$ is also finite. This implies that its set of cubes $\mathcal{C}(\mathcal{P})$ is also finite. Thus, so is the set $\mathcal{C}(R)$. Therefore, the set $\mathcal{C}^{\max}(R)$ is correctly defined as the maximal antichain of the finite partially ordered set $\mathcal{C}(R)$. Then, by definition of $\mathcal{C}^{\max}$ as the maximal antichain, for any cover $C \subseteq \mathcal{R}(R) = \mathfrak{P}(\mathcal{C}(R))$, $C \leq \mathcal{C}^{\max}(R)$. □

<figure><img src="image_172.png" /></figure>

## 4.3 Unfolding conservative covers of loops

As previously stated, we want to show that there is a close link between cubes of the base program and cube of its 2-unfolding in order to perform the deadlock detection algorithm Algorithm 3.3.23 on the unfolding of the program. More precisely, we want to perform the three following steps.

1. We start from cubes of the forbidden region of the base program that we lift to the cubes of forbidden region of its unfolding.

2. Then, we apply Algorithm 3.3.23 on the unfolding, which gives us the deadlocks, as well as unsafe and doomed regions in terms of cubes.

3. Finally, we project these covers back to cubes of the base program.

And, at the end of the third step, we hope to recover the cubes of the unsafe/doomed regions.

In order to guarantee this, we need an equivalence between “being in the past” in the unfolding and in the base program for cubes. To prove the correctness of the method above we need the projection and the lifting by $\Psi$ to at least preserve the support of cubes.

The fact that the projection commutes with the support is already proven by Proposition 4.2.44, but proving that the lifting commutes is more complicated.

Indeed, just taking the naive lifting $\Psi^{-1}$ as the inverse image by $\Psi$ does not work on all cubes. Indeed, if we look at the cubes in Example 4.3.1, we can see that lifting cubes does not preserve their supports.
*Example 4.3.1.* Let us consider $P = (\mathbf{skip} + \mathbf{skip})^*$, whose semantics is given below. The naive lifting of the cube $(\perp, \top^*)$ does not cover the lifting of its support.

<figure><img src="image_173.png" /></figure>

We could instead define the lifting of a cube $c$ as the set $C^{\max}(\Phi^1[c])$ of all maximal cubes on the lifting of its support. While this works in theory, using it would not be usable in practice, or at least would ruin our efforts of manipulating the regions through their covers.

Instead, we will prove that by considering lifting of covers instead of lifting of cubes we can, under some restrictions that will always be validated by our conservative programs, recover the lifting property.

In this section, we then start by defining a specific subset of regions, the *conservative regions*, which include the forbidden and allowed region of conservative programs. Then, we prove in Theorem 4.3.15 that when restraining to covers of these conservative regions, the naive lifting $\Psi^{-1}$ preserves the support of the associated region. Finally, we extend this lifting property in Theorem 4.3.27 to prove that the maximal cover of the lifting is actually equal to the lifting of the maximal cover of a conservative region.

### 4.3.1 Conservative regions and covers

When considering regions of conservative programs, the forbidden (resp. authorized) region can be defined as the set of positions whose consumption is negative (resp. positive). As such, the endpoints of transition that have no effect on the consumption must both be in the same region (forbidden/authorized). We will call these transitions *pure*, and regions that respect these transitions *conservative*. Most of our results depend on the fact that the regions considered are conservative. As the results presented are aimed towards verification of programs, this is not a problem.

**Definition 4.3.2.** We say a transition is *pure* if it can be obtained inductively by the following inference rules

$$ \overline{P;Q \models \perp \rightarrow \perp; \perp} $$

$$ \overline{P^* \models \perp \rightarrow \perp^*} $$

$$ \overline{P+Q \models \perp \rightarrow \emptyset+\perp} $$

$$ \overline{P+Q \models \perp \rightarrow \perp+\emptyset} $$

$$ \overline{P;Q \models \top; \top \rightarrow \top} $$

$$ \overline{P^* \models \top^* \rightarrow \top} $$

$$ \overline{P+Q \models \emptyset+\top \rightarrow \top} $$

$$ \overline{P+Q \models \top+\emptyset \rightarrow \top} $$

$$ \frac{\alpha \neq P_a, V_a}{\alpha \models \perp \rightarrow \top} $$
$$ \frac{P \models p \rightarrow p'}{P+Q \models p+\emptyset \rightarrow p'+\emptyset} $$

$$ \frac{P \models p \rightarrow p' \quad Q \models q}{P \parallel Q \models p \parallel q \rightarrow p'; q} $$

$$ \frac{P \models \bot \rightarrow p'}{P^* \models \bot^* \rightarrow p'^*} $$

$$ \frac{Q \models q \rightarrow q'}{P+Q \models \emptyset+q \rightarrow \emptyset+q'} $$

$$ \frac{P \models p \quad Q \models q \rightarrow q'}{P \parallel Q \models p \parallel q \rightarrow p \parallel q'} $$

$$ \frac{P \models p \rightarrow \top}{P^* \models p^* \rightarrow \top^*} $$

$$ \frac{P \models p \rightarrow p'}{P; Q \models p; \bot \rightarrow p'; \bot} $$

$$ \frac{Q \models q \rightarrow q'}{P; Q \models \top; q \rightarrow \top; q'} $$

$$ \frac{P \models p \rightarrow p' \quad p, p' \notin \{\bot, \top\}}{P^* \models p^* \rightarrow p'^*} $$

**Definition 4.3.3.** Given a program $P$ and $X \subseteq \mathcal{P}(P)$, we say that $X$ is conservative when for all $x, y, z \in \mathcal{P}(P)$,

* $x \to y$ is a pure transition implies $x \in X \iff y \in X$

A cover $R$ is said to be conservative when its underlying support $[R]$ is.

*Remark 4.3.4.* The forbidden and authorized regions of a conservative programs (Definition 1.2.23) are conservative. Indeed, as pure transition do not have any effect on consumption, there is no pure transition between the forbidden region and the authorized region, which are defined by the fact that the consumption differs.

Conservative regions have a lot of useful properties. Notably they form a boolean algebra (Proposition 4.3.6). Furthermore, conservative regions, when split along each process $P_i$ of a program $P_1 \parallel \dots \parallel P_n$, preserve their conservativity. This will be very important later on, when manipulating the cubes of parallel processes.

**Proposition 4.3.5.** Given a conservative region $R$ on a program $P$, the region $\Phi^{-1}([R])$ on $\mathcal{U}(P)$ is also conservative.

*Proof.* First let us prove inductively on the pure transitions of Definition 4.3.2 that for any $x, y \in \mathcal{P}(\mathcal{U}(P))$, $x \to y$ is pure implies $\Phi(x) \to \Phi(y)$ is pure. First, let us check all the base cases:

* For the pure transition $\mathcal{U}(\alpha) \models \bot \rightarrow \top$, we have $\Phi(\bot) = \bot$, $\Phi(\top) = \top$ such that

$$ \alpha \models \Phi(\bot) \rightarrow \Phi(\top) = \alpha \models \bot \rightarrow \top $$

which is a pure transition.

* For the pure transition $\mathcal{U}(P+Q) \models \bot \rightarrow \bot+\emptyset$, we have

$$ P+Q \models \Phi(\bot) \rightarrow \Phi(\bot+\emptyset) = P+Q \models \bot \rightarrow \Phi(\bot)+\emptyset = P+Q \models \bot \rightarrow \bot+\emptyset $$

which is a pure transition.

* The transitions $\mathcal{U}(P+Q) \models \bot \rightarrow \emptyset+\bot$, $\mathcal{U}(P+Q) \models \emptyset+\top \rightarrow \top$ and $\mathcal{U}(P+Q) \models \top+\emptyset \rightarrow \top$ are treated similarly

* The transitions $\mathcal{U}(P;Q) \models \bot \rightarrow \bot; \bot$, $\mathcal{U}(P;Q) \models \top; \top \rightarrow \top$ are also treated similarly.

* For the pure transition $\mathcal{U}(P^*) \models \bot \rightarrow \bot; \bot$, we have $\Phi(\bot) = \bot$, $\Phi(\bot; \bot) = \bot^*$, such that

$$ P^* \models \Phi(\bot) \rightarrow \Phi(\bot; \bot) = P^* \models \bot \rightarrow \bot^* $$

which is a pure transition.
• The transition $\mathcal{U}(P^*) \models \top; \top \rightarrow \top$ is treated similarly.

All the inductive cases follow from the inductive structure of $\Phi$, we only present here one case, all remaining others being treated in a very similar manner. Let us look at the case

$$ \mathcal{U}(P \| Q) \models p \| q \rightarrow p \| q' $$

By inference rules, it is pure, if and only if $\mathcal{U}(Q) \models q \rightarrow q'$ is. Similarly, the following transition

$$ P \| Q \models \Phi(p \| q) \rightarrow \Phi(p \| q') = P \| Q \models \Phi(p) \| \Phi(q) \rightarrow \Phi(p) \| \Phi(q') $$

is pure if and only if $Q \models \Phi(q) \rightarrow \Phi(q')$ is. By induction hypothesis, $\mathcal{U}(Q) \models q \rightarrow q'$ pure implies $Q \models \Phi(q) \rightarrow \Phi(q')$ pure. Thus, $\mathcal{U}(P \| Q) \models p \| q \rightarrow p \| q'$ pure implies $P \| Q \models \Phi(p) \| \Phi(q) \rightarrow \Phi(p) \| \Phi(q')$ pure. Now, in order to prove $R$ conservative implies $\Phi^{-1}([R])$ we proceed by contradiction. Let us suppose that $R$ is conservative and $\Phi^{-1}([R])$ is not conservative. This implies that there exists $x \in \Phi^{-1}([R])$ and $y \notin \Phi^{-1}([R])$ such that $x \rightarrow y$ is pure. As proved above, this implies that $\Phi(x) \rightarrow \Phi(y)$ is pure. By definition $\Phi(x) \in [R]$, which is conservative by hypothesis. This implies $\Phi(y) \in [R]$ and thus $y \in \Phi^{-1}([R])$, which contradicts our hypothesis. Thus, $R$ conservative implies $\Phi^{-1}([R])$. $\square$

**Proposition 4.3.6.** The conservative regions on a preorder $\mathcal{P}$ form a boolean algebra.

*Proof.* As a subset of $\mathfrak{P}(P)$, we only need to prove that conservative regions are stable by intersection, union and complement. But this arises naturally from the definition of a conservative region. For the complement, it suffices to remark that $x \rightarrow y$ is pure implies $x \in [R] \iff y \in [R]$ which is equivalent to $x \in [R]^c \iff y \in [R]^c$. $\square$

**Proposition 4.3.7.** Given a program $P = P_1 \| \dots \| P_n \in \mathbf{Pgrm}$ and $R = (\prod_{i=1}^n c_i^j)_{j \in J}$ a maximal conservative cover on $P$, we have that for all $i \in I$ and all $j \in J$:

$$ \pi_i R_{c_j} = \{c \in \mathcal{C}(P_i) \mid c_1^j \times \dots \times c \times \dots \times c_n^j \in R\} $$

are maximal conservative and $c_i^j \in \pi_i R_{c_j}$

*Proof.* Given a maximal cover $R = (\prod_{i=1}^n c_i^j)_{j \in J}$ on $P_1 \| \dots \| P_n$ and $j \in J$, let us prove that $\pi_i R_{c_j} = \{c \in \mathcal{C}(P_i) \mid c_1^j \times \dots \times c \times c_n^j \in R\}$ is maximal and conservative.

• First let us prove that it is indeed maximal. Let us suppose a cube $d \in \mathcal{C}^{\max}[\pi_i R_{c_j}]$, such that there exists $c \in \pi_i R_{c_j}$, $c \subseteq d$. This implies

$$ c_1^j \times \dots \times c \times \dots \times c_n^j \subseteq c_1^j \times \dots \times d \times \dots \times c_n^j $$

Furthermore, by definition of $[\pi_i R_{c_j}]$, $c_1^j \times \dots \times d \times \dots \times c_n^j \in \mathcal{C}[R]$. Then, by maximality of $R$,

$$ c_1^j \times \dots \times c \times \dots \times c_n^j = c_1^j \times \dots \times d \times \dots \times c_n^j $$

i.e. $c = d$. Thus, $\pi_i R_{c_j}$ is indeed maximal.
* Now let us prove that it is conservative. To simplify the proof, we will first prove that the set

$$ \pi_i R_p = \{q \in P_i \mid p_1 \| \dots \| q \| \dots \| p_n \in [R]\} $$

is conservative for any $p = p_1 \| \dots \| p_n \in \mathcal{P}(P)$. By contradiction, let us suppose that there exists $q \in [\pi_i R_p]$ and $q' \notin [\pi_i R_p]$ such that $q \to q'$ is pure. Then, by Definition 4.3.2, the following transition is pure

$$ p_1 \| \dots \| q \| \dots \| p_n \to p_1 \| \dots \| q' \| \dots \| p_n $$

But, by definition of $q'$, $p_1 \| \dots \| q' \| \dots \| p_n \notin [R]$. This contradicts the conservativity of $R$. Thus, $\pi_i R_p = \{q \in P_i \mid p_1 \| \dots \| q \| \dots \| p_n \in [R]\}$ is conservative. Then as

$$ \pi_i R_{c^j} = \bigcup_{p \in c^j} \pi_i R_p $$

and conservative regions form a boolean algebra (Proposition 4.3.6), $\pi_i R_{c^j}$ is conservative.

<figure><img src="image_174.png" /></figure>

**Corollary 4.3.8.** Given a program $P = P_1 \| \dots \| P_n \in \mathbf{Pgrm}$ and $R = (\prod_{i=1}^n c_i^j)_{j \in J}$ a conservative cover on $P$, we have that for all $i \in I$, $\pi_i R = (c_i^j)_{j \in J}$ is a conservative cover on $P_i$.

*Proof.* We remark that $\pi_i R = (c_i^j)_{j \in J} = \bigcup_{c^j \in R} \pi_i R_{c^j}$, which are all conservative by Proposition 4.3.7. Then as conservative regions form a boolean algebra (Proposition 4.3.6), $\pi_i R$ is conservative as a cover of the union of conservative regions.

<figure><img src="image_175.png" /></figure>

We regroup here a few more properties of conservative regions of programs that will be useful in some proofs later on.

**Definition 4.3.9.** Given a program $P$ and a position $p \in \mathcal{P}(P)$, we define the *predecessors* and *successors* of $x$ respectively as

$$ \text{pred}(p) = \{q \in \mathcal{P}(P) \mid q \to p\} $$

$$ \text{succ}(p) = \{q \in \mathcal{P}(P) \mid p \to q\} $$

*Remark 4.3.10.* For $P \in \mathbf{Prcs} \setminus P_a, V_a$ with a region $R$ on $P^*$. Then $R$ conservative implies

* $\text{succ}(x) \cap [R] \neq \emptyset$ implies $\text{succ}(x) \subseteq [R]$

* $\text{pred}(x) \cap [R] \neq \emptyset$ implies $\text{pred}(x) \subseteq [R]$

As by induction rules, the only transition in processes that share an endpoint with another transition are pure.

By the remark above, and the definition of pure transition Definition 4.3.2, the core $\top^*$ is not a conservative region, and will “spread” inside the loop (if the loop is not of the form $P_a^*$ or $Va^*$) and to the extremities of the program $\bot, \top$.

Then, in any maximal cover of such a region, provided the region isn't the whole program, it will always be possible to find a specific set of cubes which will ensure that the cover lifts properly. If the region is the whole program, the maximal cover $\{(\bot, \top)\}$ will also lift properly.
*Example 4.3.11.* Let us consider the program $P = (P_a; V_a)^*$, whose syntactic semantics is given below. Using the inference rules from Definition 4.1.22, we obtain that the following transition are all pure, as they are obtained using pure transitions.

$$ \begin{array}{c} \overline{P^* \models \bot \rightarrow \bot^*} \\ \overline{P;Q \models \bot \rightarrow \bot; \bot} \\ \overline{P;Q \models \top; \top \rightarrow \top} \\ \overline{P;Q \models \top; \top^* \rightarrow \top; \top^*} \\ \overline{P^* \models \bot^* \rightarrow \top} \end{array} $$

Thus a conservative region on this program containing the core $\top^*$, as shown on the left actually contains all the positions shown on the right.

<figure><img src="image_176.png" /></figure>

<figure><img src="image_177.png" /></figure>

And in the maximal cover of such a region, we get the four following cubes:

<figure><img src="image_178.png" /></figure>

<figure><img src="image_179.png" /></figure>

**Lemma 4.3.12.** Given a program $P \in \mathbf{Prcs} \setminus \{\alpha\}$ and $R$ a conservative, maximal cover on $P^*$ such that $[R] \neq \mathcal{P}(P)$. Then

$$ \bot^* \in R \implies \exists p, q \in \mathcal{P}(P), p, q \neq \bot, \top \text{ such that } \{ (\bot, \top^*, \top), (\bot, p^*), (q^*, \top) \} \subseteq R $$

Furthermore, for any maximal conservative cover $R$

$$ (q^*, \bot^*, p^*) \in R \iff \{ (\bot, p^*), (q^*, \top) \} \subseteq R $$

*Proof.* Let $P \in \mathbf{Prcs} \setminus \{\alpha\}$, $R$ a conservative, maximal cover on $P^*$ such that $[R]^c \neq \emptyset$, i.e. there exists a conservative region $X \subset \mathcal{P}(P)$ such that $R = \mathcal{C}^{\max}(X)$.

* Let us first prove that

$$ (\bot, \top^*, \top) \in R $$

By Definition 4.3.3, $\top^* \in [R]^c$ implies $\top^*, \bot, \top \in [R]$, i.e.

$$ (\bot, \top^*, \top) \in \mathcal{C}[R] $$

As $[R] \neq \mathcal{P}(P)$, $(\bot, \top) \notin \mathcal{C}(R)$. This implies that $(\bot, \top^*, \top)$ is maximal in $\mathcal{C}[R] = \mathcal{C}(X)$, i.e.

$$ (\bot, \top^*, \top) \in \mathcal{C}^{\max}(X) = R $$
• Now let us prove that there exists $p, q \in \mathcal{P}(P), p, q \neq \perp, \top$ such that:

$$ (\perp, p^*), (q^*, \top) \in R $$

By Remark 4.3.10, $\perp^* \in [R]$ implies $\mathrm{succ}(\perp^*), \mathrm{pred}(\top^*) \subseteq [R]$. As $P \neq \alpha$, this implies that the following sets are non-empty

$$ X_{\perp} = \{x \in \mathcal{P}(P) \mid \perp < x < \top, (\perp, x^*) \in \mathcal{C}(R)\} $$

$$ Y_{\top} = \{x \in \mathcal{P}(P) \mid \perp < x < \top, (y^*, \top) \in \mathcal{C}(R)\} $$

Let us take $p$ (resp. $q$) the maximal (resp. minimal) elements of $X_{\perp}$, (resp. $Y_{\top}$). Now let us suppose, that there exists a cube $c \in R$ such that, $(\perp, p^*) \subseteq c$. This implies that

$$ c = (\perp, x^*), \perp < x < \top \text{ or } c = (\perp, \top) $$

As $[R]^c \neq \emptyset$, this implies $(\perp, \top) \notin R$. Thus, $c = (\perp, x^*)$, $\perp < x < \top$ and $x \in X_{\perp}$, hence, $x \le p$ i.e. $c = (\perp, x^*) \subseteq (\perp, p^*)$. Such that

$$ (\perp, p^*) \in R $$

By a similar reasoning,

$$ (q^*, \top) \in R $$

• Finally let us prove that

$$ (q^*, \perp^*, p^*) \in R \iff \{(\perp, p^*), (q^*, \top)\} \subseteq R $$

Let $(\perp, p^*), (q^*, \top) \in R, p^*, q^* \neq \perp$. Then by Lemma 4.2.20, $(\perp^*, p^*), (q^*, \top^*) \in \mathcal{C}([R])$, which is equivalent, by definition of composite cubes to

$$ (q^*, \top^*, p^*) \in \mathcal{C}([R]) $$

Now let us prove by contradiction that $(q^*, \top^*, p^*)$ is maximal, and thus in $R$. Let us suppose $c \in \mathcal{C}^{\max}(R) = R$, such that $(q^*, \top^*, p^*) \subseteq c$. This means that for any pair of paths $(\sigma_1, \sigma_2) \in (q^*, \top^*) \times (\top^*, p^*)$ and any path $\pi \in c$, there exists paths $\mu, \nu$ such that

$$ \mu \cdot \sigma_1 \cdot \sigma_2 \cdot \nu = \pi $$

As $q^*, p^* \neq \top^*$, this implies that $\pi$ contains $\top^*$ and that it is not one of its endpoints. By Lemma 4.2.14 that implies that there exists $x, y \in \mathcal{P}(P)$, $\perp < x, y < \top$ and

$$ c = (y^*, \top^*, x^*) \in \mathcal{L}_4 $$

Furthermore $(q^*, \top^*, p^*) \subseteq (y^*, \top^*, x^*)$ is equivalent to

$$ (q^*, \top^*) \subseteq (y^*, \top^*) \text{ and } (\top^*, p^*) \subseteq (\top^*, x^*) $$

This is equivalent by Lemma 4.2.20 to

$$ (\perp = q^*)(\perp, \top^*, q^*) \subseteq (\perp, \top^*, y^*) = (\perp, y^*) $$

$$ (p^*, \top) = (p^*, \top^*, \top) \subseteq (x^*, \top^*, \top) = (x^*, \top) $$

By maximality of $(p^*, \top)$ and $(\perp = q^*)$, $p = x$ and $q = y$, which concludes the proof. □
### 4.3.2 Lifting covers of loops

As explained at the beginning of this section, the lifting by $\Psi$ does not preserve the support of cubes, but we will prove in this section that when considering the maximal covers of conservative regions, we can make the naive lifting and the support commute once more, which will give us the following theorem.

**Theorem 4.3.15.** Given a program $P \in \mathbf{Pgrm}$ and a maximal conservative cover $R$ on $P$, we have

$$ \Phi^{-1}[R] = [\bigcup_{r \in R} \Psi^{-1}(r)] = [\Psi^{-1}(R)] $$

This will be proved later on. For now let us remark that both the hypothesis of maximality and conservativity are crucial for Theorem 4.3.15 as shown in the examples below.

Let us consider the program $P = (P_a; V_a)^*$ for a resource $a$ of capacity 0, and its unfolding $\mathcal{U}(P) = (P_a; V_a); (P_a; V_a)$, whose semantics are given below. Let us consider their authorized region in grey (which is conservative by Remark 4.3.23) and a non-maximal cover $R = \{R_1, R_2, r_3\}$. We can see that Theorem 4.3.15 does not hold.

<figure><img src="image_180.png" /></figure>

<figure><img src="image_181.png" /></figure>

Now let us consider the program $P = (\mathbf{skip}+\mathbf{skip})^*$ and its unfolding $\mathcal{U}(P) = (\mathbf{skip}+\mathbf{skip}); (\mathbf{skip}+\mathbf{skip})$ whose semantics are given respectively on the left and right below. Let us consider the non-conservative region $X$, containing a single maximal cube $c$, and $\Phi^{-1}(X)$ are given in grey below. Once again, in this case, the conditions of Theorem 4.3.15 do not hold.

<figure><img src="image_182.png" /></figure>
As we cannot lift cubes of $\Pi\mathcal{L}_{-1}$ it is important to prove that they do not contribute to the support of a maximal cover. This is a direct consequence of the Lemma 4.3.12. Indeed, the presence of $(\perp, \top^*, \top)$ in a maximal conservative cover implies the existence of other cubes that cover the same support as shown in Example 4.3.13.

*Example 4.3.13.* Let us consider the program $P = (\mathbf{skip}; \mathbf{skip})^*$ from Example 4.3.11, whose semantics is given below. The region in grey on the left below is not conservative, and by Lemma 4.3.12, a conservative region $X$ such that $[\perp, \top^*, \top] \subseteq X$ will be of the form on the left, spreading inside the loop.

<figure><img src="image_183.png" /></figure>

Thus, a maximal cover of such a region will contain $(\perp, \top^*, \top)$, but also the cubes $R_1$ and $R_2$, which cover a bigger region than $(\perp, \top^*, \top)$.

**Lemma 4.3.14.** Let $R$ a conservative cover on a program $P$, such that $R$ maximal. Then

$$[R] = [R \setminus \Pi_P \mathcal{L}_{-1}]$$

*Proof.* First let us note that If $R \cap \Pi\mathcal{L}_{-1} = \emptyset$. Then by definition $[R] = [R \setminus \Pi\mathcal{L}_{-1}]$. For the rest of the proof, we can suppose, $R \cap \Pi\mathcal{L}_{-1} \neq \emptyset$. Then by induction on $P$

* $P \in \mathbf{Prcs}$. Then $\Pi\mathcal{L}_{-1} = \emptyset$. This concludes the proof.

* $P = Q^*$ Otherwise if $(\perp, \top^*, \top) \in R$. Then $\top^* \in [R]$. By Lemma 4.3.12, this implies that there exists $p, q$ such that $(\perp, q^*)$, $(p^*, \top) \in R$. Furthermore,

$$\{\perp, \top^*, \top\} \subseteq [\perp, q^*] \cup [p^*, \top] \subseteq [R \setminus \mathcal{L}_{-1}]$$

Thus

$$ \begin{align*} [R] &\subseteq [R \setminus \mathcal{L}_{-1}] \cup [\mathcal{L}_{-1}] \\ &\subseteq [R \setminus \mathcal{L}_{-1}] \cup \{\perp, \top^*, \top\} \\ &\subseteq [R \setminus \mathcal{L}_{-1}] \cup [R \setminus \mathcal{L}_{-1}] \\ [R] &\subseteq [R \setminus \mathcal{L}_{-1}] \end{align*} $$

And as the support is increasing, $[R \setminus \mathcal{L}_{-1}] \subseteq [R]$. Thus,

$$[R] = [R \setminus \mathcal{L}_{-1}]$$

* $P = P_1 \parallel P_2$. We define for all $c = c_1 \times c_2 \in R$ the sets $\pi_1 R_c = \{c' \in \mathcal{P}(P_1) \mid c' \times c_2 \in R\}$ and $\pi_1 R_c = \{c' \in \mathcal{P}(P_2) \mid c_1 \times c' \in R\}$. By definition of the sets $\pi_i R_c$, we have

$$R = \bigcup_{c \in R} \pi_1 R_c \times \pi_2 R_c$$
And furthermore, by definition

$$R \setminus \Pi_P \mathcal{L}_{-1} = \bigcup_{c \in R} \pi_1 R_c \setminus \Pi_{P_1} \mathcal{L}_{-1} \times \pi_2 R_c \setminus \Pi_{P_2} \mathcal{L}_{-1}$$

As $R$ is maximal, the Proposition 4.3.7 implies that for all $c \in R$, we have $\pi_1 R_c$ and $\pi_2 R_c$ are maximal and conservative respectively on $P_1$ and $P_2$. We can then apply the induction hypothesis on $\pi_i R_c$ for $i = 1, 2$ such that

$$[\pi_i R_c \setminus \Pi_{P_i} \mathcal{L}_{-1}] = [\pi_i R_c]$$

Thus, we get:

$$ \begin{align*} [R] &= [\bigcup_{c \in R} \pi_1 R_c \times \pi_2 R_c] \\ &= \bigcup_{c \in R} ([\pi_1 R_c] \times [\pi_2 R_c]) \\ &= \bigcup_{c \in R} ([(\pi_1 R_c) \setminus \Pi_{P_1} \mathcal{L}_{-1}] \times [\pi_2 R_c \setminus \Pi_{P_2} \mathcal{L}_{-1}]) \\ &= [\bigcup_{c \in R} (\pi_1 R_c) \setminus \Pi_{P_1} \mathcal{L}_{-1} \times \pi_2 R_c \setminus \Pi_{P_2} \mathcal{L}_{-1}] \\ [R] &= [R \setminus \Pi_P \mathcal{L}_{-1}] \end{align*} $$

□

We can finally prove Theorem 4.3.15, which states that $\Psi$ lifts conservative covers to covers of their unfolding (in terms of regions). As forbidden regions of programs are conservative (Remark 4.3.4), this implies that we can unfold the forbidden region via its cover instead of lifting each position by $\Phi^{-1}$.

In the following, we will talk interchangeably about $C^{\max}(\Psi^{-1}(R))$ and $C^{\max}(\Phi^{-1}[R])$ as they are the same set.

**Theorem 4.3.15.** Given a program $P \in \mathbf{Pgrm}$ and a maximal conservative cover $R$ on $P$, we have

$$\Phi^{-1}[R] = [\bigcup_{r \in R} \Psi^{-1}(r)] = [\Psi^{-1}(R)]$$

*Proof.* Let $P \in \mathbf{Pgrm}$ and $R$ a maximal conservative cover. Let us prove the equality by induction on $P$.

* $P \in \mathbf{Prcs}$. Trivial

* $P = P_1 \parallel P_2$. We define for all $c = c_1 \times c_2 \in R$ the sets $\pi_1 R_c = \{c' \in \mathcal{P}(P_1) | c' \times c_2 \in R\}$ and $\pi_1 R_c = \{c' \in \mathcal{P}(P_2) | c_1 \times c' \in R\}$. By definition of the sets $\pi_i R_c$, we have

$$R = \bigcup_{c \in R} \pi_1 R_c \times \pi_2 R_c$$
As $R$ is maximal, the Proposition 4.3.7 implies that for all $c \in R$, we have $\pi_1 R_c$ and $\pi_2 R_c$ are maximal and conservative respectively on $P_1$ and $P_2$. We can then apply the induction hypothesis on $\pi_i R_c$ for $i = 1, 2$. This gives us

$$ \Phi^{-1}(\pi_i R_c) = \Psi^{-1}(\pi_i R_c) $$

This implies

$$
\begin{align*}
\Phi^{-1}[R] &= \Phi^{-1}[\bigcup_{c \in R} \pi_1 R_c \times \pi_2 R_c] \\
&= \bigcup_{c \in R} \Phi^{-1}[\pi_1 R_c] \times \Phi^{-1}[\pi_2 R_c] \\
&= \bigcup_{c \in R} [\Psi^{-1}(\pi_1 R_c)] \times [\Psi^{-1}(\pi_2 R_c)] \\
&= [\Psi^{-1}(\bigcup_{c \in R} \pi_1 R_c \times \pi_2 R_c)] \\
\Phi^{-1}[R] &= [\Psi^{-1}(R)]
\end{align*}
$$

• $P = Q^*$. First let us remark that $[R] = \mathcal{P}(P)$ implies by maximality of $R$ that $R = \{(\perp, \top)\}$, and thus

$$ \Phi^{-1}(R) = \mathcal{P}(\mathcal{U}(P)) = [\perp, \top] = [\Psi^{-1}(R)] $$

We can thus suppose $[R] \neq \mathcal{P}(P)$ for the rest of this case. We proceed to prove the equality by double inclusion.

- First let us prove $\Phi^{-1}([R]) \subseteq [\Psi^{-1}(R)]$. We will proceed by separating the cases depending on the value of $x \in [R]$.

* If $x \in \{\perp, \top, \perp^*\}$, by conservativity of $R$, this implies $\perp^* \in R$. Then, as we suppose $[R] \neq \mathcal{P}(P)$, we can apply Lemma 4.3.12, which implies here exists $p, q \in \mathcal{P}(Q)$, $p, q \neq \perp, \top$ such that

$$ (\perp, p^*), (q^*, \top), (q^*, \top^*, p^*) \in R $$

By definition of $\Psi$, this implies

$$ (\perp, p; \perp), (\top; q, \top), (p; \perp, \top; q) \in \Psi^{-1}(R) $$

Thus

$$ \Phi^{-1}(x) \subseteq \Phi^{-1}(\{\perp, \top, \perp^*\}) = \{\perp; \perp, \top; \perp, \top; \top\} \subseteq [\Psi^{-1}(R)] $$

* Otherwise $x = y^*, y \neq \perp, \top$. Thus,

$$ \Phi^{-1}(x) = \{y; \perp, \top; y\} $$

• If $x \in [p^*, q^*]$, $(p^*, q^*) \in R \cap \mathcal{L}_5$. Then by Definition 4.2.13, $y \in (p, q)$. By inference rules on cubes of loop-free program, this implies

$$ y; \perp \in (p; \perp, q; \perp) \quad \text{and} \quad \top; y \in (\top; p, \top; q) $$

Thus

$$ \Phi^{-1}(x) \subseteq [(p; \perp, q; \perp), (\top; p, \top; q)] = [\Psi^{-1}(p^*, q^*)] \subseteq [\Psi^{-1}(R)] $$
· Otherwise, $x \in [R]$ implies that there is a cube $c$ of $R$ that is not in $\mathcal{L}_5 \cup \mathcal{L}_1$ such that $x \in [c]$. By looking at the supports, $c \in \mathcal{L}_4 \cup \mathcal{L}_4 \cup \mathcal{L}_2 \cup \mathcal{L}_3$, i.e. there exists $p, q \in \mathcal{P}(Q), p, q \neq \perp, \top$ such that

$$c = (\perp, p^*) \text{ or } c = (q^*, \top) \text{ or } c = (q^*, \top^*, p^*)$$

By Lemma 4.3.12, if one of these cubes belongs to $R$, then we can choose $p$ or $q$ such that they all belong to $R$. By definition of $(q^*, \top^*, p^*)$

$$x \in (q^*, \top^*, p^*) \text{ and } \left( x \in (\perp, p^*) \text{ or } (q^*, \top) \right)$$

Let us suppose $x \in [\perp, p^*] \cap [q^*, \top^*, p^*]$. By Lemma 4.2.20 and Definition 4.2.13

$$\Phi^{-1}(x) = \{y; \perp, \top; y\} \subseteq [\{(p; \perp, q; \perp), (\perp, p; \perp)\}] \subseteq [\Psi^{-1}(R)]$$

Similarly if $x \in [q^*, \top] \cap [q^*, \top^*, p^*]$

Thus for all $x \in [R]$, $\Phi^{-1}(x) \subseteq [\Psi^{-1}(R)]$. This implies

$$\Phi^{-1}([R]) \subseteq [\Psi^{-1}(R)]$$

— Now let us prove $[\Psi^{-1}(R)] \subseteq \Phi^{-1}([R])$.

$$[R] = [R \setminus \Pi \mathcal{L}_{-1}] \qquad \text{Lemma 4.3.14}$$

$$= \bigcup_{r \in R \setminus \Pi \mathcal{L}_{-1}} [r]$$

$$= \bigcup_{r \in R \setminus \Pi \mathcal{L}_{-1}, i \in \Psi^{-1}(r)} [\Psi(i)]$$

$$= \bigcup_{r \in R \setminus \Pi \mathcal{L}_{-1}, i \in \Psi^{-1}(r)} \Phi([i]) \qquad \text{Proposition 4.2.44}$$

$$= \Phi\left(\bigcup_{r \in R \setminus \Pi \mathcal{L}_{-1}} [\Psi^{-1}(r)]\right)$$

$$= \Phi([\Psi^{-1}(R \setminus \Pi \mathcal{L}_{-1})])$$

$$[R] = \Phi([\Psi^{-1}(R)])$$

□

### 4.3.3 Maximal cubical cover as a quotient of the 2-unfolding

In Theorem 4.3.15, we have already proven that conservative regions, and hence the authorized and forbidden region of a program, can be lifted to their unfolding not only point-wise via $\Phi$ but also cover-wise via $\Psi$.

In this part we will extend this lifting property to the normal form of regions. Indeed, as stated in the following Theorem 4.3.27, $\Psi^{-1}$ sends the normal form of a conservative region $X$ to the normal form of its unfolding $\Phi^{-1}(X)$.
**Theorem 4.3.27.** Given a conservative program $P \in \mathbf{Pgrm}$ and $R$ a conservative maximal cover of $P$, we have

$$C^{\max}(\Psi^{-1}(R)) = \Psi^{-1}(R)$$

Theorem 4.3.27 implies, for conservative programs, that the normal form of the forbidden region can be computed as the image by $\Psi$ of the cover of the forbidden region of the unfolding, which is loop free.

To prove Theorem 4.3.27, we will first prove that $\Psi$ preserves the order on cubes (Definition 4.2.28) in Proposition 4.3.19 and that $\Psi$ reflects maximal cubes, up to equivalence, in Proposition 4.3.24.

#### 4.3.3.1 $\Psi$ preserves inclusion of cubes

Before we can prove our result, we prove here two very important technical lemmas. First, Lemma 4.3.16 which stipulates that the equivalence on paths defined in Definition 4.2.13 can be extended to cubes of $P^*$ that do not cross the core of the loop $\top^*$. This implies, that inclusion is obtained inductively by looking at the inclusion of cubes on $P$.

Then, Lemma 4.3.17 which stipulates that when such cubes are included in a composite cube, they are actually included in one of the two cubes of the composite.

**Lemma 4.3.16.** Let $P \in \mathbf{Prcs}$, let $p, q, x, y \in \mathcal{P}(P)$ such that $x \le y$, and $p \le q$,

* If $(x, y) \ne (\bot, \top)$, then $(p, q) \subseteq (x, y) \implies (p^*, q^*) \subseteq (x^*, y^*)$

* If $(x^*, y^*)$ and $(p^*, q^*) \ne (\top^*, \top^*)$, then $(p^*, q^*) \subseteq (x^*, y^*) \implies (p, q) \subseteq (x, y)$

*Proof.* First, let us remark that $(x^*, y^*)$, $(p^*, q^*) \ne (\top^*, \top^*)$ or $(x, y) \ne (\bot, \top)$ implies $p, q \ne \bot, \top$ and $x, y \ne \bot, \top$.

* Let $(p, q) \subseteq (x, y)$ and let $\pi^* \in (p^*, q^*)$. Thus, by Definition 4.2.13, $\pi \in (p, q)$, i.e. there exists $\nu, \mu$ such that $\nu \cdot \pi \cdot \mu \in (x, y)$. Once again by Definition 4.2.13, $(\nu \cdot \pi \cdot \mu)^* = \nu^* \cdot \pi^* \cdot \mu^* \in (x^*, y^*)$. Thus, $(p^*, q^*) \subseteq (x^*, y^*)$

* Let $(p^*, q^*) \subseteq (x^*, y^*)$ and $\pi \in (p, q)$. By Definition 4.2.13, $\pi^* \in (p^*, q^*)$. Such that, there exists $\nu^*, \mu^*$ such that $\nu^* \cdot \pi^* \cdot \mu^* \in (x^*, y^*)$. By Lemma 4.2.14, we can apply Definition 4.2.13, such that $\nu \cdot \pi \cdot \mu \in (x, y)$. Thus, $(p, q) \subseteq (x, y)$. $\square$

**Lemma 4.3.17.** Given a program $P \in \mathbf{Prcs}$ and positions $p, q, x, y \in \mathcal{P}(P)$ such that $p \le q$, $x, y \notin \{\bot, \top\}$ we have

$$(p^*, q^*) \subseteq (x^*, \top^*, y^*) \text{ implies } (p^*, q^*) \subseteq (x^*, \top^*) \text{ or } (p^*, q^*) \subseteq (\bot^*, y^*)$$

*Proof.* Let $P \in \mathbf{Prcs}$. Let $p, q, x, y \in \mathcal{P}(P)$ such that $p \le q$, $x, y \notin \{\bot, \top\}$ and such that $(p^*, q^*) \subseteq (x^*, \top^*) \times (\bot^*, y^*)$.

* If $(p^*, q^*) = (\bot^*, \bot^*)$, then

$$(p^*, q^*) = (\bot^*, \bot^*) \subseteq (x^*, \top^*)$$
• Otherwise, $(p^*, q^*) \neq (\perp^*, \perp^*)$. Let $\pi \in (p^*, q^*) \subseteq (x^*, \top^*) \times (\perp^*, y^*)$. This implies there exists $\rho^*, \sigma^* \in (x^*, \top^*) \times (\perp^*, y^*)$ and $\mu^*, \nu^* \in (x^*, p^*) \times (y^*, q^*)$ such that

$$ \nu^* \cdot \pi^* \cdot \mu^* = \sigma^* \cdot \rho^* $$

By the contraposition of Lemma 4.2.14, $\perp^* \notin \pi^*$. Thus, $\perp^* \in [\mu^*] \cup [\nu^*]$. As $\sigma^*$ and $\rho^*$ are cycle-free non-empty paths and $\top^*$ is one of their respective extremities, this implies that $\top^*$ appears only once in $\sigma^* \cdot \rho^* = \nu^* \cdot \pi^* \cdot \mu^*$. Thus, we have either $\perp^* \in \mu^*$ or $\perp^* \in \nu^*$.

- Let us suppose $\perp^* \in \mu^*$. Then $\perp^* \notin \nu^* \cdot \pi^*$. Then by Definition 4.2.13, $\pi, \nu \in (p, q) \times (q, y)$. Which implies for position of a program without loops, $\perp \le p \le q \le y$ i.e. $(p, q) \subseteq (\perp, y)$. Once again by Definition 4.2.13 $(p^*, q^*) \subseteq (\perp^*, y^*)$

- Similarly, if we suppose $\perp^* \in \nu^*$, we can prove $(p^*, q^*) \subseteq (x^*, \top^*)$. $\square$

We are now ready to prove that $\Psi$ preserves order on cubes (Proposition 4.3.19). This property is first proved on single processes, then extended to parallel composition using the Proposition 4.3.7.

**Proposition 4.3.18.** Given a program $P \in \mathbf{Prcs}$, then

$$ \Psi_{P^*}: \mathcal{C}(\mathcal{U}(P^*)) \setminus \mathcal{C}_{-1} \to \mathcal{C}(P^*) \setminus \mathcal{L}_{-1} \\ c \mapsto \Psi_{P^*}(c) $$

is a surjective morphism of posets, i.e. for all $c, d \in \mathcal{C}(\mathcal{U}(P^*)) \setminus \mathcal{C}_{-1}$,

$$ c \subseteq d \implies \Psi(c) \subseteq \Psi(d) $$

*Proof.* Let us suppose given a program $P \in \mathbf{Prcs}$ and $c, d \in \mathcal{C}(P;P) \setminus \mathcal{C}_{-1}$ such that $c \subseteq d$. Let us prove that $\Psi(c) = \Psi(d)$ by differentiating on the subset of $\mathcal{C}(P;P)$ that $c, d$ belong to.

• $c \in \mathcal{C}_0 = \{(\perp, \perp), (\top, \top), (\perp; \perp, \perp; \perp), (\top; \perp, \top; \perp), (\top; \top, \top; \top)\}$

- $c = (\perp, \perp)$. Then $c \subseteq d$ implies $\perp \in d$. Hence, $d \in \mathcal{C}_0 \cup \mathcal{C}_2 \cup \mathcal{C}_1$.

* $d \in \mathcal{C}_0$. Then $\perp \in d$ implies $d = (\perp, \perp)$. Thus, $\Psi(c) = \Psi(d)$

* $d \in \mathcal{C}_2$, Then $\Psi(c) = (\perp, \perp) \subseteq (\perp, p^*) = \Psi(d)$.

* $d \in \mathcal{C}_1$, Then $\Psi(c) \subseteq (\perp, \top) = \Psi(d)$

- $c = (\perp; \perp, \perp; \perp)$. Similar to the case above.

- $c = (\top, \top)$. Dual to the case $c = (\perp, \perp)$.

- $c = (\top; \top, \top; \top)$. Similar to the case above.

- $c = (\top; \perp, \top; \perp)$. Then $c \subseteq d$ implies $(\top; \perp) \in d$, such that $d \in \mathcal{C}_4 \cup \mathcal{C}_4 \cup \mathcal{C}_0$.

* $d = (x; \perp, \top; y) \in \mathcal{C}_4 \cup \mathcal{C}_4$. Then by Lemma 4.2.20 $\Psi(c) = (\perp^*, \perp^*) \subseteq (x^*, \top^*) \times (\perp^*, y^*) = \Psi(d)$

* $d \in \mathcal{C}_0$. Then, $c = d$ and $\Psi(c) = \Psi(d)$.

• $c \in \mathcal{C}_1$ such that $c = (\perp, \top)$. Then $c \subseteq d$ implies $d = (\perp, \top) = c$.
• $c \in C_2$. Then $c \subseteq d$ implies $\perp \in d$, $d \neq (\perp, \perp)$ such that $d \in C_2 \cup C_1$.

– Let $d \in C_2$. Then $c = (\perp, \perp; p) \subseteq (\perp, \perp; x) = d$ implies

$$ (\perp; \perp, \perp; p) \subseteq (\perp; \perp, \perp; x) $$

By induction rules this implies $(\perp, p) \subseteq (\perp, x)$. Furthermore, $x \neq \top$ by definition of $C_2$. Hence,

$$ \begin{align*} \Psi(c) &= (\perp, p^*) \\ &= (\perp, \perp^*) \times (\perp^*, p^*) && \text{Lemma 4.2.20} \\ &\subseteq (\perp, \perp^*) \times (\perp^*, x^*) && \text{Lemma 4.3.16} \\ &= (\perp, y^*) && \text{Lemma 4.2.20} \\ \Psi(c) &\subseteq \Psi(d) \end{align*} $$

– Let $d \in C_1$. Then $\Psi(c) \subseteq (\perp, \top) = \Psi(d)$

• $c \in C_3$. Dual of the case $c \in C_2$

• $c \in C_4$, $c = (p; \perp, \top; q) = (p; \perp, \top; \perp) \times (\top; \perp, \top; q)$. Thus, $\top; \perp \in c$. Then $c \subseteq d$ implies $\top; \perp \in d$ and thus $d \in C_4 \cup C_1$.

– Let $d \in C_1$. Then $\Psi(c) \subseteq (\perp, \top) = \Psi(d)$

– Let $d \in C_4$. Then $d = (x; \perp, \top; y) = (x; \perp, \top; \perp) \times (\top; \perp, \top; y)$. Furthermore, $c \subseteq d$ implies

$$ (p; \perp, \top; \perp) \times (\top; \perp, \top; \perp; q) \subseteq (x; \perp, \top; \perp) \times (\top; \perp, \top; y) $$

By induction rules, we get

$$ (p, \top) \subseteq (x, \top) \text{ and } (\perp, q) \subseteq (\perp, y) $$

By Proposition 4.2.33, $x \neq \perp$ and $y \neq \top$. This implies

$$ \begin{align*} \Psi(c) &= (p^*, \top^*, q^*) && \text{Lemma 4.2.20} \\ &= (p^*, \top^*) \times (\perp^*, q^*) \\ &\subseteq (x^*, \top^*) \times (\perp^*, y^*) && \text{Lemma 4.3.16} \\ &\subseteq (x^*, \top^*, y^*) \\ \Psi(c) &\subseteq \Psi(d) \end{align*} $$

• $c \in C_5$. Then $c \subseteq d$ implies $d \cap \{x; \perp | x \in \mathcal{P}(P) \setminus \{\top\}\} \neq \emptyset$. Thus, $d \notin C_0 \cup C_3 \cup C_6$

– $d \in C_0$. Then $c \subseteq d$ implies $c = d$.

– $d \in C_1$. Then $\Psi(c) \subseteq (\perp, \top) = \Psi(d)$

– $d \in C_2$. Then $c = (p; \perp, q; \perp) \subseteq (\perp; \perp, x, \perp; \perp) \subseteq (\perp, x; \perp)$. By induction rules $(p, q) \subseteq (\perp, x)$. Furthermore, by definition of $C_2$, $x \neq \top$. Thus, by Lemma 4.3.16, $\Psi(c) = (p^*, q^*) \subseteq (\perp^*, x^*) \subseteq (\perp, x^*) = \Psi(d)$.
- $d \in C_4$. Then $c = (p; \perp, q; \perp) \subseteq (p; \perp, \top; \perp) \subseteq (x; \perp, \top; \perp) \subseteq (x; \perp, \top; y) = d$. By induction rules this implies $(p, q) \subseteq (p, \top) \subseteq (x, \top)$. Furthermore, $x \neq \perp$ by definition of $C_4$. Hence,

$$ \begin{align*} \Psi(c) &= (p^*, q^*) \\ &\subseteq (x^*, \top^*) &\qquad \text{Lemma 4.3.16} \\ &\subseteq (x^*, \top^*) \times (\perp^*, y^*) \\ &\subseteq (x^*, \top^*, y^*) \\ \Psi(c) &\subseteq \Psi(d) &\qquad \text{Lemma 4.2.20} \end{align*} $$

- $d \in C_5$. Then $c = (p; \perp, q; \perp) \subseteq (x; \perp, y, \perp; \perp) = d$ implies by induction rules $(p, q) \subseteq (x, y) \neq (\perp, \top)$. Thus, by Lemma 4.3.16, $\Psi(c) = (p^*, q^*) \subseteq (x^*, y^*) = \Psi(d)$.

* $c \in C_6$. Similar to the case $c \in C_5$. □

**Proposition 4.3.19.** Given a program $P \in \mathbf{Pgrm}$, we have that

$$ \Psi: \mathcal{C}(\mathcal{U}(P)) \setminus \Pi_{\mathcal{U}(P)} C_{-1} \to \mathcal{C}(P) \setminus \Pi_P \mathcal{L}_{-1} \\ c \mapsto \Psi(c) $$

is a surjective morphism of posets.

*Proof.* By induction on $P$

* $P \in \mathbf{Prcs}$. Then $\Psi$ is the identity.

* $P = Q^*$. By Proposition 4.3.18 and Proposition 4.2.36.

* $P = S \| T$. Let $s \times t \subseteq x \times y \in C_{\mathcal{U}(P)}^m \setminus \Phi^{-1}(R)$. Then $s \subseteq x$ and $t \subseteq y$ by Definition 4.2.21. By induction hypothesis, this implies, $\Psi(s) \subseteq \Psi(x)$ and $\Psi(t) \subseteq \Psi(y)$. Then once again, by Definition 4.2.21

$$ \Psi(s \times t) \subseteq \Psi(x \times y) $$

As $\Psi_{S \| T} = \Psi_S \times \Psi_T$, by induction hypothesis, $\Psi_{S \| T}$ is surjective.

□

### 4.3.3.2 $\Psi$ weakly reflects inclusion of maximal cubes

Before we prove our result, once again, we first prove a few characteristics of maximal cubes of loops. Indeed, for a program $P^* \in \mathbf{Prcs}^*$ the subsets $C_0$ and $\mathcal{L}_0$ of $\mathcal{C}(P^*)$ are never maximal. Furthermore, using Lemma 4.3.12 and the aforementioned properties, we then get a characterization of any maximal cover $R$ of $P^*$ in Proposition 4.3.21. Finally, we will prove that $\Psi$ weakly reflects inclusion of maximal cubes (i.e. up to the equivalence of Definition 4.2.37)

**Lemma 4.3.20.** Given a program $P \in \mathbf{Pgrm}$ and $R$ a maximal conservative cover on $P(P)$, we have

$$ R \cap \Pi_P \mathcal{L}_0 = \emptyset $$
*Proof.* Let $P \in \mathbf{Pgrm}$ and $R$ a maximal conservative cover of $P$. If $[R] = \mathcal{P}(P)$, then $R = \{(\perp, \top)\}$, which concludes the proof. We can then suppose that $[R] \neq \mathcal{P}(P)$ for the rest of the proof.

* $P \in \mathbf{Prcs}$. Then $\Pi_P \mathcal{L}_0 = \emptyset$ by definition

* $P = P^*$. Then $\Pi_P \mathcal{L}_0 = \{(\perp, \perp), (\top, \top), (\top^*, \top^*)\}$.

- If $\perp^* \notin [R]$. Then by conservativity of $R$, this implies $\perp, \top, \perp^* \notin [R]$, i.e.

$$[\perp, \perp] \cap [R] = \emptyset \text{ and } [\top^*, \top^*] \cap [R] = \emptyset \text{ and } [\top, \top] \cap [R] = \emptyset$$

This implies $R \cap \Pi_P \mathcal{L}_0 = \emptyset$.

- If $\perp^* \in [R]$, then by Lemma 4.3.12, $(\perp, \top^*, \top) \in R$, furthermore by definition of composite cubes,

$$(\perp, \perp) \subseteq (\perp, \top^*, \top) \text{ and } (\top^*, \top^*) \subseteq (\perp, \top^*, \top) \text{ and } (\top, \top) \subseteq (\perp, \top^*, \top)$$

Thus no cubes of $\Pi_P \mathcal{L}_0$ are in $R$ as they are not maximal.

* $P = P_1 \parallel P_2$. By Proposition 4.3.7, for all $c = c_1 \times c_2 \in R$ the sets

$$\pi_1 R_c = \{c' \in \mathcal{P}(P_1) \mid c' \times c_2 \in R\} \text{ and } \pi_1 R_c = \{c' \in \mathcal{P}(P_2) \mid c_1 \times c' \in R\}$$

are conservative and maximal. By definition, $c_i \in \pi_i R_c$ for $i = 1, 2$ and by induction hypothesis, this implies $c_i \notin \Pi_{P_i} \mathcal{L}_0$. Thus, $c \notin \Pi_P \mathcal{L}_0$

□

**Proposition 4.3.21.** *Given a program $P \in \mathbf{Prcs}$ and $R$ a conservative maximal region on the program $P^*$, we have the three mutually exclusive characterization of $R$:*

* If $[R] = \mathcal{P}(P^*)$, then $R = \{(\perp, \top)\}$

* If $[R] \neq \mathcal{P}(P^*)$ and $\perp^* \in [R]$, then there exists $((p_j, q_j))_{j \in J_1 \cup J_2}$, such that for all $j \in J_1 \cup J_2$, we have $p_j, q_j \in \mathcal{P}(P) \setminus \{\perp, \top\}$ and

$$R = \bigcup_{j \in J_1} \{(p_j^*, q_j^*)\} \bigcup_{j \in J_2} \{(\perp, q_j^*), (p_j^*, \top), (p_j^*, \top^*, q_j^*), (\perp, \top^*, \top)\}$$

* Otherwise, there exists $((p_j, q_j))_{j \in J} \in \mathcal{C}(P)^J$, such that for all $j \in J$, $p_j, q_j \notin \{\perp, \top\}$ and

$$R = \bigcup_{j \in J} \{(p_j^*, q_j^*)\}$$

*Proof.* Let us suppose $R$ a conservative maximal region on a program $P^* \in \mathbf{Prcs}^*$.

* If $[R] = \mathcal{P}(P^*)$, then $(\perp, \top) \in \mathcal{C}([R])$ and for any cube $c \in \mathcal{C}(P^*)$, $c \subseteq (\perp, \top)$, thus $R = \{\perp, \top\}$.
• If $[R] \neq \mathcal{P}(P^*)$ and $\perp^* \in [R]$. By Lemma 4.3.20 and Lemma 4.3.20,

$$R \subseteq \mathcal{L}_{-1} \cup \mathcal{L}_2 \cup \mathcal{L}_3 \cup (\mathcal{L}_4 \cup \mathcal{L}_4) \cup \mathcal{L}_5$$

Then, by Lemma 4.3.12, for every pair of positions $p, q \neq \perp, \top$ such that $(p^*, \top), (\perp, q^*) \in R$ or $(p^*, \top^*, q^*) \in R$ we have that

$$(p^*, \top), (\perp, q^*), (p^*, \top^*, q^*), (\perp, \top^*, \top) \in R$$

Furthermore as $R$ is conservative, we can exclude the case where only $(p^*, \top)$ or $(\perp, q^*)$ would belong to $R$. Indeed, if we define

$$X_{\perp} = \{x \in \mathcal{P}(P) \mid \perp < x < \top, (\perp, x^*) \in \mathcal{C}(R)\}$$

$$Y_{\top} = \{x \in \mathcal{P}(P) \mid \perp < x < \top, (y^*, \top) \in \mathcal{C}(R)\}$$

Let us take $p$ (resp. $q$) the maximal (resp. minimal) elements of $X_{\perp}$, (resp. $Y_{\top}$). We have seen in the proof of Lemma 4.3.12 that these are correctly defined and

$$(\perp, p^*), (q^*, \top) \in R$$

Now we only need to prove that the cubes of $R \cap \mathcal{L}_5$ do not have $\top^*$ as an endpoint. By contradiction, let us suppose that there exists such a cube $(\perp^*, q^*) \in R$. Then by definition

$$(\perp^*, q^*) \subseteq (\perp, q^*) \in \mathcal{C}([R])$$

This contradicts the definition of $R$ as maximal. Thus, $(\perp^*, q^*) \notin R$ (the case $(p^*, \top^*)$ is dual).

• Otherwise, the only possible maximal cubes of $R$ are cubes of $\mathcal{L}_5$ such that the support does not intersect $\top^*$. By Lemma 4.2.14, this is precisely the cubes of the form $(p^*, q^*)$ such that $p, q \neq \perp, \top$. □

**Proposition 4.3.22.** Given a program $P \in \mathbf{Prcs}$ such that $P \neq P_a, V_a$, a maximal conservative cover $R$ of $P^*$ and $c, d \in \mathcal{C}^{\max}(\Psi^{-1}(R))$, we have

$$\Psi(c) \subseteq \Psi(d) \implies \exists k \in \Psi^{-1}(\Psi(d)), i \subseteq k$$

*Proof.* Let us suppose given a program $P \in \mathbf{Prcs}$, a maximal conservative cover $R$ of $P^*$ and $c, d \in \mathcal{C}^{\max}(\Psi^{-1}(R))$. Furthermore, let us suppose $\Psi(c) \subseteq \Psi(d)$. Let us prove that

$$\exists k \in \Psi^{-1}(\Psi(d)), i \subseteq k$$

First let us remark that by definition of $\Psi$, and by Lemma 4.3.20

$$\Psi(c), \Psi(d) \notin \mathcal{L}_{-1} \cup \mathcal{L}_0$$

We will now proceed to check all cases depending on the subset of $\mathcal{C}(P^*)$ in which $c, d$ are contained.

• $\Psi(d) \in \mathcal{L}_1$. Then by definition for all $c \in \mathcal{C}(\Phi^{-1}(R)), c \subseteq (\perp, \top) = d$.

• $\Psi(d) \in \mathcal{L}_2$, i.e. $\Psi(d) = (\perp, y^*)$. Then $\Psi(c) \subseteq \Psi(d)$ implies by looking at the supports: $\Psi(c) \notin \mathcal{L}_3 \cup \mathcal{L}_1$.
- $\Psi(c) \in \mathcal{L}_2$. Then $\Psi(c) = (\perp, q^*) \subseteq (\perp, y^*) = \Psi(d)$ implies by Lemma 4.2.20 $(\perp, q^*) \subseteq (\perp, y^*)$. Furthermore, we have $y, q \neq \top$. Then

* $y = \perp$ implies $q = \perp$. Thus, $c = d$

* $q = \perp$ implies $c = (\perp, \perp; \perp) \subseteq (\perp, y; \perp) = d$.

* Otherwise, $y, q \notin \{\perp, \top\}$ Thus by Lemma 4.3.16, $(\perp, q) \subseteq (\perp, y)$ and by induction rules $c = (\perp, q; \perp) \subseteq (\perp, y; \perp) = d$

- $\Psi(c) \in \mathcal{L}_4$, i.e. $\Psi(c) = (p^*, \top^*, q^*)$, $p, q \notin \{\perp, \top\}$. Let us prove by contradiction that

$$ \Psi(c) \not\subseteq \Psi(d) $$

Let us suppose, $\Psi(c) \subseteq \Psi(d)$, then for any $\sigma \cdot \rho \in \Psi(c)$, there exists $\mu, \nu \in (\perp, p^*) \times (q^*, y^*)$ such that

$$ \nu \cdot \sigma \cdot \rho \cdot \mu \in (\perp, y^*) $$

By definition, $\top^* \in \sigma \cdot \rho$ and $\top^* \in \mu$. Furthermore, as $\top^*$ is not the endpoint of $\mu$ as $p \neq \perp, \top$. Thus, there is a non-trivial loop in $\nu \cdot \sigma \cdot \rho \cdot \mu$ contradicts the fact that it is an element of $(\perp, y^*)$.

- $\Psi(c) \in \mathcal{L}_5$. $\Psi(c) = (p^*, q^*) \neq (\perp^*, \top^*)$. Then $\Psi(c) = (p^*, q^*) \subseteq (\perp^*, y^*) = \Psi(d)$ implies $y \neq \perp$. As $y \neq \top$ by definition, this implies by Lemma 4.3.16, $(p, q) \subseteq (\perp, y)$.

* If $c \in \mathcal{L}_5$, this implies $c = (p; \perp, q; \perp) \subseteq (\perp; \perp, y; \perp) \subseteq (\perp, y; \perp) = d$.

* Otherwise, $c \in \mathcal{L}_6$. Then $(p, q) \subseteq (\perp, y)$

$$ c = (\top; \perp, \top; q) \in \mathcal{C}^{\max}(\Psi^{-1}(R)) $$

As $P \neq P_a, V_a$, by Definition 4.3.2, there exists $z \in \mathcal{P}(P)$, such that $z; \perp \to \top; \perp$ is pure. As $R$ is conservative, so is $\Psi^{-1}(R)$. This implies that

$$ c \subset (z; \perp, \top; q) \in \mathcal{C}([\Psi^{-1}(R)]) $$

which contradicts the fact that $c$ is maximal.

* $\Psi(d) \in \mathcal{L}_3$. Symmetric to the case above.

* $\Psi(d) \in \mathcal{L}_4$, such that $\Psi(d) = (x^*, \top^*, y^*)$ and $x, y \notin \{\perp, \top\}$. Then $\Psi(c) \subseteq \Psi(d)$ implies $\Psi(c) \in \mathcal{L}_4 \cup \mathcal{L}_5$.

- $\Psi(c) \in \mathcal{L}_4$. $\Psi(c) = (p^*, \top^*, q^*)$, $p, q \notin \{\perp, \top\}$. Then $\Psi(c) \subseteq \Psi(d)$ implies $(p^*, \top^*) \times (\top^*, q^*) \subseteq (x^*, \top^*) \times (\top^*, y^*)$ i.e.

$$ (p^*, \top^*) \subseteq (x^*, \top^*) \text{ and } (\top^*, q^*) \subseteq (\top^*, y^*) $$

By Lemma 4.3.16, this implies $(p, \top) \subseteq (x, \top)$ and $(\perp, q) \subseteq (\perp, y)$. Thus, by induction rules $c = (p; \perp, \top; q) \subseteq (x; \perp, \top; y) = d$

- $\Psi(c) \in \mathcal{L}_5$. $\Psi(c) = (p^*, q^*) \subseteq (x^*, \top^*, y^*) = \Psi(d)$ implies by Lemma 4.3.17,

$$ (p^*, q^*) \subseteq (x^*, \top^*) \text{ or } (p^*, q^*) \subseteq (\perp^*, y^*) $$
Let us suppose $(p^*, q^*) \subseteq (x^*, \top^*)$, and $c \in \mathcal{C}_5$. By definition $(p^*, q^*)$ and $(\bot^*, y^*) \neq (\top^*, \top^*)$. Thus, by Lemma 4.3.16, $(p, q) \subseteq (x, \top)$ and by induction rules,

$$c = (p; \bot, q; \bot) \subseteq (x; \bot, \top; \bot) \subseteq x; \bot, \top; y = d$$

The cases where $(p^*, q^*) \subseteq (y^*, \top^*)$ and/or $c \in \mathcal{C}_6$ follow the same proof.

* $\Psi(d) \in \mathcal{L}_5$. $\Psi(d) = (x^*, y^*) \neq (\bot^*, \top^*)$, $p \leq q$. Then $\Psi(c) \subseteq \Psi(d)$ implies by looking at the supports that $\Psi(c)$ can only belong to $\mathcal{L}_4 \cup \mathcal{L}_5$

- $\Psi(c) \in \mathcal{L}_4$, i.e. $\Psi(c) = (p^*, \top^*, q^*)$, $p, q \notin \{\bot, \top\}$. Let us prove by contradiction that

$$\Psi(c) \not\subseteq \Psi(d)$$

Let us suppose $\Psi(c) \subseteq \Psi(d)$, then for any $\sigma \cdot \rho \in \Psi(c)$ there exists $\mu, \nu \in (x^*, p^*) \times (q^*, y^*)$ such that

$$\nu \cdot \sigma \cdot \rho \cdot \mu \in (x^*, y^*)$$

The contraposition of Lemma 4.2.14 implies $\top \notin \nu \cdot \sigma \cdot \rho \cdot \mu$, which contradicts the fact that by definition $\top^* \in \sigma \cdot \rho$.

- $\Psi(c) \in \mathcal{L}_5$. $\Psi(c) = (p^*, q^*) \neq (\bot^*, \bot^*)$. Then $\Psi(c) = (p^*, q^*) \subseteq (x^*, y^*) = \Psi(d)$ implies by Lemma 4.3.16, $(p, q) \subseteq (x, y)$ and by induction rules

$$(p; \bot, q; \bot) \subseteq (x; \bot, y; \bot) \approx d$$

$$(\top; p, \top; q) \subseteq (\top; x, \top; y) \approx d$$

As $c \in \{(p; \bot, q; \bot), (\top; p, \top; q)\}$ by definition, this concludes the proof. $\square$

**Remark 4.3.23.** If the program $P^*$ is conservative, then $P \neq P_a, V_a$, as otherwise $\Delta(P) \neq 0$. Thus, for all $P \in \mathbf{Pgrm}$, with $P$ conservative there are no sub-programs of the form $P_a^*$ or $V_a^*$.

**Proposition 4.3.24.** Given a conservative program $P = \in \mathbf{Pgrm}$, a maximal conservative cover $R$ of $P$ and $c, d \in \mathcal{C}^{\max}(\Psi^{-1}(R))$, we have

$$\Psi(c) \subseteq \Psi(d) \implies \exists d' \in \Psi^{-1}(\Psi(d)) \text{ such that } c \subseteq d'$$

*Proof.* By induction on $P$.

* $P \in \mathbf{Prcs}$. Trivial.

* $P \in \mathbf{Prcs}^*$. By Remark 4.3.23 we can apply Proposition 4.3.22.

* $P = P_1 \parallel P_2$. Let $c, d \in \mathcal{C}(\Psi^{-1}(R))$, i.e. $c = c_1 \times c_2$, $d = d_1 \times d_2$. Then, by Proposition 4.3.7

$$c = c_1 \times c_2 \in \pi_1 R_c \times \pi_2 R_c$$

$$d = d_1 \times d_2 \in \pi_1 R_d \times \pi_2 R_d$$

with $\pi_i R_c$ and $\pi_i R_d$ conservative maximal. Then $\Psi(c) \subseteq \Psi(d)$ implies

$$\Psi(c_1) \subseteq \Psi(d_1) \text{ and } \Psi(c_2) \subseteq \Psi(d_2)$$

By induction hypothesis, there exists $d' = d'_1 \times d'_2 \in \Psi^{-1}(\Psi(d_1)) \times \Psi^{-1}(\Psi(d_2)) = \Psi^{-1}(\Psi(d))$ such that $c \subseteq d'$. $\square$
### 4.3.3.3 Maximal cubical cover as a quotient of the 2-unfolding

Given a conservative program $P$, $\Psi_P$ actually lifts all cubes of a conservative region $X$ to the cubes of its unfolding $\Phi^{-1}(X)$. But this lifting is not surjective, as all cubes in $\Pi_{\mathcal{U}(P)}C_{-1}$ do not have an image by $\Psi$. This constraint disappears when considering the maximal cubes, as cubes of $\Pi_{\mathcal{U}(P)}C_{-1}$ are not maximal in unfolding of conservative regions (proved in Proposition 4.3.25 below).

One thing to remember is that the cube $(\perp, \top^*, \top)$ (and thus all cubes in $\Pi_P \mathcal{L}_{-1}$) do not have an antecedent by $\Psi$.

**Proposition 4.3.25.** Given a program $P \in \mathbf{Pgrm}$ and $R$ a maximal conservative cover on $\mathcal{P}(P)$, we have

$$C^{\max}([\Psi^{-1}(R)]) \cap \Pi_{\mathcal{U}(P)}C_{-1} = \emptyset$$

*Proof.* Let $P \in \mathbf{Pgrm}$ and $R$ a maximal conservative cover of $P$. If $[R] = \mathcal{P}(P)$, then $R = \{(\perp, \top)\}$ by Proposition 4.3.21, which concludes the proof. We can then suppose that $[R] \neq \mathcal{P}(P)$ for the rest of the proof. Let us prove the property by induction on the program $P$.

* $P \in \mathbf{Prcs}$. Then $\Pi_{\mathcal{U}(P)}C_{-1} = \emptyset$, which concludes the proof.

* $P = Q^*$. Then $C_{\mathcal{U}(P)}^m \setminus \Psi^{-1}(R) = C_{Q;Q}^m \setminus \Phi^{-1}(R)$.

- If $[R] = \mathcal{P}(P)$, then $R = \{(\perp, \top)\}$ and thus

$$\Psi^{-1}(R) = \{(\perp, \top)\} = C^{\max}([\Psi^{-1}(R)])$$

- Otherwise, let us prove by contradiction that

$$C^{\max}([\Psi^{-1}(R)]) \cap C_{-1} = \emptyset$$

Let us suppose $c \in C_{-1} \cap C^{\max}(\Phi^{-1}[R])$. This implies

$$[\perp; \perp; \top; \top] \subseteq \Phi^{-1}[R] \text{ or } [\top; \perp; \top; \top] \subseteq \Phi^{-1}[R]$$

In both cases, this implies $\{q^* | q \in \mathcal{P}(Q)\} \subseteq \Phi(\Phi^{-1}[R]) = [R]$. By conservativeness $\top^* \in R$ also implies $\perp, \top \in R$. Thus, $\mathcal{P}(Q^*) \subseteq R$, which contradicts our hypothesis on $R$. Thus,

$$C_{-1} \cap C^{\max}(\Phi^{-1}[R]) = \emptyset$$

* $P = P_1 \parallel P_2$. By Proposition 4.3.5, $\Phi^{-1}[R]$ is conservative, thus by Theorem 4.3.15, $S = C^{\max}(\Psi^{-1}(R))$ is also conservative. By Proposition 4.3.7, for all $c = c_1 \times c_2 \in S$ the sets

$$\pi_1 S_c = \{c' \in \mathcal{P}(P_1) | c' \times c_2 \in S\} \text{ and } \pi_1 S_c = \{c' \in \mathcal{P}(P_2) | c_1 \times c' \in S\}$$

are conservative and maximal. By definition, $c_i \in \pi_i R_c$ for $i = 1, 2$ and by induction hypothesis, this implies $c_i \notin \Pi_{\mathcal{U}(P_i)}C_{-1}$. Thus, $c \notin \Pi_{\mathcal{U}(P)}C_{-1}$

□
**Proposition 4.3.26.** Given a conservative program $P \in \mathbf{Pgrm}$ and $R$ a conservative maximal cover of $P$, we have

$$C(\Psi^{-1}(R)) \setminus \Pi_{\mathcal{U}(P)}C_{-1} = \Psi^{-1}(C(R))$$

*Proof.* We recall that $\Psi^{-1}(C(R)) = \Psi^{-1}((C(R)) \setminus \Pi_P \mathcal{L}_{-1})$. If $[R] = \emptyset$, then

$$C(\Psi^{-1}(R)) = \emptyset = \Psi^{-1}(C(R))$$

Which concludes the proof. Thus, for the rest of the proof, we will suppose $[R] \neq \emptyset$.

* Let $c \in \Psi^{-1}(R)$. We want to prove that $c \in C(\Psi^{-1}(R)) \setminus \Pi_{\mathcal{U}(P)}C_{-1}$. By definition of $\Psi$, $c \notin \Pi_{\mathcal{U}(P)}C_{-1}$. Thus, we simply need to prove that

$$c \in C(\Psi^{-1}(R))$$

Then $c \in \Psi^{-1}(R)$ implies that there exists $d \in R$ such that $\Psi(c) = d$. Then,

$$\begin{align*}
\Phi([c] \cap [\Psi^{-1}](R)) &\subseteq \Phi[c] \cap \Phi[\Psi^{-1}(R)] \\
&\subseteq [\Psi(c)] \cap \Phi[\Psi^{-1}(R)] & \text{Proposition 4.2.44} \\
&\subseteq [\Psi(c)] \cap \Phi[\Phi^{-1}[R]] & \text{Theorem 4.3.15} \\
&\subseteq [d] \cap [R] \\
\Phi([c] \cap [\Psi^{-1}](R)) &\subseteq \emptyset
\end{align*}$$

Thus by definition of $\Phi$, this implies $[c] \cap [\Psi^{-1}](R) = \emptyset$ i.e.

$$c \in C(\Psi^{-1}(R))$$

* Let us prove that

$$C(\Psi^{-1}(R)) \setminus \Pi_{\mathcal{U}(P)}C_{-1} \subseteq \Psi^{-1}(C(R))$$

i.e. for all $c \in C(\Psi^{-1}(R)) \setminus \Pi_{\mathcal{U}(P)}C_{-1}$, we have

$$\Psi(c) \in C(R)$$

As $c \notin \Pi_{\mathcal{U}(P)}C_{-1}$, $\Psi(c)$ is correctly defined. Now, by contradiction let us suppose there exists $q \in [\Psi(c)] \cap [R]$. $q \in [\Psi(c)] = \Phi[c]$ (by Proposition 4.2.44) implies that there exists $p \in [c]$ such that $\Phi(p) = q$, i.e.

$$p \in \Phi^{-1}(q) \subseteq \Phi^{-1}[R] = [\Psi^{-1}(R)] \quad \text{Theorem 4.3.15}$$

Then $p \in [c] \cap [\Psi^{-1}(R)] = \emptyset$ by definition. As this is impossible, we get $[\Psi(c)] \cap [R] = \emptyset$, i.e.

$$\Psi((C(\Psi^{-1}(R))) \setminus \Pi_{\mathcal{U}(P)}C_{-1}) \subseteq C(R) \setminus \Pi_P \mathcal{L}_{-1}$$

Thus by applying $\Psi^{-1}$, we get

$$(C(\Psi^{-1}(R))) \setminus \Pi_{\mathcal{U}(P)}C_{-1} \subseteq \Psi^{-1}(C(R)) \quad \square$$
Combining both Proposition 4.3.24 and Proposition 4.3.18, we can finally prove that $\Psi^{-1}$ sends maximal covers onto maximal covers. Thus, $\Psi$ defines an equivalence between the maximal cubes of a conservative region $X$ of a program $P$ and the quotient of the set of maximal cubes of $\Phi^{-1}(X)$ by the equivalence relation of Definition 4.2.37.

**Theorem 4.3.27.** Given a conservative program $P \in \mathbf{Pgrm}$ and $R$ a conservative maximal cover of $P$, we have

$$C^{\max}(\Psi^{-1}(R)) = \Psi^{-1}(R)$$

*Proof.* We first remind ourselves that, by definition $\Psi^{-1}(R) = \Psi^{-1}(R \setminus \Pi_P \mathcal{L}_{-1})$. Thus, we can instead prove

$$C^{\max}(\Psi^{-1}(R)) = \Psi^{-1}(R \setminus \Pi_P \mathcal{L}_{-1})$$

* Let us prove

$$\Psi^{-1}(R \setminus \Pi_P \mathcal{L}_{-1}) \subseteq C^{\max}(\Psi^{-1}(R))$$

Let $c \in R \setminus \Pi_P \mathcal{L}_{-1}$, $d \in \Psi^{-1}(c)$. By Proposition 4.3.26, $d \in C(\Psi^{-1}(R))$. Now let us prove that $d$ is maximal. Let us suppose that there exists

$$d' \in C^{\max}(\Psi^{-1}(R)), d \subseteq d'$$

Then by Proposition 4.3.19

$$c = \Psi(d) \subseteq \Psi(d') \in R \setminus \Pi_P \mathcal{L}_{-1}$$

By maximality of $c$ this implies, $d' \in \Psi^{-1}(c)$. Thus, by the contraposition of Proposition 4.2.40 for $d, d' \in \Psi^{-1}(c)$, we get $d = d'$, thus $d$ is maximal and

$$\Psi^{-1}(R \setminus \Pi_P \mathcal{L}_{-1}) \subseteq C^{\max}(\Psi^{-1}(R))$$

* We want to show that

$$C^{\max}(\Psi^{-1}(R)) \subseteq \Psi^{-1}(R \setminus \Pi_P \mathcal{L}_{-1})$$

i.e. that for every $c \in C^{\max}(\Psi^{-1}(R))$, $\Psi(c) \in R$. By Proposition 4.3.19, $\Psi(c) \in C(R)$, with $R$ maximal. Thus, there exists $d \in R$, such that

$$\Psi(c) \subseteq d$$

By the inclusion $\Psi^{-1}(R \setminus \Pi_P \mathcal{L}_{-1}) \subseteq C^{\max}(\Psi^{-1}(R))$ proved above, there exists $c' \in C^{\max}(\Psi^{-1}(R))$ such that $d = \Psi(c')$, which implies

$$\Psi(c) \subseteq \Psi(c')$$

As $c \in C^{\max}(\Psi^{-1}(R))$, we can apply Proposition 4.3.24, thus $\exists r \in \Psi^{-1}(\Psi(c'))$, $c \subseteq r$. By maximality of $c$, $r = c$, i.e. $\Psi(c) = \Psi(r) = \Psi(c') \in R$. $\square$

For programs, in particular for Algorithm 3.3.23, we are given a cover of the forbidden region, and we wish to compute the authorized region from there. This means that we require a bit more than Theorem 4.3.27 if we wish to implement Algorithm 3.3.23 via the unfolding.
**Theorem 4.3.28.** Given a conservative program $P \in \mathbf{Pgrm}$ and $R$ a conservative maximal cover of $P$, we have

$$ (\Psi^{-1}(R))^c = \Psi^{-1}(R^c) $$

where for any cover $S$, $S^c = C^{\max}([S]^c)$.

*Proof.* As $R$ is conservative, by Proposition 4.3.6, so is $R^c$. Then by applying Theorem 4.3.27 to $R^c$ maximal conservative, we get

$$ \begin{align*} \Psi^{-1}(R^c) &= C^{\max}(\Psi^{-1}(R^c)) \\ &= C^{\max}(\Phi^{-1}([R^c])) \tag*{Theorem 4.3.15} \\ &= C^{\max}(\Phi^{-1}([R]^c)) \\ &= C^{\max}((\Phi^{-1}[R])^c) \\ &= C^{\max}([\Psi^{-1}(R)^c]) \tag*{Theorem 4.3.15} \end{align*} $$

$$ \Psi^{-1}(R^c) = (\Psi^{-1}(R))^c \qquad \text{by maximality of } (\Psi^{-1}(R))^c $$

□

## 4.4 Deadlock detection algorithm for looped programs

In this section we finally implement the extension of Algorithm 3.3.23 for programs with loops. We recall that the idea behind this algorithm is to first generate a cubical partition of the authorized region that is compatible with the maximal cubical cover. Then, cubes are arranged in order to reflect reachability but on the level of cubes instead of points.

This guarantees that the cubes that do not contain the terminal position $\top$ but do not lead to another cube are deadlocks. Any cube that lead to a deadlock is unsafe, and cubes leading only to deadlocks are doomed.

Now that cubes are properly defined on semantics of programs with loops, one could implement intersection and complement of cubes for looped syntactic semantics. There are some difficulties in setting up intersection and complements as they do not behave very well in the case of loops, but it is entirely possible. Proving that the generic partition is still a partition is also not trivial.

We do not opt for this approach, instead, we study the generic partition of the base programs through the generic partition of its unfolding. Indeed, we already know that the maximal covers of forbidden and authorized regions lift, so it is natural to check if the generic partition also lifts directly to its unfolding. This is not the case, but through some manipulation, which consists of separating the cubes at the lifting of the core of the loop, we get the same lifting property for the cubical partition. This is detailed in Example 4.4.1 below.

*Example 4.4.1.* Given a resource of capacity $\kappa_a = 0$, let us consider a very simple program $P = (P_a; V_a)^*$, whose semantics is given below.
<figure><img src="image_184.png" /></figure>

Now if we consider the lifting, on its unfolding $U(P) = (P_a; V_a); (P_a; \bar{V}_a)$, of the generic partition (on the bottom below) we can see that it is finer than the partition of the lifting (on top below)

<figure><img src="image_185.png" /></figure>

*Remark 4.4.2.* The same phenomena appear for more classical parallel programs. Indeed, if one looks at $P = (P_a; V_a)^* \parallel P_a; \bar{V}_a$, with $\kappa_a = 1$ which would be a “looped” version of the floating square (Example 1.4.3), a similar result holds.

As the separation operations detailed above do not impact reachability of cubes, this transformation does not affect the algorithm. Then to get the generic partition of the base program, as well as the unsafe and doomed regions we simply apply the algorithm on the unfolding.

We start by introducing formally the core-cutting operators before extending the lifting property of Theorem 4.3.28 to the generic cubical partition, proving that the generic cubical partition of the base program corresponds to the quotient of the cubical partition of the unfolding.

Finally, we prove that there is an equivalence for the relation “being in the past of” (Definition 1.4.31) between cubes of the base program and their lifting.

All this allows us to implement a modified version of Algorithm 3.3.23 on the unfolding of a program, which allows us to detect deadlocks in the base programs (which potentially has loops).

### 4.4.1 Cubical partition and loops

In this section we will prove that the lifting property of Theorem 4.3.27 extends to the cubes of the generic partition (Definition 4.1.1) of the maximal cover. We recall that this generic partition is the one we use to represent the set of positions in Algorithm 3.3.23 and compute deadlocks.
**Definition 4.4.3.** Given a cover $R$ on a sequential program $P$, we define the 1-dimensional generic cubical partition as

$$ \Gamma_1^m(R) = \bigcup_{\substack{U \cup V = R \\ U \neq \emptyset}} \mathcal{C}^{\max}(Z_{U,V}) $$

$$ \text{with } Z_{U,V} = \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^c $$

**Definition 4.4.4.** Given a cover $R$ on the parallel composition of $n$ sequential programs $P = P_1 \parallel \cdots \parallel P_n$, we define the generic cubical partition as

$$ \Gamma^*(R) = \Gamma^m \circ \Gamma^m(R) $$

where $\Gamma^m(R)$ is defined as

$$ \Gamma^m(R) = \prod_{i=1}^{n} \Gamma_1^m(\{c_i \mid \exists (r_k)_{1 \le k \le n} \in R, r_i = c_i\}) $$

*Remark 4.4.5.* For now, we do not prove that the generic partition is a partition. That is not necessary as it will be a consequence of Theorem 4.4.45.

As seen in Example 4.4.1, we cannot directly prove that the lifting and the generic partition commute. In order to enforce the commutation, we define what we call the core-cutting operators, which separates the cubes of the partition of the unfolding in order to replicate what happens at the core of the loop in the base program.

*Remark 4.4.6.* Given a program $P^*$, there is one maximal conservative cubical cover that does not get cut when taking its cubical partition: that is the cover $R = \{(\perp, \top)\}$. Here, we will cut this cube in the unfolding, meaning that we will need to cut it in the final partition. This should not be needed, but no proof circumventing this problem could be found.

The idea is that for a loop, as shown in Example 4.4.1, conservative regions crossing the core of the loop $p^*$ are separated in four disjoint regions by the generic partition: before the loop, at the core of the loop, strictly inside the loop and after the loop.

In the unfolding, as the partition does not provide this kind of action, we need to do it ourselves. Where we need to cut is given by the Example 4.4.1 and is quite naturally at the lifting of the core $\top^*$, thus separating the cubes of the lifting in exactly the right way.

This cutting operation is formalized through the operator $\Theta$ for the unfolding and $\chi$ for the base program.

**Definition 4.4.7.** Given a program $P \in \mathbf{Prcs}^*$, we define the unfolded-core-cutting operator $\Theta_P$ on cubes of $P$ as follows.

$$ \Theta_{\mathcal{U}(P)}: \mathcal{C}(\mathcal{U}(P)) \to \mathcal{R}(\mathcal{U}(P)) \\ c \mapsto \begin{cases} \mathcal{C}^{\max}([c] \setminus \Phi^{-1}(\top^*)) & \text{if } P = Q^* \\ \bigcup_{x \in \Phi^{-1}(\top^*)} \mathcal{C}^{\max}([c] \cap \{x\}) & \\ \{c\} & \text{otherwise} \end{cases} $$
And for parallel composition $P = \mathcal{U}(P_1)\|\mathcal{U}(P_2)$ we define

$$ \Theta_{\mathcal{U}(P_1)\|\mathcal{U}(P_2)}: \mathcal{C}(\mathcal{U}(P_1)\|\mathcal{U}(P_2)) \to \mathcal{R}(\mathcal{U}(P_1)\|\mathcal{U}(P_2)) \\ c_1\|c_2 \mapsto \Theta_{\mathcal{U}(P_1)}(c_1) \times \Theta_{\mathcal{U}(P_2)}(c_2) $$

Then we can easily extend $\Omega_P$ to regions of $P$ as follows.

$$ \Theta_{\mathcal{U}(P)}: \mathcal{R}(\mathcal{U}(P)) \to \mathcal{R}(\mathcal{U}(P)) \\ \{c_i \mid i \in I\} \mapsto \bigcup_{i \in I} \Theta_{\mathcal{U}(P)}(c_i) $$

**Definition 4.4.8.** Given a program $P \in \mathbf{Prcs}^*$, we define the $\Pi_P \mathcal{L}_{-1}$ core-cutting operator $\chi_P$ on cubes of $P$ as follows.

$$ \chi_P: \mathcal{C}(P) \to \mathcal{R}(P) \\ c \mapsto \begin{cases} \mathcal{C}^{\max}([c] \setminus \{\top^*\}) & \text{if } c = (\bot, \top) \text{ and } P = Q^* \\ \cup \mathcal{C}^{\max}([c] \cap \{\top^*\}) & \\ \{c\} & \text{otherwise} \end{cases} $$

And for parallel composition $P = P_1\|P_2$ we define

$$ \chi_{P_1\|P_2}: \mathcal{C}(P_1\|P_2) \to \mathcal{R}(P_1\|P_2) \\ c_1\|c_2 \mapsto \chi_{P_1}(c_1) \times \chi_{P_2}(c_2) $$

Then we can easily extend $\chi_P$ to regions of $P$ as follows.

$$ \chi_P: \mathcal{R}(P) \to \mathcal{R}(P) \\ \{c_i \mid i \in I\} \mapsto \bigcup_{i \in I} \chi_P(c_i) $$

**Example 4.4.9.** Let us consider the program $(\mathbf{skip}+\mathbf{skip});(\mathbf{skip}+\mathbf{skip})$ whose semantics is given below. On the left we see the result of $\mathcal{C}^{\max}([\bot, \top] \setminus \Phi^{-1}(\top^*))$ and on the right the result of $\bigcup_{x \in \Phi^{-1}(\top^*)} \mathcal{C}^{\max}([\bot, \top] \cap \{x\})$

<figure><img src="image_186.png" /></figure>

**Example 4.4.10.** Let us consider the cube $(\bot, \top)$ on the program $(\mathbf{skip}+\mathbf{skip})^*$ which unfolds to the program of Example 4.4.9. Its semantics are shown on the left with the support of $(\bot, \top)$ in grey. The result by the operator $\chi$ is given on the right.
<figure><img src="image_187.png" /></figure>

If $\Theta$ left the cube $(\perp, \top)$ untouched, the operator $\chi$ would be totally unnecessary, as indeed the generic partition of the lifting is equal to $(\perp, \top)$ which is equal to the lifting of the generic partition. Unfortunately, this breaks the fact that cubes included in the support of a cube in the image of $\Theta$ are stable by $\Theta$, which we needed in our proof of Theorem 4.4.45 (more precisely Proposition 4.4.37 and accompanying lemmas).

With this choice, we can now formulate the first main theorem of this chapter

**Theorem 4.4.45.** Given a program $P \in \mathbf{Pgrm}$ and a maximal conservative cover $R$ on $P$ we have

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Psi^{-1} \circ \Gamma^*(\chi(R)) $$

This is a tall order, so we break down the proof in smaller proofs, each time proving a step of the commutation.

We also introduce a third separation operator $\Omega$ that performs the same separation as $\chi$ but to all cubes.

**Definition 4.4.11.** Given a program $P \in \mathbf{Prcs}$, we define the core-cutting operator $\Omega_P$ on cubes of $P$ as follows.

$$ \Omega_{P^*}: \mathcal{C}(P^*) \to \mathcal{R}(P^*) \\ (p, q) \mapsto \begin{cases} \mathcal{C}^{\max}([c] \setminus \{\top^*\}) & \text{if } c = (p, q) \\ \cup \mathcal{C}^{\max}([c] \cap \{\top^*\}) \\ \Omega(p, \top^*) \cup \Omega(\top^*, q) & \text{if } c = (p, \top^*, q) \end{cases} $$

Otherwise, when not dealing with loops, $\Omega$ sends each cube to the region containing only that cube.

$$ \Omega_P: \mathcal{C}(P) \to \mathcal{R}(P) \\ c \mapsto \{c\} $$

And for parallel composition $P = P_1 \Vert P_2$ we define

$$ \Omega_{P_1 \Vert P_2}: \mathcal{C}(P_1 \Vert P_2) \to \mathcal{R}(P_1 \Vert P_2) \\ c_1 \Vert c_2 \mapsto \Omega_{P_1}(c_1) \times \Omega_{P_2}(c_2) $$
Then we can easily extend $\Omega_P$ to regions of $P$ as follows.

$$ \Omega_P : \mathcal{R}(P) \to \mathcal{R}(P) \\ \{c_i \mid i \in I\} \mapsto \bigcup_{i \in I} \Omega_P(c_i) $$

*Remark 4.4.12.* For all operators we omit the subscript when it is obvious from the context.

*Example 4.4.13.* Let us consider the program $(skip+skip)^*$ whose semantics is given below. We show the action of the operator $\Omega$ on the cubes $(\perp, (\top+\emptyset)^*)$ and $((\top+\emptyset)^*, \perp)$.

<figure><img src="image_188.png" /></figure>

This operator will be very useful in the proof of Theorem 4.4.45. Indeed instead of proving Theorem 4.4.45 we can first prove the weaker Proposition 4.4.38.

**Proposition 4.4.38.** Given a program $P \in \mathbf{Pgrm}$ and a maximal conservative cover $R$ on $P$ we have

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Psi^{-1} \circ \Gamma^* \Omega(R) $$

The proof of Proposition 4.4.38 will consists in proving the commutativity of the following diagram, in which we will prove all commutative squares individually.
<figure><img src="image_189.png" /></figure>

We define an object that appears in most of our proofs. This corresponds to the cover of one of the elements of our cubical partition. This was already introduced in previous section, but is reminded here as it will be frequently used in the following proofs.

**Definition 4.4.14.** For a partition $U \amalg V = R$ of a cover $R$, the associated support separation $Z_{U,V}$ is defined as follows

$$Z_{U,V} = \bigcap_{u \in U} [u] \cap \bigcap_{v \in V} [v]^c$$

### 4.4.2 Cubical partition as a quotient of the 2-unfolding

$$\Psi^{-1} \circ \Omega = \Theta \circ \Psi^{-1}$$

In this section we will prove the commutation of the lifting with the separation operators.

**Proposition 4.4.21.** Given a program $P \in \mathbf{Prcs}^*$, $R$ a maximal conservative cover on $P$. Then

$$\Psi^{-1} \circ \Omega(R) = \Theta \circ \Psi^{-1}(R)$$

In order to do so, we will fully characterize the image of $\Theta$ and $\Omega$ in Proposition 4.4.17 and Proposition 4.4.18. Indeed, $\Theta$ actually creates a cubical partition when cutting the cubes, and those can be computed by looking at the successors and predecessors of the core's lifting. Indeed, there is only a single pair of cubes that creates a non-empty-cube w.r.t. the cube being cut.

*Example 4.4.15.* Let us look at the action of $\theta$ on some of the more problematic cubes of the program $P = \mathcal{U}((\text{skip}+\text{skip})^*)$. The cube $((\top + \emptyset); \bot, \top)$ shown below on the left is properly partitioned by $\theta$ as shown on the right. The fact that a copy of the loop is separated in disjoint is a consequence of Lemma 4.4.16 as explained above.

<figure><img src="image_190.png" /></figure>
Unfortunately, such a property doesn't hold for $\Omega$ as the separation of composite cubes might lead to some overlapping as shown below on the cube $((\top + \emptyset)^*, \top^*, (\top + \emptyset)^*)$

<figure><img src="image_191.png" /></figure>

Then Proposition 4.4.20 allows us to link the cubes of $\Theta$ and $\Omega$ through these unique antecedents.

**Lemma 4.4.16.** Let $P \in \mathbf{Prcs} \setminus \alpha$. Let $p, q \in \mathcal{P}(P) \setminus \{\bot, \top\}$. Then

* There exists a unique element $\overline{\top}_p \in \text{pred}\top$, such that a path $p \to^* \overline{\top}_p \to \top$ exists and is without trivial loops.

* There exists a unique element $\overline{\bot}_p \in \text{succ}\bot$, such that a path $\bot \to \overline{\bot}_q \to q$ exists and is without trivial loops.

*Proof.* Let $P \in \mathbf{Prcs} \setminus \alpha$. Let $p, q \in \mathcal{P}(P) \setminus \{\bot, \top\}$. Let us prove the property for $\overline{\top}_p$, the other property being dual.

* If $P = S;T$. Then $\text{pred}\top = \top;\top$. And it is easy to show that $p < \top$ implies $p \le \top;\top \le \top$. By Proposition 4.1.33, this implies $p \to^* \top;\top \to \top$. As the program $P$ is loop-free, the path is cycle-free and $\overline{\top}_p = \top;\top$.

* If $P = S+T$. Then $\text{pred}\top = \{\emptyset+\top, \top+\emptyset\}$. $\bot < p < \top$ implies $p = s+\emptyset$ or $p = \emptyset+t$.

- If $p = s+\emptyset$ Then $s+\emptyset \not\le \emptyset+\top$. Thus, by Proposition 4.1.33, there is no path $s+\emptyset \to^* \emptyset+\top$. By the same argument, as $s+\emptyset \le \top+\emptyset$ there is a path $s+\emptyset \to^* \top+\emptyset$. As the program $P$ is loop-free so are all the paths. Thus, $\overline{\top}_p = \top+\emptyset$.

- If $p = \emptyset+t$, then, by a similar argument $\overline{\top}_p = \emptyset+\top$.

□

**Proposition 4.4.17.** Given a program $\mathcal{U}(P^*)$, and two positions $p, q$ of $\mathcal{U}(P^*)$, such that $p, q \notin \{\bot, \top\}$ and a cube $c \in \mathcal{C}_0$ we have

$$ \Theta(p; \bot, q; \bot) = \{(p; \bot, q; \bot)\} $$

$$ \Theta(\top; p, \top; q) = \{(\top; p, \top; q)\} $$

$$ \Theta(\bot, \bot; \bot) = \{(\bot, \bot), (\bot; \bot, \bot; \bot)\} $$

$$ \Theta(\top; \top, \top) = \{(\top, \top), (\top; \top, \top; \top)\} $$

$$ \Theta(\bot; \top, q; \bot) = \{(\bot; \top, \bot; \bot), (\overline{\bot}_q; \bot, q; \bot)\} $$

$$ \Theta(\top; \bot, \top; q) = \{(\top; \bot, \top; \bot), (\top; \overline{\bot}_q, \top; q)\} $$

$$ \Theta(p; \bot, \top; \bot) = \{(\top; \bot, \top; \bot), (p; \bot, \overline{\top}_p; \bot)\} $$

$$ \Theta(\top; p, \top; \top) = \{(\top; \top, \top; \top), (\top; p, \top; \overline{\top}_p)\} $$

$$ \Theta(c) = \{c\} $$
$$ \Theta(\perp, \top) = C_0 \cup \{(x; \perp, \overline{\top}_x; \perp), (\top; x, \top; \overline{\top}_x) \mid x \in \text{succ}\perp\} $$

*Proof.* Given a program $\mathcal{U}(P^*)$, we have the first three cases directly by definition of $\Theta$.

* The cases $c \in C_0$, $(\perp, \perp; \perp)$, $(\top; \top, \top)$ are easily deduced from the definition of $\Theta$.

* Let us consider the case $(p; \perp, q; \perp)$. Then, we have $[p; \perp, q; \perp] \subseteq \{\top^*\}^c$. Thus, by definition of $\Theta$, $\Theta(p; \perp, q; \perp) = C^{\max}([p; \perp, q; \perp]) = \{(p; \perp, q; \perp)\}$

* The case $(\top; p, \top; q)$ is dual to the previous case.

* For the case $(\perp, \top)$, we first prove

$$ \Theta(\perp; \top, \top; \top)\{(\perp; \perp, \perp; \perp), (\top; \perp, \top; \top)\} \cup \{(x; \perp, \overline{\top}_x; \perp) \mid x \in \text{succ}\perp\} $$

Indeed, by Lemma 4.4.16 for any $p; \perp, q; \perp$ there exist a unique pair, $x, y$ such that $\perp \to x \to^* p \to^* q \to^* y \to \top$. Furthermore, $y = \overline{\top}_x; \perp$ and by inference rules we can show that the cubes $(x; \perp, \overline{\top}_x; \perp)$ are exactly the maximal cubes of $[\perp; \perp, \top; \top] \setminus \{\perp; \perp, \top; \top\}$. Thus,

$$ \Theta(\perp; \top, \top; \top)\{(\perp; \perp, \perp; \perp), (\top; \perp, \top; \top)\} \cup \{(x; \perp, \overline{\top}_x; \perp) \mid x \in \text{succ}\perp\} $$

Similarly

$$ \Theta(\top; \perp, \top; \top)\{(\perp; \perp, \perp; \perp), (\top; \perp, \top; \top)\} \cup \{(\top; x, \top; \overline{\top}_x) \mid x \in \text{succ}\perp\} $$

then we conclude by remarking that we can decompose $(\perp, \top)$ as the composite of the cubes $(\perp, \perp; \perp)$, $(\perp; \perp, \top; \perp)$, $(\top; \perp, \top; \top)$ and $(\top; \top, \top)$.

* $(\perp; \perp, q; \perp)$ follows a similar proof to the case $\Theta(\perp; \perp, \top; \perp)$ in the case above, where we take $y = q$.

* The case $(\top; \perp, \top; q), (p; \perp, \top; \perp), (\top; p, \top; \top)$ are all treated similarly to the case above.

□

**Proposition 4.4.18.** Given a program $\mathcal{U}(P^*)$, two positions $p, q$ of $\mathcal{U}(P^*)$, such that $p, q \notin \{\perp, \top\}$, and a cube $c \in \mathcal{L}_0$, we have

$$ \begin{align*} \Omega(c) &= \{c\} & \Omega(p^*, q^*) &= \{(p^*, q^*)\} \\ \Omega(\perp, \top^*) &= \{(\top^*, \top^*), (\perp, \perp)\} & \Omega(p^*, \top^*) &= \{(p^*, \overline{\top}_p^*), (\top^*, \top^*)\} \\ \Omega(\top^*, \top) &= \{(\top^*, \top^*), (\top, \top)\} & \Omega(\top^*, q^*) &= \{(\overline{\top}_q^*, q^*) (\top^*, \top^*)\} \end{align*} $$

$$ \Omega(\perp, \top) = \{(\perp, \perp), (\top^*, \top^*), (\top, \top)\} \cup \{(x^*, \overline{\top}_x^*) \mid x \in \text{succ}\top\} $$

*Proof.* Given a program $\mathcal{U}(P^*)$, we have the first three cases directly by definition of $\Omega$.

* The cases $c \in C_0$, $(\perp, \top^*), (\top^*, \top)$ are easily deduced from the definition of $\Omega$.
* Let us consider the case $(p^*, q^*)$. Then, we have $[p^*, q^*] \subseteq \{\top^*\}^c$. Thus, by definition of $\Omega$, $\Omega(p^*, q^*) = C^{\max}([p^*, q^*]) = \{(p^*, q^*)\}$

* Let us consider the case $(p^*, \top^*)$. For all paths $\pi \in (p^*, \top^*)$, as $p \neq \bot, \top$, we have $\pi = \sigma^* \cdot \tau^*$ such that

$$ \sigma^*: p^* \to^{\text{lf}} x^* \text{ and } \tau^*: x^* \to \top^* $$

By Definition 4.2.13, we have $\sigma: p \to^{\text{lf}} x$ and by inference rules $\tau: x \to \top$. Thus, there is a cycle-free path $p \to^* x \to \top$. By Lemma 4.4.16 $x = \bar{\top}_p$. This implies

$$ [p^*, \top^*] = [p^*, \bar{\top}_p^*] \cup \{\top^*\} $$

Thus by definition of $\Omega$,

$$ \Omega(p^*, \top^*) = C^{\max}([p^*, \bar{\top}_p^*]) \cup C^{\max}(\{\top^*\}) $$

$$ \Omega(p^*, \top^*) = \{(p^*, \bar{\top}_p^*)\} \cup \{(\top^*, \top^*)\} $$

* $(\top^*, q^*)$. Dual to the case above.

* Let us consider the case $(\bot, \top)$. If $P = \alpha$ the proposition holds as $\{(x^*, \bar{\top}_x^*) | x \in \text{succ}\top\}$ is empty. Thus, for the rest of the proof, we will suppose

$$ \mathcal{P}(P) \setminus \{\bot, \top\} \neq \emptyset $$

then, by definition, for any pair of positions $(p, q) \in \mathcal{P}(P) \setminus \{\bot, \top\}$, there is a pair $x_p, y_q \in \text{succ}\bot \times \text{pred}\top$ such that $(p, q) \subseteq (x_p, y_q)$. Thus, by Lemma 4.3.16,

$$ (p^*, q^*) \subseteq (x_p^*, y_q^*) $$

Furthermore, by Lemma 4.4.16, $y_q = \bar{\top}_{x_p}$, and by inference rules $x_p \in \text{succ}\top$ This implies by Lemma 4.2.14 that $C^{\max}(\mathcal{P}(P^*) \setminus \{\bot, \top, \top^*\}) \subseteq \{(x^*, \bar{\top}_x^*) | x \in \text{succ}\top\}$ which concludes the proof. $\square$

<figure><img src="image_192.png" /></figure>

*Remark 4.4.19.* The Proposition 4.4.18 and Proposition 4.4.17 also imply that $\Theta$ and $\Omega$ can be computed if we know how to find the successors and predecessors of points as well as intersection of cubes. This is much quicker in practice than using the definition of $\theta$ which requires the calculation of many complements and intersection to obtain the same result.

**Proposition 4.4.20.** Let $P \in \mathbf{Prcs} \setminus \alpha$. Let $p, q \in \mathcal{P}(P) \setminus \{\bot, \top\}$

$$ \Psi^{-1}(p^*, \bar{\top}_p^*) = \{(\top; p, \top; \bar{\top}_p), (p; \bot, \bar{\top}_p; \bot)\} $$

$$ \Psi^{-1}(\bar{\bot}_q^*, q^*) = \{(\top; \bar{\bot}_q, \top; q), (\bar{\bot}_q; \bot, q; \bot)\} $$

*Proof.* By definition $\bar{\top}_p, \bar{\bot}_q \notin \{\bot, \top\}$. Thus, $(p^*, \bar{\top}_p^*)$, $(\bar{\bot}_q^*, q^*) \in \mathcal{L}_5$. By Proposition 4.2.36, we obtain our result. $\square$

<figure><img src="image_193.png" /></figure>
**Proposition 4.4.21.** Given a program $P \in \mathbf{Prcs}^*$, $R$ a maximal conservative cover on $P$. Then

$$ \Psi^{-1} \circ \Omega(R) = \Theta \circ \Psi^{-1}(R) $$

*Proof.* By induction on $P$

* $P \in \mathbf{Prcs}$. OK.

* $P = P_1 \parallel P_2$. By Proposition 4.3.7, for all $c = c_1 \times c_2 \in R$ the sets

$$ \pi_1 R_c = \{c' \in \mathcal{P}(P_1) \mid c' \times c_2 \in R\} \text{ and } \pi_1 R_c = \{c' \in \mathcal{P}(P_2) \mid c_1 \times c' \in R\} $$

are conservative and maximal and $R = \bigcup_{c \in R} \pi_1 R_c \times \pi_2 R_c$. Thus,

$$ \Psi^{-1} \circ \Omega(R) = \bigcup_{c \in R} \Psi^{-1} \circ \Omega(\pi_1 R_c) \times \Psi^{-1} \circ \Omega(\pi_2 R_c) $$

$$ \bigcup_{c \in R} \Theta \circ \Psi^{-1}(\pi_1 R_c) \times \Theta \circ \Psi^{-1}(\pi_2 R_c) \text{ by induction hypothesis} $$

$$ \Psi^{-1} \circ \Omega(R) = \Theta \circ \Psi^{-1}(R) $$

* $P = Q^*$. Then by definition of $R$,

- $\top^* \notin [R]$. Then, by Proposition 4.3.21,

$$ R = \{(p_i^*, q_i^*) \mid \forall i \in I, p_i, q_i \neq \bot, \top\} $$

As $\top^* \notin [R]$, a fortiori for all $i \in I$, $\top^* \notin [(p_i^*, q_i^*)]$, i.e. $\Omega((p_i^*, q_i^*)) = \{(p_i^*, q_i^*)\}$. Thus, for all $i \in I$

$$ \begin{aligned} \Psi^{-1}(\Omega(p_i^*, q_i^*)) &= \Psi^{-1}(p_i^*, q_i^*) \\ &= \{(p_i; \bot, q_i; \bot), (\top; p_i, \top; q_i)\} \\ &= \Theta(\{(p_i; \bot, q_i; \bot), (\top; p_i, \top; q_i)\}) \quad \text{as } p_i, q_i \neq \bot, \top \end{aligned} $$

$$ \Psi^{-1}(\Omega(p_i^*, q_i^*)) = \Theta(\Psi^{-1}(p_i^*, q_i^*)) $$

Thus, $\Psi^{-1} \circ \Omega(R) = \Theta \circ \Psi^{-1}(R)$

- $R \neq \{(\bot, \top)\}$ and $\top^* \in [R]$. Then by Proposition 4.3.21,

$$ R = \bigcup_{j \in J_1} \{(p_j^*, q_j^*)\} \bigcup_{j \in J_2} \{(\bot, q_j^*), (p_j^*, \top), (p_j^*, \top^*, q_j^*), (\bot, \top^*, \top)\} $$

Such that $p_j^*, q_j^* \neq \top^*$. By the same argument as the case above we have,

$$ \Psi^{-1} \circ \Omega(\bigcup_{j \in J_1} \{(p_j^*, q_j^*)\}) = \Theta \circ \Psi^{-1}(\bigcup_{j \in J_1} \{(p_j^*, q_j^*)\}) $$

Then, for each $j \in J_2$, we write

$$ R_j = \{(\bot, q_j^*), (p_j^*, \top), (p_j^*, \top^*, q_j^*), (\bot, \top^*, \top)\} $$

Then
$$ \ast \Omega(\perp, q_j^*) = \{(\perp, \perp), (\top^*, \top^*), (\vec{\perp}_{q_j}, q_j^*)\} $$

$$ \ast \Omega(p_j^*, \top) = \{(\top, \top), (\top^*, \top^*), (p_j^*, \overline{\top}_{p_j}^*)\} $$

$$ \ast \Omega(p_j^*, \top^*, q_j^*) = \{(\top^*, \top^*), (p_j^*, \overline{\top}_{p_j}^*), (\vec{\perp}_{q_j}, q_j^*)\} $$

$$ \ast \Omega(\perp, \top^*, \top) \subseteq \Omega(R_j \setminus (\perp, \top^*, \top)) $$

With $\Psi^{-1}(R_j) = \{(p; \perp, \top; q), (\perp, q; \perp), (\top; p, \top)\}$, we have

$$ \ast \Theta(\perp, q; \perp) = \{(\perp, \perp), (\perp; \perp, \perp; \perp), (\vec{\perp}_q; \perp, q; \perp)\} $$

$$ \ast \Theta(\top; p, \top) = \{(\top, \top), (\top; \top, \top; \top), (\top; p, \top; \overline{\top}_p)\} $$

$$ \ast \Theta(p; \perp, \top; q) = \{(p; \perp, \overline{\top}_p; \perp), (\top; \perp, \top; \perp), (\top; \vec{\perp}_q, \top; q)\} $$

Now as we have that

$$ \ast \text{By Proposition 4.4.20, } \Psi^{-1}(p^*, \overline{\top}_p^*) = \{(p; \perp, \overline{\top}_p; \perp), (\top; p, \top; \overline{\top}_p)\} $$

$$ \ast \text{By Proposition 4.4.20, } \Psi^{-1}(\vec{\perp}_q^*, q^*) = \{(\vec{\perp}_q; \perp, q; \perp), (\top; \vec{\perp}_q, \top; q)\} $$

$$ \ast \Psi^{-1}(\top^*, \top^*) = \{(\perp; \perp, \perp; \perp), (\top; \perp, \top; \perp), (\top; \top, \top; \top)\} $$

$$ \ast \Psi^{-1}(\perp, \perp) = (\perp, \perp) \text{ and } \Psi^{-1}(\top, \top) = (\top, \top) $$

We can conclude

$$ \Psi^{-1} \circ \Omega(R_j) = \Theta \circ \Psi^{-1}(R_j) $$

$$ \Psi^{-1} \circ \Omega(R) = \bigcup_{j \in J_1} \Psi^{-1} \circ \Omega(R) \{(p_j^*, q_j^*)\} \bigcup_{j \in J_2} \Psi^{-1} \circ \Omega(R)(R_j) $$

$$ = \bigcup_{j \in J_1} \Theta \circ \Psi^{-1} \{(p_j^*, q_j^*)\} \bigcup_{j \in J_2} \Theta \circ \Psi^{-1}(R_j) $$

$$ \Psi^{-1} \circ \Omega(R) = \Theta \circ \Psi^{-1}(R) $$

$$ - R = \{(\perp, \top)\}. \text{ By Proposition 4.4.18, we have} $$

$$ \Omega(\perp, \top) = \{(\perp, \perp), (\top, \top), (\top^*, \top^*)\} \cup \{(\vec{\perp}_q^*, q^*) | q \to \top\} $$

And Proposition 4.4.17, we have

$$ \Theta(\perp, \top) = \{(\perp, \perp), (\top, \top), (\perp; \perp, \perp; \perp), (\top; \perp, \top; \perp), (\top; \top, \top; \top)\} $$

$$ \cup \{(\vec{\perp}_q; \perp, q; \perp), (\top; \vec{\perp}_q, \top; q) | q \to \top\} $$

Using the same argument as the case above, we have thus,

$$ \Psi^{-1} \circ \Omega(R) = \Theta \circ \Psi^{-1}(R) $$

□

#### 4.4.2.2 $\Gamma^* \circ \Theta = \Theta \circ \Gamma^*$

In this section we prove the commutation of the separation operator $\Theta$ and the generic partition.
**Proposition 4.4.29.** Let $P \in \mathbf{Pgrm}$, for any conservative cover $R$ on a program $\mathcal{U}(P)$,

$$ \Theta \circ \Gamma^*(R) = \Gamma^* \circ \Theta(R) $$

We begin by stating a few of the important properties about $\Theta$, namely, the fact that $\Theta$ defines a cubical partition of the support of cubes it cuts and that it preserves and reflects inclusion of cubes to a degree.

**Lemma 4.4.22.** Given a program $P \in \mathbf{Pgrm}$ and a cube $c \in \mathcal{C}(\mathcal{U}(P))$, we have

$$ [\Theta(c)] = \prod_{d \in \Theta_P(c)} [d] = [c] $$

*Proof.* By induction on $P$.

* $P \in \mathbf{Prcs}$. Then $\Theta$ is the identity.

* $P = P_1 \parallel P_2$. Then, $c \in \mathcal{C}(\mathcal{U}(P))$ implies $c = c_1 \times c_2$ and

$$ \begin{align*} [\Theta(c)] &= [\Theta(c_1)] \times [\Theta(c_2)] \\ &= \prod_{d_1 \in \Theta_P(c_1)} [d_1] \times \prod_{d_2 \in \Theta_P(c_2)} [d_2] \quad \text{induction hypothesis} \\ [\Theta(c)] &= \prod_{d \in \Theta_P(c)} [d] \end{align*} $$

Furthermore,

$$ \begin{align*} [\Theta(c)] &= [\Theta(c_1)] \times [\Theta(c_2)] \\ &= [c_1] \times [c_2] \qquad \text{induction hypothesis} \\ [\Theta(c)] &= [c] \end{align*} $$

Which concludes the proof.

* $P = Q^*$. Then by definition of $\Theta$,

$$ \begin{align*} [\Theta(c)] &= [\mathcal{C}^{\max}([c] \setminus \Phi^{-1}(\top^*)) \bigcup_{x \in \Phi^{-1}(\top^*)} \mathcal{C}^{\max}([c] \cap \{x\})] \\ [\Theta(c)] &= [c] \setminus \Phi^{-1}(\top^*) \bigcup_{x \in \Phi^{-1}(\top^*)} [c] \cap \{x\}[\Theta(c)] \end{align*} $$

The fact that all cubes of $\Theta(c)$ are disjoint is a direct consequence of Proposition 4.4.17. The only case not directly treated $c \in \mathcal{C}_{-1}$ can be done so in the same manner as the case $(\perp, \top)$.

□

**Lemma 4.4.23.** Given a program $P \in \mathbf{Pgrm}$ and a cube $u \in \Theta(\mathcal{C}(P))$, then we have

* $\Theta_P \circ \Theta_P = \Theta_P$
• For any subset $X \subseteq [u]$, $C(X) \in \Theta(C(P))$

*Proof.* This holds directly by definition of $\Theta$. $\square$

**Lemma 4.4.24.** Given a program $P \in \mathbf{Pgrm}$ and $c, d \in C(\mathcal{U}(P))$, then $c \subseteq d$ implies for all $x \in \Theta(c)$, there exists $y \in \Theta(d)$ such that $x \subseteq y$

*Proof.* Let us prove the property by induction on $P$

• $P \in \mathbf{Prcs}$. Then $\Theta$ is the identity.

• $P = P_1 \parallel P_2$. Let $c = c_1 \times c_2 \subseteq d_1 \times d_2 = d$. Then $c_1 \subseteq d_1$ and $c_2 \subseteq d_2$. By induction hypothesis, this is implies for all $x_1, x_2 \in \Theta(c_1) \times \Theta(c_2) = \Theta(c)$, there exists $y_1 \times y_2 \in \Theta(d_1) \times \Theta(d_2) = \Theta(d)$ such that $x_1 \times x_2 \subseteq y_1 \times y_2$. Which concludes the proof.

• $P = Q^*$. Then by definition of $\Theta$,

$$ \begin{aligned} \Theta(c) &= C^{\max}([c] \setminus \{\Phi^{-1}(\top^*)\}) \bigcup_{x \in \Phi^{-1}(\top^*)} C^{\max}([c] \cap \{x\}) \\ &\leq C^{\max}([d] \setminus \{\Phi^{-1}(\top^*)\}) \bigcup_{x \in \Phi^{-1}(\top^*)} C^{\max}([d] \cap \{x\}) \\ \Theta(c) &\leq \Theta(q) \end{aligned} $$

where $\leq$ is the order on region defined in Definition 4.2.46. Thus, the property holds. $\square$

**Lemma 4.4.25.** Given a conservative cover $X$ on a program $\mathcal{U}(P)$, $P \in \mathbf{Prcs}^*$, such that $C(X) \cap C_{-1} = \emptyset$. Given $c \in C(X)$, $u \in \Theta(c)$. Then $u \subseteq v \in \Theta(C(X))$ implies that there exists $d \in C(X)$, such that $c \subseteq d$

*Proof.* By induction on $P$.

• $P \in \mathbf{Prcs}$. Then, $\theta$ is the identity on all cubes, concluding the proof.

• $P = L^*$, such that $\mathcal{U}(P) = L; L$. Given $s \in \Theta(C(X))$,

$$ s \in C_0 \cup C(\{q; \perp | q \in \mathcal{P}(L) \setminus \{\perp, \top\}\}) \cup C(\{\top; q | q \in \mathcal{P}(L) \setminus \{\perp, \top\}\}) $$

Then as $u \in \Theta(c) \subseteq \Theta(C(X))$ and $v \in \Theta(C(X))$ we can separate the different cases:

- $u \in C_0$. Then $v \neq u$ implies $u \not\subseteq v$. Thus, $v = u$ and $d = c$ verifies the conditions.

- $u \in C(\{q; \perp | q \in \mathcal{P}(L) \setminus \{\perp, \top\}\})$. Then $u \subseteq v$ implies $v$ is also a cube of $\{q; \perp | q \in \mathcal{P}(L) \setminus \{\perp, \top\}\}$. This implies:

* Either $c = (p, q; \perp)$, $p \leq \perp; \perp$, $q < \top$. This implies $u = (\perp_q; \perp, q; \perp)$. Then, $u \subseteq v$ implies $v = (\perp_q; \perp, t; \perp)$, $t \geq q$. We define, $d = (p, t; \perp)$. Then $c \subseteq d$, and $v \in \Theta(C(X))$ implies $d \in C(X)$

* or $c = (p; \perp, q)$, $p > \perp$ and $\top; \perp \leq q$, which is dual to the case above.

- $u \in C(\{\top; q | q \in \mathcal{P}(L) \setminus \{\perp, \top\}\})$. Similar to the case above.
<figure><img src="image_194.png" /></figure>

**Lemma 4.4.26.** Given a cover R, and any partition U ⋀ V = R, such that U ̸ =  . Then

$$
\coprod_{U_{\theta} \in S_U} \mathcal{C}(Z_{U_{\theta}, V_{\theta}}) = \Theta(\mathcal{C}(Z_{U,V}))
$$

$$
\text{With } S_U = \{U_\theta \mid U = \{r \in R \mid U_\theta \cap \Theta(r) \neq \emptyset\}, U_\theta \sqcap V_\theta = \Theta(R)\}
$$

*Proof.* Let us suppose given a partition $U \sqcap V = \Omega(R)$ such that $U \neq \emptyset$. We will proceed by double inclusion:

• Let $c \in \Theta(\mathcal{C}(Z_{U,V}))$ i.e. $c \in \Theta(x)$, $d \in \mathcal{C}(Z_{U,V})$,

- If $[d] \subseteq [v]^c$, then by Lemma 4.4.23, we have $[c][\Theta(d)] \subseteq [d] \subseteq [v]^c \subseteq [\Theta(v)]^c$

- $d \subseteq u$ implies by Lemma 4.4.24 that there exists a unique $u_c \in \Theta(u)$ such that $c \subseteq u_c$. Thus, for any $w \in \Theta(u) \setminus u_c$, $[c] \subseteq [w]^c$

Thus, $d \subseteq \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^c$ implies

$$
[c] \subseteq \bigcap_{u \in U} \left( [u_c] \bigcap_{\substack{w \in \Theta(u) \\ w \neq u_c}} [w]^c \right) \bigcap_{v \in V} [\Theta(v)]^c
$$

$$
[c] \subseteq \bigcap_{u \in U} \left( [u_c] \bigcap_{\substack{w \in \Theta(u) \\ w \neq u_c}} [w]^c \right) \bigcap_{v \in V} \bigcap_{w \in \Theta(v)} [w]^c
$$

Then by defining $U_{\theta} = \{u_c \mid u \in U\}$ and $V_{\theta} = \Theta(V) \cup \Theta(U) \setminus U_{\theta}$, we have $U_{\theta} \sqcap V_{\theta} = \Theta(U) \cup \Theta(V) = \Theta(R)$ and

$c \in \mathcal{C}(Z_{U_0, V_0})$

• Given $U \sqcap V = R$, let us show that for any $U_{\theta} \sqcap V_{\theta} = \Theta(R)$ such that $U_{\theta} \in S_U$, we have

$$
Z_{U_{\theta}, V_{\theta}} \subseteq Z_{U, V}
$$

for all $u \in U$ such that $U_{\theta} \cap \Theta(u) \neq \emptyset$, if there exists $u_1 \neq u_2 \in U_{\theta} \cap \Theta(u)$, then by Lemma 4.4.22, $[u_1] \cap [u_2] = \emptyset$ i.e.

$$
Z_{U_{\theta}, V_{\theta}} = \emptyset
$$

If that's the case, then we can conclude the whole proof. Let us then suppose that for all $u \in U$ there exists a unique $u_{\theta} \in \Theta(u)$ such that $u_{\theta} \in \Theta(u) \cap U_{\theta}$. Thus, by definition of $S_U$, we have:

$$
U_{\theta} = \{u_{\theta} \mid u \in U\}
$$

$$
V_{\theta} = \bigcup_{u \in U} \{w \in \Theta(u) \mid w \neq u_{\theta}\} \cup \Theta(V)
$$
Then,

$$
\begin{align*}
Z_{U_{\theta}, V_{\theta}} &= \bigcap_{u' \in U_{\theta}} [u'] \bigcap_{v \in V_{\theta}} [v]^{c} \\
&= \bigcap_{u_{\theta} \in U_{\theta}} [u_{\theta}] \bigcap_{\substack{u \in U \\ w \in \Theta(u) \\ w \neq u_{\theta}}} [w]^{c} \bigcap_{v \in \Theta(V)} [v']^{c} \\
&= \bigcap_{u \in U} \left( [u_{\theta}] \bigcap_{\substack{w \in \Theta(u) \\ w \notin \{u_{\theta}\}}} [w]^{c} \right) \bigcap_{v \in V} \left( \bigcup_{w \in \Theta(v)} [w] \right)^{c} \\
&= \bigcap_{u \in U} [u_{\theta}] \bigcap_{v \in V} [\Theta(v)]^{c} \tag*{Lemma 4.4.22} \\
&\subseteq \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^{c} \tag*{Lemma 4.4.22} \\
Z_{U_{\theta}, V_{\theta}} &\subseteq Z_{U, V}
\end{align*}
$$

Thus, $\mathcal{C}(Z_{U_{\theta},V_{\theta}}) \subseteq \mathcal{C}(Z_{U,V})$ and hence

$$
\Theta(\mathcal{C}(Z_{U_{\theta}, V_{\theta}})) \subseteq \Theta(\mathcal{C}(Z_{U, V}))
$$

By definition, there exists at least an element $u \in U_{\theta}$. Thus, $Z_{U_{\theta},V_{\theta}} \subseteq [u]$, which
implies by Lemma 4.4.23,

$$
\mathcal{C}(Z_{U_{\theta}, V_{\theta}}) \subseteq \Theta(\mathcal{C}(Z_{U_{\theta}, V_{\theta}})) \subseteq \Theta(\mathcal{C}(Z_{U,V}))
$$

Thus, for any cover $R$ and any $U \amalg V = R$ such that $\mathcal{C}(Z_{U,V}) \cap C_{-1}$, we have

$$
\bigcap_{U_{\theta} \in S_{U}} \mathcal{C}(Z_{U_{\theta}, V_{\theta}}) = \Theta(\mathcal{C}(Z_{U,V}))
$$

□

**Lemma 4.4.27.** Given a cover $R$ and any partition $U \amalg V = R$ such that $U \neq \emptyset$, we have

$$
\prod_{U_{\theta} \in S_U} \mathcal{C}^{\max}(Z_{U_{\theta}, V_{\theta}}) = \Theta(\mathcal{C}^{\max}(Z_{U,V}))
$$

$$
\text{With } S_U = \{U_\theta \mid U = \{r \in R \mid U_\theta \cap \Theta(r) \neq \emptyset\}, U_\theta \amalg V_\theta = \Theta(R)\}
$$

Proof. By the previous Lemma 4.4.26, we have

$$
\prod_{U_{\theta} \in X_U} \mathcal{C}(Z_{U_{\theta}, V_{\theta}}) = \Theta(\mathcal{C}(Z_{U,V}))
$$

Let us prove that the equality holds on maximal cubes by double inclusion
* Let us suppose $c \in \mathcal{C}^{\max}(Z_{U_\theta, V_\theta}^0)$. By Lemma 4.4.26, we have that $c \in \Theta(i)$, $i \in \mathcal{C}(Z_{U,V})$. Now, let us suppose $i \subseteq j \in \mathcal{C}^{\max}(Z_{U,V})$, Then by Lemma 4.4.24, there exists $d \in \Theta(j) \subseteq \prod_{U_\theta \in X_U} \mathcal{C}(Z_{U_\theta, V_\theta})$ such that

$$c \subseteq d$$

Furthermore, as the $Z_{U_\theta, V_\theta}$ are disjoint, this implies $d \in \mathcal{C}(Z_{U_\theta, V_\theta}^0)$. Thus, by maximality of $c$, we have $c = d$, which implies $i = j$, i.e.

$$c \in \Theta(\mathcal{C}^{\max}(Z_{U,V}))$$

* Let us suppose $c \in \Theta(\mathcal{C}^{\max}(Z_{U,V}))$ there exists $i \in \mathcal{C}^{\max}(Z_{U,V})$ such that $c \in \Theta(i)$, By Lemma 4.4.26, we have that $c \in \mathcal{C}(Z_{U_\theta, V_\theta})$, $U_\theta \in X_U$. Let us suppose $d \in \mathcal{C}^{\max}(Z_{U_\theta, V_\theta})$, $U_\theta \in S_U$ such that

$$c \subseteq d$$

By Lemma 4.4.26, $d \in \Theta(\mathcal{C}(Z_{U,V}))$. Then by Lemma 4.4.25 there exists $j \in \mathcal{C}(Z_{U,V})$ such that $d \in \Theta(j)$ and $i \subseteq j$. This implies by maximality of $i$ that $i = j$, and by Lemma 4.4.22 that $c = d$ i.e.

$$c \in \mathcal{C}^{\max}(Z_{U_\theta, V_\theta})$$

□

**Proposition 4.4.28.** Let $P \in \mathbf{Pgrm}$, for any conservative cover $R$ on a program $\mathcal{U}(P)$,

$$\Theta \circ \Gamma^m(R) = \Gamma^m \circ \Theta(R)$$

*Proof.* First we will write $X = \bigcup_{\substack{U \sqcup V = R \\ U \neq \emptyset}} X_U$ with

$$X_U = \{U_\theta \mid U = \{r \in R \mid U_\theta \cap \Theta(r) \neq \emptyset\}, U_\theta \sqcup V_\theta = \Theta(R)\}$$

as previously defined. Let us prove that

$$X = \{U_\theta \mid U_\theta \neq \emptyset, U_\theta \subseteq \Theta(R)\}$$

By definition $X \subseteq \{U_\theta \mid U_\theta \subseteq \Theta(R)\}$. Furthermore, given a partition $U_\theta \sqcup V_\theta$, if we define

$$U = \{r \in R \mid U_\theta \cap \Theta(r) \neq \emptyset\}$$

$$V = \{r \in R \mid U_\theta \cap \Theta(r) = \emptyset\}$$

We have, $U_\theta \in X_U$ and $U \sqcup V = R$, such that $\{U_\theta \mid U_\theta \subseteq \Theta(R)\} \subseteq X$. And thus,

$$X = \{U_\theta \mid U_\theta \neq \emptyset, U_\theta \subseteq \Theta(R)\} \qquad (4.4)$$

Now let us proceed by induction on the program $P$.
• $P \in \mathbf{Prcs}^*$. Given a cover $R$ on $P$, we get

$$
\begin{align*}
\Theta \circ \Gamma^m(R) &= \bigcup_{\substack{U \sqcup V = R \\ U \neq \emptyset}} \Theta(\mathcal{C}^{\max}(Z_{U,V})) \\
&= \bigcup_{\substack{U \sqcup V = R \\ U \neq \emptyset}} \prod_{U_{\theta} \sqcup V_{\theta} \in X_U} \mathcal{C}^{\max}(Z_{U_{\theta}, V_{\theta}}) \qquad \text{Lemma 4.4.27} \\
&= \bigcup_{\substack{U_{\theta} \sqcup V_{\theta} = \Theta(R) \\ U_{\theta} \neq \emptyset}} \mathcal{C}^{\max}(Z_{U_{\theta}, V_{\theta}}) \qquad \text{Eq. (4.4)} \\
\Theta \circ \Gamma^m(R) &= \Gamma^m \circ \Theta(R)
\end{align*}
$$

• $P = P_1 \| \cdots \| P_n$, for all $1 \le i \le n$, $P_i \in \mathbf{Prcs}^*$. Then for any cover $S$ on $P$, we have

$$
\Gamma^m(S) = \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(S)) \right) \cap \mathcal{C}[S]
$$

where $\mathcal{P}_k(S) = \{c_k \mid c_1 \| \dots \| c_n \in S\}$. We can remark that by linearity

$$
\Theta(\mathcal{P}_k(S)) = \mathcal{P}_k(\Theta(S))
$$

We have for any $1 \le k \le n$,

$$
\Theta \circ \Gamma^m(\mathcal{P}_k(R)) = \Gamma^m(\Theta(\mathcal{P}_k(R))) \quad \text{by the case above}
$$

$$
\Theta \circ \Gamma^m(\mathcal{P}_k(R)) = \Gamma^m(\mathcal{P}_k(\Theta(R)))
$$

Furthermore, by Lemma 4.4.22

$$
\mathcal{C}(R) = \mathcal{C}(\Theta(R))
$$

This is true for all $1 \le k \le n$, then as $\Theta$ distributes over products, we get:

$$
\begin{align*}
\Theta \circ \Gamma^m(R) &= \left( \prod_{1 \le k \le n} \Theta \circ \Gamma^m(\mathcal{P}_k(R)) \right) \cap \mathcal{C}(R) \\
&= \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(\Theta(R))) \right) \cap \mathcal{C}(\Theta(R)) \\
\Theta \circ \Gamma^m(R) &= \Gamma^m \circ \Theta(R)
\end{align*}
$$

<figure><img src="image_195.png" /></figure>

**Proposition 4.4.29.** Let $P \in \mathbf{Pgrm}$, for any conservative cover $R$ on a program $\mathcal{U}(P)$,

$$
\Theta \circ \Gamma^*(R) = \Gamma^* \circ \Theta(R)
$$

Proof.

$$
\Theta \circ \Gamma^*(R) = \Theta \circ \Gamma^m \circ \Gamma^m(R) \qquad \text{Proposition 3.3.22}
$$

$$
= \Gamma^m \circ \Theta \circ \Gamma^m(R) \qquad \text{Proposition 4.4.28}
$$

$$
= \Gamma^m \circ \Gamma^m \circ \Theta(R) \qquad \text{Proposition 4.4.28}
$$

$$
\Theta \circ \Gamma^*(R) = \Gamma^* \circ \Theta(R)
$$

<figure><img src="image_196.png" /></figure>
4.4.2.3 $\Gamma^* \circ \Psi^{-1} = \Psi^{-1} \circ \Gamma^*$

Instead of directly proving the commutation of $\Gamma^*$ and $\Psi^{-1}$ (bottom right square in the diagram) we prove the commutation of the bottom part of the diagram, which corresponds to the following commutation.

**Proposition 4.4.37.** Let $P \in \mathbf{Pgrm}$, $R$ a maximal conservative cover on $P$. Then

$$ \Psi^{-1} \circ \Gamma^* \circ \Omega(R) = \Gamma^* \circ \Theta \circ \Psi^{-1}(R) $$

We begin by a few technical lemmas, which are for most direct consequences of our definition that are restated in this form for practicality.

**Lemma 4.4.30.** Given a cube $u \in \Omega(C(P))$. Then

* $\Omega \circ \Omega = \Omega$

* For any subset $X \subseteq [u]$, $C(X) \in \Omega(C(P))$

*Proof.* Directly by definition of $\Omega$

□

**Corollary 4.4.31.** Given a cover $R$ and a partition $U \amalg V = \Omega(R)$, $U \neq \emptyset$, then

$$ C(Z_{U,V}) = \Omega(C(Z_{U,V})) $$

*Proof.* As $U \neq \emptyset$, there exists $u \in \Omega(R)$ such that $Z_{U,V} \subseteq [u]$. Thus, by Lemma 4.4.30 $C(Z_{U,V}) \in \Omega(C(P))$, and $C(Z_{U,V}) = \Omega(C(Z_{U,V}))$

□

We have a complementary version of Proposition 4.3.22, that implies the reflection of order on lifting of cut cubes.

**Lemma 4.4.32.** Let $P \in \mathbf{Prcs}$, $R$ a conservative cover of $P^*$. Let $i, j \in \Psi^{-1}(\Omega(R))$. Then

$$ \Psi(i) \subseteq \Psi(j) \implies \exists k \in \Psi^{-1}(\Psi(j)), i \subseteq k $$

*Proof.* First let us remark that $\Psi(j) \notin \mathcal{L}_1 \cap \Omega(R)$. As by definition, no cubes of $\Omega(R)$ can contain $\top^*$, we are left with $\Psi(i), \Psi(j) \in \mathcal{C}_0 \cup \mathcal{L}_5$.

* $\Psi(i) \in \mathcal{C}_0$. Then $\Psi(i) \subseteq \Psi(j)$, $\Psi(j) \in \Omega(R)$ implies $\Psi(i) = \Psi(j)$, and then $i = j$ by Proposition 4.2.36.

* $\Psi(i) \in \mathcal{L}_5$. Then $\Psi(i) \subseteq \Psi(j)$ implies $\Psi(j) \in \mathcal{L}_5$. Then $\Psi(i) = (p^*, q^*) \neq (\top^*, \top^*)$. Then $\Psi(i) = (p^*, q^*) \subseteq (x^*, y^*) = j$ implies by Lemma 4.3.16, $(p, q) \subseteq (x, y)$ and by induction rules

$$ (p; \perp, q; \perp) \subseteq (x; \perp, y; \perp) \approx j $$

$$ (\top; p, \top; q) \subseteq (\top; x, \top; y) \approx j $$

As $i \in \{(p; \perp, q; \perp), (\top; p, \top; q)\}$ by definition, this concludes the case.

□

**Lemma 4.4.33.** Let $P \in \mathbf{Pgrm}$, $R$ a conservative cover on $P$. Let $c, d \in \Omega(R)$. Then
• $[c] \subseteq [d]^c$ implies for all $x \in \Psi^{-1}(c)$, $[x] \subseteq \bigcap_{y \in \Psi^{-1}(d)} [y]^c$

*Proof.* Let $P \in \mathbf{Pgrm}$, $R$ a conservative cover on $P$. Let $c, d \in \Omega(R)$.

• By contraposition, let us suppose that there exists $x \in \Psi^{-1}(c)$, $y \in \Psi^{-1}(d)$ such that

$$ 
\begin{align*}
& [x] \subseteq [y] \\
\Rightarrow & \Phi[x] \subseteq \Phi[y] \\
\Rightarrow & [\Psi(x)] \subseteq [\Psi(y)] \qquad \text{Proposition 4.2.44} \\
\Rightarrow & [c] \subseteq [d] \\
\Rightarrow & [c] \not\subseteq [d]^c
\end{align*}
$$

Thus $[c] \subseteq [d]^c$ implies for all $x \in \Psi^{-1}(c)$, $[x] \subseteq \bigcap_{y \in \Psi^{-1}(d)} [y]^c$

□

The core of the commutation is proven in the following lemmas by proving that the maximal cover of the associated partition supports commute with $\Psi^{-1}$

**Lemma 4.4.34.** *Given a cover $R$ on a program $P \in \mathbf{Prcs}^*$, such that $R = \Omega(R)$ and any partition $U \sqcap V = R$.*

$$ \coprod_{U_{\psi} \in X_U} \mathcal{C}(Z_{U_{\psi}, V_{\psi}}) = \Psi^{-1}(\mathcal{C}(Z_{U,V})) $$

*With $X_U = \{U_{\psi} \mid U = \{r \in R \mid U_{\psi} \cap \Psi^{-1}(r) \neq \emptyset\}, U_{\psi} \sqcap V_{\psi} = \Psi^{-1}(R)\}$*

*Proof.* Let us suppose given a partition $U \sqcap V = \Omega(R)$, $U \neq \emptyset$. We will proceed by double inclusion:

• Let $c \in \Psi^{-1}(\mathcal{C}(Z_{U,V}))$ i.e. $c \in \Psi^{-1}(x), x \in \mathcal{C}(Z_{U,V}) = \Omega(\mathcal{C}(Z_{U,V}))$ (by Corollary 4.4.31)

– By Lemma 4.4.33 $[x] \subseteq [v]^c$ implies $[c] \subseteq [\Psi^{-1}(v)]^c$

– $x \subseteq u$ implies by Lemma 4.4.32 that there exists $u_c \in \Psi^{-1}(u)$ such that $c \subseteq u_c$. And, by Proposition 4.2.40, for any $w \in \Psi^{-1}(u)$, $w \neq u_c$ implies $[c] \subseteq [w]^c$

Thus, $x \subseteq \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^c$ implies

$$ 
\begin{align*}
[c] &\subseteq \bigcap_{u \in U} \left( [u_c] \bigcap_{\substack{w \in \Psi^{-1}(u) \\ w \neq u_c}} [w]^c \right) \bigcap_{v \in V} [\Psi^{-1}(v)]^c \\
[c] &\subseteq \bigcap_{u \in U} \left( [u_c] \bigcap_{\substack{w \in \Psi^{-1}(u) \\ w \neq u_c}} [w]^c \right) \bigcap_{v \in V} \bigcap_{w \in \Psi^{-1}(v)} [w]^c
\end{align*}
$$

Then by defining $U_{\psi} = \{u_c \mid u \in U\}$ and $V_{\psi} = \Psi^{-1}(V) \cup \Psi^{-1}(U) \setminus U_{\psi}$, we have $U_{\psi} \sqcap V_{\psi} = \Psi^{-1}(U) \cup \Psi^{-1}(V) = \Psi^{-1}(R)$ and

$$ c \in \mathcal{C}(Z_{u_{\psi}, V_{\psi}}) $$
• Given a partition $U \amalg V = \Omega(R)$. Let $c \in \mathcal{C}(Z_{U_\psi, V_\psi})$ such that $U_\psi \in X_U$.

- By Proposition 4.3.18, $c \subseteq u_\psi$ implies $\Psi(c) \subseteq \Psi(u_\psi)$

- By definition of $X_U$, we have that for any $v_\psi \in V_\psi$, with $v = \Psi(v_\psi)$, we have that $\Psi^1(v) \subseteq V_\psi$. Thus, for any $v \in V$, $[c] \subseteq [\Psi^{-1}(v)]^c$. By contraposition of Lemma 4.4.32, we get that $[\Psi(c)] \subseteq [\Psi \circ \Psi^{-1}(v)]^c = [v]^c$

Thus we get

$$ \Psi(c) \subseteq \bigcap_{u_\psi \in U_\psi} [\Psi(u_\psi)] \bigcap_{v \in V} [v] $$

$$ \Psi(c) \subseteq \bigcap_{u \in U} [u] \bigcap_{v \in V} [v] $$

i.e. $c \in \Psi^{-1}(\mathcal{C}(Z_{U,V}))$

□

**Lemma 4.4.35.** Given a cover $R$, such that $R = \Omega(R)$ and any $U \amalg V = R$ such that $U \neq \emptyset$

$$ \coprod_{U_\psi \in X_U} \mathcal{C}^{\max}(Z_{U_\psi, V_\psi}) = \Psi^{-1}(\mathcal{C}^{\max}(Z_{U,V})) $$

With $X_U = \{U_\psi | U = \{r \in R | U_\psi \cap \Psi^{-1}(r) \neq \emptyset\}, U_\psi \amalg V_\psi = \Psi^{-1}(R)\}$

*Proof.* By the previous Lemma 4.4.34, we have

$$ \coprod_{U_\psi \in X_U} \mathcal{C}(Z_{U_\psi, V_\psi}) = \Psi^{-1}(\mathcal{C}(Z_{U,V})) $$

Let us prove that the equality holds on maximal cubes by double inclusion

• Let us suppose $c \in \mathcal{C}^{\max}(Z_{U_\psi^0, V_\psi^0})$. By Lemma 4.4.34, we have that $c \in \Psi^{-1}(x)$, $x \in \mathcal{C}(Z_{U,V})$. Now, let us suppose $x \subseteq y \in \mathcal{C}^{\max}(Z_{U,V})$, Then by Lemma 4.4.32, there exists $d \in \Psi^{-1}(y)$ i.e. $d \in \coprod_{U_\psi \in X_U} \mathcal{C}(Z_{U_\psi, V_\psi})$ such that

$$ c \subseteq d $$

As the $Z_{U_\psi, V_\psi}$ are disjoint, this implies $d \in \mathcal{C}^{\max}(Z_{U_\psi^0, V_\psi^0})$. Thus, $c = d$, which implies $x = y$, i.e.

$$ c \in \Psi^{-1}(\mathcal{C}^{\max}(Z_{U,V})) $$

• Let us suppose $c \in \Psi^{-1}(\mathcal{C}^{\max}(Z_{U,V}))$. By Lemma 4.4.34, we have that $c \in \mathcal{C}(Z_{U_\psi, V_\psi})$, $U_\psi \in X_U$. Let us suppose $d \in \mathcal{C}^{\max}(Z_{U_\psi, V_\psi})$ such that

$$ c \subseteq d $$

Then by Proposition 4.3.18 $\Psi(c) \subseteq \Psi(d)$. This implies by maximality of $\Psi(c)$ that $\Psi(c) = \Psi(d)$ and by Proposition 4.2.40, $c \subseteq d$ implies $c = d$.
<figure><img src="image_197.png" /></figure>

**Proposition 4.4.36.** Let $P \in \mathbf{Pgrm}$, $R$ a maximal conservative cover on $P$. Then

$$ \Psi^{-1} \circ \Gamma^m(\Omega(R)) = \Gamma^m \circ \Theta \circ \Psi^{-1}(R) $$

*Proof.* First we will write $X = \bigcup_{\substack{U \sqcup V = R \\ U \neq \emptyset}} X_U$ with

$$ X_U = \{U_{\psi} \mid U = \{r \in R \mid U_{\psi} \cap \Psi^{-1}(r) \neq \emptyset\}, U_{\psi} \sqcup V_{\psi} = \Psi^{-1}(R)\} $$

as previously defined. Let us prove that

$$ X = \{U_{\psi} \mid U_{\psi} \neq \emptyset, U_{\psi} \subseteq \Psi^{-1}(R)\} $$

By definition $X \subseteq \{U_{\psi} \mid U_{\psi} \subseteq \Psi^{-1}(R)\}$. Furthermore, given a partition $U_{\psi} \sqcup V_{\psi} =$, $U_{\psi} \neq \emptyset$, if we define

$$ U = \{r \in R \mid U_{\psi} \cap \Psi^{-1}(r) \neq \emptyset\} $$

$$ V = \{r \in R \mid U_{\psi} \cap \Psi^{-1}(r) = \emptyset\} $$

We have, $U \neq \emptyset$ as $U_{\psi} \neq \emptyset$. Thus, $U_{\psi} \in X_U$ and $U \sqcup V = R$, such that $\{U_{\psi} \mid U_{\psi} \subseteq \Psi^{-1}(R)\} \subseteq X$. And thus,

$$ X = \{U_{\psi} \mid U_{\psi} \neq \emptyset, U_{\psi} \subseteq \Psi^{-1}(R)\} \quad (4.5) $$

Now we will proceed by induction on $P$

* $P \in \mathbf{Prcs}^*$. Given $R$ a cover on $P$, such that $R = \bigcup_{i \in I} R_i$, with $R_i$ maximal conservative. As $\Omega(R) = \Omega(\Omega(R))$, we can apply the previous lemmas

$$ \Psi^{-1} \circ \Gamma^m \circ \Omega(R) = \bigcup_{\substack{U \sqcup V = \Omega(R) \\ U \neq \emptyset}} \Psi^{-1}(\mathcal{C}^{\max}(Z_{U,V})) $$

$$ = \bigcup_{\substack{U \sqcup V = \Omega(R) \\ U \neq \emptyset}} \prod_{U_{\psi} \in X_U} \mathcal{C}^{\max}(Z_{U_{\psi}, V_{\psi}}) \qquad \text{Lemma 4.4.35} $$

$$ = \bigcup_{\substack{U_{\psi} \sqcup V_{\psi} = \Psi^{-1} \circ \Omega(R) \\ U_{\psi} \neq \emptyset}} \mathcal{C}^{\max}(Z_{U_{\psi}, V_{\psi}}) \qquad \text{Eq. (4.5)} $$

$$ = \Gamma^m \circ \Psi^{-1} \circ \Omega(R) $$

$$ = \Gamma^m \circ \Psi^{-1} \circ \Omega(\bigcup_{i \in I} R_i) $$

$$ = \Gamma^m \circ \bigcup_{i \in I} \Psi^{-1} \circ \Omega(R_i) $$

$$ = \Gamma^m \circ \bigcup_{i \in I} \Theta \circ \Psi^{-1}(R_i) \qquad \text{Proposition 4.4.21} $$

$$ \Psi^{-1} \circ \Gamma^m \circ \Omega(R) = \Gamma^m \circ \Theta \circ \Psi^{-1}(R) $$
• $P = P_1 \| \dots \| P_n, P_k \in \mathbf{Prcs}^*$. Then for any cover $S$ on $P$, we have

$$ \Gamma^m(S) = \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(S)) \right) \cap \mathcal{C}[S] $$

where $\mathcal{P}_k(S) = \{c_k \mid c_1 \| \dots \| c_n \in S\}$. We can remark that by linearity

$$ \mathcal{P}_k(\Omega(S)) = \Omega(\mathcal{P}_k(S)) \quad \Psi^{-1}(\mathcal{P}_k(S)) = \mathcal{P}_k(\Psi^{-1}(S)) \quad \mathcal{P}_k(\Theta(S)) = \Theta(\mathcal{P}_k(S)) $$

As the case of sequential process above does not require $R$ to be maximal, we have for any $1 \le k \le n$,

$$ \begin{aligned} \Psi^{-1} \circ \Gamma^m(\mathcal{P}_k(\Omega(R))) &= \Psi^{-1} \circ \Gamma^m \circ \Omega(\mathcal{P}_k(R)) \\ &= \Gamma^m \circ \Theta \circ \Psi^{-1}(\mathcal{P}_k(R)) \quad \text{by the case above} \\ \Psi^{-1} \circ \Gamma^m(\mathcal{P}_k(\Omega(R))) &= \Gamma^m \circ \mathcal{P}_k(\Theta \circ \Psi^{-1}(R)) \end{aligned} $$

As $R$ is maximal and conservative, by Proposition 4.3.26

$$ \Psi^{-1}(\mathcal{C}(\Omega(R))) = \Psi^{-1}(\mathcal{C}(R)) = \mathcal{C}(\Psi^{-1}(R)) \setminus \mathcal{C}_{-1} = \mathcal{C}(\Theta \circ \Psi^{-1}(R)) \setminus \mathcal{C}_{-1} $$

This is true for all $1 \le k \le n$, then as $\Psi^{-1}$ and $\Omega$ distribute over products, we get:

$$ \begin{aligned} \Psi^{-1} \circ \Gamma^m \circ \Omega(R) &= \left( \prod_{1 \le k \le n} \Psi^{-1} \circ \Gamma^m(\mathcal{P}_k(\Omega(R))) \right) \cap \Psi^{-1}(\mathcal{C}(\Omega(R))) \\ &= \left( \prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(\Theta \circ \Psi^{-1}(R))) \right) \cap \mathcal{C}(\Theta \circ \Psi^{-1}(R)) \setminus \Pi_{\mathcal{U}(P)} \mathcal{C}_{-1} \\ \Psi^{-1} \circ \Gamma^m \circ \Omega(R) &= \Gamma^m \circ \Theta \circ \Psi^{-1}(R) \end{aligned} $$

As by definition, no cube of $\prod_{1 \le k \le n} \Gamma^m(\mathcal{P}_k(\Theta \circ \Psi^{-1}(R)))$ are in $\Pi_{\mathcal{U}(P)} \mathcal{C}_{-1}$ $\square$

**Proposition 4.4.37.** Let $P \in \mathbf{Pgrm}$, $R$ a maximal conservative cover on $P$. Then

$$ \Psi^{-1} \circ \Gamma^* \circ \Omega(R) = \Gamma^* \circ \Theta \circ \Psi^{-1}(R) $$
Proof.

$$ \Psi^{-1} \circ \Gamma^*(\Omega(R)) = \Psi^{-1} \circ \Gamma^m \circ \Gamma^m(\Omega(R)) \qquad \text{Lemma 3.3.20} $$

$$ = \Psi^{-1} \prod_{\substack{U \cap V = \Omega(R) \\ U \neq \emptyset}} \Gamma^m(\mathcal{C}^{\max}(Z_{U,V})) \qquad \text{Lemma 3.3.21} $$

$$ = \prod_{\substack{U \cap V = \Omega(R) \\ U \neq \emptyset}} \Psi^{-1} \circ \Gamma^m(\mathcal{C}^{\max}(Z_{U,V})) $$

$$ = \prod_{\substack{U \cap V = \Omega(R) \\ U \neq \emptyset}} \Psi^{-1} \circ \Gamma^m \circ \Omega(\mathcal{C}^{\max}(Z_{U,V})) \qquad \text{Corollary 4.4.31} $$

$$ = \prod_{\substack{U \cap V = \Omega(R) \\ U \neq \emptyset}} \Gamma^m \circ \Theta \circ \Psi^{-1}(\mathcal{C}^{\max}(Z_{U,V})) \qquad \text{Proposition 4.4.36} $$

$$ = \Gamma^m \left( \prod_{\substack{U \cap V = \Omega(R) \\ U \neq \emptyset}} \Theta \circ \Psi^{-1}(\mathcal{C}^{\max}(Z_{U,V})) \right) \qquad \text{by the remark below} $$

$$ = \Gamma^m \circ \Theta \circ \Psi^{-1} \left( \prod_{\substack{U \cap V = \Omega(R) \\ U \neq \emptyset}} \mathcal{C}^{\max}(Z_{U,V}) \right) $$

$$ = \Gamma^m \circ \Theta \circ \Psi^{-1} \circ \Gamma^m \circ \Omega(R) $$

$$ = \Gamma^m \circ \Theta \circ \Gamma^m \circ \Theta \Psi^{-1}(R) \qquad \text{Proposition 4.4.36} $$

$$ = \Gamma^m \circ \Theta \circ \Theta \circ \Gamma^m \circ \Psi^{-1}(R) \qquad \text{Proposition 4.4.28 as } \Psi^{-1}(R) \text{ maximal} $$

$$ = \Gamma^m \circ \Theta \circ \Gamma^m \circ \Psi^{-1}(R) $$

$$ = \Gamma^m \circ \Gamma^m \circ \Theta \circ \Psi^{-1}(R) \qquad \text{Proposition 4.4.28} $$

$$ \Psi^{-1} \circ \Gamma^*(\Omega(R)) = \Gamma^* \circ \Theta \circ \Psi^{-1}(R) $$

<figure><img src="image_198.png" /></figure>

We can now prove the full commutation announced at the start of the section

**Proposition 4.4.38.** Given a program $P \in \mathbf{Pgrm}$ and a maximal conservative cover $R$ on $P$ we have

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Psi^{-1} \circ \Gamma^* \Omega(R) $$

Proof. Given a program $P \in \mathbf{Pgrm}$ and a maximal conservative cover $R$ on $P$ we have

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Gamma^* \circ \Theta \circ \Psi^{-1}(R) \qquad \text{Proposition 4.4.29} $$

$$ = \Gamma^* \circ \Psi^{-1} \circ \Omega(R) \qquad \text{Proposition 4.4.21} $$

$$ \Theta \circ \Gamma^* \circ \Psi^{-1}(R) = \Psi^{-1} \circ \Gamma^* \circ \Omega(R) \qquad \text{Proposition 4.4.37} $$

<figure><img src="image_199.png" /></figure>

As $\Omega$ and $\Theta$ preserve reachability, this could be enough to define Algorithm 4.4.51, but cutting through $\Omega$ really is quite costly in terms of number of cubes generated, and we are going to prove that the only cube that $\Omega$ needs to cut is the cube $(\perp, \top)$ to comply with the action of $\Theta$.
4.4.2.4 $\Gamma^* \circ \Omega = \Gamma^* \circ \chi$

In this section we prove that the operator $\Omega$ is entirely unnecessary when considering the partition, and can instead be replaced by $\chi$.

**Proposition 4.4.44.** Let $P \in \mathbf{Pgrm}$, let $R$ a conservative maximal cover of $P$. Then

$$ \Gamma^*(\Omega(R)) = \Gamma^*(\chi(R)) $$

The core of the proof lies in Proposition 4.4.41 which gives an equivalence between partition of $\Omega(R)$ and $\chi(R)$.

*Example 4.4.39.* Indeed, by Proposition 4.3.21, the cubes of a maximal conservative cover that cross the core will always be grouped in quadruplets of the form $(p^*, \top^*), (\top^*, q^*), (p^*, \top^*, q^*), (\bot, \top^*, \top)$. In the figure below we show the cubical partition associated to such a quadruplet.

<figure><img src="image_200.png" /></figure>

Now we give the result of the operations of cutting with $\Omega$.

<figure><img src="image_201.png" /></figure>
<figure><img src="image_202.png" /></figure>

$$ \Omega((\perp+\emptyset)^*, \top^*, (\top+\emptyset)^*) $$

Now if we apply the cubical partition to the union of these covers, we will obtain exactly the same partition as before. This process generalizes to all maximal conservative covers (Proposition 4.4.41), and all covers that are a union of maximal conservative cover (Corollary 4.4.42). The reason $\chi$ appears is that we cut $(\perp, \top)$ whose partition is equal to itself.

**Lemma 4.4.40.** Given a program $P \in \mathbf{Pgrm}$ and a cube $c \in \mathcal{C}(\mathcal{U}(P))$, we have

$$ [\Omega(c)] = [c] $$

*Proof.* By induction on $P$.

* $P \in \mathbf{Prcs}$. Then $\Omega$ is the identity.

* $P = P_1 \parallel P_2$. Then, $c \in \mathcal{C}(\mathcal{U}(P))$ implies $c = c_1 \times c_2$ and

$$ \begin{align*} [\Omega(c)] &= [\Omega(c_1)] \times [\Omega(c_2)] \\ &= [c_1] \times [c_2] \qquad \text{induction hypothesis} \\ [\Omega(c)] &= [c] \end{align*} $$

Which concludes the proof.

* $P = Q^*$.

- $c \notin \mathcal{L}_4$. The, by definition of $\Omega$,

$$ \begin{align*} [\Omega(c)] &= [\mathcal{C}^{\max}([c] \setminus \{\top^*\}) \cup \mathcal{C}^{\max}([c] \cap \{\top^*\})] \\ [\Omega(c)] &= [c] \setminus \{\top^*\} \cup ([c] \cap \{\top^*\}) \\ [\Omega(c)] &= [c] \end{align*} $$

- $c = (p, \top^*, q^*)$. Then, by definition of $\Omega$,

$$ \begin{align*} [\Omega(c)] &= [\Omega(p, \top^*)] \cup [\Omega(\top^*, q)] \\ &= [p, \top^*] \cup [\top^*, q] \qquad \text{by the case above} \\ &= [(p, \top^*, q^*)] \\ [\Omega(c)] &= [c] \end{align*} $$
<figure><img src="image_203.png" /></figure>

**Proposition 4.4.41.** Let $P \in \mathbf{Prcs}^*$, $X \subseteq \mathcal{P}(P)$ and $R$ a maximal conservative cover on $P$. Then, the existence of a partition $U \sqcap V = \chi(R)$ such that

$$X = \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^c$$

is equivalent to the existence of a partition $U_\Omega \sqcap V_\Omega = \Omega(R)$ such that

$$X = \bigcap_{u_\Omega \in U_\Omega} [u_\Omega] \bigcap_{v_\Omega \in V_\Omega} [v_\Omega]^c$$

*Proof.* For any partition $C \sqcap D = S$ of a cover, we write

$$Z_{C,D} = \bigcap_{c \in C} [c] \bigcap_{d \in D} [d]^c$$

Let us proceed by separating the case where our program has a loop.

* $P \in \mathbf{Prcs}$. Then $\Omega$ is the identity on cubes. Taking $U^\Omega = U$ and $V^\Omega = V$ suffice.

* $P = Q^*$. First let us remind that $\mathcal{L}_0 \cap R = \emptyset$.

- $R = \{(\perp, \top)\}$. Then $\Omega(R) = \chi(R)$ which concludes the proof.

- $\perp^* \notin [R]$. Then by Proposition 4.3.21, there exists $((p_j, q_j))_{j \in J} \in \mathcal{C}(P)^J$, such that for all $j \in J$, $p_j, q_j \notin \{\perp, \top\}$ and

$$R = \bigcup_{j \in J} \{(p_j^*, q_j^*)\}$$

By Proposition 4.4.18, this implies $\Omega(R) = R = \chi(R)$ which concludes the proof.

- $(\perp, \top) \notin R, \top^* \in R$. Then $\chi(R) = R$, thus we simply need to prove the equivalence between partitions of $R$ and $\Omega(R)$.

By Proposition 4.3.21, there exists $((p_j, q_j))_{j \in J_1 \cup J_2}$, such that for all $j \in J_1 \cup J_2$, we have $p_j, q_j \in \mathcal{P}(P) \setminus \{\perp, \top\}$ and

$$R = \bigcup_{j \in J_1} \{(p_j^*, q_j^*)\} \bigcup_{j \in J_2} \{(\perp, q_j^*), (p_j^*, \top), (p_j^*, \top^*, q_j^*), (\perp, \top^*, \top)\}$$

And we write

$$R_{J_1} = \bigcup_{j \in J_1} \{(p_j^*, q_j^*)\}$$

$$R_{J_2} = \bigcup_{j \in J_2} R_j$$

with for all $j \in J_2$

$$R_j = \{(\perp, q_j^*), (p_j^*, \top), (p_j^*, \top^*, q_j^*), (\perp, \top^*, \top)\}$$
We define for all $j \in J_2$,

$$U_1 = R_{J_1} \cap U$$

$$U_j = R_j \cap U$$

$$U_2 = R_{J_2} \cap U$$

$$V_1 = R_{J_1} \cap V$$

$$V_j = R_j \cap V$$

$$V_2 = R_{J_2} \cap V$$

By construction we have,

$$U = U_1 \amalg U_2$$

$$V = V_1 \amalg V_2$$

$$U = U_1 \amalg (\bigcup_{j \in J} U_j)$$

$$V = V_1 \amalg (\bigcup_{j \in J} V_j)$$

Let us prove that for a fixed $j \in J_2$ the existence of the partition $U_j \amalg V_j = R_j$, is equivalent to the existence of a partition $U_j^\Omega \amalg V_j^\omega = \Omega(R_j)$ such that $Z_{U_j, V_j} = ZU_j^\Omega, V_j^\omega$.

Let us fix the notations, we write $p = p_j, q = q_j$, and

$$w = (p^*, \top)$$

$$y = (p^*, \top^*, q^*)$$

$$x = (\bot, q^*)$$

$$z = (\bot, \top^*, \top)$$

such that $R_j = \{w, x, y, z\}$ By definition,

$$\Omega(R_j) = \Omega\{(p^*, \top), (\bot, q^*), (p^*, \top^*, q^*), (\bot, \top^*, \top)\}$$

$$\Omega(R_j) = \{(p^*, \bar{\top}_p^*), (\bot^*, \bot^*), (\bot_q^*, q), (\bot, \bot), (\top, \top)\}$$

* If $U_j = \{x, z\}$ then we have $U_j^\Omega = \{(\bot, \bot)\}$. Indeed,

$$[p^*, \bar{\top}_p^*]^c \cap [\bot^*, \bot^*]^c \cap [\bot_q^*, q]^c \cap [\bot, \bot] \cap [\top, \top]^c = \{\bot\} = [w]^c \cap [x] \cap [y]^c \cap [z]$$

* If $U_j = \{w, z\}$ then we have $U_j^\Omega = \{(\top, \top)\}$. Indeed,

$$[p^*, \bar{\top}_p^*]^c \cap [\bot^*, \bot^*]^c \cap [\bot_q^*, q]^c \cap [\bot, \bot]^c \cap [\top, \top] = \{\top\} = [w] \cap [x]^c \cap [y]^c \cap [z]$$

* If $U_j = \{w, x, y, z\}$ then we have $U_j^\Omega = \{(\bot^*, \bot^*)\}$. Indeed,

$$[p^*, \bar{\top}_p^*]^c \cap [\bot^*, \bot^*]^c \cap [\bot_q^*, q]^c \cap [\bot, \bot]^c \cap [\top, \top]^c = \{\bot^*\} = [w] \cap [x] \cap [y] \cap [z]$$

* If $U_j = \{w, y\}$ then we have $U_j^\Omega = \{(p^*, \bar{\top}_p^*)\}$. Indeed, by Proposition 4.4.18

$$\begin{align*} [x]^c \cap [y] &= [\bot, \bot]^c \cap [\bot^*, \bot^*]^c \cap [\bot_q^*, q]^c \cap ( [p^*, \bar{\top}_p^*] \cup [\bot^*, \bot^*] \cup [\bot_q^*, q] ) \\ &= ([\bot, \bot]^c \cap [\bot^*, \bot^*]^c \cap [p^*, \bar{\top}_p^*]) \cap [\bot_q^*, q]^c \end{align*}$$

$$[x]^c \cap [y] = [p^*, \bar{\top}_p^*] \cap [\bot_q^*, q]^c$$

Furthermore

$$\begin{align*} [w] \cap [z]^c &= ([p^*, \bar{\top}_p^*] \cup [\bot^*, \bot^*] \cup [\top, \top]) \cap ([\bot, \bot]^c \cap [\bot^*, \bot^*]^c \cap [\top, \top]^c) \\ &= [p^*, \bar{\top}_p^*] \cap ([\bot, \bot]^c \cap [\bot^*, \bot^*]^c \cap [\top, \top]^c) \end{align*}$$

$$[w] \cap [z]^c = [p^*, \bar{\top}_p^*]$$