1 The Cstat State Transition Model

Δ is a finite set of symbols:

Δ = {δ_{ij} | 3 ≤ i < 6 ∧ 0 ≤ j < 4} ∪
{δ_{ij} | 0 ≤ i < 4 ∧ 3 ≤ j < 6} ∪
{ϵ_{ij} | 0 ≤ i < 6 ∧ 0 ≤ j < 4} ∪
{ϵ_{ij} | 0 ≤ i < 4 ∧ 0 ≤ j < 6}

It’s convenient to introduce a finite state transition model on Δ. This model has alphabet

A^{Δ} = \{ \begin{matrix}c^{O}, c^{I}, c_{−}^{I}, q^{O}, q^{I}, i^{O}, i^{I}, \\ \overline{c}^{O}, \overline{c}^{I}, \overline{c}_{−}^{I}, \overline{q}^{O}, \overline{q}^{I}, \overline{i}^{O}, \overline{i}^{I} \} \end{matrix}

The transition function T^{Δ} is given in figure ??. In this diagram, all arcs are directed from left to right, or top to bottom.

The transition model describing the history of a channel is an “augmented” version of this finite state model. The state space Cstat is a subset of

Δ × Ports_{⊥} × Ports × Ports_{⊥} × Values_{⊥} ×
Ports_{⊥} × Ports × Ports_{⊥} × Values_{⊥},

namely

Cstat = {(d, P_{−}, P, P_{+}, u, Q_{−}, Q, Q_{+}, v) |
((d = δ_{ij} ∨ d = ϵ_{ij}) ⇒

( \begin{matrix}(i < 3 ⇒ P_{−} ∈ Ports)∧ \\ (4 ≤ i ⇒ P_{+} ∈ Ports)∧ \\ ((i = 0) ∨ (i = 2) ∨ (i = 4)) ⇒ u ∈ Values)∧ \\ (j < 3 ⇒ (Q_{−} ∈ Ports)∧ \\ (4 ≤ j ⇒ (Q_{+} ∈ Ports)∧ \\ ((j = 0) ∨ (j = 2) ∨ (j = 4)) ⇒ v ∈ Values) ))∧ \end{matrix}

(d = ϵ_{0j} ⇒ Q_{−} ∈ Ports) ∧
(d = ϵ_{i0} ⇒ P_{−} ∈ Ports)}.

The restrictions ensure that various fields don’t take the undefined value ⊥ in various states—necessary in the definition of the transition function.

The alphabet of a Cstat system associated with C ∈ Chans is

A_{C}^{Cstat} = \{ \begin{matrix}( , )^{O}.mes (E, ), \\ ( , )^{O}.mes (\overline{E}, ), \\ ( , )^{O}.ini (E, , ), & ( , )^{I}.ini (E, , ), \\ ( , )^{O}.ini (\overline{E}, , ), & ( , )^{I}.ini (\overline{E}, , ), \\ ( , )^{O}.chg (E, , ), & ( , )^{I}.chg (E, , ), \\ ( , )^{O}.chg (\overline{E}, , ), & ( , )^{I}.chg (\overline{E}, , ), \\ ( , )^{O}.quo (E, ), & ( , )^{I}.quo (E, ), \\ ( , )^{O}.quo (\overline{E}, ), & ( , )^{I}.quo (\overline{E}, ) \}. \end{matrix}

where E = out (C), \overline{E} = in (C).

[figure: q^{I}; i^{O}; i^{I}; c^{O}; c^{I}; c^{I}; q^{O}; ^{\overline{q}^{I}}; ^{\overline{i}^{O}}; ^{\overline{i}^{I}}; ^{\overline{c}^{O}}; ^{\overline{c}^{I}}; ^{\overline{c}^{I}}; ^{\overline{q}^{O}}; δ_{05}; δ_{15}; δ_{25}; δ_{35}; δ_{04}; δ_{14}; δ_{24}; δ_{34}; δ_{03}; δ_{13}; δ_{23}; δ_{33}; δ_{43}; δ_{53}; δ_{32}; δ_{42}; δ_{52}; δ_{31}; δ_{41}; δ_{51}; δ_{30}; δ_{40}; δ_{50}; ϵ_{00}; δ_{03}; δ_{30}]
[figure: ^{\overline{c}I −}; i^{O}; i^{I}; c^{O}; c^{I}; q^{O}; c_{−}^{I}; ^{\overline{i}^{O}}; ^{\overline{i}^{I}}; ^{\overline{c}^{O}}; ^{\overline{c}^{I}}; ^{\overline{q}^{O}}; ϵ_{05}; ϵ_{15}; ϵ_{25}; ϵ_{35}; ϵ_{04}; ϵ_{14}; ϵ_{24}; ϵ_{34}; ϵ_{03}; ϵ_{13}; ϵ_{23}; ϵ_{33}; ϵ_{43}; ϵ_{53}; ϵ_{02}; ϵ_{12}; ϵ_{22}; ϵ_{32}; ϵ_{42}; ϵ_{52}; ϵ_{01}; ϵ_{11}; ϵ_{21}; ϵ_{31}; ϵ_{41}; ϵ_{51}; ϵ_{00}; ϵ_{10}; ϵ_{20}; ϵ_{30}; ϵ_{40}; ϵ_{50}; ϵ_{00}; δ_{03}; δ_{30}]

Figure 1: The Δ state transition function The transition function is

T_{C}^{Cstat}(d, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v) =

{((Q, P)^{O}.mes (E, ) ↦ (d, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v)) |

(d = δ_{3i} ∨ d = ϵ_{3i}) ∧ 0 ≤ i < 5} ∪

\{((Q^{+}, P)^{O}.mes (\overline{E}, ) ↦ (d, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v)) |

d = δ_{35} ∨ d = ϵ_{35}} ∪

{((Q, P)^{O}.chg (E, P^{+}′, u′) ↦ (d′, P^{−}, P, P^{+}′, u′, Q^{−}, Q, Q^{+}, v)) |

(c^{O} ↦ d′) ∈ T^{Δ}(d) ∧ d′ ≠ ϵ_{00}} ∪

{((Q, P)^{O}.chg (E, P^{+}′, u′) ↦ (d′, P, P^{+}′, ⊥, v, Q, Q^{+}, ⊥, u′)) |

(c^{O} ↦ d′) ∈ T^{Δ}(d) ∧ d′ = ϵ_{00}} ∪

{((Q, P)^{I}.chg (E, P^{+}, u) ↦ (d′, P^{−}, P, P^{+}, ⊥, Q^{−}, Q, Q^{+}, v)) |

(c^{I} ↦ d′) ∈ T^{Δ}(d)} ∪

{((Q^{−}, P^{−})^{I}.chg (E, P, v) ↦ (d′, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, ⊥)) |

(c_{−}^{I} ↦ d′) ∈ T^{Δ}(d)} ∪

{((P, Q)^{O}.quo (E, u′) ↦ (d′, P, P^{+}, ⊥, u′, Q^{−}, Q, Q^{+}, v)) |

(q^{O} ↦ d′) ∈ T^{Δ}(d)} ∪

{((P^{−}, Q)^{I}.quo (E, u) ↦ (d′, P^{−}, P, P^{+}, ⊥, Q^{−}, Q, Q^{+}, v)) |

(q^{I} ↦ d′) ∈ T^{Δ}(d)} ∪

{((P, P^{−})^{O}.ini (E, Q, u′) ↦ (d′, P^{−}, P, P^{+}, u′, Q^{−}, Q, Q^{+}, v)) |

(i^{O} ↦ d′) ∈ T^{Δ}(d)} ∪

{((P, P^{−})^{I}.ini (E, Q, u) ↦ (d′, P^{−}, P, P^{+}, ⊥, Q^{−}, Q, Q^{+}, v)) |

(i^{I} ↦ d′) ∈ T^{Δ}(d)} ∪

\{((P, Q)^{O}.mes (\overline{E}, ) ↦ (d, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v)) |

(d = δ_{j3} ∨ d = ϵ_{j3}) ∧ 0 ≤ j < 5} ∪

\{((P^{+}, Q)^{O}.mes (\overline{E}, ) ↦ (d, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v)) |

d = δ_{53} ∨ d = ϵ_{53}} ∪

\{((P, Q)^{O}.chg (\overline{E}, Q^{+}′, v′) ↦ (d′, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}′, v′)) |

(\overline{c}^{O} ↦ d′) ∈ T^{Δ}(d) ∧ d′ ≠ ϵ_{00}\} ∪

\{((P, Q)^{O}.chg (\overline{E}, Q^{+}′, v′) ↦ (d′, P, P^{+}, ⊥, v′, Q, Q^{+}′, ⊥, u)) |

(\overline{c}^{O} ↦ d′) ∈ T^{Δ}(d) ∧ d′ = ϵ_{00}\} ∪

\{((P, Q)^{I}.chg (\overline{E}, Q^{+}, v) ↦ (d′, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, ⊥)) |

(\overline{c}^{I} ↦ d′) ∈ T^{Δ}(d)\} ∪

\{((P^{−}, Q^{−})^{I}.chg (\overline{E}, Q, u) ↦ (d′, P^{−}, P, P^{+}, ⊥, Q^{−}, Q, Q^{+}, v)) |

(\overline{c}_{−}^{I} ↦ d′) ∈ T^{Δ}(d)\} ∪

\{((Q, P)^{O}.quo (\overline{E}, v′) ↦ (d′, P^{−}, P, P^{+}, u, Q, Q^{+}, ⊥, v′)) |

(\overline{q}^{O} ↦ d′) ∈ T^{Δ}(d)\} ∪

\{((Q^{−}, P)^{I}.quo (\overline{E}, v) ↦ (d′, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, ⊥)) |

(\overline{q}^{I} ↦ d′) ∈ T^{Δ}(d)\} ∪

\{((Q, Q^{−})^{O}.ini (\overline{E}, P, v′) ↦ (d′, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v′)) | (\overline{i}^{O} ↦ d′) ∈ T^{Δ}(d)\} ∪

d  p^{s}(P^{−})  p^{s}(P)  p^{s}(P^{+})
ϵ_{0j} π_{2}(E, Q^{−}, P)  π_{0}
δ_{0j} π_{2}(E, Q, P)  π_{0}
η_{1j} π_{3}(E, Q, P)  π_{0}
η_{2j}  π_{0}
η_{3j}  π_{1}(E, Q)
η_{4j}  π_{2}(E, Q, P^{+})  π_{0}
η_{5j}  π_{2}(E, Q, P^{+})  π_{0}
ϵ_{05} π_{2}(E, Q^{−}, P) π′_{0}(Q^{+}, Q)
δ_{05} π_{2}(E, Q, P)  π′_{0}(Q^{+}, Q)
η_{15} π_{3}(E, Q, P)  π′_{0}(Q^{+}, Q)
η_{25}  π′_{0}(Q^{+}, Q)
η_{35}  π′_{1}(E, Q^{+}, Q)
d  p^{s}(Q^{−})  p^{s}(Q)  p^{s}(Q^{+})
ϵ_{i0} π_{2}(\overline{E}, P^{−}, Q)  π_{0}
δ_{i0} π_{2}(\overline{E}, P, Q)  π_{0}
η_{i1} π_{3}(\overline{E}, P, Q)  π_{0}
η_{i2}  π_{0}
η_{i3}  π_{1}(\overline{E}, P)
η_{i4}  π_{2}(\overline{E}, P, Q^{+})  π_{0}
η_{i5}  π_{2}(\overline{E}, P, Q^{+})  π_{0}
ϵ_{50} π_{2}(\overline{E}, P^{−}, Q) π′_{0}(P^{+}, P)
δ_{50} π_{2}(\overline{E}, P, Q)  π′_{0}(P^{+}, P)
η_{51} π_{3}(\overline{E}, P, Q)  π′_{0}(P^{+}, P)
η_{52}  π′_{0}(P^{+}, P)
η_{53}  π′_{1}(\overline{E}, P^{+}, P)

Figure 2: The partial function p^{s} for s = (d, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v)

\{((Q, Q^{−})^{I}.ini (\overline{E}, P, v) ↦ (d′, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, ⊥)) |

(\overline{i}^{I} ↦ d′) ∈ T^{Δ}(d)\}.

The elements of the bisimulation between the Cstat system and the Pstat, Mstat system are the partial functions p^{s}, m^{s}. these functions are defined in the tables of figures ?? and ??. Here, η means δ or ϵ. In figure ??, i and j run from 0 to 4; in figure ?? they run from 0 to 5.

d m^{s}(P^{−}, Q^{−}) m^{s}(P^{−}, Q) m^{s}(P, P^{−})  m^{s}(Q, P)
ϵ_{0j} ⟨chg (\overline{E}, Q, u)⟩
δ_{0j}  ⟨quo (E, u)⟩
η_{1j}  ⟨⟩
η_{2j}  ⟨ini (E, Q, u)⟩
η_{3j}  ⟨⟩
η_{4j}  ⟨chg (E, P^{+}, u)⟩

η_{5j}

d m^{s}(Q^{−}, P^{−}) m^{s}(Q^{−}, P) m^{s}(Q, Q^{−})  m^{s}(P, Q)
ϵ_{i0} ⟨chg (E, P, v)⟩
δ_{i0}  ⟨quo (\overline{E}, v)⟩
η_{i1}  ⟨⟩
η_{i2}  ⟨ini (\overline{E}, P, v)⟩
η_{i3}  ⟨⟩
η_{i4}  ⟨chg (\overline{E}, Q^{+}, v)⟩

η_{i5}

Figure 3: The partial function m^{s} for s = (d, P^{−}, P, P^{+}, u, Q^{−}, Q, Q^{+}, v)