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

実現可能性の必要条件に基づいた
不完全リアクティブシステム合成
冨田 尭

萩原 茂樹

島川 昌也

米崎 直樹

外部環境と継続的に相互作用する高信頼リアクティブシステムを得るために，線形時相論理 LTL で記述された動作仕様の実現可能性を判定し，実現可能な場合にシステムを合成する手法がこれまでに研究されてきた．また，仕様が実現不能であった場合にその欠陥を検出・分類するために，実現可能性の幾つかの必要条件及びその判定手法も導入されている．しかし，LTL の表現力では，実現可能性と仕様記述者の意図を両立する適切な仕様を表現できない場
合がある．また，現実的には，仕様を厳密には満たしていないシステムでもしばしば運用されている．そのため，不完全であっても一定の水準を満たすシステムが合成できれば有用である．
本研究では，より詳細な仕様欠陥分析を可能とするために，真段階的充足可能性，半強充足可能性，段階的許容可能性という 3 つの実現可能性必要条件を新たに導入する．そして，仕様がそれらの必要条件を満たすかを判定し，満たす場合に不完全なリアクティブシステムを合成する手続きを与える．

にシステムを得ることができる．その際，仕様記述以

1 はじめに外の工程では，人手を介さないため，不具合が混入す

リアクティブシステム合成（reactive system syn-る恐れがない．そのため，妥当な仕様さえ与えること

thesis）とは，外部環境と継続的に相互作用するリアができれば，仕様を実現するリアクティブシステムをクティブシステムを仕様から自動的に合成する手法で確実に得ることができる．

ある．リアクティブシステムは外部環境からの入力をしかしながら，実現可能性判定及び自動合成は一般制御できないため，与えられた仕様を満たすリアクに計算コストが非常に大きく，欠陥のある仕様を試行

ティブシステムが存在するためには，その仕様は無矛

錯誤を通して実現可能かつ合理的になるよう修正・洗盾，即ち，充足可能（satisfiable）なだけでは不十分

練することは容易ではない．そのため，森ら [15] は，であり，実現可能 [16] [1] [18]（realizable）でなければ充足可能性よりも強いいくつかの実現可能性必要条件

ならない．リアクティブシステム合成は，仕様の実現

及びそれらの充足判定手続きを提案している [15] [23]．

可能性判定も兼ねており，仕様が実現可能であるとき• 強充足可能性 [15]（strong satisfiability）• 段階的充足可能性 [15]（stepwise satisfiability）

Imperfect Reactive System Synthesis Based on Necessary Conditions of Realizability
Takashi Tomita, 北陸先端科学技術大学院大学 情報社会基盤研究センター, Research Center for Advanced Computing Infrastructure, Japan Advanced Institute of
Science and Technology.
Shigeki Hagihara, Masaya Shimakawa, 東京工業大学
大学院情報理工学研究科 計算工学専攻, Departmentof Computer Science, Graduate School of Information Science and Engineering, Tokyo Institute ofTechnology.
Naoki Yonezaki, 放送大学, Open University of Japan.

• 段階的強充足可能性 [15]（stepwise-strong satisfiability）
これらの必要条件充足判定は実現可能性判定よりも計算量が小さく，仕様に欠陥がある，即ち，仕様が実現不能である際に，その必要条件充足判定手続きの結果に基いた欠陥分析や欠陥箇所抽出 [10] により，効率的な仕様修正が可能となる．また，Damm らも森らとは独立に別の必要条件を提案している [5]．

• 許容可能性 [5]（admissibility）

以上のような仕様の欠陥分析・検出やリアクティブシステム合成の研究は盛んに行われてきたが，既存• 段階的許容可能性（stepwise admissibility）– 許容可能性よりも強い性質．

の形式言語の表現力では現実的なシステム要求を正真段階的充足可能性（resp. 半強充足可能性）は，段確に反映した仕様を記述できないことも多い．その階的強充足可能性と実現可能性（resp. 強充足可能性）

ような場合，厳密に安全なシステムを得るためには，の差と同様の差を段階的充足可能性との間にもち，ま要求よりも強い性質を仕様として与えることが妥当

た，段階的強充足可能性と段階的充足可能性の差と同である．しかし，合理的な強化によって仕様が実現不様の差を実現可能性（resp. 強充足可能性）との間に能となってしまうこともあり得る．また，現実には，もつ性質である．また，本研究では，許容可能性と強不具合をもつシステムでもしばしば運用されている．

充足可能性の間には，それらを満たす仕様の集合の共そのため，仕様が実現不能であったとしても，可能な通部分が実現可能な仕様の集合と一致するという関係

限り仕様を満たすようにふるまうシステムを合成するがあることを示す．段階的許容可能性は，それと同様

ことには大きな意義がある．ここで，既存の実現可能の関係を半強充足可能性との間にもつ性質である．そ性必要条件のうち，段階的充足可能性や段階的強充足

して，これらの必要条件の充足判定手続きとして，既可能性，許容可能性は，ある種のリアクティブシステ

存必要条件充足判定手続きと類似の手続きを与える．

ムの存在を示す性質である．そして，そのリアクティ

これにより，より詳細な仕様欠陥分析が可能となる．

ブシステムは，仕様を実現するとは限らないが，ある

さらに，これら 3 つの充足可能性必要条件に基づい一定の水準を満たすシステムである．吉浦らは段階的た不完全合成手続きとして，既存の（不完全）合成手

充足可能な仕様から，充足可能性を保持するシステ法と類似の手続きを与える．これにより，仕様が実現

ムを合成する手法を提案している [24]．また，Damm

不能であった場合でも，導入した実現可能性必要条件

らは許容可能性な仕様から支配的リアクティブシステ

を満たしていれば，既存の不完全合成手法よりもよりムを合成する手法を与えている [5]．これらは，与え望ましい水準を満たすシステムの合成が可能となる．

られた仕様から，実現可能性必要条件に基づいた一定

本稿の構成は以下の通りである．2 章では，準備の水準を満たすシステムを合成する手法，即ち，不完として，リアクティブシステムや線形時間論理 LTL，全合成（imperfect synthesis）手法の一種である．そオートマトンの定義を与え，また，仕様の実現可能性

して，不完全合成された各部分システムを不備が露呈の定義及び既存のその必要条件について紹介する．3

しないように組み合わせ，全体として安全な分散シス

章では，新たに 3 つの実現可能性必要条件を導入し，テムを構成する応用手法も研究されている [5]．

その充足判定手続きを与える．4 章では，新たに導入

本研究の目的は，より詳細な仕様欠陥分析を可能とした必要条件も含め，実現可能性必要条件の間の包し，また，それに基づいて不完全合成を行う手法を提含関係に関する階層定理を示す．5 章では，新たに導案することである．

入した必要条件に基づいた不完全合成手法を与える．

本研究では，既存必要条件及び実現可能性の間の隔たりを埋める新たな必要条件として以下の 3 つの性

そして 6 章で関連研究について述べ，最後に 7 章でまとめる．

質を導入する．

• 真段階的充足可能性（properly-stepwise satisfiability）– 段階的充足可能性よりも強く，段階的強充足可能性とは比較不能な性質．

• 半強充足可能性（semi-strong satisfiability）– 充足可能性よりも強く，強充足可能性や段階的充足可能性よりも弱い性質．

2 準備
本章では，リアクティブシステム，その仕様記述言語としてしばしば用いられる線形時間論理 LTL，そして，オートマトンの定義を与える．
また，仕様の実現可能性の定義及びその必要条件を紹介する．

2. 1 リアクティブシステム（model checking）でも広く用いられている．LTL 式

制御システムなどの環境（ユーザや外部モジューは，命題論理の論理結合子 ¬，∨，∧，→，↔ と時間ル）と継続的に相互作用するオープンシステムは，リ

演算子 ⃝，3，2，U を用いて記述される．

アクティブシステムとしてしばしばモデル化される．

定義 3 (LTL の構文). 原子命題集合 P 上の LTL 式

この種のシステムの特性として，以下の二点が挙げら

φ の構文は以下の通りである．
φ ::= a | ¬φ | φ ∨ φ | φ ∧ φ | φ → φ | φ ↔ φ |れる．

⃝ φ | 3φ | 2φ | φ U φ.

特性 1: リアクティブシステムは出力を制御できる

ただし，a ∈ P は原子命題である．

が，外部環境からの入力は制御できない．
特性 2: リアクティブシステムは過去の相互作用履
歴のみを用いて現在の出力を決定しなければな(1)■

なお，リアクティブシステムの仕様記述に用いる際には P = I ∪ O である．
直感的には，⃝φ は「次のステップで φ を満たす」，

らない．
形式的には，リアクティブシステムは以下のように

3φ は「いつか φ を満たす」，2φ は「常に φ を満た定義される．

す」，φ1 U φ2 は「いつか φ2 を満たし，それまでの間

定義 1 (リアクティブシステム). リアクティブシス

は φ1 を満たす（強い until）」ことをそれぞれ表す．

テムは応答関数 r : (2I )+ → 2O である．

LTL では，これらの演算子を組み合わせて，例え

ただし，I/O は外部環境/システムが制御する入力/

ば，以下のような性質を記述できる．

出力イベントの生起を表す互いに素，即ち，I ∩ O = ∅

23φ,

■

32φ,

(3)

2(φ1 → 3φ2 ).

(4)である入力/出力原子命題集合である．

以下では，すべてのリアクティブシステムの集合をR で表す．

(2)

式 (2) は「無限にしばしば φ が成り立つ」，式 (3) は定義 2 (ふるまい). 外部環境からの無限長入力列 α =I ωa0 a1 a2 · · · ∈ (2 ) に対するリアクティブシステム r
O ωの無限長出力列 r(a0 )r(a0 a1 )r(a0 a1 a2 ) · · · ∈ (2 )に，φ1 が成り立った後には必ず φ2 が成り立つ」という性質をそれぞれ表す．

LTL の意味論，即ち，無限長語 σ ∈ (2P )ω と LTL

を r ω (α) とする．
このとき，α に対する r のふるまいは，各点和集I∪O ω合 α ⊔ r (α) ∈ (2ω

「ある時刻以後，常に φ が成り立つ」，式 (4) は「常) ，即ち，(a0 ∪ r(a0 ))(a1 ∪r(a0 a1 ))(a2 ∪ r(a0 a1 a2 )) · · · である．

式 φ の間の充足関係 |= は通常通りの定義に従うものとし，本稿では省略する．

■

LTL 式 φ で与えられた仕様を満たすふるまいが存

入力/出力列を有限長前半部分列と無限長後半部在するとき，φ は充足可能（あるいは無矛盾）である

分 に 分 割 し た と き ，そ れ ら を そ れ ぞ れ 入 力/出 力という．

接頭辞（input/output prefix）と入力/出力接尾辞

定義 4 (充足可能性). LTL 式 φ について，以下を満（input/output suﬃx）と 呼 ぶ ．ま た ，入 力 接 頭 辞

たすとき，φ は充足可能であるという．

∃σ ∈ (2P )ω : σ |= φ.

I +x̃ = a0 a1 · · · an ∈ (2 ) に対するリアクティブシス■

テム r の出力接頭辞 r(a0 )r(a0 a1 ) · · · r(a0 a1 · · · an )を r ∗ (x̃) で表す．

(5)

LTL 式 φ は，それを満たす語の集合（即ち，言語）{σ ∈ (2P )ω | σ |= φ} を規定する．これを L(φ) で

2. 2 線形時相論理 LTL表す．

線形時相論理 [17]（Linear Temporal Logic，LTL）

また，LTL 式 φ に対して，任意の接尾辞と連結しは，一つの時間系列上の性質を記述することができても φ を満たすことがない，即ち，以下を満たす接る時間論理である．動的システムのふるまいの性質

頭辞 s0 · · · sn ∈ (2P )∗ を悪性接頭辞（bad prefix）と（動作仕様）の記述にしばしば用いられ，モデル検査

呼ぶ．

る状態の集合を Inf (ρ) とする．
P ω∀σ ∈ (2 ) : s0 · · · sn σ ̸|= φ.

(6)

φ が悪性接頭辞をもたないとき，φ は safety prop-

Inf (ρ) = {q ∈ Q | ∀i ∈ N : ∃j ∈ N>i : q = qj }.

erty であるという．そして，φ の非悪性接頭辞のみ(8)ω-オートマトン A は，実行の特徴と Acc 及びオーを接頭辞としてもつ語からなる言語，即ち，以下のよ

トマトンの種類に応じて受理/不受理を判定する．そうに定義される言語 Safe(φ) を φ の safety 成分とのような受理語の集合を A の受理言語という，LTLいう．

式 φ に関するモデル検査等の形式的検証は，L(φ) をP

Safe(φ) = {s0 s1 · · · ∈ 2 | 任意の i ∈ N に関して

受理言語とするオートマトンに対するグラフ解析によ

s0 · · · si は φ の悪性接頭辞でない }.

り行うことができる．LTL により規定できる言語の(7)

クラスは，ω-正規言語（ω-regular language）のクラスの部分集合であり，Büchi オートマトン（BA）や

2. 3 オートマトン

Rabin オートマトン（RA）などの ω-正規オートマ

与えられた無限長語に対して，受理/不受理を判定

トンによって認識できる．この ω-正規言語オートマト

する有限状態機械を ω-オートマトン（ω-automaton）

ン A は，無限にしばしば出現する状態の集合 Inf (ρ)という．

に基づいて実行 ρ の特徴を捉え，受理/不受理を判定

2. 3. 1 定義

する．

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

定義 6 (Büchi オートマトン). BA は，ω-オートマト

定義 5 (ω-オートマトン). ω-オートマトン A は，5
つ組 ⟨Q, Σ, ∆, qinit , Acc⟩ である．ただし，• Q は有限の状態集合，• Σ は有限のアルファベット，ン ⟨Q, Σ, ∆, qinit , F ⟩ である．ただし，• F ⊆ Q は受理状態集合であり，• 以 下 の Büchi 受 理 条 件 を 満 た す 受 理 実 行
ρ ∈ Run A (σ) が存在する語 σ を受理する．

• ∆ : Q × Σ → 2Q は，各状態 qi ∈ Q において文Inf (ρ) ∩ F ̸= ∅.

(9)

字 si ∈ Σ を読んだ際に遷移可能な状態の集合を返す遷移関数，• qinit ∈ Q は初期状態，■
定義 7 (Rabin オートマトン). RA は，ω-オートマ
トン ⟨Q, Σ, ∆, qinit , F⟩ である．ただし，• Acc は受理条件を規定するための要素である．■• F ⊆ 2Q×Q は，無限にしばしば訪れるべき集合

オ ー ト マ ト ン A の 実 行 は ，与 え ら れ た 語 σ =Ui ⊆ Q と高々有限回しか訪れるべきでない集合

s0 s1 s2 · · · ∈ Σ の文字 si を先頭から順に読み，現ωVi ⊆ Q の対の集合であり，在の状態 qi （ただし q0 = qinit ）とその文字 si から• 以 下 の Rabin 受 理 条 件 を 満 た す 受 理 実 行

遷移関数 ∆ が与える遷移可能な状態 qi+1 に遷移し

ρ ∈ Run A (σ) が存在する語 σ を受理する．
∨(Inf (ρ) ∩ Ui ̸= ∅ ∧ Inf (ρ) ∩ Vi = ∅).

ていくことで進行する．形式的には，σ に対する実行 ρ は，無限長状態列 q0 q1 q2 · · · ∈ Qω で与えられる．ただし，q0 = qinit かつすべての i ∈ N に関して⟨Ui ,Vi ⟩∈F(10)■

qi+1 ∈ ∆(qi , si ) である．ここで，任意の状態 q ∈ Q

決定性 RA の受理言語のクラスは ω-正規言語のクと文字 s ∈ Σ について |∆(q, s)| ≤ 1 であるとき，そラスと一致している．一方で，決定性 BA の受理言のオートマトンは決定的（deterministic）であるという．また，σ に対する実行の集合を Run A (σ) で表す．

Run A (σ) は複数の要素をもち得るが，A が決定的な
らば 1 つ以下の要素しかもたない．そして，無限状
態列 ρ = q0 q1 q2 · · · ∈ Qω 上に無限にしばしば出現す

語のクラスは，それよりも真に小さく，また，LTLにより規定できる言語のクラスとは比較不能である．
本稿では，決定性と明示されたオートマトンは決定性 RA を指し，そうでないオートマトンは BA を指すこととする．以降では，この 2 種のオートマトン

を利用する手続きを扱うが，これらと同等な表現能力をもつオートマトンを利用することも可能である．

2. 4 実現可能性
リアクティブシステムの仕様 φ は充足可能（無矛2. 3. 2 強連結成分盾）なだけでは不十分である．なぜならば，リアク

オートマトン A = ⟨Q, Σ, ∆, qinit , Acc⟩ 上で，状態

ティブシステムは，2. 1 節で述べた特性 1 と特性 2 を

q0 から状態 qn へ遷移可能であるとは，ある有限長状

満たしながら，任意の入力列に対して仕様を満たすよ

態列 p = q0 . . . qn ∈ Q が存在し，すべての i ∈ N<n

うにふるまえなければならないためである．与えられに関して，ある文字 si が存在し qi+1 ∈ ∆(qi , si ) でた仕様に対して，そのようなリアクティブシステムがあることである．そのような p を（q0 を始点とする）

存在するとき，その仕様は実現可能である．

パスといい，状態 q を始点とするすべてのパスの集

定義 8 (実現可能性). 言語 L ⊆ (2P )ω について，以合を Path A (q) で表す．そして，互いに到達可能であ

下を満たすリアクティブシステム r ∈ R が存在する

る極大な状態集合を強連結成分（strongly-connected

とき，L は実現可能であるという．

+

component，SCC）という．オートマトン（有向グ∀α ∈ (2I )ω : α ⊔ rω (α) ∈ L.

ラフ）上のすべての SCC を列挙することを SCC 分

また，LTL 式 φ について，L(φ) が実現可能である

解（SCC decomposition）といい，Tarjan のアルゴ

とき，即ち，以下を満たす r ∈ R が存在するとき，φリズム等により効率的に計算できる．

は実現可能 [16] [1] であるという．

また，初期状態 qinit を始点とするあるパス p1 ∈

Path

A

∀α ∈ (2I )ω : α ⊔ rω (α) |= φ.

(11)

(12)

(qinit ) が存在し，p1 pω
2 が受理実行（例えば，Aが BA であるときには Inf (pω
2 ) ∩ F ̸= ∅）となるよう■
本稿ではその詳細については省略するが，素朴な実な巡回パス p2 を受理閉路と呼ぶ．そして，受理閉路現可能性判定手続きの概略は以下の通りである．

を含む SCC を受理 SCC と呼ぶ．

手続き 9 (実現可能性判定手続き).

2. 3. 3 LTL 式からオートマトンへの変換

入力：LTL 式 φ

LTL 式 φ から L(φ) を受理言語とする，即ち，等価出力：φ が実現可能か否かな BA への効率的に変換する手法 [6] [2] [14] は盛んに研究されており，変換器として SPOT†1 [6]，LTL3BA†2

1. L(φ) を受理する決定性オートマトン Aφ を構[2]，Trans†3 [14] などが開発されている．

2. Aφ の状態及び遷移を入力/出力のターンに分割

また，LTL 式から等価な決定性 RA への変換器としては，Safra の構成法 [19] を実装した LTL2dstar†4[12] や，Safraless†5 な変換手法 [8] を実装した Ra-

binizer3†6 が開発されている．
†1 https://spot.lrde.epita.fr/†2 http://sourceforge.net/projects/ltl3ba/†3 https://sites.google.com/site/yonezakilab/
tools†4 http://www.ltl2dstar.de/†5 Esparza-Křetı́nský 法 [8] は，Safra の構成法を用いずに LTL 式から等価な決定性 ω-正規オートマトンを構成する手法であるため，Safraless と形容される．
しかし，実現可能性判定/自動合成においては，決定性 ω-正規オートマトンではなく，決定性 safety オー
トマトン等のより表現力の弱いオートマトンを利用した手法/アプローチを Safraless と形容する．
†6 https://www7.in.tum.de/~kretinsk/
rabinizer3.html

成する．
し，二人ゲーム Gφ に変換する．

• Gφ 上では，φ を満たす振る舞いに対応する
プレイでは出力側（即ち，リアクティブシステム側）プレイヤが勝利する．

3. Gφ 上の出力側プレイヤの勝利戦略が存在するならば「実現可能」と判定し，そうでないならば「実現不能」と判定する．

■

ゲーム上の戦略はリアクティブシステムと見なせる
ため，この勝利戦略は仕様を実現するリアクティブシ
ステムである．よって，自動合成では，この勝利戦略を出力する．

LTL 式の実現可能性判定及び自動合成は 2EXPTIME 完全 [16] [18] であり，計算コストは非常に大きい．さまざまな効率化手法 [13] [20] [9] 及びツール[11] [7] [4] [26] が提案されているが，(1) 仕様と等価な

決定性オートマトンを構成し，(2) それに対応する
ゲームに変換し，(3) そのゲームの勝利戦略を求める，という流れはどの手法/ツールも同じである †7 ．

2. 5. 3 段階的強充足可能性
段階的強充足可能性は，強充足可能性と段階的充足可能性を掛け合わせた，「各時刻において強充足可能性を保持するような出力を決定するリアクティブシス

2. 5 既存の実現可能性必要条件

テムが存在する」という実現可能性必要条件である．

本節では，森ら [15] 及び Damm ら [5] が提案した実

定義 12 (段階的強充足可能性 [15]). LTL 式 φ について，以下を満たすリアクティブシステム r ∈ R が存現可能性必要条件について紹介する．

2. 5. 1 強充足可能性

在するとき，φ は段階的強充足可能であるという．

強充足可能性は，2. 1 節で述べた特性 1 のみに注目∀x̃ ∈ (2I )∗ , ∀α ∈ (2I )ω : ∃β ∈ (2O )ω :(x̃ ⊔ r∗ (x̃))(α ⊔ β) |= φ.

した，「任意の入力列に対して仕様を満たす出力列が■存在する」という実現可能性必要条件である．
定義 10 (強充足可能性 [15]). LTL 式 φ について，以下を満たすとき，φ は強充足可能であるという．

∀α ∈ (2I )ω : ∃β ∈ (2O )ω : α ⊔ β |= φ.

(17)

なお，強充足可能かつ段階的充足可能であることと段階的強充足可能であることは一致しない [15]．

(13)

2. 5. 4 許容可能性■

許容可能性は，ゲーム理論の支配（dominance）のここで，φ の強充足可能性の反例となる入力列，即概念に基づいた，「仕様を満たすような出力列が存在I ω

ち，以下を満たす無限長入力列 α ∈ (2 ) を悪性入しない入力列を除くどのような入力列に対しても仕力列（bad input sequence）と呼ぶ．

様を満たすようにふるまうリアクティブシステムが存∀β ∈ (2O )ω : α ⊔ β ̸|= φ.

(14)

在する」という実現可能性必要条件である．

φ の強充足可能性の反例となる悪性入力列は φ が成り

定義 13 (許容可能性 [5]). LTL 式 φ について，以下

立たないように強制する無限長入力列である．そのよを満たすリアクティブシステム r ∈ R が存在するとうな入力列に対する任意の振る舞いの集合を CST (φ)

き，φ は許容可能であるという．

で表す．

∀α ∈ (2I )ω :P ω((∃β ∈ (2O )ω : α ⊔ β |= φ) ⇒ α ⊔ rω (α) |= φ).

O ω

CST (φ) = {α ⊔ β ∈ (2 ) | β ∈ (2 ) andα は φ の悪性入力列 }.
2. 5. 2 段階的充足可能性(18)
また，そのような r は φ に関して支配的であると段階的充足可能性は，「各時刻において充足可能性

いう．

(15)

■

を保持するような出力を決定できるリアクティブシス

即ち，支配的リアクティブシステムは，すべてのテムが存在する」という実現可能性必要条件である．

入力列に対して最適な出力列を応答するシステムで定義 11 (段階的充足可能性 [15]). LTL 式 φ についある．

て，以下を満たすリアクティブシステム r ∈ R が存在するとき，φ は段階的充足可能であるという．

∀x̃ ∈ (2I )∗ : ∃α ∈ (2I )ω : ∃β ∈ (2O )ω :∗3 新たな実現可能性必要条件
本章では，2. 5 節で紹介した既存実現可能性必要条(16)

件及び実現可能性の間の隔たりを埋める新たな必要■条件として，真段階的充足可能性と半強充足可能性，

即ち，φ が段階的充足可能ならば，かつそのときに段階的許容可能性の 3 つの必要条件を各節で導入し，(x̃ ⊔ r (x̃))(α ⊔ β) |= φ.

限り，φ の safety 成分 Safe(φ) は実現可能である．
†7 交代木オートマトン及びその全受理判定を利用するものもあるが，それらはゲームとその勝利戦略探索と対応しており本質的には同じである．

その判定手法を与える．

3. 1 真段階的充足可能性
本節では，新たな実現可能性必要条件として真段階

的充足可能性を導入し，その判定手続きを与える．

たならば「真段階的充足可能」と判定し，そうで段階的充足可能性の証拠となる，即ち，式 (16) をないならば「真段階的充足不能」と判定する．

満たすリアクティブシステム r は，任意の入力接頭辞(a) 初期状態から到達不能または受理閉路（のに対して充足可能性は保持している．しかしながら，上に現れる状態）へ到達不能な状態をすべて

段階的充足可能性はあくまで仕様の safety 成分を実取り除く．

現するシステムの存在を示すものであり，式 (16) 中(b) 行き止まり状態をすべて取り除く．
（行きの出力接尾辞 β は r に束縛されていないため，r はど止まり状態が存在しないように除去する）■のような入力列に対しても φ を満たすようにふるま

ここで，A = ⟨Q, 2P , ∆, qinit , Acc⟩ の状態 q が行きうことができない可能性がある．つまり，φ の safety

止まりであるとは，ある入力 a ∈ 2I が存在し，任意

成分 Safe(φ) を実現するためのいかなる戦略に従うの出力 b ∈ 2O について，∆(q, a ∪ b) = ∅，即ち，q

ことも，φ 自体を満たすために必要な動作を阻害してから a ∪ b で遷移可能な状態が存在しないことである．

しまう可能性がある．

段階的充足可能は，状態除去操作 (a) と (b) を 1 回

そこで，「各時刻において充足可能性を “真” に保持ずつだけ行うことで判定できる．1 回ずつしか行わなするような出力を決定できるリアクティブシステムがいため，(b) で行き止まり状態が除去されたことによ存在する」という実現可能性必要条件として，新たにり，受理閉路へ到達不能となってしまう状態が存在し真段階的充足可能性を定義する．

得る．一方で，(a) と (b) を繰り返す真段階的強充足

定義 14 (真段階的充足可能性). LTL 式 φ について，可能性判定では，行き止まる状態や，受理閉路へ繰り

以下を満たすリアクティブシステム r ∈ R が存在す

返し到達可能な状態は存在しない．

るとき，φ は真段階的充足可能であるという．
I ∗

I ω

この手続きの正当性は，5. 1 節で示す．

∀x̃ ∈ (2 ) : ∃α ∈ (2 ) : (x̃α) ⊔ r (x̃α) |= φ.
ω

(19)
■
真段階的充足可能性の証拠となる，即ち，式 (19)を満たすリアクティブシステム r は，任意の入力接頭辞に対して充足可能性は保持し，また，何らかの入力接尾辞に対しては仕様をみたすようにふるまうことが可能なシステムである．段階的充足可能性と段階的強充足可能性の定義から，実現可能性は真段階的強充足可能性ともいうべき性質であり，真段階的充足可能性と段階的充足可能性の差は実現可能性と段階的強充足可能性の差と類似している．
この真段階的充足可能性判定手続きは以下のように与えられる．
手続き 15 (真段階的充足可能性判定手続き).
入力：LTL 式 φ
出力：φ が真段階的充足可能か否か

1. L(φ) を受理する決定性オートマトン Aφ を構成する．

2. Aφ に対して以下の 2 ステップの状態除去操作
を変化がなくなるまで繰り返し，初期状態が残っ

3. 2 半強充足可能性
本節では，新たな実現可能性必要条件として半強充足可能性を導入し，その判定手続きを与える．
真段階的充足可能性は，任意の時刻までの有限長出力列（即ち，各時刻の出力）と段階的充足可能性がその存在を保証していた出力接尾辞に関して，一貫した生成戦略が存在することを保証した性質ともいえる．
この性質は式 (16) 中の出力接尾辞 β を r で束縛することで得られたが，逆に，出力接頭辞 r ∗ (x̃) の r による束縛を排除した性質を考えることもできる．この性
質は，「各時刻において，必要であれば過去の出力を改竄することで，充足可能性を保持できるリアクティ
ブシステムが存在する」という段階的充足可能性よりも弱い性質であり，また，「任意の入力接頭辞に対して，仕様を満たすような入力接尾辞及び出力列が存在する」という強充足可能性よりも弱い性質でもある．
そこで，この新しい実現可能性必要条件を半強充足可能性と定義する．†8†8 本文中でも述べているように，この性質は半段階的充足可能性（semi-stepwise satisfiability）ともいえる

定義 16 (半強充足可能性). LTL 式 φ について，以下を満たすとき，φ は半強充足可能であるという．

∀q ∈ Q : ∀s ⊆ P :∆′ (q, s) =∀x̃ ∈ (2I )∗ : ∃α ∈ (2I )ω , ∃β ∈ (2O )ω :(x̃α) ⊔ β |= φ.

(20)■

ここで，φ の半強充足可能性の反例となる入力接頭辞，即ち，以下を満たす有限長入力列 x̃ ∈ (2I )∗ を悪性入力接頭辞（bad input prefix）と呼ぶ．

∀α ∈ (2I )ω , ∀β ∈ (2O )ω , (x̃α) ⊔ β |= φ.

∪∆(q, (s ∩ I) ∪ b).

(23)

b⊆O

定理 18. 手続き 17 は正当な半強充足可能性判定手続きである．

(証明)■

まず，ASeSt
が CSEST (φ) を受理言語とする
φ

オートマトンであることを示す．ステップ 2 においては，φ の悪性接頭辞をもたない語の構成される Asafeφ(21)集合，即ち，φ の safety 成分 Safe(φ) を受理言語とφ の半強充足可能性の反例となる悪性入力接頭辞は φするオートマトンである．そのため，そのオートマト

が成り立たないことを決定付ける有限長入力列であは，なンの出力命題をドントケアに変更した ASeStφ

る．そのような接頭辞をもつ入力列に対する任意の振んらかの出力接頭辞 ỹ ∈ (2O )∗ が存在しそれとの各る舞いの集合を CSEST (φ) で表す．

点和からなる接頭辞 x̃ ⊔ ỹ が悪性接頭辞になることがCSEST (φ) = {x̃α ⊔ β ∈ (2P )ω |I ω

ない入力接頭辞 x̃ ∈ (2I )∗ のみをもつ入力列を受理すO ωα ∈ (2 ) , β ∈ (2 ) andx̃ は φ の悪性入力接頭辞 }.

るオートマトンである．よって，ASeStの補オートマφ(22)

この半強充足可能性判定手続きは以下のように与えられる．

トン ASeSt
は，CSEST (φ) を受理言語とするオートφ
マトンである．
の受理言語がまた，定義 16 と式 (22) より．ASeStφ

手続き 17 (半強充足可能性判定手続き).

空であるならば，かつその時に限り，φ は半強充足可

入力：LTL 式 φ

能である．

出力：φ が半強充足可能か否か

以上により示された．

1. L(φ) を受理するオートマトン Aφ を構成する．

なお，強充足可能性は，ステップ 2 を飛ばし，ス

2. Aφ の受理閉路に到達可能な状態をすべて受理

テップ 3 において「Aφ にラベル付けされている出力状態に変更し，そうでない状態を取り除く．

命題をドントケアに変更する」ことで最終的に得られ• 変更されたオートマトンを Asafeとする．
φ
3. Asafeにラベル付けされている出力命題をドンφ

る CST (φ) を受理するオートマトン ASt
φ の空判定により判定できる．

トケアに変更する．

• 変更されたオートマトンを ASeStとする．
φ

3. 3 段階的許容可能性

4. ASeStの補オートマトン ASeStを構成する．
φφ

本節では，許容可能性と強充足可能性の関係に関す

5. ASeStの空判定を行い，空ならば「半強充足可φる定理を示し，また，新たな実現可能性必要条件とし能」と判定し，そうでないならば「半強充足不て段階的許容可能性を導入し，その判定手続きを与能」と判定する．

■

ここで，A = ⟨Q, 2P , ∆, qinit , Acc⟩ にラベル付けされている出力命題をドントケアに変更するとは，遷移関数 ∆ を，以下を満たす遷移関数 ∆′ で置き換えることを指す．

える．
許容可能性を提案した Damm ら [5] は指摘していないが，強充足可能性の定義から，支配的リアクティ
ブシステムにおいて仕様を満たすようにふるまえな
くてもよい入力列とは，明らかに悪性入力列である．
従って，以下の定理が成り立つ．

性質であるが，「段階的」と呼称される既存の実現可能性必要条件は何らかのリアクティブシステムの存在を示す性質として用いられているため，ここでは半強充足可能性と呼ぶ．

定理 19. LTL 式 φ について，φ が強充足可能かつ許容可能であるならば，かつそのときに限り，φ は実現

可能である．

■(証明) 定義より明らか．

9 のステップ 2–3 を行い，実現可能ならば「段階的許容可能」と判定し，そうでないならば「段階的許容不能」と判定する．

この定理から以下の系が導出される．

■

系 20. LTL 式 φ について，L(φ) ∪ CST (φ) が実現

定理 24. 手続き 23 は正当な段階的許容可能性判定可能であるならば，かつそのときに限り，φ は許容可

手続きである．

■■(証明) 手続き 9 の正当性及び，定理 18 の証明中に即ち，許容可能性は，悪性入力列（強充足可能性の示された CSEST (φ) を受理するオートマトン ASeSt
φ

能である．

反例）を許容するリアクティブシステムの存在を示すの構成法の正当性より明らか．

性質である．同様に，悪性入力接頭辞（半強充足可能

なお，許容可能性は，ステップ 1 で用いるオートマ性の反例）を許容するリアクティブシステムの存在をトン ASeStの代わりに，強充足可能性判定の際に用φ示す性質を考えることもできる．

いられる CST (φ) を受理するオートマトン ASt
φ を利

そこで，この新しい実現可能性必要条件を段階的許用することで判定できる．

容可能性と定義する．
定義 21 (段階的許容可能性). LTL 式 φ について，

4 階層定理L(φ) ∪ CSEST (φ) が実現可能であるとき，φ は段階

本章では，実現可能性必要条件の間の関係に関す的許容可能であるという．

る定理を示す．なお，充足可能，半強充足可能，強充

また，L(φ)∪CSEST (φ) を実現するリアクティブシ

足可能，段階的充足可能，段階的強充足可能，真段階

ステムは φ に関して段階支配的（stepwise dominant)的充足可能，許容可能性，段階的許容可能性，実現■可能な仕様の集合をそれぞれ Sat ，SeStSat ，StSat ，であるという．

支配的リアクティブシステムはすべての無限長入力列に対して最適な出力列を応答するシステムであったが，段階支配的リアクティブシステムは各時刻において最適な出力を応答するシステムである．

SwSat ，SwStSat ，PrSwSat ，Adm ，SwAdm ，Realとする．
森らは，提案した実現可能性必要条件（強充足可能性，段階的充足可能性，段階的強充足可能性）の間の段階的許容可能性の定義より，強充足可能性と許容関係について，以下の定理を示している．

可能性の関係に関する定理 19 と同様の定理が半強充定理 25 ( [15]). 以下の関係が成り立つ．

足可能性と段階的許容可能性に関して成り立つ．

SwStSat ⊂ StSat ⊂ Sat,(24)

定理 22. LTL 式 φ について，φ が半強充足可能かつ

SwStSat ⊂ SwSat ⊂ Sat,(25)

段階的許容可能であるならば，かつそのときに限り，

StSat \ SwSat ̸= ∅,

(26)

■

SwSat \ StSat ̸= ∅,(27)

Real ⊂ SwStSat ⊂ StSat ∩ SwSat.

(28)

φ は実現可能である．
(証明) 定義より明らか．

■

従って，この段階的許容可能性判定手続きは以下のように与えられる．

同様に，本稿で提案した真段階的充足可能性及び半手続き 23 (段階的許容可能性判定手続き).

強充足可能性と，実現可能性及び森らが提案した実現

入力：LTL 式 φ

可能性必要条件との間の関係について，以下の定理が出力：φ が段階的許容可能か否か成り立つ．

1. 手続き 17（半強充足可能性判定手続き）のス

定理 26. 以下の関係が成り立つ．

テップ 1–4 で得られる ASeStを決定化した上で，φ

StSat ∪ SwSat ⊂ SeStSat ⊂ Sat,(29)

手続き 9（実現可能性判定手続き）のステップ 1

PrSwSat ⊂ SwSat,(30)で構成した決定性オートマトンと和合成を行う．

SwSat \ (StSat ∪ PrSwSat) ̸= ∅,(31)

2. その決定性和合成オートマトンに対して手続き

PrSwSat \ StSat ̸= ∅,(32)

力が {req 1 } であっても充足可能性を保持し続けている（段階的充足可能）．これは，入出力接尾辞が(StSat ∩ SwSat) \ (SwStSat ∪ PrSwSat) ̸= ∅,(33){req 2 , res 1 }ω であれば f29 が成り立つためである．ま(StSat ∩ PrSwSat) \ SwStSat ̸= ∅,(34)

た，{req 1 }ω が f29 に対する悪性入力列である（強充SwStSat \ PrSwSat ̸= ∅,(35)足不能）．そして，初期入力が {req 1 } であるとき，充Real ⊂ SwStSat ∩ PrSwSat.

(36)

足可能性を保持するためには ¬res 1 を出力し続けな■ければならない．これは，一度でも res 1 を出力して(証明) 式 (29) と式 (30)，式 (36) の関係が部分集合しまうと，それ以後 2req 2 を成立させなければならであることは定義から明らかである．それらが真部分

ないが，システムは入力接尾辞を制御できないため集合であること及び式 (31)–(35) は補題 27–34 よりである．しかし，充足可能性を保持するために ¬res 1

成り立つ．

を出力し続けていれば 3res 1 を成立させることはで

補題 27. 充足可能かつ半強充足不能な仕様が存在きない（真段階的充足不能）．従って，f29 は段階的■充足可能かつ強充足不能かつ真段階的充足不能であ

する．

る．

(証明) 以下の LTL 式 f27 を考える．
f27 = (req 1 → res 1 ) ∧ (req 2 → ¬res 1 ).

(37)

補題 30. 真段階的充足可能かつ強充足不能な仕様が

■

存在する．

ただし，req 1 , req 2 ∈ I ，res 1 ∈ O である．
このとき，初期入出力が {req 1 , res 1 } であれば f27は成り立つ（充足可能）．また，{req 1 , req 2 } が f27に対する悪性入力接頭辞である（強充足不能）．従っ(証明) 以下の LTL 式 f30 を考える．
f30 = (23req 1 → 23res 1 )∧ (32req 2 → 32¬res 1 ).

(40)

ただし，req 1 , req 2 ∈ I ，res 1 ∈ O である．

て，f27 は充足可能かつ半強充足不能である．
補題 28. 半強充足可能かつ強充足不能かつ段階的充

このとき，常に res 1 を出力し続けるシステムは，■{req 1 }ω が接尾辞の任意の入力列に対して f30 を満

足不能な仕様が存在する．

たすようにふるまう（真段階的充足可能）．また，(証明) 以下の LTL 式 f28 を考える．

{req 1 , req 2 }ω が f30 に対する悪性入力列である（強f28 = 2(res 1 ↔ ⃝req 1 ) ∧ 32(req 2 → ¬res 1 ).
(38)
ただし，req 1 , req 2 ∈ I ，res 1 ∈ O である．

充足不能）．従って，f30 は真段階的充足可能かつ強充足不能である．

このとき，接尾辞が {req 1 } である任意の入力列 ã

補題 31. 強充足可能かつ段階的充足可能かつ段階的に対して，f28 を成立させる（req 1 出現の 1 ステップ

強充足不能かつ真段階的充足不能な仕様が存在する．

前に res 1 を置く）出力列が存在する（半強充足可能）．

■

また，{req 1 , req 2 } が f28 に対する悪性入力列である(証明) 後述の式 (43) で与えられる LTL 式 f33 を部（強充足不能）．そして，左連言肢 2(res 1 ↔ ⃝req 1 )分式として含む，以下の LTL 式 f31 を考える．

ω

ω

は典型的な段階的充足不能な式である．従って，f28
は半強充足可能かつ強充足不能かつ段階的充足不能

f31 = (32req 1 ↔ res 1 ) ∧ ⃝f33 .

(41)

ただし，req 1 ∈ I ，res 1 ∈ O である．
このとき，連言肢は意味的に互いに独立である．まである．
補題 29. 段階的充足可能かつ強充足不能かつ真段階

た，補題 33 の照明中で述べるように f33 は強充足■

可能かつ段階的充足可能かつ真段階的充足不能であ的充足不能な仕様が存在する．

り，右連言肢 ⃝f33 と同様である．そして，左連言肢(証明) 以下の LTL 式 f29 を考える．
f29 = (req 1 → 3res 1 ) ∧ 2(res 1 → 2req 2 ).

(39)

ただし，req 1 , req 2 ∈ I ，res 1 ∈ O である．
このとき，∅ を出力し続けるシステムは，初期入(32req 1 ↔ res 1 ) に関しては，無限にしばしば req 1が入力されるか否かに応じた初期出力が存在し（強充足可能），また，任意の初期出力に対しても f31 を成立にする入力接尾辞が存在する（段階的充足可能）がf31 を不成立にする入力接尾辞も存在する（段階的強充足不能）．従って，f31 は強充足可能かつ段階的充足可能かつ段階的強充足不能かつ真段階的充足不能
である．

' Sat
'
'
StSat
'
'
SwStSat'Real

補題 32. 強充足可能かつ真段階的充足可能かつ段階
的強充足不能な仕様が存在する．

■(証明) 以下の LTL 式 f32 を考える．
f32 = 23req 1 ↔ res 1 .

(42)

ただし，req 1 ∈ I ，res 1 ∈ O である．
このとき，無限にしばしば req 1 が出現する入力列$$
SeStSat
$
f28
$
$
f31
f33
f29
$

f34

&
&
&
PrSwSat
&
&
&
図1

f27

%
f30%
%
%
SwSat
%
%
f32

実現可能，真段階的充足可能，段階的強充足可能，に対しては {res 1 }ω ，そうでない入力列に対しては段階的充足可能，強充足可能，半強充足可能，充足可能な∅ω という出力列で f32 を満たす（強充足可能）．ま仕様の集合（それぞれ Real ，PrSwSat ，SwStSat ，た，初期出力が ∅ であるシステムは，∅ω が接尾辞のSwSat ，StSat ，SeStSat ，Sat ）の包含関係．ただし，任意の入力列に対して f32 を満たすようにふるまう

f27 –f34 は，それぞれ，補題 27–34 の証明中で挙げてい（真段階的充足可能）．そして，初期出力が res 1 のとた，その領域に含まれる式の例である．

き ∅ω ，そうでないとき {req 1 }ω が接尾辞の入力列に対して f32 を成立させる出力接尾辞が存在しない．
（段

たす（段階的強充足可能）．また，res 1 を出力し続け階的強充足不能）．従って，f32 は強充足可能かつ真るシステムは，∅ω が接尾辞の入力列に対して，f34 を段階的充足可能かつ段階的強充足不能である．

満たすようにふるまう真段階的充足可能）．しかしな

補題 33. 段階的強充足可能かつ真段階的充足不能ながら，res 1 を常に出力する/しないようになるタイミ■

ングを環境の協力なしに決定できない．
（実現不能）．

仕様が存在する．

(証明) 以下の LTL 式 f33 を考える．

従って，f34 は段階的強充足可能かつ真段階的充足可

f33 = (req 2 → 3res 1 )∧ 2(res 1 → ⃝2(⃝req 2 ↔ res 1 )).

能かつ実現不能である．

(43)

ただし，req 2 ∈ I ，res 1 ∈ O である．

定理 25 と定理 26 が示す包含関係をまとめると，図1 のように与えられる．

このとき，∅ を出力し続けるシステムは強充足可能

また，充足可能性，半強充足可能性，強充足可能性を保持し続けている（段階的強充足可能）．これ性，許容可能性，段階的許容可能性の間の関係に関しは，2(⃝req 2 ↔ res 1 ) が強充足可なためである．まては，以下の定理が成り立つ．

た，f29 と同様の理由で，f33 は真段階的充足不能で定理 35. 以下の関係が成り立つ．

ある．従って，f33 は段階的強充足可能かつ真段階的Sat c ⊂ SwAdm ⊂ Adm,(45)

充足不能である．

StSat \ Adm ̸= ∅,(46)

SeStSat \ (StSat ∪ Adm) ̸= ∅,(47)

Sat \ (SeStSat ∪ Adm) ̸= ∅,(48)(SeStSat ∩ Adm) \ SwAdm ̸= ∅,(49)(Sat ∩ Adm) \ (SeStSat ∪ SwAdm) ̸= ∅,(50)(Sat ∩ SwAdm) \ SeStSat ̸= ∅.

(51)

補題 34. 段階的強充足可能かつ真段階的充足可能かつ実現不能な仕様が存在する．

■(証明) 以下の LTL 式 f34 を考える．
f34 = 23req 1 ↔ 32res 1 .

(44)

ただし，req 1 ∈ I ，res 1 ∈ O である．
このとき，req 1 が無限にしばしば出現する入力列にc

ただし， は補集合演算である．

■

ω

対しては {res 1 } ，そうでない入力列に対しては ∅(証明) SwAdm ⊆ Adm は定義より明らか．これがが接尾辞の出力列で，出力接頭辞に関わらず f34 を満

真部分集合であることは，式 (49) や式 (50) より成ωり立つ．Sat c ⊂ SwAdm は, 仕様 φ が充足不能ならば CSEST (φ) = (2P )ω であること及び実現可能
ならば段階的許容可能であることから成り立つ．式

'
Sat
'
'
StSat
'

f36

✓

補題 36. 強充足可能かつ許容不能な仕様が存在する．

■(証明) 強充足可能かつ段階的充足不能な以下の LTL

✓&
&
&
✓

式 f36 を考える．

(52)

ただし，req 3 ∈ I ，res 2 ∈ O である．

図2

このとき，CST (f36 ) が空集合であるため，f36 は許容不能である．

$
$
$
f38
f37
$
$

'

(46)–(51) は，以下の補題 36–41 より成り立つ．

f36 = 2(⃝req 3 ↔ res 2 ).

SeStSat

f39

Real

✓&
SwAdm
&

%
%
f40
f41
%
Adm

%
%

実現可能，強充足可能，段階的許容可能，半強充足可能，許容可能，充足可能な仕様の集合（それぞれ，Real ，StSat ，SwAdm ，SeStSat ，Adm ，Sat ）の包含関係．た補題 37. 半強充足可能かつ強充足不能かつ許容不能

だし，f36 –f41 は，それぞれ，補題 36–41 の証明中で挙■げていた，その領域に含まれる式の例である．また，チェッな仕様が存在する．

(証明) 半強充足可能かつ強充足不能な LTL 式 f28

ク記号 ✓ が付けられた領域は空集合である．

と，強充足可能かつ段階的充足不能な LTL 式 f36 の(証明) 半強充足可能かつ許容可能かつ強充足不能か

連言 f37 を考える．

f37 = f28 ∧ f36 .

(53)

つ段階的許容不能な LTL 式 f39 と，後述の式 (57) で各連言肢は意味的に互いに独立であるため，それら与えられる充足可能かつ段階的許容可能かつ半強充足不能な LTL 式 f41 の連言 f40 を考える．

の連言 f37 は明らかに許容不能である．

f40 = f39 ∧ f41 .

補題 38. 充足可能かつ半強充足不能かつ許容不能な

(56)

■

各連言肢は意味的に互いに独立であるため，この連(証明) 充足可能かつ半強充足不能な LTL 式 f27 と，

言 f40 は充足可能かつ許容可能かつ半強充足不能かつ強充足可能かつ段階的充足不能な LTL 式 f36 の連言

段階的許容不能である．

φ38 を考える．

補題 41. 充足可能かつ段階的許容可能かつ半強充足仕様が存在する．

f38 = f27 ∧ f36 .

(54)

各連言肢は意味的に互いに独立であるため，それら不能な仕様が存在する．

(証明) 以下の LTL 式 f41 を考える．
f41 = 2req 2 .

の連言 f38 は明らかに許容不能である．
補題 39. 半強充足可能かつ許容可能かつ強充足不能
かつ段階的許容不能な仕様が存在する．

■

(57)

ただし，req 2 ∈ I である．
このとき，f41 は充足可能かつ半強充足不能である．そして，CSEST (f41 ) は L(f41 ) の補集合である．

(証明) 以下の LTL 式 f39 を考える．
f39 = 32req 1 .

■

(55)

ただし，req 1 ∈ I である．

従って，f41 は充足可能かつ段階的許容可能かつ半強充足不能である．

このとき，f39 は半強充足可能かつ強充足不能である．そして，CSEST (f39 ) は空集合，CST (f39 ) は定理 19 と定理 22，定理 35 が示す包含関係をまとめると，図 2 のように与えられる．

L(f39 ) の補集合である．従って，f39 は半強充足可能
かつ許容可能かつ強充足不能かつ段階的許容不能で5 不完全合成ある．

本章では，3. 1–3. 3 節で提案した実現可能性必要条

補題 40. 充足可能かつ許容可能かつ半強充足不能かつ段階的許容不能な仕様が存在する．

■

件に基づいて，与えられた仕様から不完全なリアク
ティブシステムを合成する手法を与える．

5. 1 真段階的充足可能性に基づいた不完全合成
本節では，真段階的充足可能な仕様から，式 (19)まとめると，真段階的充足可能な仕様からの不完全合成手続きは以下のように与えられる．

を満たすリアクティブシステムを合成する手続きを与手続き 42 (真段階的充足可能性に基づいた不完全合

える．

成手続き).

手続き 15（真段階的充足可能性判定手続き）のス
テップ 2 において，Aφ に対して 2 ステップの状態除

入力：真段階的充足可能な LTL 式 φ
出力：式 (19) を満たすリアクティブシステム

去操作を変化がなくなるまで繰り返した結果の決定

1. 手続き 15 のステップ 2 の状態除去操作を変化= ⟨Q, 2P , ∆, qinit , Acc⟩ と性オートマトンを APrSw
φがなくなるまで繰り返し，その結果のオートマト

する．このオートマトン上の任意の状態は，受理実行

ン APrSwを得る．
φに繰り返し到達可能，かつ，行き止まりでない．ここの SCC 分解を行い，受理 SCC 毎に 1 つ
2. APrSw
φで，オートマトンの現在の状態が q であるとき入力ずつ受理閉路を抽出し，そこに現れる状態の集合

a ⊆ I に対して何を出力するかを決定する関数（即Qacc 得る．

Iち，戦略）µ : Q × 2 → 2

Oは，以下のリアクティブシステム rµ と見なせる．

3. Qacc へ到 達す る まで の 距離 DQacc から ，式(61) を満たす戦略 µQacc （リアクティブシステ

rµ (a0 · · · an ) = µ(qn , an ).

(58)

■

定理 43. 手続き 15 と手続き 42 はそれぞれ正当な真

ただし，q0 = qinit かつ任意の i < n について，{qi+1 } = ∆(qi , ai ∪ µ(qi , ai )).

ム rµQacc ）を生成し出力する．

(59)

APrSw
の構成法から，各状態及び各入力に対してφ

段階的充足可能性判定手続きと式 (19) を満たすリア
クティブシステムの合成手続きである．

■

遷移を可能とする出力が存在し，また，どの状態も初(証明) Q ̸= ∅ のとき，APrSw
構成法から，Q に含φ期状態から到達可能かつ受理強連結成分（受理 SCC）

まれる任意の状態は初期状態から到達可能かつ受理に到達可能である．よって，現在の状態が受理閉路上SCC に到達可能であり，非空な Qacc を必ず得ることにある場合には受理閉路を辿り，そうでない場合にはができる．Qacc が固定されていれば，DQacc と µQacc

近づくように出力を決定する戦略 µ は，式 (19) を満PrSwは一意に定まる．ここで，Aφが行き止まり状態

たすリアクティブシステムと等価である．

をもたないことから，rµQacc は全域的関数である．まそこで，各受理 SCC から受理閉路をちょうど 1 つた，すべての状態から Qacc へ到達可能もあるため，ずつ抽出する．ただし，それらの受理閉路上に現れる

DQacc はすべての状態に対して有限の値をもってい状態は重複しないものとし，抽出した各受理閉路上にる．そして，Qacc を構成する受理閉路が属する SCC現れる状態の集合を Qacc とする．このとき，各状態は相異なるため，異なる受理閉路上の 2 つの状態が互から Qacc へ到達するまでの距離 DQacc (q) は以下のいに到達可能となることはない．よって，任意の入力ように与えられる．

接頭辞に対して，DQacc を 0 まで減少させ（つまり，DQacc (q) = min{n | qn ∈ Qacc andq0 q1 . . . qn ∈ Path

なんらかの受理閉路に到達し）その後 DQacc が 0 で
APrSw
φ

(q)}.

(60)
各状態 q において入力部分が a ⊆ I である場合に，
DQacc (q ′ ) が最も小さい状態に遷移するための出力をあることを保持する（つまり，その閉路を巡回し続ける）入力接尾辞が存在する．即ち，rµQacc は式 (19)を満たすリアクティブシステムである．

Q = ∅ のとき，任意の入力列に対して，受理閉路へ選ぶ戦略，即ち，以下を満たす戦略 µQacc が目的の関繰り返し到達可能ないずれかの状態に留まらせる戦略数である．

が存在しない．よって，真段階的強充足不能である．

µQacc (q, a) =argmin{DQacc (q ′ ) | q ′ ∈ ∆(q, a ∪ b)}. (61)b⊆O

以上により示された．

5. 2 半強充足可能性に基づいた不完全合成

段階的強充足可能性を導入し [15] [27]，また，その判半強充足可能性は，なんらかのリアクティブシステ

定手続きを与えている [23] [15] [27]．これらの性質及びムの存在を示す性質ではなく，また，充足可能性に次その充足判定手続きにより，仕様が実現不能であっいで実現可能性から遠い．そこで，この性質と許容可た際に，その欠陥を分類することを可能とした．ま能性を組み合わせて不完全合成に利用する．

た，これら性質の判定問題は，実現可能性判定/自動系 20 から，仕様 φ の許容可能性判定は L(φ) ∪合成（2EXPTIME 完全 [16] [18]）よりも計算量が小CST (φ) の 実 現 可 能 性 判 定 と 同 値 で あ る ．こ のさく，仕様の修正・洗練を効率的に行うことも可能とL(φ) ∪ CST (φ) の実現可能性判定では，通常の LTLしている．判定の効率化も盛んに研究されており，安実現可能性判定と同様に，L(φ) ∪ CST (φ) を実現す

藤らは分散計算による効率的な段階的充足可能性判るリアクティブシステム（即ち，φ に対する支配的リ定手続きを実装した [25]．また，島川らは，SAT ベー

アクティブシステム）を合成できる．

スの有界強充足可能性判定を提案し [21]，さらに，強従って，仕様が許容可能であれば，その仕様に対す充足可能性判定の計算量が EXPSPACE 完全である

る支配的リアクティブシステムを合成でき，さらにそことを示した [22]．これらの実現可能性必要条件充足の仕様が半強充足可能ならば，そのシステムは悪性入判定では欠陥の種類を分類できるが，具体的に仕様の力接頭辞をもたない悪性入力列のみを許容すること

どの箇所に欠陥があるかを特定できない．そのため，を保証できる．即ち，そのシステムは，仕様に反する

萩原らは，仕様の欠陥箇所を特定する手法として，強ための選択を永久に行い続ける環境のみを許容する．

充足不能の原因となる最小な部分仕様抽出する手法を提案していた [10]．

5. 3 段階的許容可能性に基づいた不完全合成

一方，本研究では，新たに 3 つの実現可能性必要定義 21 から，仕様 φ の段階的許容可能性判定は条件を提案し，その充足判定手続きを与えている（3L(φ) ∪ CSEST (φ) の実現可能性判定と同値である．

章各節）．また，既存のものも含め，実現可能性必要

この L(φ) ∪ CSEST (φ) の実現可能性判定では，通常条件の間の関係についての定理を示した（4 章）．この LTL 実現可能性判定と同様に，L(φ) ∪ CSEST (φ)

れにより，これまでよりも詳細な仕様欠陥解析が可能を実現するリアクティブシステム（即ち，φ に対するとなる．提案した判定手続きは，既存実現可能性必要段階支配的リアクティブシステム）を合成できる．

条件充足判定手続きと類似のものであるため，既存の従って，仕様が段階的許容可能であれば，その仕様

効率化・応用技術を適用することも可能である．

に対する段階支配的リアクティブシステムを合成できる．このシステムは，5. 2 節で与えた半強充足可能

6. 2 リアクティブシステム合成

性と許容可能性に基づいた不完全合成で得られるシ

素朴な実現可能性判定手続き（手続き 9）では，ス

ステムとは異なり，悪性入力接頭辞をもつ入力列のみ

テップ 1 において，LTL2dstar†4 [12] で実装されてを許容するシステムである．即ち，そのシステムは，仕様に反することを有限時間以内に決定付けてしまいる Safra の構成法 [19] や，Rabinizer3†6 で実装されている Esparza-Křetı́nský 法 †5 [8] などを用いた

う一連の選択を行う環境のみを許容する．

ω-正規オートマトンの決定化が必要である．これらの手法は非常に煩雑で効率化が困難なため，実現可能6 関連研究6. 1 実現可能性必要条件

性判定/自動合成では Safraless†5 な手続き [13] [20] [9]がいくつも提案されており，Lily†9 [11]，Unbeast†10

最も基本的な実現可能性必要条件は充足可能性（無矛盾性）である．しかしながら，充足可能性と実現可能性の間の隔たりは非常に大きい．森らは，その隔たりを埋める，強充足可能性，段階的充足可能性，†9 http://www.iaik.tugraz.at/content/research/
design_verification/lily/†10 http://www.react.uni-saarland.de/tools/
unbeast/[7]，Acacia+†11 [4]， [26] などの合成器が開発された．

そして，実現可能性必要条件に基づいた一定の水準

本研究では，これらの手続き/ツールが目的とする，

を満たすシステムを合成する不完全合成手法を提案

仕様を厳密に実現する完全なリアクティブシステムのした. これにより，仕様が実現不能であっても，仕様

合成ではなく，新たに導入した 3 つの実現可能性必に反するふるまいをある程度許容するシステムを合要条件に基づいた不完全な合成を扱っている（5 章）．

成できる．

吉浦らは段階的充足可能性に基づいた不完全合成手法を提案していた [23]．その手法で得られるシステム

7. 2 今後の課題

は，3. 1 節でも述べたように，どのような入力列に対仕様に欠陥がなかったとしても，その規模が大きけしても仕様を満たすようにはふるまうことができな

れば現実的な時間では実現可能性判定/合成することい可能性がある．それに対して，5. 1 節の真段階的充はできない．そのため，現実的な問題に対応するため足可能性に基づいた不完全合成では，仕様を満たすよには，仕様が実現可能か否かに関わらず，尤もらしくうな入力列が必ず保証された，より実現に近いシス

ふるまうシステムを合成する手法の開発は非常に重テムを合成できる．また，Damm らは，許容可能性要である．それが今後の課題の 1 つである．

に基づいた不完全合成手法を提案していた [5]．その

また，現実的な問題を扱うためには，実現可能性判

不完全合成手法は悪性入力列を許容するシステムを定の問題設定には改良の余地がある．実現可能性判定

合成するものであり，不完全合成された各部分システの問題設定では，「外部環境は仕様に反するよう敵対

ムを不備が露呈しないように組み合わせ，全体とし的にふるまう」という仮定を置いているに等しい．実て安全な分散システムの構成する応用手法も提案さ際，実現可能性判定/合成では，システムと環境の相れている [5]．一方，5. 2 節と 5. 3 節で与えた不完全合

互作用は敵対的なゲームとしてモデル化されている．

成では，それぞれ許容するふるまいを「悪性入力接頭しかしながら，なんらかのサービスを提供するシステ

辞をもたないもの」と「悪性入力接頭辞をもつもの」

ムとそのサービスを利用するユーザ（外部環境）の関にさらに限定したシステムを合成できる．

係のように，必ずしもシステムと環境の目的が相反しない場合にはその相互作用は協力ゲーム（非零和ゲー

7 おわりにム）としてモデル化することが妥当である．そのよう7. 1 結論な相互作用する主体毎に異なる目的をもち得る場合の本研究では，以下の 3 つの新しい実現可能性必要

一般化実現可能性に関する研究も今後の課題である．

条件を導入した．

• 真段階的充足可能性

参 考 文 献• 半強充足可能性[ 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 ] Babiak, T., Křetı́nský, M., Řehák, V., andStrejček, J.: LTL to Büchi Automata Translation: Fast and More Deterministic, Tools and Algorithms for the Construction and Analysis of Systems, Flanagan, C. and König, B.(eds.), Lecture
Notes in Computer Science, Vol. 7214, Springer
Berlin Heidelberg, 2012, pp. 95–109.
[ 3 ] Bloem, R., Ehlers, R., Jacobs, S., andKönighofer, R.: How to Handle Assumptions inSynthesis, Proceedings 3rd Workshop on Synthesis,• 段階的許容可能性
また，これらの新たな必要条件に関して，既存の実現可能性必要条件充足判定手続きと類似の充足判定手法も与えた．さらに，既存のものも含め，実現可能性
必要条件間の階層定理を証明した．本研究で導入した
必要条件は既存の必要条件及び実現可能性の間の隔たりを埋めるものであり，より詳細な仕様欠陥分析が可能となる．

†11 http://lit2.ulb.ac.be/acaciaplus/

Chatterjee, K., Ehlers, R., and Jha, S.(eds.), Electronic Proceedings in Theoretical Computer Science, Vol. 157, Open Publishing Association, 2014,
pp. 34–50.
[ 4 ] Bohy, A., Bruyére, V., Filiot, E., Jin, N., andRaskin, J.-F.: Acacia+, a Tool for LTL Synthesis,
Computer Aided Verification, Madhusudan, P. andSeshia, S.(eds.), Lecture Notes in Computer Science, Vol. 7358, Springer Berlin Heidelberg, 2012,
pp. 652–657.
[ 5 ] Damm, W. and Finkbeiner, B.: Automatic
Compositional Synthesis of Distributed Systems,
FM 2014: Formal Methods, Jones, C., Pihlajasaari,P., and Sun, J.(eds.), Lecture Notes in Computer
Science, Vol. 8442, Springer International Publishing, 2014, pp. 179–193.
[ 6 ] Duret-Lutz, A. and Poitrenaud, D.: SPOT:
an Extensible Model Checking Library Using
Transition-Based Generalized Büchi Automata,Modeling, Analysis, and Simulation of Computer
and Telecommunications Systems, 2004. (MASCOTS 2004). Proceedings. The IEEE Computer
Society’s 12th Annual International Symposium on,IEEE Computer Society, 2004, pp. 76–83.
[ 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 ] Esparza, J. and Křetı́nský, J.: From LTL to Deterministic Automata: A Safraless Compositional
Approach, Computer Aided Verification, Biere, A.
and Bloem, R.(eds.), Lecture Notes in Computer
Science, Vol. 8559, Springer International Publishing, 2014, pp. 192–208.
[ 9 ] 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.
[10] Hagihara, S., Egawa, N., Shimakawa, M., andYonezaki, N.: Minimal Strongly Unsatisfiable Subsets of Reactive System Specifications, Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE ’14,
ACM, 2014, pp. 629–634.
[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] 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.
[13] Kupferman, O. and Vardi, M.: Safraless Decision Procedures, Foundations of Computer Science,
2005. FOCS 2005. 46th Annual IEEE Symposium

on, 2005, pp. 531–540.
[14] Mochizuki, S., Shimakawa, M., Hagihara, S.,
and Yonezaki, N.: Fast Translation from LTL
to Büchi Automata via Non-transition-based Automata, Formal Methods and Software Engineering, Merz, S. and Pang, J.(eds.), Lecture Notes in
Computer Science, Vol. 8829, Springer International
Publishing, 2014, pp. 364–379.
[15] Mori, R. and Yonezaki, N.: Several Realizability Concepts in Reactive Objects, Information Modelling and Knowledge Bases IV, Kangassalo, H.,
Jaakkola, H., Hori, K., and Kitahashi, T.(eds.),
Frontiers in Artificial Intelligence and Applications,Vol. 16, IOS Press, 1993, pp. 407–424.
[16] 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, ACM, 1989,
pp. 179–190.
[17] Pnueli, A.: The Temporal Logic of Programs,
Foundations of Computer Science, 1977., 18th Annual Symposium on, 1977, pp. 46–57.
[18] Rosner, R.: Modular Synthesis of Reactive Systems, PhD Thesis, Weizmann Institute of Science,
1992.
[19] Safra, S.: On the Complexity of Omega Automata, Proceedings of the 29th Annual Symposium
on Foundations of Computer Science, SFCS ’88,
IEEE Computer Society, 1988, pp. 319–327.
[20] 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.
[21] Shimakawa, M., Hagihara, S., and Yonezaki, N.:
SAT-Based Bounded Strong Satisfiability Checkingof Reactive System Specifications, Information andCommunication Technology, Mustofa, K., Neuhold,E., Tjoa, A., Weippl, E., and You, I.(eds.), Lecture Notes in Computer Science, Vol. 7804, Springer
Berlin Heidelberg, 2013, pp. 60–70.
[22] Shimakawa, M., Hagihara, S., and Yonezaki, N.:
Complexity of Checking Strong Satisfiability of Reactive System Specifications, Signal Processing andInformation Technology, Das, V. and Elkafrawy,P.(eds.), Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, Vol. 117, Springer International Publishing, 2014, pp. 41–50.
[23] Yoshiura, N.: Decision Procedures for Several
Properties of Reactive System Specifications, Software Security - Theories and Systems, Futatsugi,K., Mizoguchi, F., and Yonezaki, N.(eds.), Lecture Notes in Computer Science, Vol. 3233, Springer
Berlin Heidelberg, 2004, pp. 154–173.
[24] Yoshiura, N. and Yonezaki, N.: Program Synthesis for Stepwise Satisfiable Specification of Re-

active System, Principles of Software Evolution,
2000. Proceedings. International Symposium on,
2000, pp. 58–67.
[25] 安藤崇央, 宮本佑樹, 萩原茂樹, 米崎直樹: リアクティ
ブシステム仕様に対する段階的充足可能性判定器の分散オブジェクト技術を利用した実装, コンピュータ ソフト
ウェア, Vol. 28, No. 4(2011), pp. 262–281.
[26] 上野篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹:

LTL 式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装に関する研究, 日本ソフト
ウェア科学会第 30 回大会論文集, 2013.
[27] 森亮靖, 友石正彦, 米崎直樹: 時相論理によるリア
クティブシステム仕様の実現可能性に関する分類, コン
ピュータ ソフトウェア, Vol. 15, No. 3(1998), pp. 213–
225.