日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

確率的環境下において平均利得時間論理仕様を実現する最適マルコフ決定過程の自動合成法
冨田 尭

山崎 徹郎

萩原 茂樹

米崎 直樹

制御系のように，外部環境と継続的に相互作用するシステムをリアクティブシステムと呼ぶ．仕様からのシステムの自動合成は，不具合のないシステムを，誤りを起こしやすい人間の介入なしに生成するための手法として盛んに研究されてきた．しかし，古典的な自動合成では機能仕様のみに注目していた．一方で，性能仕様にも注目し，それを実現するだけでなく最適な性能を持つシステムを自動合成できることが実用上望ましい．そこで本稿では，与えられた
確率的環境下において，平均利得時間論理 LTLmp で記述された機能及び性能仕様を実現し，かつ，平均利得目的関数に関して最適なリアクティブシステムをマルコフ決定過程として自動合成する手法を提案する．本手法では，環境とリアクティブシステムの相互作用を，LTLmp 仕様を反映した重み付きゲームとしてモデル化する．そして，そのゲーム上の線形制約充足可能性判定と線形計画法を利用して自動合成を行う．

力を決定し仕様を満たすことができる RS が存在す

1 はじめにる」という性質である．

外部環境と継続的に相互作用するシステムをリアク

RS 仕様の記述には，しばしば線形時相論理 LTL

ティブシステム（reactive system，RS）と呼ぶ．各[12]（Linear Temporal Logic）が用いられてきた．

種制御系などの多くのシステムは RS であり，しばしLTL は 時 間 的 性 質 を 記 述 で き る 様 相 論 理 で あ り，

ば高い安全性が要求されている．そうした高い信頼「常に，要求 req に対してはいつか応答 res を返す性が求められる RS の開発には仕様（speciﬁcation） （2(req → 3res)）」などのイベント生起順序に関すの形式的検証がしばしば行われているが，究極的にる，機能要求（functional requirements）を反映したは，仕様からのプログラムの自動合成（automatic

性質を直観的に記述できる．LTL で記述された RS 仕

synthesis）が望まれる．RS は，RS が直接制御でき様の実現可能性判定問題は 2EXPTIME 完全 [11] [13]ない外部環境から次々に与えられる入力に対して，各であり，実現可能であるときにはプログラムを自動合成をできることが示されている．そして，Lily†2 [9]，時点で適切に応答しなければならない．そのため，RS

Acacia+†3 [4]，Unbeast†4 [7] や [16] などの LTL 実現

仕様は単に無矛盾（充足可能）なだけでなく，実現可能性†1 [11] [1] [13]（realizability）を満たす必要があ

可能性判定器（自動合成器）が開発されている．しかる．これは「外部環境から与えられる任意の入力列にしながら，LTL では機能要求を反映した性質しか記対して，各時点において，過去の情報のみを用いて出述できないため，LTL 仕様からの自動合成で得られAutomatic Synthesis of Optimal Markov Decision
Processes Realizing Mean-Payoﬀ Temporal Logic
Speciﬁcations under Probabilistic Environments
Takashi Tomita, Tetsurou Yamazaki, Shigeki Hagihara,Naoki Yonezaki, 東京工業大学大学院情報理工学研究科計算工学専攻, Dept. of Computer Science,
Graduate School of Information Science and Engineering, Tokyo Institute of Technology.
†1 プログラム可能（programmable）ともいう．

るプログラムは，機能的には安全でも非効率的にふるまう可能性がある．一方で，現実的なシステムでは，
例えば，「（できるだけ/一定の以上）無駄な動作をし†2 http://www.iaik.tugraz.at/content/research/
design verification/lily/†3 http://lit2.ulb.ac.be/acaciaplus/†4 http://www.react.uni-saarland.de/tools/unbeast/

ない」や「（できるだけ/ある程度）短い時間で応答は重み付き正規ゲームの一種である多閾値平均利得する」などの性能要求（performance requirements）

Rabin ゲーム（multi-threshold mean-payoﬀ Rabin

を満たすことが求められる．

game，MTMPRG，単に MPRG）を用いる．そして，

そこで本研究では，機能要求だけでなく性能要求もそのゲーム上で，環境側プレイヤの戦略に対抗する反映した仕様から，プログラムを自動合成する手法を

RS 側プレイヤの戦略を，線形制約充足可能性判定/

開発することを目的とする．性能要求を反映した性質

線形計画法（linear programming，LP）を用いて構も記述可能な仕様記述言語としては，LTL に平均利成/最適化することで，実現可能性判定及び最適自動得の概念を導入した線形時間論理 LTLmp [14] を用い合成を行う．

mp

る．LTL

は，各時間で発生する利得（payoﬀ）を規定することができ，その平均利得（mean-payoﬀ）に本稿の構成: まず 2 章で RS と環境及びそれらのふ関する閾値条件を記述できる．それにより，例えば，

るまいの定義を与える．次に 3 章で仕様記述言語と「平均的な動作コストが一定以下である」や「要求待して用いる LLTLmp の構文と意味論を紹介する．まち状態である時間の割合が一定以下である」などの性た，本稿で扱う弱い（確率的）実現可能性の定義を与能仕様や，「故障状態である頻度（をできるだけ小さえる．

く）」などの最適化対象となる目的関数も記述できる．

4 章では，与えられた確率的環境の下で LLTLmp

そして，このような仕様に対してモデル検査と充足可仕様を実現し，かつ，LLTLmp 目的関数に関して最能性判定を指数時間で行うことができ，また，充足可適な RS を自動合成する手法について述べる．4. 1 節

能な範囲で仕様を最適化することもできる [14]．ただでは，RS と環境をモデル化し，LLTLmp 仕様を反映

mp

し，LTL

は表現力が高く実現可能性の検証は困難

する MPRG の定義を与える．また，そのゲーム上でである．そこで，実現可能性判定のための仕様記述にの RS 側/環境側プレイヤの行動指針である戦略に関mpを用する定義も与える．4. 2 節で LLTLmp 実現可能性判いる．また，性能に関する評価という面では，「任意

定/最適合成問題が MPRG 上の戦略合成問題に帰着の環境」を想定した最悪ケースの解析よりも「限定さできることを示す．

は，構文を一部制限したフラグメント LLTL

れた環境」を想定した平均ケースの解析の方がしば5 章では，その戦略合成の基本的なアイディアと手しば重要となる．そこで本研究では，通常の実現可能続きの概略を示す．そして，6 章で MPRG 戦略合成性とは異なる，「確率的にふるまう既知の環境に対し手続きの主要部分のアルゴリズムを説明し，7 章でそて，過去の情報のみを用いて出力を決定することで，れらを用いた具体的な MPRG 戦略合成手続きを与えほとんどすべてのふるまいが仕様を満たすことがでる．8 章では，7 章で与えた MPRG 戦略合成手続き

きる RS が存在する」という弱い（確率的）実現可能の計算量と LLTLmp 実現可能性判定/最適合成問題

性に注目する．つまり，環境をある種の Markov 決の計算量について述べる．

定過程（Markov decision process，MDP）として捉え，その環境に対して適切に応答する RS のみに注目

9 章で関連研究について述べ，最後に 10 章でまとめる．

する．
そ し て 本 稿 で は ，既 知 の MDP 環 境 に 対 し て ，mp

2 リアクティブシステムと環境

目的関数に

本章では，リアクティブシステム（RS）と環境，そ関して最適な RS を MDP として自動合成する手法をしてそれらの相互作用からなる振る舞いの定義を与与える．この手法では，古典的な自動合成 [9] [8] [7] [16]

える．

LLTL

仕様を実現し，かつ LLTL

mpと同様に，RS と環境の相互作用を，仕様を反映した

本稿では，RS と環境を，互いに相手から与えられゲーム（game）としてモデル化する．ただし，LTLる（自身にとっては非決定的な）アクションあるいは自動合成で用いる正規ゲームとは異なり，本手法でイベント生起に対して確率的に応答するシステム，つまり，ある種の Markov 決定過程（Markov decision

初期状態 s0 の遷移確率関数に関する制約から，RS

process，MDP）としてモデル化する．

の最初の出力は入力に依存しない．RS と環境の相互定義 1 (MDP). MDP は五つ組 hS, ΣI , ΣO , P, s0 i で作用開始時にはどちらか一方（この定義では RS）がある．ただし，入力なしで出力しなければならないためこの最初の• S は状態集合，

入力を無視することで相互作用開始時の同期を行う．

• ΣI /ΣO は ΣI ∩ ΣO = ∅ である入/出力アクショ

なお，無限状態をもつ RS は現実には実装できないため，実用的な RS は有限状態である必要がある．

ンの集合，• P : S × ΣI × ΣO → ([0, 1] × S) は遷移確率関数，• s0 ∈ S は初期状態である．

一方で，環境は，2OAP /2IAP を入/出力アクションとする MDP である．

また，任意の状態 s と入力アクション A ∈ ΣI につい

定義 3 (MDP 環境). 環境 E は，入/出力アクションて，以下の条件が成り立っているものとする．
X
Prob(P (s, A, B)) = 1.

ΣI /ΣO に関して，以下の制約をもつ MDP である．
(1)

• ΣI = 2OAP ，

ここで，P (s, A, B) = hp, s0 i のとき，Prob(P (s, A, B))• ΣO = 2IAP ．

B∈ΣO



は p を，State(P (s, A, B)) は s0 を与える関数である．

RS R と環境 E のふるまい（behavior）は，互いに

相手の出力（自身の入力）に対して確率的な出力（相P (s, A, B) は，状態 s で入力アクション A ∈ ΣI が与えられたときにアクション B ∈ ΣO を出力する確率 p とその際に遷移する先の状態 s0 の対 hp, s0 i を与える関数である．
アクション（イベント生起）は，しばしば原子命題
集合の部分集合で表現される．つまり，それぞれの原子アクションと対応する原子命題を定義し，原子命題の集合で複数の原子アクションの同時発生を表すアクションとする．本稿では，RS のアクションを（RSにとって）出力原子命題 OAP の部分集合，環境のアクションを（RS にとって）入力原子命題 IAP の部
分集合とする．ただし，OAP と IAP は共通部分をもたないものとし，その和集合 OAP ∪ IAP を APで表す．形式的には，RS は以下のような制約をもつ構成される．ただし，既に述べたように，RS の最初の入力を無視することで RS と環境の相互作用の同期を行う．形式的には，RS と環境の状態対とアクション対（入出力命題集合の和）の交代列として定義される．
定義 4 (RS と環境のふるまい). R = hS, 2IAP , 2OAP ,P, s0 i を MDP RS，E = hS 0 , 2OAP , 2IAP , P 0 , s00 i を
MDP 環境とする．
このとき，R と E のふるまいは，状態対-アクション
交代無限列 r = hs0 , s00 i(a0 ∪ b0 )hs1 , s01 i(a1 ∪ b1 ) . . . ∈((S × S 0 )(2AP ))ω である．ただし，• ある b ∈ 2IAP に関して，State(P (s0 , b, a0 ))

=

s1 ,

=

si+1 ,=

s0i+1 .

• 任意の i ∈ N>0 について，

MDP である．
定義 2 (MDP RS). RS R は，入/出力アクションΣI /ΣO ，遷移確率関数 P に関して，以下の制約をもつ MDP である．

State(P (si , bi−1 , ai ))0State(P (s0i , ai , bi ))また，R と E のふるまいの集合を BhvR,E で表す．
こ の 定 義 で は ，RS の ア ク ション と そ れ に 対 す• ΣI = 2IAP ,る 環 境 の ア ク ション の 組 を 一 単 位 時 間 で 発 生 す• ΣO = 2OAP ，• 初期状態 s0 に関して，任意の入力アクション
A, A0 ∈ ΣI と出力アクション B ∈ ΣO に関して，
P (s0 , A, B) = P (s0 , A0 , B).

手の入力）と，それに伴う状態遷移の繰り返しにより(2)


るアクションと解釈する．そして，ふるまい r =hs0 , s00 i(a0 ∪ b0 )hs1 , s01 i(a1 ∪ b1 ) . . . の AP に関する時間的性質は偶数番目要素列 σ = (a0 ∪b0 )(a1 ∪b1 ) . . .
で特徴付けられる．この σ を r 上の語（word）といい，word(r) で表す．

また，2n + 1 番目の要素までのプレフィックス

3. 1 LLTLmp

hs0 , s00 i(a0 ∪b0 ) . . . hsn−1 , s0n−1 i(an−1 ∪bn−1 )hsn , s0n i

RS の仕様記述言語には，線形時相論理 LTL [12]を pref n (r) で表す．ある実行 r ∈ BhvR,E のプレフィッがしばしば用いられている．LTL では，「常にある

クス rﬁn = pref n (r) に対して，rﬁn をプレフィックス

性質 ϕ を満たす（2ϕ）」や「無限にしばしばあるとしてもつふるまいの集合を rﬁn の筒集合（cylinder

イベント ϕ が生起する（23ϕ）」，「常に，イベントset）といい，Cyl
R,E

R,E
0

ϕ1 が生起したならばいつかイベント ϕ2 が生起する(rﬁn ) で表す．
R,E0|rﬁn = pref n (r )}. (3)（2(ϕ1 → 3ϕ2 )）」などのイベント生起順序に関する

このとき，その筒集合 CylR,E (rﬁn ) に含まれるふる定性的性質，すなわち，システムの機能要求に関する

まいの生起確率は，以下のように定義される．

仕様を記述できる．しかしながら，LTL では性能要

Cyl

R,E

(rﬁn ) = {r ∈ Bhv

R,EPr(rﬁn )) =8 (Cyl
>
>
1
>
>
>
>
>
>
>
if n = 0,
>
>
>
>
>
>
>
Prob(P (s0 , b0 , a0 )) · Prob(P 0 (s00 , a0 , b0 ))
>
>
>
>
>
< if n = 1,>
0>
PrR,E (CylR,E (rﬁn
))
>
>
>
>
>
>
>
· Prob(P (si−1 , bi−2 , ai−1 ))
>
>
>
>
>
>
>
· Prob(P 0 (s0i−1 , ai−1 , bi−1 ))
>
>
>
>
>
: if n > 1.

求を反映した仕様を記述できなかった．
そ こ で ，我々は LTL の 平 均 利 得 拡 張 時 間 論 理

LTLmp [14] を開発した．LTLmp では，それぞれの時間で発生する利得（payoﬀ）を規定することができ，その平均利得（mean-payoﬀ）に関する閾値条件を記(4)0
ただし，rﬁn = rﬁn(an−1 ∪ bn−1 )hsn , s0n i とする．

述できる．それにより，LTL で記述できるイベント
生起順序に関する定性的性質に加えて，平均コストやイベント生起頻度などに関する定量的性質，すなわ
ち，システムのある種の性能要求に関する仕様を記述できる．
時間論理仕様の実現可能性判定及び自動合成では，

このとき，この PrR,E は，標本空間 BhvR,E とす

時間論理仕様と等価な決定性オートマトンを構成し，べての筒集合 CylR,E (rﬁn ) から生成される完全加法

それを解析することで判定と合成を行うアプローチが族からなる可測空間上の確率測度となる．

一般的である [9] [8] [7] [4] [16]．しかしながら，LTLmp

なお，RS と環境がどちらも有限状態であるとき，で規定される言語は決定性オートマトンでは認識でそのほとんどすべてのふるまい r について，r 上の状

きないことが示されており [15]，LTLmp 実現可能性

態対 hs, s0 i やアクション a ∪ b の出現頻度は収束する．

判定/自動合成には同様のアプローチを適用することはできない．そこで本稿では，決定性オートマトンで3 仕様認識可能であることが保証されている LTLmp フラグ

システムが満たすべき性質を仕様という．モデル検

メント Lite LTLmp （LLTLmp ）を仕様記述言語とし査や無矛盾性（充足可能性）判定などの形式的検証でて用いる．

は，仕様は曖昧性なく記述されていなければならな

定義 5 (LLTLmp の構文). AP 上の LLTLmp 式 ϕ はい．そのため，仕様記述言語には時間論理やオートマ

以下のように帰納的に定義される．

トンがしばしば用いられている [2]．
本章では，本研究で仕様記述言語として用いる平

LLTLmp 式:

Φ ::=Ψ ∧ Θ,

LTL 式:Ψ ::=ψ | ¬Ψ | Ψ ∨ Ψ |Ψ ∧ Ψ | XΨ | ΨUΨ,

均利得線形時間論理 LLTLmp の定義を与える．また，

ω-正規言語を受理可能である決定性 Rabin オートマ

ブール式:

ψ ::=

γ | ¬ψ | ψ ∨ ψ | ψ ∧ ψ

トンについても簡単に紹介する．そして，LLTLmp 仕

平均利得式:Θ ::=θ | Θ ∨ Θ | Θ ∧ Θ,

原子平均利得式:

θ ::=MP(t)  0

利得項:

t ::=

c |1ψ | t + t | t · t | − t.

様の実現可能性の定義を与える．

ただし，γ ∈ AP ，c ∈ R， ∈ {>, ≥} とする．



時間演算子 X と U は，それぞれ next 演算子と until

定 義 6 (LLTLmp の 意 味 論). 無 限 長 語 σ

演算子と呼ばれる．直観的には，XΨ は「次のステッA0 A1 . . . ∈ (2プで Ψ が成り立つ」，Ψ1 UΨ2 は「いつか Ψ2 が成り

関係 |= は以下のように帰納的に定義される．

立ち，それまでの間は Ψ1 が成り立っている」ことを表す．
利得項 t は各時間で発生する利得を規定しており，

AP ω

mp

) と AP 上の LLTL=

式 Ψ の充足σ |= Ψ ∧ Θ⇔σ |= Ψ and σ |= Θ,σ |= ψ

⇔σ[0] 6|= ψ,σ |= ¬Ψ⇔σ 6|= Ψ,実定数 c ∈ R，ブール式 ψ の充足に対する利得を表す

σ |= Ψ1 ∨ Ψ2⇔

σ |= Ψ1 or σ |= Ψ2 ,特性変数 1ψ ，及び，それらの代数演算（和 “+”，差σ |= Ψ1 ∧ Ψ2⇔

σ |= Ψ1 and σ |= Ψ2 ,“−”，積 “·”）からなる．直観的には，特性変数 1ψ

σ |=

Ψ

⇔

σ[1 . . .] |= Ψ,は ψ を満たすとき 1，そうでないとき 0 を与える項

σ |= Ψ1 UΨ2⇔∃i ∈ N.(σ[i . . .] |= Ψ2 and∀j ∈ N<i .σ[j . . .] |= Ψ1 ),である．
原子平均利得式 θ = MP(t)  0 は「t で規定される

A |= γ⇔γ ∈ AP,

利得の平均値（平均利得）の下極限が閾値条件 0 を

A |= ¬ψ⇔A 6|= ψ,満たす」ことを表す．また，平均利得式 Θ は，原子A |= ψ1 ∨ ψ2⇔

A |= ψ1 or A |= ψ2 ,平均利得式の連言と選言からなり，否定は含まない．

A |= ψ1 ∧ ψ2⇔

A |= ψ1 and A |= ψ2 ,ここで，以下のような略記も用いてよいものとする．

σ |= MP(t)  0⇔[[MP(t)]]σ  0,

σ |= Θ1 ∨ Θ2⇔

σ |= Θ1 or σ |= Θ2 ,σ |= Θ1 ∧ Θ2⇔

σ |= Θ1 and σ |= Θ2 .

>≡ϕ ∨ ¬ϕ≡MP(1ψ ) ≥ 0,

⊥

≡

¬⊥,

ただし，γ ∈ AP ，c ∈ R， ∈ {>, ≥}，σ[i] は語 σ

ϕ1 → ϕ2≡¬ϕ1 ∨ ϕ2 ,の i 番目の要素 Ai ，σ[i . . .] は語 σ の i 番目以降のサ

ϕ1 ↔ ϕ2≡(ϕ1 → ϕ2 ) ∧ (ϕ2 → ϕ1 ),フィックス Ai Ai+1 . . . とする．また，[[MP(t)]]σ は平

3Ψ

≡

>UΨ,

均利得項 MP(t) の語 σ の下での解釈，[[t]]A は利得項

t の文字 A の下での解釈である．
n
1 X[[t]]σ[m] ,[[MP(t)]]σ = lim inf
n→∞ n + 1m=0[[c]]A = c,8>
<1 if A |= ψ,[[1ψ ]]A =>:0 otherwise,[[t1 + t2 ]]A = [[t1 ]]A + [[t2 ]]A ,

2Ψ

≡

¬3¬Ψ,

Ψ1 WΨ2≡

Ψ1 UΨ2 ∨ 2Ψ1 ,MP(t)  c≡MP(t − c)  0.

MP(t)  c≡MP(−t)  −c.

ただし，ϕ はブール式または LTL 式とする．

3Ψ と 2Ψ は，それぞれ「いつか ϕ が成り立つ」と「常に ϕ が成り立つ」ことを表す．また Ψ1 WΨ2 は，「Ψ2 を満たすまで Ψ1 を満たし続けているが，必ずし[[t1 · t2 ]]A=[[t1 ]]A · [[t2 ]]A ,[[−t]]A=−[[t]]A .

もいつか Ψ2 を満たす必要はない（そのときには常にΨ1 を満たす）」という性質を表す．この W は，
「必ず
しもいつか Ψ2 を満たす必要はない」という until より弱い性質を表現するため，弱い until 演算子と呼ばれる．
そして，MP(t)  c は「t で規定される利得の平均値（平均利得）の下極限が閾値条件 c を満たす」，

MP(t)  c は「t で規定される利得の平均値（平均利得）の上極限が閾値条件 c を満たす（ ∈ {<, ≤}）」
ことを表す．


ここで，平均利得式で記述できる定量的性質をいく
つか紹介する．

• MP(1ψ ) > 1/3– 長期的に見て，ブール式 ψ を満たす時間（頻度）が全体の 1/3 より多い．

• MP(1ψ1 − 4 · 1ψ2 ) > 0– 長期的に見て，ブール式 ψ1 の充足頻度はブール式 ψ2 の充足頻度の 4 倍より大きい．

• MP(1ψ1 − 4 · 1ψ2 ) ≥ 0

理（accept）する．

– 長期的に見て，ブール式 ψ1 の充足頻度はブール式 ψ2 の充足頻度の 4 倍以上である，
あるいは，ψ1 と ψ2 の充足頻度はどちらも0 に収束する．
P• MP( ci · 1γi ) < 5

RabinF (r) ⇔0∃hH, Ii ∈ F. @Inf(r) ∩ H = ∅

1

A.
(5)
∧ Inf(r) ∩ I 6= ∅ただし，Inf(r) は実行 r 上に無限にしばしば現れる状態の集合である．

– それぞれの原子命題 γi がコスト ci を必要

Inf(r) = {q ∈ Q|∀i ∈ N, ∃j > i.r[j] = q}.

(6)とするアクションと対応しているとき，長期

F の要素 hH, Ii ∈ (2Q )2 は Rabin 対とも呼ばれ，直的に見たときの平均コストは 5 より小さい．

観的には，H は高々有限回しか通るべきでない状態の集合，I は無限にしばしば通るべき状態の集合を表

3. 2 全域的決定性 Rabin オートマトン

している．そして，オートマトン A に受理されるすω-オートマトンは，与えられた無限長語の受理/不べての語の集合を A の受理言語という．

受理を判定するある種の状態遷移系である．決定性

DRA が認識できる言語（ω-正規言語）のクラスは，

Rabin オートマトン（deterministic Rabin automa-

LTL 式が規定できる言語のクラスよりも真に大きい．

ton，DRA）などの ω-オートマトンは，ω-正規言語

そして，以下の定理が成り立つ．

（ω-regular language）を認識することができる．ω-定理 8 (LTL から DRA への変換). AP 上の任意の正規言語は正規言語を無限長に拡張した言語であり，

LTL 式 Ψ に対して，アルファベットが 2AP ，受理言安全性や応答性，イベント生起順序などの，システム

語が {σ ∈ (2AP )ω |σ |= Ψ}，状態数が O(2|Ψ| )（最小が満たすべき多くの機能的性質を記述できる．

上界）である DRA AΨ を構成できる．

定義 7 (全域的 DRA). 全域的 DRA A は五つ組

†
LTL から DRA への変換器としては，ltl2dstar 5[10] が開発されている．

hQ, Σ, ∆, q0 , F i である．ただし，• Q は有限の状態集合，• Σ は有限アルファベット，

3. 3 実現可能性• ∆ : Q × Σ → Q は遷移関数，

一般に，どのような環境下でも仕様を満たす（実現する）ように応答する RS が存在するとき，その仕• q0 ∈ Q は初期状態，
様は実現可能 [11] [1] [13] であるという．古典的な LTL∆(q, a) は，状態 q ∈ Q で文字 a ∈ Σ を読んだと実現可能性判定 [9] [8] [7] [16] でも，この意味での実現

きに遷移する状態を表す．オートマトンの実行は，可能性を判定している．本稿では通常の実現可能性判次々に与えられる文字を読み，遷移関係に従って状定とは異なり，「与えられた特定の確率的環境下で仕態を遷移していくことで進行する．形式的には，語様を満たすように応答する RS が存在する」という弱σ = A0 A1 ∈ Σω に対して，任意の i ∈ N に関して

い実現可能性を扱う．

Q 2• F ∈ 2(2 ) は状態集合対の集合である．

∆(qi , Ai ) = qi+1 であるような状態-文字交代無限列

定義 9 (LLTLmp 実現可能性). Φ を LLTLmp 式，Er = q0 A0 q1 A1 . . . ∈ (QΣ)ω を σ に対する実行（run）

を MDP 環境とする．

Aという．また，A 上の実行の集合を Runs

で表す．

このとき，以下の条件を満たす（有限状態）RS R

そしてオートマトンは，その実行がもつ性質により語を E の下での ϕ の（有限メモリ）実現という．

の受理/不受理を判定する．Rabin オートマトンでは，

PrR,E ({r ∈ BhvR,E |word(r) |= Φ}) = 1.

以下のように定義される Rabin 受理条件 RabinF (r)を満たすを満たす実行 r をもつ語 σ = word(r) を受(7)

また，そのような（有限メモリ）実現の集合を RealE,Φ
(ﬁn)
と書く．
そして，|RealE,Φ
(ﬁn) | 6= ∅ であるとき，Φ は E の下で†5 http://www.ltl2dstar.de/（有限メモリ）実現可能であるという．
mp

LLTL

が記述できる平均利得に関する定量的な自動合成する手法について述べる．ここで，本稿ではLLTLmp 最適合成問題を以下のように定義する．

性質は，平均利得項 MP(t) に関する閾値条件である．

定義 12 (LLTLmp 最適合成問題). Φ を LLTLmp 仕様，

そのため，MP(t) の解釈値 [[MP(t)]]word(·) を通して，

E を有限状態 MDP 環境とする．MP(t) を LLTLmp

RS と環境のふるまい上の t に関する平均利得性能を目的関数とする．

定量的に評価できる．そこで本稿では，RS の性能を

このとき，E の下で Φ が，その解釈値の期待値として定義する．

• 実現不能ならば，“実現不能”，

定義 10 (RS の性能). R を MDP RS，E を MDP 環• 実現可能だが有限メモリ実現不能ならば，“有限mp境，MP(t) を LLTL

平均利得項とする．

メモリ実現不能”，

このとき，以下のように定義される値 PfmER (MP(t))
を E のもとでの R の MP(t) に関する性能値（per-• 有限メモリ実現可能ならば，MP(t) に関して (ε-)
最適な MDP RS R ∈ RealE,Φ
ﬁnを出力する問題を LLTLmp 最適合成問題という． 

formance value）という．
PfmER (MP(t)) = EPrR,E [[[MP(t)]]word(·) ].

(8)

実現可能性判定や合成において，RS と環境のふる

ただし，期待値 E は標本空間 Ω とその上の確率測度

まいは二人交代手番ゲームとしてしばしば形式化さ

Pr : Ω → [0, 1]，確率変数 X : Ω → R に対して，以れる [9] [8] [7] [4] [16]．そのゲームでは，RS 側プレイヤ

下のように定義される．
Z
EPr [X] =と環境側プレイヤが交互に行動（2OAP /2IAP ）を選

X(x) · Pr(x)dx.

x∈Ω

(9)

択することでゲームが進行する．また，ゲームの構造

と勝利条件は仕様を反映しており，ゲームの進行（プそして，E の下での Φ を実現する RS のふるまレイ）と対応する RS と環境のふるまいが仕様を満たい上の MP(t) に関する性能上限値（最適性能値）

すときに RS 側プレイヤは勝利する．そして，そのよSupPfmE,Φ
(ﬁn) (MP(t)) は，以下のように定義できる．
sup
SupPfmE,Φ
{PfmER (MP(t))}.
(ﬁn) (MP(t)) =E,Φ
R0 ∈Real(fin)うなゲーム上で RS 側プレイヤが取るべき行動方針(10)
この上限値を与える RS を合成できることが望まし
いが，一般には有限状態 RS ではその性能上限値を実現できない．そこで，そのような場合には，この性（戦略）を検証することで，実現可能性判定及び合成が行われる．
本章では，LLTLmp 実現可能性判定及び最適合成
問題を，環境や仕様，目的関数を反映したゲーム上の問題に帰着できることを示す．

能上限との差がある許容誤差以内となる性能を持つ，

4. 1 準備

すなわち，ε-最適な RS に注目することとする．
定義 11 (RS の ε-最適性). Φ を LLTLmp 式，MP(t)を LLTLmp 平均利得項，E を MDP 環境，ε ≥ 0 を
許容絶対誤差とする．
このとき，以下の条件を満たす（有限メモリ）RSR ∈ RealE,Φ
(ﬁn) は MP(t) に関して（有限メモリ）ε-最適であるという．

PfmER (MP(t)) + ε ≥ SupPfmE,Φ
(ﬁn) (MP(t)).

(11)


4 LLTLmp 最適合成問題
与えられた確率的環境の下で LLTLmp 仕様を実現
し，かつ，LLTLmp 目的関数に関して最適な RS を

本節では，LLTLmp 最適合成に利用するゲームとそれに関連した概念の定義を与える．

4. 1. 1 平均利得 Rabin ゲーム
LTL の表現力は DRA よりも小さいため，Rabin
受理条件を勝利条件としてもつ Rabin ゲームなどを利用することで LTL 実現可能性判定/合成を行うことができる．しかしながら，LLTLmp で記述できる
平均利得に関する定量的性質は，DRA などが捉えることができる ω-正規性質とは全く異なる．そのため，ゲームベースのアプローチで LLTLmp 実現可能性判
定/最適合成を行うには，平均利得に関する性質を勝利条件として反映できるゲームが必要がある．

本稿では，Rabin 条件の他に平均利得受理条件を勝利条件としてもつゲーム，多閾値平均利得 Rabin
ゲーム（MPRG）を用いる．
定義 13 (MPRG). MPRG G は，十組 hQ0 , Q1 , Σ0 , Σ1 ,

∆0 , ∆1 , q0 , w, F, Gi である．ただし，• Qn （n ∈ {0, 1}）はプレイヤ n が遷移先を選択する状態の有限集合，• ∆n : Qn × Σn → Qn̄ （n̄ 6= n）はプレイヤ n が遷移先を決定する状態の遷移関数，

させることを意図している．G の要素の重みインデックス集合対 hJ, Ki ∈ (2{1,...,d} )2 に関して，J は平均

以下のように定義される条件 MPG (r) を平均利得受
理条件という．

MPG (ρ) ⇔• q0 ∈ Q0 は初期状態，• w : ((Q0 × Σ0 ) ∪ (Q1 × Σ1 )) → Rd は遷移に対して d 次元実数ベクトルを与える重み関数，• G∈ 2

この下極限は，ある平均利得項 MP(t) の解釈と対応ければならない次元のインデックスを表す．そして，– Σ0 ∩ Σ1 = ∅,は Rabin 対の集合，(2{1,...,d} )2(12)デックス，K は平均利得の下極限が 0 より大きくな• Σn はプレイヤ n のアクション集合，

Q0 ∪Q1 2)平均利得の下極限を mpw
i (ρ) で表す．
n
X
1
w
·
w[i](qj , Aj ).
mpi (ρ) = lim inf
n→∞ n + 1
j=0

利得の下極限が 0 以上でなければならない次元のイン– Q0 ∩ Q1 = ∅,• F ∈ 2(2

ρ = q0 A0 q1 A1 . . . ∈ PlaysG に対して，i 番目次元の0∀j ∈ Ji .mpw
j (ρ) ≥ 0

1

A . (13)∃hJi , Ki i ∈ G. @∧∀k ∈ Ki .mpw
k (ρ) > 0
そして，MPRG G でのプレイヤ 0 の勝利条件 WinG
は以下のように定義される．

は重みインデックス集合対のWinG (·)=

RabinF (·) ∧ MPG (·).

(14)



つまり，Rabin 条件と平均利得受理条件を同時に満以降では，Q0 ∪ Q1 を Q，Σ0 ∪ Σ1 を Σ，∆0 ∪ ∆1

たすプレイではプレイヤ 0 が勝利し，そうでないプ

集合．

を ∆ で表し，G も単に七つ組 hQ, Σ, ∆, q0 , w, F, Giと略記する．

レイではプレイヤ 1 が勝利する．

4. 1. 2 戦略

オートマトンの場合に似て，ゲームの実行は，プ

二人交代手番ゲームのプレイ中，両プレイヤは自身

レイヤ 0 とプレイヤ 1 から交互に与えられるアクが勝利するための行動を選択していく．その行動方針

ション（文字）をもとに遷移関係に従って状態を遷のことを戦略（strategy）という．形式的には，以下移 し て い く こ と で 進 行 す る ．つ ま り，ア ク ションのように定義される．

列（語）σ = A0 A1 ∈ (Σ0 Σ1 ) ⊂ Σω に対して，∀i ∈定義 14 (戦略). G = hQ, Σ, ∆, q0 , w, F, Gi を MPRG

N.∆(qi , Ai ) = qi+1 であるような状態-アクション交代
無限列 ρ = q0 A0 q1 A1 . . . ∈ (Q0 Σ1 Q1 Σ1 ) ⊂ (QΣ)ω
が σ に対する実行である．ゲームでは，これをプレイ（play）と呼び，G 上のプレイの集合を PlaysG で表す．なお，初期状態がプレイヤ 0 が遷移先を決定する状態であるのは，RS と環境のふるまいと対応させとする．
プ レ イ ヤ n（n ∈ {0, 1}）の 戦 略 は ，三 つ 組

hM, µn , minit i である．ただし，• M はメモリ空間，• µn : Qn × M × Σn → ([0, 1] × M ) は出力確率関数，

るためである．つまり，実現可能性判定及び合成のた• 初期メモリ minit ∈ M は初期メモリである．

めのゲーム上では，プレイヤ 0 が RS 側プレイヤ，プまた，プレイヤ n が遷移先を決定する任意の状態

レイヤ 1 が環境側プレイヤとなる．

q ∈ Qn ，とメモリ状態 m ∈ Mn について以下の条件

重 み 関 数 w が 与 え る 実 数 ベ ク ト ル x ∈ Rd はそれぞれの遷移によって発生する d 種類の利得を表す．ここで，ある i 番目次元に関する重み関数を w[i] で表す．つまり，w(q, A) = hx1 , . . . , xd i に対して，w[i](q, A) = xi とする．そして，プレイが成り立っているものとする．
X
Prob(µn (q, m, A)) = 1.
A∈Σn

た だ し ，µn (q, m, A)

=

(15)

hp, m0 i に 関 し て ，Prob(µn (q, m, A)) は p を，Mem(µn (q, m, A)) は m0を与える関数である．

ている．そのような特定の相手プレイヤの戦略に対し

そして，|M | = 1 のときメモリレス，|M | < ∞ のとき有限メモリ，|M | = ∞ のとき無限メモリである



という．

なお，以降では，メモリレス戦略 h{minit }, µn , minit iて，ほとんど必ず勝利する戦略を対抗戦略（counter

strategy）という．
定義 15 (対抗戦略). G を MPRG，Str1 をプレイヤ

1 の戦略とする．

を 単 に µn と 書 く こ と と す る ．ま た そ の と き ，

このとき，以下の条件を満たすプレイヤ 0 の（有µn (q, minit , A) = hp, minit i も単に µn (q, A) = p と限メモリ/メモリレス）戦略 Str0 を G 上の Str1 に対する．

する（有限メモリ/メモリレス）対抗戦略という．

両 プ レ イ ヤ の 戦 略 が 固 定 さ れ て い る と き ，プG

レ イ 集 合 Plays

上の確率測度は一意に定まる．

RS と 環 境 の ふ る ま い と 同 様 に ，奇 数 長 プ レ イ
ρﬁn = q0 A0 . . . qn−1 An−1 qn の筒集合は以下のように(18)

また，そのような（有限メモリ/メモリレス）対抗戦
1
略の集合を CntG,Str(ﬁn/ml) と書く．



RS と環境のふるまいと同様に，ゲーム上のプレイの性能もある次元 i の平均利得 mpw
i (·) を通して定量定義できる．
G

PrG,Str0 ,Str1 ({ρ ∈ PlaysG |WinG (ρ)}) = 1.

0

G

0

Cyl (ρﬁn ) = {ρ ∈ Plays |ρﬁn = pref n (ρ )}. (16)

的に評価できる．ただし本稿では，性能の指標を，最そして，ゲーム G 上で，プレイヤ 0 が戦略 Str0 =も大きいインデックスの次元の重みに関する平均利0hM, µ0 , m0 i，プレイヤ 1 が戦略 Str1 = hM , µ1 , m00 i

得 mpw
d (·) に固定する．そして，RS の性能と同様に，に従うとき，CylG (ρﬁn ) に含まれるプレイの生起確率

対抗戦略の性能は平均利得 mpw
d (·) の期待値として定は以下のように与えられる．

義する．

G,Str0 ,Str1(CylG (ρﬁn )) =Pr8>>1
if n = 0,
>
>
>
>
>
>
>
PrG,Str0 ,Str1 (CylG (ρ0ﬁn )) · µ0 (qn−1 , mi , An−1 )>><if n = 2i + 1,
>
>
>
>
>
>
PrG,Str0 ,Str1 (CylG (ρ0ﬁn )) · µ1 (qn−1 , m0i , An−1 )
>
>
>
>
>
:
if n = 2i + 2.
(17)

定義 16 (対抗戦略の性能). G を MPRG，Str0 をプ

ただし，ρﬁn = ρ0ﬁn An−1 qn であり，また，任意の1 < j ≤ i について，• µ0 (q2(j−1) , mj−1 , A2(j−1) ) = hp2(j−1) , mj i，•µ1 (q2(j−1)+1 , m0j−1 , A2(j−1)+1 ) =hp2(j−1)+1 , m0j i.

レイヤ 1 の戦略，Str1 をプレイヤ 1 の戦略とする．
このとき，以下のように定義される値 PfmG,Str0 ,Str1を，Str1 に対する Str0 の性能値という．
1= EPrG,Str0 ,Str1 [mpwPfmG,Strd (·)].
Str0

(19)


式 (10) と同様に，プレイヤ 1 の戦略 Str1 に対する
（有限メモリ/メモリレス）対抗戦略の性能上限，すな
1
わち，最適性能値 SupPfmG,Str(ﬁn/ml) は以下のように定義できる．
1
SupPfmG,Str(ﬁn/ml) =supG,Str1Str00 ∈Cnt(fin/ml)

1{PfmG,Str}. (20)Str00

RS と同様に．一般に，この上限値を与える有限メ

なお，RS と環境のふるまいと同様に，戦略 Str0 とモリ（メモリレス）戦略が存在するとは限らない．そStr1 がどちらも有限メモリであるとき，そのほとんのような場合には，やはり ε-最適な戦略に注目する．

どすべてのプレイ ρ について，ρ 上の状態 q やアク

定義 17 (ε-最適対抗戦略). G を MPRG，Str1 をプ

ション A の出現頻度は収束する．

レイヤ 1 の戦略とする．

4. 1. 3 対抗戦略

このとき，以下の条件を満たすような，Str1 に対する

本研究では，特定の確率的環境のもとで仕様を満

1（有限メモリ/メモリレス）対抗戦略 Str0 ∈ CntG,Str(ﬁn/ml)

たす RS に注目している．ゲーム上では，そのようなを，（有限メモリ/メモリレス）ε-最適であるという．

RS は，環境に対応するプレイヤ 1 の戦略に対して，
ほとんど必ず勝利できるプレイヤ 0 の戦略と対応し

1
1
PfmG,Str+ ε ≥ SupPfmG,Str
Str0(ﬁn/ml) .

(21)
4. 2 LLTLmp 最適合成問題から MPRG 対抗戦

RunsAΨ に関して，以下の性質が成り立つ．

略合成問題への帰着
本節では，LLTL

mp

最適合成問題を MPRG 最適対抗戦略合成問題に帰着できることを示す．

Φ = Ψ ∧ Θ を LLTL
目的関数，E = hS, 2

mp

OAP

AΨ = hQ, 2

AP仕様，MP(t) を平均利得

,2

IAP

, P, s0 i を MDP 環境，, ∆, q0 , F i を LTL 式 Ψ と等価な全域

的 DRA とする．ただし，Θ は n 種類の原子平均利得式 θm = MP(tm ) m 0（1 ≤ m ≤ n）の連言節のW V
選言からなり，Θ = i θm ∈Ci θm であると仮定す
る（それぞれの Ci について Ci ⊆ {θ1 , . . . , θn }）．
E
ここで以下のような MPRG GΦ,MP(t)= hQ0 , 2AP ,∆0 , hq0 , s0 i, w, F 0 , Gi を考える．
• Q00 = Q × S,
• Q01 = Q × S × 2OAP ,• ∆00 (hq, si, a) = hq, s, ai,• ∆01 (hq, s, ai, b) = h∆(q, a∪b), State(P (s, a, b))i,0• w[m](q8 , A) =>2 · [[tm ]]a∪b
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
<

if 1 ≤ m ≤ n,
q 0 = hq, s, ai ∈ Q1
and A = b ∈ 2IAP ,2 · [[t]]a∪b
if m = n + 1,
>
>
>
>
>
>
q 0 = hq, s, ai ∈ Q1
>
>
>
>
>
>
and A = b ∈ 2IAP ,
>
>
>
>
>
:
0
otherwise,0• F = {hHi × S, Ii × Si|hHi , Ii i ∈ F },S
• G(·) = i hJi , Ki i．ただし，– Ji = {j|∃θj ∈ Ci .j は ≥},– Ki = {k|∃θk ∈ Ci .k は >}.
E
GΦ,MP(t)と AΨ はどちらも全域的かつ決定的であり，また，E も入力 a ∈ 2OAP に対して出力 b ∈ 2IAP を応答した際の遷移先の状態は一意に決まっている．そEのため，GΦ,MP(t)の任意のプレイρ = hq0 , s0 i . . . hqi , si iai hqi , si , ai ibi hqi+1 , si+1 i . . .
は，AΨ の以下のような実行rρ = q0 . . . qi (ai ∪ bi )qi+1 . . .
と一対一対応する．
そしてこのとき，以下の補題が成り立つ．
補題 18.

と，全域的 DRA AΨ のそれに対応する実行 rρ ∈GE
E
MPRG GΦ,MP(t)のプレイ ρ ∈ Plays Φ,MP(t)(a). RabinF 0 (ρ) ⇔ word(rρ ) |= Ψ,(b). MPG (ρ) ⇔ word(rρ ) |= Θ,(c). mpw
n+1 (ρ) = [[MP(t)]]word(rρ ) .

証明. (a): F 0 の定義から RabinF 0 (ρ) ⇔ RabinF (rρ )である．また，AΨ の構成から明らかに RabinF (rρ )⇔ word(rρ ) |= Ψ．よって成り立つ．
(b): G の定義から，1 ≤ m ≤ n である m について以下を満たすことを示せばよい．

mpw
m (ρ)

=

[[MP(tm )]]word(rρ ) .

(22)

E
E
GΦ,MP(t)の定義から，GΦ,MP(t)の 2 ステップが AΨ の

1 ステップに対応している．そして，w の定義から，
E
GΦ,MP(t)の 2 ステップのうちの前のステップは重み0，後のステップの重みは AΨ の 1 ステップの利得の倍である．よって，式 (22) は明らかに成り立つ．

(c): (b) と同様．
E
そして，GΦ,MP(t)上では，環境 E は以下のようなプレイヤ 1 のメモリレス戦略 µE1 と見なせる．

µE1 (hq, s, ai, b) = Prob(P (s, a, b)).

(23)

E
一方で，GΦ,MP(t)上のプレイヤ 0 の戦略 Str0hM, µ0 , minit i は次のような RS R
R

Str0

=

Str0

=

と見なせる．

h(Q01 ∪ {hq0 , s0 i}) × M, 2IAP , 2OAP ,P 0 , hhq0 , s0 i, minit ii.

(24)

0

ただし，遷移確率関数 P は以下の制約を満たす．
0
P 0 (hq
8 , mi, A, B) =>>hProb(µ0 (q 0 , m, B)),
>
>
>
>
>
>
>
h∆0 (q 0 , B), Mem(µ0 (q 0 , m, B))ii
>
>
>
>
>
<
if q 0 = hq0 , s0 i and m = minit ,>>hProb(µ0 (q 00 , m, B)),
>
>
>
>
>
>
> h∆0 (q 00 , B), Mem(µ0 (q 00 , m, B))ii
>
>
>
>
>
:
if q 0 ∈ Q1 and q 00 = ∆1 (q 0 , A).
ここで，以下の補題が成り立つ．

(25)

補題 19 (対抗戦略から RS への変換). E を有限状態

MDP 環境，Φ を LLTLmp 仕様，MP(t) を LLTLmp
目的関数とする．
E
このとき，µ0 が MPRG GΦ,MP(t)上のプレイヤ 1

のメモリレス戦略 µE1 に対するプレイヤ 0 の（有限メモリ）対抗戦略ならば，Rµ0

は E のもとで Φ をE
GΦ,MP(t),µE1上の最適な対抗戦略を合成する問題に帰着できる．

実現する有限メモリ RS であり，Pfmµ0=

5 MPRG 最適対抗戦略合成の概略

PfmERµ0 (MP(t)) を満たす．



前章では，LLTLmp 最適合成問題を MPRG 最適対抗戦略合成問題に帰着できることを示した．本章で証明. 本稿では省略．

は，MPRG 最適対抗戦略合成手法の概略について述

これより，以下の定理が成り立つ．

べる．

最適合成問題から MPRG 最適対

まず，MPRG 最適対抗戦略合成に関する基本的な抗戦略合成問題への帰着). E を有限状態 MDP 環境，

アイディアを示す．その後，MPRG 最適対抗戦略合Φ を LLTLmp 仕様，MP(t) を LLTLmp 目的関数と成手続きの概略を示す．

mp

定理 20 (LLTL

そして，6 章で MPRG 最適対抗戦略合成手続きでする．
このとき，E のもとで Φ を実現する（有限状態）

MDP RS R ∈ RealE,Φ
(ﬁn) が存在するならば，かつそEのときに限り，MPRG GΦ,MP(t)上のプレイヤ 1 のメモリレス戦略 µE1 に対する（メモリレス）対抗戦略
G,µE
1用いる部分手続きについて説明し，7 章で具体的な

MPRG 最適対抗戦略合成手続きを与える．
5. 1 基本的なアイディア
ゲーム G = hQ, Σ, ∆, q0 , w, F, Gi においてプレイ

Str0 ∈ Cnt(ml) が存在する
また，その R が LLTLmp 目的関数 MP(t) に関し

ヤ 1 がメモリレス戦略 µ1 に従うと仮定した場合，て (ε)-最適であるならば，かつそのときに限り，µ0

ゲームは MDP と見なすこともできる．このとき，ほとんどすべてのプレイ ρ について，µ1 で規定されるも (ε)-最適である．

確率的選択に関して閉じた，ある強連結な部分グラフ
証明. 補題 19 と補題 21，補題 22 から成り立つ．

hQ0 , ∆0 i ⊆ hQ, ∆i の状態集合のみを無限にしばしば補題 21 (RS から対抗戦略への変換). E を有限状態訪れる，すなわち，Inf(ρ) = Q0 となるはずである．

MDP 環境，Φ を LLTLmp 仕様，MP(t) を LLTLmp

そのような確率的選択に関して閉じた強連結な部分グ

目的関数とする．

ラフを終端成分（end component，EC）と呼ぶ．形

このとき，E のもとで Φ を実現する（有限状態）

MDP RS R が 存 在 す る な ら ば ，MPRG

E
GΦ,MP(t)上 の プ レ イ ヤ 1 の メ モ リ レ ス 戦 略 µE1 に 対 し て ，EGΦ,MP(t),µE
1

PfmER (MP(t)) = PfmStr0となる（有限メモ

G,µEリ）対抗戦略 Str0 ∈ Cnt(ﬁn)1 が存在する．



式的には，これは以下のように定義される．
定義 23 (EC). G = hQ, Σ, ∆, q0 , w, F, Gi を MPRG，µ1 を G 上のプレイヤ 1 のメモリレス戦略とする．
このとき，以下の条件を満たす非空かつ強連結な部分グラフ hQ0 , ∆0 i を，G 上の µ1 に対する EC という．

証明. 本稿では省略する．

• Q0n ⊆ Qn ,補題 22 (有限メモリ対抗戦略のメモリレス性). 任意• ∆0n : Q0n × Σn 7→ Q0n̄ （⊆ ∆n ）,S• Q00 = q∈Q0 {∆1 (q, b)|µ1 (q, b) > 0}.

の MPRA G とその上のプレイヤ 1 のメモリレス戦略
1が存µ1 に対して有限メモリ対抗戦略 Str0 ∈ CntG,µ
ﬁn
G,µ1
G,µ1
在するならば，PfmStr0 = Pfmµ0 となるメモリレ1が存在する．
ス対抗戦略 µ0 ∈ CntG,µ
ml





ほとんどすべてのプレイ ρ について，Inf(ρ) があということは，µ1 に対する対抗戦略 Str0 が定理 20 より，定義 9 の弱い意味での LLTLmp 実現
可能性判定問題や LLTL

EC，MEC）と呼ぶ．

る EC E = hQ0 , ∆0 i の状態集合 Q0 と一致している

証明. 本稿では省略する．

mp1

また，EC の中で極大なものを極大 EC（maximal

最適合成問題は MPRG

(a). ある EC E 上で，WinG (ρ) かつ Inf(ρ) = Q0

とするための局所的戦略とである．そのような到達戦略を合成する問題は MDP(b). そのような局所的戦略をもつ EC へ誘導する
戦略の最大到達確率問題と類似の問題であり，プレイヤ 1の戦略がメモリレス戦略ならば容易に構成できる．

の組合わせにより構成されていることを意味している．
そこでまず，(a) の戦略について考える．この戦略は，別の言い方をすれば，初期状態を E の任意の状
態 q00 ∈ Q00 に変更したゲーム Gq00 上の µ1 に対して，
以下の条件を満たす対抗戦略
StrE
0 である．91
08
Gq 0 ˛<=˛Eρ ∈ Plays 0
G 0 ,Str ,µ1@
A=1
Pr q0 0S
: ∀i.Q0 =;j∈N ρ[2(i + j)](26)
そのような戦略 StrE
0 を E 上の局所対抗戦略（local

counter strategy）といい，また，E のことを対抗
EC（counter EC，CEC）と呼ぶ．特に，StrE
0 が有限メモリ戦略であるとき，StrE
0 をメモリレス局所対
抗戦略，E をメモリレス CEC（memoryless CEC，

MLCEC）という．ここで，(ML)CEC 上の（メモリG,µ1 ,Eレス）局所対抗戦略の集合を Cnt(ml)と書くこととする．また，そのようなの中で ε-最適な戦略 StrE
0 を

E 上の（メモリレス）局所 (ε-) 最適対抗戦略といい，
E

そのときの性能値 PfmG,Str0 ,Str1 を（メモリレス）局
所 ε-最適性能値という．
E

PfmG,Str0 ,Str1 + ε ≥supG,µ ,E

0{PfmG,Str0 ,µ1 }.

Str00 ∈Cnt(ml)1(27)

5. 2 MPRG 最適対抗戦略合成手続きの概略
MPRG 上でプレイヤ 1 が µ1 に対する最適対抗戦
略を合成する手続きの概略は以下の通りである．

i. ゲームのグラフを MEC 分解する．
ii. それぞれの MEC が CEC を含むか判定する．
iii. 初期状態 q0 から CEC を含む MEC への最大到達確率を計算する．

• もしその最大到達確率が 1 でなければ，対抗戦略は存在しない．

iv. それぞれの MEC が MLCEC を含むかを判定する．

• 同時に，MLCEC の中で最大の局所最適性
能値を与える MLCEC を探索し，そのメモ
リレス最適対抗戦略を計算する．

v. 「それぞれの MLCEC 上のメモリレス局所最適対抗戦略」が与える性能値を考慮して，それぞれの状態で最大期待性能値を計算する．

• ただし，MLCEC に含まれる状態への最大到達確率が 1 でない状態の最大期待性能値
は −∞ とする．

また，CEC に関しては，その状態集合 Q0 は少な• もし q0 での最大期待性能値が −∞ である

くとも以下の条件を満たしているはずである．
`´∃hHi , Ii i ∈ F. Q0 ∩ Hi = ∅ ∧ Q0 ∩ Ii 6= ∅(28)

（つまり，MLCEC への最大到達確率が 1 でこの条件 (28) を満たす EC を Rabin EC（REC），

ない）ならば，メモリレス対抗戦略は存在しない．

その中で極大のものを極大 REC（maximal REC，vi. 「それぞれの MLCEC 上のメモリレス局所最MREC）と呼ぶ．ゲームは状態集合が有限であり，ま適対抗戦略」と「遷移先が最大期待性能値が最た，EC が REC であるか否かはグラフ構造から判定も高い状態となるようにアクションを選ぶ戦略」

できるため，ゲーム上の REC はすべて列挙することを組み合わせ，ゲーム全体の上のメモリレス最適ができる．そして，それぞれの REC についてメモリ対抗戦略を構成する．

レス局所対抗戦略の存在判定及び最適化を行うこと
で，(a) の戦略を合成できる．
次に，(b) の戦略について考える．これは (a) の戦

6 MPRG 最適対抗戦略合成のための部分手続き

略をもつ MLCEC へ到達させることを目的とした戦本章では，7 章で与える MPRG 最適対抗戦略合成

略である．また，その中で最適な戦略は，到達させる

手続きで用いる主要な部分手続きについて説明する．

MLCEC 上の最適性能値の期待値を最大とする戦略

これらの部分手続きは，「REC が (ML)CEC であるかを判定する手続き」や「最大到達確率を計算する手続

き」などである．

と零ベクトルの対を返す．

なお，ゲーム上の通常の MEC 分解手続きは，MDP∗ 最適値は，opt = max のときには最大の MEC 分解手続き [5] と同様であり，多項式時間で値（最大が定義できない場合は上限値），

計算できる．そのため，本稿では手続きの詳細は省略

opt = min のときには最小値（最小がするが，以下の手続きが利用できるものとする．

定義できない場合は下限値）である．

00

本稿では，線形制約や線形目的関数はベクトルや行列– MPRG G 上のプレイヤ 1 のメモリレス戦

を用いて表現する．そのため，目的関数は Obj は行• DecompMEC(G, hQ , ∆ i, µ1 )略 µ1 に対する，部分グラフ hQ0 , ∆0 i に含まれる MEC の集合を返す．

ベクトルとして与えられる．
なお，本稿で SolveLCSP と SolveLPPopt の入力

また，本章で与える部分手続きの中では，しばしばとなるすべての線形制約 Cnst は，それらを満たす解

線形制約充足可能性問題 (（linear constraint satisfac-

ベクトルは零ベクトルではない．そのため，零ベクト

tion problem，LCSP）や線形計画問題（LP problem，
LPP）を解く．この LCSP は，Z3†6 や Yices†7 など

ルが返されたならば，かつそのときに限り，線形制約の SMT（satisﬁable modulo theories）ソルバを利用して多項式時間で解くことができる．また，LPP
も，GLPK†8 や CPLEX†9 などの LP ソルバや MAT-

LAB†10 や Scilab†11 ，Mathematica†12 などの汎用数
値計算ソフトェアを利用して多項式時間で解くことができる．そこで，以下のような手続きも利用できるものとする．

• SolveLCSP(Cnst)– 線形制約 Cnst : (R≥0 )n → B を満たす n 次
元非負実数解ベクトルを返す．

∗ ただし，Cnst が充足不能のとき，零ベ
クトル（すべての要素が 0 のベクトル）を返す．

• SolveLPPopt (Obj, Cnst)– 線形制約 Cnst : (R≥0 )n → B に従う線形目
的関数 Obj : (R≥0 )n → R の最適値とそれが充足不能である．
注意 24 (ベクトルと行列の表記法). 本稿では，単にベクトルと言う場合には列ベクトルを指し，行ベクト
ルは T を付けて表記する．また，0 は零ベクトル，uは単位ベクトル（すべての要素が 1 のベクトル）を表す．これらのベクトルのサイズは，他の行列やベク
トルのサイズから一意に定まる場合には省略する．
そして本稿では，状態集合 Q の大きさ |Q| などを行/列のサイズとする行列やベクトルを主に用いる．
そのような場合，行列やベクトルの行/列にはその集合のそれぞれの要素が対応しているものとする．また，その要素で行/列のインデックスを指定する．例えば，|Q| 次元（Q は状態集合）のベクトル x の状態 q に対応する要素は x[q]，|Q| 行 |J| 列（J ⊆ {1, . . . , d} は
インデックスの集合）の行列 A の状態 q に対応する
行のインデックス j が対応する列の要素は A[q, j] と表記する．

を与える n 次元非負実数解ベクトルの対を返す．

∗ ただし，Cnst が充足不能のとき，−∞†6 http://research.microsoft.com/en-us/um/
redmond/projects/z3/†7 http://yices.csl.sri.com/†8 http://www.gnu.org/software/glpk/†9 http://www-01.ibm.com/software/integration/
optimization/cplex-optimization-studio/†10 http://www.mathworks.com/products/matlab/†11 http://www.scilab.org/†12 http://www.wolfram.com/mathematica



6. 1 MREC 分解手続き DecompMREC
この手続きは，MPRG G 上でプレイヤ 1 がメモ
リレス戦略 µ1 に従うときに，与えられた MEC に含まれる MREC の集合を計算する手続きである．

(ML)CEC は必ず REC であるため，その中で極大なものと計算するために用いる．これは，通常の MEC
分解を用いる以下のような手続きとして与えられる．
手続き 25 (MREC 分解手続き DecompMREC).

• 入力:

– MPRG G = hQ, 2AP , ∆, q0 , w, F, Giにより解くことができる．

– G 上のプレイヤ 1 のメモリレス戦略 µ1

手続き 27 (最大到達確率計算手続き SolveReach-– G 上の MEC hQ0 , ∆0 i ⊆ hQ, ∆iProb).

• 出力:

• 入力:

– hQ0 , ∆0 i 上の MREC の集合
1: M := ∅;// MREC の集合

2: for all hH, Ii ∈ F do// それぞれの Rabin 対について
0

M := DecompMEC(G, hQ0 \ H, ∆0 i, µ1 );3:// 態を取り除いて MEC 分解を行う
000

for all E = hQ , ∆ i ∈ M such that

4:

0

• 出力:
0

1 ,Q
pG,µ
を与える |Q| 次元ベクトル p
q
0

1 ,Q
);
1: return SolveLPPmin (uT , LCQ,∆,µreach
0Q00 ∩ I 6= ∅) then// 得られた EC が極大な REC であるとき
M := (M \ {E 0 ∈ M |E 0 ⊆ E}) ∪ E;

6:

– G の部分状態集合 Q0 ⊆ Q

1 ,Q
ここで，LCQ,∆,µ: (R≥0 )|Q| → B は以下のよう
reach

0

(∀E ∈ M.E 6⊆ E and5:– G 上のプレイヤ 1 のメモリレス戦略 µ1– それぞれの状態から Q0 への最大到達確率// 高々有限回しか通るべきでない状
00– MPRG G = hQ, 2AP , ∆, q0 , w, F, Giに定義される線形制約である．
0pBQ,∆,µ1 ,Q0
Q,∆0
B
LCreach(p) ⇔ @ Anc p
1 ,µ1
AQ,∆
p
pc
0

0

≥

bQ,Q
reach ,

≥

0,

≥

0

1

C
C . (30)
A// M から E に含まれる EC をQ,∆0
た だ し ，bQ,Q
はreach は |Q| 次 元 ベ ク ト ル ，Anc// 取り除いた後で E を加える|{hq, q 0 i ∈ Q0 × Q1 |∆0 (q, a) = q 0 }| × |Q| 行 列 ，
1 ,,µ1
AQ,∆
は |Q1 | × |Q| 行列であり，以下のように定pc

end for

義される．

7: end for

8: return M ;0bQ,Qreach [q]

=

0
AQ,∆
[hq, q 0 i, q 00 ]nc=

1 ,,µ1AQ,∆[q, q 0 ]pc=

補題 26 (手続き 25 の正当性). 手続き 25 の結果得られる状態の集合 M は，MPRG G の MEC hQ0 , ∆0 i

上の MREC の集合である．
証明. 自明．

6. 2 最大到達確率計算手続き SolveReachProb
この手続きは，MPRG G 上でプレイヤ 1 がメモ
リレス戦略 µ1 に従っているときに，それぞれの状態

q ∈ Q に関して，状態部分集合 Q0 ⊆ Q への最大到達確率（プレイヤ 0 が適切に遷移先を選ぶことで得られる到達確率の最大値）を計算する手続きである．
01 ,Qq から Q0 への最大到達確率 pG,µは，厳密には以q

下のように定義される．
0

1 ,Q
pG,µ
= max{PrGq ,Str0 ,µ1 ({ρ|∃i.ρ[2i] ∈ Q0 })}.
q

Str0

(29)
この最大到達確率問題は MDP の最大到達確率問題と同値であり，以下のような LPP に帰着する手続き

8><1

if q ∈ Q0 ,(31)>
:0 otherwise.
8>>1
if q 00 = q ∈ Q0 ,>><−1 if q 00 = q 0 ∈ Q1 ,(32)
>
>
>
>
:0
otherwise.
8>>1 if q 0 = q ∈ Q1 ,
>
>
>
>
X
>
>
>
µ1 (q, b)<−hq,b,q 0 i∈∆1
(33)
>
>
0
>
>
if
q
∈
Q
,
0
>
>
>
>
>
:0 otherwise.
0
直観的には，AQ,∆
p ≥ 0 の hq, q 0 i 行に関する線nc

形制約は，q ∈ Q0 から 1 回の遷移で到達できる状態

q 0 ∈ Q1 について，「q から Q0 への最大到達確率」が「q 0 から Q0 への最大到達確率」以上であることを表している．これは，プレイヤ 0 が遷移先を自由に選択で
1 ,,µ1
きることに由来している．一方で，AQ,∆p≥0pcの q 行に関する線形制約は，「q ∈ Q1 から Q0 への最大到達確率」が「プレイヤ 0 が Q0 へ到達させるために最適の選択を行う場合の到達確率の期待値」であることを表している．これは，プレイヤ 1 が µ1 で規定された確率的選択によって遷移先を決定していることに由来している．
補題 28 (手続き 27 の正当性). 手続き 27 が返す解ベ
クトル p の各要素 p[q] は，q から Q0 への最大到達01 ,Q確率 pG,µである．
q

証明. 自明．

6. 3 CEC 判定手続き SolveCEC
こ の 手 続 き は ，MPRG G 上 で プ レ イ ヤ 1 が メモリレス戦略 µ1 に従うときに，与えられた REC

E = hQ0 , ∆0 i が CEC であるかを判定する手続きである．具体的には，以下のような LCSP に帰着する手続きとして与えられる．
手続き 29 (CEC 判定手続き SolveCEC).

に定義される線形制約である．
0
uT x
B
B AE xB
cyc
B E,µµ1 ,E,w,g
1
LCCEC(x) ⇔ BA
B str x
B E,w,JBA@ mp,≥ x

0,

1

C
0,C
C
C
= 0,C
C (. 34)
C≥ 0,C
A
AE,w,K> 0
mp,> xE,µ100
は |∆01 |×|∆0 |ただし，AEcyc は |Q |×|∆ | 行列，Astr
=

E,w,K
0
0
行列，AE,w,J
mp,≥ は |J|×|∆ | 行列，Amp,> は |K|×|∆ |行列であり，以下のように定義される．
8>>
1
if q = q 0 ,
>
>
<
0
00
AE
=
−1 if q = q 00 , (35)cyc [q, hq , A, q i]
>
>
>
>
:0
otherwise,
0
00
000
1
AE,µ
str [hq,
8b, q i, hq , A, q i] =>1>
if q = q 00 ∧ b = A,>><−µ1 (q, b) if q = q 000 ,
>
>
>
>
:0
otherwise,(36)

0
AE,w,J
mp,> [j, hq, A, q i]=w[j](q, A),(37)

0AE,w,K
mp,> [k, hq, A, q i]=w[k](q, A).

(38)


• 入力:
– MPRG G = hQ, 2AP, ∆, q0 , w, F, Gi– G 上のプレイヤ 1 のメモリレス戦略 µ1 ，
– G 上の EC E = hQ0 , ∆0 i，• 出力:– E 上の局所対抗戦略を表現した |∆0 | 次元の非負実数ベクトル x∗ ただし，E が CEC でないときには零ベクトル 0 を返す．

1: for all g = hJ, Ki ∈ G do
2:

1 ,E,w,gx := SolveLCSP(LCµ
);
CEC

3:

if x 6= 0 then4:

return x;

5:>

1 ,E,w,g
直観的には，線形制約 LCµを満たす解 x は，
CEC

局所対抗戦略が漸近的に近づけるべき遷移出現数（出現比）を表している．ここで，線形制約 uT x > 0 は何らかの遷移が出現することを表している．また，AE「q へ入る遷cyc x = 0 の q 行に関する線形制約は，移の出現数」と「q から出る遷移の出現数」が等しいことを表している．よって，この二種類の線形制約に従う x は，一つ以上の閉路とその出現数（出現比）
を表す．これは，有限個の状態しかもたない MPRGのプレイは，閉路の無限個の連結と挿入から構成されていることに由来する．このことから，Inf(ρ) ⊆ Q0となる任意のプレイ ρ について，その上で漸近的にend if近づく遷移出現比はこの二種類の線形制約を満たす

6: end for

はずである．

7: return 0;0

1 ,E,w,g
ここで，LCµ: (R≥0 )|∆ | → B は以下のよう
CEC

01
そして，AE,µstr x = 0 の hq, b, q i 行に関する線形制約は，「µ1 に従うプレイヤ 1 が状態 q ∈ Q01 で b を選択する確率 µ1 (q, b)」と「“遷移 hq, b, q 0 i の出現数”と “q へ入る遷移の出現数” の比」が一致していることを表す．これは，プレイヤ 1 が µ1 に従うときに，Inf(ρ) ⊆ Q0 となるほとんどすべてのプレイ ρ が満たする．

すべき性質である．
さらに，AE,w,J
mp,≥ x のインデックス j が対応する行に関して，遷移の出現比が x に漸近的に近づくプレイ ρ については，以下の式が成り立つ．
AE,w,J
mp,≥ x
= mpw
(39)
j (ρ)
uT x
T
ここで u x > 0 より，以下の条件が成り立つ．

(AE,w,Jmp,≥ x)[j] ≥ 0⇔mpw
j (ρ) ≥ 0(40)

同様に，以下の式も成り立つ(AE,w,K
mp,> x)[k] > 0⇔

mpw
k (ρ) > 0(41)

1 ,E,w,g
従って，線形制約 LCµを満たす解ベクトル
CEC

x に遷移出現比が漸近的に近づくプレイ ρ では，平均利得受理条件を満たす．

このとき，E 0 = hQ00 , ∆00 i ⊆ E が CEC ならば E

も CEC である．
0

1 ,E ,w,g
証明. E 0 が CEC ならば，線形制約 LCµ
(x0 )
CEC

を満たす |∆00 | 次元ベクトル x0 が存在する．ここで，以下のような |∆0 | 次元ベクトルx を考える．
8>0<x [δ] if δ ∈ ∆00 ,x[δ] =>:0otherwise.

(42)

1 ,E,w,g
このとき，明らかに x は線形制約 LCµ
(x) を
CEC

満たす．従って，E も CEC である．

6. 4 メ モ リ レ ス 局 所 最 適 戦 略 探 索 手 続 き

補題 30 (手続き 29 の正当性). 手続き 29 が返す解ベ

SolveOptLocStr

クトル x が零ベクトルでないならば，かつそのとき

こ の 手 続 き は ，MPRG G 上 で プ レ イ ヤ 1 が メ



モリレス戦略 µ1 に従うときに，与えられた RECに限り，E は µ1 に対する CEC である．

証明. (概略)（⇒:）x 6= 0 のとき，線形制約 uT x > 0，E,µ1AE
cyc x = 0，Astr x = 0 を満たされるため，Gq（q ∈ Q0 ）上で，ほとんどすべてのプレイ ρ について
以下のような特徴を持つプレイヤ 0 の戦略が構成でE = hQ0 , ∆0 i に含まれる MLCEC の中で最も高い局
所性能上限もつ MLCEC を探索し，そのメモリレス
局所 (ε-) 最適性能値とそれを与える対抗戦略の対を計算する再帰的手続きである．ただし，この手続きでは打ち切り性能閾値を設定し，局所性能上限がその値きる．

• ρ 上の遷移出現比が x に収束し，かつ，• Q0 に含まれるすべての状態を無限にしばしば訪れる（Inf(ρ) = Q0 ）．

– ただし，ある状態については出現頻度が 0に収束するかもしれない．
E,w,K
そして，線形制約 AE,w,J
mp,≥ x ≥ 0 と Amp,> x > 0 も満たされるために，ほとんどすべてのプレイ ρ は平均利得受理条件を満たす．また，E は REC でもある
ことから，ρ は Rabin 条件も満たしているはずである．よって，E は EC である．
1 ,E,w,g（⇐:）x = 0 のとき，線形制約 LCµ
を満CEC

たす解ベクトルが存在しない．そのため，プレイヤ

1 が µ1 に従うとき，平均利得受理条件を満たすようなプレイを生成する E 上の局所対抗政略は存在しな

以下であるときには再帰を停止する．この手続きの概略は以下の通りである．

i. E が CEC であるかを判定する．
– 同時に，E 上の局所最適性能値 v とその最適対抗戦略 y も計算する．

– その局所最適性能値が打ち切り性能閾値未
満ならば計算を打ち切る．

∗ 系 31 より，E の局所最適性能値は Eの部分 CEC E 0 ⊆ E の局所最適性能値以上であるためである．

ii. E が MLCEC であるかを判定する．
– 同時に，E 上のメモリレス局所対抗戦略 xも計算する．

iii. もし E が MLCEC ならば，局所最適性能値 vを与えるメモリレス局所対抗戦略 z があるか判

い．

定する．
また，以下のような系も成り立つ．
系 31. G を MPRG，µ1 をプレイヤ 1 のメモリレス
00

戦略，E = hQ , ∆ i を G 上の µ1 に対する REC と– メモリレス局所対抗戦略が存在するならば，
それを E 上のメモリレス局所最適対抗戦略とする．

– そうでないならば，x と y からメモリレス
局所 ε-最適対抗戦略を構成する．

4:
5:

return x;
end ifiv. E のそれぞれの子 REC について，メモリレス

6: end for

局所最適対抗戦略探索手続き SolveOptLocStr を

7: return 0;

再帰的に計算する．

v. 子 REC に対する手続き SolveOptLocStr の計算結果を用いて，E とその部分 REC の中で最

0|∆ |1 ,E,w,g
ここで，LCµ→ B は以下のよう
MLCEC : (R≥0 )に定義される線形制約である．
0も高いメモリレス局所 (ε-) 最適性能値を持つ

MLCEC を同定する．

1 ,E,w,g
LCµ
MLCEC (x)⇔– そして，そのメモリレス局所 (ε-) 最適性能
値とそれを与えるメモリレス局所 (ε-) 最適x

B
B AE xB
cyc
B E,µ
B A 1x
B str
B E,w,JBA@ mp,≥ x
AE,w,K
mp,> x>==≥>対抗戦略の対を返す．

0,

1

C
0,C
C
C
0,C
C (. 44)
C
0,C
A
0


ここで，E のそれぞれの子 REC とは，E より真CEC 判定手続きの線形制約式 (34) とこの線形制約に小さい REC の中で極大は REC を指す．その集合

式 (44) の違いは，式 (34) の線形制約 uT x > 0 が式

ChildRECG,µ1 (E) は，以下のように定義できる．
G,µ1ChildREC(E) =(44) では線形制約 x > 0 となっている点である．既に述べたように，x は遷移出現比を表すベクトルであ{REC E 0 ⊂ E|∀REC E 00 ⊂ E.E 0 6⊆ E 00 } (43)り，x > 0 は「すべての遷移の出現数（出現比）が 0

本節ではまず，メモリレス局所最適対抗戦略探索手

より大きい」という制約を表す．両プレイヤがメモリ

続き SolveOptLocStr で用いる部分手続きを説明し，レス戦略に従うとき，状態や遷移の出現頻度はほとん

その後手続き SolveOptLocStr の詳細を示す．

どすべてのプレイ ρ で収束するため，Inf(ρ) = Q0 で

6. 4. 1 MLCEC 判定手続き SolveMLCEC

あるならば，かつそのときに限り，「すべての遷移の

この手続きは，MPRG G でプレイヤ 1 がメモリレス

出現数（出現比）が 0 より大きい」．

戦略 µ1 に従うときに，与えられた REC E = hQ0 , ∆0 i

補題 33 (手続き 32 の正当性). 手続き 32 が返す解ベ

が MLCEC であるかを判定する手続きである．CEC

クトル x が零ベクトルでないならば，かつそのとき判定手続き 29 と同様に，以下のような LCSP に帰着に限り，E は µ1 に対する MLCEC であり，x からメする手続きとして与えられる．

モリレス局所対抗政略を構成できる.

手続き 32 (MLCEC 判定手続き SolveMLCEC).

証明. （⇒:）x 6= 0 のとき，任意の q ∈ Q00 につい• 入力:– MPRG G = hQ, 2AP , ∆, q0 , w, F, Gi– G 上のプレイヤ 1 のメモリレス戦略 µ1 ，
– G 上の EC E = hQ0 , ∆0 i，• 出力:– メモリレス局所対抗戦略を表現した |∆0 | 次
元の非負実数ベクトル x∗ ただし，E が MLCEC でないとき零ベ

て，MPRG Gq 上でプレイヤ 1 が µ1 に従い，プレイ
ヤ 0 が以下のように与えられる戦略 µx0 に従う場合を考える．

µx0 (q, a)=x[hq, a, q 0 i]X
x[hq, a0 , q 00 i](45)

a0 ∈Σ0

このとき，線形制約 x > 0 が満たされるため，ほとん
どすべてのプレイ上で遷移出現比は x に収束する．ここで，x のすべての要素が 0 より大きい，かつ，E は

クトル 0 を返す．

REC であるため，ほとんどすべてのプレイは Rabin

1: for all g = hJ, Ki ∈ G do

受理条件を満たす．また，x は他の線形制約も満たす

2:

1 ,E,w,gx := SolveLCSP(LCµMLCEC );

ため，ほとんどすべてのプレイは平均利得受理条件も

3:

if x 6= 0 then満たす．よって，µx0 はメモリレス局所対抗戦略であ2: for all g = hJ, Ki ∈ G do

り，E は MLCEC である．
（⇐:）対 偶 を 示 す．x = 0 の と き ，線 形 制 約

3:µ1 ,E,w,gT
hv 0 , y0 i := SolveLPPmax ((cE,w
obj ) , LCOptCEC );1 ,E,w,g
LCµ
MLCEC を満たす解ベクトルが存在しない．そ4:

if v > v 0 thenのため，プレイヤ 1 が µ1 に従うとき，E 上のすべて

5:の遷移の出現比が 0 に収束せずに平均利得受理条件

6:を満たすようなプレイを生成する E 上のメモリレス

7: end for

hv, yi := hv 0 , y0 i;
end if

8: return hv, yi;

局所対抗政略は存在しない．

0

6. 4. 2 局 所 最 適 対 抗 戦 略 合 成 手 続 きSolveOptCEC
こ の 手 続 き は ，MPRG A 上 で プ レ イ ヤ 1 が メモリレス戦略 µ1 に従うときに，与えられた REC

E = hQ0 , ∆0 i 上の（無限メモリ）局所最適性能値とそれを与える対抗戦略を計算する手続きである．6. 3 節
で述べたように，CEC 判定手続きの線形制約式 (34)を満たすベクトル x は，局所対抗戦略を表現している．このとき，その x は遷移出現比を表現している
ため，最適化対象である性能値は，|∆0 | 次元非負実数T
T
ベクトル上では (cE,w
obj ) x/(u x) で表現できる．た
0

T
|∆ |
だし，(cE,w→ R は以下のように定義
obj ) : (R≥0 )

された |∆0 | 次元の行ベクトルとして与えられる線形|∆ |1 ,E,w,g
ここで，LCµ→ B は以下のよう
OptCEC : (R≥0 )に定義される線形制約である．
0uT y
B
B AE yB
cyc
B E,µµ1 ,E,w,g
B
LCOptCEC (y) ⇔ B Astr 1 y
B E,w,JBA@ mp,≥ y
AE,w,K
mp,> y=w[d](q, A)

(46)

T
T
従って，線形制約式 (34) に従う (cE,w
obj ) x/(u x) の最適値とそれを与える x を求めればよい．これは，以下のような LPP に帰着する手続きとして与えること
ができる．

=
=
≥
≥

1,

1

C
0,C
C
C
0,C
C (. 47)
C
0,C
A
0.


この手続きで求める E 上の局所最適性能値は，それぞれの g = hJ, Ki ∈ G に対する以下のような線形分数計画問題（linear fractional programming

problem）の最適解の中の最大値である．
maximizex:

subject to:目的関数である．
T0(cE,w
obj ) [hq, A, q i]=

(cE,w )T x/(uT x)
(48)
0obj
1
uT x
≥ 1,
B
C
B AE x
= 0,C
B
C
cyc
B E,µ
C
B A 1 x = 0,C . (49)
B str
C
B E,w,JC
BA
C@ mp,≥ x ≥ 0,A

AE,w,K≥ u
mp,> x
1 ,E,g
この線形制約式 (49) と式 (34) で与えられる LCµ
CECの違いは，> 0 と > 0 の代わりに ≥ 1 と ≥ u を用い

手 続 き 34 (局 所 最 適 対 抗 戦 略 合 成 手 続 きている点である．これは線形（分数）計画法では境界SolveOptCEC).

を含む関係のみしか扱えないためである．なお，式
1 ,E,g(49) は実質的には LCµと等価である．なぜなら
CEC

• 入力:
– MPRG G = hQ, 2AP , ∆, q0 , w, F, Gi

1 ,E,gば，x が LCµ
CEC (x) を満たすならば，cx（c ≥ 1）

– G 上のプレイヤ 1 のメモリレス戦略 µ1 ，

1 ,E,gについても LCµ
CEC (cx) を満たし，さらに，目的関– G 上の EC E = hQ0 , ∆0 i，数の値も変化しないためである．そしてこの線形分数• 出力:– E 上の局所最適性能値 v と局所最適対抗戦
略を表現した |∆0 | 次元の非負実数ベクトルy の対 hv, yi∗ た だ し ，E が CEC で な い と き ，h−∞, 0i を返す．
1: hv, yi := h−∞, 0i;

計画問題は，以下の線形計画問題に帰着できる．

maximizey,y0

:

(cE,w
)T y
0obj T01– 性能値 v を与えるメモリレス局所対抗戦略を表す |∆0 | 次元の非負実数ベクトル z

(50)

u y
≥ y,
C
B
B AE
=
0, C
cyc y
C
B
C
B E,µ1C
B Astr y =0,CBC
B E,w,J
subject to : B Amp,≥ y ≥0, C .(51)C
B
C
B E,w,K
BAmp,> y ≥ y 0 u,CC
B
B uT y
=
1, C
A
@
y0
≥
0
ただし，新たに追加した変数 y 0 は y 0 = 1/(uT x) を意図しており，y = y 0 x である．ここで，この問題では明らかに 1 ≥ y 0 ≥ 0 である．また，1 ≥ y 0 > 0 のときの解となる y は，y 0 = 0 のときも解である．そのため，ここでは y 0 = 0 と固定してもよい．これに
1 ,E,gより，式 (51) から LCµ
OptCEC が得られる．

補題 35 (手続き 34 の正当性). 手続き 34 が返す対

∗ ただし，そのような戦略が存在しない
とき，零ベクトル 0 を返す．

1: for all g = hJ, Ki ∈ G do
2:

1 ,E,g,v
z := SolveLCSP(LCµOptMLCEC );3:

if z 6= 0 then4:

return z;

5:

end if

6: end for7: return 0;0|∆ |1 ,E,g,v
ここで，LCµ→ B は以下のよOptMLCEC : (R≥0 )うに定義される線形制約である．
0
1
1 ,E,gLCµ(z),µ1 ,E,g,v
MLCEC
A . (52)
LCOptMLCEC (z) ⇔ @ E,w(cobj − v · u)T z = 0.
hv, yi が h−∞, 0i でないとき，かつそのときに限り，T
式 (52) で追加されている線形制約 (cE,w
obj −v·u) z =E は CEC である．またそのとき，v は局所最適性能

0 は，性能値が v であることを表現している．よって，値であり，y から局所最適対抗戦略を構成できる．

1 ,E,g,v
線形制約 LCµ
OptMLCEC (z) を満たす z は性能値 v を

証明. （概略）hv, yi 6= h−∞, 0i ならば，かつそのともつメモリレス局所対抗政略を表現している．

きに限り，E が CEC かつ y から対抗政略が構成でき

補題 37 (手続き 36 の正当性). 手続き 36 が返す解ベることは，補題 30 と同様に成り立つ．また，v が局

クトル z が零ベクトルでないならば，かつそのときに所最適性能値であることは明らか．

限り，E は µ1 に対する MLCEC であり，z から性能

6. 4. 3 メ モ リ レ ス 局 所 対 抗 戦 略 合 成 手 続 きSolveOptMLCEC

値 v をもつメモリレス局所対抗政略を構成できる. 
1 ,E,g,v
証明. （⇒:）z 6= 0 のとき，線形制約 LCµ
OptMLCEC (z)こ の 手 続 き は ，MPRG G 上 で プ レ イ ヤ 1 が メが満たされているため，式 (45) と同様に構成されるモリレス戦略 µ1 に従うときに，与えられた REC

戦略 µz0 は，明らかにメモリレス局所対抗戦略である．

E = hQ0 , ∆0 i 上で与えられた性能値 v をもつ有限メ

また，プレイヤ 0 が µz0 に従うとき，ほとんどすべて

モリ対抗戦略を計算する手続きである．これは，以下のプレイ上の遷移出現比が z に収束するため，そののような LCSP に帰着する手続きとして与えられる．

T
性能値は (cE,w
obj z)/(u z) である．そして，線形制約

手 続 き 36 (メ モ リ レ ス 局 所 対 抗 戦 略 合 成 手 続 きSolveOptMLCEC).
• 入力:– MPRG G = hQ, 2AP , ∆, q0 , w, F, Gi– G 上のプレイヤ 1 のメモリレス戦略 µ1 ，
– G 上の EC E = hQ0 , ∆0 i，– 目標性能値 v
• 出力:

T
(cE,w
obj − v · u) z = 0 を満たされているため，明らかにその性能値は v と一致する．
（⇒:）対 偶 を 示 す．z 6= 0 の と き ，線 形 制 約
E,w
T
1 ,E,g,v
LCµOptMLCEC (z) と線形制約 (cobj − v · u) z = 0のどちらも満たす解ベクトルは存在しない．つまり，

E は MLCEC でない，または，性能値 v を与えるメ
モリレス局所対抗戦略は存在しない．

6. 4. 4 手続き SolveOptLocStr の詳細

10:o := hvsup , zi;

6. 4. 1-6. 4. 3 節の部分手続きを用いて，メモリレス

11:

else if ε > 0 then// 最適戦略を更新する

局所最適戦略探索手続き SolveOptLocStr は具体的に// メモリレスのものが存在しない，

は以下のように与えられる．

// かつ，許容誤差が 0 でないとき

手 続 き 38 (メ モ リ レ ス 局 所 最 適 戦 略 探 索 手 続 きv,εx := x + (τx,y
)y;

12:

// メモリレス局所 ε-最適対抗戦略を合成する

SolveOptLocStr).

T
T
v := (cE,w
obj ) x/(u x);

13:

• 入力:
– MPRG G = hQ, 2AP , ∆, q0 , w, F, Gi– G 上のプレイヤ 1 のメモリレス戦略 µ1– G 上の REC E = hQ0 , ∆0 i ⊆ hQ, ∆i– 打切性能閾値 vcutoﬀ// 局所最適値を局所 ε-最適値に変更する
14:

15: for all E 0 = hQ00 , ∆00 i ∈ ChildRECG,µ1 (E)
do
16:

• 出力

end ifhv 0 , x0 i := SolveOptLocStr(G, µ1 , E 0 , vsup );// 子 REC のメモリレス局所最適– MLCEC E 0 ⊆ E の中で最も高い局所最適// 対抗戦略を再帰的に計算する性能値もつ MLCEC 上の，メモリレス局所(ε-) 最適性能値 v とそのメモリレス局所 (ε-)

17:0if v > v or
(v 0 = v and最適対抗戦略を表す |∆0 | 次元の非負実数ベ

num6=0 (x0 ) < num6=0 (x)) then

クトル x の対 hv, xi// より性能が高い，または，同性能でも∗ ただし，MLCEC E 0 ⊆ E が存在しな// 遷移関係のサイズがより小さいとき，い，または，それらすべての局所最適性
能値が vcutoﬀ 未満のとき，対 h−∞, xi
を返す．

1: o = hv, xi := h−∞, 0i;// 局所 (ε-) 最適値とそれを与える戦略の組
2: hvsup , yi := SolveOptCEC(G, µ1 , E);// REC E が CEC か判定し，// 同時に局所最適性能値も計算する
3: if vcutoﬀ > vsup then// 局所最適性能値が打切閾値未満のとき
4:

return h−∞, 0i;

5: end if
6: x := SolveMLCEC(G, µ1 , E);// メモリレス局所対抗戦略を計算
7: if x 6= 0 thenz := SolveOptMLCEC(G, µ1 , E, vsup );// 無限メモリ最適性能をもつ// メモリレス対抗戦略を計算する
9:18:

v := v 0 ;19:

for all δ ∈ ∆0 do

20:

if δ ∈ ∆00 then21:x[δ] := x0 [δ];

22:

else

23:

x[δ] := 0;24:

end if

25:
26:

end forend if

27: end for
28: return o;v,εただし，τx,yは以下を満たす最小の非負実数とする．
“
”
v,ε
τx,y

// メモリレス局所対抗戦略が存在するとき
8:// 局所最適値と局所最適戦略を更新する

if z 6= 0 then// メモリレスのものが存在するとき≥T(v − ε)uT − (cE,wxobj ). (53)
ε
また，num6=0 (x) はベクトル x の非零の要素数を表す．
系 31 より，E が CEC のとき，ステップ 2 において計算される E 上の（無限メモリ）局所最適性能値

v は，E の部分 CEC の局所最適性能値以上である．
そのため，v が打切閾値 vcutoﬀ より小さい場合，E

の部分 CEC の局所最適性能値が打切閾値 vcutoﬀ 以
上となることはない．

ダーである．
なお，この再帰的手続きでは，同じ部分 REC に対E が MLCEC であるとき，v と等しい局所性能値

する手続き SolveOptLocStr を複数回呼び出し得る．

をもつメモリレス対抗戦略が存在するならば，その戦そうした場合に前の計算結果をそのまま返しても，全略は局所最適なメモリレス対抗戦略であり，E の部

体の手続きの正当性は保たれる．



分 MLCEC の中で最大の最適性能値をもつ．ただし，同性能の，より小さい（遷移数が少ない）MLCEC が6. 5 最大到達期待値計算手続き SolveReachExp

存在する可能性がある．また，v と等しい性能値をも

この手続きは，MPRG G 上でつメモリレス局所対抗戦略が存在しない場合でも，局• 状態の部分集合 Q0i とは，ステップ 2 で得られる（無限メモリ）局所最適対• プレイ上で Q0i へ到達することの優先度 vi
Sの組 hQ0i , vi i の集合 L = i hQ0i , vi i が与えられてい抗戦略を表す y と，ステップ 6 で得られるメモリレ

るときに，プレイヤ 1 のメモリレス戦略 µ1 に対して，

ス局所対抗戦略を表す x から構成される．なぜならそれぞれの状態 q での最大到達期待値（プレイヤ 0 が

所 ε-最適なメモリレス対抗戦略を構成できる．これ0

1 ,E ,w,gば，線形制約 LCµ
MLCEC (x) を満たす x と線形制約
0
1 ,E ,w,g
LCµOptCEC (y) を満たす y に関して，任意の c > 001 ,E ,w,g
で x + cy が線形制約 LCµ
MLCEC (x + cy) を満たす
v,εためである．このとき，c = τx,yとすれば，その性能値は局所 ε-最適となる．

適切に遷移先を選ぶことで得られる優先度期待値の最大値）を計算する手続きである．これは最大到達確率計算手続き 27 と似ているが，到達される状態に優先度が付けられている点が異なる．直観的には，Q0i
は MEC の状態集合，優先度 vi はその MEC に含ま

そして，ステップ 15-27 ですべての部分 MLCEC

れる MLCEC の中で最大の局所最適性能値であるこの中で最大の局所最適性能値をもつ MLCEC を探索とを意図している．つまり，優先度期待値が高いプレしている．

イの生起させようとする戦略では，局所最適性能値がよって，以下の補題が成り立つ．

高い MLCEC へ到達する期待値が高くなる．ここで，補題 39 (手続き 38 の正当性). 手続き 38 が返す対

hv, xi が h−∞, 0i でないならば，かつそのときに限り，E の部分 REC の中に MLCEC であるものが存

どの Q0i にも含まれない状態の優先度は −∞ であるものとする．つまり ρ の優先度 ν L (ρ) は以下のように定義する．

在し，それらの中で最大の局所最適性能値が v ，かつ，

x から性能値 v をもつ局所メモリレス対抗戦略を構


成できる．

証明. MLCEC 判 定 手 続 き SolveMLCEC の 正 当性（ 補 題 33） ，局 所 最 適 対 抗 戦 略 合 成 手 続 きSolveOptCEC の正当性（補題 35），メモリレス対抗戦略合成手続き SolveOptMLCEC の正当性（補題37）より明らか．

ν L (ρ)8>max {vi |∃j.ρ[j] ∈ Q0i }>>>hQ0i ,vi i∈L
>
>
>
[
>
>
< if ∃j.ρ[j] ∈
Q0i ,

(54)
hQi ,vi i∈L
>
>
>
>
>
−∞
>
>
>
>
:
otherwise.
このように定義するのは，プレイ中に MLCEC へ到=達した場合でも，より性能の高い別の MLCEC へ到
達させられる可能性があるためである．そして，それ
1 ,Loc
ぞれの状態 q での最大到達期待値 eG,µは，厳密q

注意 40 (手続き 38 の計算量). 手続き 38 は最悪の場
00合，グラフ E = hQ , ∆ i 上のすべて REC を網羅的に列挙する必要がある．グラフ E の部分グラフの個数は，E のサイズの指数オーダーであるため，手続
き 38 の時間計算量は E のサイズに関して指数オーには以下のように定義される．
1 ,L
eG,µ
q

=

max{EPrGq ,Str0 ,µ1 [ν L ]}.
Str0

(55)

そしてこれは，以下のような LPP に帰着する手続
きとして与えられる．
手続き 41 (最大到達期待値計算手続き SolveReach-証明. 補題 28 と同様．ただし，p[q] < 1 である q に

Exp).
• 入力

関しては，明らかに e[q] = −∞ となるが，線形制約
1 ,p,LLCG,µではそれに関する制約を与えていない．そexp– MPRG G = hQ, 2AP , ∆, q0 , w, F, GiS– L = i hQ0i , vi i∗のため，ステップ 3-5 で代入している．

Q0i ⊆ Q は状態集合ただし，· それぞれの Q0i は互いに共通部分をもたないと仮定する．

∗ vi ∈ R は Q0i に含まれる状態を訪れた際に保証される利益– それぞれの状態の最大利益期待値 eqG,µ1 ,Lを与える |Q| 次元のベクトル eS
1: p := SolveReachProb(G, µ1 , hQ0 ,vi i∈L Q0 );ス戦略に対するメモリレス最適対抗戦略を合成する

これは，6 章で与えた手続きを部分手続きとして用い，5. 2 節の概略に沿った以下の手続きである．
手続き 43 (MPRG メモリレス最適対抗戦略合成手
続き).

T
G,µ1 ,Loc
e := SolveLPPmin ((cp);
reach ) , LCexp• 入力:

3: for all q ∈ Q such that p[q] < 1 do
4:

本章では，MPRG においてプレイヤ 1 のメモリレ
手続きを与える．

• 出力

2:7 MPRG 最適対抗戦略合成手続き– MPRG G = hQ, 2AP , ∆, q0 , w, F, Gi

e[q] := −∞;5: end for– G 上のプレイヤ 1 の戦略 µ1

6: return e;– 許容誤差 ε ≥ 0T
ここで，線形目的関数 (cpreach ) は，は以下のように定義される |Q| 次元の行ベクトルである．
8><1 if p[q] = 1,
cp
[q]
=
reach
>
:0 otherwise.

(56)

1 ,p,Lまた，線形制約 LCG,µ: (R≥0 )|Q| → B は以下のexpように定義される線形制約である．
0
1
AQ,L≥ bQ,L
exp e
exp ,
B
C
1 ,L
Q,∆0
LCG,µ
(e) ⇔ B≥
0, C
exp
@ Anc eA . (57)
Q,∆1 ,µ1
Apc
e ≥
0
Q,L
ただし，AQ,L
exp は |Q| × |Q| 行列，bexp は |Q| 次元の実数ベクトルであり，以下のように定義される．
8>>1 if ∃hQ0 , vi ∈ L.q ∈ Q0
>
>
<
0
AQ,L
[q,
q
]
=
(58)
and q = q 0 ,
exp
>
>
>
>
:0 otherwise.
8><v if ∃hQ0 , vi ∈ L.q ∈ Q0 ,
bQ,L
=
(59)
exp [q]>:0 otherwise.
• 出力:8>>“対抗戦略は存在しない”
>
>
>
>
>
>
>
if |CntG,µ1 | = 0,
>
>
>
>
>
<“メモリレス対抗戦略は存在しない”–>
1>
if |CntG,µ1 | 6= 0 and |CntG,µ>ml | = 0,
>
>
>
>
>
>
メモリレス (ε-) 最適対抗戦略 µ0
>
>
>
>
>
: otherwise.
1: M := DecompMEC(G, µ1 );// ゲーム上の MEC の集合を計算する
2: N := ∅;// な CEC の集合の対の集合
3:
4:

1 ,L
eG,µ
である．
q



for all Ei = hQ0i , ∆0i i ∈ M do
Mi0 := DecompMREC(G, µ1 , Ei );// MEC E 上の MREC の集合を計算する

5:

Mi00 := ∅;6:0
for all Eij∈ Mi0 do7:// Mi0 中の CEC の集合

0
x := SolveCEC(G, µ1 , Eij);// MREC E 0 上の対抗戦略を計算する

補題 42 (手続き 41 の正当性). 手続き 41 が返す解ベクトル e の各要素 e[q] は，q での最大到達期待値// MEC とそこに含まれる極大8:

if x 6= 0 then// E 0 上に対抗戦略が存在する

//（E 0 が CEC である）とき

if vi > −∞ then30:// E 0 が MLCEC を含むとき

0Mi00 := Mi00 ∪ {Eij};9:

Loc := Loc ∪ {hEi , oi i};

10:

end if

31:

11:

end for32:

12:

if Mi00 6= ∅ then33: end forS
34: L := hhQ0 ,∆0 i,hvi ,xi ii∈Loc hQ0i , vi i;

13:
14:

N := N ∪ {hEi , Mi00 i};

end ifii

35: e := SolveReachExp(G, µ1 , L);

end if// 各状態の最大期待性能値を計算する

15: end for
16: Qreach :=S0
hhQ0 ,∆0 i,M 00 i∈N Qi ;i

i

i

36: if e[q0 ] = −∞ then// CEC を含む MEC に含ま// 初期状態で期待される最適性能値が −∞// れる状態の集合を計算する// (メモリレス戦略では対抗できない) とき

17: p := SolveReachProb(G, µ1 , Qreach );// 各状態の Qreach への最大到達確率を計算する
18: if p[q0 ] < 1 thenreturn “メモリレス対抗戦略は存在しない”;

37:

38: end if
39: µ0 := µLoc,e;0// 最適対抗戦略を構成する// 初期状態から Qreach への// 最大到達確率が 1 でないとき
19:

return “対抗戦略は存在しない”;// Loc と e からメモリレス

40: return µ0 ;また，メモリレス戦略 µLoc,e: Q0 × Σ0 → [0, 1] は以
0

20: end if

下のように与える．

21: Loc := ∅;(q, a) =µLoc,e08xi [hq, a, q 0 i]
>
>
P
>
>
> a0 ∈Σ0 xi [hq, a0 , q 00 i]
>
>
>
>
>
>
if ∃hEi , hvi , xi ii ∈ Loc.(
>
>
>
>
>
<
e[q] = vi and xi [hq, a, q 0 i] > 0),// “MEC” と “その中の最大のメモリレス// 局所最適性能値とそれを与えるメモリ// レス局所最適対抗戦略の対” の対の集合
22: for all hEi , Mi00 i ∈ N do
23:oi = hvi , xi i := h−∞, 0i;// メモリレス局所最適性能値とそれを与// えるメモリレス局所最適対抗戦略の対

24:
25:

0
for all Eij∈ Mi00 do>>
0 if e[∆(q, a)] < max{e[∆(q, a0 )]},>>a0 ∈Σ0
>
>
>
>
1
>
>
>
0 i|e[∆(q, a0 )] > 0}|
>
|{hq,
a
>
>
>
>
:
otherwise.

(60)

hvij , xij i :=0SolveOptLocStr(G, µ1 , Eij, vi , ε);

直観的には，µLoc,eは，それぞれの状態 q ∈ Q0 に
00// 極大な CEC Eijに含まれる MLCEC の中でおいて，以下のような特徴を持つメモリレス戦略で// 最大の局所最適性能を与えるものを探索する
26:

if vij > vi or(vij = vi andnum6=0 (xij ) < num6=0 (xi )) then

27:

ある．

• q がある MEC Ei 上でメモリレス局所最適性能
値 vi を与える MLCEC に含まれており，かつ，

q の最大期待性能値 e[q] が vi と等しいとき，// より性能が高い，または，同性能でも– Ei 上で性能値 vi を与える（xi で表現され// 遷移関係のサイズがより小さいときた）メモリレス局所最適対抗戦略に従う．

oi := hvij , xij i;// メモリレス最適局所対抗戦略を更新する• そうでないとき，– 最大期待性能値が最も高い状態を遷移先と

28:

end ifするようなアクションを（ただし，複数存在

29:

end for

するときにはそれらを等確率で）選択する．

定理 44 (手続き 43 の正当性). 手続き 43 が “(メモリレス）対抗戦略は存在しない” を返すならば，かつ

8 計算量

そのときに限り，G 上の µ1 に対する（対抗戦略は存

本章では，MPRG メモリレス最適対抗戦略合成手続き（手続き 43）と LLTLmp 最適合成問題の計算量在するがメモリレス）対抗戦略は存在しない．
また，手続き 43 がプレイヤ 0 のメモリレス戦略 µ0について述べる．

を返すならば，かつそのときに限り，µ0 は G 上の µ1に対するメモリレス最適対抗戦略である．



証明. （概略）MREC 分解手続き DecompMREC の正当性（補題 26）と CEC 判定手続き SolveCEC の正当性（補題 30），系 31 より，ステップ 1-15 の結果として得られる N は，
「CEC を含む MEC Ei 」と「それに含まれる極大な CEC の集合 Mi00 」の対の集合となっている．そして，最大到達確率計算手続き

SolveReachProb の正当性（補題 28）より，p は，プ
レイヤ 1 が µ1 に従うときの各状態から CEC に含まれる状態への最大到達確率を表している．よって，初期状態 q0 から CEC への最大到達確率が 1 未満であるとき，プレイヤ 0 がどのような戦略に従ったとしても CEC へ到達できない確率は 0 より大きい．つまり，対抗戦略は存在しない．
そうでないとき，メモリレス局所最適対抗戦略探索
手続き SolveOptLocStr の正当性（補題 39）より，ス
テップ 1-15 の結果として得られる Loc は，「MLCECを含む MEC Ei 」と「“それに含まれる MLCEC の中で最大のメモリレス局所最適性能値 vi ” と “それを与えるメモリレス局所最適対抗戦略を表すベクトルx”」の対の集合となっている．そして，最大到達期
待値計算手続き SolveReachExp の正当性（補題 42）より，e はプレイヤ 1 が µ1 に従うときの各状態の最大期待性能値を表している．よって，q0 の最大期待性能値が −∞，すなわち，q0 から MLCEC への最大到達確率が 1 未満であるとき，プレイヤ 0 がどのような戦略に従ったとしても MLCEC へ到達できない
確率は 0 より大きい．つまり，メモリレス対抗戦略は存在しない．
そうでないとき，e はそれぞれの状態での (ε-) 最適な最大性能期待値を表すため，µLoc,eは明らかに
0
メモリレス (ε-) 最適対抗戦略となっている．以上により示された．

8. 1 MPRG メモリレス最適対抗戦略合成手続きの計算量

MPRG メモリレス最適対抗戦略合成手続きの各ブ
ロックの計算量は以下の通りである．

• ステップ 1-15
まず，MEC 分解はゲームのサイズに関して多項式時間で計算できる．ゲーム上の MREC の総
サイズは，その極大性より，ゲームのサイズとRabin 対の個数に関して線形である．そして，それぞれの MREC に対する CEC 判定は，CEC 判
定手続き SolveCEC（手続き SolveCEC）により対象とする MREC のサイズに対して多項式時間で計算できる．そのため，このブロックの計算量
はゲームのサイズに関して多項式時間である．

• ステップ 16-21 及び 34-40
最大到達確率計算手続き SolveReachProb（手続き 27）と最大到達期待値計算手続き SolveReach-Exp（手続き 41）はどちらもゲームのサイズに対して多項式時間で計算できるため，この二つのブロックの計算量はゲームのサイズに関して多項式時間である．

• ステップ 22-33
メモリレス局所最適戦略探索手続き SolveOpt-

LocStr（手続き 38）の計算量は注意 40 で述べたように，指数時間オーダーである．そのため，
このブロックの計算量はゲームのサイズに関して
指数時間である．
よって，MPRG メモリレス最適対抗戦略合成手続
きの計算量は指数時間オーダーである．なお，対抗戦
略であるか否かは多項式時間で検証可能であるため，最適化を行わない MPRG メモリレス対抗戦略合成問
題は NP に属す．

8. 2 LLTLmp 最適合成問題の計算量

1Ψ などを用いることができる．

仕様 Φ = Ψ ∧ Θ の LTL 式部分 Ψ と等価Φ::=Ψ | Θ | Φ ∨ Φ | Φ ∧ Φ,

な DRA は最悪で O(2|Ψ| ) の状態数をもつ．そして，Θ::=θ | ¬Θ | Θ ∨ Θ | Θ ∧ Θ,

注意 8. 1 で述べたように，MPRG メモリレス最適対

θ::=MP(t)  0,

抗戦略合成手続き（手続き 43）はゲームのサイズにt::=

c | 1Ψ | t + t | t · t | − t.

mp

LLTL

mp

最

定義 9 の弱い意味での LLTLmp 有限メモリ実現可能

適合成問題は 3EXPTIME に属す．なお，最適化を性判定及び合成においては，平均利得式の否定は本行わない PRG メモリレス対抗戦略合成問題が NP に

質的な拡張にはならない．なぜならば，RS と環境が対して指数時間で計算できる．従って，LLTL

属すことから，定義 9 の弱い意味での LLTL

mp

実現

有限状態ならば，状態やアクションの出現頻度が収可能性判定及び合成問題は N2EXPTIME に属す．

束するため，¬MP(t) > 0 と MP(−t) ≥ 0 は等価とDRA の構成に関しては，平均利得式を上手く用い見なせる．表現力が大きく異なる点は，LTL 式 Ψ にることで，計算量を抑制できる可能性がある．例えば，関する特性変数 1Ψ を記述できる点である．例えば，2(req → wait U res)(61)

1ψ1 Uψ2 のような利得項を用いることができる．一般という LTL 式は，「常に，“リクエスト req が生起したに，ある時間で LTL 式 ψ1 Uψ2 が成り立つか否かは非とき，応答 res するまで待ち wait 続ける”」という性

有界な未来に依存するため，各時点での 1ψ1 Uψ2 の解質を表すが，平均利得式も用いることで同じ意図（同釈値を決定できない [15]．ゲームベースの実現可能性

じ意味ではない）の性質を以下のように表現できる．

判定/合成 [9] [8] [7] [3] [16] では，仕様を丁度表現するよ2(req → wait W res) ∧ MP(1wait ) < 1(62)

うな決定性オートマトンが必要となるため，1ψ1 Uψ2

このとき，式 (61) は「req が成り立ったならばいつかのような各時点で解釈値を決定できない利得項を含必ず res も成り立つ」という強い性質を表している．

む LLTLmp 仕様の実現可能性判定及び合成は困難で一方で，式 (62) の LTL 部分では「req が成り立ったある．一方で，モデル検査や充足可能性判定では，仕としても，必ずしもその後 res が成り立たなくてもよ様を丁度表現するようなオートマトンは必ずしも決定い」という弱い性質を表している．こうした違いは，的でなくてもよい．そのため，LTLmp モデル検査問構成される決定性オートマトンの構造に大きな影響

題/充足可能性判定問題は EXPTIME に属し，また，を与える．そのため，解析に適した表現を選択して仕LTLmp 仕様の充足可能な範囲での最適化問題も指数様を記述することで，検証を効率化できる可能性が時間で計算できる [14]．これらの問題は，本研究の実ある．

現可能性判定/最適合成手法と同様に，線形制約充足
可能性判定や線形計画法を用いて解くことができる．

9 関連研究本章では，本研究と関連する研究をいくつか紹介する．

LTL 実現可能性判定器 Acacia+ [3] を開発している
Bohy らは，LLTLmp よりも表現力が若干小さい平均
利得線形時間論理 LTLMP [4] を，我々の研究とは独本研究では，仕様記述言語として，平均利得線形立に開発している．この LTLMP は，LLTLmp の構

時間論理 LTLmp [14] のフラグメントである LLTLmp

文を，平均利得式 Θ は連言のみ，原子平均利得式 θを用いている．LTLmp では LLTLmp の場合とは異なは境界を含む閾値条件のみに制限したようなフラグ

り，LTL 式 Ψ と平均利得式 Θ の選言 Ψ ∨ Θ や，平メントである．

均利得式 Θ の否定 ¬Θ，LTL 式 Ψ に関する特性変数Θ::=θ | Θ ∧ Θ,θ::=MP(t) ≥ c.

そして Bohy らは，通常の実現可能性「任意の環境に対して仕様を満たす RS が存在するか」を判定し，仕様を実現する RS を自動合成する問題（co-N2EXPTIME

[4]）を解けるように Acacia+を拡張している．その実

くとも，「ある限定された環境の集団」に対して仕様

現可能性判定/合成には，平均利得 parity ゲーム†13を実現し，かつ，最適にふるまうシステムを合成でき[6] の有限メモリ勝利戦略問題（co-NP 完全）の解法

るように本手法を拡張することは今後の興味ある課

アルゴリズムを利用している．しかしながら，Bohy

題の一つである．また，非線形制約充足可能性判定，らの手法では，目的関数 MP(t) の最適化を行うには，

非線形目的関数最適化，多目的最適化などの SMT や

MP(t) ≥ c を仕様に追加し，閾値 c を手動で変更しLP に関連する応用技術を利用することで，より表現ながら繰り返し検証する必要がある．一方で，本手法力の高い言語による仕様記述に対応するように本手

では，弱い（確率的）実現可能性「特定の確率的環境法を拡張できる．

のみに対してほとんどかならず仕様を満たす RS が存本手法のボトルネックは，以下の二点である．

在するか」を判定し，仕様を実現するだけでなく，与• LTL 式から DRA への変換

えた目的関数に関して最適な RS の自動合成を行うこ• メモリレス局所最適戦略探索（手続き 38）とができる．

LTL 式から DRA への変換に関しては，直接的に計算量を改善することは困難である．ただし，LLTLmp

10 おわりには LTL より表現力が高く，特性の異なる式で同じ意

本稿では，既知の MDP 環境に対して，LLTL

mp

仕図の性質を表現できることがある．そのため，解析に

目的関数に関して最適な適した表現を選択して仕様を記述することで検証を効RS を MDP として自動合成法する手法を与えた．こ率化できる可能性がある．メモリレス局所最適戦略探れにより，特定の環境下において，イベント生起順序

索に関しては，その中で行われているそれぞれの線形に関する機能仕様を満たすだけでなく，平均コストや制約充足可能性判定/線形計画法の独立性が高いため，

イベント頻度などに関する性能仕様を満たし，かつ，並列化が効果的であると考えられる．また，ヒューリ

一部の性能が最適化されたシステムを自動合成するこスティックを用いた探索も有効であると考えている．

mp様を実現し，かつ LLTLとが可能となった．実現可能性判定器 Acacia+で実装されている，若干弱い表現力を持った仕様からの自参 考 文 献

動合成手法 [4] は，「任意の環境」を想定した最悪ケー[ 1 ] Abadi, M., Lamport, L., and Wolper, P.: Realizable and unrealizable speciﬁcations of reactive
systems, Automata, Languages and Programming,
LNCS 372, Springer Berlin / Heidelberg, 1989,
pp. 1–17.
[ 2 ] Baier, C. and Katoen, J.-P.: Principles of Model
Checking, The MIT press, 2008.
[ 3 ] Bohy, A., Bruyére, V., Filiot, E., Jin, N., andRaskin, J.-F.: Acacia+, a Tool for LTL Synthesis,
Computer Aided Verification, LNCS 7358, Springer
Berlin / Heidelberg, 2012, pp. 652–657.
[ 4 ] Bohy, A., Bruyére, V., Filiot, E., and Raskin, J.F.: Synthesis from LTL Speciﬁcations with MeanPayoﬀ Objectives, Tools and Algorithms for theConstruction and Analysis of Systems, LNCS 7795,
Springer Berlin Heidelberg, 2013, pp. 169–184.
[ 5 ] Chatterjee, K. and Henzinger, M.: Faster anddynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic veriﬁcation, Proceedings of the TwentySecond Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’11, SIAM, 2011, pp. 1318–
1336.
[ 6 ] Chatterjee, K., Randour, M., and Raskin, J.-F.:スに対応するシステムを自動合成する手法だが，最適化に関しては取り扱っていなかった．それに対して本
手法は，「特定の確率的環境」を想定し，それに特化したシステムを自動合成する手法であり，最適化についても自動化している．また，実現可能性判定を線形制約充足可能性判定に帰着して SMT ソルバで解き，最適化を線形計画問題に帰着して LP ソルバで解く，

SMT-LP ベースのアプローチをとっている点も大きな特徴の一つである．
ただし，本手法で合成した RS は，想定した環境に特化しすぎてしまい，環境がほんの少し違うものに変わっただけでも仕様（特に性能仕様）を満たさなくなる可能性がある．そのため，「任意の環境」ではな†13 MPRG の Rabin 受理条件の代わりに parity 受理
条件を用い，平均利得受理条件 G を単集合 {hJ, ∅i}に制限したゲーム．

Strategy Synthesis for Multi-Dimensional Quantitative Objectives, CONCUR 2012 - Concurrency
Theory, LNCS 7454, Springer Berlin Heidelberg,
2012, pp. 115–131.
[ 7 ] Ehlers, R.: Symbolic Bounded Synthesis, Computer Aided Verification, LNCS 6174, Springer
Berlin / Heidelberg, 2010, pp. 365–379.
[ 8 ] Filiot, E., Jin, N., and Raskin, J.-F.: An Antichain Algorithm for LTL Realizability, Computer
Aided Verification, LNCS 5643, Springer Berlin /Heidelberg, 2009, pp. 263–277.
[ 9 ] Jobstmann, B. and Bloem, R.: Optimizations for LTL Synthesis, Formal Methods in Computer Aided Design, 2006. FMCAD ’06, nov. 2006,
pp. 117 –124.
[10] Klein, J. and Baier, C.: Experiments with deterministic -automata for formulas of linear temporal logic, Theoretical Computer Science, Vol. 363,
No. 2(2006), pp. 182 – 195.
[11] Pnueli, A. and Rosner, R.: On the synthesis ofa reactive module, Proceedings of the 16th ACM
SIGPLAN-SIGACT symposium on Principles ofprogramming languages, POPL ’89, New York, NY,
USA, ACM, 1989, pp. 179–190.
[12] Pnueli, A.: The temporal logic of programs,
Foundations of Computer Science, 1977., 18th Annual Symposium on, 31 1977-nov. 2 1977, pp. 46–57.
[13] Rosner, R.: Modular synthesis of reactive systems, PhD Thesis, Weizmann Institute of Science,
1992.
[14] Tomita, T., Hiura, S., Hagihara, S., andYonezaki, N.: A temporal logic with meanpayoﬀ constraints, 14th International Conference
on Formal Engineering Methods (ICFEM 2012),
LNCS 7635, Springer Berlin / Heidelberg, 2012,
pp. 249–265.
[15] 冨田尭, 萩原茂樹, 米崎直樹: Mean-Payoﬀ 制約を記述可能な線形時間論理, 日本ソフトウェア科学会第 29
回大会論文集, 2012.
[16] 上野 篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹:
LTL 式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装に関する研究, 日本ソフト
ウェア科学会第 30 回大会論文集, 2013.

A 線形制約充足問題と線形計画問題「線形制約 aT x ∼ b（∼∈ {<, >, ≤, ≥}）の和積で与えられる制約を満たす x が存在するか否か」を決定する問題を線形制約充足問題（LCSP）という．これは，線形実数算術（linear real arithmetic，LRA）に対応した SMT ソルバを用いて多項式時間で決定可
能である．
また，
「線形制約 Ax ≥ b に従う線形目的関数 cT xの最大値/最小値（及びそれを与える解 x）」を求める
問題を線形計画問題（LPP），それを解く手法を線形計画法（LP）という．線形計画問題はしばしば以下のように表現される．

maximize/minimizex

:

cT x,

(63)

subject to:

Ax ≥ b.

(64)

これは，LP ソルバや汎用数値計算ソフトウェアを用いて多項式時間で計算可能である．
そして，「線形制約 Ax ≥ b に従う線形分数目的関数 (cT x + e)/(dT x + f ) （ただし，dT x + f は常に正）の最大値/最小値（及びそれを与える解 x）」を線形分数計画問題という．

maximize/minimizey,z:cT y + ez,

subject to:

Ay − zb ≥ 0, (66)(65)

dT y + f z = 1,(67)z ≥ 0.

(68)T

ただし，補助変数 z と y は，z = 1/d x + f ，y = zx
を意図した変数である．ここで，得られた最適値は，

z = 0 のときには上限値/下限値であり z > 0 のときには最大値/最小値である．