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

LTL 式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装に関する研究
上野 篤史

望月 翔平

島川 昌也

萩原 茂樹

米崎 直樹

オープンなシステムは一般に，環境からの入力に対して出力を返すという相互作用を維持し続けるリアクティブシス
テムとしてモデル化される．リアクティブシステムの動作仕様を形式的に記述し，仕様を満たすシステムが存在するかどうかを調べシステムを合成する，実現可能性判定というという手法が研究されている．本研究では，リアク
ティブシステム仕様の高速な実現可能性判定器を実装した．実現可能性判定では，ω オートマトンの決定化がなされ，セーフティゲームと呼ばれる構造に変換される．この決定化のコストを削減するためにオートマトンの遷移表現にBDDP S という二分決定グラフを利用する．二分決定グラフは部分グラフ中の等価なノードを共有でき，決定化の際はノード同士の単一な演算を行うため，計算結果を再利用しやすく，また等価なノードが共有される性質を利用し，途中で生成されるターンベースオートマトンの状態数の削減も行った．実装段階では，演算の結果のキャッシュや等価なノードを素早く見つける必要があり，ハッシュテーブルを用いることで高速化を図った．実験では，他の高速な判定器と速度の比較を行った．その結果，本判定器はそれらに引けを取らない性能であることを確認した．

(Linear Tempral Logic, LTL) で与えるが，計算量の1 はじめにオーダーが二重指数であるという問題があり，一般に安全性が求められるシステムは，その動作が仕様を実現可能判定器は簡単な仕様しか扱うことができな満たすように構築されなくてはならない．オープンない．そのため，実際のシステムの複雑な仕様を現実的システムは一般的に，環境からの入力に対して出力をな時間で計算するためには，高速化が求められる．

返すという相互作用を維持し続けるリアクティブシ

リアクティブシステム仕様の実現可能性判定は環ステムとしてモデル化される．リアクティブシステム

境とシステム間のゲームに勝利戦略があるかどうか

は，環境からの任意の入力に対して適切に出力するよの判定とみなすことができる．システムは環境からうに制御されなくてはならないため，その構築が非常の入力に対応して出力を返し，環境はシステムの出に難しい．そこで，仕様を形式的に記述し，仕様を満力に対応して入力を返すという振る舞いを繰り返す．

たすシステムが存在するかどうかを調べ，存在するな

その振る舞いが仕様を満たす場合，システムの勝利，らば自動的に合成する，実現可能性判定というという仕様を満たさないときは環境の勝利となる．どんな入手法が研究されている．実現可能性判定によって合成力の履歴に対してもシステムが勝てるような次の出されたシステムは，仕様を満たすことが保証されてい力が一意に決まるとき，システム側には勝利戦略がある．一方，実現可能性判定は，仕様を線形時相論理式

るという．システム側に勝利戦略があるとき，仕様は実現可能である．また，仕様を満たすシステムを勝利

Eﬃcient Implcation of Checknig Realizability of LTL
Specification
Atsushi Ueno, Shohei Mochizuki, Masaya Shimakawa,
Shigeki Hagihara, Naoki Yonezaki, 東京工業大学大学
院情報理工学研究科計算工学専攻, Dept. of Information and Computer Science, Graduate School of Information Science and Engineering,Tokyo Instituteof Technology..

戦略を基に合成することが可能である．
実現可能性判定と合成問題を解く古典的なアルゴ
リズムは，ω オートマトンの決定化に Safra の決定化手続き [11] を用いるものだった．しかし，この手続きは実装が非常に難しく，Safra の決定化手続きを用いない，Safraless な手法 [9] が提案された．この手法

は，主に以下のような手順を踏む．

1. 仕様を universal coBüchi オートマトンに変換する．

2 リアクティブシステム仕様と実現可能性
リアクティブシステムとは，外部環境からの制御で2. universal coBüchi オートマトンの状態をシス

きない入力と内部システムの制御可能な出力の相互

テム側と環境側に分けた，ターンベースオートマ

作用を維持しているシステムのことである．リアク

トンにする．

ティブシステム仕様とは，リアクティブシステムの振3. universal coBüchi オートマトンを universal k-

る舞いが満たすべき性質のことである．リアクティブ

coBüchi オートマトンとしてみて，サブセット構システムの振る舞いは，有限なリテラルの集合の無限成法で決定化する．

列として表されるので，リアクティブシステムの仕様

4. 決定化されたオートマトンをセーフティゲーム

は LTL 式で記述できる．本節では，対象とするリアと見て，勝利戦略があるかどうかを判定する．

クティブシステムの形式的定義と動作仕様に関する諸その結果，様々な Safraless な手法とそれを基にした定義を与える．これらの定義は [13] を基にしている．

実現可能判定器（Acacia+ [1]，Lily [3]，Unbeast [4] など）が作られた．これらの判定器は非常に高速である

2. 1 リアクティブシステム

が，現実規模の複雑な仕様の判定には時間がかかるとリアクティブシステムは，三つ組RS = ⟨I, O, r⟩でいう問題が依然として残っている．

表される．

本研究では，実現可能性判定器の新しい実装方法

1. I は入力信号の有限集合である．入力信号とは，を提案し，高速化することを目的とする．実現可能システムの外部環境から入力される信号のことで性判定では，サブセット構成法でオートマトンの決ある．あるタイミングの入力信号は複数存在して定化がなされ，4. でセーフティゲームと呼ばれる構もよい．タイミングごとの入力信号の集合をタイ造に変換される．このセーフティゲームの状態数がミング順に並べた列を入力信号集合列と呼ぶ．入二重指数オーダーで増えていくことが，実現可能性

力信号集合列は，有限列もしくは無限列である．

判定のボトルネックになっている．そこで，決定化の

2. Oは出力信号の有限集合である．出力信号とは，コストを削減するためにオートマトンの遷移表現に，システムが外部環境へ出力する信号のことであ安藤らが提案したBDDP S [12] を利用する．決定化にる．入力信号と同様，あるタイミングの出力信号は単一の演算のみが使われる点，似たBDDP S の構造は複数存在してもよい．タイミングごとの出力信が多くできる点から，演算結果のキャッシュ化が有効号の集合をタイミング順に並べた列を入力信号である．さらに，等価なノードが共有される性質を利集合列と呼ぶ．出力信号集合列は，有限列もしく

用すると，ターンベースオートマトンへの変換後のは無限列である．

状態の数を簡単に小さくできる．実装では，演算の結3. r : (2I )∗ → 2O はリアクティブシステムの動作

果のキャッシュや等価なノードを素早く見つけるためを規定する関数で，リアクション関数と呼ぶ．こに，ハッシュテーブルを用いるなどの工夫をした．まのリアクション関数は，あるタイミングまでの有た，セーフティゲームの遷移先の表現にBDDP S をそ

限長の入力信号集合列から，そのタイミングでリのまま適用することができないので，適用できるよアクティブシステムが出力すべき出力信号集合をうに改良を加えた．実験では，Acacia+，Lily などの決定する関数である．

実現可能性判定器と性能を比較評価した．その結果，

2. 1. 1 振る舞い

本実装の判定器は世界最速の判定器に引けを取らな

リアクティブシステムの振る舞いを次のように定い性能であることを確認した．

義する．ある入力信号集合列 ωi = i0 i1 i2 . . . に対するリアクティブシステムRS = ⟨I, O, r⟩の振る舞いを

簡単のために，動作仕様 ⟨I, O, ϕ⟩ を単に仕様 ϕ と

bhvr(r, ωi )と表し，bhvr(r, ωi ) = (o0 ∪ i0 )(o1 ∪ i1 )(o2 ∪ i2 ) . . .

いうことがある．

と定める．ただし，o0 = r(ε), ok = r(i0 i1 i2 . . . ik−1 )(1 ≤ k)とする．

2. 3 実現可能性
実現可能性とは，環境がどのような入力をしても，仕様を満たすような出力をし続けるようなリアクティ

2. 2 リアクティブシステム仕様

ブシステムが存在するかどうかを表す性質である．

リアクティブシステムの入力信号や出力信号を命題変数と見なすと，リアクティブシステムの振る舞いは条件 (1) を満たす r が存在するとき，仕様 ϕ は実現可能であるという．

∀ωi ∈ (2I )ω bhvr(r, ωi ) |= ϕ

命題変数の無限列として扱うことができる．本稿では，この振る舞いの仕様記述に時相論理式 (LTL) を
用いる．

(1)

ま た ，条 件 (1) を 満 た す r が 存 在 し な い と き ，仕様 ϕ は実現不可という．リアクティブシステム

2. 2. 1 LTL 式の構文

RS = ⟨I, O, r⟩ を仕様 ϕ の実現と呼び，実現を一つP rop を命題変数の有限集合とする．集合 P rop 上

具体的に求めることを合成という．

の LTL 式は以下のように定義される．

3 実現可能性判定アルゴリズム
ϕ ::= p|¬ϕ|ϕ ∨ ϕ|ϕ ∧ ϕ|Xϕ|ϕU ϕ|ϕRϕただし，p ∈ P rop である．

Schewe ら [10] と Filiot ら [7] が提案した手法により，実現可能性を判定する．この章では，定義 3. 1. 2

2. 2. 2 LTL 式の意味

で実現可能性とオートマトンの受理言語の関係を説

LTL 式 ϕ と無限列 w = σ0 σ1 . . . ∈ (2P rop ω) の充明する．そして，節 3. 2 でオートマトンをセーフティ

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

ゲームへ変換し，項 3. 2. 4 で実現可能性判定問題と1. w |= p ⇐⇒ p ∈ σ0

セーフティゲームの勝利戦略存在問題の関係を説明

2. w |= ¬ϕ ⇐⇒ w ̸|= ϕ

する．

3. w |= ϕ1 ∨ ϕ2 ⇐⇒ w |= ϕ1 or w |= ϕ2
4. w |= ϕ1 ∧ ϕ2 ⇐⇒ w |= ϕ1 and w |= ϕ2

3. 1 オートマトン

5. w |= Xϕ ⇐⇒ σ1 σ2 . . . |= ϕ

3. 1. 1 定義

6. w |= ϕ1 U ϕ2 ⇐⇒ ∃k ≥ 0(σk σk+1 . . . |= ϕ2

オートマトンの遷移はリテラルの論理積でラベルand ∀i(0 ≤ i < k)σi σi+1 . . . |= ϕ1 )7. w |= ϕ1 Rϕ2 ⇐⇒ ∀k ≥ 0(σk σk+1 . . . |= ϕ2 or∃i(0 ≤ i < k)σi σi+1 . . . |= ϕ1 )付けされる．リテラルとは信号もしくは信号の否定である．O上のリテラルの全ての論理積の集合を C(O)と表す．ΣO = 2O ，ΣI = 2I とする．どんな論理積

また，

ψ と文字 σ ∈ ΣO に対しても，文字 σ が ψ を満たす

1. true ≡ p ∨ ¬p

とき，σ |= ψ と書く．C(I) も同様にして定義され2. f alse ≡ ¬true

る．入力と出力は分けて考えるので，オートマトン

3. ♢ϕ ≡ trueU ϕはターンベースである必要がある．オートマトンは

4. □ϕ ≡ ¬♢¬ϕ

組 A = ⟨Σ, Q = QI ⊎ QO , q0 , F, δ⟩ で表される．こと略記する．

こで，Q は QI と QO に分けられた状態の有限集合

2. 2. 3 動作仕様

で，q0 ∈ Q は初期状態，F ⊆ Q は終了状態の集合，

リ ア ク ティブ シ ス テ ム の 動 作 仕 様 は ，三 つ 組

δ ⊆ Q×C(O)×QI ∪QI ×C(I)×QO は遷移関係であ⟨I, O, ϕ⟩ で表される．ここで，ϕ は I ∪ O に含まる．また，δ̄ = {(q, σ, q ′ ) | ∃ψ(q, ψ, q ′ ) ∈ δ ∧ σ |= ψ}れる命題変数からなる LTL の式である．

とする．無限語 ω = (o1 ∪ i1 )(o2 ∪ i2 ) . . . ∈ Σω 上の A

のランは状態の無限列 r = p1 q1 p2 q2 . . . ∈ (QO QI )ω

2. f (q) = i(0 ≤ i ≤ k)：q で終わるランが存在し，である ．ただし，p1 = q0 であり，全ての j ≥ 1

かつ q で終わるランのうちで最も多く終了状態に対して (pj , oj , qj ) ∈ δ̄ ，(qj , ij , pj+1 ) ∈ δ̄ である．

を通る回数が i 回である．

occr (q) ∈ N + {+∞} をラン r 中に q が起きた回数と

3. f (q) = k + 1：q で終わるランが存在し，かつする．coBüchi オートマトンにおけるランの受理条件

q で終わるランのうちで最も多く終了状態を通るは次のようになる．

回数が k + 1 回もしくはそれ以上である．
となる．この関数をカウント関数と呼ぶ．

∀q ∈ F (occr (q) ∈ N)

状態が QO と QI に分けられたターンベースなA の ω 上の全てのランが coBüchi の受理条件を

オートマトンを決定化するため，カウント関数も満たすとき，ω は universal coBüchi によって受理さ

fO : QO → {−1, 0, 1, . . . , k, k + 1} と fI : QI →れる．

{−1, 0, 1, . . . , k, k + 1} に分けられる．fO の集合を

また，k-coBüchi(k ∈ N) におけるランの受理条件
は次のようになる．

FO と表し，fI の集合を FI と表す．
(A, k) を 基 に 構 築 さ れ る セ ー フ ティゲ ー ム を 組
G(A, k) = (FO , FI , f0 , succ, Saf e) で表す．ここで，∀q ∈ F (occr (q) ≤ k)

全ての f ∈ FO ∪ FI ，σ ∈ Σ についてカウント関数

A の ω 上の全てのランが k-coBüchi の受理条件をの遷移先 succ(f, σ) を次のように定義する．∀q ∈ Q

満たすとき，ω は universal k-coBüchi によって受理について，される．また，組 (A, k) を universal k-coBüchi オー

succ(f, σ)(q)=max{min(k + 1, f (p) + 1(q∈F ) )| (p, σ, q) ∈ δ, f (p) ̸= −1}

トマトンと呼ぶ．

(4)

universal coBüchi の受理条件でオートマトン A

ただし，q ∈ F なら 1(q∈F ) = 1 であり，q ̸∈ F ならによって受理される語の集合を LU C (A)，universal

1(q∈F ) = 0 である．初期状態 f0 を次のように定義

k-coBüchi の受理条件でオートマトン A によって受する．

理される語の集合を LU kC (A) と表す．

3. 1. 2 Aϕ と実現可能性に関する定理
全ての LTL 式 ϕ に対して，次を満たすオートマト
ン Aϕ と K ∈ N が存在する [10] [7]．

1. LU C (Aϕ ) = {ω | ω |= ϕ}
−1 (q ̸= q0 )

f0 (q) = 0(q = q0 ∧ q ̸∈ F )




1
(q = q0 ∧ q ∈ F )Saf e は k + 1 に到達していないカウント関数の集2. ϕ が実現可能 ⇐⇒ (Aϕ , K) が実現可能．

合である．すなわち，Saf e = {f ∈ FO ∪ FI | ∀q ∈ただし，(A, k) が実現可能であるとは，以下を満たQO ∪ QI , f (q) = k + 1} である．

す r が存在することである．

簡単のため，G(Aϕ , k) を単に G(ϕ, k) と書くこと∀ωi bhvr(r, ωi ) ∈ LU kC (A)O(|A|)

また，K のオーダーは 2(2)である．ここで，| A |はオートマトン A の状態数を表す．

がある．

3. 2. 2 勝利戦略構築された G(Aϕ , k) を環境とシステム間のゲームと見なす．環境側は入力を，システム側は出力を交互

3. 2 セーフティゲームにプレイする．プレイヤー１は f (q) = k + 1 を含むよ

3. 2. 1 定義

うなカウント関数の状態を避け続け，Saf e 内に居続け

セーフティゲームの状態を関数ることができれば勝利する．この概念を勝利戦略といf : Q → {−1, 0, 1, . . . k, k + 1}
で表す．ここで，f (q) の値は，1. f (q) = −1：q で終わるランが存在しない．

(3)

う．プレイヤー１の戦略とは，マップ λ : FO → 2ΣO
であり，全ての f ∈ FO について，λ(f ) ̸= ∅ である．
これがもし，reach(λ) ⊆ Saf e であれば，λ は勝利戦

略であるという．ただし，reach(λ) は戦略 λ によっ前述の通り，k の値が大きいと G(ϕ, k) は非常に大て初期状態 f0 から到達可能なカウント関数の集合できくなるため，実際の実現可能性判定は k ≤ K の範あり，次のように定義される．

囲で k を徐々に大きくしていき，G(ϕ, k) の勝利戦略

reach(λ) は次を満たす最小の集合である．全てのカウント関数 f と全ての σ ∈ Σ について，の有無を判定するという手法をとる．

3. 3. 3 実現不可の判定

1. f0 ∈ reach(λ)

仕様 ϕ が実現可能ではないことを判定するために

2. f ∈ FO ∩ reach(λ) か つ σ ∈ λ(f ) な ら ば ，succ(f, σ) ∈ reach(λ)

は，セーフティゲーム G(Aϕ , k) の k の値を K まで
大きくすればよい．しかし，一般に K の値は巨大に3. f ∈ FI ∩ reach(λ) か つ σ ∈ ΣI な ら ば ，なるので，実際のアルゴリズムはこの方法を採用しな

succ(f, σ) ∈ reach(λ)

い．代わりに，次のような特性を利用する．仕様 ϕ が

3. 2. 3 勝利戦略の探索

システム側にとって実現可能でないならば，仕様 ¬ϕ

セーフティゲーム中の勝利戦略を求めるアルゴリ

が環境側にとって実現可能である．仕様 ¬ϕ が環境側

ズムは [7] で提案されている．W0 = Saf e として，にとって実現可能であるとは，システムの任意の出力

Wi+1 を Wi から次の手順で帰納的に求める．Wi にの履歴に対しても，¬ϕ を満たすような環境側の勝利含まれる状態への遷移が存在するようなカウント関数

戦略が存在することである．仕様 ¬ϕ の環境側の実現

f ∈ (FO ∪ Wi ) の集合，および，全ての遷移が WO

可能性判定は，システム側の場合と同様に G(¬ϕ, k)に含まれるようなカウント関数 f ∈ (FI ∪ Wi ) の集を構築し，環境側の勝利戦略を探索する．実際の計算

合，それら両者の和集合を Wi+1 とする．Wi+1 を帰では G(ϕ, k) と G(¬ϕ, k) を k を増やしつつ並行に判納的に求めていき，不動点 Wi = Wi+1 で，Wi に初定することで，k = K に達する前に実現可能かどう期状態 f0 が含まれていれば，勝利戦略が存在する．

かが分かる場合が多い．

また，全ての f ∈ F について λ(f ) ⊆ Wi となる戦略

4 実装

λ は勝利戦略である．
3. 2. 4 実現可能性と勝利戦略の関係

本章では，実現可能性判定器の実装について説明∀k ∈ N において，(Aϕ , k) が実現可能 ⇐⇒ セー
フティゲーム G(Aϕ , k) に勝利戦略が存在する．

する．本研究では，既存のツールにより LTL 式から変換された universal k-coBüchi オートマトンと入力

ϕ が実現可能かどうかを調べるには，G(Aϕ , K) の信号，出力信号の読み込みから実現可能性判定するところまでを C++を用いて実装した．この実装では勝利戦略の有無を調べればよい．

Acacia+と同様にセーフティゲームへ帰着する構造を
3. 3 実際に使われるアルゴリズム利用する．Acacia+はセーフティゲームを具体的に計G(Aϕ , K) の構築は，K の値が仕様に対して指数的な大きさであり，G(Aϕ , K) の状態数は O(K|Aϕ |算せずに反鎖 (antichain) と呼ばれる抽象的な構造に)の落とし込み，勝利戦略を計算する際に具体的な計算

オーダーの大きさであることから困難である．そこをするという手法をとっている．一方，本実装は先にで，実際の判定には次の性質 [10] [7] を利用する．

セーフティゲームを具体的に計算してから，勝利戦略

3. 3. 1 k の大小関係と実現可能性に関する定理

を計算する．

全ての ∀k1 ∈ N，∀k2 ∈ N において，k1 < k2 かつ(A, k1 ) が実現可能ならば，(A, k2 ) が実現可能．
このことより，次の性質 [10] [7] がいえる．

4. 1 BDDP S
本稿では，オートマトンの決定化のコストを削減

3. 3. 2 実現可能性に関する性質するために，ある状態からの遷移先をBDDP S で表現ϕ が実現可能 ⇐⇒ ∃k ≤ K.G(ϕ, k) に勝利戦略がする．BDDP S は安藤らがオートマトンの遷移先を表ある．

現するために [12] で提案した手法であり，終端ノード

は状態の集合でラベル付けされる．BDDP S は等価な部分式を共有でき，簡単に論理和演算ができるという特徴をもつ．またBDD 演算の途中式をキャッシュし，再利用できるため，同じ計算を何度もする必要が無い．

4. 1. 1 BDDP S の定義
BDDP S は，一般的なBDDと同様に二分決定グラ
図1

フである．非終端ノードは入力変数および出力変数にあるオートマトンの状態 P0 の遷移

よってラベル付けされ，終端ノードは遷移先の状態の集合によりラベル付けされる．根ノードから終端ノードから終端ノードへのパス中に現れる非終端ノードの編集順序は固定されており，任意の出力変数はどの
入力変数よりも先に現れる．

4. 1. 2 BDDP S の実装
BDDP S のノードの集合を N とし，非終端ノード
n を組 (low, high, val) で表す．ここで，low ∈ N ，high ∈ N であり，val は対応する命題変数ラベルの順序を表す整数値である．
２ つ の 終 端 ノ ー ド を 引 数 に とって 新 し い 終 端
ノ ー ド を 返 す ２ 項 演 算 OP と ，２ つ の ノ ー ド

図2

BDDP S による遷移先の表現

n1 (low1 , high1 , val1 ) と n2 (low2 , high2 , val2 ) を引数
にとって新しい非終端ノードを返す，OP に対応する
２項演算 op は次のように再帰的に計算される．

れる．
また，本実装では，既存の等価なノードや計算結

op(n1 , n2 ) =果を素早く見つけるために，ハッシュテーブルを用

1. n1 と n2 が終端ノードのときいた．

OP (n1 , n2 )2. val1 = val2 のとき

4. 2 セーフティゲームの構築(op(low1 , low2 ), op(high1 , high2 ), val1 )LTL 仕様 ϕ をセーフティゲームに変換する手順は

3. val1 < val2 または，n2 のみが終端ノード

次の通りである．まず，ϕ を等価な universal coBüchi(op(low1 , n2 ), op(high1 , n2 ), val1 )4. val1 > val2 または，n1 のみが終端ノード(op(n1 , low2 ), op(n1 , high2 ), val2 )オートマトンに変換する．本実装では，この変換は既存のツールにさせる．そして，universal coBüchi オー
トマトンの遷移先 (図 1) を (図 2) のようにBDDP S

決定化の際にノード n1 と n2 の和集合を計算する．

で表し．それを利用して (図 3) のように新しい状態

和集合も上記と同様に再帰的に計算されるので，決定を遷移の間に差し込むように追加することで，ターン化の速度は演算 op(n1 , n2 ) の速度に依存する．そのた

ベースオートマトンに変換する．その後，k を適当なめ，op(n1 , n2 ) の計算結果をキャッシュして再利用す値に設定し，universal k-coBüchi オートマトンとみる方法が非常に有効である．ある例では，キャッシュ

なして決定化を行う．

のヒット率が全体の 3/4 以上であった．キャッシュされた計算が再利用された場合，再帰的な計算はそこで止まるので，実際にはそれよりも多くの計算が省略さ

4. 2. 1 BDDP S を用いたターンベースオートマト

図3

変換後のターンベースオートマトン

ンへの変換

BDDP S で遷移先を表現されたオートマトンは，BDDP S の構造を利用すると簡単にターンベースオー
トマトンに変換できる．元のオートマトンの状態はシ

図4

変換後

ステム側の状態として扱う．システム側の各状態の遷移先BDDP S を以下のように計算する．元のオートマ変換により追加された環境側の状態を表す．

トンの状態からの遷移先BDDP S の根ノードから終端

4. 2. 2 BDDP S を用いた決定化

ノードへのパスをたどる．初めて入力変数がラベル

BDDP S の決定化には和集合演算を用いる．２つの付けされたノード n にたどり着いたとき，ノード n

BDDP S の和集合とは，各論理式集合で到達できる終に対応する終端ノード tn を作り，n の直前のノード

端ノードが，元の２つのBDDP S において同じ論理式

npre の指す先を tn に変える．このノード tn に対応

集合で到達できる終端ノードの和集合になっている

する状態 sn を新たに作り，これを環境側の状態とす

BDDP S のことである [12]．

る．このとき，sn の遷移先BDDP S はノード n であセーフティゲームの状態の遷移先を表す succ もる．また，終端ノード tn のラベルは要素が sn のみ

BDDP S で表現する．ただし，終端ノードは集合での状態集合である．

ある必要があるため，カウント関数 f を組の集合

ただし，この手順でたどっているパスが入力変数を{(q, f (q)) | q ∈ Q} で表す．succ の定義上カウント

介せずに終端ノード t へ直接達したときは，終端ノー値の最大値をとる必要があるため，BDDP S の決定化

ド t に対応する終端ノード tt を作り，同様の手順を手続きと同様に和集合演算をそのまま適用すること行う．

はできない．

また，ノード n に複数回到達した場合，２つ目以カウント関数の遷移先の決定化は，カウント関数を降の終端ノード tn は作らずに共有する．これらの状表す集合 f ，通常のBDDP S の決定化と同じように和態のノードは遷移先が等しく，等価と見なすことがで集合をとり，その集合 P ⊆ Q × N の極大な要素 ⌈P ⌉きるからである．この手続きにより，同じオートマト

を使う．極大な要素の集合は次のように定義されるンから変換されるターンベースオートマトンは複数[7]．

存在するが，その中でも小さいものができる．
例として，図 2 を変換すると，図 4 のようになる．

⌈P ⌉ = {p ∈ P |̸ ∃p′ ∈ P, p′ ̸= p ∧ p ⪯ p′ }
′

(5)

′

ただし，p ⪯ p ⇐⇒ ∀q, p(q) ≤ p (q) である．

ただし，a1 と a2 は出力信号，b は入力信号，P0 P1 P2

セーフティゲーム G(Aϕ , k) 中のカウント関数 f のは元のオートマトンの状態を表しており，P3 P4 P5 は遷移先を次のように計算し，BDDP S で表す．ただし，

図5

オートマトンの状態 (1,0) と状態 (3,1) の遷移先

| {q ∈ Q | f (q) ≥ 0} |= 1 かつ f (q) = i となるような f を fq,i と表す．

1. fq,i のとき：もとのオートマトンの状態 q の遷移先BDDP S をコピーし，たどった各終端ノードの状態集合 Q′ ⊆ Q を次の規則に従ってカウント

図6

状態 (1,0) と (4,1) のBDDP S

図7

状態 {(1, 0)(4, 1)} のBDDP S

関数 f ′ に変換する．


i + 1 (q ′ ∈ Q′ ∧ q ′ ∈ F )
f ′ (q ′ ) = i(q ′ ∈ Q′ ∧ q ′ ̸∈ F )




−1
(otherwise)
2. ∀q ∈ Q, f (q) = −1 のとき：遷移先は f 自身でラベル付けされている終端ノードである．この状
態は Saf e に含まれているものとして扱う．

3. | {q ∈ Q | f (q) ≥ 0} |≥ 2 の と き：集 合
F ′ = {fq,f (q) | q ∈ Q, f (q) ≥ 0} とおいて，
F ′ の全ての要素についてBDDP S の和集合演算をとり，たどり着く全ての終端ノード P ⊆ Q × N
について ⌈P ⌉ をとったものを新たな終端ノードとする．
以上の手順で，初期状態から到達可能であり，かつ

Saf e に含まれる状態の全ての遷移先を計算する．

が組 (q, f (q)) であるリスト構造で収納した．ただし，

例えば，(図 5) のようなオートマトンの状態 (1, 0)

リストの長さを抑えるために，リストの要素に入れと (4, 1) からの遷移先は，BDDP S では (図 6) のようるのは f (q) ≥ 0 であるような (q, f (q)) だけとする．

に表現される．これから {(1, 0)(4, 1)} の遷移先を計

この構造の利点は，２つのリストの要素がソート済み

算するとは (図 7) のようなBDDP S を得る．これは，であれば，リストの和集合から極大の要素だけを残しセーフティゲーム中の (図 8) のような遷移を表してたソート済みリストを生成する手続きが簡単に実装いる．

できることであり，L1 と L2 をそれぞれ元のリスト

4. 2. 3 決定化手続きの実装の長さとしたとき，その計算量が O(L1 + L2 ) で済む

決定化で極大の要素を調べる際に，集合の要素をことである．

全て調べる必要があること，また，要素の挿入が頻

また，上記の決定化手続きの３番目の手順は，複数繁に起こることから，カウント関数のデータは要素のノードの和集合をとるが，その途中式を記録しておくことで最適化できる．

U ∩ post(f ) の数を記憶する couter(f ) を用意する．初期値は counter(f ) := 0 である．

2. 関数 f ∈ S を取り出す．新たに S := S\{f } とする．また，U := U ∪ {f } とする．

3. 全ての prereach (f )\{U } の要素 fpre について
次の手続きをする．

4. fpre ∈ FI のとき，新たに S = S ∪ fpre とする．
図8

5. fpre ∈ FO のとき，新たに counter(fpre ) :=決定化後の状態 {(1,0),(4,1)} の遷移先

counter(fpre ) + 1 と す る ．counter(fpre ) =例えば，{(1, 0)(2, 0)(3, 0)} の計算は，上記通りに行うと，{(1, 0)} と {(2, 0)} の遷移先の和集合を計算し，{(1, 0)(2, 0)} と {(3.0)} の遷移先の和集合を計算するという手順を踏む．この後，{(1, 0)(2, 0)(4, 0)} の計算

postnum (fpre ) ならば，新たに S := S ∪ fpreとする．

6. 2 からここまでの手順を S = ∅ となるまで繰り返す．

をする場合，{(1, 0)} と {(2, 0)} の遷移先の和集合を

7. M := R\U として，f0 ∈ M ならば，勝利戦略

もう一度計算することになる．そこで，{(1, 0)(2, 0)}が存在し，M 以外のカウント関数と遷移を取りを記憶し，{(1, 0)(2, 0)(4, 0)} の計算時には，まず除いたものがその勝利戦略になる．

{(1, 0)(2, 0)} が計算済みかどうかを調べるように

これはシステムがどのようにプレイしても，

f (q) = k + 1 を含むカウント関数にたどり着いてする．

しまうような環境側のプレイが存在するカウント関

4. 3 セーフティゲームの勝利判定

数を，エッジごと除外していくアルゴリズムである．

f ∈ F の前の状態を表す pre(f ) : F 7→ 2 と次のF状態を表す post(s) 7→ 2 を次のように定義する．
F

エッジの除外判定は各エッジにつき全体で 1 回しか行
われないため，計算量は到達可能なカウント関数から出るエッジの数を E とすると，O(E) である．

post(f ) = {fpost ∈ F | ∃a ∈ Σ, δ(f, a) = fpost }(6)

また，post(f ) と pre(f ) のマッピングと集合 S の作成も O(E) であり，特に，G(Aϕ , k1 ) で作成したpost(f ) と pre(f ) は G(Aϕ , k2 )(k2 ≥ k1 ) の post(f )pre(f ) = {fpre ∈ F | ∃a ∈ Σ, δ(fpre , a) = f } (7)と pre(f ) の一部として再利用できる．

また，到達可能かつ前の状態を prereach (f ) : F 7→

2F で表す．

4. 4 合成
prereach (f ) = pre(f ) ∩ R(8)

探索された勝利戦略 λ から実現となるリアクティ

ただし，R は初期状態から到達可能なカウント関数

ブシステムを Moore マシンで表現する．一般には，の集合であり，次を満たす最小の集合で定義される．

ある仕様に対してその実現は複数存在し，その中でR = R ∪ post(R), f0 ∈ R(9)も小さく簡単な実現を作ることがよいとされている．

また，次の状態の数を表す post num(f ) ∈ N を次

ところが，最小の Moore マシンを求める問題は NPのように定義する．

post num(f ) =| post(s) |困難であることが分かっている [5]．本実装では，小さ(10)

な Moore マシンを求めようとはせずに，λ(f ) ∈ 2Σo

勝利戦略は次のアルゴリズムで求められる．

の要素の中から無作為に一つ選んで Moore マシンと1. f (q) = k + 1 となる q が存在し，かつ到達可

して出力した．

能であるカウント関数 f からなる集合を S と
おき，U := ∅ とおく．全ての f ∈ R について，

は 17 勝 48 敗であった．

5 実験
前節の手法を適用し，実現可能性判定器を実装した．

5. 3 考察

言語は C++を用い，LTL 式から universal coBüchi

仕様 5 は LTL3BA が出力する universal coBüchi

オートマトンへの変換は LTL3BA [2] を使用した．

オートマトンの状態数が比較的多くなる傾向がある．
例として，n=6 のときは 22230 個であった．Unbeast

5. 1 実験環境と目的

はオートマトンの状態を命題と対応させる形で BDD

本実験では，MacOS 上の Ubuntu の仮想マシン上を使っているため，このように状態数の大きすぎるで実験を行う．主なスペックは以下の通りである．

オートマトンを表現することが苦手である．その結

1. Intel Core i7 2GHz

果，Unbeast は n の値が比較的小さい段階でタイム

2. MacOSX 10.8.4

アウトしてしまう．一方，本実装では状態の表現に

3. VirtualBox 4.2.12

BDD を使わず，状態を明示的に構築するため，この

4. ubuntu 12.04 LTS (32bit)

ように universal coBüchi の状態数が大きい場合でも5. 2.0GB（仮想マシンに対する割り当て）

オートマトンを構築することができる．

入力として使用するリアクティブシステム仕様は，n

また，表の全体をみると，Acacia+は n の増加に対台負荷分散装置 (Load Balancer) 仕様 [6] とする．こする判定時間の増加率が他の判定器よりも極端に大の仕様は Unbeast ベンチマークに使われている．

きいことが多い．Acacia+は命題変数の処理をシンボ

本実験では高速な実現可能判定器として有名な

リックに行うため，命題数の多い仕様を苦手としていAcacia+ [1] と Unbeast [4] と比較実験を行い，本実装

る [8]．そのため，Acacia+は一般的に実現可能性判がどれだけ速いのかを調べる．

定が簡単な仕様に対しても，命題数が多くなるだけで判定に時間がかかることがある．一方，本実装のよう

5. 2 評価に命題変数を BDD のノードで表現すると，命題の増本実験では，各仕様について n を 2 から 9 まで増加数に対して比較的強くなる．

やして実現可能性判定にかかる時間とシステムの合以上より，本実装は universal coBüchi オートマト

成までにかかる時間を調べた．結果は表 1，2 のようンの状態数が非常に大きく，命題変数の数が多い場合になった．ただし，判定に 3 分以上かかるものは計に他の判定器よりも高速に判定できることがわかる．

算を打ち切り，TO と表記している．また，メモリ不足で実行が中断されたものは，MO と表記してい6 まとめと今後の課題

る．S は合成を含めた時間，N は含めない時間であ

本稿では，高速な実現可能性判定器の実装方法を提る．Unbeast は仕様が実現不可のときは環境側の実案した．オートマトンの遷移先をBDDP S で表現し，現となる反例を合成しない．そのため，実現不可な仕実装上の工夫として，ノードの共有化，計算結果の様については Unbeast の計測時間は合成を行わない

キャッシュ化などをすることで決定化にかかるコスト

場合のみとなる．

を削減した．実験から，他の高速な判定器よりも速い

また，他の判定器は合成するシステムの大きさを小例があり，BDDP S を使って明示的にセーフティゲー

さくする処理を含むため，合成を含んだ時間を比較す

ムを構築するという本手法のアプローチが有効な例

るのは公平ではない．そのため本章では合成をしないがあることが確認できた，

場合の処理速度を比較する．

今回の実装では，実現となるリアクティブシステ

仕様 10 個と n の値 8 種類の仕様について，双方ムの状態数の削減を行わなかった．一般に，合成するがタイムアウトした場合をのぞいた速度比較結果は，システムの状態数が小さい方が良いとされており，まAcacia+に対しては 13 勝 44 敗，Unbeast に対して

た，現状では比較実験の公平性を保つことが難しいた

表1

仕様

1

本実装

UnbeastAcacia+2

本実装

UnbeastAcacia+

3

4

本実装

n=2

3

4

5

6

7

8

9

S

0.39

0.20

0.17

0.19

0.19

0.21

0.21

0.22

N

0.09

0.08

0.08

0.08

0.08

0.11

0.09

0.12

S

0.07

0.05

0.05

0.06

0.06

0.07

0.08

0.09

N

0.06

0.05

0.05

0.06

0.06

0.07

0.07

0.10

S

0.01

0.02

0.03

0.16

0.16

0.65

3.33

26.54

N

0.01

0.02

0.00

0.02

0.04

0.10

0.24

1.10

S

0.21

0.17

0.19

0.20

0.21

0.23

0.30

0.49

N

0.09

0.08

0.08

0.08

0.02

0.11

0.16

0.35

S

0.06

0.06

0.06

0.07

0.08

0.12

0.26

1.06

N

0.06

0.06

0.06

0.07

0.09

0.12

0.25

1.02

S

0.02

0.13

10.20

TO

TO

TO

TO

TO

N

0.02

0.08

7.51

TO

TO

TO

TO

TO

S

0.63

0.11

0.17

0.14

0.17

0.31

0.70

2.27

N

0.12

0.10

0.10

0.12

0.12

0.29

0.69

2.12

Unbeast

N

0.07

0.07

0.08

0.09

0.11

0.15

0.29

1.04

Acacia+

S

0.01

0.00

0.02

0.03

0.10

0.48

3.04

21.70

N

0.01

0.00

0.02

0.03

0.07

0.19

0.62

2.04

S

0.21

0.25

2.19

TO

TO

TO

TO

TO

N

0.10

0.20

2.50

TO

TO

TO

TO

TO

S

0.08

0.22

0.66

7.82

109.84

TO

TO

TO

N

0.07

0.14

0.25

1.04

1.74

3.76

14.54

127.18

S

0.02

0.14

9.93

TO

TO

TO

TO

TO

N

0.01

0.08

7.22

TO

TO

TO

TO

TO

S

0.12

0.12

0.19

0.62

3.81

MO

MO

MO

本実装

UnbeastAcacia+5

Load Balancing 仕様の実験結果その 1

本実装

N

0.18

0.14

0.34

0.62

3.87

MO

MO

MO

Unbeast

N

0.10

0.91

TO

TO

TO

TO

TO

TO

Acacia+

S

0.02

0.05

0.26

2.01

35.88

TO

TO

TO

N

0.02

0.05

0.25

1.98

35.72

TO

TO

TO

め，合成するリアクティブシステムの状態数を既存の参 考 文 献判定器の出力するものと同程度もしくはそれ以下に[ 1 ] : http://lit2.ulb.ac.be/acaciaplus/.
[ 2 ] : http://sourceforge.net/projects/ltl3ba/.
[ 3 ] : http://www.iaik.tugraz.at/content/research/design verification/lily/.
[ 4 ] : http://www.react.uni-saarland.de/tools/unbeast/.
[ 5 ] Ehlers, R.: Short Witnesses and Accepting Lassos in ω-Automata, Language and Automata Theory
and Applications, Vol. 6031(2010), pp. 261–272.
[ 6 ] Ehlers, R.: Symbolic Bounded Synthesis, 22ndInternational Conference on Computer Aided Verification, Touili, T., Cook, B., and Jackson, P.(eds.),

する実装を行うことが今後の課題である．本実装の方針に従えば，状態数の少ない実現を探索する際に明示的に作ったセーフティゲームを再利用できるため，他の判定器よりも高速に探索できることが期待できる．

表2

仕様

6

7

8

本実装

3

4

5

6

7

8

9

S

0.19

0.28

8.87

MO

MO

MO

MO

MO

N

0.13

0.27

9.07

MO

MO

MO

MO

MO

N

0.12

1.75

TO

TO

TO

TO

TO

TO

Acacia+

S

0.02

0.05

0.27

2.45

39.76

TO

TO

TO

N

0.02

0.05

0.27

2.41

39.52

TO

TO

TO

S

0.21

0.29

9.17

MO

MO

MO

MO

MO

N

0.19

0.30

9.26

MO

MO

MO

MO

MO

Unbeast

N

0.25

2.82

TO

TO

TO

TO

TO

TO

Acacia+

S

0.03

0.09

0.55

4.14

65.28

TO

TO

TO

N

0.03

0.08

0.54

4.05

62.07

TO

TO

TO

S

0.32

0.29

1.58

TO

TO

TO

TO

TO

N

0.14

0.18

1.72

TO

TO

TO

TO

TO

本実装

本実装

S

0.10

0.31

1.41

23.98

TO

TO

TO

TO

N

0.10

0.23

0.62

3.31

4.95

11.78

27.15

TO

S

0.03

0.15

7.89

TO

TO

TO

TO

TO

N

0.02

0.12

7.61

TO

TO

TO

TO

TO

S

0.21

0.16

0.16

0.26

0.56

1.62

5.14

16.82

N

0.17

0.11

0.16

0.23

0.51

1.51

5.15

16.76

Unbeast

N

0.09

0.09

0.13

0.18

0.24

0.56

1.32

1.62

Acacia+

S

0.02

0.02

0.05

0.15

0.53

2.29

12.28

77.30

N

0.02

0.02

0.04

0.13

0.41

1.35

4.87

16.38

S

0.09

0.13

0.64

16.36

TO

TO

TO

TO

N

0.11

0.13

0.66

16.58

TO

TO

TO

TO

S

0.15

0.31

2.99

23.72

TO

TO

TO

TO

N

0.12

0.17

1.19

1.69

35.99

121.50212.54

TO

S

0.03

0.06

0.48

20.97

TO

TO

TO

TO

N

0.02

0.05

0.40

20.17

TO

TO

TO

TO

Acacia+10n=2

UnbeastUnbeast9

Load Balancing 仕様の実験結果その 2

本実装

本実装

UnbeastAcacia+

LNCS, Vol. 6174, Springer Verlag, 2010, pp. 365–379.
[ 7 ] Emmanuel Filiot, Naiyong Jin, J.-F. R.: An
Antichain Algorithm for LTL Realizability, CAV,
Vol. 5643(2009), pp. 263–277.
[ 8 ] Emmanuel Filiot, Naiyong Jin, J.-F. R.: Exploiting Structure in LTL Synthesis, International
Journal on Software Tools for Technology Transfer,(2012).
[ 9 ] Orna Kupferman, M. Y. V.: Safraless Decision
Procedures, (2005).
[10] S. Schewe, B. F.: Bounded Synthesis, ATVA,(2007), pp. 474–488.
[11] Safra, S.: On the complexity of ω automata,Foundations of Computer Science, (1989), pp. 319–
327.
[12] 安藤崇央 宮本佑樹 萩原茂樹米崎直樹: リアクティ
ブシステム仕様に対する段階的充足可能性判定器の分散オブジェクト技術を利用した実装, コンピュータソフト
ウェア, Vol. 28, No. 4(2011), pp. 262–281.
[13] 森亮靖 友石正彦米崎直樹: 時相論理によるリアクティ
ブシステム仕様の実現可能星に関する分類, コンピュー
タソフトウェア, Vol. 15, No. 3(1992), pp. 25–37.