同期ネットワークモデル

定義:プロセス

空でない集合QQ,集合MMに対し,v=(Q,M,δ,μ,Q0)v=(Q,M,\delta,\mu,Q_0)

  • δ:Q×MεQ\delta:Q \times M_\varepsilon \to Q
  • μ:Q×NMε\mu:Q \times \N \to M_\varepsilon
  • Q0Q\varnothing \subsetneq Q_0 \subseteq Q

を満たすvvを,プロセスという。
MMvvメッセージの集合といい,M(v)M(v)と表す。
QQvv状態の集合といい,Q(v)Q(v)と表す。
δ\deltavv遷移関数といい,δ(v)\delta(v)と表す。
μ\muvvメッセージ生成関数といい,μ(v)\mu(v)と表す。
Q0Q_0vv開始状態の集合といい,Q0(v)Q_0(v)と表す。

定義:ネットワーク

プロセスの有限集合VVに対し,ハッシュ付き有向グラフG=(V,E)G=(V,E)

  • vVv \in Vに対し,Nin(v)\mathcal N_{in}(v)上の全順序<<e<ehash(e)<hash(e)e < e^\prime \Longleftrightarrow \hash(e) < \hash(e^\prime)と定義する

を満たすGGを,ネットワークという。
V,EV,EGGプロセスの集合チャンネルの集合という。
vVM(v)\bigcup_{v \in V} M(v)GGメッセージの集合といい,M(G)M(G)と表す。
vVQ(v)×eEM(G)ε\prod_{v \in V} Q(v) \times \prod_{e \in E} M(G)_\varepsilonGG状態の集合といい,Q(G)Q(G)と表す。
δ:Q(G)Q(G)\delta:Q(G) \to Q(G)func δ({qv}vV,{me}eE) returns ({qv}vV,{me}eE)for vV dofor eNout(v) domeμ(v)(qv,hash(e))doneqvqvfor eNin(v) do in orderif meM(v) thenqvδ(v)(qv,me)endifdonedoneendfunc\begin{aligned} &\text{func}\ \delta(\{q_v\}_{v \in V},\{m_e\}_{e \in E})\ \text{returns}\ (\{q^\prime_v\}_{v \in V},\{m^\prime_e\}_{e \in E}) \\ &\qquad \text{for}\ v \in V\ \text{do} \\ &\qquad \qquad \text{for}\ e \in \mathcal N_{out}(v)\ \text{do} \\ &\qquad \qquad \qquad m^\prime_e \leftarrow \mu(v)(q_v,\hash(e)) \\ &\qquad \qquad \text{done} \\ &\qquad \qquad q^\prime_v \leftarrow q_v \\ &\qquad \qquad \text{for}\ e \in \mathcal N_{in}(v)\ \text{do in order} \\ &\qquad \qquad \qquad \text{if}\ m_e \in M(v)\ \text{then} \\ &\qquad \qquad \qquad \qquad q^\prime_v \leftarrow \delta(v)(q^\prime_v,m_e) \\ &\qquad \qquad \qquad \text{endif} \\ &\qquad \qquad \text{done} \\ &\qquad \text{done} \\ &\text{endfunc} \end{aligned}という疑似コードで定義し,GG遷移関数といいδ(G)\delta(G)と表す。
vVQ0(v)×eE{ε}\prod_{v \in V} Q_0(v) \times \prod_{e \in E}\{\varepsilon\}GG開始状態の集合といい,Q0(G)Q_0(G)と表す。

定義:ネットワークの実行

ネットワークG=(V,E)G=(V,E)に対し,X=q0q1Q(G)NX = q_0q_1\ldots \in Q(G)^\Nで,

  • q0Q0(G)q_0 \in Q_0(G)
  • nN (n1), qn=δ(G)(qn1)\forall n \in \N\ (n \geq 1),\ q_n = \delta(G)(q_{n-1})

を満たすXXを,GG実行という。

定義:チャンネルが故障したネットワーク

ネットワークG=(V,E)G=(V,E)eEe \in Eに対し,eeの始点をv=(Q,M,δ,μ,Q0)v = (Q,M,\delta,\mu,Q_0)とする。v=(Q,M,δ,μ,Q0)v^\prime = (Q,M,\delta,\mu^\prime,Q_0)

  • μ:Q×NMε\mu^\prime:Q \times \N \to M_\varepsilonμ(q,i)={μ(q,i)(ihash(e))ε(i=hash(e))\mu^\prime(q,i) = \begin{cases} \mu(q,i) & (i \neq \hash(e)) \\ \varepsilon & (i = \hash(e)) \end{cases}と定義する

を満たすとする。vvvv^\primeで置換したGGを,ee故障したGGという。

定義:チャンネルがいくつかのラウンドで故障したネットワーク

ネットワークG=(V,E)G=(V,E)eEe \in ENNN \subseteq \Nに対し,eeの始点をv=(Q,M,δ,μ,Q0)v = (Q,M,\delta,\mu,Q_0)とする。v=(Q,M,δ,μ,Q0)v^\prime = (Q^\prime,M,\delta^\prime,\mu^\prime,Q_0^\prime)

  • Q=Q×NQ^\prime = Q \times \N
  • δ:Q×MεQ\delta^\prime:Q^\prime \times M_\varepsilon \to Q^\primeδ((q,n),m)=(δ(q,m),n+1)\delta^\prime((q,n),m) = (\delta(q,m),n+1)と定義する
  • μ:Q×NMε\mu^\prime:Q^\prime \times \N \to M_\varepsilonμ((q,n),i)={μ(q,i)(ihash(e)nN)ε(i=hash(e)nN)\mu^\prime((q,n),i) = \begin{cases} \mu(q,i) & (i \neq \hash(e) \lor n \notin N) \\ \varepsilon & (i = \hash(e) \land n \in N) \end{cases}と定義する
  • Q0=Q0×{0}Q_0^\prime = Q_0 \times \{0\}

を満たすとする。vvvv^\primeで置換したGGを,eeがラウンドNN故障したGGという。

定義:ネットワークの実行の識別不可能性

ネットワークG=(V,E),H=(W,F)G=(V,E),H=(W,F)UVW (G[U]=H[U]uU, {hash(e)eEG(VU,u)}={hash(f)fEH(WU,u)})U \subseteq V \cap W\ (G[U]=H[U] \land \forall u \in U,\ \{\hash(e) \mid e \in E_G(V \setminus U,u)\}=\{\hash(f) \mid f \in E_H(W \setminus U,u)\})GGの実行X=q0q1X=q_0q_1\dotsHHの実行Y=r0r1Y=r_0r_1\dotsk,lN (k<l)k,l \in \N_\infty\ (k < l)に対し,

  • qk=({sv}vV,{me}eE),rk=({tw}wW,{nf}fF)q_k = (\{s_v\}_{v \in V},\{m_e\}_{e \in E}),r_k = (\{t_w\}_{w \in W},\{n_f\}_{f \in F})とおくとuU, (su=tueNin,G(u),fNin,H(u) (hash(e)=hash(f)), me=nfme,nfM(u))\begin{aligned} \forall u \in U,\ ( & s_u=t_u \land \mathord{}\\ & \forall e \in \mathcal N_{in,G}(u), f \in \mathcal N_{in,H}(u)\ (\hash(e)=\hash(f)),\ m_e=n_f \lor m_e,n_f \notin M(u)) \end{aligned}
  • iN (k<i<l)i \in \N\ (k < i < l)に対し,qi=({sv}vV,{me}eE),ri=({tw}wW,{nf}fF)q_i = (\{s_v\}_{v \in V},\{m_e\}_{e \in E}),r_i = (\{t_w\}_{w \in W},\{n_f\}_{f \in F})とおくとuU, eEG(VU,u),fEH(WU,u) (hash(e)=hash(f)), me=nfme,nfM(u)\forall u \in U,\ \forall e \in E_G(V \setminus U, u), f \in E_H(W \setminus U, u)\ (\hash(e)=\hash(f)),\ m_e=n_f \lor m_e,n_f \notin M(u)

を満たすことを,X,YX,YはラウンドkkからllまででUU-識別不可能であるという。

命題:ネットワークの実行の識別不可能性の性質

ネットワークG=(V,E),H=(W,F)G=(V,E),H=(W,F)UVW (G[U]=H[U]uU, {hash(e)eEG(VU,u)}={hash(f)fEH(WU,u)})U \subseteq V \cap W\ (G[U]=H[U] \land \forall u \in U,\ \{\hash(e) \mid e \in E_G(V \setminus U,u)\}=\{\hash(f) \mid f \in E_H(W \setminus U,u)\})GGの実行X=q0q1X=q_0q_1\dotsHHの実行Y=r0r1Y=r_0r_1\dotsk,lN (k<l)k,l \in \N_\infty\ (k < l)に対し,X,YX,YがラウンドkkからllまででUU-識別不可能であるならば,

  • iN (kil)i \in \N\ (k \leq i \leq l)に対し,qi=({sv}vV,{me}eE),ri=({tw}wW,{nf}fF),qi+1=({sv}vV,{me}eE),ri+1=({tw}wW,{nf}fF)q_i = (\{s_v\}_{v \in V},\{m_e\}_{e \in E}),r_i = (\{t_w\}_{w \in W},\{n_f\}_{f \in F}),q_{i+1} = (\{s^\prime_v\}_{v \in V},\{m^\prime_e\}_{e \in E}),r_{i+1} = (\{t^\prime_w\}_{w \in W},\{n^\prime_f\}_{f \in F})とおくとuU, (su=tueNout,G(u),fNout,H(u) (hash(e)=hash(f)), me=nf\begin{aligned} \forall u \in U,\ ( & s_u=t_u \land \mathord{} \\ & \forall e \in \mathcal N_{out,G}(u), f \in \mathcal N_{out,H}(u)\ (\hash(e)=\hash(f)),\ m^\prime_e=n^\prime_f \end{aligned}

証明

  • G[U]=H[U]uU, {hash(e)eEG(VU,u)}={hash(f)fEH(WU,u)}G[U]=H[U] \land \forall u \in U,\ \{\hash(e) \mid e \in E_G(V \setminus U,u)\}=\{\hash(f) \mid f \in E_H(W \setminus U,u)\}より,uU, {hash(e)eNin,G(u)}={hash(f)fNin,H(u)}\forall u \in U,\ \{\hash(e) \mid e \in \mathcal N_{in,G}(u)\}=\{\hash(f) \mid f \in \mathcal N_{in,H}(u)\}
  • iNi \in \Nに対し,qi=({sv}vV,{me}eE),ri=({tw}wW,{nf}fF),qi+1=({sv}vV,{me}eE),ri+1=({tw}wW,{nf}fF)q_i = (\{s_v\}_{v \in V},\{m_e\}_{e \in E}),r_i = (\{t_w\}_{w \in W},\{n_f\}_{f \in F}),q_{i+1} = (\{s^\prime_v\}_{v \in V},\{m^\prime_e\}_{e \in E}),r_{i+1} = (\{t^\prime_w\}_{w \in W},\{n^\prime_f\}_{f \in F})とおくとuU, (su=tueNin,G(u),fNin,H(u) (hash(e)=hash(f)), me=nfme,nfM(u))\begin{aligned} \forall u \in U,\ ( & s_u=t_u \land \mathord{} \\ & \forall e \in \mathcal N_{in,G}(u), f \in \mathcal N_{in,H}(u)\ (\hash(e)=\hash(f)),\ m_e=n_f \lor m_e,n_f \notin M(u)) \end{aligned}ならばuU, (su=tueNout,G(u),fNout,H(u) (hash(e)=hash(f)), me=nf)\begin{aligned} \forall u \in U,\ ( & s^\prime_u=t^\prime_u \land \mathord{} \\ & \forall e \in \mathcal N_{out,G}(u), f \in \mathcal N_{out,H}(u)\ (\hash(e)=\hash(f)),\ m^\prime_e=n^\prime_f) \end{aligned}
  • iNi \in \Nに対し,qi=({sv}vV,{me}eE),ri=({tw}wW,{nf}fF)q_i = (\{s_v\}_{v \in V},\{m_e\}_{e \in E}),r_i = (\{t_w\}_{w \in W},\{n_f\}_{f \in F})とおくとuU, (eNout,G(u),fNout,H(u) (hash(e)=hash(f)), me=nfeEG(VU,u),fEH(WU,u) (hash(e)=hash(f)), me=nfme,nfM(u))\begin{aligned} \forall u \in U,\ ( & \forall e \in \mathcal N_{out,G}(u), f \in \mathcal N_{out,H}(u)\ (\hash(e)=\hash(f)),\ m_e=n_f \land \mathord{} \\ & \forall e \in E_G(V \setminus U, u), f \in E_H(W \setminus U, u)\ (\hash(e)=\hash(f)),\ m_e=n_f \lor m_e,n_f \notin M(u)) \end{aligned}ならばuU, eNin,G(u),fNin,H(u) (hash(e)=hash(f)), me=nfme,nfM(u)\forall u \in U,\ \forall e \in \mathcal N_{in,G}(u), f \in \mathcal N_{in,H}(u)\ (\hash(e)=\hash(f)),\ m_e=n_f \lor m_e,n_f \notin M(u)