確率時間オートマトンの確率時間強模倣検証器の開発

確率時間オートマトンの確率時間強模倣検証器の開発

山根 智 小寺 広志 荒井 恒夫

2003年，我々は以下の判定問題を定義して，その決定可能性を示した：「ソフトリアルタイムシステムを表現・解析 する1つの有用な道具である確率時間オートマトンというモデル上において，時間強模倣関係と確率模倣関係の組 合せとして定義される確率時間強模倣関係が計算可能であるか否か」．但し，判定アルゴリズムは与えていない．そ こで，本論文では具体的な判定アルゴリズムを提案し，更に実装して評価する．リアルタイムシステムの検証は検証 コストが大きいので,以下のような効率的なアルゴリズムを考案した．アルゴリズムの基本的な考え方は，注意深く 選んだ初期集合から反例(確率時間強模倣関係を規定する条件を充たさない状態対)を段階的に取除き，残った集合 内に初期状態対が含まれるか否かを判定する，というものである．

In 2003, we have defined a strong probabilistic timed simulation relation of probabilistic timed automata, which is given by the combination of a strong timed simulation relation and a probabilistic simulation re- lation. Also, we have shown that a strong probabilistic timed simulation relation of probabilistic timed automata is decidable. But we didn’t give the algorithm. In this paper, we propose a concrete algorithm Mand implement the algorithm. As the verification cost of real-time systems is very high, we propose the following algorithm: In the algorithmM, counter examples such as pairs of states, which do not satisfy the conditions of a strong probabilistic timed simulation relation, are gradually removed from the initial set, and finally judge whether one probabilistic timed automaton simulates another or not.

1

 近年，コンピュータソフトウェアの巨大化，並列 化，分散化,一言で言えば複雑化，及び，社会環境の コンピュータシステムへの依存が強まっていく傾向に 伴い，ソフトウェアの信頼性の保証が強く要求されて おり,形式的検証の理論が大いに期待されている．検 証対象とするシステムをグラフやオートマトンなど の数学モデルで表現して，その上で状態空間を網羅的 に探索することでバグの取り残しがないように検証 するという方法は形式的検証法として重要な位置を Development of Verifier of Strong Probabilistic Timed

Simulation for Probabilistic Timed Automata.

Satoshi Yamane, Hiroshi Kodera, Tsuneo Arai,金沢 大学大学院自然科学研究科, Graduate School of Nat- ural Science and Technology, Kanazawa University.

コンピュータソフトウェア, Vol.25, No.3 (2008), pp.148–193.

[研究論文] 2006年3月9日受付.

しめている．形式的検証法は，テストなどの，人間の 直観と経験と推理力に頼った有限パターンの検査とは 異なり，バグの取り残しはないが，モデル化の問題と 網羅的な探索を行うが故の計算量の問題がある．

我々は確率時間オートマトンを用いて,以下のよう な通信プロトコルやプロセス間通信などにおける制 約や条件を仕様記述できる:

1. 送信開始から3単位時間未満なら待つが3単位 時間以上は待たないといった受信待ち時間の時間 制約

2. 送信データがロストする確率が0.5%，ロスト しない確率が99.5といった送信エラーの動作に 対する確率的条件

さらに,我々は確率時間時相論理PTCTL(Probabilistic Timed Computation Tree Logic) を 用 い て, qsend,E |=Adv z.[true∃U asend ∧ (z≤5)]_≥0.8 と いった性質を仕様記述できて,その性質が成り立つか 否かを自動的にモデル検証できる[7]．なお,この性質

は,スケジューラAdv により決められた動作におい て，初期状態から送信開始状態qsendまで5単位時間 内に確率0.8以上で到達可能であることを意味する．

この確率時間オートマトンは，ωオートマトン[2]を 拡張した時間オートマトン[2], [6]の更なる拡張とし て考案されていて，理論的バックボーンがある．

近年の複雑なコンピュータシステムの多くが並列 分散システムやリアルタイムシステムで構成されて いることから，これらのシステムが検証対象となる．

分散システムの記述には非決定性を用いることが有 効であることが知られている[11]．一方，リアルタイ ムシステムのオートマトンによるモデル化には，時間 オートマトンが標準的である．これらより，オートマ トン理論を使う限りにおいては，非決定性の時間オー トマトン,或いは非決定性の確率時間オートマトンで システムをモデル化しそれを検証するという流れが 自然である．一方で，非決定性の時間オートマトンは 補集合に対し閉じていない[2]. これに対し，模倣関 係を用いた検証は決定可能である．模倣関係と言語 包含関係は相関があり，模倣関係が成り立つならば言 語包含関係も成り立つ という性質がある．この意味 で，模倣関係は言語包含関係よりも優れた検証法であ ると言える．模倣関係と検証のつながりを直感的に 述べると，仕様 B^が実装 A^{の任意動作を真似るこ} とが出来るならば，B^にはA^{に対応する構造が全て} 含まれていて，B上で調べたい確率時間時相論理式 [7](例えば,ある確率以上で,ある時間以内に性質を満 たすといったソフトリアルタイム性)が成り立ってい れば，A上でもその論理式が成り立つ．

 以上述べたように，本研究は形式的検証の研究に含 まれ，確率時間オートマトンというモデル上での確率 時間強模倣関係を用いた検証に関係している．より具 体的には，本論文では次の2点を新規に実現した．

1. 確率時間強模倣関係が規定する条件を充たさな い状態対(反例)を段階的に構造化された手続き で検出する反例法を構成して，この反例法を基礎 として，確率時間強模倣検証問題[12]を解く確 率時間強模倣検証アルゴリズムを構成した．提案 する反例法では,局所的な情報,つまり,反例が削 除された部分的な状態対の集合だけで確率時間

強模倣関係が検証できるという意味で新規性が 高い．確率模倣の検証コストは高いので,局所的 な情報のみで判定できるという性質は極めて有 効である．

2. 確率時間強模倣検証アルゴリズムを実行する検 証器を実装し，ワイヤレスLANのプロトコルを事 例として検証実験を行い，実験結果に基づいて確 率時間強模倣検証アルゴリズムの評価を行った．

提案する反例法を基礎とする確率時間強模倣検証ア ルゴリズムは，初期状態対から少ない遷移回数で到 達可能な状態対の集合内で反例が多く見つかるほど，

計算に要するメモリ使用量と計算時間が共に小さく なる，という性質を有する．また,一般的にも,反例 法はバグが多く見つかる設計の初期段階では大変な 効力を発揮するアルゴリズムとしても機能する．な お,確率時間強模倣検証アルゴリズム及びその検証器 は現時点では存在しない.

 次に関連研究を紹介する．

関連研究の紹介

1. 1996年, S. Tasiran, R. Alurらにより，時間 オートマトン上での時間強模倣関係が定義され，

その決定可能性が示された[5]．

2. 1999年, M. Kwiatkowskaらにより，モデル 確 率時間オートマトンが提案され，そのモデル上で Model-Checkingアルゴリズムが提案された[7]． 3. 1999年, C. Baierらにより，確率オートマトン

上での確率模倣関係を解くアルゴリズムが提案 された[8]．

4. 2003年, S. Yamaneにより，確率時間オートマ トン上で確率時間強模倣関係が定義された．また その関係を計算するアルゴリズムの決定可能性 の証明も行われている[12]．但し，この論文では 具体的なアルゴリズムは与えられていない．

5. 2003年, R. Lanotteらにより，確率時間オート マトン上で弱双模倣関係が定義され，その関係 を計算するアルゴリズムが提案されている[13]． 但し，彼らは双模倣関係に特化したPartitionア ルゴリズムを採用していて，そのアルゴリズム は一方向性の模倣関係の計算には適用できない．

また，彼らの扱っているモデルは確率分布の非決 定性がないのに対し，本論文で扱うモデルは確率 分布の非決定性を有するため，本論文で扱うモデ ルの方が表現力が高い．

本研究が直接関連している研究は4. である．

研究の目的

 本論文では，第1に，論文[12] で述べられていな い確率時間強模倣関係の計算アルゴリズムを構成す ることを目的とし，第2に，そのアルゴリズムを実 装して評価することを目的とする．

本論文の構造

 先ず2章で，確率時間オートマトンと確率時間強 模倣関係，そして確率時間強模倣検証問題をそれぞ れ定義する．次に3章で，4章の議論で前提として用 いる定義や補題を述べる．そして, 4章で，確率リー ジョングラフベースの確率時間強模倣検証アルゴリ ズムに関して，アルゴリズムの原理とその具体的構 成とアルゴリズムの停止性を述べる．そして, 5章で, そのアルゴリズムを実装向けの等価なゾーンベース のアルゴリズムに変換する原理と共に具体的構成を 述べる．6章では,実装した検証器を用いワイヤレス LANプロトコルを事例として,検証手法の有効性と その特性を述べる．最後に, 7章で，まとめと今後の 課題を述べる．

基本的な記号

 ここで，2章以降で用いる記号の中で基本的なもの を幾つかまとめておく．記号^def= は左辺を右辺で定義 する，という意味で用いる(例えば，2^def= 1 + 1)．記 号 ⇐⇒^def はその左辺と右辺とが等価であると定義す る，という意味で用いる(例えば，a < b ⇐⇒^def a≤b かつa=b)．また，記号 ⇐⇒ はその左辺と右辺と がそれ以前に定義されていて，かつ，等価であるこ とを表す(例えば，1<2 ⇐⇒ −2<−1)．集合A の要素数を|A|^{で表す．空集合を}∅^で表す．AがB の部分集合である(a∈Aならばa∈Bである)こ とをA⊆B で表す．A ⊆B は，A=B の場合も 含む．A のべき集合(∅^を含む，A の部分集合の集 合)を2^A で表し，2^{A def}= {A|A ⊆A}と定義す る．自然数の集合を で表す(0∈ とする)．整数

の集合をで表す．実数の集合を で表す．0を含 む非負の実数の集合を_≥0 で表す．正の実数の集合 を>0 で表し，>0def

= _≥0\{0}と定義する．_≥0 の元をn個それぞれ独立に並べた列の集合をⁿ_≥0 で 表し，ⁿ_≥0 ^def= {(a₁, a₂,· · ·, an)|1≤i≤nに対し ai∈≥0}^{と定義する．}x∈ ^{の整数部分を}x^で 表し，x^def= max{n|n≤x, n∈ }^{と定義する．}

 以降では原則として，1つの記号は1つの意味での み用いる．

2

 本章では，確率時間オートマトンと確率時間強模倣 関係の定義を行う．そして，確率時間強模倣検証問題 を定義する．

2. 1 確率時間オートマトンの構文と意味の定義  以下に定義する確率時間オートマトン(Probabilis- tic Timed Automata ; PTA)というモデルは，時間 制約と確率的条件の両方を表現する．但し, 時間制 約は，時間を測定する変数 x₁, x₂ ∈ を用いて，1 つの変数又は, 2つの変数の差に対する制約条件を 単位とした論理積で表現されるものに限る．例えば，

x₁<3 ∧ x₁−x₂≤5を1つの時間制約とする．ま た,確率的条件は，状態から状態集合上の離散確率分 布への遷移によって表現されるものに限る．

 時間制約は次のように定式化される．

定義2.1 (ゾーン) X ={x₁, x₂,· · ·, xn}^を非負の 実数変数の有限集合とする．ゾーンは以下の論理式に よって定義される:

0≤i=j≤n(xi−xj≺i,jci,j)

ここで,x₀= 0,≺i,j∈ {<,≤},ci,j∈∪ {∞}.  ゾーン ζの集合をZ_Xと表記する．ここで，集合 Z_X は非負の実数変数の有限集合X ^{のみによって規} 定されることに注意しておく．次に,ゾーンの解釈の 仕方を定義する．

定義2.2 (ゾーンの解釈) ゾーンζ∈Z_X 内には常

に|X | 個の非負の実数変数が出現すると考える．そ して，[[·]] :Z_X →2^{Ê|X |≥0} を ゾーンの解釈とする．

例えば，ゾーンの解釈の例は以下である.

[[x₁−x₂≤c ∧ x₃−x₀< d]] = [[x₁−x₂≤c]]× [[x₃−0< d]] =

(a₁, a₂, a₃)∈^|{_≥0^x1,x2}|×^|{_≥0^x3}|

a₁−a₂< c ∧ a₃< d}

 確率的条件の表現のために離散確率分布を定義する．

定義2.3 (離散確率分布) U を空でない集合として，

U 上の離散確率分布の集合を次式で定義する：

Dist(U)^def= {µ |µ:U →[0,1]

ここで,

u∈Uµ(u) = 1.

ただし,µ(u)>0なるuがせいぜい可算である．}.  オートマトンは形式的な構造とその構造上での動 作の2つを規定すれば厳密に定義される．

 非決定性の有限オートマトンに対し 時間を測定す るクロック変数が附加され拡張されたモデルが時間 オートマトンであり，時間オートマトンに対して,離 散確率分布が附加され拡張されたモデルが確率時間 オートマトンである[7]．

定義2.4 (PTAの構文) PTA A は7つ 組A =

S_A, s_A,Σ_A,XA, inv_A, prob_A, τs^A

s∈S_A

で あ る ． ここで，

1. S_Aはロケーションの有限集合．

2. s_A∈S_Aは初期ロケーション．

3. Σ_A はアクションラベルの有限集合．

4. XA は非負実数値を取るクロック変数の有限 集合．

5. inv_A:S_A→Z_XA は各ロケーションに時間制 約(不変条件)を与える関数．

6. prob_A : S_A → 2^{ΣA×2XA×Dist(SA)} は ，各 ロ ケーションに対し，そのロケーションから外向き

に出る辺(σ, λ, µ)の有限集合を与える関数．た

だし,σ∈Σ_A,λ∈2^XA,µ∈Dist(S_A)である. 7.

τs^A

s∈S_A は，ロケーションsから外向きに出 ている各辺に対し時間制約(ガード条件)を与え る関数τ_s^A:prob_A(s)→Z_XA の有限集合．

 ある時刻における次の動作の範囲を規定する情報 を状態と言う．PTAにおける状態はロケーションと 各クロック変数の値の対で定義される．

定義2.5 (PTAの状態)集合states(A) ^def= _s∈S

A

{s,a |a∈[[inv_A(s)]]} ⊆S_A×^|X_≥0^{A| の元を}PTA A^{の状態と言う．}

定義2.6 (PTAの初期状態の時間制約の条件) 状態 q_A^def= s_A,(0,· · ·,0)を初期状態の時間制約の条件 と言い，任意のPTAA ^{の状態集合}states(A)は初 期状態の時間制約の条件を満たすものとする．ここ で，(0,· · ·,0)は，0が|XA|個続くものを省略した 表記であり，例えば|XA|= 5なら，(0,· · ·,0) は，

(0,0,0,0,0)の省略と考えなければならない．

 オートマトンの動作とは状態遷移の系列であり，1 回の状態遷移が定義されれば動作が定義される．

定義2.7 (PTAの意味) PTA A ^における1回の 状態遷移は，次の2通りの遷移集合の和集合の元で ある．

1. 時間遷移(Timed Transitions)

 状態s,aにて，あるδ∈≥0 (0)に対し，次の 条件が真であることを，s,a→ ^δ s,a+ (δ,· · ·, δ) と表し，状態s,a^{から，時間経過量}δの時間遷移 が可能と言う：

性質2.1:

a∈[[inv_A(s)]] ∧ a+ (δ,· · ·, δ)∈[[inv_A(s)]].

こ こ で ，(δ,· · ·, δ) は δ が |XA| 個 続 く も の を 省 略 し た 表 記 で あ り，例 え ば |XA| = 5 で ，a = (a₁, a₂, a₃, a₄, a₅) ∈ ^|X_≥0^A| ならば ，a+ (δ,· · ·, δ) は，(a₁+δ, a₂+δ, a₃+δ, a₄+δ, a₅+δ)の省略とす る．ところで，上の性質2.1が真ならば，[[inv_A(s)]]

はゾーンだから，次が成り立つ：

∀δ∈≥0 {

 δ≤δ ⇒ a+ (δ,· · ·, δ)∈[[inv_A(s)]] }. 2. 離散遷移(Discrete Transitions)

• ^{先ず，状態}q=s,a^にて，a∈[[τs(σ, λ, µ)]]を 充たす辺の集合の中から1つの辺e= (σ, λ, µ)∈

prob_A(s)が選択される．もし，a∈[[τs(e)]]を 充たす辺e が存在しない場合は，離散遷移は生 じない．

• 次に, |XA|=n として，a∈ ⁿ_≥0 とリセット の指定λ⊆ XA(={x₁,· · ·, xn}) に対し各成分 (a[λ:= 0])_i (1≤i≤n)が

(a[λ:= 0])_i=





0 (if xi∈λ), ai (otherwise) に よ り 定 ま る a[λ := 0] ∈ ⁿ_≥0 ^{と ，任 意 の} s∈S_Aに対して，

p^qe

s,a[λ:= 0]

=µ(s)

を 充 た す 状 態 集 合 上 の 離 散 確 率 分 布 p^qe ∈ Dist(states(A))が構成される．

• そして，確率的遷移により，p^q_e(s,a[λ:= 0])>

0を充たす遷移先の状態s,a[λ:= 0]^が選択さ れる．

以 上 の 過 程 を 経 て ，状 態 q = s,a ^{が 状 態}

s,a[λ:= 0] へと遷移することを次のように表し，

状態qから辺e= (σ, λ, µ)を通る離散遷移が可能と 言う(qはeを通れる，とも表現する)．

s,a^(σ,λ,µ−→^),pqe

s,a[λ:= 0]

これが成り立つのは次の条件が真となるときである ことを注意してほしい：

a∈

τ_s^A(σ, λ, µ)

∧ ∃s∈S_A s.t.

p^qe(s,a[λ:= 0])>0.

 上記の時間遷移と離散遷移の条件はそれぞれ，遷移 前の事前条件と遷移後の事後条件の両方を含んでい ることに注意されたい．

 PTAはNon-Zenoであると仮定する[3], [7]．Non- Zenoとは，有限時間内には有限回の遷移のみが生じ ることを意味しており，現実的なリアルタイムシステ ムの動作の1つの側面をモデルに反映させたもので ある．

2. 1. 1 意味的エラー

 任意の離散遷移s,a ^(σ,λ,µ−→^),pqe s,a[λ:= 0] ^に おいて，p^q_e が状態集合上の離散確率分布であるなら ば，p^qe(s,a[λ:= 0]) >0 を充たすs,a[λ:= 0]

は 状 態 集 合 の 元 で な け れ ば な ら な い ．そ し て ， s,a[λ:= 0] ∈ states(A) ならば，定義 2.5(PTA

図2.1 意味的エラーの例

の状態の定義) より，s,a[λ:= 0] ∈[[inv_A(s)]]で なければならない．そこで，全ての離散遷移の中で，

次の条件を充たすものは，意味的エラーと見なす：

「p^q_e(s,a[λ:= 0])>0かつ s,a[λ:= 0] ∈states(A)」.

但し，意味的エラーは意味上での制約であって，構 文上の制約ではない．図2.1 はPTAの構文に従っ てはいるが，遷移s₀,0.5^(σ,{x1},µ−→^),pse0,0.5 s₁,0.0 にて，0.0∈[[inv_A(s₁)]] = [[x₁ ≥1]]という意味的エ ラーを含んでいるため，PTAではない．

以降，意味的エラーが存在しない場合のみを扱う．

2. 2 確率時間強模倣関係の定義

 確率時間強模倣関係 [12]は時間強模倣関係[5] と 確率分布の模倣関係[4]の組合せとして与えられる．

ここで先ず，確率分布の模倣関係を定義しておく．

定義2.8 (確率分布の模倣関係) 2つのPTAA, B に 対 し て ，R ⊆ states(A) × states(B), p₁ ∈ Dist(states(A)),p₂∈Dist(states(B))が与えられ るとする．但し，集合{q1∈states(A)|p₁(q₁)>0}

及び{q₂∈states(B)|p₂(q₂)>0}^{はそれぞれ有限集} 合あるいは可算無限集合とする．離散確率分布p₁,p₂ が関係R上で模倣関係があるということをp₁Rp₂ で表し，次のように定義する：

p₁Rp₂

⇐⇒ ∃wdef :states(A)×states(B)→[0,1] s.t.

図2.2 確率分布の模倣関係の例



























i) ∀q₁∈states(A),

q₂∈states(B)w(q₁, q₂) =p₁(q₁).

ii) ∀q2∈states(B),

q₁∈states(A)w(q₁, q₂) =p₂(q₂).

iii) ∀(q₁, q₂)∈states(A)×states(B), If w(q₁, q₂)>0 then(q₁, q₂)∈R.

この関数wを重み関数と言う[1]．

以下に, 確率分布の模倣関係の例を説明する．図 2.2のPTA AとPTA Bにおいて,以下のような重 み関数wが定義できる．

w(s₁,a,s₁,a) = ¹₃ w(s₃,b,s₄,b) = ¹₂ w(s₃,b,s₁,a) = ¹₆

ただし,s₁,a^とs₃,b^はPTA Aの状態であり, s1,aとs4,bはPTA Bの状態である．

以下に,定義2.8の3つの条件をチェックする．

1. 定義2.8のi)は,以下のように成り立つ．

w(s₁,a,s₁,a) =1

3 =p₁(s₁,a), w(s3,b,s4,b) +w(s3,b,s1,a)

=1 2+1

6=2

3 =p₁(s₃,b).

2. 定義2.8のii)は,以下のように成り立つ．

w(s₁,a,s₁,a) +w(s₃,b,s₁,a) = 1 2

=p₂(s1,a), w(s3,b,s4,b) =1

2 =p₂(s4,b).

3. 定義2.8のiii)は,以下のように成り立つ. w(s₁,a,s₁,a) = 1

3>0 のとき

(s₁,a,s₁,a)∈R, w(s3,b,s4,b) = 1

2>0 のとき

(s3,b,s4,b)∈R, w(s3,b,s1,a) =1

6 >0 のとき

(s₃,b,s₁,a)∈R.

以上より,p₁Rp₂が成り立つ．p₁Rp₂が意味 するところを直感的に言えば, PTA Aでは,イベント 列abは確率 ¹₃ で発生し,イベント列acは確率 ²₃ で 発生する. これに対応して,上記で定義した重み関数 wを使うならば, PTA Bにおいても,イベント列ab は確率¹₃ で発生し,イベント列acは確率¹₂+¹₆ = ²₃ で発生する.以上が確率分布の模倣関係の直感的な説 明である．

 次に，記法を1つ定義しておく．

定義2.9 (辺の集合edge_A(s, σ)) PTAAにて，ロ ケーションs ∈S_A 上にある，アクションラベルが σ∈Σ_Aの辺の集合をedge_A(s, σ)で表し，次式で定 義する：

edge_A(s, σ)^def=

(σ, λ, µ)∈prob_A(s) σ=σ .  確率時間強模倣関係は次のように定義される．

定義2.10 (確率時間強模倣関係) A =

S_A, s_A,Σ_A,XA, inv_A, prob_A, τ_s^A

s∈S_A

, B =

S_B, s_B,Σ_B,XB, inv_B, prob_B, τs^B

s∈S_B

をそ れ ぞ れ PTA と し ，次 の 条 件 を 充 た す 二 項 関 係 R ⊆ states(A)×states(B) を 確 率 時 間 強 模 倣 関

係と言う．また，確率時間強模倣関係R の中で最大

の集合をR_[A×B] で表す．

全ての(s1,a,s2,b)∈Rに対して，次の2つ の条件が両方とも成り立つ：

1. 時間模倣条件: 任意のδ∈>0 に対して,

 s₁,a→ ^δ s₁,a+ (δ,· · ·, δ)^ならば,  s2,b→ s^δ 2,b+ (δ,· · ·, δ)

∧(s₁,a+ (δ,· · ·, δ),s₂,b+ (δ,· · ·, δ))∈R． 2. 確率模倣条件:

任意のe₁= (σ, λ₁, µ₁)∈prob_A(s₁)に対して, s₁,a^(σ,λ1,µ−→^1),pse11,as₁,a[λ₁ := 0] ^ならば, edge_B(s₂, σ)=∅

∧ ∃e2= (σ, λ₂, µ₂)∈edge_B(s₂, σ) s.t.

  {s2,b^(σ,λ2,µ−→^2),pse22,bs₂,b[λ₂:= 0]

 ∧ pe^s₁^1,aR pe^s₂^2,b }^．

 PTA間の模倣関係を，確率時間強模倣関係を用い て次のように定義する．

定義2.11 (PTA間の模倣関係)初期状態対(q_A, q_B)

がR_[A×B] に含まれているとき，かつそのときに限

りA ptBと表し(即ち，(q_A, q_B)∈R_[A×B] ⇐⇒^def A ptB^と定義し)，PTAA^はPTAB^{に模倣され} ると言う．

2. 3 確率時間強模倣検証問題の定義

 確率時間強模倣検証問題とは次のように定義され る判定問題である[12]．

定義2.12 (確率時間強模倣検証問題)

 入力: 2つのそれぞれNon-ZenoなPTAA,B.

 出力: A ptB^ならばyes /そうでなければno．  本論文ではこれ以降，確率時間強模倣検証アルゴリ ズムを具体的に構成する．

3 4

 本章では，4章の確率時間強模倣検証アルゴリズム の議論のための準備として，並列合成演算，クロック リージョン，そして,確率リージョングラフの各定義 および4章で必要とする性質と記法を述べる．

3. 1 並列合成演算

 経過時間に関する同期を取るために，4章で並列合

成演算 [5], [12]を利用する．並列合成演算を定義す

る前に，準備として確率分布に関する2つの定義を 行う．

定義3.1 (Dirac分布) PTAA^{のロケーションの} 集合S_A上の離散確率分布で，s₁∈S_Aとして，次 のように定義される µ^s_A¹ ∈Dist(S_A) をDirac分布 と言う：

µ^s_A¹(s₁)^def=





1 (if s₁=s₁), 0 (otherwise)

定義3.2 (確率分布の合成) 離 散 確 率 分 布 µ₁ ∈ Dist(S_A) と µ₂ ∈ Dist(S_B) とから次の離散確率 分布µ₁×µ₂ ∈Dist(S_A×S_B)が構成できる：

任意のロケーション対(s₁, s₂)∈S_A×S_Bに対して，

(µ₁×µ₂)(s₁, s₂)^def= µ₁(s₁)×µ₂(s₂)．  並列合成演算は次のように定義される．

定義3.3 (並列合成演算) P TAA=

S_A, s_A,Σ_A,XA, inv_A, prob_A,

τs^A

s∈S_A

, B=

S_B, s_B,Σ_B,XB, inv_B, prob_B,

τ_s^B

s∈S_B

から P T AA B=

S_AB, s_AB,Σ_AB,X_AB, inv_AB, prob_AB,

τ_s^AB

s∈S_AB

を構成する演算を並列合 成演算と言う．但し，

• S_AB^def= S_A×S_B．

• s_AB^def= (s_A, s_B)．

• Σ_AB^def= Σ_A∪Σ_B．

• XABdef

= XA XB (disjoint)．

• 全ての(s₁, s₂)∈S_ABに対して，

  inv_AB(s₁, s₂)^def= inv_A(s₁) ∧ inv_B(s₂)．

• 任意の(s₁, s₂)∈S_ABに対するprob_AB(s₁, s₂)

⊆Σ_AB×2^XAB×Dist S_AB

及びτ₍^AB_s

1,s₂) : prob_AB(s₁, s₂)→Z_XAB は以下のように構成 する：

– 同 期 辺 の 構 成； 任 意 の (σ₁, λ₁, µ₁) ∈ prob_A(s₁)に対し，(σ₂, λ₂, µ₂)∈prob_B(s₂) が存在して σ₁ = σ₂ を満たすならば，辺 (σ₁, λ₁ λ₂, µ₁ ×µ₂) を prob_AB(s₁, s₂) に 加 え ，τ₍^AB_s

1,s₂)(σ₁, λ₁ λ₂, µ₁ ×µ₂) ^def= τ_s^A₁(σ₁, λ₁, µ₁) ∧ τ_s^B₂(σ₂, λ₂, µ₂)と定める．

– Aの非同期辺の構成； 任意の(σ₁, λ₁, µ₁)∈ prob_A(s₁)に対し，edge_B(s₂, σ₁) =∅なら ば，辺(σ₁, λ₁, µ₁×µ^s_B²)をprob_AB(s₁, s₂) に 加 え ，τ₍^AB_s

1,s₂)(σ₁, λ₁, µ₁ × µ^s_B²) ^def= τ_s^A₁(σ₁, λ₁, µ₁)と定める．

– Bの非同期辺の構成； 任意の(σ₂, λ₂, µ₂)∈ prob_B(s₂) に対し，edge_A(s₁, σ₂) =∅^なら ば，辺(σ₂, λ₂, µ^s_A¹×µ₂)をprob_AB(s₁, s₂) に 加 え ，τ₍^AB_s

1,s₂)(σ₂, λ₂, µ^s_A¹ × µ₂) ^def= τs^B₂(σ₂, λ₂, µ₂)と定める．

 定義3.3におけるA Bの構成法より，次の性質 が成り立つ．

性質3.1 (A Bの性質)   ロ ケー ション (s₁, s₂)

∈S_AB と，アクションラベルσをそれぞれ1つず つ固定した時，ロケーション(s₁, s₂)におけるσ が ラベル付けされた,全ての外向きの辺は，

• σによる同期辺

• σによるAの非同期辺

• σによるBの非同期辺 の3種類の内のいずれかとなる．

 ここで，便宜上，2つの記法を導入する．

定義3.4 (辺の分類)  ロケーション (s₁, s₂)から 外向きに出ている辺のラベルの集合

σ∈Σ_AB | (σ, λ, µ)∈prob_AB(s₁, s₂) を label_AB(s₁, s₂) で表す．性質 3.1より，ロケー

ション(s₁, s₂)∈S_ABとアクションラベルσをそれ ぞれ決めると(σ∈label_AB(s₁, s₂) である場合，つ まり，σ がロケーション(s₁, s₂) から外向きに出て いるいずれかの辺のラベルである場合)，辺の種類が 1つだけ決まる．そこで，次の関数ekが定義できる (ekはedge kindの略)：

ek:S_AB×Σ_AB→ {syn, asyn_A, asyn_B, empty}. こ こ で ，syn は 同 期 辺, asyn_A は A の 非 同 期 辺, asyn_B は B の 非 同 期 辺, emptyは 辺 が 存 在 し な い こ と を そ れ ぞ れ 意 味 す る ．以 降 ，σ ∈ Σ_AB\label_AB(s₁, s₂) に対 す るek((s₁, s₂), σ) は 参照しない．

定義3.5 (2つのクロック変数値の結合) a= (a₁,

· · ·, a_|XA|)∈^|X_≥0^A|,b= (b₁,· · ·, b_|XB|)∈^|X_≥0^{B| と} して，

(a₁,· · ·, a_|XA|, b₁,· · ·, b_|XB|)∈^|X_≥0^{A XB|} をa◦bで表記する．

 次に，A B上における離散遷移が，元々のA^上 とB上ではどのような意味を持つかを考察する．

性質3.2 (A B 上の3種の離散遷移) A B 上 で の ，辺 e = (σ, λ₁ λ₂, µ₁ × µ₂) を 通 る 離 散 遷 移 (s₁, s₂),c ^{(σ,λ1 λ2,µ1×µ}−→^{2),p(se 1,s2),c} (s₁, s₂),c[(λ₁λ₂) := 0]^はA,B^上では，c=a◦b として次の意味を持つ：

1. ek((s₁, s₂), σ) =synの場合かつ，その場合に 限り；

辺e₁= (σ, λ₁, µ₁)∈prob_A(s₁)は次を充たし：

  s₁,a^{(σ,λ1,µ1),p}

s1,a e1

−→ s₁,a[λ₁:= 0]

かつ，辺e₂= (σ, λ₂, µ₂)∈edge_B(s₂, σ)は次を 充たす：

  s2,b^(σ,λ2,µ−→^2),pse22,bs₂,b[λ₂ := 0]． 2. ek((s₁, s₂), σ) =asyn_Aの場合かつ，その場合

に限り；

辺e₁= (σ, λ₁, µ₁)∈prob_A(s₁)は   s1,a^(σ,λ1,µ−→^1),pse11,as₁,a[λ₁:= 0]

を充たし，かつ，edge_B(s₂, σ) =∅^．

3. ek((s₁, s₂), σ) =asyn_B の場合かつ，その場合

に限り；

辺e₂= (σ, λ₂, µ₂)∈prob_B(s₂)は   s₂,b^{(σ,λ2,µ2),p}

s2,b e2

−→ s₂,b[λ₂:= 0]

を充たし，かつ，edge_A(s₁, σ) =∅．

 離散遷移に対する一方で，A B^{上での時間遷移} についても考察する．

性質3.3 (A B上の時間遷移)  状態集合states (A B) 上での時間遷移(s₁, s₂),c −→ ^δ (s₁, s₂),

c+ (δ,· · ·, δ)は，A,B上では同期した時間遷移を意 味する．即ち，c=a◦bとして，s1,a−→ s^δ 1,a+

(δ,· · ·, δ) ∧ s2,b−→ s^δ 2,b+ (δ,· · ·, δ)を意味 する．

 更に，任意の状態 q ∈ states(A B) からの任 意 の 時 間 遷 移 先 は states(A B) に 含 ま れ る た め，遷移元の状態が states(A B) 内にある限り，

states(A B)内には同期しない時間遷移先は存在し

ない．従って，q∈states(A B)からの同期しない 時間遷移先が存在するとすれば，states(A B)の外

S_AB×^|X_≥0^AB|

\states(A B)に存在する(この 考えは，補題4.1の証明で前提として用いる)．

3. 2 クロックリージョン

 4章にて，A ptBか否かを計算する手続きの有 限化のために クロックリージョン[2]を利用する．ま ず，クロックリージョン の定義を述べよう．

定義3.6 (リージョン等価関係) [6] 次のように定義 される^|X_≥0^A| 上の二項関係 ⊆^|X_≥0^A|×^|X_≥0^A| を，

リージョン等価関係と言う．max{ |c| ∈ | c∈ はPTAA上に出現する不変条件inv_Aとガード条件 の式τs^Aに出現する}をC_Aで表す．

 ab ⇐⇒^{def 次の条件}1.と2.が成り立つ：

1. 任意の i(1≤i≤ |XA|)に対し,次の (a), (b) どちらか一方が成り立つ．

(a)ai> C_Aならば，bi> C_A．

(b)ai≤C_A ならば，ai=bi ∧ (ai− ai  = 0 ⇐⇒ bi− bi= 0)．

2. 任意のi, j(1≤i≤ |XA|, 1≤j ≤ |XA|, i=

j) と,任意のc∈ {−CA,· · ·,−1,0,1,· · ·, C_A} と，任意の≺ ∈ {<,≤}に対し,ai−aj≺c ⇐⇒

bi−bj≺c．

 このリージョン等価関係^{は同値関係であり，実} 数を有限個の同値類に直和分割する[6]．リージョン 等価関係は同値関係であるため，次の3つの命題 が成り立つ：

1. 任意のa,b∈^|X_≥0^A|に対し，ab ⇐⇒ [a] = [b]．

2. 任 意 の a,b ∈ ^|X_≥0^{A| に 対 し ，}a b ⇐⇒

[a] ∩ [b] =∅^． 3. a∈^Ê|XA|_≥0 [a] =^|X_≥0^A|．

これらは広く知られている事実である．

定義3.7 (クロックリージョン) [2] リージョン等価 関係 ^{により定まる同値類}[a] = {a|aa} ⊆

|X_A|

≥0 を ク ロック リ ー ジョン と 言 う．便 宜 上 ， ク ロック リ ー ジョン の 全 体 集 合 を V(X_A,C_A) def

=

[a] a∈^|X_≥0^A|

で表す．これは商集合 ^|X_≥0^A|/ のことである．

 ここで，クロックリージョンの中でも特殊な性質を 持つものを区別しておく．

定義3.8 (時間発散的なクロックリージョン) 1 ≤ i ≤ |XA| ^{なる全ての} i に対し，ai > C_A を充た すクロックリージョン[a]∈ V_(XA,C_A)を時間発散的 なクロックリージョンと言う．

 ρを時間発散的なクロックリージョンとすると，ρ 内の任意点からいくら無限に時間を経過させても，同 じクロックリージョン内に留まることが出来る．

 次に，4章で用いるクロックリージョンの性質を幾 つか述べておく．

性質3.4 (時間安定性) [6]ρ∈ V(X_A,C_A)をクロック リージョンとする．このとき，次の性質が成り立つ．

任意のa,b∈ρと,任意のδ∈>0に対し,

∃δ∈>0 s.t.[a+ (δ,· · ·, δ)] = [b+ (δ,· · ·, δ)]．  この時間安定性は，補題4.9の証明で用いる．