an expression encoded using different encodings evaluates the same for the memories, that is:

$$ \forall e \in \mathit{Expr}_{AP} : \mathit{eval}(\mathit{idt}(e), \mathcal{M}_{\mathcal{A}}^i) \Leftrightarrow \mathit{eval}(\mathit{ts}_i(e), \mathcal{M}^i). $$

PROOF OF LEMMA A.1. We first note that for the first evaluation eval(idt(e), M<sub>Mon</sub><sup>i</sup>), we rely only on the event evt<sub>i</sub> since M<sub>Mon</sub><sup>i</sup> = memc(evt<sub>i</sub>, idt). This is not the case for eval(ts<sub>i</sub>(e), M<sup>i</sup>) as M<sup>i</sup> = ⊔⊕<sup>2</sup><sub>t∈[1,i]</sub>{memc(evt<sub>t</sub>, ts<sub>t</sub>)} . However, we notice that for the second evaluation we evaluate the expression ts<sub>i</sub>(e), that is, where the expression where all atomic propositions have been encoded by the timestamp i. Therefore, let us denote the memory with timestamp i by M' = memc(evt<sub>i</sub>, ts<sub>i</sub>). We can rewrite M<sup>i</sup> as follows:

$$ \begin{aligned} \mathcal{M}^i &= \text{memc}(\text{evt}_i, \text{ts}_i) \quad \dagger_2 \biguplus_{t \in [1, k]}^2 \{\text{memc}(\text{evt}_k, \text{ts}_k)\}, \\ &= \mathcal{M}' \quad \dagger_2 \biguplus_{t \in [1, k]}^2 \{\text{memc}(\text{evt}_k, \text{ts}_k)\}. \end{aligned} $$

We know that all entries ⟨k, a⟩ ∈ dom(M<sup>i</sup>) with k < i do not affect at all the evaluation of an expression encoded with ts<sub>i</sub>. As such, we have:

$$ \forall e \in \mathit{Expr}_{AP} : \mathit{eval}(\mathit{ts}_i(e), \mathcal{M}^i) \Leftrightarrow \mathit{eval}(\mathit{ts}_i(e), \mathcal{M}') $$

We now show that the two memories M<sub>Mon</sub><sup>i</sup> and M' contain simply an encoding of the same atomic propositions. By construction, we have the following:

$$ \begin{aligned} \forall a \in \text{dom}(\mathcal{M}_{\mathcal{A}}^i) : & \quad \langle i, a \rangle \in \text{dom}(\mathcal{M}^i) \wedge \mathcal{M}_{\mathcal{A}}^i(a) = \mathcal{M}'(\langle i, a \rangle), \\ \forall \langle i, a' \rangle \in \text{dom}(\mathcal{M}') : & \quad a' \in \text{dom}(\mathcal{M}_{\mathcal{A}}^i) \wedge \mathcal{M}'(\langle i, a' \rangle) = \mathcal{M}_{\mathcal{A}}^i(a'). \end{aligned} $$

$$ \text{As such, we have: } \forall e \in \mathit{Expr}_{AP} : \mathit{eval}(\mathit{idt}(e), \mathcal{M}_{\mathcal{A}}^i) \Leftrightarrow \mathit{eval}(\mathit{ts}_i(e), \mathcal{M}') \Leftrightarrow \mathit{eval}(\mathit{ts}_i(e), \mathcal{M}^i). \quad \square $$

PROOF OF PROPOSITION 4.10. Given a trace tr of length i and a reconstructed global trace ρ (tr) = evt<sub>1</sub> . . . . . evt<sub>i</sub> , the proof is done by induction on the length of the trace |ρ (tr) | . We omit the label ℓ for clarity.

Base case: |ρ (tr) | = 0 , ρ (tr) = ϵ

$$ \Delta^*(q_0, \epsilon) = q_0 = \text{sel}(\mathcal{I}^0, [0, 0]) $$

$$ \mathcal{I}^0 = \text{mov}([0 \mapsto q_0 \mapsto \top], 0, 0) = [0 \mapsto q_0 \mapsto \top] $$

We only have expression ⊤ which is mapped to q<sub>0</sub> at t = 0 . Expression ⊤ requires no memory to be evaluated.

Inductive step: We assume that the property holds for a trace of length i for some i ∈ N , that is Δ<sup>*</sup>(q<sub>0</sub>, evt<sub>1</sub> . . . . . evt<sub>i</sub>) = sel( I<sup>i</sup>, M<sup>i</sup>, i ) = q<sub>i</sub> . Let us prove that the property holds for any trace of length i + 1 .

We now consider the transition functions in the automaton:

$$ \begin{align*} q_{i+1} &= \Delta^*(q_0, \mathit{evt}_1 \dots \mathit{evt}_{i+1}) \\ &= \Delta(\Delta^*(q_0, \mathit{evt}_1 \dots \mathit{evt}_{i}), \mathit{evt}_{i+1}) \tag*{(Def. 4.2)} \end{align*} $$

$$ = \Delta(q_i, \mathit{evt}_{i+1}) \qquad (\text{Hyp.}) $$

⇔ ∃e ∈ Expr<sub>AP</sub> :

$$ \delta(q_i, expr) = q_{i+1} \wedge \mathit{eval}(e, \mathcal{M}_{\mathcal{A}}^{i+1}) = \top \quad (1) $$
We note that, since the automaton is deterministic, there is a unique $q_{i+1}$ such that $q_{i+1} = \Delta(q_i, evt_{i+1})$.

We now consider the EHE operations to reach $q_{i+1}$ from $q_i$.

$$q_i = \mathrm{sel}(\mathcal{I}^i, \mathcal{M}^i, i)$$

$$\Leftrightarrow e = \mathcal{I}^i(i, q_i) \text{ with } \mathrm{eval}(e, \mathcal{M}^i) = \top \qquad (2)$$

$$\wedge \forall q'_i \in Q : q'_i \neq q_i \implies \mathrm{eval}(\mathcal{I}^i(i, q'_i)) \neq \top \qquad (\mathrm{Prop. 4.8})$$

$$\Leftrightarrow \mathrm{to}(\mathcal{I}^i, i, q_{i+1}, \mathrm{ts}_{i+1}) = \top \qquad (3)$$

(3) From the induction hypothesis, we know that $\mathcal{I}^i(i, q_i) = \top$, thus:

$$\begin{align*}
\mathrm{to}(\mathcal{I}^i, i, q_{i+1}, \mathrm{ts}_{i+1})
&= \bigvee_{\{\langle q, e' \rangle | \delta(q, e') = q'_{i+1}\}} (\mathcal{I}^i(i, q) \wedge \mathrm{ts}_{i+1}(e')) \\
&= \bigvee_{\{\langle q, e'' \rangle | \delta(q, e'') = q'_{i+1} \wedge q \neq q_i\}} (\mathcal{I}^i(i, q) \wedge \mathrm{ts}_{i+1}(e'')) \\
&\quad \vee \bigvee_{\{\langle q_i, e''' \rangle | \delta(q_i, e''') = q'_{i+1}\}} (\mathrm{ts}_{i+1}(e''')).
\end{align*}$$

We split the disjunction to consider the expressions that only come from state $q_i$, we now show that one such expression evaluates to $\top$. We know from (1), that one such expression can be taken in the automaton:

$$\exists e \in \mathrm{Expr}_{AP} : \delta(q_i, e) = q_{i+1} \wedge \mathrm{eval}(e, \mathcal{M}_{\mathcal{I}}^{i+1}) = \top \qquad (1)$$

$$\Leftrightarrow \mathrm{eval}(\mathrm{ts}_{i+1}(e), \mathcal{M}^{i+1}) = \top \qquad (4)$$

$$\Leftrightarrow \mathrm{to}(\mathcal{I}^i, i, q_{i+1}, \mathrm{ts}_{i+1}) = \top \qquad (5)$$

(4) is obtained using Lemma A.1 and idt(e) = e.

(5) follows from the disjunction.

Using the same approach, we can show that $\forall q' \in \mathrm{next}(\mathcal{I}^i, i) : q' \neq q_{i+1} \implies \mathrm{to}(\mathcal{I}^i, i, q', \mathrm{ts}_{i+1}) \neq \top$, since the first part of the conjunction does not evaluate to $\top$, and we know that the second part cannot evaluate to $\top$ by (2).

Finally, $\mathrm{to}(\mathcal{I}^i, i, q_{i+1}, \mathrm{ts}_{i+1}) = \top$ iff $\mathrm{sel}(\mathcal{I}^{i+1}, \mathcal{M}^{i+1}, i+1) = q_i$.

□

## B CHIRON SYSTEM ATOMIC PROPOSITIONS

We broke down the Chiron system based on analysis of the examples provided in [22, 50], using the various specifications rewritten in [2]. Table 6 displays various associations we used to generate our traces and events. Column C assigns an ID to the component. Column Name lists the logical module of the system we considered as a component. Column Original (AP) lists the atomic proposition provided by the authors of Chiron, and then edited by [22]. Column AP maps the atomic proposition to our traces. Column Comments includes comments on the atomic propositions.
<table><caption>Table 6. Chiron Atomic Propositions and Components.</caption><thead><tr><th>C</th><th>Name</th><th>Original (AP)</th><th>AP</th><th>Comments</th></tr></thead><tbody><tr><td rowspan="12">A</td><td rowspan="12">Dispatcher</td><td>registered_event_a1_e1</td><td>a0</td><td rowspan="4">True after an artist has completed registration</td></tr><tr><td>registered_event_a1_e2</td><td>a1</td></tr><tr><td>registered_event_a2_e1</td><td>a2</td></tr><tr><td>registered_event_a2_e2</td><td>a3</td></tr><tr><td>notify_a1_e1</td><td>a4</td><td rowspan="4">True when starting to dispatch an event to an artist</td></tr><tr><td>notify_a1_e2</td><td>a5</td></tr><tr><td>notify_a2_e1</td><td>a6</td></tr><tr><td>notify_a2_e2</td><td>a7</td></tr><tr><td>lst_sz0_e1</td><td>a8</td><td rowspan="4">Tracking the size of the list (state)</td></tr><tr><td>lst_sz0_e2</td><td>a9</td></tr><tr><td>lst_gt2_e1</td><td>a10</td></tr><tr><td>lst_gt2_e2</td><td>a11</td></tr><tr><td rowspan="6">B</td><td rowspan="6">Artist1</td><td>notify_client_a1_e1</td><td>b0</td><td rowspan="2">Artist receives a notification</td></tr><tr><td>notify_client_a1_e2</td><td>b1</td></tr><tr><td>register_event_a1_e1</td><td>b2</td><td rowspan="2">Artist requests to register for event</td></tr><tr><td>register_event_a1_e2</td><td>b3</td></tr><tr><td>unregister_event_a1_e1</td><td>b4</td><td rowspan="2">Artist requests to unregister</td></tr><tr><td>unregister_event_a1_e2</td><td>b5</td></tr><tr><td rowspan="6">C</td><td rowspan="6">Artist2</td><td>notify_client_a2_e1</td><td>c0</td><td rowspan="6">See Artist1</td></tr><tr><td>notify_client_a2_e2</td><td>c1</td></tr><tr><td>register_event_a2_e1</td><td>c2</td></tr><tr><td>register_event_a2_e2</td><td>c3</td></tr><tr><td>unregister_event_a2_e1</td><td>c4</td></tr><tr><td>unregister_event_a2_e2</td><td>c5</td></tr><tr><td>D</td><td>Main</td><td>term</td><td>d0</td><td>Main program terminates</td></tr></tbody></table>

## C CHANGES IN THEMIS

Figure 14 shows the data transferred for the migration algorithms, which is associated with the size of the EHE. We reduced the size of the EHE by making calls to the simplifier only for complex simplifications, and implement the basic Boolean simplification while traversing the expression to replace atomic propositions by looking up the memory (in the operation rw). Since we have less calls, we apply a more aggressive simplification that is more costly<fnref n="26" />, but also reduces the size of the expressions. The x-axis indicates the algorithm's variant and the number of components, where Migr (resp. Migrr) stands for earliest the variant obligation (resp. round-robin). The y-axis is presented in logarithmic scale. We notice a significant drop in the size of EHE, dropping from 769 in the ISSTA'17 version for Migr-5 to 73.12.

## D DETAILED COMPARISON

Tables 7 and 8 present the detailed comparison for the synthetic scenario and Chiron, respectively. The metrics presented are (in order of columns): average information delay ($\delta_t$), normalized average number of messages (#Msgs), normalized data transferred (Data), maximum simplifications done by any given monitor per run, averaged across all runs ($S_{max}$), normalized critical simplifications

<footnote n="26">²⁶We use `ltlfilt` from [21] with `-boolean-to-isop` to rewrite Boolean subformulas as irredundant sum of products.</footnote>
<figure><img src="image_14.png" /><figcaption>Fig. 14. Size of EHE.</figcaption></figure>

<table><caption>Table 7. Synthetic Benchmark. Cells contains mean and standard deviation in parentheses.</caption><thead><tr><th>Alg.</th><th>|C|</th><th>δ<sub>t</sub></th><th>#Msgs</th><th>Data</th><th>S<sub>max</sub></th><th>S<sub>crit</sub></th><th>Conv<sub>E</sub></th></tr></thead><tbody><tr><td rowspan="4">Orch</td><td>3</td><td>0.48 (0.50)</td><td>2.44 (0.61)</td><td>31.84 (8.07)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.65 (0.02)</td></tr><tr><td>4</td><td>0.53 (0.50)</td><td>3.85 (0.94)</td><td>50.05 (12.39)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.74 (0.02)</td></tr><tr><td>5</td><td>0.64 (0.48)</td><td>5.30 (1.16)</td><td>69.20 (15.55)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.79 (0.02)</td></tr><tr><td>6</td><td>0.69 (0.46)</td><td>7.04 (1.50)</td><td>91.86 (20.02)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.83 (0.02)</td></tr><tr><td rowspan="4">Migr</td><td>3</td><td>0.58 (0.58)</td><td>0.27 (0.32)</td><td>8.46 (15.32)</td><td>4.72 (4.41)</td><td>3.08 (2.66)</td><td>0.65 (0.02)</td></tr><tr><td>4</td><td>0.71 (0.67)</td><td>0.32 (0.34)</td><td>17.45 (35.87)</td><td>6.10 (6.17)</td><td>4.03 (3.75)</td><td>0.73 (0.03)</td></tr><tr><td>5</td><td>0.96 (0.71)</td><td>0.43 (0.34)</td><td>30.41 (56.68)</td><td>7.41 (6.18)</td><td>4.97 (3.76)</td><td>0.79 (0.03)</td></tr><tr><td>6</td><td>1.19 (0.86)</td><td>0.50 (0.34)</td><td>98.80 (244.94)</td><td>10.09 (8.32)</td><td>6.74 (4.87)</td><td>0.82 (0.04)</td></tr><tr><td rowspan="4">Migrr</td><td>3</td><td>0.76 (0.69)</td><td>0.78 (0.33)</td><td>14.51 (18.40)</td><td>5.62 (4.99)</td><td>3.51 (2.93)</td><td>0.65 (0.02)</td></tr><tr><td>4</td><td>1.02 (0.90)</td><td>0.76 (0.36)</td><td>31.76 (51.55)</td><td>7.64 (7.16)</td><td>4.58 (4.04)</td><td>0.74 (0.03)</td></tr><tr><td>5</td><td>1.39 (1.04)</td><td>0.75 (0.35)</td><td>62.83 (91.89)</td><td>9.70 (7.88)</td><td>5.70 (4.25)</td><td>0.79 (0.03)</td></tr><tr><td>6</td><td>1.72 (1.19)</td><td>0.70 (0.37)</td><td>180.35 (360.25)</td><td>12.56 (9.76)</td><td>7.35 (5.14)</td><td>0.82 (0.03)</td></tr><tr><td rowspan="4">Chor</td><td>3</td><td>1.47 (1.99)</td><td>2.79 (1.10)</td><td>24.98 (9.85)</td><td>60.22 (242.88)</td><td>12.27 (6.55)</td><td>0.16 (0.12)</td></tr><tr><td>4</td><td>1.36 (1.52)</td><td>3.84 (1.23)</td><td>34.36 (10.94)</td><td>44.71 (184.05)</td><td>12.95 (5.98)</td><td>0.13 (0.12)</td></tr><tr><td>5</td><td>1.41 (1.55)</td><td>4.63 (1.37)</td><td>41.17 (12.16)</td><td>44.06 (223.15)</td><td>12.68 (6.06)</td><td>0.12 (0.11)</td></tr><tr><td>6</td><td>1.29 (1.38)</td><td>5.87 (1.66)</td><td>52.09 (14.77)</td><td>38.35 (215.27)</td><td>13.01 (6.01)</td><td>0.13 (0.12)</td></tr></tbody></table>

$(S_{crit})$, and convergence based on expressions evaluated $(Conv_E)$. For more details on the metrics, see Section 9.
<table><caption>Table 8. Metrics for Chiron traces. Cells contains mean and standard deviation in parentheses.</caption><thead><tr><th>Alg.</th><th>Spec</th><th>δ<sub>t</sub></th><th>#Msgs</th><th>Data</th><th>S<sub>max</sub></th><th>S<sub>crit</sub></th><th>Conv<sub>E</sub></th></tr></thead><tbody><tr><td rowspan="6">Orch</td><td>1</td><td>0.77 (0.42)</td><td>2.95 (0.00)</td><td>87.46 (0.00)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.74 (0.00)</td></tr><tr><td>2</td><td>1.00 (0.00)</td><td>2.95 (0.00)</td><td>87.46 (0.00)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.74 (0.00)</td></tr><tr><td>3</td><td>0.99 (0.10)</td><td>3.42 (0.02)</td><td>101.62 (1.00)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.75 (0.00)</td></tr><tr><td>5</td><td>0.94 (0.24)</td><td>2.95 (0.00)</td><td>87.46 (0.00)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.74 (0.00)</td></tr><tr><td>15a</td><td>1.00 (0.00)</td><td>2.95 (0.00)</td><td>87.46 (0.00)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.74 (0.00)</td></tr><tr><td>15b</td><td>1.00 (0.00)</td><td>3.00 (0.01)</td><td>88.90 (0.16)</td><td>0.00 (0.00)</td><td>0.00 (0.00)</td><td>0.75 (0.00)</td></tr><tr><td rowspan="6">Migr</td><td>1</td><td>1.66 (0.03)</td><td>0.02 (0.00)</td><td>0.52 (0.00)</td><td>8.00 (0.00)</td><td>2.03 (0.00)</td><td>0.74 (0.00)</td></tr><tr><td>2</td><td>1.00 (0.00)</td><td>0.57 (0.00)</td><td>13.09 (0.10)</td><td>4.00 (0.00)</td><td>3.10 (0.01)</td><td>0.74 (0.00)</td></tr><tr><td>3</td><td>1.86 (0.00)</td><td>0.88 (0.01)</td><td>70.23 (1.00)</td><td>13.00 (0.00)</td><td>9.76 (0.05)</td><td>0.75 (0.00)</td></tr><tr><td>5</td><td>1.67 (0.00)</td><td>0.02 (0.00)</td><td>0.52 (0.00)</td><td>8.00 (0.00)</td><td>2.03 (0.00)</td><td>0.74 (0.00)</td></tr><tr><td>15a</td><td>1.00 (0.00)</td><td>0.97 (0.00)</td><td>10.71 (0.04)</td><td>4.00 (0.00)</td><td>3.90 (0.00)</td><td>0.74 (0.00)</td></tr><tr><td>15b</td><td>1.00 (0.00)</td><td>1.00 (0.00)</td><td>19.36 (0.35)</td><td>9.02 (2.00)</td><td>7.00 (0.03)</td><td>0.75 (0.00)</td></tr><tr><td rowspan="6">Migrr</td><td>1</td><td>1.98 (0.00)</td><td>1.01 (0.01)</td><td>50.19 (0.33)</td><td>9.80 (1.37)</td><td>5.29 (0.07)</td><td>0.74 (0.00)</td></tr><tr><td>2</td><td>1.81 (0.02)</td><td>1.01 (0.01)</td><td>212.55 (3.17)</td><td>12.00 (0.00)</td><td>5.82 (0.05)</td><td>0.74 (0.00)</td></tr><tr><td>3</td><td>2.37 (0.03)</td><td>0.89 (0.02)</td><td>147.00 (3.97)</td><td>15.97 (0.22)</td><td>10.65 (0.09)</td><td>0.75 (0.01)</td></tr><tr><td>5</td><td>1.98 (0.01)</td><td>1.01 (0.00)</td><td>50.16 (0.30)</td><td>9.80 (1.35)</td><td>5.28 (0.06)</td><td>0.74 (0.00)</td></tr><tr><td>15a</td><td>1.99 (0.01)</td><td>1.01 (0.01)</td><td>83.80 (0.34)</td><td>8.64 (0.94)</td><td>4.91 (0.01)</td><td>0.74 (0.00)</td></tr><tr><td>15b</td><td>2.50 (0.01)</td><td>1.00 (0.00)</td><td>136.05 (0.27)</td><td>16.86 (0.35)</td><td>11.41 (0.01)</td><td>0.75 (0.00)</td></tr><tr><td rowspan="6">Chor</td><td>1</td><td>1.01 (0.00)</td><td>4.89 (0.00)</td><td>44.02 (0.00)</td><td>20.00 (0.00)</td><td>15.88 (0.32)</td><td>0.20 (0.01)</td></tr><tr><td>2</td><td>133.86 (0.17)</td><td>2.95 (0.00)</td><td>26.52 (0.00)</td><td>2798.38 (211.11)</td><td>21.41 (0.74)</td><td>0.67 (0.02)</td></tr><tr><td>3</td><td>1.22 (0.04)</td><td>4.40 (0.13)</td><td>39.64 (1.16)</td><td>23.65 (0.87)</td><td>18.18 (0.93)</td><td>0.33 (0.02)</td></tr><tr><td>5</td><td>1.01 (0.00)</td><td>4.89 (0.00)</td><td>44.02 (0.00)</td><td>20.00 (0.00)</td><td>15.85 (0.33)</td><td>0.20 (0.01)</td></tr><tr><td>15a</td><td>1.00 (0.00)</td><td>0.98 (0.00)</td><td>8.84 (0.00)</td><td>10.00 (0.00)</td><td>9.25 (0.07)</td><td>0.47 (0.01)</td></tr><tr><td>15b</td><td>116.52 (1.19)</td><td>2.00 (0.00)</td><td>18.00 (0.00)</td><td>3387.04 (316.16)</td><td>28.01 (1.13)</td><td>0.71 (0.00)</td></tr></tbody></table>

## E CHOREOGRAPHY SETUP PHASE

Choreography as presented in [15] splits the initial LTL formula into subformulas and delegates each subformula to a monitor on a component. Thus choreography presents a complicated setup phase. In this section, we present the setup phase. As such, we present the generation of the decentralized specification from a start LTL formula.

Choreography begins by taking the main formula, then deciding to split it into subformulas. Each monitor will monitor the subformula, notify other monitors of its verdict, and when needed *respawn*. Recall from the definition of $\Delta'$ (see Definition 5.4), that monitoring is recursively applied to the remainder of a trace starting at the current event. That is, initially we monitor from $e_0$ to $e_n$ and then from $e_1$ to $e_n$ and so forth. To do so, it is necessary to reset the state of a monitor appropriately, this process is called in [15] a *respawn*. Once the subformulas are determined, we generate an automaton per subformula to monitor it. Then, we construct the network of monitors in the form of a tree, in which the root is the main monitor. Verdicts for each subformula are then propagated in the hierarchy until a verdict can be reached by the root monitor.

A choreography monitor is a tuple $(id, A_{\phi_{id}}, ref_{id}, coref_{id}, respawn_{id})$ where:

* $id$ denotes the monitor unique identifier (label);

* $A_{id}$ the automaton that monitors the subformula;

* $ref_{id} : 2^{\text{Mons}}$ the monitors that this monitor should notify of a verdict;

* $coref_{id} : 2^{\text{Mons}}$ the monitors that send their verdicts to this monitor;
* `respawn_{id}: B_2` specifies whether the monitor should `respawn`;

To account for the verdicts from other monitors, the set of possible atoms is extended to include the verdict of a monitor identified by its id. Therefore, `Atoms = (N × AP) ∪ (Mons × N)`. Monitoring is done by replacing the subformula by the id of the monitor associated with it.

Before splitting a formula, it is necessary to determine the component that hosts its monitor. The component score is computed by counting the number of atomic propositions associated with a component in the subformula.

$$ 
\begin{align*}
\text{scor}(\varphi, c) : LTL \times C \to \mathbb{N} \\
&= \text{match } \varphi \text{ with} \\
& | a \in AP \quad \rightarrow \quad \begin{cases} 1 & \text{if } \text{lu}(a) = c \\ 0 & \text{otherwise} \end{cases} \\
& | \text{op } \varphi \quad \rightarrow \quad \text{scor}(\varphi, c) \\
& | \varphi \text{ op } \varphi' \quad \rightarrow \quad \text{scor}(\varphi, c) + \text{scor}(\varphi', c)
\end{align*}
$$

The chosen component is determined by the component with the highest score, using `chc: LTL → C`:

$$ \text{chc}(\varphi) = \underset{c \in C}{\operatorname{argmax}}(\text{scor}(\varphi, c)) $$

In order to setup the network of monitors, firstly the LTL expression is split into subformulas and the necessary monitors are generated to monitor each subformula. The tree of monitors is generated by recursively splitting the formula at the binary operators. We present the `setup` phase as a tree traversal of the LTL formula to generate the monitor network, merging nodes at each operator, which is a different flavor of the generation procedure in [15]. Given the two operands, we choose which operands remains in the host component, and (if necessary) which would be placed on a different component. Therefore, we add the constraint that at least one part of the LTL expression must still remain in the same component. Given two formulas $\varphi$ and $\varphi'$ and an initial base component $c_b$ we determine the two components that should host $\varphi$ and $\varphi'$ with the restriction that one of them is $c_b$:

$$ 
\begin{align*}
c_1 &= \text{chc}(\varphi), & c_2 &= \text{chc}(\varphi') \\
s_1 &= \text{scor}(\varphi, c_b), & s_2 &= \text{scor}(\varphi', c_b) \\
\text{split}(\varphi, \varphi', c_b) &= \begin{cases} \langle c_b, c_b \rangle & \text{if } c_1 = c_2 = c_b \\ \langle c_1, c_b \rangle & \text{if } (c_1 \neq c_b) \\ \langle c_b, c_2 \rangle & \text{otherwise} \end{cases} \quad \begin{array}{l} \wedge (c_2 = c_b \lor s_2 > s_1) \\ \\ \text{otherwise} \end{array}
\end{align*}
$$

Algorithm 3 displays the procedure to split the formula. For each binary operator, we determine which of the operands needs to be hosted in a new component. The result is a tuple: $\langle \text{root}, N, E \rangle$ where:

* `root` is the root of the tree;

* `N` is the set of generated monitor data;

* `E` is the set of edges between the monitors.

Monitor data is a pair $\langle \text{id}, \text{spec} \rangle$ that represents the id of the monitor and the formula that it monitors.

* First, `chc` determines the host component where the root monitor resides.

* Second, the AST of the LTL formula is traversed using `netx`, which splits on binary operators.
<table><caption>**Algorithm 3** Setting up the monitor tree</caption><tr><td>1:</td><td>procedure NET_CHOR(φ, C, M)</td><td></td></tr><tr><td>2:</td><td>id ← 0</td><td></td></tr><tr><td>3:</td><td>c<sub>h</sub> ← chc(φ)</td><td></td></tr><tr><td>4:</td><td>⟨root, mons, edges⟩ ← netx(φ, id, c<sub>h</sub>)</td><td></td></tr><tr><td>5:</td><td>return ⟨{root} ∪ mons, edges⟩</td><td></td></tr><tr><td>6:</td><td>end procedure</td><td></td></tr><tr><td>7:</td><td>procedure netx(φ, id<sub>c</sub>, c<sub>h</sub>)</td><td></td></tr><tr><td>8:</td><td>if φ ∈ AP then</td><td></td></tr><tr><td>9:</td><td>m ← ⟨φ, id<sub>c</sub>⟩</td><td></td></tr><tr><td>10:</td><td>return ⟨m, ∅, ∅⟩</td><td></td></tr><tr><td>11:</td><td>else if φ matches op e then</td><td>► Unary Operator</td></tr><tr><td>12:</td><td>o ← netx(e, id<sub>c</sub>, c<sub>h</sub>)</td><td></td></tr><tr><td>13:</td><td>m ← ⟨op o.f, id<sub>c</sub>⟩</td><td></td></tr><tr><td>14:</td><td>return ⟨m, o.N, o.E⟩</td><td></td></tr><tr><td>15:</td><td>else if φ matches e op e' then</td><td></td></tr><tr><td>16:</td><td>⟨c<sub>1</sub>, c<sub>2</sub>⟩ ← split(e, e', c<sub>h</sub>, M)</td><td></td></tr><tr><td>17:</td><td>if c<sub>1</sub> = c<sub>2</sub> = c<sub>h</sub> then</td><td>► No Split</td></tr><tr><td>18:</td><td>l ← netx(e, id<sub>c</sub>, c<sub>h</sub>)</td><td></td></tr><tr><td>19:</td><td>r ← netx(e', id<sub>c</sub>, c<sub>h</sub>)</td><td></td></tr><tr><td>20:</td><td>m ← ⟨l.f op r.f, id<sub>c</sub>⟩</td><td></td></tr><tr><td>21:</td><td>return ⟨m, l.N ∪ r.N, l.E ∪ r.E⟩</td><td></td></tr><tr><td>22:</td><td>else if c<sub>1</sub> = c<sub>h</sub> then</td><td>► Split Right Branch</td></tr><tr><td>23:</td><td>id<sub>n</sub> ← newid()</td><td></td></tr><tr><td>24:</td><td>l ← netx(e, id<sub>c</sub>, c<sub>h</sub>)</td><td></td></tr><tr><td>25:</td><td>r ← netx(e', id<sub>n</sub>, c<sub>2</sub>)</td><td></td></tr><tr><td>26:</td><td>m ← ⟨l.f op ⟨id<sub>n</sub>⟩, id<sub>c</sub>⟩</td><td></td></tr><tr><td>27:</td><td>return ⟨m, (l.N ∪ r.N ∪ r.root), (l.E ∪ r.E ∪ ⟨⟨id<sub>n</sub>, id<sub>c</sub>⟩⟩)</⟩</td><td></td></tr><tr><td>28:</td><td>else</td><td>► Split Left Branch</td></tr><tr><td>29:</td><td>id<sub>n</sub> ← newid()</td><td></td></tr><tr><td>30:</td><td>l ← netx(e, id<sub>n</sub>, c<sub>1</sub>)</td><td></td></tr><tr><td>31:</td><td>r ← netx(e', id<sub>c</sub>, c<sub>h</sub>)</td><td></td></tr><tr><td>32:</td><td>m ← ⟨⟨id<sub>n</sub>⟩ op r.f, id<sub>c</sub>⟩</td><td></td></tr><tr><td>33:</td><td>return ⟨m, (l.N ∪ r.N ∪ l.root), (l.E ∪ r.E ∪ ⟨⟨id<sub>n</sub>, id<sub>c</sub>⟩⟩)</⟩</td><td></td></tr><tr><td>34:</td><td>end if</td><td></td></tr><tr><td>35:</td><td>end if</td><td></td></tr><tr><td>36:</td><td>end procedure</td><td></td></tr></table>

- If both formulae can be monitored with the same monitor it does not split.

- Otherwise

(1) We recurse on the side kept, to further split the formula;

(2) We recurse on the side split, with a new *host* and *id*;

(3) We merge the subnetworks by:

(a) Generating the host monitor with the formula resulting from the recursion;

(b) Connecting the split branch's root monitor to the current host monitor;

(c) Adding the split branch's root monitor to the set of additional monitors;

(d) Merging the set of additional monitors and edges from both branches.

Once the monitor data tree is created, monitors are created accordingly, generating an automaton for the subformula, where some of its atomic propositions have been replaced with monitor ids. Each monitor is initialized with the refs and corefs set based on the edges setup.

REMARK 2 (COMPACTING THE NETWORK). The monitor network can further be compacted as follows; monitors with the same subformula are merged into one, and their refs and corefs will be the result of the set union. However, one or more merged monitor will have to replace all occurrences of the id of the other monitors in all subformulas of all monitors.