Diagnosability analysis of patterns on bounded labeled prioritized Petri nets

Abstract

Checking the diagnosability of a discrete event system aims at determining whether a fault can always be identified with certainty after the observation of a bounded number of events. This paper investigates the problem of pattern diagnosability of systems modeled as bounded labeled prioritized Petri nets that extends the diagnosability problem on single fault events to more complex behaviors. An effective method to automatically analyze the diagnosability of a pattern is proposed. It relies on a specific Petri net product that turns the pattern diagnosability problem into a model-checking problem.

Appendix: Proofs

1.1 A.1 Proof of Lemma 1

Lemma 1

For any reachable marking $M \in R({\Theta }_{\Omega },M_{{\Theta }_{\Omega }0})$ of Θ _Ω , there exists a reachable marking M ₁ ∈ R(Θ,M _Θ0 ) and a reachable marking M ₂ ∈ R(Ω,M _Ω0 ) such that M=M ₁ ∪M ₂.

Proof

We respectively denote by P _Θ, T _Θ, P _Ω, T _Ω, $P_{{\Theta }_{\Omega }},T_{{\Theta }_{\Omega }}$ the set of places and transitions of Θ, Ω, Θ_Ω. M _Θ0, M _Ω0 and $M_{{\Theta }_{\Omega }0}$ are also their respective initial marking. We proceed by induction on the set of reachable markings of $R({\Theta }_{\Omega },M_{{\Theta }_{\Omega }0})$ starting from the initial marking $M_{{\Theta }_{\Omega }0}$. The property obviously holds for $M_{{\Theta }_{\Omega }0}$ by definition of the system-pattern product (Definition 10).

Now suppose the existence in $R({\Theta }_{\Omega },M_{{\Theta }_{\Omega }0})$ of a marking M ^′ such that the property holds: there exist a reachable marking $M^{\prime }_{1} \in R({\Theta },M_{\Theta 0})$ and a reachable marking $M^{\prime }_{2} \in R({\Omega },M_{\Omega 0})$ such that $M^{\prime } = M^{\prime }_{1} \cup M^{\prime }_{2}$. Consider a marking M that is reachable from M ^′: $\exists t \in T_{{\Theta }_{\Omega }}: M^{\prime }\overset {t}{\longrightarrow }M$, it follows that $M \in R({\Theta }_{\Omega },M_{{\Theta }_{\Omega }0})$ and $\text {pre}_{{\Theta }_{\Omega }}(t) \subseteq M^{\prime }$. Let K _Θ, K _Ω respectively denote the transition mask of Θ over Θ_Ω and the transition mask of Ω over Θ_Ω formally defined as follows: let ε denote here the empty sequence of transitions,

$$K_{\Theta}(t) = \left\{\begin{array}{lllll} t & \text{if } t \in T_{\Theta}\\ \varepsilon & \text{if } t \in T_{\Omega}\\ t_{1} & \text{if } t = t_{1}\|t_{2} \end{array}\right. K_{\Omega}(t) = \left\{\begin{array}{lllll} \varepsilon & \text{if } t \in T_{\Theta}\\ t & \text{if } t \in T_{\Omega}\\ t_{2} & \text{if } t = t_{1}\|t_{2} \end{array}\right. $$

The transition masks can be easily extended to any sequence of transitions of Θ_Ω, let s = t ₀…t _n be such a sequence, K _Θ(s) = K _Θ(t ₀).K _Θ(t ₁)…K _Θ(t _n ) (similar for K _Ω(s)). From Definition 10, we get:

$$\text{pre}_{{\Theta}_{\Omega}}(t) = \text{pre}_{\Theta}(K_{\Theta}(t)) \cup \text{pre}_{\Omega}(K_{\Omega}(t)),$$

with the following definition extension of pre: $\text {pre}_{{\Theta }_{\Omega }}(\varepsilon ) = \text {pre}_{\Theta }(\varepsilon ) = \text {pre}_{\Omega }(\varepsilon ) = \varnothing$. However any place of pre_Θ(K _Θ(t)) is in P _Θ and any place of pre_Ω(K _Ω(t)) is in P _Ω. As P _Θ and P _Ω are disjoint pre_Θ(K _Θ(t))⊆M1′ and pre_Ω(K _Ω(t))⊆M2′. From this, two cases hold.

• 1. Transition t = t ₁∥t ₂ is synchronized. This transition results from the synchronization of transition t ₁ in Θ and transition t ₂ in Ω therefore, as pre_Θ(K _Θ(t)) = pre_Θ(t ₁)⊆M1′, t ₁ is firable from $M^{\prime }_{1}$ in Θ and, as pre_Ω(K _Ω(t)) = pre_Ω(t ₂)⊆M2′, t ₂ is firable from $M^{\prime }_{2}$ in Ω. By Definition 10, $\text {post}_{{\Theta }_{\Omega }}(t) = \text {post}_{\Theta }(t_{1}) \cup \text {post}_{\Omega }(t_{2})$.

• 2. Transition t belongs to T _Θ, so t is firable from $M^{\prime }_{1}$ in Θ and $\text {post}_{{\Theta }_{\Omega }}(t) = \text {post}_{\Theta }(t)$.

Based on the extended definition of post: $\text {post}_{{\Theta }_{\Omega }}(\varepsilon ) = \text {post}_{\Theta }(\varepsilon ) = \text {post}_{\Omega }(\varepsilon ) = \varnothing$, the three previous cases can be synthesized as follows:

$$\text{post}_{{\Theta}_{\Omega}}(t) = \text{post}_{\Theta}(K_{\Theta}(t)) \cup</p><p class="noindent">\text{post}_{\Omega}(K_{\Omega}(t)). $$

We have supposed that $M^{\prime }\overset {t}{\longrightarrow }M$ so $M = M^{\prime } \setminus \text {pre}_{{\Theta }_{\Omega }}(t) \cup \text {post}_{{\Theta }_{\Omega }}(t)$ which leads to M = M ^′∖(pre_Θ(K _Θ(t))∪pre_Ω(K _Ω(t)))∪(post_Θ(K _Θ(t))∪post_Ω(K _Ω(t))) to finally obtain M = M ₁∪M ₂ with M ₁ = (M1′∖pre_Θ(K _Θ(t)))∪post_Θ(K _Θ(t)) and M ₂ = (M2′∖pre_Ω(K _Ω(t)))∪post_Ω(K _Ω(t)). □

1.2 A.2 Proof of Theorem 1

Theorem 1

Let Θ be the LLPPN of a system over the alphabet Σ and Ω be the LLPPN of a pattern:

$$\mathcal{L}({\Theta} \ltimes {\Omega}) = \{ \rho \in \mathcal{L}({\Theta}) : \rho \Supset {\Omega} \}. $$

Proof

By Definition 5, we have to prove that $\mathcal {L}({\Theta } \ltimes {\Omega }) \subseteq \{ \rho \in \mathcal {L}({\Theta }) : \exists \sigma \in \mathcal {L}({\Omega }): \rho \Supset \sigma \}$.

• 1. Let us prove first that $\mathcal {L}({\Theta } \ltimes {\Omega }) \subseteq \{ \rho \in \mathcal {L}({\Theta }) : \exists \sigma \in \mathcal {L}({\Omega }): \rho \Supset \sigma \}$ . The first step is to prove that any word of $\mathcal {L}({\Theta } \ltimes {\Omega })$ is indeed in $\mathcal {L}({\Theta })$. By Lemma 1, recalling the transition masks K _Θ and K _Ω defined in the proof of this lemma, we get: $\forall r \in {T_{{\Theta }_{\Omega }}}: M_{0} \to [r] M, \exists r_{1} \in {T_{\Theta }} = K_{\Theta }(r) : {M_{0}}_{1} \to [r_{1}] M_{1}, \exists r_{2} \in {T_{\Omega }} = K_{\Omega }(r) : {M_{0}}_{2} \to [r_{2}] M_{2} \land M = M_{1}\cup M_{2}.$ Moreover, by Definition 10, $\ell _{{\Theta }_{\Omega }}(r) = \ell _{\Theta }(K_{\Theta }(r))$. For any firable sequence of Θ_Ω, there exists a firable sequence in Θ with the same sequence of labels. As $\mathcal {L}({\Theta })$ is a prefix-closed language (Q _Θ = R(Θ, M _Θ0), see Definition 3) any sequence of labels resulting from a firable sequence of Θ is in $\mathcal {L}({\Theta })$, so $\mathcal {L}({\Theta } \ltimes {\Omega }) \subseteq \mathcal {L}({\Theta })$.

  Consider now such a firable sequence r:M ₀→[r]M of ${\Theta } \ltimes {\Omega }$ such that $\rho = \ell _{\Theta \ltimes {\Omega }}(r) \in \mathcal {L}({\Theta } \ltimes {\Omega })\subseteq \mathcal {L}({\Theta })$. It means that there exists M _{0 2}→[K _Ω(r)]M ₂ (M ₂ ∈ Q _Ω). Let σ = ℓ _Ω(K _Ω(r)) it follows that $\sigma \in \mathcal {L}({\Omega })$. We now prove that $\rho \Supset \sigma$. Let T _s denote the set of synchronized transitions of ${\Theta } \ltimes {\Omega }$ (see Definition 10). As $\rho \in \mathcal {L}({\Theta } \ltimes {\Omega }), \rho \not = \varepsilon$ and r contains at least one transition t _s of T _s . Sequence r can then be decomposed as r = r ^′ t _s r′′:∀t ∈ r ^′, t∉T _s . Therefore, ρ can be written as ℓ _Θ(K _Θ(r ^′))ℓ _Θ(K _Θ(t _s ))ℓ _Θ(K _Θ(r′′)) and σ can be written as ℓ _Ω(K _Ω(r ^′))ℓ _Ω(K _Ω(t _s ))ℓ _Ω(K _Ω(r′′)). As t _s is the first synchronized transition in r, ℓ _Ω(K _Ω(r ^′)) = ε. Moreover, ℓ _Ω(K _Ω(t _s )) = ℓ _Θ(K _Θ(t _s )), which leads to σ = ℓ _Θ(K _Θ(t _s ))ℓ _Ω(K _Ω(r′′)). Let $\rho ^{\prime \prime } = \ell _{\Theta \ltimes {\Omega }}(r^{\prime \prime })$ and σ′′ = ℓ _Ω(K _Ω(r′′)), it follows that $\rho \Supset \sigma$ iff $\rho ^{\prime \prime } \Supset \sigma ^{\prime \prime }$. Two cases hold:

  • (a) If r′′ does not contain some transitions of T _s , it means that K _Ω(r′′) is an empty sequence: ℓ _Ω(K _Ω(r′′)) = ε, so σ′′ = ε and, by Definition 6, $\rho ^{\prime \prime } \Supset \sigma ^{\prime \prime }$.

  • (b) If r′′ contains some transitions of T _s , the previous reasoning recursively applies on r′′ and its first synchronized transition (by replacing r by r′′, ρ by ρ′′, σ by σ′′) to finally lead to prove that $\rho _{end} \Supset \sigma _{end}$ with $\rho _{end} = \ell _{\Theta \ltimes {\Omega }}(r_{end})$ and σ _end = ℓ _Ω(K _Ω(r _end )) with r _end a sequence without any synchronized transition left. This is exactly the previous case a): $\rho _{end} \Supset \sigma _{end}$ so finally $\rho ^{\prime \prime } \Supset \sigma ^{\prime \prime }$.

• 2. Let us prove that $\mathcal {L}({\Theta } \ltimes {\Omega }) \supseteq \{ \rho \in \mathcal {L}({\Theta }) : \exists \sigma \in \mathcal {L}({\Omega }): \rho \Supset \sigma \}$ . ρ belongs to $\mathcal {L}({\Theta })$ so there exists a sequence of transitions r from Θ such that M _Θ0→[r]M _r ∧ℓ _Θ(r) = ρ. σ belongs to $\mathcal {L}({\Omega })$ so σ≠ε and there exists a sequence of transitions r ^′ from Ω such that $M_{\Omega 0} \to [r^{\prime }] M_{r^{\prime }} : \ell _{\Omega }(r^{\prime }) = \sigma$ and $M_{r^{\prime }}$ is a final marking of Ω. As $\rho \Supset \sigma$, there exists σ ₀ ∈ Σ such that σ = σ ₀ σ ^′ and ρ can be written as ρ = ρ ₀ σ ₀ ρ ₁, σ ₀∉ρ ₀ and $\rho _{1} \Supset \sigma ^{\prime }$. It implies firstly that r can be written as M _Θ0→[r ₀]M _r0→[t ₁]M _t1→[r ₁]M _r with ℓ _Θ(t ₁) = σ ₀ and secondly that r ^′ can be written as $M_{\Omega 0} \to [t_{2}] M_{t2} \to [r^{\prime }_{1}] M_{r^{\prime }}$ with ℓ _Ω(t ₂) = σ ₀. σ ₀ not being a label of a transition in r ₀, (M _Θ0∪M _Ω0)→[r ₀](M _r0∪M _Ω0) is a sequence of transitions of the reachable marking graph of ${\Theta } \ltimes {\Omega }$. By Definition 10, the transition t ₁ is in ${\Theta } \ltimes {\Omega }$ and there exists a transition t ₁∥t ₂. Both transitions are firable in the marking (M _r0∪M _Ω0) but t ₁∥t ₂≻t ₁ so only t ₁∥t ₂ can be fired: the reachable marking graph of ${\Theta } \ltimes {\Omega }$ thus contains a sequence $(M_{\Theta 0} \cup M_{\Omega 0} ) \to [r_{0}.t_{1}\|t_{2}] (M_{t_{1}} \cup M_{t_{2}})$ and $\rho _{0}\sigma _{0} = \ell _{\Theta \ltimes {\Omega }}(r_{0}.t_{1}\|t_{2})$ . Suppose now that σ = σ ₀…σ _k ∈ Σ^∗, as $\rho _{1} \Supset \sigma ^{\prime }$ , we can reapply k times the previous reasoning starting from $M_{t_{1}}$ in Θ and from $M_{t_{2}}$ in Ω and then show the existence of reachable markings $M_{\sigma _{1}},{\dots } M_{\sigma _{k}}$ so that we prove there exists a sequence of transitions $(M_{\Theta 0} \cup M_{\Omega 0} ) \to [s] M_{\sigma _{k}} = (M_{\sigma _{k}}^{\Theta } \cup M_{\sigma _{k}}^{\Omega })$ such that $\ell _{\Theta \ltimes {\Omega }}(s) = \rho _{k}\sigma _{k}$ in ${\Theta } \ltimes {\Omega }$, $M_{\sigma _{k}}^{\Theta }$ being a marking of Θ and $M_{\sigma _{k}}^{\Omega }$ being a marking of Ω. As $\rho \in \mathcal {L}({\Theta })$, there must finally exist a firable sequence $M_{\sigma _{k}}^{\Theta } \to [s^{\prime }] M_{r}$ in Θ such that ℓ _Θ(s.s ^′) = ℓ _Θ(r) = ρ. On the other side, as $\sigma \in \mathcal {L}({\Omega })$, it follows that $(M_{\sigma _{k}}^{\Theta } \cup M_{\sigma _{k}}^{\Omega }) \to [s^{\prime }] (M_{r}\cup M_{\sigma _{k}}^{\Omega })$ belongs to the reachable marking graph of ${\Theta } \ltimes {\Omega }$. Therefore, there exists a firable sequence of transitions $(M_{\Theta 0} \cup M_{\Omega 0}) \to [s^{\prime \prime }] (M_{r}\cup M_{r^{\prime }})$ in ${\Theta } \ltimes {\Omega }$ such that $\ell _{\Theta \ltimes {\Omega }}(s^{\prime \prime }) = \rho$ . Finally as M _r is a final marking of Θ and $M_{r^{\prime }}$ is a final marking of Ω, $(M_{r}\cup M_{r^{\prime }})$ is a final marking of ${\Theta } \ltimes {\Omega }$, hence the result: $\rho \in \mathcal {L}({\Theta } \ltimes {\Omega })$.

□

1.3 A.3 Proof of Corollary 1

Corollary 1

Let Θ be the LLPPN of a system over an alphabet Σ and Ω be the LLPPN of a pattern:

$$\mathcal{L}({\Theta} \ltimes \overline{\Omega}) = \{ \rho \in \mathcal{L}({\Theta}) : \forall \sigma \in \mathcal{L}({\Omega}): \rho \not \Supset \sigma \}. $$

Proof

Let $\rho \in \mathcal {L}({\Theta })$, so there exists in Θ a transition sequence $M_{\Theta 0} \overset {t_{1}}{\longrightarrow } {\dots } \overset {t_{n}}{\longrightarrow } M$ such that ℓ _Θ(t ₁…t _n ) = ρ. Then, by Definition 10, there exists in ${\Theta } \ltimes {\Omega }$ a transition sequence $M_{\Theta {\Omega }0} \overset {t^{\prime }_{1}}{\longrightarrow } {\dots } \overset {t^{\prime }_{m}}{\longrightarrow } M^{\prime }$ such that $\ell _{\Theta \ltimes {\Omega }}(t^{\prime }_{1}{\dots } t^{\prime }_{m}) = \rho$ . Let $M^{\prime }_{1} \cup M^{\prime }_{2} = M^{\prime }$ with $M^{\prime }_{1}$ in R(Θ, M _Θ0) and $M^{\prime }_{2}$ in R(Ω, M _Ω0) (Lemma 1), if $M^{\prime }_{2} \in Q_{\Omega }$ then $\rho \in \mathcal {L}({\Theta } \ltimes {\Omega })$ , otherwise $M^{\prime }_{2} \in \overline {Q_{\Omega }}$ and $\rho \in \mathcal {L}({\Theta } \ltimes \overline {\Omega })$. From this it follows that $\mathcal {L}({\Theta }) = \mathcal {L}({\Theta } \ltimes {\Omega }) \cup \mathcal {L}({\Theta } \ltimes \overline {\Omega })$. The result then follows from Theorem 1. □

1.4 A.4 Proof of Theorem 2

Theorem 2

$\mathcal {L}(N_{1}\|N_{2}) = \{\rho \in {({\Sigma }_{1} \cup {\Sigma }_{2})}: \mathcal {P}_{{\Sigma }_{1} \cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho ) \in \mathcal {L}(N_{1}) \land \mathcal {P}_{{\Sigma }_{1} \cup {\Sigma }_{2}\to {\Sigma }_{2}}(\rho ) \in \mathcal {L}(N_{2})\}$.

Proof

First, let us prove that $\mathcal {L}(N_{1}\|N_{2}) \subseteq \{ \rho \in {({\Sigma }_{1} \cup {\Sigma }_{2})}: \mathcal {P}_{{\Sigma }_{1} \cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho ) \in \mathcal {L}(N_{1}) \land \mathcal {P}_{{\Sigma }_{1} \cup {\Sigma }_{2}\to {\Sigma }_{2}}(\rho ) \in \mathcal {L}(N_{2})\}$. Let $\rho \in \mathcal {L}(N_{1} \| N_{2})$, so there exists in N ₁∥N ₂ a transition sequence $M_{0} \overset {r}{\longrightarrow } M$ with M ∈ Q and ℓ(r) = ρ. Recalling the definition of masks $K_{N_{1}}$ and $K_{N_{2}}$ (see the proof of Lemma 1).

$$K_{N_{1}}(t) = \left\{\begin{array}{lllll} t & \text{if } t \in T_{N_{1}}\\ \varepsilon & \text{if } t \in T_{N_{2}}\\ t_{1} & \text{if } t = t_{1}\|t_{2} \end{array}\right. K_{N_{2}}(t) = \left\{\begin{array}{lllll} t & \text{if } t \in T_{N_{2}}\\ \varepsilon & \text{if } t \in T_{N_{1}}\\ t_{2} & \text{if } t = t_{1}\|t_{2} \end{array}\right., $$

by construction of N ₁∥N ₂, the transition sequence r can be associated to a transition sequence $r_{1}: M_{01} \overset {r_{1}}{\longrightarrow } M_{1}$ of N ₁ and a transition sequence $r_{2}: M_{02} \overset {r_{2}}{\longrightarrow } N_{2}$ of N ₂ such that $r_{1} = K_{N_{1}}(r)$ and $r_{2} = K_{N_{2}}(r)$. Moreover, as M belongs to Q, M ₁ ∈ Q ₁ and M ₂ ∈ Q ₂, therefore $\ell _{1}(r_{1}) \in \mathcal {L}(N_{1})$ and $\ell _{2}(r_{2}) \in \mathcal {L}(N_{2})$. Now, remark that $\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho ) = \ell _{1}(r_{1})$ as any transition of N ₁∥N ₂ labeled with a label of Σ₁ comes from N ₁, therefore $\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho ) \in \mathcal {L}(N_{1})$ . Similarly $\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{2}}(\rho ) \in \mathcal {L}(N_{2})$.

Now we prove $\mathcal {L}(N_{1}\|N_{2}) \supseteq \{ \rho \in {({\Sigma }_{1} \cup {\Sigma }_{2})}: \mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho ) \in \mathcal {L}(N_{1}) \land \mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{2}}(\rho ) \in \mathcal {L}(N_{2})\}$. Let ρ defined as above, suppose that ρ contains a set of n, n ≥ 0 events from Σ₁ ∩ Σ₂ then ρ can be written as ρ = ρ ₀ σ ₁ ρ ₁…σ _n ρ _n with ∀i ∈ {1,…, n}, σ _i ∈ Σ₁ ∩ Σ₂ and ∀i ∈ {0,…, n}, ρ _i ∈ ((Σ₁∪Σ₂)∖(Σ₁ ∩ Σ₂))^∗. As $\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho ) \in \mathcal {L}(N_{1})$, $\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho _{0})\sigma _{1}\dots \sigma _{n}\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho _{n}) \in \mathcal {L}(N_{1})$. Then there must exist in N ₁ a sequence of transitions $M_{01} \overset {r_{1}}{\longrightarrow } M^{1}_{n+1} = M_{01} \overset {{r^{1}_{0}}}{\longrightarrow } {M^{1}_{1}} \overset {{t^{1}_{1}}}{\longrightarrow } M^{1'}_{1}{\dots } \overset {r^{1}_{n-1}}{\longrightarrow } {M^{1}_{n}} \overset {{t^{1}_{n}}}{\longrightarrow } M^{1'}_{n} \overset {{r^{1}_{n}}}{\longrightarrow } M^{1}_{n+1}$ with ${r^{1}_{j}} \in T_{1}^{\ast }, j\in \{ 0,\dots ,n\}, \ell _{1}({t^{1}_{i}}) = \sigma _{i}, i\in \{ 1,\dots ,n\}$ and $M^{1}_{n+1} \in Q_{1}$ such that $\ell _{1}(r_{1}) =\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{1}}(\rho )$. Similarly, there must exist in N ₂ a sequence of transitions $M_{02} \overset {r_{2}}{\longrightarrow } M^{2}_{n+1} = M_{02} \overset {{r^{2}_{0}}}{\longrightarrow } {M^{2}_{1}} \overset {{t^{2}_{1}}}{\longrightarrow } M^{2'}_{1}{\dots } \overset {r^{2}_{n-1}}{\longrightarrow } {M^{2}_{n}} \overset {{t^{2}_{n}}}{\longrightarrow } M^{2'}_{n} \overset {{r^{2}_{n}}}{\longrightarrow } M^{2}_{n+1}$ with ${r^{2}_{j}} \in T_{2}^{\ast }, j\in \{ 0,\dots ,n\}, \ell _{2}({t^{2}_{i}}) = \sigma _{i}, i\in \{ 0,\dots ,n\}$ and $M^{2}_{n+1} \in Q_{2}$ such that $\ell _{2}(r_{2}) =\mathcal {P}_{{\Sigma }_{1}\cup {\Sigma }_{2}\to {\Sigma }_{2}}(\rho )$. Now, let us prove by induction that for any k from 0 to n, $M^{1}_{k+1} \cup M^{2}_{k+1}$ is a reachable marking of N ₁||N ₂.

• Case k = 0. By construction M ₀₁∪M ₀₂ is a reachable marking of N ₁||N ₂. $M_{01} \overset {{r^{1}_{0}}}{\longrightarrow } {M^{1}_{1}}$ and $M_{02} \overset {{r^{2}_{0}}}{\longrightarrow } {M^{2}_{1}}$ do not share any common label and might even be empty (i.e. ${r^{1}_{0}}=\varepsilon$ and ${M^{1}_{1}} = M_{01}$ or ${r^{2}_{0}}=\varepsilon$ and ${M^{2}_{1}} = M_{02}$ ). If both are empty then $M_{01} \cup M_{02} = {M^{1}_{1}}\cup {M^{2}_{1}}$ so ${M^{1}_{1}}\cup {M^{2}_{1}}$ is reachable. If now at least one of the run is not empty, by construction of N ₁||N ₂ any sequence of transitions s of N ₁||N ₂ such that $K_{N_{1}}(s) = M_{01} \overset {{r^{1}_{0}}}{\longrightarrow } {M^{1}_{1}}$ and $K_{N_{2}}(s) = M_{02} \overset {{r^{2}_{0}}}{\longrightarrow } {M^{2}_{1}}$ is actually a run of N ₁||N ₂ from M ₀₁∪M ₀₂, ${M^{1}_{1}} \cup {M^{2}_{1}}$ is thus reachable.

• General case. Assume ${M^{1}_{k}} \cup {M^{2}_{k}}$ is a reachable marking of N ₁||N ₂ and consider the part of the runs ${M^{i}_{k}} \overset {{t^{i}_{k}}}{\longrightarrow } M^{i^{\prime }}_{k} \overset {{r^{i}_{k}}}{\longrightarrow } M^{i}_{k+1}, i\in \{1,2\}$ . ${t^{i}_{k}}$ is firable from ${M^{i}_{k}}$ in N _i for i ∈ {1,2}. By construction of N ₁||N ₂, there must exist a transition ${t^{1}_{k}}||{t^{2}_{k}}$ such that $\ell ({t^{1}_{k}}||{t^{2}_{k}}) = \sigma _{k}$ firable from ${M^{1}_{k}} \cup {M^{2}_{k}}$ and that leads to the marking $M^{1'}_{k} \cup M^{2'}_{k}$ that is thus reachable. Considering now the run parts $M^{i^{\prime }}_{k} \overset {{r^{i}_{k}}}{\longrightarrow } M^{i}_{k+1}, i\in \{1,2\}$ , as $M^{1'}_{k} \cup M^{2'}_{k}$ is reachable, this is similar reasoning as in the case k = 0: it follows that $M^{1}_{k+1} \cup M^{2}_{k+1}$ is also reachable in N ₁||N ₂.

Consequently, $M^{1}_{n+1} \cup M^{2}_{n+1}$ is a reachable marking of N ₁||N ₂. Finally, remark that $M^{1}_{n+1}\in Q_{1}$ and $M^{2}_{n+1}\in Q_{2}$ so $M^{1}_{n+1} \cup M^{2}_{n+1}\in Q$, therefore $\rho \in \mathcal {L}(N_{1}||N_{2})$. □

1.5 A.5 Proof of Theorem 3

Theorem 3

$\mathcal {L}({\Gamma }) = \{ \rho \in {\Sigma }_{\Gamma }^{\ast }, \exists \rho _{1}, \rho _{2} \in \mathcal {L}({\Theta }), \rho _{1} \Supset {\Omega } \land \rho _{2} \not \Supset {\Omega }, \mathcal {P}_{\Sigma \to {\Sigma }_{o}}(\rho _{1}) = \mathcal {P}_{\Sigma \to {\Sigma }_{o}}(\rho _{2}) \land \rho _{1}= \mathcal {P}_{{\Sigma }_{\Gamma }\to {\Sigma }}(\rho ) \land \rho _{2}= \mathcal {R}_{{\Sigma }^{\prime }\to {\Sigma }}(\mathcal {P}_{{{\Sigma }_{\Gamma }}\to {{\Sigma }^{\prime }}}({\rho }))\}$.

Proof

The synchronized product Γ ensures by Theorem 2 that $\mathcal {L}({\Gamma }) = \{ \rho \in {\Sigma }_{\Gamma }^{\ast },\mathcal {P}_{{\Sigma }_{\Gamma }\to {\Sigma }}(\rho ) \in \mathcal {L}({\Theta } \mathbin {\ltimes } {\Omega })\land \mathcal {P}_{{\Sigma }_{\Gamma }\to {\Sigma }^{\prime }}(\rho ) \in \mathcal {L}({\Theta }^{\prime } \mathbin {\ltimes } \overline {\Omega }^{\prime }) \}$. Theorem 1 states that $\mathcal {P}_{{\Sigma }_{\Gamma }\to {\Sigma }}(\rho ) \Supset {\Omega }$ and Corollary 1 states that $\mathcal {R}_{{\Sigma }^{\prime }\to {\Sigma }}(\mathcal {P}_{{\Sigma }_{\Gamma }\to {\Sigma }^{\prime }}(\rho )) \not \Supset {\Omega }$. Finally, as Σ ∩ Σ^′ = Σ _o , we get $\mathcal {P}_{\Sigma \to {\Sigma }_{o}}(\mathcal {P}_{{{\Sigma }_{\Gamma }}\to {\Sigma }}({\rho })) = \mathcal {P}_{{\Sigma }^{\prime }\to {\Sigma }_{o}}(\mathcal {P}_{{{\Sigma }_{\Gamma }}\to {{\Sigma }^{\prime }}}({\rho })) = \mathcal {P}_{{\Sigma }_{\Gamma }\to {\Sigma }_{o}}(\rho )$. □