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

協調的リアクティブシステムの合成手法
冨田 尭

上野 篤史

萩原 茂樹

米崎 直樹

外部環境と継続的に相互作用するソフトウェア/ハードウェアのモデルとなるリアクティブシステムの時間論理仕様からの自動合成では，しばしば環境が仕様 φenv に従うと仮定し，システムの仕様 φsys に対して，含意式 φenv → φsysが実現可能か否か検査する．しかしながら，素朴な自動合成手法では，環境が環境仕様 φenv を違反することを強いる，あるいは，少しでも環境仕様 φenv に違反した時にシステム仕様 φsys に従うことを放棄してしまうシステムを合成してしまうことがある．特に，既存の自動合成器では，状態数のより小さいシステムを合成しようとするため，
そのような非協調的なシステムが合成され易い．そこで本研究では，システムの協調性を定量化するいくつかの評価関数を導入し，それらの評価関数に関して局所最適なシステムを自動合成する手法を与える．

され，Lily†1 [11]，Acacia+†2 [3]，Unbeast†3 [7] など

1 はじめにの自動合成器が開発されている．仕様からのシステム

1. 1 背景の自動合成は，非常に大きい計算量を要するものの不制御システムや組み込みシステムのような，外部具合が混入する余地がなく，高い計算コストを掛けて環境（ユーザや外部モジュールなど）と継続的に相互でも安全性を保証する必要があるシステムの安全な作用するソフトウェア/ハードウェアには，しばしば開発に適している．

高い安全性が求められる．それらのシステムは，近年増々，大規模化・複雑化し，その安全性を確保するこ

1. 2 動機と目的とが困難となっており，それを保証するための手法とリアクティブシステムの時間論理仕様からの自動して形式手法に注目が集まっている．
外部環境と継続的に相互作用するソフトウェア/

合成では，しばしば環境が仕様 φenv に従うと仮定し，システムの仕様 φsys に対して，過去の相互作用履歴

ハードウェアはリアクティブシステムとしてしばしばのみを用いて含意式 φenv → φsys （⇔ ¬φenv ∨ φsys ）モデル化される．そして，与えられたモデルが時間論を満たすように現在の出力を逐次決定できるか否か，

理 [9] などで規定された仕様を満たすか否かの網羅的

即ち，φenv → φsys が実現可能か否かを検査し，可能検査（モデル検査 [4] [5]）は，実際のシステム開発でである場合にはその実現システムを出力する．このもしばしば用いられている [2]．一方で，モデル検査

とき，一般には，環境が φenv を違反することを強いのような与えられたモデルの検証ではなく，与えられる，あるいは，少しでも φenv に違反した時に φsys にた時間論理仕様の実現可能性 [13] [1] [15]（プログラム従うことを放棄してしまうシステムが生成され得る．

可能性）を判定しシステムを自動合成する手法も提案

ただし，φenv として，環境入力に関する物理的制約

A Synthesis Method of Cooperative Reactive Systems
Takashi Tomita, Atsushi Ueno, Shigeki Hagihara,Naoki Yonezaki, 東京工業大学大学院情報理工学研究科計算工学専攻, Dept. of Computer Science,
Graduate School of Information Science and Engineering, Tokyo Institute of Technology.

など，システム出力に依存しない制約のみをしばしば†1 http://www.iaik.tugraz.at/content/research/
design_verification/lily/†2 http://lit2.ulb.ac.be/acaciaplus/†3 http://www.react.uni-saarland.de/tools/unbeast/true

考慮する．その場合，φenv が充足可能でさえあれば

φenv を違反することを強いるシステムは存在しない．

q s0 : resさらに，φenv が物理的制約である場合などには，環境が φenv に反する動作を行う可能性を考慮する必要

図1

常に res を出力し続ける非協調的システム f1 ．

もない．そのため，既存の自動合成器は，単に，制御構造がより単純なシステム，即ち，状態数のより小さ

s2 : resいシステムを合成しようとする．

¬req

しかしながら，一般には，φenv はシステム出力に依存している．特に，相互作用する複数のモジュールからなるシステムをモジュール毎に合成する場合，合成しようとしているモジュールからみた環境は他モジュールであり，その環境仕様はシステム出力に依存
1 s1 : ¬res @ true
@
@
R
req

req
図2

s0 : ¬res i


¬req

req が立ち下がった直後に res を返し，それ以外のしている．そのため，他モジュールの仕様の違反を強ときには ¬res を返す協調的システム f2 ．

制しないモジュールや，他モジュールの仕様に反する動作が生起したとしても自身の仕様を放棄しないモ

後に res を返し，それ以外のときには ¬res を返す」

ジュールが合成されることが望ましい．ここで例としという，φe → φs を実現し，かつ，¬φe を強いるこて，線形時間論理 LTL [14] で記述された，以下のよとがない協調的なシステム f2（図 2，状態数 3）も存うな環境仕様 φe とシステム仕様 φs を考える．

在しており，環境もシステムもそれぞれの仕様を満た

φe = 2(res → ¬req) ∧ 23req ∧ 23¬req,(1)

しながら動作し続けることができるため，現実的には

φs = 2(req → ⃝¬res) ∧ 2(req → ⃝3res).

(2)

このシステムの方がより望ましいと考えられる．

ただし，req は環境が真偽を制御する入力命題（信そこで本研究では，環境仕様が満たされ易いように号），res はシステムが真偽を制御する出力命題（信配慮する，あるいは，（環境仕様が満たされない場合号）である．また，システム（先手）の出力とそれにでも）システム仕様をできるだけ満たすように努力す

対する環境（後手）からの応答入力を LTL の意味論

る協調的なシステムを合成する手法の開発を目的とにおける一つの時間とする．直観的には，φe は「常する．

に “レスポンス res を受け取ったときには直ちにリク
エスト req を出さない”，かつ，無限にしばしばリク

1. 3 内容

エストを出すがリクエストを出さないタイミングも無本研究では，まず，システムの協調性の度合いを定限にしばしばある」，φs は「常に “リクエストを受け量化するいくつかの評価関数を導入する．これらの評取った直後にはレスポンスを返さないないが，その後価関数は，環境仕様 φenv を満たす環境の集合の大きいつか返す”」という性質を表す．ここで，φs は，環さやシステム仕様 φsys を満たす環境の集合の大きさ

境が常に req を入力し続けた場合に対応できるシステを確率論的な観点から想定した環境分布に基づき協ムが存在しないため，実現不能である．一方，含意式

調性の度合いを評価する．

φe → φs は実現可能である．これは，「常に res を出

そして，それらの協調性評価関数に関して局所最適

力し続ける」システム f1 （図 1，状態数 1）が，環なシステムを合成する手法を提案する．時間論理仕様

境仕様の否定を実現する，即ち，環境に ¬φe を強いからの実現可能性判定/自動合成では，（1）時間論理ることができるためである．既存の自動合成器では，仕様から決定性オートマトンを経て ω-正規ゲームへ

単純なシステムを合成しようとするあまり，このようの変換し，（2）ゲーム上の勝利戦略の合成する．シスな非協調的で望ましくないシステムが合成され易い．

テムはこの勝利戦略として得られるが，近年の研究でしかしながら，この例では，「req が立ち下がった直は，仕様を上方近似した性質の緩和実現可能性判定を

徐々に近似を狭めながら反復して行うことで，Safra

ムの協調性の度合いを定量化する協調性評価関数につの構成法 [16] と呼ばれる煩雑なオートマトン決定化手

いて述べる．4 章では，システムの協調性特性がその法を避ける漸進的有界合成アプローチ [17] [10] [7] が主

協調性評価関数に反映されていることを，1. 2 節の例に用いられている．本稿で与える合成手法では，このを用いて説明する．5 章では，その協調性評価関数に

漸進的有界合成アプローチを基に，Markov 決定過程

関して局所最適なシステムを合成する手法を与える．

に対する確率的モデル検査 [6] を用いて各反復ステッ

6 章では，まとめと今後の課題について述べる．

プにおいて最適なシステム（勝利戦略）を合成することで，元の仕様より強い性質を実現する局所最適なシ2 準備

ステムを得ることができる．

本章では，準備としてリアクティブシステムと環境
及びそのふるまい（相互作用）の形式的定義を与え

1. 4 関連研究

る．また，システムと環境の動作仕様を記述するため

状態数が小さいシステムは，制御構造が単純で理解の言語としてしばしば用いられる線形時相論理 LTL

し易く，また，モデル検査等の解析も容易である．そ及び実現可能性の定義も簡単に紹介する．

のため，既存の自動合成器 [11] [3] [7] では，状態数がより小さいシステムを合成しようとする．ただし，漸2. 1 リアクティブシステムと環境

進的有界合成手法で用いられる safety ゲームの最小外部環境（ユーザや外部モジュールなど）と継続的勝利戦略（システム）合成問題はゲームサイズに対しに相互作用するソフトウェア/ハードウェアは，リアて NP 完全 [12] であり，厳密な状態数最小化を伴う自クティブシステム（以下，単にシステムと呼ぶ）とし動合成の計算量クラスは伴わない自動合成の計算量クてモデル化される．システムと環境の相互作用では，

ラスより大きい．そのため，発見的手法などを用いた• システムにとっての入力は環境の出力であり，そ近似的最小化手法がいくつか提案されている [12] [8]．

の値をシステム側が制御することはできないが，また， [8] では，各近似的最小化手法の性能を比較し• システムの出力は環境にとっての入力であり，そている．

の値をシステム側が制御することができる．

一方，本研究で与える合成手法は，システムの協調

ここで，各時刻のシステムへの入力は入力原子命題性に注目してシステムを合成する．本手法では，環境

集合 API の部分集合，各時刻のシステムの出力は出仕様を満たす環境の集合の大きさやシステム仕様を

力原子命題集合 APO の部分集合で与えられるもの

満たす環境の集合の大きさに基づいた協調性評価関とする．なお，ここでは API ∩ APO = ∅ と仮定し，数に関して局所最適なシステム，即ち，状況に応じてAPI ∪ APO を AP と記す．

柔軟に対応する協調的システムを得ることができる．

このとき，システムは，過去の入力履歴から現在

また，局所最適化にはゲームサイズに対して多項式時間で計算可能な確率的モデル検査を利用することがの出力を逐次決定する応答関数 f : (2API )∗ → 2APO
（Moore 型状態遷移系）として与えることができる†4 ．

でき，協調性の局所最適化を伴う自動合成と伴わない

一方，環境は，入力列 ã ∈ (2API )ω として与えられ自動合成の計算量クラスは同じである．

る（注意 1）．
そして，システム f と環境 ã のふるまい（相互作1. 5 本稿の構成

用）behavior(f, ã) ∈ (2AP )ω は以下のように与える

2 章では，準備として，リアクティブシステムと環境及びそのふるまい（相互作用）の形式的な定義を与える．また，システムと環境の動作仕様の記述にしばしば用いられる線形時相論理 LTL とその実現可能性の定義についても簡単に紹介する．3 章では，システ†4 環境の入力とそれに対するシステムの応答を一つの時間単位とし，「過去の入力履歴」のみではなく「現在の入力情報」も用いて現在の出力を逐次決定する応答関数 f ′ : (2API )+ → 2APO （Mealy 型状態遷移系）
として定義することもある．

ことができる．

behavior(f, ã) = (ã[0] ∪ b̃[0])(ã[1] ∪ b̃[1]) . . . , (3)f (ϵ)
if i = 0,b̃[i] =(4)
f (ã[0, i − 1]) otherwise.
ただし，入力列 ã = a0 a1 . . . ∈ (2API )ω に対して，ã[i] を i 番目の要素 ai ，ã[i, j] を i 番目以降 j 番目までの部分列 ai . . . aj とする．
注意 1. なお，環境は，現在までのシステムの出力履歴の入力を逐次決定する応答関数 g : (2APO )+ → 2API
（Mealy 型状態遷移系）として定義することも可能である．ここで，ある固定されたシステム f との相互作用のみを考慮したときには，応答関数は単なる入力列と見なせる．そのため，本稿では，3 章で述べる協調性の定量化を容易にするために，環境を入力列という単純な構造として定義する．

3 協調性の定量化
本章では，リアクティブシステムの協調性の定量化
する協調性評価関数を導入する．

3. 1 協調性の基準
システムの協調性特性は様々なものが考えられるが，本研究では以下のような点を考慮してシステムの協調性を評価する．

• 環境仕様 φenv に対して，システム f は，環境集
合 SATφenv (f ) が大きいほど φenv を充足させ易い，即ち，受容性（acceptability）が高い．

• システム仕様 φsys に対して，システム f は，環境集合 SATφsys (f ) が大きいほど φsys を充足し易い，即ち，許容性（tolerability）が高い．
ただし，SATφ (f ) は以下のように定義される，シス
テム f との相互作用において φ を満たす環境の集合

2. 2 線形時相論理 LTL
線形時相論理 [14]（Linear Temporal Logic，LTL）
は，状態遷移系のふるまいの時間的性質の記述にしば（充足環境集合）である．

SATφ (f ) = {ã ∈ (2API )ω | behavior(f, ã) |= φ}.

しば用いられる，線形時間論理の一つである．LTL(7)
ここで，φenv を満たすために環境が選ぶことが出は，命題論理で用いられる通常の論理結合子に加え，来る選択肢が多くなるように配慮するシステムではnext 演算子 ⃝ と until 演算子 U の二つの時間演算子

受容性が高い．また，φsys を満たすように努力するをもつ．直感的には，⃝φ1 は「次（next）の時刻でシステムでは許容性が高い．本研究では，この二種のφ1 が成り立つ」，φ1 U φ2 は「φ2 がいつか成り立ち，充足環境集合を協調性の基準として協調性評価関数

それまでの間（until）は φ1 が成り立っている」といを与える．

う性質を表現している．また，一般的な略記として

3φ1 （≡ true U φ1 ）と 2φ1 （≡ ¬3¬φ1 ）も用いる．
そして，ふるまい σ ∈ (2AP )ω と LTL 式 φ の間の充足関係 |= も通常通りの意味で用いる．

3. 2 環境分布
シ ス テ ム f1 と f2 の 間 の 3. 1 節 の 基 準 に 基 づ
い た 協 調 性 に 関 す る 順 序 関 係 は ，充 足 環 境 集 合

ここで，どのような環境との相互作用においてもSATφenv (f1 ) と SATφenv (f2 ) （または SATφsys (f1 )LTL 仕様 φ を満たすことができるシステムが存在すると SATφsys (f2 )）の包含関係により定義できる．しかならば，かつそのときに限り，φ は実現可能 [13] [1] [15]しながら，環境集合上の包含関係は一般には半順序であるという．

関係であり，非加算無限集合である環境集合の大きさ

φ が実現可能 ⇔は単純には定量化できない．本節では，環境の集合を∃f. ∀ã ∈ (2API )ω . behavior(f, ã) |= φ.

(5)

なお，充足可能性（無矛盾性）は実現可能性より真に弱い性質である．

標本空間とする可測空間上の測度を定義することで，環境集合の大きさを定量化する．
環境の全体集合 (2API )ω は非可算無限集合であφ が充足可能 ⇔ ∃σ ∈ (2) . σ |= φ.

AP ω

(6)

るが，Markov 連鎖と同様に，筒集合から生成される筒完全加法族を用いて可測空間を定義できる．即ち，h̃ ∈ (2API )∗ を入力履歴，Cyl(h) を h̃ の筒集合

また，Unsafef (φenv ) は，システム f との相互作用に{ã ∈ (2おいて φenv の安全性成分の反例となる入力履歴の集) | h̃[i] = ã[i] for i < |h̃|}，FAPI ω

本空間 (2

API

を標

API ω

) から生成される筒完全加法族とした

とき，対 ⟨(2API )ω , F API ⟩ は可測空間となる．この可測空間上の確率測度を環境分布として定義することで，各環境の重要度を考慮して重み付けした，環境合である．

Unsafef (φenv ) ={h̃ ∈ (2API )∗ | ∀σ ∈ (2AP )ω .
((∀i < |h̃|. h̃[i] ∪ f (h̃[0, i]) = σ[i]) ⇒ σ ̸|= φenv }.
(11)

集合の大きさを規定することができる．
ここで，「各環境の重要度が等しい」という単純な仮定を反映した一様環境分布（uniform environment

distribution）UED : 2(2

API ω
)

→ [0, 1] は，形式的に

3. 3 協調性評価関数
本節では，3. 1 節で与えた協調性基準と 3. 2 節で与えた環境分布に基づいて定量化する協調性評価関数をは以下のように与えられる．

UED(Cyl(h̃)) = 2−|h̃|·|API | .

(8)

この一様環境分布 UED では，すべての環境に同じ重要度が与えられるため，環境仕様 φenv の安全性成分に反する，即ち，φenv の違反を決定付ける選択を行う環境も他の環境と同じ重要度をもつ．しかし，そのような環境の重要度を無視するという立場もあり得る．このとき，φenv の安全性成分に反する選択を行う環境の重要度を無視することで，システムの協調性評価において，φenv を明確に違反しようとする環境を除外することができる．ここで，「φenv の安全性成分に反する選択の重要度は無視できるものとし，それ以外の各選択の重要度が等しい」という仮定を反映した安全一様環境分布（safely-uniforom environment
API ω
)

env
distribution）SUEDφ: 2(2f→ [0, 1] は，形

式的には以下のように与えられる．
∏
env
SUEDφ
(Cyl(h)) =SafeProbfφenv (h̃[0, i]).
f
i<|h̃|

(9)
φenv
API ∗
ただし，SafeProbf: (2) → [0, 1] は，以下の与える．
一様環境分布 UED に基づいて環境の重要度を考慮した場合，協調性の基準にする性質 φq ∈ {φenv , φsys }に対するシステム f の一様環境充足率（uniform en-

vironment satisfaction rate）UESRφq は以下のように与えられる．

UESRφq (f ) = UED(SATφq (f )).

(12)

env
同様に，安全一様環境分布 SUEDφに基づいて環f

境の重要度を考慮した場合，システム f の安全一様環
境充足率（safety-uniform environment satisfactionrate）SUESRφq は以下のように与えられる．
env
SUESRφq (f ) = SUEDφ(SATφq (f )).
f(13)

なお，この UESRφq (f )（あるいは SUESRφq (f )）は，ふるまい behavior(f, ã) の生起確率が UED(ã)
env（あるいは SUEDφ(ã)）であるような Markov 連f鎖モデルに対する仕様 φq の確率的モデル検査 [6] により，|φq | に対して指数時間，f を Moore 型状態遷移系として表現したときの状態数に対して多項式時間で求めることができる．

ように定義される，φenv の安全性成分を満たす選択に対して等確率を割り振る関数である．

4 協調性評価関数を用いたシステム評価

env
SafeProbφ(h̃) =f

本章では，システムの協調性特性が 3. 3 節で与え
0
if |h̃| > 0 and h̃ ∈ Unsafef (φenv ),






|{h̃′ ̸∈ Unsafef (φenv ) ||h̃′ | = |h̃| ∧ (∀i < |h̃| − 1. h̃′ [i] = h̃[i])}|−1






if |h̃| > 0 and h̃ ̸∈ Unsafef (φenv ),





1
otherwise.
(10)た協調性評価関数の評価値に概ね反映されていることを，1. 2 節で挙げた環境仕様 φe（式 (1)）とシステ
ム仕様 φs （式 (2)）の含意式 φe → φs を実現するシ
ステム f1 （図 1）と f2 （図 2）及びそれらを修正したシステムを例として用いて示す．
なお，以下では，∅ を 0，{req} を 1，2API を B（= {0, 1}），環 境（∈ (2API )ω ）を B 上 の 無 限 列

（∈ Bω ）で表し，環境の集合（⊆ (2API )ω ）を B 上の

ω 正規表現を用いて表現する．

true

1. 2 節のシステム f1 (図 1). f1 は ¬φe を実現す

q s3 : res
6る，即ち，φe の違反を強いるシステムであるため，

req

f1 との相互作用において φe を満たす環境は存在し
s2 : resない．

SATφe (f1 ) = ∅.

(14)

¬req



@ ¬req@@R

よって，UESRφe と SUESRφe の評価は以下の通り

1 s1 : ¬res である．

UESRφe (f1 ) = UED(∅) = 0,e
SUESRφe (f1 ) = SUEDφf1 (∅) = 0.

(15)



(16)

req

また，f1 は，req が入力された直後でも res を返し，

図3

req

s0 : ¬res i


¬req

引き金戦略に基づいたシステム f3 ．

φs（の部分仕様 2(req → ⃝¬res)）に反するため，「常に ¬req を入力する」という φe （の部分仕様 23req）
ω

を放棄した環境 0 との相互作用においてのみ φs を性成分である．即ち，Unsafef2 (φe )Bω = B∗ 101Bω .

(23)e
安全一様環境分布 SUEDφf2 では，この φe の安全性満たす．

SATφs (f1 ) = {0ω }.

(17)

この f1 の無許容性は，UESRφs と SUESRφs の評価

成分に反する環境は無視できる．
∗
ω
ω
φe
e
SUEDφ
f2 (Unsafef2 (φe )B ) = SUEDf2 (B 101B ) = 0.

(24)でも反映されている．

UESRφs (f1 ) = UED({0 }) = 0,ωωe
SUESRφs (f1 ) = SUEDφf1 ({0 }) = 0.

(18)
(19)

1. 2 節のシステム f2 (図 2). φe に関する充足環境
集合 SATφe (f2 ) は，以下のように与えられる．

SATφe (f2 ) = Bω \ (B∗ (101Bω + 0ω + 1ω )). (20)
一様環境分布 UED では，ほとんどすべての環境が，101 を含む入力列であり，f2 との相互作用において「いずれ “res を受けたタイミングで req を送る”」という φe （の部分仕様 2(res → ¬req)）に反する動作

そのため，SUESRφe での評価は高い．
ω
φe
∗
ω
e
SUESRφe (f2 ) = SUEDφf2 (B ) − SUEDf2 (B 101B )
∗ ω
∗ ω
φe
e
− SUEDφ
f2 (B 0 ) − SUEDf2 (B 1 )= 1 − 0 − 0 − 0 = 1.

(25)

これは，f2 が，φe に従う環境に対して φe に違反することを強制しないという性質を反映している．一方，φs に関する充足環境集合 SATφs (f2 ) は，以下のように与えられる．

SATφs (f2 ) = Bω \ (B∗ (1010ω + 1ω )).

(26)

ここで，S(S)ED では，f2 との相互作用において φs

を行う．
∗

ω

UED(B 101B ) = 1.

(21)

従って，UESRφe での評価は低い．

に反する環境は無視できる．
∗
ωe
UED(B∗ 1010ω ) = SUEDφf2 (B 1010 ) = 0.

(27)

そのため，UESRφs と SUESRφs の評価は高い．

UESRφe (f2 ) = UED(SATφe (f2 ))= UED(Bω ) − UED(B∗ 101Bω )UESRφs (f2 ) = SUESRφs (f2 ) = 1.

− UED(B∗ 0ω ) − UED(B∗ 1ω )これは，f2 が，ほとんどすべての環境に対して φs を

= 1 − 1 − 0 − 0 = 0.

(22)

これは，f2 が，φe に従おうとしない環境に対して φeを満たすことを強制できないという性質を反映している．ただし，部分仕様 2(res → ¬req) は φe の安全(28)

満たすことができるという性質を反映している．以上のように，f2 は，φe の安全性成分に従うほとんどすべての環境に対して φe と φs を満すように応答するだけでなく，φe の安全性成分に従わないほとんどすべての環境に対して φs を満たすように応答できる，
頑強なシステムといえる．

f1 と f2 を組み合わせたシステム f3 (図 3). 一般に，
s2 : res

環境仕様 φenv の安全性成分とシステム仕様 φsys には依存関係がないが，環境仕様の安全性成分に反する

¬req



環境も考慮する UESRφsys と考慮しない SUESRφsys

reqが異なる値を持つシステムも存在し得る．ここで，f1
1 s1 : ¬res と f2 を組み合わせたシステム f3 を考える（図 3）．



このシステムは，引き金戦略と呼ばれる戦略に基づいており，φe の安全性成分に反する選択を引き金とし@ ¬req
@
@
R

req

req
図4

s0 : ¬res i


¬req

システム f2 （図 2）を修正したシステム f4 ．

てそれ以後 f1 と同様に応答するが，それまでの間はf2 と同様に応答する．
SATφe (f3 ) = SATφe (f2 ).

(29)

SATφs (f3 ) = Bω \ (Unsafef3 (φe )Bω + B∗ 1ω ),5 合成手続き
LTL 仕様からのリアクティブシステム合成では，(30)

Safra の構成法 [16] と呼ばれる非常に煩雑なオートマ(31)

トン決定化手法を避ける，漸進的有界合成アプローチ

このとき，UED ではほとんどすべての環境が φe の[17] [10] [7] がしばしば用いられている．本章では，そe
安全性成分に反するが，SUEDφf3 ではほとんどすべの漸進的有界合成アプローチを基に，前章で与えた協ての環境が φe の安全性成分に従う．

調性評価関数に関して局所最適なシステムを LTL 仕

Unsafef3 (φe ) = Unsafef2 (φe )ωUED(Unsafef3 (φe )B ) = 1

(32)

ω
e
SUEDφ
f3 (Unsafef3 (φe )B ) = 0.

(33)様から合成する手法を与える．

このような特性は，UESR と SUESR の評価値の違

5. 1 手続きの概略

いとして反映される．

LTL 式で与えられたシステム仕様 φsys と環境仕様(35)

φenv に対して，含意式 φenv → φsys の実現可能性判
定及び合成は，システム側プレイヤ（先手†5 ）と環境

従って，f3 は，環境が φe の安全性成分に従わない限

側プレイヤの間の展開型二人プレイヤ ω-正規ゲーム

り φs を満たすことができない，f2 より脆弱なシステの勝利戦略合成に帰着され，そのゲーム上のシステム

ムといえる．

側プレイヤの戦略は Moore 型状態遷移系，即ち，シUESRφe (f3 ) = UESRφs (f3 ) = 0,(34)

SUESRφe (f3 ) = SUESRφs (f3 ) = 1.

f2 を修正したシステム f4 (図 4). 3. 3 節で与えたステムと見なすことが出来る．よって，前章で与えた協調性評価関数では評価が等しいが，f2 をよりも協協調性評価関数に関して最適な勝利戦略を合成する

調性が高い，即ち，集合 SATφe （あるいは SATφs ）ことで，目的のシスデムを得ることができる．

がより大きいシステムも存在する．ここで，f2 の状
態 s2 において req が入力された際の出力を修正したシステム f4 を考える（図 4）．f4 との相互作用において φs を満たす環境の集合 SATφs (f4 ) は，SATφs (f2 )本研究では，漸進的有界合成アプローチに基づいた，以下のような手続きを与える（注意 2）．

1. 含意式 φenv → φsys に関する近似パラメータk ∈ N の初期値を設定する．
2. φenv → φsys と等価な，「すべての実行について

より真に大きい．

SATφs (f4 ) = Bω \ (B∗ 1ω ) ⊃ SATφs (f2 ).

(36)

受理状態を有限回しか訪れないような語を受理

しかしながら，UED と SUED では SATφs (f4 ) \する」という受理条件を持つ universal co-Büchi∗

SATφs (f2 ) （= B 1010 ）の大きさは 0 であるため，ω

オートマトン A を構成する．

UESR と SUESR ではその差を捉えることはできな

3. A の受理条件を「すべての実行について受理状

い．このような場合を除き，システムの協調性特性は†5 なお，システムを Mealy 型状態遷移系として定義した場合（†4）には，システム側プレイヤが後手である．

協調性評価関数の評価値に概ね反映されている．

態を高々k 回しか訪れないような語を受理する」

注意 2. なお，本手法のステップ 1-6 は半決定手続き

上方近似したオートマトン Ak の受理言語に対であり，実現可能である場合には有界時間で合成可能

応するプレイにおいてシステム側（先手）が勝利であるが，実現不能である場合には停止しない．通する safety ゲーム Gk を構成する．

常，漸進的有界合成アプローチでは，ステップ 2-5

4. Gk 上のシステム側プレイヤの勝利領域を求める．

と平行して，漸進的有界実現不能判定を行う補手続

5. Gk の初期状態が勝利領域に含まれないとき，

きを実行することで，実現可能でない場合にも有界

k := k + 1 としてステップ 2-5 を繰り返す．含ま

時間で停止することを保証する．この補手続きは，れる（即ち，実現可能である）とき，Gk から勝システムと環境の立場を入れ替えた状況下における利領域でない部分を取り除く．

¬(φenv → φsys ) の実現可能性判定手続きであり，具6. Gk 上の協調性評価値（一様環境充足率 UESRφq
あるいは安全一様環境充足率 SUESRφq ）に関して最適なシステム（勝利戦略）fk を合成し出力する．

• 最適システム合成手続きの詳細は 5. 2 節で述べる．
本合成手続きのステップ 1-5 は，通常の漸進的有界合成手続きと同様である．ここで，ステップ 2 において構成されるオートマトン A は，状態数が |φenv → φsys |体的には，ステップ 2-5 を，• 入力原子命題集合 API と出力原子命題集合 APOを交換し，• ステップ 2 のオートマトンを「¬(φenv → φsys )」と等価となるように構成し，• ステップ 3 の safety ゲームを「システム側プレイヤが後手」となるように構成し，• ステップ 5 において，「初期状態が勝利領域に含まれるとき，実現不能と判定する」

に対して指数オーダーとなるように構成できる．スように変更した手続きである．

テップ 3 において構成される Gk は，（k が小さいほ注意 3. 含意式のサイズ |φenv → φsys | に対して，本ど）φenv → φsys よりも強い性質を勝利条件として持手法のステップ 2-5 とその補手続き（注意 2）によるつ．従って，Gk 上でシステム側プレイヤが勝利戦略

自動合成の計算量は二重指数時間である．また，スに従う任意のふるまいは φenv → φsys を満たす．まテップ 6 の計算量も二重指数時間である（5. 2 節参た，Gk は，Ak の決定化，及び，入出力の分割により，照）．従って，本自動合成手続き全体の計算量も二重状態数が |φenv → φsys | に対して二重指数オーダーと指数時間となる．

なるように構成できる．Ak は safety オートマトンへ

一方，既存の漸進的有界合成手法 [17] [10] [7] では，容易に変換可能であるため，この決定化には Safra のステップ 6 において状態数がより小さいシステムを構成法ではなく冪集合構成法を用いることができる．

合成しようとする．ただし，safety ゲーム上の状態数

なお，ステップ 6 で合成されるシステムは，状態空間最小の勝利戦略合成問題はゲームサイズに対して NP及び遷移関係を Gk に制限した場合には最適ではある

完全 [12] であり，状態数を厳密に（局所）最小化するが，大域的最適である保証はない．

漸進的有界合成手続き全体の計算量は非決定性二重ここで，ステップ 6 において得られたシステムをそ

指数時間である．

のまま出力するのではなく．必要に応じて k := k + 1としてステップ 2-6 を繰り返してもよい．その際の手

5. 2 最適システムの合成

続きを継続する条件としては，例えば，以下のような環境側プレイヤの選択のすべてに確率が振られたものが挙げられる．

ゲームは，システム側プレイヤの非決定的な選択に対• k が予め設定した下限値未満である．

して次の遷移先が確率的に決定される Markov 決定• fk の協調性評価値が目標閾値未満である．

過程（MDP）と見なせる．また，MDP モデルに対• fk の協調性評価値が fk−1 の協調性評価値よりする確率的 LTL モデル検査問題 [6] は，LTL 仕様を大きい．

満たすふるまいの生起確率を最大化（あるいは最小化）する戦略を求める問題と見なせる．

を合成できる．

システム側の勝利領域のみからなる safety ゲーム
ではゲーム上のすべてのふるまいでシステム側が勝利するため，勝利領域のみから成るゲーム上の環境
側選択に対して環境分布 UED あるいは SUED に従

1. 環境仕様 φenv の安全性成分と等価な決定性
safety オートマトン B を構成する．
2. B とゲーム Gk の同期合成ゲームを MDP MBkに変換する.

う確率を割り当て MDP と見なし，その MDP に対• ここでは，同期合成ゲーム上の環境が遷移する φq ∈ {φenv , φsys } の確率的モデル検査により，先を決定する各状態において，B の受理状

UESRφq あるいは SUESRφq に関して最適なシステ

態集合に留まることが可能な n 個の入力にム（勝利戦略）を合成できる．

確率 1/n，その他の入力に確率 0 を割り当

なお，MDP モデルに対する確率的 LTL モデル検査の計算量は，LTL 仕様のサイズに対して二重指数
時間，モデルのサイズに対して多項式時間である [6]．

てる．

– ただし，n = 0 のとき，すべての入力に確率 2−|API | を割り当てる．

3. MDP MB
k 上で φq を満たす最大確率を与える

5. 2. 1 UESR に基づいた最適化
一様環境充足率 UESR は一様環境分布 UED に基づいて定義されているため，前節のゲーム Gk 上の環戦略（システム）fk を確率的 LTL モデル検査によって計算し出力する．

境側の各選択に等確率を割り当てた MDP 上の φq を

なお，safety オートマトンは，受理状態集合上を常満たす最大確率を与える戦略が，状態空間及び遷移関に遷移し続ける語を受理するオートマトンである．任係を Gk に制限した範囲での，UESRφq の最大値を与意の時間論理式 φ に対して，φ の安全性成分と等価えるシステムである．従って，以下のような手続きにな safety オートマトンは，（1）φ と等価な Büchi オーより，目的のシステムを合成できる．

トマトンを構成し，（2）その受理状態集合に無限にし

1. ゲーム Gk を MDP Mk に変換する.

ばしば到達可能な状態集合を新たに受理状態集合に• ここでは，Gk 上の環境が遷移先を決定するすべての状態について，各入力に確率 2−|API |

を割り当てる．

2. MDP Mk 上で φq を満たす最大確率を与える
戦略（システム）fk を確率的 LTL モデル検査によって計算し出力する．
なお，fk の状態数は，φq と等価な決定性オートマ
トンの状態数以下であり，|φq | に対して二重指数オー

変更することで得られる．safety オートマトンは冪集合構成法により決定化可能であり，φ の安全性成分と等価な決定性 safety オートマトンは状態数が |φ| に対して二重指数オーダーとなるように構成できる.
従って，fk の状態数は，φq と等価な決定性オート
マトンの状態数と φenv の安全性成分と等価な決定性

safety オートマトンの状態数の積以下であり，|φq | と|φenv | に対して二重指数オーダーである．

ダーである．

5. 2. 2 SUESR に基づいた最適化

6 おわりに

安全一様環境充足率 SUESR は安全一様環境分布

本研究では，外部環境と継続的に相互作用するリ

SUED に基づいて定義されているため，「環境仕様

アクティブシステムの協調性を定量化するいくつか

φenv の安全性成分と等価な決定性 safety オートマトの評価関数を導入した．これらの協調性評価関数は，

ン B 」と前節のゲーム Gk の同期合成ゲームの「B のシステムとの相互作用において環境仕様を満たす環

受理状態集合に留まるための環境選択」に等確率を境の集合の大きさやシステム仕様を満たす環境の集割り当てた MDP 上の φq を満たす最大確率を与える

合の大きさを，確率論的な観点から想定した環境分布

戦略が，状態空間及び遷移関係を Gk に制限した範囲に基づいて定量化しており，システムの協調性特性をでの，SUESRφq の最大値を与えるシステムである．

概ね反映した定量的評価を与えることができる．

従って，以下のような手続きにより，目的のシステム

また，導入した協調性評価関数に関して局所最適なシステムを合成する手法を提案した．本合成手法では，リアクティブシステムの自動合成においてしばしば用いられる漸進的有界合成手法を基に，システムと環境との相互作用をモデル化した Markov 決定過程
に対する確率的モデル検査を用いてシステムを最適化する．これにより，既存の自動合成器によって合成され易い，環境仕様の違反を強いるシステムや環境仕様に少しでも違反した際にシステム仕様を放棄してしまうシステムではなく，環境仕様やシステム仕様を満たし易い協調的なシステムを得ることができる．
今後の課題としては，以下のようなものが挙げられる．

• 本合成手法の実装及びベンチマーキング• 本研究とは異なる協調性基準や環境分布に基づいた協調性評価関数の開発• 効率的な最適化を可能とする協調性評価関数の開発• 発見的手法などを用いた近似最適化手法の開発• 入力列環境から応答関数環境への拡張• 環境が個別に仕様（目的）を持つ複数主体からなる場合への拡張

参 考 文 献[ 1 ] Abadi, M., Lamport, L., and Wolper, P.: Realizable and Unrealizable Specifications of Reactive Systems, Automata, Languages and Programming, Ausiello, G., Dezani-Ciancaglini, M., andDella Rocca, S.(eds.), Lecture Notes in Computer
Science, Vol. 372, Springer Berlin / Heidelberg,
1989, pp. 1–17.
[ 2 ] Ball, T., Levin, V., and Rajamani, S. K.: A
Decade of Software Model Checking with SLAM,
Commun. ACM, Vol. 54, No. 7(2011), pp. 68–76.
[ 3 ] Bohy, A., Bruyére, V., Filiot, E., and Raskin, J.F.: Synthesis from LTL Specifications with MeanPayoﬀ Objectives, Tools and Algorithms for theConstruction and Analysis of Systems, Piterman,
N. and Smolka, S.(eds.), Lecture Notes in Computer Science, Vol. 7795, Springer Berlin Heidelberg, 2013, pp. 169–184.
[ 4 ] Clarke, E. M., Emerson, E. A., and Sistla, A. P.:
Automatic Verification of Finite-State Concurrent
Systems Using Temporal Logic Specifications, ACM
Trans. Program. Lang. Syst., Vol. 8, No. 2(1986),
pp. 244–263.
[ 5 ] Clarke, E. M., Grumberg, O., and Peled, D. A.:

Model Checking, The MIT press, 2000.
[ 6 ] Courcoubetis, C. and Yannakakis, M.: The
Complexity of Probabilistic Verification, J. ACM,
Vol. 42, No. 4(1995), pp. 857–907.
[ 7 ] Ehlers, R.: Symbolic Bounded Synthesis, Computer Aided Verification, Touili, T., Cook, B., andJackson, P.(eds.), Lecture Notes in Computer Science, Vol. 6174, Springer Berlin / Heidelberg, 2010,
pp. 365–379.
[ 8 ] Ehlers, R. and Moldovan, D.: Sparse Positional Strategies for Safety Games, Proceedings
First Workshop on Synthesis, Berkeley, California, USA, 7th and 8th July 2012, Peled, D. andSchewe, S.(eds.), Electronic Proceedings in Theoretical Computer Science, Vol. 84, Open Publishing
Association, 2012, pp. 1–16.
[ 9 ] Emerson, E. A.: Temporal and Modal Logic,
Handbook of Theoretical Computer Science, Vol. B,
Elsevier, 1995, pp. 995–1072.
[10] Filiot, E., Jin, N., and Raskin, J.-F.: An
Antichain Algorithm for LTL Realizability, Computer Aided Verification, Bouajjani, A. and Maler,O.(eds.), Lecture Notes in Computer Science,Vol. 5643, Springer Berlin / Heidelberg, 2009,
pp. 263–277.
[11] Jobstmann, B. and Bloem, R.: Optimizations for LTL Synthesis, Formal Methods in Computer Aided Design, 2006. FMCAD ’06, nov. 2006,
pp. 117 –124.
[12] Neider, D.: Small Strategies for Safety Games,
Automated Technology for Verification and Analysis, Bultan, T. and Hsiung, P.-A.(eds.), Lecture
Notes in Computer Science, Vol. 6996, Springer
Berlin Heidelberg, 2011, pp. 306–320.
[13] Pnueli, A. and Rosner, R.: On the Synthesis of a Reactive Module, Proceedings of the 16th
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89, New
York, NY, USA, ACM, 1989, pp. 179–190.
[14] Pnueli, A.: The Temporal Logic of Programs,
Foundations of Computer Science, 1977., 18th Annual Symposium on, 31 1977-nov. 2 1977, pp. 46–57.
[15] Rosner, R.: Modular Synthesis of Reactive Systems, PhD Thesis, Weizmann Institute of Science,
1992.
[16] Safra, S.: On the Complexity of Omega Automata, Proceedings of the 29th Annual Symposium
on Foundations of Computer Science, SFCS ’88,
Washington, DC, USA, IEEE Computer Society,1988, pp. 319–327.
[17] Schewe, S. and Finkbeiner, B.: Bounded Synthesis, Automated Technology for Verification andAnalysis, Namjoshi, K., Yoneda, T., Higashino, T.,
and Okamura, Y.(eds.), Lecture Notes in Computer Science, Vol. 4762, Springer Berlin Heidelberg, 2007, pp. 474–488.