Place Bisimulation and Liveness for Open Petri Nets

Petri nets are a kind of concurrent models for distributed and asynchronous systems. However they can only model closed systems, but not open ones. We extend Petri nets to model open systems. In Open Petri Nets, the way of interaction is achieved by composing nets. Some places with labels, called open or external, are considered as an interface with environment. Every external places are both input and output ones. Two such open Petri nets can be composed by joining the external places with the same label. In addition, we focus on the operational semantics of open nets and study observational properties, especially bisimulation properties. We define place bisimulations on nets with external places. It turns out that the largest bisimulation, i.e. the bisimilarity, is a congruence. A further result is that liveness is preserved by bisimilarity.

The work is supported by the National Nature Science Foundation of China(61472239, 61100053). The authors would like to thank the unknown reviewers for the comments.

Authors and Affiliations

1. BASICS, Department of Computer Science, Shanghai Jiao Tong University, Shanghai, China

   Xiaoju Dong & Yuxi Fu

2. PPS - CNRS and Université Paris Diderot, Paris, France

   Daniele Varacca

Corresponding author

Correspondence to Xiaoju Dong .

Editors and Affiliations

1. Carl von Ossietzky Universität, Oldenburg, Germany

   Martin Fränzle

2. University of New Mexico, Albuquerque, New Mexico, USA

   Deepak Kapur

3. Chinese Academy of Sciences, Beijing, China

   Naijun Zhan

Appendix

Theorem 3

The equivalence \(\approx \) is a congruence.

Proof

Suppose \(N_{1}\approx N_{2}\). Then \(N_{1}\,|\,N_{0} \approx N_{2}\,|\,N_{0}\) and \((x)N_{1}\approx (x)N_{2}\).

1. 1.

   Suppose \(\mathcal{R}=\{(N_{1}\,|\,N_{0}, N_{2}\,|\,N_{0})\mid N_{1}\approx N_{2}\}\). Then \(\mathcal R\) is a bisimulation. Let \(N_{10}\) and \(N_{20}\) denote \(N_{1}\,|\,N_{0}\) and \(N_{2}\,|\,N_{0}\) respectively. \(N_{10}=\langle P_{N_{10}},T_{N_{10}},F_{N_{10}},K_{N_{10}},W_{N_{10}},L_{N_{10}},M_{N_{10}}\rangle \), where

   • \(P_{N_{10}}=P_{N_{10}}^{i} \cup P_{N_{10}}^{e}\) where

     $$\begin{aligned} P_{N_{10}}^{i}= & {} P_{N_{1}}^{i}\cup P_{N_{0}}^{i} \end{aligned}$$

     (8)
     $$\begin{aligned} P_{N_{10}}^{e}= & {} P_{N_{1}\setminus N_{0}}^{e} \cup P_{N_{0}\setminus N_{1}}^{e} \cup P_{N_{1}\cap N_{0}} \end{aligned}$$

     (9)

   • \(T_{N_{10}}=T_{N_{1}}\cup T_{N_{0}}\);

   • \(F_{N_{10}}\) is the following relation

     $$\begin{array}{l} F_{N_{1}}\upharpoonright P_{N_{1}\setminus N_{0}} \cup F_{N_{0}}\upharpoonright P_{N_{0}\setminus N_{1}} \\ \cup \{\langle \langle s_{1},s_{0}\rangle ,t\rangle \mid \langle s_{1},t\rangle \in F_{N_{1}}, \langle s_{1},s_{0}\rangle \in P_{N_{1}\cap N_{0}}\} \\ \cup \{\langle t,\langle s_{1},s_{0}\rangle \rangle \mid \langle t,s_{1}\rangle \in F_{N_{1}}, \langle s_{1},s_{0}\rangle \in P_{N_{1}\cap N_{0}}\} \\ \cup \{\langle \langle s_{1},s_{0}\rangle ,t\rangle \mid \langle s_{0},t\rangle \in F_{N_{0}}, \langle s_{1},s_{0}\rangle \in P_{N_{1}\cap N_{0}}\} \\ \cup \{\langle t,\langle s_{1},s_{0}\rangle \rangle \mid \langle t,s_{0}\rangle \in F_{N_{0}}, \langle s_{1},s_{0}\rangle \in P_{N_{1}\cap N_{0}}\} \end{array}$$

   • \(W_{N_{10}}\) is the function defined as follows:

     $$W_{N_{10}}(\langle s,t\rangle )=\left\{ \begin{array}{ll} W_{N_{1}}(\langle s,t\rangle ), &{} \mathrm{if}\ s\in P_{N_{1}\setminus N_{0}} \\ W_{N_{0}}(\langle s,t\rangle ), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{1}} \\ W_{N_{1}}(\langle s_{1},t\rangle ) &{} \\ \ \ \ \ \ \ \ \ \ + \ \ \ \ \ \ \ \ \ , &{} \mathrm{if}\ s=\langle s_{1},s_{0}\rangle \\ W_{N_{0}}(\langle s_{0},t\rangle ) &{} \end{array}\right. $$

     and

     $$W_{N_{10}}(\langle t,s\rangle )=\left\{ \begin{array}{ll} W_{N_{1}}(\langle t,s\rangle ), &{} \mathrm{if}\ s\in P_{N_{1}\setminus N_{0}} \\ W_{N_{0}}(\langle t,s\rangle ), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{1}} \\ W_{N_{1}}(\langle t,s_{1}\rangle ) &{} \\ \ \ \ \ \ \ \ \ \ + \ \ \ \ \ \ \ \ \ , &{} \mathrm{if}\ s=\langle s_{1},s_{0}\rangle \\ W_{N_{0}}(\langle t,s_{0}\rangle ) &{} \end{array}\right. $$

   • \(L_{N_{10}}\) is the function defined as follows:

     $$L_{N_{10}}(s)=\left\{ \begin{array}{ll} L_{N_{1}}(s), &{} \mathrm{if}\ s\in P_{N_{1}\setminus N_{0}} \\ L_{N_{0}}(s), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{1}} \\ L_{N_{1}}(s_{1}), &{} \mathrm{if}\ s=\langle s_{1},s_{0}\rangle \end{array}\right. $$

   • \(M_{N_{10}}\) is the function defined as follows:

     $$M_{N_{10}}(s)=\left\{ \begin{array}{ll} M_{N_{1}}(s), &{} \mathrm{if}\ s\in P_{N_{1}\setminus N_{0}} \\ M_{N_{0}}(s), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{1}} \\ M_{N_{1}}(s_{1}){+}M_{N_{0}}(s_{0}), &{} \mathrm{if}\ s=\langle s_{1},s_{0}\rangle \end{array}\right. $$

\(N_{20}=\langle P_{N_{20}},T_{N_{20}},F_{N_{20}},K_{N_{20}},W_{N_{20}},L_{N_{20}},M_{N_{20}}\rangle \), where

• \(P_{N_{20}}=P_{N_{20}}^{i} \cup P_{N_{20}}^{e}\) where

  $$\begin{aligned} P_{N_{20}}^{i}= & {} P_{N_{2}}^{i}\cup P_{N_{0}}^{i} \end{aligned}$$

  (10)
  $$\begin{aligned} P_{N_{20}}^{e}= & {} P_{N_{2}\setminus N_{0}}^{e} \cup P_{N_{0}\setminus N_{2}}^{e} \cup P_{N_{2}\cap N_{0}} \end{aligned}$$

  (11)

• \(T_{N_{20}}=T_{N_{2}}\cup T_{N_{0}}\);

• \(F_{N_{20}}\) is the following relation

  $$\begin{array}{l} F_{N_{2}}\upharpoonright P_{N_{2}\setminus N_{0}} \cup F_{N_{0}}\upharpoonright P_{N_{0}\setminus N_{2}} \\ \cup \{\langle \langle s_{2},s_{0}\rangle ,t\rangle \mid \langle s_{2},t\rangle \in F_{N_{2}}, \langle s_{2},s_{0}\rangle \in P_{N_{2}\cap N_{0}}\} \\ \cup \{\langle t,\langle s_{2},s_{0}\rangle \rangle \mid \langle t,s_{2}\rangle \in F_{N_{2}}, \langle s_{2},s_{0}\rangle \in P_{N_{2}\cap N_{0}}\} \\ \cup \{\langle \langle s_{2},s_{0}\rangle ,t\rangle \mid \langle s_{0},t\rangle \in F_{N_{0}}, \langle s_{2},s_{0}\rangle \in P_{N_{2}\cap N_{0}}\} \\ \cup \{\langle t,\langle s_{2},s_{0}\rangle \rangle \mid \langle t,s_{0}\rangle \in F_{N_{0}}, \langle s_{2},s_{0}\rangle \in P_{N_{2}\cap N_{0}}\} \end{array}$$

• \(W_{N_{20}}\) is the function defined as follows:

  $$W_{N_{20}}(\langle s,t\rangle )=\left\{ \begin{array}{ll} W_{N_{2}}(\langle s,t\rangle ), &{} \mathrm{if}\ s\in P_{N_{2}\setminus N_{0}} \\ W_{N_{0}}(\langle s,t\rangle ), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{2}} \\ W_{N_{2}}(\langle s_{2},t\rangle ) &{} \\ \ \ \ \ \ \ \ \ \ + \ \ \ \ \ \ \ \ \ , &{} \mathrm{if}\ s=\langle s_{2},s_{0}\rangle \\ W_{N_{0}}(\langle s_{0},t\rangle ) &{} \end{array}\right. $$

  and

  $$W_{N_{20}}(\langle t,s\rangle )=\left\{ \begin{array}{ll} W_{N_{2}}(\langle t,s\rangle ), &{} \mathrm{if}\ s\in P_{N_{2}\setminus N_{0}} \\ W_{N_{0}}(\langle t,s\rangle ), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{2}} \\ W_{N_{2}}(\langle t,s_{2}\rangle ) &{} \\ \ \ \ \ \ \ \ \ \ + \ \ \ \ \ \ \ \ \ , &{} \mathrm{if}\ s=\langle s_{2},s_{0}\rangle \\ W_{N_{0}}(\langle t,s_{0}\rangle ) &{} \end{array}\right. $$

• \(L_{N_{20}}\) is the function defined as follows:

  $$L_{N_{20}}(s)=\left\{ \begin{array}{ll} L_{N_{2}}(s), &{} \mathrm{if}\ s\in P_{N_{2}\setminus N_{0}} \\ L_{N_{0}}(s), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{2}} \\ L_{N_{2}}(s_{2}), &{} \mathrm{if}\ s=\langle s_{2},s_{0}\rangle \end{array}\right. $$

• \(M_{N_{20}}\) is the function defined as follows:

  $$M_{N_{20}}(s)=\left\{ \begin{array}{ll} M_{N_{2}}(s), &{} \mathrm{if}\ s\in P_{N_{2}\setminus N_{0}} \\ M_{N_{0}}(s), &{} \mathrm{if}\ s\in P_{N_{0}\setminus N_{2}} \\ M_{N_{2}}(s_{2}){+}M_{N_{0}}(s_{0}), &{} \mathrm{if}\ s=\langle s_{2},s_{0}\rangle \end{array}\right. $$

Since \(N_{1} \approx N_{2}\), \(N_{1}\sigma \approx N_{2}\sigma \) and \(M_{N_{1}}^{e}\asymp M_{N_{2}}^{e}\). Assume the bijection \(\iota : P_{N_{1}}^{e}\rightarrow P_{N_{2}}^{e}\) satisfies the following conditions:

• \(M_{N_{1}}^{e}=M_{N_{2}}^{e}\circ \iota \);

• \(L_{N_{1}}^{e}\upharpoonright P_{N_{1}}^{e}=L_{N_{2}}^{e}\circ \iota \);

• \(K_{N_{1}}^{e}\upharpoonright P_{N_{1}}^{e}=K_{N_{2}}^{e}\circ \iota \).

(1) A bijection \(\iota ': P_{N_{10}}^{e}\rightarrow P_{N_{20}}^{e}\) can be defined as follows:

Then \(M_{N_{10}}^{e}\asymp M_{N_{20}}^{e}\). Therefore, \(\mathcal R\) is equipotent. If \(N_{10}{\mathcal R}N_{20}\), then \((N_{10}\sigma ){\mathcal R}(N_{20}\sigma )\) for \(N_{10}\sigma \equiv N_{1}\sigma \,|\,N_{0}\sigma '\) and \(N_{20}\sigma \equiv N_{2}\sigma \,|\,N_{0}\sigma '\), where

Hence, \({\mathcal R}\) is fully equipotent.

(2) Suppose \(N_{10}\longrightarrow N_{10}'\). Then there exists a marking \(M_{N_{10}}'\) of \(N_{10}\) such that \(M_{N_{10}}[t\rangle M_{N_{10}}'\) and \(M_{N_{10}}^{e} = M_{N_{10}}'^{e}\).

• If \(t\in T_{N_{1}}\), then there are two cases.

  • If there is a marking \(M_{N_{1}}'\) such that \(M_{N_{1}}[t\rangle M_{N_{1}}'\) and \(M_{N_{1}}^{e} = M_{N_{1}}'^{e}\), i.e. \(N_{1}\longrightarrow N_{1}'\), then \(N_{10}'\equiv N_{1}'\,|\, N_{0}\). Since \(N_{1}\approx N_{2}\), \(N_{2}\Longrightarrow N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Then \(N_{20} \Longrightarrow N_{2}'\,|\,N_{0}\) and \((N_{1}'\,|\,N_{0}){\mathcal R}(N_{2}'\,|\,N_{0})\). Otherwise,

  • \(O=(^{\bullet }t\cup t^{\bullet })\cap P_{N_{1}\cap N_{0}} \ne \emptyset \) and \(\forall s=\langle s_{1}, s_{0}\rangle \in O\), \(s\in ^{\bullet }t\cap t^{\bullet }\) and \(W(s,t)=W(t,s)\). We define

    $$\begin{aligned} \sigma (a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} M_{1}(s_{1})+M_{0}(s_{0}), &{}\\ \ \ \mathrm{if} a=L(s_{1}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{} \\ M_{1}(s_{1}), &{} \\ \ \ \mathrm{if}\ a=L(s_{1}), \mathrm{where}\ s_{1} \in P_{N_{1}}^{e}\setminus O &{} \\ \end{array}\right. \end{aligned}$$

    (14)
    $$\begin{aligned} \sigma _{0}(a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} 0, &{} \\ \ \ \mathrm{if} a=L(s_{0}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{} \\ M_{0}(s_{0}), &{} \\ \ \ \mathrm{if}\ a=L(s_{0}), \mathrm{where}\ s_{0} \in P_{N_{0}}^{e}\setminus O &{} \end{array}\right. \end{aligned}$$

    (15)

    Then \(N_{10}\equiv N_{1}\sigma \,|\,N_{0}\sigma _{0}\). Obviously, \(N_{1}\sigma \longrightarrow N_{1}'\) such that \(N_{10}'\equiv N_{1}'\,|\,N_{0}\sigma _{0}\). Since \(N_{1}\sigma \approx N_{2}\sigma \),\(N_{2}\sigma \Longrightarrow N_{2}'\) and \(N_{1}'\approx N_{2}'\). Then \(N_{20}\equiv N_{2}\sigma \,|\,N_{0}\sigma _{0}\Longrightarrow N_{2}'\,|\,N_{0}\sigma _{0}\) and \((N_{1}'\,|\,N_{0}\sigma _{0}){\mathcal R}(N_{2}'\,|\,N_{0}\sigma _{0})\).

• If \(t\in T_{N_{0}}\), then there are also two cases.

  • If there is a marking \(M_{N_{0}}'\) such that \(M_{N_{0}}[t\rangle M_{N_{0}}'\) and \(M_{N_{0}}^{e} = M_{N_{0}}'^{e}\), i.e. \(N_{0}\longrightarrow N_{0}'\), then \(N_{10}'\equiv N_{1}\,|\, N_{0}'\) and \(N_{20} \longrightarrow N_{2}\,|\,N_{0}'\). Since \(N_{1}\approx N_{2}\), \((N_{1}\,|\,N_{0}'){\mathcal R}(N_{2}\,|\,N_{0}')\). Otherwise,

  • \(O=(^{\bullet }t\cup t^{\bullet })\cap P_{N_{1}\cap N_{0}} \ne \emptyset \) and \(\forall s=\langle s_{1}, s_{0}\rangle \in O\), \(s\in ^{\bullet }t\cup t^{\bullet }\) and \(W(s,t)=W(t,s)\). It can be defined as

    $$\begin{aligned} \sigma (a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} M_{0}(s_{0})+M_{1}(s_{1}), &{} \\ \ \ \mathrm{if} a=L(s_{0}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{} \\ M_{0}(s_{0}), &{} \\ \ \ \mathrm{if}\ a=L(s_{0}), \mathrm{where}\ s_{0} \in P_{N_{0}}^{e}\setminus O &{} \end{array}\right. \end{aligned}$$

    (16)
    $$\begin{aligned} \sigma _{1}(a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} 0, &{} \\ \ \ \mathrm{if} a=L(s_{1}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{} \\ M_{1}(s_{1}), &{} \\ \ \ \mathrm{if}\ a=L(s_{1}), \mathrm{where}\ s_{1} \in P_{N_{1}}^{e}\setminus O &{} \end{array}\right. \end{aligned}$$

    (17)

    Then \(N_{10}\equiv N_{1}\sigma _{1}\,|\,N_{0}\sigma \). Obviously, \(N_{0}\sigma \longrightarrow N_{0}'\), \(N_{10}'\equiv N_{1}\sigma _{1}\,|\,N_{0}'\) and \(N_{20}\equiv N_{2}\sigma _{1}\,|\,N_{0}\sigma \longrightarrow N_{2}\sigma _{1}\,|\,N_{0}'\). Since \(N_{1}\approx N_{2}\), \((N_{1}\sigma _{1}\,|\,N_{0}') {\mathcal R} (N_{2}\sigma _{1}\,|\,N_{0}')\).

Suppose \(N_{10}\mathop {\longrightarrow }\limits ^{\tau } N_{10}'\). Then there exists a marking \(M_{N_{10}}'\) of \(N_{10}\) such that \(M_{N_{10}}[t\rangle M_{N_{10}}'\) and \(M_{N_{10}}^{e} \ne M_{N_{10}}'^{e}\).

• If \(t\in T_{N_{1}}\), then there are two cases.

  • If there is a marking \(M_{N_{1}}'\) such that \(M_{N_{1}}[t\rangle M_{N_{1}}'\) and \(M_{N_{1}}^{e} \ne M_{N_{1}}'^{e}\), i.e. \(N_{1}\mathop {\longrightarrow }\limits ^{\tau } N_{1}'\), then \(N_{10}'\equiv N_{1}'\,|\, N_{0}\). Since \(N_{1}\approx N_{2}\), \(N_{2}\mathop {\Longrightarrow }\limits ^{\tau } N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Then \(N_{20} \mathop {\Longrightarrow }\limits ^{\tau } N_{2}'\,|\,N_{0}\) and \((N_{1}'\,|\,N_{0}){\mathcal R}(N_{2}'\,|\,N_{0})\). Otherwise,

  • \(O=(^{\bullet }t\cup t^{\bullet })\cap P_{N_{1}\cap N_{0}} \ne \emptyset \). We define

    $$\begin{aligned} \sigma (a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} M_{1}(s_{1})+M_{0}(s_{0}), &{} \\ \ \ \mathrm{if} a=L(s_{1}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{}\\ M_{1}(s_{1}), &{} \\ \ \ \mathrm{if}\ a=L(s_{1}), \mathrm{where}\ s_{1} \in P_{N_{1}}^{e}\setminus O &{} \end{array}\right. \end{aligned}$$

    (18)
    $$\begin{aligned} \sigma _{0}(a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} 0, &{} \\ \ \ \mathrm{if} a=L(s_{0}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{} \\ M_{0}(s_{0}), &{} \\ \ \ \mathrm{if}\ a=L(s_{0}), \mathrm{where}\ s_{0} \in P_{N_{0}}^{e}\setminus O \\ \end{array}\right. \end{aligned}$$

    (19)

    Then \(N_{10}\equiv N_{1}\sigma \,|\,N_{0}\sigma _{0}\). Obviously, \(N_{1}\sigma \mathop {\longrightarrow }\limits ^{\tau } N_{1}'\) such that \(N_{10}'\equiv N_{1}'\,|\,N_{0}\sigma _{0}\). Since \(N_{1}\sigma \approx N_{2}\sigma \), \(N_{2}\sigma \mathop {\Longrightarrow }\limits ^{\tau } N_{2}'\) and \(N_{1}'\approx N_{2}'\). Then \(N_{20}\equiv N_{2}\sigma \,|\,N_{0}\sigma _{0}\mathop {\Longrightarrow }\limits ^{\tau } N_{2}'\,|\,N_{0}\sigma _{0}\) and \((N_{1}'\,|\,N_{0}\sigma _{0}){\mathcal R}(N_{2}'\,|\,N_{0}\sigma _{0})\).

• If \(t\in T_{N_{0}}\), then there are also two cases.

  • If there is a marking \(M_{N_{0}}'\) such that \(M_{N_{0}}[t\rangle M_{N_{0}}'\) and \(M_{N_{0}}^{e} \ne M_{N_{0}}'^{e}\), i.e. \(N_{0}\mathop {\longrightarrow }\limits ^{\tau } N_{0}'\), then \(N_{10}'\equiv N_{1}\,|\, N_{0}'\) and \(N_{20} \mathop {\longrightarrow }\limits ^{\tau }N_{2}\,|\,N_{0}'\). Since \(N_{1}\approx N_{2}\), \((N_{1}\,|\,N_{0}'){\mathcal R}(N_{2}\,|\,N_{0}')\). Otherwise,

  • We have \(O=(^{\bullet }t\cup t^{\bullet })\cap P_{N_{1}\cap N_{0}} \ne \emptyset \). We also define

    $$\begin{aligned} \sigma (a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} M_{0}(s_{0})+M_{1}(s_{1}), &{} \\ \ \ \mathrm{if} a=L(s_{0}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{} \\ M_{0}(s_{0}), &{} \\ \ \ \mathrm{if}\ a=L(s_{0}), \mathrm{where}\ s_{0} \in P_{N_{0}}^{e}\setminus O &{} \end{array}\right. \end{aligned}$$

    (20)
    $$\begin{aligned} \sigma _{1}(a)&\mathop {=}\limits ^\mathrm{def}&\left\{ \begin{array}{ll} 0, &{} \\ \ \ \mathrm{if} a=L(s_{1}), \mathrm{where}\ s=\langle s_{1}, s_{0}\rangle \in O &{} \\ M_{1}(s_{1}), &{} \\ \ \ \mathrm{if}\ a=L(s_{1}), \mathrm{where}\ s_{1} \in P_{N_{1}}^{e}\setminus O &{} \end{array}\right. \end{aligned}$$

    (21)

    Then \(N_{10}\equiv N_{1}\sigma _{1}\,|\,N_{0}\sigma \). We get \(N_{0}\sigma \mathop {\longrightarrow }\limits ^{\tau } N_{0}'\), \(N_{10}'\equiv N_{1}\sigma _{1}\,|\,N_{0}'\) and \(N_{20}\equiv N_{2}\sigma _{1}\,|\,N_{0}\sigma \mathop {\longrightarrow }\limits ^{\tau } N_{2}\sigma _{1}\,|\,N_{0}'\). Since \(N_{1}\approx N_{2}\), \((N_{1}\sigma _{1}\,|\,N_{0}') {\mathcal R} (N_{2}\sigma _{1}\,|\,N_{0}')\).

1. 2.

   Suppose \(\mathcal{R}=\{((x)N_{1}, (x)N_{2})\mid N_{1}\approx N_{2}\}\). Then \(\mathcal R\) is a bisimulation.

   • Suppose \((x)N_{1}\longrightarrow N_{1\setminus x}'\) and \(M_{1\setminus x}\) is the initial marking of \((x)N_{1}\). Then there is a marking \(M_{1\setminus x}'\) of \((x)N_{1}\) such that \(M_{1\setminus x}[t\rangle M_{1\setminus x}'\) for some t and \(M_{1\setminus x}^{e}=M_{1\setminus x}'^{e}\).

     • If \(\forall s\in P_{N_{1}}^{e}\).\(x\ne L(s)\), then \((x)N_{1}\equiv N_{1}\) and \((x)N_{2}\equiv N_{2}\). Then \(N_{1} \longrightarrow N_{1}'\) and \(N_{1\setminus x}'\equiv N_{1}'\equiv (x)N_{1}'\). Since \(N_{1}\approx N_{2}\), \(N_{2}\Longrightarrow N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Hence \((x)N_{2}\equiv N_{2}\Longrightarrow N_{2}'\equiv (x)N_{2}'\) and \((x)N_{1}'{\mathcal R} (x)N_{2}'\).

     • If \(\exists s\in P_{N_{1}}^{e}\).\(x = L(s)\), then there are two cases:

       • \(*\) If \(\forall s \in ^{\bullet }t \cup t^{\bullet }. x\ne L(s)\), then \(N_{1}\longrightarrow N_{1}'\) and \(N_{1\setminus x}'\equiv (x)N_{1}'\). Since \(N_{1}\approx N_{2}\), \(N_{2}\Longrightarrow N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Hence \((x)N_{2}\Longrightarrow (x)N_{2}'\) and \((x)N_{1}'{\mathcal R} (x)N_{2}'\).

       • \(*\) If \(\exists s \in ^{\bullet }t\, \cup \, t^{\bullet }. x = L(s)\), then \(O=(^{\bullet }t \cup t^{\bullet })\, \cap \, P_{N_{1}}^{e} \ne \emptyset \). We can conclude that \(\forall s\in O \wedge L(s)\ne x. W(s,t)=W(t,s)\). If (\(\exists s \in ^{\bullet }t \cap t^{\bullet }. x = L(s))\) and \(W(s,t)=W(t,s)\), then \(N_{1}\longrightarrow N_{1}'\) and \(N_{1\setminus x}'\equiv (x)N_{1}'\). Since \(N_{1}\approx N_{2}\), \(N_{2}\Longrightarrow N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Hence \((x)N_{2}\Longrightarrow (x)N_{2}'\) and \((x)N_{1}'{\mathcal R} (x)N_{2}'\). Otherwise, if \((\exists s \in ^{\bullet }t \cap t^{\bullet }. x = L(s))\) and \(W(s,t)\ne W(t,s)\) or \((\forall s \in ^{\bullet }t \cap t^{\bullet }. x \ne L(s))\), then \(N_{1}\mathop {\longrightarrow }\limits ^{\tau }N_{1}'\) and \(N_{1\setminus x}'\equiv (x)N_{1}'\). It is obvious that the external place \(s_{1}\) of \(N_{1}\), which satisfies \(x=L(s_{1})\), is the unique external one with \(M_{1}(s_{1})\ne M_{1}'(s_{1})\). Since \(N_{1}\approx N_{2}\), \(N_{2}\Longrightarrow N_{21}\mathop {\longrightarrow }\limits ^{\tau }N_{22}{\Longrightarrow } N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Then there must be an external place \(s_{2}\) of \(N_{2}\), which satisfies \(x=L(s_{2})\), is the unique external one with \(M_{2}(s_{2})\ne M_{2}'(s_{2})\). The change is induced by the transition \(N_{21}\mathop {\longrightarrow }\limits ^{\tau }N_{22}\). Hence \((x)N_{2}\Longrightarrow (x)N_{21}\longrightarrow (x)N_{22}{\Longrightarrow } N_{2}'\equiv (x)N_{2}'\) and \((x)N_{1}'{\mathcal R} (x)N_{2}'\).

   • Suppose \((x)N_{1}\mathop {\longrightarrow }\limits ^{\tau } N_{1\setminus x}'\) and \(M_{1\setminus x}\) is the initial marking of \((x)N_{1}\). Then there is a marking \(M_{1\setminus x}'\) of \((x)N_{1}\) such that \(M_{1\setminus x}[t\rangle M_{1\setminus x}'\) for some t and \(M_{1\setminus x}^{e}\ne M_{1\setminus x}'^{e}\).

     • If \(\forall s\in P_{N_{1}}^{e}\).\(x\ne L(s)\), then \((x)N_{1}\equiv N_{1}\) and \((x)N_{2}\equiv N_{2}\). Then \(N_{1} \mathop {\longrightarrow }\limits ^{\tau } N_{1}'\) and \(N_{1\setminus x}'\equiv N_{1}'\equiv (x)N_{1}'\). Since \(N_{1}\approx N_{2}\), \(N_{2}\mathop {\Longrightarrow }\limits ^{\tau } N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Hence \((x)N_{2}\equiv N_{2}\mathop {\Longrightarrow }\limits ^{\tau } N_{2}'\equiv (x)N_{2}'\) and \((x)N_{1}'{\mathcal R} (x)N_{2}'\).

     • If \(\exists s\in P_{N_{1}}^{e}\).\(x = L(s)\), then there are two cases:

       • \(*\) If \(\forall s \in ^{\bullet }t \cup t^{\bullet }. x\ne L(s)\), then \(N_{1}\mathop {\longrightarrow }\limits ^{\tau } N_{1}'\) and \(N_{1\setminus x}'\equiv (x)N_{1}'\). Since \(N_{1}\approx N_{2}\), \(N_{2}\mathop {\Longrightarrow }\limits ^{\tau } N_{2}'\) such that \(N_{1}'\approx N_{2}'\). Hence \((x)N_{2}\mathop {\Longrightarrow }\limits ^{\tau } (x)N_{2}'\) and \((x)N_{1}'{\mathcal R} (x)N_{2}'\).

       • \(*\) If \(\exists s \in ^{\bullet }t\, \cup \, t^{\bullet }. x = L(s)\), then \(O=(^{\bullet }t\, \cup \, t^{\bullet })\, \cap \, P_{N_{1}}^{e} \ne \emptyset \). We can conclude that \(\exists s\in O \wedge L(s)\ne x. M_{1\setminus x}(s)\ne M_{1\setminus x}'(s)\). Hence \(N_{1}\mathop {\longrightarrow }\limits ^{\tau } N_{1}'\) and \(N_{1\setminus x}'\equiv (x)N_{1}'\). Since \(N_{1}\approx N_{2}\), \(N_{2}\Longrightarrow N_{21}\mathop {\longrightarrow }\limits ^{\tau }N_{22}{\Longrightarrow } N_{2}'\) and \(N_{1}'\approx N_{2}'\). Hence \((x)N_{2}\Longrightarrow (x)N_{21}\longrightarrow (x)N_{22}{\Longrightarrow } N_{2}'\equiv (x)N_{2}'\) and \((x)N_{1}'{\mathcal R} (x)N_{2}'\).

Reprints and permissions

© 2016 Springer International Publishing AG

Policies and ethics