Proof of Compositionality of CFT Correctness

TL;DR

This paper provides a formal proof demonstrating the compositional correctness of component fault trees, ensuring that system reliability can be verified through modular analysis.

Contribution

It offers the first formal proof of the central theorem on the compositionality of fault tree correctness, advancing theoretical understanding.

Findings

Formal proof of fault tree compositionality

Validation of modular reliability analysis

Theoretical foundation for fault tree methods

Abstract

In the paper Compositionality of Component Fault Trees, we present a discussion of the compositionality of correctness of component fault trees. In this technical report, we present the formal proof of the central theorem of the aforementioned publication.

Equations

$$m_1{\approx }_{\overline{A_i}}\square \text{ and }{m}_2{\approx }_{\overline{A_i}}\square \text{ or }$$

$$q_i=q_1=q_2\text{ and }{t}_i=ex\text{ or }$$

$$q_i=q_1=q_2\text{ and }{t}_i=val\text{ and }{v}_1=v_2$$

$$t_1=\varnothing \text{ and }{t}_2=\varnothing \text{ or}$$

$$t_1=m_1⌢t_1^{\prime }\text{ and }{m}_1{\approx }_{\overline{A_i}}\square \text{ and }{t}_1^{\prime }{\approx }_{\overline{A_i}}{t}_2\text{ or}$$

$$t_2=m_2⌢t_2^{\prime }\text{ and }{m}_2{\approx }_{\overline{A_i}}\square \text{ and }{t}_1{\approx }_{\overline{A_i}}{t}_2^{\prime }\text{ or}$$

$$t_1=m_1⌢t_1^{\prime }\text{ and }{t}_2=m_2⌢t_2^{\prime }\text{ and }{m}_1{\approx }_{\overline{A_i}}{m}_2\text{ and }{t}_1^{\prime }{\approx }_{\overline{A_i}}{t}_2^{\prime }$$

$$\forall p?v\in \omega (t_1)$$

$$\forall q?u\in {\omega }_f(t_2)$$

$$\forall {\omega }_f,{\omega }_c\forall t_f\bullet {\omega }_f{\approx }_{\overline{P},\overline{E}}{\omega }_c\wedge {\omega }_f\models c\stackrel{t_f}{\to }⟹\exists t_c\bullet {\omega }_c\models c\stackrel{t_c}{\to }\wedge t_f{\approx }_{\overline{P},\overline{E}}{t}_c$$

$$c\stackrel{p?v}{\to }$$

$$c\stackrel{m_1}{\to }\text{ and }c\stackrel{m_2}{\to }\text{ and }{m}_1\ne m_2$$

$$c\stackrel{m}{\to }{c}_1\text{ and }c\stackrel{m}{\to }{c}_2$$

$$\overline{P_{c,d}^{\prime }}=$$

$$\overline{P_i^{\prime }}=$$

$$(\overline{A_1}\sqcap \dots \overline{A_m}\sqcap \overline{A_{m+1}}\sqcap \overline{P_{m+1}^{2x1}}\sqcap \dots \sqcap \overline{A_{m+k}}\sqcap \overline{P_{m+k}^{2xk}})\bigsqcup$$

$$\dots \bigsqcup$$

$$(\overline{A_1}\sqcap \dots \overline{A_m}\sqcap \overline{A_{m+1}}\sqcap \overline{P_{m+1}^{ox1}}\sqcap \dots \sqcap \overline{A_{m+k}}\overline{P_{m+k}^{oxk}})$$

$$\overline{P_i^{\prime }}=$$

$$\dots \bigsqcup (\overline{P_i}\sqcap \overline{P_{m+1}^{ox1}}\sqcap \dots \sqcap \overline{P_{m+k}^{oxk}})$$

$$\overline{P_i^{\prime }}=$$

$$(\overline{A_1}\sqcap \dots \overline{A_m}\sqcap \overline{A_{m+1}}\sqcap \overline{P_{m+1}^{2x1}}\sqcap \dots \sqcap \overline{A_{m+k}}\sqcap \overline{P_{m+k}^{2xk}})\bigsqcup$$

$$\dots \bigsqcup$$

$$(\overline{A_1}\sqcap \dots \overline{A_m}\sqcap \overline{A_{m+1}}\sqcap \overline{P_{m+1}^{ox1}}\sqcap \dots \sqcap \overline{A_{m+k}}\overline{P_{m+k}^{oxk}})$$

$${\omega }_f^{\prime }(t)$$

$${\omega }_c^{\prime }(t)$$

$${\omega }_f^{\prime }(t)$$

$${\omega }_c^{\prime }(t)$$

Full text

1 Introduction

This technical report presents the formal proof for the compositionality of correctness of Component Fault Trees (CFTs). This report accompanies the paper [3], which contains additional explanations and examples for the definitions, Lemmas and theorems presented here. Please note that this technical report is not meant to be self contained, but is intended to be comprehensible only in combination with the original paper.

The structure of this report is as follows: First we provide a formal definition for components, Component Fault Trees, and correctness of CFTs. In the following section, we define composition of component fault trees and formulate our central theorem stating that correctness of CFTs is compositional. The formal proof for this theorem is rather lengthy and technical and is presented in the final section.

2 Components and Component Fault Trees

In the remainder of this work we take the formalization of components from Greiner and Grahl  [1] and reuse their notation for better comparability of further results in this paper.

A component has an internal state, input ports, and output ports. A component can receive messages via input ports and send messages via its output ports. Received messages can trigger the component to change its internal state. Formally, we consider components as Input-Output Labeled Transition Systems (see [2] for a formal definition of IOLTS). A port has a name and a signature, i. e. names and types of variables that can be communicated via the port. For a message $m$ communicated via an input port with name $p$ with value $v$, we write $m=p?v$, for a message $n$ communicated via an output port with name $q$ with value $w$, we write $n=q!w$. We refer to the set of all messages communicated via an input port as inputs, and the set of all messages communicated via an output port as outputs. If it does not matter whether a message is an input or an output, we write $m=p.v$ or $n=q.w$ respectively. We write $c\xrightarrow{m}c^{\prime}$ for a component $c$ communicating message $m$ and transitioning to a component $c^{\prime}$. You can consider $c^{\prime}$ to have a changed internal state. If $c^{\prime}$ is irrelevant, we write $c\xrightarrow{m}$, if there exists some $c^{\prime}$ such that $c\xrightarrow{m}c^{\prime}$.

The behavioral definition of a component limits the sequence of messages a component can communicate. We refer to a sequence of messages as a trace. We use $\smallfrown$ as the concatenation operator for traces and $\varnothing$ to refer to the empty trace. The length of a trace is defined as the amount of messages in a trace. We write $c\xrightarrow{t}c^{\prime}$ if a component $c$ transitions to component $c^{\prime}$ while communicating the trace $t$. A component $c$ can communicate a trace $t\smallfrown m$ while transitioning to component $c^{\prime}$, if there exists a component $c^{\prime\prime}$ such that $c\xrightarrow{t}c^{\prime\prime}$ and $c^{\prime\prime}\xrightarrow{m}c^{\prime}$. We again write $c\xrightarrow{t}$, if there exists some $c^{\prime}$ such that $c\xrightarrow{t}c^{\prime}$. We refer to all possible traces as $\mathcal{T}$. Finally, we explicitly define environments in which components can run. Environments model the entities providing inputs to a component after observing the behavior of the component.

Definition 1 (Environment).

An environment $\omega$ is a function $\mathcal{T}\mapsto\mathcal{P}(\mathcal{I})$, where $\mathcal{P}(\mathcal{I})$ is the powerset of all inputs.

Definition 2 (Communication under Environment).

A component $c$ can communicate a trace $t$ under an environment $\omega$, written $\omega\models c\xrightarrow{t}$, iff $c\xrightarrow{t}$ and for all $t_{1},t_{2},p?v$ with $t=t_{1}\smallfrown p?v\smallfrown t_{2}$, it holds that $p?v\in\omega(t_{1})$.

Definition 3 (Event).

An event $E$ is a tuple $(p,t)$, where $p$ is port and $t$ is a type. If $p$ is an input (output) port, $E$ is an input (output) event.

Definition 4 (CFT).

A CFT is a tuple $(P,E)$, where $P$ is a propositional logic formula, where each literal in $P$ is an input event, and each input event only appears non-negated in $P$. $E$ is an output event.

For every propositional formula $P$, with literals only appearing non-negated, the formula $\overline{P}$ is a propositional formula with literals only appearing negated. For $\overline{P}$ we can always find a disjunctive normal form with clauses $\overline{P_{1}},...\overline{P_{n}}$, such that $\overline{P}=\overline{P_{1}}\sqcup...\sqcup\overline{P_{n}}$. $\overline{P}\Rightarrow\overline{E}$ then holds, iff for all clauses $\overline{P}_{i}$ it holds that $\overline{P}_{i}\Rightarrow\overline{E}$.

Definition 5 (Clause).

A clause $\overline{P_{i}}$ is a propositional formula, where each literal only appears negated and $\sqcap$ is the only logical operator in the formula.

Definition 6 (Message Event-Equivalence).

A message $m=q.v$ is irrelevant w.r.t. an event $A_{i}=(q_{i},t_{i})$, if $q\neq q_{i}$. For a message $m$ that is irrelevant, we write $m\approx_{\overline{A_{i}}}\square$.

Two messages $m_{1}=q_{1}.v_{1}$ and $m_{2}=q_{2}.v_{2}$ are event-equivalent w.r.t. an event $A_{i}=(q_{i},t_{i})$, written $m_{1}\approx_{\overline{A_{i}}}m_{2}$, if

[TABLE]

Two messages $m_{1}=q_{1}.v_{1}$ and $m_{2}=q_{2}.v_{2}$ are event-equivalent w.r.t. a clause $\overline{P_{i}}=\overline{A_{1}}\sqcap\dots\sqcap\overline{A_{n}}$, written $m_{1}\approx_{\overline{P_{i}}}m_{2}$, if $m_{1}\approx_{\overline{A_{i}}}m_{2}\text{ for all }0<i\leq n$

Two messages $m_{1}=q_{1}.v_{1}$ and $m_{2}=q_{2}.v_{2}$ are event-equivalent w.r.t. a clause $\overline{P_{i}}$ and an event $E$, written $m_{1}\approx_{\overline{P_{i}},\overline{E}}m_{2}$, if $m_{1}\approx_{\overline{P_{i}}}m_{2}\text{ and }m_{1}\approx_{E}m_{2}$

Definition 7 (Trace Event-Equivalence).

Two traces $t_{1},t_{2}$ are event-equivalent w.r.t. an event $A_{i}$, written $t_{1}\approx_{\overline{A_{i}}}t_{2}$, iff

[TABLE]

Event-equivalence of traces w.r.t. a clause is defined analogously.

Definition 8 (Erroneous Environment).

$\omega_{f}$ is an erroneous environment for $\omega$ w.r.t. a clause $\overline{P_{i}}$ and an output event $E$, written $\omega_{f}\approx_{\overline{P_{i}},\overline{E}}\omega$, iff for all $t_{1}\approx_{\overline{P_{i}},\overline{E}}t_{2}$ it holds that

[TABLE]

Definition 9 (Environment (extd.)).

A function $\omega$ is an environment w.r.t. a clause $\overline{P_{i}}$ and an event $E$, iff it is an environment according to Definition 1, and $\omega$ is an erroneous environment to itself according to Definition 8 (i. e., $\omega\approx_{\overline{P_{i}},\overline{E}}\omega$).

Definition 10 (Clause correctness w.r.t. a component).

Given the relation $\approx_{\overline{P},\overline{E}}$ for the clause $\overline{P}$ and the output event $E$. $\overline{P}$ and $E$ are correct w.r.t. a component $c$, if

[TABLE]

Definition 11 (CFT correctness w.r.t. a component).

Given a component $c$, a CFT $(P,E)$ with $\overline{P}=\overline{P_{1}}\sqcup...\sqcup\overline{P_{n}}$. $(P,E)$ is correct w.r.t. $c$, iff $\overline{P_{i}}$ and $E$ are correct w.r.t. $c$ for all $0<i\leq n$.

3 Compositionality of Component Fault Tree Correctness

Definition 12 (CFT composition).

Let $c$ and $d$ be components, $p_{1}\ldots p_{n}$ ports, which are input ports of $c$ and outputs ports of $d$, $A^{1}_{1}\ldots A^{1}_{m_{1}},\ldots A^{n}_{1}\ldots A^{n}_{m_{n}}$ events with $A^{i}_{j}$ being an event on port $p_{i}$, i.e. an input event of $c$ and an output event of $d$. Let further be $(P_{c},E)$ be a CFT of $c$ and $(P^{i}_{j},A^{i}_{j})$ the CFTs of $d$ for the output events $A^{i}_{j}$.

We define the CFT of the composition of $c$ and $d$ for output event $E$ as $(P_{c,d},E)$, where $P_{c,d}$ is formula $P_{c}$ with each occurrence of $A^{i}_{j}$ is replaced by $P^{i}_{j}$.

Definition 13 (Deterministic components).

A component $c$ is deterministic, if

[TABLE]

In the remainder, we assume all components to be deterministic.

Theorem 3.1 (Composed CFT correctness w.r.t. composition).

Given components $c$ and $d$, CFT $(P_{c},E)$ of $c$ and $(P^{i}_{j},A^{i}_{j})$ of $d$ as in Definition 12, such that the CFTs are correct w.r.t. the respective components. Then the composed CFT $(P_{c,d},E)$ is correct w.r.t. the composition of $c$ and $d$.

4 Proof of Compositionality of CFT Correctness

In this section, we present the proof for Theorem 3.1.

The structure of the proof is as follows. First we define a notion of CFT composition in Definition 14 which is more strict than the composition as defined above. We then show two lemmas about the structure of the formula resulting from the strict CFT composition in Lemmas 1 and 2. We then show correctness of the strict composed CFT w.r.t. the component $c$ (Lemma 3) and $d$ (Lemma 5). For the correctness w.r.t. $d$, we require an additional Lemma about counterexamples for the correctness (Lemma 4).

Finally, the proofs for the correctness of the strict composition w.r.t. the composition of $c$ and $d$ (Theorem 4.1) and finally Theorem 3.1 follow relatively directly from the Lemmas.

Definition 14 (Strict CFT composition).

Let $c$ and $d$ be components, $p_{1}\ldots p_{n}$ ports, which are input ports of $c$ and outputs ports of $d$, $A^{1}_{1}\ldots A^{1}_{m_{1}},\ldots A^{n}_{1}\ldots A^{n}_{m_{n}}$ events with $A^{i}_{j}$ being an event on port $p_{i}$, i.e. an input event of $c$ and an output event of $d$. Let further be $(P_{c},E)$ be a CFT of $c$ and $(P^{i}_{j},A^{i}_{j})$ the CFTs of $d$ for the output events $A^{i}_{j}$.

We then define the CFT of the strict composition of $c$ and $d$ for the output event $E$ as $(P_{c,d}^{\prime},E)$, where $P_{c,d}$ is the formula $P_{c}$ with each occurrence of $A^{i}_{j}$ is replaced by $A^{i}_{j}\sqcap P^{i}_{j}$.

Note that Definition 14 differs from Definition 12 only in a way such that we keep the events of the connected ports in the formula.

Lemma 1.

Let $\overline{P_{1}}\ldots\overline{P_{n}}$ be the clauses of the CFT $(P_{c},E)$, i. e. $\overline{P_{c}}=\overline{P_{1}}\sqcup\ldots\sqcup\overline{P_{n}}$

Then $\overline{P_{c,d}^{\prime}}=\overline{P_{1}^{\prime}}\sqcup\ldots\sqcup\overline{P_{n}^{\prime}}$ with $\overline{P_{i}^{\prime}}=\overline{P_{i}}\sqcap\overline{P_{m+1}}\sqcap\ldots\sqcap\overline{P_{m+k}}$, where $P_{m+i}$ is the formula from the CFT $(P_{m+1},A_{i})$ of $d$.

Proof.

[TABLE]

∎

Lemma 2.

Let $\overline{P_{1}}\ldots\overline{P_{n}}$ be the clauses of the CFT $(P_{c},E)$, i. e. $\overline{P_{c}}=\overline{P_{1}}\sqcup\ldots\sqcup\overline{P_{n}}$

Then $\overline{P_{c,d}^{\prime}}=\overline{P_{1}^{\prime}}\sqcup\ldots\sqcup\overline{P_{n}^{\prime}}$ with

[TABLE]

where $\overline{A_{1}}\ldots\overline{A_{m}}$ are clauses of the CFT $(P_{c},E)$ and $\overline{P^{1x1}_{m+1}}$ is a clause of the CFT $(P_{m+i},A_{m+i})$ of $c$.

Proof.

We continue the re-ordering of the formula of $P_{i}^{\prime}$ from the proof of Lemma 1

[TABLE]

∎

Now we can show that the strict composition of the CFTs is correct w.r.t. the component $c$.

Lemma 3.

If CFT $(P_{c},E)$ is correct w.r.t. $c$, then $(P_{c,d}^{\prime},E)$ is also correct w.r.t. $c$.

Proof.

A closer look at Lemma 1 shows that the clause $\overline{P_{i}^{\prime}}$ differs from $\overline{P_{i}}$ only by the clauses $\overline{P_{m+1}}$ to $\overline{P_{m+k}}$, which only contain events of input ports of $d$. By assumption, $c$ can not communicate messages over these ports, therefore the difference has no effect on the specification of $\approx_{\overline{P_{i}^{\prime}},\overline{E}}$ w.r.t. messages $c$ can communicate. Therefore, the correctness of $(P_{c,d}^{\prime},E)$ w.r.t. $c$ follows directly from the correctness of $(P_{c},E)$. ∎

Lemma 4.

Let $\omega_{f},\omega_{c}^{\prime\prime},t_{1}$ be a counterexample for correctness of clause $\overline{P_{f}}$ w.r.t. $d$ and $\omega_{c}^{\prime\prime}$ does not provide irrelevant inputs w.r.t. $\overline{P_{f}},\overline{E}$.

Let further $\omega_{c}^{\prime}$ and $\omega_{f}^{\prime}$ be environments such that for all $t$ with for all prefixes $t_{1}^{\prime}$ of $t_{1}$, i. e. $t_{1}=t_{1}^{\prime}\smallfrown t_{1}^{\prime\prime}$ it does not hold that $t\approx_{\overline{P_{f}},\overline{E}}t_{1}^{\prime}$, it holds

[TABLE]

Let further $\omega_{c}^{\prime}$ and $\omega_{f}^{\prime}$ be such that for all $t$ with for all $t_{1}=t_{1}^{\prime}\smallfrown p?v\smallfrown t_{1}^{\prime\prime}$ and $t\approx_{\overline{P_{f}},\overline{E}}t_{1}^{\prime}$ (i. e. there exists a prefix of $t_{1}$ equivalent to $t$), it holds

[TABLE]

Then $\omega_{f}^{\prime},\omega_{c}^{\prime},t_{1}$ is a counterexample for correctness of clause $\overline{P_{f}}$ w.r.t. $d$.

Note that $\omega_{f}^{\prime}$ only offers input messages used in the counterexample and $\omega_{c}^{\prime}$ only offers messages required to be equivalent to $\omega_{f}^{\prime}$. Further, of course, $\omega_{c}^{\prime}$ does not provide irrelevant input messages.

Proof.

By definition, $\omega_{c}^{\prime}$ only contains one message per trace and port, and does not provide invisible input.

By construction, $\omega_{c}^{\prime}$ and $\omega_{f}^{\prime}$ are environments w.r.t. $\approx_{\overline{P_{f}},\overline{E}}$ (Definition 9).

It holds that $\omega_{f}^{\prime}\approx_{\overline{P_{f}},\overline{E}}\omega_{c}^{\prime}$, $\omega_{f}^{\prime}\models d\xrightarrow{t_{1}}$, and for all traces $t$ it holds $\omega_{c}^{\prime}\models d\xrightarrow{t}\implies\omega_{c}\models d\xrightarrow{t}$.

Therefore, if $\omega_{f},\omega_{c}^{\prime\prime},t_{1}$ is a counterexample for the correctness of $P_{f},E$ w.r.t. $d$, then $\omega_{f}^{\prime},\omega_{c}^{\prime},t_{1}$ is a counterexample. ∎

Showing correctness of $(P_{c,d}^{\prime},E)$ w.r.t. $d$ is more complex.

Lemma 5.

If all CFTs $(P_{m+i},A_{i})$ are correct w.r.t. $d$, then $(P_{c,d}^{\prime},E)$ is correct w.r.t. $d$.

Proof.

All CFTs of $d$ are correct w.r.t. $d$. We assume towards contradiction that CFT $(P_{c,d}^{\prime},E)$ is not correct w.r.t. $d$.

Thus, there exist a clause $\overline{P_{f}}$ defined by the CFT $(P_{c,d}^{\prime},E)$, such that $\overline{P_{f}}$ is not correct w.r.t $d$ according to Definition 11.

According to Definition 10, there has to exists a correct environment $\omega_{c}$ and an erroneous environment $\omega_{f}$ with $\omega_{f}\approx_{\overline{P_{f}},\overline{E}}\omega_{c}$, and a trace $t_{1}$ with $\omega_{f}\models c\xrightarrow{t_{1}}$ such that for all $t_{2}$ with $\omega_{c}\models d\xrightarrow{t_{2}}$, it does not hold that $t_{1}\approx_{\overline{P},\overline{E}}t_{2}$.

Note that $t_{1}$ and $t_{2}$ can only contain messages, which are communicated via ports which are input or output ports of $d$, since according to Definition 10, $d$ can communicate the traces.

From the counterexample $\omega_{f},\omega_{c}$, and $t_{1}$, we construct a simpler counterexample. We construct an environment $\omega_{c}^{\prime\prime}$ by removing all invisible events: $\omega_{c}^{\prime\prime}(t)=\{m|m\in\omega_{c}(t)\wedge!(m\approx_{\overline{P_{f}},\overline{E}}\square)\}$ for all $t$. According to Lemma 7 in [1], $\omega_{f},\omega_{c}^{\prime\prime},t_{1}$ is a counterexample for correctness of $P_{f}$ w.r.t. $d$.

According to Lemma 4, there exists a simpler counterexample $\omega_{f}^{\prime}$, $\omega_{c}^{\prime}$, $t_{1}$.

We now show that $\omega_{f}^{\prime},\omega_{c}^{\prime},t_{1}$ can not be a counterexample for correctness.

Let $t_{1}^{\prime}$ be the longest prefix of $t_{1}$, such that there exists a $t_{2}^{\prime}$ under $\omega_{f}^{\prime}$ and $\omega_{c}^{\prime}$ with $t_{1}^{\prime}\approx_{\overline{P_{f}},\overline{E}}t_{2}^{\prime}$. Then $t_{1}^{\prime}\smallfrown m_{1}$ is a prefix of $t_{1}$. Further, $m_{1}$ has to be relevant w.r.t. $\approx_{\overline{P_{f}},\overline{E}}$, because otherwise $t_{1}^{\prime}\smallfrown m_{1}$ would be longer than $t_{1}^{\prime}$ and $t_{1}^{\prime}\smallfrown m_{1}\approx_{\overline{P_{f}},\overline{E}}t_{2}^{\prime}$.

Also, $m_{1}$ can not be an input to $d$. Otherwise, we would know that $m_{1}\in\omega_{f}^{\prime}(t_{1}^{\prime})$. Since $\omega_{f}^{\prime}\approx_{\overline{P_{f}},\overline{E}}\omega_{c}^{\prime}$ there exists $m_{2}\in\omega_{c}^{\prime}(t_{2}^{\prime})$ with $m_{1}\approx_{\overline{P_{f}},\overline{E}}m_{2}$. By construction of $\approx_{\overline{P_{f}},\overline{E}}$ (Definition 6) $m_{1}$ and $m_{2}$ are communicated over the same port (Definition 13), and since $d$ is input-indiscriminate $t_{1}^{\prime}\smallfrown m_{1}\approx_{\overline{P_{f}},\overline{E}}t_{2}^{\prime}\smallfrown m_{2}$ and $\omega_{c}^{\prime}\models d\xrightarrow{t_{2}^{\prime}\smallfrown m_{2}}$ (also Definition 13). This means, again, $t_{1}^{\prime}$ would not be the longest suffix with the property mentioned above.

Since all CFTs of $d$ are correct w.r.t. $d$, also all clauses $P_{i}^{\prime}$, defined by its CFTs, are correct w.r.t. $d$. Let $\overline{P^{i}_{j}}$ and $\overline{P^{k}_{l}}$ be arbitrary clauses for CFTs with output events $A^{x}_{i}$ and $A^{y}_{l}$ contained in the clause $P_{f}$. Due to correctness w.r.t. $d$, we know that there exist traces $t^{a}_{2}$ and $t^{b}_{2}$ such that $\omega_{c}^{\prime}\models d\xrightarrow{t^{a}_{2}}$ and $\omega_{c}^{\prime}\models d\xrightarrow{t^{b}_{2}}$ with $t_{1}\approx_{\overline{A^{x}_{i}},\overline{P^{i}_{j}}}t^{a}_{2}$ and $t_{1}\approx_{\overline{A^{y}_{l}},\overline{P^{k}_{l}}}t^{b}_{2}$.

We inductively show that $t^{a}_{2}$ and $t^{b}_{2}$ are in fact the same traces, i.e. $t^{a}_{2}=t^{b}_{2}$.

Induction Hypothesis: For prefixes ${t^{a}}_{2}^{\prime}$ of $t^{a}_{2}$ with length $n$, and all prefixes ${t^{b}}_{2}^{\prime}$ of $t^{b}_{2}$ with length $n$ it holds that ${t^{a}}_{2}^{\prime}={t^{b}}_{2}^{\prime}$.

Induction Start: For length $n=0$ ${t^{a}}_{2}^{\prime}$ and ${t^{b}}_{2}^{\prime}$ are empty traces and the Hypothesis holds trivially.

Induction Step: Let ${t^{a}}_{2}^{\prime}={t^{a}}_{2}^{\prime\prime}\smallfrown m^{a}_{2}$ and ${t^{b}}_{2}^{\prime}={t^{b}}_{2}^{\prime\prime}\smallfrown m^{b}_{2}$.

Case 1: $m^{a}_{2}$ is input. Since $\omega_{c}^{\prime}$ does not provide irrelevant inputs, $m^{a}_{2}$ has to be relevant w.r.t. $\approx_{\overline{P_{f}},\overline{E}}$, and analogous for $m^{b}_{2}$. Further, since $t^{a}_{2}\approx_{\overline{A^{x}_{i}},\overline{P^{i}_{j}}}t_{1}$ and $t^{b}_{2}\approx_{\overline{A^{y}_{l}},\overline{P^{k}_{l}}}t_{1}$, there exists an $m_{1}$ with $t_{1}^{\prime}\smallfrown m_{1}$ being a prefix of $t_{1}$ with ${t^{a}}_{2}^{\prime}\smallfrown m^{a}_{2}\approx_{\overline{A^{x}_{i}},\overline{P^{i}_{j}}}t_{1}^{\prime}\smallfrown m_{1}$ and ${t^{b}}_{2}^{\prime}\smallfrown m^{b}_{2}\approx_{\overline{A^{y}_{l}},\overline{P^{k}_{l}}}t_{1}^{\prime}\smallfrown m_{1}$. Therefore, $m_{1},m^{a}_{2},m^{b}_{2}$ are communicated on the same port. By construction, $\omega_{c}^{\prime}$ only provides one relevant input per port, therefore $m^{a}_{2}=m^{b}_{2}$, and thus with the induction hypothesis ${t^{a}}_{2}^{\prime}\smallfrown m^{a}_{2}={t^{b}}_{2}^{\prime}\smallfrown m^{b}_{2}$.

Case 2: $m^{a}_{2}$ is output. Since $d$ is output deterministic and by induction hypothesis, $m^{a}_{2}=m^{b}_{2}$, and again ${t^{a}}_{2}^{\prime}\smallfrown m^{a}_{2}={t^{b}}_{2}^{\prime}\smallfrown m^{b}_{2}$.

Since $t^{a}_{2}=t^{b}_{2}$ and by the structure of $P_{f}$ (Lemma 2), by the definition of $\approx_{\overline{A^{x}_{i}},\overline{P^{i}_{j}}}$, $\approx_{\overline{A^{y}_{l}},\overline{P^{k}_{l}}}$, and $\approx_{\overline{P_{f}},\overline{E}}$ according to Definition 6, and since $t^{1}\approx_{\overline{A^{x}_{i}},\overline{P^{i}_{j}}}t^{a}_{2}$, and $t^{1}\approx_{\overline{A^{y}_{l}},\overline{P^{k}_{l}}}t^{a}_{2}$, it follows iteratively over all respective clauses in $P_{f}$ that $t^{1}\approx_{\overline{P_{f}},\overline{E}}t^{a}_{2}$. Therefore, there exists a $t_{2}$ which contradicts the assumption that $\omega_{f}^{\prime},\omega_{c}^{\prime},t_{1}$ is a counterexample for the safety of $d$, thus also $\omega_{f},\omega_{c},t_{1}$ is no counterexample. Finally, this shows that $(P_{c,d}^{\prime},E)$ is correct w.r.t. $d$. ∎

Now, we have constructed a CFT $(P_{c,d}^{\prime},E)$, which is correct w.r.t. $c$ and $d$. We can show that $(P_{c,d}^{\prime},E)$ is a also correct w.r.t. the composition o $c$ and $d$.

Theorem 4.1.

Let $c$ and $d$ be components, $p_{1}\ldots p_{n}$ ports, which are input ports of $c$ and outputs ports of $d$, $A^{1}_{1}\ldots A^{1}_{m_{1}},\ldots A^{n}_{1}\ldots A^{n}_{m_{n}}$ events with $A^{i}_{j}$ being an event on port $p_{i}$, i.e. an input event of $c$ and an output event of $d$. Let further be $(P_{c},E)$ be a CFT of $c$ and $(P^{i}_{j},A^{i}_{j})$ the CFTs of $d$ for the output events $A^{i}_{j}$.

Then the strict CFT composition $(P_{c,d}^{\prime},E)$ (Definition 14) is correct w.r.t. to the composition of $c$ and $d$.

Proof.

From Lemmas 3 and 5 it follows that $(P_{c,d}^{\prime},E)$ is correct w.r.t. $c$ and w.r.t. $d$. From Theorem 1 in [1], it then directly follows that $(P_{c,d},E)$ is correct w.r.t. the composition of $c$ and $d$. ∎

It is left to show that correctness of the strictly composed CFT for the composition, implies that the composed CFT according to Definition 12 is correct w.r.t. the composition of $c$ and $d$. We prove Theorem 3.1.

Proof for Theorem 3.1.

When we compare the definition of strict CFT composition (Definition 14) and CFT composition (Definition 12), we see that the strict composition keeps the events, on which the components are composed in the formula, while they disappear in the definition of non-strict composition.

Note that the normal composition therefore considers messages over the respective ports irrelevant.

We consider messages over these ports as outputs, therefore is the equivalence relation over messages implied by strict composition more strict that the equivalence relation over messages implied by composition. Therefore every counterexample for $(P_{c,d},E)$ is also a counterexample for $(P_{c,d}^{\prime},E)$

Therefore it directly follows that $(P_{c,d},E)$ is correct w.r.t. the composition of $c$ and $d$. ∎