この規格 プレビューページの目次
※一部、英文及び仏文を自動翻訳した日本語訳を使用しています。
B.2 弱いバイシミュレーション
B.2.1 定義
Sys = < S , A , T , s0 > をラベル付き遷移系とする。
s , s '∊ S , a1 ,.., a n ∊ Aとすると、次の表記法が定義されます。
| s -; a1 ,.., a n → s ' | s1 ,.., sn +1 ∊ Swiths = s1 , s ' = sn +1 , が存在する場合 |
| s i − a i → s i +1 for all 1 ≤ i ≤ n |
s , s '∊ S , a ∊ A , kを自然数とすると、次の表記が定義されます。
| s − k → s ' | iff s - a , a ,..., a → s ' ここでa , a ,..., aは、a のk回の出現のリストですa |
s , s ' ∊ S , a1 ,.., an ∊ A -{i} とすると、次の表記が定義されます。
| s = a1 ,.., a n ⇒ s ' | 自然数k0 ,.., k nが存在する場合 |
| s − i k 0 , a1 , i k 1 , s , a , i kn → n ' |
| ss | s = s ' または自然数nが存在する場合 |
| s − i n → s ' |
Sを状態の集合とします。関係R ⊆ S × Sは弱いバイシミュレーション関係です。
< S1 , S2 > ∊ Rの場合、すべてのt ∊ ( A -{i})*
- a)s1 = t ⇒ s1 ' のs1 '∊ Sが存在するということは、 s2 = t ⇒ s2 ' および < S1 ', S2 ' > ∊ Rs2 '∊ Sが存在することを意味します。
- b) there exists an s2 '∊ S with s2 = t ⇒ s2 ' は、 s1 ' ∊ S with s1 = t ⇒ s1 ' and < s1 ', s2 ' > ∊ Rが存在することを意味します。
Ｓｙｓ１およびＳｙｓ２を、それぞれ状態集合S１およびS２ 、ならびに初期状態s０１およびs０２を有する遷移システムとラベル付けする。 Sys1とSys2は、弱いバイシミュレーション関係R ⊆ S × Sが存在する場合、弱いバイシミュレーション等価です。
- a)s = S1 ∪ S2 ;
- b) < s01 , s02 > ∊ R
代数仕様と完全なプロセス環境のコンテキストにおける 2 つの閉じた LOTOS 動作表現は、7.5.4 で定義されている遷移システムの場合、弱いバイシミュレーションと同等です。弱いバイシミュレーションと同等です。
{ x1 ,.., xn} に含まれるすべての自由な値識別子を持つ 2 つの LOTOS 動作表現B1 , B2は、すべてのインスタンスが [ E1/ x1 ,..E n/x n ] B1および [ E1/ x1 ,.., E n/ x n ] B2は、弱いバイシミュレーションと等価です。ここで、 E1 ,..., E nは、 x1 ,. と同じ種類の閉値式です。 .、 x n 、それぞれ。
LOTOSコンテキスト C [] は、正式なプロセス パラメータ '[ ]' を持つ LOTOS 動作表現です。 C [] がコンテキストであり、 Bが動作式である場合、 C [ B ] は、 C [] 内のすべての「[]」オカレンスをBで置き換えた結果である動作式です。
2 つの LOTOS 動作表現B1 、 B2は、すべての LOTOS コンテキストC [], C [ B1 ] がC [ B 2 ] と等価な弱バイシミュレーションであることを条件に、弱バイシミュレーション合同です。
B.2.2 弱いバイシミュレーション合同の法則。
2 つの LOTOS 動作表現B1とB2が弱いバイシミュレーション合同である場合、これはB1 = B2と書かれます。ここで、' = ' の使用は、すべての LOTOS でB1がB2に置き換えられ、その逆も成り立つという事実によって正当化されます。意味を変えずに文脈を変える。動作表現の変数を含む形式B1 = B2の方程式が呼び出されます (弱いバイシミュレーション合同法則) 。弱いバイシミュレーション合同の最も有用な法則を以下に示します。これらの法則のいくつかの定式化は、関連する動作表現のいくつかのラベル セットに依存します。動作表現Bのラベル セットL ( B ) は、非表示演算子、または sum-domain- または par-domain-expression によってバインドされていない、 Bで発生するすべてのゲート識別子のセットとして定義されます。
- a)アクションプレフィックスgをしましょう..？ x: t .. 実験オファーを伴うアクション表示になりますか? x: tとし、 zをgに出現しない値識別子とします ... ? x: t ... [ E ]; B
- 1)g ... ? x: t ... [ E ]; B = g ... ? z: t ... [ z/ x ][ E ];[ z/ x ] B
- 2)g ... ? x: t ... ; B = 選択肢 x: t [] g ... ! x ... ; B
- 3)g ！ E1 ... ! E n [ E ]; B = [ E ] -> g ! E1 ... ! n ; B
b)選択
1)B[ ] B2 = B [ BB 2) B1 [] ( B2 [] B3 ) = ( B1 [] B2 ) [] B3 3) B [] 停止 = B 4) B [] B = B 5) [ E/ x ] B [] ( 選択 x: t [] B ) ≈ 選択 x: t [] B [ E ] ∊ Q ( t ) の場合 6) 選択 x: t [] B = B xがBで自由でない場合 7) 選択 x: t [] exit ( ... , x , ... ) = exit ( ... , 任意の t , ... ) c)並行して
法則がすべての並列演算子 '|' に当てはまる場合それらのいずれかを示すために使用されます（法律全体で同じインスタンスを使用）
1 ) B | B=B2BB1 2 ) B |( B2 | B) = (BBB|B3 3a) 出口 ( E1 , ... , E n ) | exit ( E1 ', ... , E n ') = 終了 ( E1 , ... , E n ) n = m場合 ([ E i ] = [ E i ' ]または 1) BにA を 隠す = BにA ' を 隠す A ' が A と同じ要素を含むリストの場合 2) BにAを 隠す = BにA ' を 隠す A ' = A ∩ L ( B ) の場合 3) hide A in B で hide A ' in B = hide A " in B ここでA " ≈ A ∪ A ' 4) A を Bに 隠す = B もしA ∩ L ( B ) =ϕ 5a) aA を 隠す ！ E1 ... ! n ; B = i ;( A を Bに 隠す ) ∊ Aa 5b) gでA を 非表示 にします。 B = g ;( A を Bに 隠す ) if name( g ) ∉A 6) A を B1に 隠す [] B2 = ( B1にA を 隠す ) [ ] ( B2にA を 隠す ) 7） hide A in ( B1 |[ A ' ]| B2 ) = ( hide A in B1 ) |[ A ' ]| ( A を B2に 隠す ) もしA ∩ A ' = ϕ 8日） A を 隠す ( B1 >>* B2 ) = ( B1でA を 隠す ) >>* ( B2でA を 隠す ) 9) ( B1 [ > B2 ) でA を 隠す = ( B1でA を 隠す ) [ > ( BzでA を 隠す ) 10) hide A in [ E ]-> B = [ E ]->( hide A in B ) g)ガーディング
1a) [ L = R ] -> B = B L = Rの場合 [ L = R ] -> B = ストップ そうでなければ 1b) [ be ] -> B = [ be = true ] -> B beが値式の場合 h)インスタンス化
b [ a1 , ... , a n ]( E1 , ... , E m ) = ([ E1/ x1 , ... , E m/ x m ] B b )[ a1/ g1 , ... , a n/ g n ]
if process b [ g1 , ... , g n ]( x1 , ... , x m ): f: = B b endproc は、プロセス識別子bに対応するプロセス抽象化の形式です。
j)ローカル定義
let x1: t1 = E1 , ... , x n: t n = E n in B = [ E1/ x1 , ... , E n/ x n ] B
k)再ラベル付け
[ S ] を (後置) 再ラベル付け演算子の任意のインスタンス [ a1/ g1 , ... , a n/ g n ] とする。 [ S ] で定義されるゲート識別子上の関数Sを関連付けます。
S ( g ¡ ) = a i (1 ≤ i ≤ n )
S ( g )= g if g ≠ g ¡ ( 1 ≤ i ≤ n )
Sは、ゲート識別子を含むリスト、セット、文字列などに拡張できます。この場合、 Sを適用すると、すべてのゲート識別子 g に対してすべての出現gがS ( g ) に置き換えられた同じカテゴリのオブジェクトが生成されます。 .
1) 停止 [ S ] = 停止 2) 終了 (...)[ S ] = 終了 (...) 3) ( a ; B )[ S ] = S ( a ); B [ S ] 4) ( B1 [ ] B2 )[ S ] = B1 [ S ] [ ] B2 [ S ] 5) ( B1 |[ A ]| B2 )[ S ] = B1 [ S ] |[ S ( A ) ]| B2 [ S ] もしSがL ( B1 )∪ L ( B2 )∪ A上で単射ならば 6) ( B1 >>* B2 )[ S ] = B1 [ S ] >>* B2 [ S ] 7) ( B1 [ > B2 )[ S ] = B1 [ S ] [ > B2 [ S ] 8) ( hide A ' in B )[ S ] = hide A in B [ S ] SがL ( B )∪ A ' について単射であり、 S ( A ') = A場合 9) B [ S ] = B SがL上の恒等式 ( S ) の場合 10)B [ S ] = B [ S ] すべてa ∊ L ( B ) についてS1 ( a ) = S2 ( a ) の場合 11) B [ S1 ] [ S2 ] = B [ S2S1 ] m)内部アクション
- 1)a i ; B = aB
- 2)B [] i ; B = i ; B
- 3)a ;( B1 [] i ; B2 ) [] a ; B = a ; (B1 [] i BB)
- 4) [ E/ x ] B []( 選択 x: t [] i ; B ) = 選択 x : t [] i; B if [ E ] ∊ Q ( t )
n)展開定理
便宜上、次の表記規則が導入されています。
B1 [] B2 [] ... [] B n []{ B1 , ... , B n} と書かれています 選択 x: t [] B []{[ E/ x ] B | と書かれています。 [ E ] ∊ Q{ t )} 選択 g in [ a1 , ... , a n ] [] B []{ B [ a i/ g ] | と書かれています。 a1 ∊{ a1 , ... , a n}) このようにして、一般的な形式 [] Sを導入しました。ここで、 Sは動作表現のセットです。 Sの要素は、適切に選択されたインデックス セットによって常に列挙できると想定されています。 Sの要素がすべてb iの形式である場合。 B iの場合、次の有用な法則が適用されます
B = []{ b i , B i | i ∊ l}、 C = []{ c j ; C j | j ∊ J}
1) B |[ A ]| C = []{ b i ;( B i ,|[ A ]| C ) |名前( b ¡ )∉ A , i ∊ l} [] []{ C j ,( B |[ A ]| C j ) |名前( c j )∉ A , j ∊ J ] [] []{ a ;( B i |[ A ]| C j ) | a = b ¡ = c j , name ( a )∊ A , i ∊ l , j ∊ J} すべてのb i ( i ∊ l )、 C j ( j ∊ J ) がg ! E1 ... ! n 2) B [ > C = C [] []{ b i ;( b i ,[> C )| il} 3) A を Bに隠す = []{ b1 ; B iにA を 隠す | name ( b i )∊ A , i ∊ l}
[] []{ i ; B iにA を 隠す | name ( b i )∊ A , i ∊ l}すべてのb i ( i ∊ l ) がg ! E... ! n 4) B [ S ] = []{ S ( b i ); i [ S ] | il}
B.2.3 弱いバイシミュレーションの等価性の法則
B.2.3.1 表記法
2 つの動作表現B1とB2が弱いバイシミュレーション等価である場合、これはB1 = B2で示されます。
B.2.3.2 一般法
B.2.3.3 ≈ の規則
- 1)C [ ] を次の形式の LOTOS コンテキストとする:
- a)g ;[ ]
- b) [ ]|[ A ]| B 、またはB |[ A ]|[ ]
- c) [ ]>>* B 、またはB >>*[ ]
- d) [ ] [ > B
- e) [ ] でA を 隠す
- f) [ E ]->[ ]
- g) [ ][ S ]
- h) let ... in [ ]
B1 ≈ B2ならばC [ B1 ] ≈ C [ B2 ]
2)B ≈ Cの場合a ; B = aすべてのアクション表示のC ' a '
3)B = Cの場合、 B ≈ C
B.2 Weak bisimulation
B.2.1 Definitions
Let Sys = <S,A,T,s0>be a labelled transition system.
Let s,s'∊S, a1,..,an ∊A,then the following notation is defined:
| s-;a1,..,an →s' | iff there exist s1,..,sn+1 ∊ Swiths =s1,s' =sn+1, and |
| si −ai →si +1 for all 1 ≤ i ≤ n |
Lets,s'∊ S, a ∊ A,k be a natural number then the following notation is defined:
| s−ak → s' | iff s-a,a,...,a → s' where a,a,...,a is a list of k occurrences of a |
Let s, s' ∊ S,a1 ,..,an ∊ A-{i}, then the following notation is defined:
| s = a1,..,an ⇒ s' | iff there exist natural numbers k0,..,kn with |
| s − i k0, a1, i k1,..., an, i kn → s' |
| s ε⇒ s' | iff either s = s'or there exists a natural number n with |
| s - i n → s' |
Let S be a set of states. A relation R ⊆ S × S is a weak bisimulation relation iff:
If < S1 ,S2 > ∊ R then for all t ∊ (A-{i})*
- a) there exists an s1'∊S with s1 =t ⇒ s1' implies there exists ans2'∊ S withs2 = t ⇒s2 'and < S1',S2' > ∊R;
- b) there exists an s2'∊S withs2 =t ⇒ s2'implies there exists an s1' ∊ S with s1 = t⇒ s1 ' and < s1',s2' > ∊ R ;
Let Sys1 and Sys2 be labelled transition systems, with state sets S1 and S2, and initial states s01 and s02, respectively. Sys1 and Sys2 are weak bisimulation equivalentiff there exists a weak bisimulation relation R ⊆ S ×S, with
- a)s = S1 ∪ S2;
- b) < s01,s02 > ∊ R
Two closed LOTOS behaviour expressions, in the context of an algebraic specification and a complete process environment, are weak bisimulation equivalent iff their transition systems as defined in 7.5.4. are weak bisimulation equivalent.
Two LOTOS behaviour expressions B1,B2 with all their free value-identifiers contained in{x1,..,xn} are weak bisimulation equivalent, iff all instances [E1/x1 ,..E n/x n ]B1 and [E1/x1 ,..,En/xn ]B2 are weak bisimulation equivalent, where E1,...,En are closed value expressions of the same sort as x1,..,xn , respectively.
A LOTOS context C [] is a LOTOS behaviour expression with a formal process parameter ' [ ] '. If C [ ] is a context and B is a behaviour expression thenC [ B ] is the behaviour expression that is the result of replacing all ' [ ] ' occurrences in C [ ] by B.
Two LOTOS behaviour expressions B1, B2 are weak bisimulation congruent iff for all LOTOS contextsC[], C [ B1 ] is weak bisimulation equivalent withC [ B2 ].
B.2.2 Laws for weak bisimulation congruence.
If two LOTOS behaviour expressions B1 and B2 are weak bisimulation congruent this is written B1 = B2, where the use of ' = ' is justified by the fact that B1 may be replaced by B2 and vice versa in all LOTOS contexts without changing the meaning. Equations of the form B1 =B2 involving variables for behaviour expressions are called (weak bisimulation congruence) laws. The most useful laws for weak bisimulation congruence are listed below. The formulation of some of these laws depends on the label sets of some of the involved behaviour expressions. The label set L(B) of a behaviour expression B is defined as the set of all gateidentifiers that occur in B that are not bound by a hiding-operator, or a sum-domain- or par-domainexpression.
- a)Action-prefixLet g..? x: t.. be an action-denotation with an experiment-offer ? x: t, and let z be a value-identifier that does not occur in g ... ? x: t ... [ E ]; B.
- 1)g ... ? x: t ... [ E ]; B = g ... ? z: t ... [ z/ x ][ E ];[ z/x ] B
- 2)g ... ? x: t ... ;B = choice x: t [] g ... ! x ... ; B
- 3)g ! E1 ... !En [ E ]; B = [ E ] -> g ! E1 ... ! En ; B
b)Choice
1) B1 [] B2 = B2 [] B1 2) B1 [] (B2 [] B3) = (B1 [] B2) [] B3 3) B [] Stop = B 4) B [] B = B 5) [ E/x ]B [] ( choice x:t [] B) ≈ choice x:t [] B if [ E ] ∊ Q(t) 6) choice x:t[]B = B if x is not free in B 7) choice x:t[] exit ( ... ,x, ... ) = exit ( ... , any t, ... ) c)Parallel
If a law holds for all of the parallel operators '|' is used to denote any of them (using the same instance throughout the law)
1) B1 | B2 = B2 | B1 2) B1 |(B2 | B3) = (B1 | B2)| B3 3a) exit (E1, ... ,En ) | exit (E1', ... ,En ') = exit (E1, ... ,En ) if n = m and ([ Ei ] = [ Ei ' ]or 1) hide A in B = hide A ' in B if A ' is a list containing the same elements as A 2) hide A in B = hide A ' in B if A' = A ∩ L(B) 3) hide A in hide A ' in B = hide A" in B where A" ≈ A ∪ A ' 4) hide A in B = B if A ∩ L(B) =ϕ 5a) hide A in a!E1 ... !En ;B = i ;( hide A in B) if a ∊ A 5b) hide A in g;B = g;( hide A in B) if name(g) ∉A 6) hide A in B1 [] B2 = ( hide A in B1) [ ] ( hide A in B2) 7) hide A in (B1 |[ A ' ]| B2) = ( hide A in B1) |[ A ' ]| ( hide A in B2) if A ∩ A ' = ϕ 8) hide A in (B1 >>* B2) = ( hide A in B1) >>* ( hide A in B2) 9) hide A in (B1 [ > B2) = ( hide A in B1) [ > ( hide A in Bz) 10) hide A in [E]-> B = [E]->( hide A in B) g)Guarding
1a) [L = R ]-> B = B if L = R [L = R]-> B = stop otherwise 1b) [ be ] -> B = [ be = true ]-> B if be is a value-expression h)Instantiation
b[ a1, ... ,an ](E1, ... ,Em ) = ([ E1/x1, ... ,Em/xm ]Bb )[ a1/g1, ... ,an/gn ]
if process b [ g1, ... ,gn ](x1, ... ,xm ):f: = Bb endproc is the format of the corresponding process abstraction for the process-identifier b.
j)Local definition
let x1:t1 = E1, ... ,xn:tn = En in B = [E1/x1, ... ,En/xn ]B
k)Relabelling
Let [ S ] be any instance [ a1/g1, ... ,an/gn ] of the (post-fix) relabelling operator. We associate with [ S ] the function S on gate-identifiers defined by
S(g¡ ) = ai (1 ≤ i ≤ n)
S (g)= g if g ≠ g¡ ( 1 ≤ i ≤ n)
S can be extended to lists, sets, strings etc. containing gate-identifiers, in which case the application of S yields an object of the same category in which all occurrencesg have been replaced by S(g) for all gate-identifiers g.
1) stop [ S ] = stop 2) exit (...)[ S ] = exit (...) 3) (a;B)[ S ] = S(a);B[ S ] 4) (B1 [ ] B2)[ S ] = B1[ S ] [ ] B2[ S ] 5) (B1 |[ A ]| B2)[ S ] = B1[ S ] |[ S(A) ]| B2[ S ] if S is injective on L(B1)∪L(B2)∪A 6) (B1 >>* B2)[ S ] = B1[ S ] >>* B2[ S ] 7) (B1 [ > B2)[ S ] = B1[ S ] [ > B2[ S ] 8) ( hide A ' in B)[ S ] = hide A in B [ S ] if S is injective on L(B)∪A', and S(A ') = A 9) B[ S ] = B if S is the identity on L(S) 10) B[ S1 ] = B[ S2 ] if S1(a) = S2(a) for all a ∊ L(B) 11) B[ S1 ][ S2 ] = B[ S2 · S1 ] m)Internal action
- 1)a; i ;B = a;B
- 2)B[] i ;B = i ;B
- 3)a;(B1 [] i ;B2) [] a;B2 = a;(B1 [] i ;B2)
- 4) [E/x ]B[]( choice x:t[] i ;B) = choice x :t[] i;B if [ E ] ∊ Q(t)
n)Expansion theorems
For the sake of convenience, the following notational convention is introduced:
B1 [] B2 [] ... [] Bn is written []{B1, ... ,Bn} choice x:t [] B is written []{[ E/x ]B | [ E ] ∊ Q{t)} choice g in [ a1, ... ,an ] [] B is written []{B [ai/g ] | a1 ∊{a1, ... ,an}) In this way we have introduced the general format []S where S is a set of behaviour expressions. It is assumed that the elements of S can always be enumerated by some suitably chosen index set. If the elements of S are all of the form bi ;Bi then the following useful laws apply
Let B = []{bi ,Bi | i ∊ l}, C = []{cj ;Cj |j ∊J}
1) B|[ A ]| C = []{bi ;(Bi ,|[ A ]|C) | name(b¡ )∉ A, i ∊ l} [] []{Cj ,(B|[ A ]|Cj ) | name(cj )∉ A, j ∊ J] [] []{a;(Bi |[ A ]|Cj ) | a = b¡ = cj , name(a)∊A, i ∊ l, j ∊ J} if all bi (i ∊l), Cj (j ∊ J) are of the form g!E1 ... !En 2) B[ > C = C [] []{bi ;(bi ,[>C)|i∊l} 3) hide A in B = []{b1; hide A in Bi | name(bi )∊A, i ∊ l}
[] []{ i ; hide A in Bi | name(bi )∊A, i∊l}if all bi (i∊l) are of the form g!E1 ... !En 4) B[ S ] = []{S(bi );Bi [ S ] | i ∊ l}
B.2.3 Laws for weak bisimulation equivalence
B.2.3.1 Notation
If two behaviour expression B1 and B2 are weak bisimulation equivalent this is denoted by B1 = B2.
B.2.3.2 General law
B.2.3.3 Rules for ≈
- 1) LetC [ ] be a LOTOS context of the following forms:
- a)g;[ ]
- b) [ ]|[A ]|B , or B|[A ]|[ ]
- c) [ ]>>* B, or B>>*[ ]
- d) [ ] [ > B
- e) hide A in [ ]
- f) [E]->[ ]
- g) [ ][S]
- h) let ... in [ ]
then if B1 ≈ B2 then C [ B1 ] ≈ C [B2 ]
2) if B ≈ C then a;B = a;C for all action-denotations 'a'
3) if B = C then B ≈ C