数理解析研究所講究録
第 1649 巻 2009 年 39-46

39

確率時間ゲーム理論による組込みシステムのモデル化, 仕様記述及び検証
金沢大学自然科学研究科電子情報工学専攻

林

将志 (Masashi Hayashi)

山根智 (Satoshi Yamane)

Division of Electrical and Computer Engineering,
Kanazawa University Graduate School of Natural Science & Technology

1

まえがき

近年, マイクロプロセッサの 99 % 以上は組込みシステムに使われており, 制御システムから情報家電までの多岐に渡り, safety-critical な状況で使われることが多く, 大規模化しており [1], 組込みシステム

一方, A.Pnueli らの時間ゲームにおいて, 到達
可能ゲームを効率的に検証するアルゴリズムがK.G.Larsen. らによって提案されている [12].
本論文では, 我々は ワイヤレス LAN13[13] などの$f$

確率リアルタイムシス’テムのゲーム理論的な仕テムのゲーム理論的な仕様記

述と検証を提案する. A.Pnueli らの時間ゲーム [11]の設計を難しくしている要因としては, 以下の 3 つを確率で拡張して,concurrent な確率時間ゲーム理が知られている [2].
論を提案して, さらに,

1. オープンシステムとして様々な構成要素が並行に動作していること [3]K.G.Larsen らの検証アルゴ
リズム [12] を確率で拡張して確率時間ゲームの到達可能ゲーム検証アルゴリズムを撫案する.
$’$

2 節で意味モデルである確率時間ゲームを-;

以下,

2. デジタルな離散的状態遷移に加えて, タイミン 3 節で仕様記述言語確率時間ゲームオートマトンをグ制約や制御法則などのアナログ動作が混在しているといったリアルタイム性があること$[4|$

3. 組込みシステムが動作する環境の不確定性があること [5]
これらの要因を解決するために, 今までに, 以下の手法が開発されている.

1. システムと環境との間のゲーム理論により, オー
プンシステムの構成要素の並行動作, つまり, リ
アクティブ性をモデル化している [6].

2. デジタル動作とアナログ動作が混在しているシ
ステムの記述のために, 時間オートマトンやハイ
ブリッドオートマトンが開発されている [7, 8].

3. 組込みシステムが動作する環境の不確定性を表現するために, 確率オートマトンや確率時間オー
トマトンが開発されている [9, 10].

2

確率時間ゲ-ム

2.1

確率時間ゲーム

定義 1 離散確率分布
集合 $S$ 上の有限な確率分布の集合を $\mu(S)$ とする.
$p\in\mu(S)$ は関数 $p:Sarrow[0,1]$ である. ただし,$\Sigma_{s\in S}p(s)=1$$l$

提案する tum-based ゲーム及び同時並行に動作を提案する concurrent ゲームがある. 時間ゲームはconcurrent ゲームである.
(2) 時間ゲームには, 遅延動作と離散動作があり,である.

$\square$

確率時間ゲームの構造を, 以下のように定義する.
定義 2 確率時間ゲーム
確率時間ゲームを組 $G=(S$ , so, Actsl, $Ac$お 2, 乃,
5, ) で定義する$\delta$(1) $S$ は状態の集合(2)

注目すべき既存研究として, リアクティブ性とア
ナログ動作を同時にモデル化するための, A.Pnueli
らの時間ゲームの研究がある [11]. 時間ゲームには,
以下の重要な特徴がある ;(1) ゲームには, システムと環境が交互に動作を遅延動作よりも離散動作が優先される.

それぞれ定義し, 4 節で検証法を説明し, 最後に 5
節で, まとめと今後の課題について述べる.

$s_{0}\in S$

は初期状態, Acts2 はそれぞれプレイヤー 1, 2 のアク(3) 孟ションの集合. Actsl, $A$ 伽 2 は互いに素な集合である. プレイヤーの行動は時間領域 $R$ とアク$cts_{1}$ションの組となる(4)$M_{i}=R\cross Acts_{i}(i=1,2)$.

妬は, 状態に対してプレイヤー
選択可能な行動を割り当てる関数である.

$\Gamma\cdot Sarrow 2$$i$(5) $\delta:Sx(NI_{1}\cup M_{2})arrow\mu(S)$ は遷移関数.

$i$

が

口

40

確率時間ゲームは二人非協カゲームであり, 各プレ
イヤーは状態 において, 行動 $m_{i}\in\Gamma(s)$ を同時に,かつ独立的に選択し, その結果, どちらか一方の行が選択され, $\delta((s, m_{i}))$ により, 不確定に次の動$s$$m_{i}$

状態に遷移する.
確率時間ゲームを実際のシステム上で次のように適用する.
プレイヤー 2

2. コントローラと環境は, 同時に, かつ独立して動作している.
システムは確率的に変化する.

システムをコントローラ, または環境により動作するものとし, 環境はシステムの正常な動作を妨害するものとして, 定義する.
各プレイヤーが行動を起こした時に, どちらか一方のプレイヤーの行動を選択することにより,

シス

テムの状態遷移が起きる.
行動の選び方を次のように定義する.
を起こし,プレイヤー 1 が行動を起.
同時に, プレイヤー 2 が行動
が, 選択さこした時, $\Delta_{1}<\Delta_{2}$ ならば,が, 選択される.
ならば,れる.
を選択する. 今回は,ならば,のゲームのプレイヤー 1 をコントローラ, プレイヤー
2 を環境と考えて検証を行う. 従って, 同時にアクションが起きる場合は, 環境を優先して選択することで, より安全な検証を行う.
形式的には, 選択関数 :SXMi $\cross M_{2}arrow\mu(S)$$\langle\triangle_{1},$$a_{1}\rangle\in\Gamma_{1}(s)$$\langle\Delta,$$a_{2}\rangle\in\Gamma_{2}(s)$$\langle\triangle_{1},$$\Delta_{2}<\Delta_{1}$$\Delta_{1}=\Delta_{2}$

定義 3 クロック変数
クロック変数は非負の実数値をとる変数であり, 同
じ速さで増加し, アクションが起こるときに にリセットすることができる. $R$ 上のクロック変数の集
口
合を $X$ とする.
$0$

する. クロック制約により, 遷移のタイミング制御を行う.

定義 4 クロック制約
上のクロック制約は $x\prec c$ または $x-y\prec c$ のは整数, $x,$ $y\in X,$
プール結合である. ここで,はくまたはである. $X$ 上のすべてのクロック制
口
約の集合を $\Xi[X]$ と表記する.

$X$$\prec$$c$

3. コントローラと環境がシステムに対して行った行動により,

構文

次にクロック制約条件とクロック変数の評価を定義

1. プレイヤーはコントローラと環境である.
(プレイヤー 1 がコントローラ,
が環境)

31

$(\Delta_{2},$$\langle\Delta_{2},$$a_{1}\rangle$$a_{2}\rangle$$a_{2}\rangle$

こ$\overline{\delta}$を用いて以下のように定義する.

$\leq$

定義 5 クロツク変数の評価
クロック変数の評価は関数 $v:Xarrow R$ である. $X$ の
すべてのクロック変数に を割り付ける評価を $0$ と表記する. $X$ のすべての評価を $V(X)$ と表記する.
評価 $v\in V(X)$ を与えたとき, すべてのクロック変数 $x\in X$ に対して, 評価 $(v+\delta)(x)=v(x)+\delta$ を$v+\delta$ と表記する.
クロック変数の集合 $r\subseteq X$ に対して,の中のクロック変数に を割り当てることを $v[r:=0]$ と表記する. クロック制約 $g\in$ 三と評価を満たすならば, $v\models g$ と表記す
が
に対して,
口
る. また, $[gI=\{v\in V(X)|v\models g\}$ とする.
$0$

$0$

$r$

$v$

$v$

$g$

確率時間ゲームオートマトンを以下のように定義する.

確率時間ゲームオートマトンは確率時間オートマ
トン [10] のアクションを制御可能なものと制御不能なものとに分けることにより実現する. 制御不能なアクションは環境のアクションである. これにより,確率時間ゲームオートマトン上の遷移は 2 種類存在する.

$\overline{\delta}(s, \langle\Delta_{1}, a_{1}\rangle, \langle\triangle_{2}, a_{2}\rangle)=\{\begin{array}{l}\delta(s, \langle\Delta_{1}, a_{1}) \Delta_{1}<\Delta_{2}\delta(s, \langle\Delta_{2}, a_{2}) \Delta_{1}\geq\Delta_{2}\end{array}$

定義 6 確率時間ゲームオートマトン
確率時間ゲームオートマトンは組 $A=(Q_{!},$

次に, 確率時間ゲームの表記法として, 確率時間ゲー$Acts_{c},$ $Acts_{u},$ $Inv,$ $\rho)$$q_{0},$

$X$

,

で定義する

ムオー トマトンを定義する.

(1) $Q$ はロケーションの有限集合,

3

確率時間ゲームオートマトン(2) $q_{0}\in Q$ は初期ロケーション.

確率時間オートマトンを拡張して, 確率時間ゲー
ムオートマトンを定義する. 確率時間ゲームオートマ
トンを確率時間ゲームとして, その動作を定義する.

(3) $X$ はクロック変数の有限集合.

(4) $Acts_{c}$ は制御可能 (controllable) なアクション.

(5) $Acts_{u}$ は制御不能 (un control lable) なアクシ
ョン.

41

行動

は $(q’, v’)$ へ遷移させる. ここで, $v’$ はにおいて 内の全てのクロック変数をリセット$\langle\triangle,$$v+\Delta$$a\rangle$$r$したものである. またこのとき $(q,v+\triangle)arrow a(q’,v’)$と表記する.
形式的に, 確率時間ゲームオー トマ トン$A=(Q, q0, X, Acts_{c}, Acts_{u}, Inv, \rho)$

問 ゲ

$-$

は確率時
$G=(S$ , so, Acts 1, $Acts_{2},$ム$\Gamma_{1},$として意味づけられる.

Acts 1$=$

各状態$\langle q,$$S$$Acts_{c}\cup\{\perp\},$ $Acts_{2}$$v\rangle\in S$

に対して,$\Gamma_{2},$$\delta)$$Q\cross V(X)$ ,$=$$=Acts_{u}\cup\{\perp\}$ ,$\Gamma_{i}((q, v\rangle)$

は

鋼御司能な

.

アクション

$\Gamma_{i}(\langle q,v\rangle)=\{\langle\Delta,a\rangle\in A/I_{i}’|\forall\Delta’\in[0, \Delta]$$v+\Delta’\models Inv(q)\wedge(a\neq\perp\Rightarrow$鱒御不能な

ヨ $q’\in Q$

.

アクション
$((q,g,a, r,p)\in\rho\wedge(v+\Delta)\models g\wedge p(s’)\neq 0\wedge$$(v+\Delta)[r:=0]\models Inv(q’)))\}\cup\{\langle 0, \perp\rangle\}$

図 1: 確率時間ゲームオートマトンの一例

(6)

遷移関数
$Inv:Qarrow\Xi[X]$ は各ロケーションに不変式を割り当てる関数$\delta$は$\delta(\langle q, v\rangle, \langle\Delta, a\rangle)=\overline{p}$全てののとき$\langle\Delta,$.

$a\rangle\in\Gamma_{i}(\langle q, v\rangle),$$\langle q’,$$v’\rangle\in S$に対して$a=\perp$(7) $p\subseteq Q\cross\Xi[X]x\{Acts_{c}\cup Acts_{u}\}\cross 2^{X}\cross\mu(Q)$ は
遜移関係. $(q, g, a, r_{\dagger}p)\in\rho$ に対して, $q\in Q$ は
遷移元のロケーション, $g\in\Xi[X]$ は遷移が起きるときのクロック制約条件, $a\in Acts_{c}\cup Acts_{u}$ ,は遷移にラベ/レ付けられたアクション, $r\in 2^{X}$$\overline{p}(\langle q’,$$a\neq\perp$$v’\rangle)=\{\begin{array}{l}1 \langle q’.v’\rangle=\langle q, v+\Delta\rangle \text{のとき}0 \text{上記以外}\end{array}$のとき,$(q,$ $g,$ $a,$ $r,$ $p)\in\rho$

は遷移によってリセットされるクロック集合,$p\in\mu(Q)$ はロケーション上の確率分布である,に対して$\overline{p}(\langle q’, v’\rangle)=\sum p(q’)$

口

32

意味

確率時問オートマトンの状態はロケーションとク
ロックの評価値の組 $(q, v)\in Q\cross V(X)$ である. $S=$
$Q\cross V(X)$ . プレイヤーは,時間経過する間,$Inv(q)$ が満たされているならば, すなわち, すべてのに対して $v+\Delta’\models Inv(q)$ となっている
ならば, 行動が $(q, v)$ で可能で, 行動により, 状態 $(q, v+\Delta)$ へ遷移する. この遷移を$(q, v)arrow(q, v+\Delta)$ と表記する.
状態 $(q, v)$ で, アクション $Q\in Acts_{i}$ に対して, 以下の条件を満たすとき, 行動が可能である.
$i$$\Delta$$\Delta’\leq\Delta$$\langle\Delta,$$\perp\rangle$$\langle\overline{\Delta},$$\perp\rangle$$\langle\Delta,$1.

$\triangle$$a\rangle$

時間経過するとき, $Inv(q)$ が連続的に満たさ

れる.

2.

$\rho$

内に $(q, v+\Delta)$ で可能な遷移 $(q,g, a, r,p)$ が存在する.

定義 7 パス
確率時間ゲームオートマトン $A$ の状態 $(q, v)$ から始まる状態列の集合を Paths $((q, v), A)$ と表記し,Paths $((q0,0), A)$ を Paths $(A)$ と表記する. また, 有限状態列 の最後の状態 f を lastの $n$ 番とし,$\omega$$(\omega)$

目の状態を $\omega(n)$ と記す.

口

確率時間ゲームオートマトンの実行例は以下のようになる.

$(q_{0},0)arrow^{\Delta_{0}}(q_{0},0+\Delta_{0})\underline{g0,r_{0},a_{0},p_{0}}(q_{1},0+\Delta_{0}[r_{0};=$$0])arrow(q_{1},0+\Delta_{0}[r_{0}\Delta_{1}:=0]+\Delta_{1})$$arrow^{g_{1,},a_{1_{1}},ri_{1},p_{1}}(q_{2}, (0+\Delta_{0}[r_{0};=0]+\Delta_{1})[r_{1};=0])arrow$. . 各状態においてシズテム動作を決定させる戦略を次のように定義する.

定義 8 戦略プレイヤー の戦略は状態列から行動への関数で$f_{i}:S^{+}arrow$ 雌を純戦略といい,$f_{i}:S^{+}arrow\mu(M_{i})$を混合戦略と呼ぶ. ここで,は状態の 1 回以上の繰り返しである. ゼロ和 2 人ゲームでは, 混合戦略
$i$

$S^{+}$

3. $Inv(q’)$ が満たされている.

ただし,$p(q’)\neq 0$.

$\omega$42の範囲で均衡点が存在することが知られているため,[19/ 各プレイヤーの戦略を混合戦略とする. また, 混
合戦略は純戦略を包含しているため, 混合戦略の場
合のみを考えれば十分である. $\forall\omega,\omega’\in Paths(A)$に対して, last $(\omega)=last(\omega’)$ ならば $f(\omega)=f(\omega’)$とする.

$c1.0\leq v\leq 2$

口

各プレイヤーの戦略により, 確率時間ゲームのパスが決定される.
定義 9 ゲームの経歴
プレイヤー の戦略ゐにより, ゲームの経歴が決定される. ゲームの経歴 Hist $((q, v), fi, f_{2})$ はパスの部分集合であり, 帰納的に以下のように定義される.

$0\leq \mathfrak{i}$

$i$

.

く1

$2<x\leq 3$$1\leq x\leq 2$$(q,v)\in Hist((q,v), f_{1}, f_{2})$$\omega\in Hist((q, v), fi, f_{2})$ ならば $\omega’=\omegaarrow e(q’, v’)$

ただし以下の条件を満たすものとする.
$-\omega’\in Paths((q,v),A)$

図 2: ロケーション内での利得行列の変化$-e\in\Lambda 1_{1}\cup A’I_{2}$$-e=\overline{\delta}(last(\omega),f_{1}(\omega),f_{2}(\omega))$1.
$1^{\backslash }A$

口

降では,

このグラフを確率時間ゲームグラフと呼$S\backslash$まず, 確率時間ゲームグラフを定義するために,$t\epsilon$

$4$

4.1

到達ゲームの検証
利得行列不変条件集合に置き換えた後に均衡点を計算し, その確率値を求める. 確率時間ゲームオートマトンの各状態において, 利得行列の行はコントローラのアクション,

列は環境のアクションとして利得行列が形成される.
がどの状態でも可能である
ため利得行列は必ず存在する. ただし, ロケーショ
で均衡点が一意には決まらない. そこで, 新たに利得行列不変条件を導入し各利得行列に対して均衡点を計算する. 利得行列不変条件をその条件内では利得行列が変化しないクロック条件として定義する.

example 1 図 2 のような確率時間ゲームオートマ
トンのロケーションにおいて,クロック値の値によ利得行列が変化していく.

新たに利得行列不変条件を定義し, この条
件に従いノードを生成し, このグラフに対して均衡点を計算する
そこで,を行う.

$\not\in$義 10 利得行列不変条件

. .
確:

.i

準

–t-

ームオートマトンの各ロケー

ション $q\in Q$

に対して, 利得行列不変条件の集合を割り当てる関
数 $mInv:Qarrow 2^{\equiv(X)}$ を以下のように定義する.
$\Gamma(q, v),$$(q, g, a, r,p)\in\rho$ に対して

$mInv(q)=\{(q,$ ん $|h=[$ ん, ん i $=$ん1
または }また, $mInv(Q)=\{mInv(q)|q\in Q\}$ と表記する
$)$

$g$

$0\wedge$$\wedge\cdots\wedge h_{n}J$$\overline{g}$口$\perp$ン内に利得行列が複数あるため同一ロケーション内

り,

$F$

$l\epsilon$

確率時間ゲームの状態は, ロケーションとクロッ
ク値の組で表わされるため, 無限の状態数を持つこととなる. そこで, 連続した無限の状態空間を有限の

また, 各プレイヤーは$\{j$

定義 11 successor$di$(l)discrete-successor$X\subset S$$A$
cts_{u}\}$と $a\in\{Acts_{c}\cupActsに対して,X の a-を以下のように定義する.
successor を以下のように定Post $a(X)=\{(q’,v’)|$ ヨ $(q, v)\in X, (q, v)$ 乳 $(q’, v’)\}$(2) timed-su
me $-su$ ccess orを以下のように定timed-successor
med-successor を以下のように定義する.
$X\nearrow=\{(q, v+d)|(q,v)\in X, v, v+d\models Inv(q), d\geq 0\}$$\square$

43

次に,

確率時間ゲームグラフを定義する.

1. last2.

定義 12 確率時間ゲームグラフ$(\omega)\in$$\omegaarrow a$

Goal $\cross V(X)$ならば,$a\in Acts_{u}$確率時間ゲームグラフを遷移システム$(mInv(Q), So, arrow)$ と定義する.

1. $mInv(Q)$ はっまり, 長さが有限ならば最終的に Goal に到達するようなものを考える. しかし, Goal に到達する上の利得行列不変条件の集合$Q$

2. $S_{0}=(q_{0}, h_{0})$$h_{0}$$q_{0}$

口

ここで,はクロック評価 を含むようなロケーションの利得行列不変条件.
$0$

前にシステムの行える制御可能なアクションが無い
為にシステムが停止する可能性のあるパスも考慮に入れて (2). の条件を付ける.

zeno となるときには正しく検証を行うことができ$(q_{0}, v_{0})\in mInv(Q),$ $0\in h_{0}$$3$.

$arrow$.

は時間遷移$arrow\perp$と離散遷移亀め和集合

時間遷移$mInv’$$mInv(q)$ かつ $mInv+\epsilon$$mInv’(0<\epsilon<1)$ を満たす $mInv’$ が存
$\in$

.

$\models$

在するとき,$(q, mInv)arrow\perp(q, mInv’)$$\rho$$\nearrow$口$p(q’\rangle\neq 0$

確率時間ゲームの到達ゲームの検証を行う. まず到達ゲームに関する定義をし, 検証を行う. 検証は次のような手順で行う.

1. Goal に到達可能な状態を全て求める.

2. 各状態の均衡点を求め, ゲームの結果により,Goal に到達する確率を求める.
Goal は到達すべきロケーションの集合である.

つまり, 与えられた確率時間ゲームオートマ
トンの初期状態 $(q_{0},0)$ から Goalへの到達可能性を検証する.
制御不能なアクションはシステムが Goal に到達するのを阻止するようなものと考える. つまり, 制御$\subseteq Q$

不能なアクションでは Goal- に到達できないとして検証を行う. そこで, K.G. Larsen らの考え方 [12]を採用して, 次のように最大パスを定義する.

定義 13 最大ゲーム
下記の条件を満たすゲームの経歴を最大ゲームとする.

...

$arrow^{e_{n}}(q_{n+1}, v_{n+1})\cdots$$v_{k})\in$ Goal $\cross V(X)$ が存在
こ対して, $k\geq 0$ でするとき, そのゲームの経歴を勝利ゲームとする.
$(q_{k},$$|$口さらに, 状態に関して勝利可能状態を以下のように定義する.

定義 15 勝利可能状態
状態 $(q,$ $v)$ に対して, その状態から始まる勝利ゲー
ムが存在するとき, その状態を勝利可能状態とする.
口

検証アルゴリズムは次のようなステップから成る.

ステップ 1 到達可能性判定を行う.
ステップ 2 各ノードに対して, 均衡点を計算して確率を求める.

42

到達可能性判定ステップ 1 では, 時間ゲームに対するアルゴリズム[12] を確率遷移を含むよ、うなオートマトンに拡張したアルゴリズムを用いる. 与えられたオートマトンがGoal に到達するかを解析する.
図 3 に示す.

長さが有限で次の条件のどちらかを満たすもの

このアルゴリズムを

このアルゴリズムはゲームグラフの作成を行いつつ, Goal への到達可能性を検証する. まず, 初期状態から 以上の確率で到達可能な状態を求め, Waitng に入れながら確率時間ゲームを作成する. 到達可能な状態を求める際には Waiting から一つ取り出し $e=(S, \alpha, S’)$ として, $S’$ に対して Goal$0$・長さが無限$\bullet$各プレイヤーの戦略あにより, 決定される最大ゲーム$\omega=(q_{0}, v_{0})arrow e_{0}(q_{1}, v_{1})arrow e_{1}$.

$arrow a$

ここで,ムの勝利を以下のように定義する.
定義 14 勝利ゲーム.

離散遷移
かつ $mInv’$$=$$(q,g, a;r,p)$( $(mInv\cap[gI)[r := 0])$
が存在す
るとき,
$(q,mInv)$$(q’, rrtInv’)$ ただし,$\in$ないため, 記述されたオートマトンに対し, zeno の判定を行うことが必要である. 確率時間ゲームオー
トマトンの zeno の判定には, 既存の確率時間オー
トマトンに関する判定法 [18] を利用する. 確率時間
ゲームオートマトンに対して, システムが到達ゲー

44

図 3: 到達可能性検証アルゴリズム

か否かを判定する. ここで, $\alpha\in\{Acts_{c}\cup Acts_{u}\cup\perp\}$である. また, その際に $S’$ を Passed に入れ, ノー
ド作成済みであることを記憶する. この一連の操作を Waiting の中身がなくなるまで繰り返す. ただし,この繰り返しは $S’$ がすでに, Passed に含まれている記号的状態 $S”$ に含まれる場合は新たに追加する
操作をせずに, 次の Waiting の中身に対して, 操作を行う. 最終的に作成された確率時間ゲームグラフのノードに Goal が含まれていれば, オートマトン
は Goal に到達可能であると言える.

に到達する確率を計算する.

431

均衡点

生成されたグラフの各ノードからの Goal への到達確率に基づき, 各プレイヤーの利得を定義する.
プレイヤー 1 の利得を到達確率 とし, プレイヤー
2 の利得を $1-p$ と想定することにより, 確率時間
ゲームは 2 人ゼロ和非協カゲームとなる. 2 人非協
カゲームは混合戦略の範囲で均衡点が求まることが知られており, あるノードにおいて, ゲームの均衡
点が, そのノードからの到達確率となる.
$p$

図 1 のオートマドンに対してこのアルゴリズムを行った結果を図 4 に示す. 確率時間ゲームグラフが作成され, このグラフに対して確率計算を行う.

432

43

を求める.

確率計算法

図 3 のアルゴリズムにより作成されるグラフに対して. 確率ゲームでの手法を用いて, 確率値 (均衡点)を求める.

Alfaro らの手法 [16, 17] を用いて Goal

確率計算

確率時間ゲームの均衡点として, マックスミニ値
ゲームグラフのノードに対して, 図 5 のような利得行列となるとき’, ノードの均衡点 (マックスミニ値) を求めることは, 以下の問題を解くこ45

図 5: 利得行列$.\sim,$$\supset$

.

$.-$

.

環填

$!$

のアクシ 1 ン

ントローう.

.

$|$$\perp$$\int$$C$$1$のアクシ. ン1.
$0$$\perp$$X_{b^{\dot{\prime}}}$0.1 甚, $+0.9t_{7}$$b$図 4: 確率時間ゲームグラフとに等しい.

$\prime 1_{t!}^{\wedge}$

図 6: ノード 3 の利得行列

最大化$:x_{i}$p J ま図 6 のようになる.

したがって, ノード 3 においてマックスミニ値を求める問題は以下のようになる.
$|$

$|$

制約条件

$:x_{i} \leq\sum_{0\leq k\leq m}r_{k}b_{k0}$$x_{i} \leq\sum_{0\leq k\leq m}r_{k}b_{k1}$最大化$:x_{3}$

制約条件 $:x_{3}\leq r00+r_{1}(0.1x_{3}+0.9x_{7})$$xs\leq r_{0}x_{8}+r_{1}x_{8}$$x_{i} \leq\sum_{0\leq k\leq m}r_{k}b_{kn}$$\sum_{0\leq k\leq m}r_{k}=1$

ここで,$i,\langle\Delta,$$b_{ij}= \sum p(j)x_{j},p=\delta((q, v)\}\langle\Delta, a)),(q, v)\in$$r_{0}+r_{1}=1$

さらに, 各ノードのマックスミニ値は以下の問題を解くことで求められる.

最大化 : $\sum x_{i}$$a\rangle\in\Gamma((q, v))$

制約条件で. プレイヤー 2 の確率を最小化するような動作を表し, そのなかでプレイヤー 1 が到達確率を最大化することにより, マックスミニ値を求める.

example 2 ノード $3(q1,1\leq x=y\leq 2)$ の利得行

制約条件 $:x_{i} \leq\sum_{0\leq k\leq m}r_{k}b_{k}i(0\leq l\leq n)$$\sum_{0\leq k\leq m}r_{k}=1$

46

図 4 のグラフについて上記の問題を解くと,の均衡点 (到達確率) は 0.99 となる.

ノード

$0$

5

まとめと今後の課題
今回の結果で到達ゲームに関しては不確定性を持つシステムと環境との相互作用を記述できた. また
その記述を用いて, 確率時間ゲームオートマトンの到達ゲームに関する検証を行い, その検証アルゴリ
ズムの動作を実際に計算機上で確認をした.
今回は到達ゲームに関する検証を行ったが. 今後は到達ゲーム以外のゲームに関しての検証を行う.

参考文献[1] T.A. Henzinger, C.M. Kirsch. Embedded Software: Proceedings of the First Intemational
Workshop, EMSOFT 01. LNCS 2211, P.504,
Springer-Verlag, 2001.
[2] T.A. Henzinger. Games, time, and probability: Graph models for system design and analysis.Proceedings of the $33rd$ Intemational Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), LNCS
4362, pp. 103-110, Springer, 2007,[3] D. Harel, A. Pnueli. On the Development ofReactive Systems. NATO $ASI$ Senes F. Vol.
13, pp477-498, SpringerVerlag, 1985.
[4] M.K. Inan, R.P. Kurshan. Verification of Digital and Hybrid Systems. NATO $ASI$ Series$F$ ;Computer and Systems Sciences, Vol. 170,

[9] R. Segala, N.A. Lynch. Probabilistic Simulations for Probabilistic Processes. Nordic
Joumal of Computing, Vol.2, No.2, pp.250-273,

1995.

[10] M. Kwiatkowska, G. Norman, R. Segala, J.
Sproston. Automatic verication of real-timesystems with discrete probability distributions.
$TCS282$ , pp 101-150, 2002[11] O. Maler, A.Pnueli, J.Sifakis. On the Synthesis of Discrete Controllers for Timed Systems.
LNCS 900, pp.229-242, 1995.
[12] F. Cassez, A. avid, E. Fleury, K.G. Larsen,
D. Lime: Efficient On-the-Fly Algorithms for
the Analysis of Timed Games. LNCS 3653,
pp.66-80, 2005.
$D$[13] Wireless LAN Medium Access Control(MAC)and Physical Layer(PHY) Specifications
ANSI/IEEE Std 802.11, 1999 Edition.
[14] C. Courcoubetis and M. Yannakakis. Markov
decision processes and regular events. IEEE
Trans. on Automatic Control, 43:1399-1418,

1998.

[15] A. Biaiico and L. de Alfaro. Model Checking of
Probabilistic aiid Nondeterministic Systems. In
FST TCS 95: Foundations of Software Technology and Theoretical Computer Science, LNCS
1026, pp. 499-513. 1995.

[5] H.A. Hansson. Time and Probability in Formal
Design of Distributed Systems. $PhD$ tnesis, Uppsala University, 1991.

[16] L. de Alfaro. Computing Minimum and Maximum Reachability Times in Probabilistic Systems. In CONCUR 99: 10th Intemational Conference on Concurrency Theory, LNCS 1664,
pp.66-81, 1999.

[6] A. Pnueli, R. Rosner A Framework for the Synthesis of Reactive Modules. LNCS 335, pp.4-17,
Springer 1988.

[17] L. de Alfaro, R. Majumdar: Quantitative Solution of Omega-Regular Games. In Journal ofComputer and System Scien ces 68, pp 374-397,

Springer-Verlag, 2000

[7] R. Alur, D.L. Dill. A theory of timed automata.
$TCS,Vol.126$ , pp.183-235, 1994.
[8] R. Alur, C. Courcoubetis, N. Halbwachs, T.A.
Henzinger, Pei-Hsin Ho, X. Nicollin, A. Olivero,
J. Sifakis, S. Yovine. The Algorithmic Analysis
of Hybrid Systems. $TCS$ , Vol.138, No.1, pp.
3-34, 1995.

2004.

[18] M. Kwiatkowska, G. Norman, J.-Sproston andF. Wang. Symbolic Model Checking for Prob-

abilistic Timed Automata. Information andComputation, 205 (7), pp. 1027-1077. July 2007.

$[$

19

$]$

鈴木光男, 新ゲーム理論, (社) 勤草書房, 東京,

1994