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

リアクティブシステム実現可能性必要条件の判定手続き
冨田 尭

外部環境と継続的に相互作用するリアクティブシステムの高信頼化のために，その動作仕様を線形時相論理 LTL な
どで形式的に記述してその実現可能性を判定した上でシステムを自動合成する手法が研究されてきた．また，仕様が実現不能であった場合にその欠陥を効果的に分類するために，網羅性，戦略化可能性，保存可能性，安定化可能性の観点から階層的・体系的に定義される実現可能性必要条件群が導入されている．しかし，形式検証でしばしば用いられる ω-正規仕様に対する実現可能性必要条件判定手続きは，一部の必要条件にしか与えられておらず，近年新たに導入された実現可能性必要条件群の判定手続きが与えられていなかった．
本稿では，仕様欠陥分析を実施可能にするために，それらの実現可能性必要条件群に対する系統的な判定手続き
群を与える．実現可能性必要条件群が体系的に整理されたことで，それらの判定手続きもいくつかの共通的操作の組合せとして構成できる．また，判定手続きの対称性に基いた新たな実現可能性必要条件及びその判定手続きも与える．そして，判定問題に対する計算量上界について考察する．

ができれば，仕様を実現するリアクティブシステムを

1 はじめに
1. 1 背景

確実に得ることができる．
しかしながら，実現可能性判定及び自動合成は一リアクティブシステム合成（reactive system syn-

般に計算コストが非常に大きく，欠陥のある仕様を試

thesis）とは，利用者や外部システムなど環境（envi-

行錯誤を通して実現可能かつ合理的になるよう修正・

ronment）と継続的に相互作用するリアクティブシス

洗練することは容易ではない．そのため，森ら [25] 及

テムを仕様から自動的に合成する手法である．リアク

び冨田ら [45] [34] は，充足可能性よりも強い実現可能

ティブシステムは環境からの入力を制御できないた

性必要条件を階層的・体系的に提案した．

め，与えられた仕様（speciﬁcation）を満たすリアク• 振舞性必要条件

ティブシステムが存在するためには，その仕様は無矛– 接 頭 的 半 強 充 足 可 能 性 [45]（preﬁxically

盾，即ち，充足可能（satisﬁable）なだけでは不十分

semi-strong satisﬁability）

であり，実現可能 [26] [1] [29]（realizable）でなければ– 接 尾 的 半 強 充 足 可 能 性 [34]（suﬃxicallyならない．リアクティブシステム合成は，仕様の実現

semi-strong satisﬁability）

可能性判定も兼ねており，仕様が実現可能であるとき– 接尾的半真強充足可能性 [34]（suﬃxicallyにシステムを得ることができる．その際，仕様記述以

semi-properly strong satisﬁability）

外の工程では，人手を介さないため，不具合が混入す– 強充足可能性 [25]（strong satisﬁability）

る恐れがない．そのため，妥当な仕様さえ与えること– 真強充足可能性 [34]（properly strong sat-

Decision Procedures for necessary conditions of Reactive System Speciﬁcations.
Tomita, Takashi, 北陸先端科学技術大学院大学 情報社会基盤研究センター, Research Center for Advanced Computing Infrastructure, Japan Advanced Institute of
Science and Technology.

isﬁability）• 保存性必要条件– 保存的充足可能性 †1 [25]（preservably step-†1[25] [43] [38] [45] 用いられている「段階的」に代わりに，本稿では単に「保存的」という用語を用い， [34]

wise satisﬁability）– 保 存 的 強 充 足 可 能 性 †1 [25]（preservably

2 準備

stepwise strong satisﬁability）– 真 保 存 的 充 足 可 能 性 †1 [45]（properly

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

preservably stepwise satisﬁability）• 安定性必要条件– 安定的充足可能性 †2 [34]（stably stepwise
satisﬁability）– 安定的強充足可能性 †2 [34]（stably stepwise
strong satisﬁability）

これらの必要条件充足判定を行うことで，仕様に欠陥がある，即ち，仕様が実現不能である際に，欠陥の外部環境と継続的に相互作用する開放系はしばしばリアクティブシステムとしてモデル化される．受信した感知信号を基に制御信号を送信して対象を制御し続けるような制御器はその典型例である．非形式的には，リアクティブシステムは次のような特徴を持つ．

1. 入力非制御性（Input uncontrollability）：リア
クティブシステムは，自身から環境へ出力のみを制御でき，環境から自身への入力は制御できない．

分類や分析，欠陥箇所抽出 [18] により，効率的な仕様

2. 出力逐次性（Output sequentiality）：各時刻の修正が可能となる．しかしながら， [34] で新たに導入

出力は，過去の振舞い（入出力列）のみから決定された実現可能性必要条件群に対しては判定手続き

されなければならない．

が提案されていなかった．

ここで，リアクティブシステム・環境が制御する出力・入力イベントの出現を表す出力・入力命題をそれ

1. 2 目的

ぞれ O と I と記す．形式的には，リアクティブシス

本稿では，仕様欠陥分析を実施可能にするために，

テムは次のように定義される．

これらの実現可能性必要条件群に対する系統的な判定手続き群を与える．
実現可能性必要条件群は階層的・体系的に定義されており， [25] [45] で導入された実現可能性必要条件の判定手続きはいくつかの共通的操作の組合せとして与えることができる．そこで， [25] [45] で導入された実現可能性必要条件の判定手続きをその共通的操作の組み合わせとして再整理するとともに， [34] で新たに導入された実現可能性必要条件にも判定手続きも同様の形で与える．
また，共通的操作の組み合わせとして再整理した結果として発見された手続き間の対称性に基づき新し

定義 1 (リアクティブシステム) リアクティブシステ
ムは，応答関数 r : (2I )+ → 2O である．

■

ここで，すべての可能なリアクティブシステムの集合を R と記す．また，環境からの無限入力列（つまり無限入力語）α = a0 · a1 · · · ∈ (2I )ω に対する，リアクティブシステム r の無限出力列（つまり無限出
力語）r(a0 ) · r(a0 · a1 ) · · · ∈ (2O )ω を rω (α) と記す．
そして，無限入力列 α = a0 · a1 · · · ∈ (2I )ω と無限出
力列 β = b0 · b1 · · · ∈ (2O )ω の各点和集合列（つまり無限入出力語）(a0 ∪ b0 ) · (a1 ∪ b1 ) · · · ∈ (2I∪O )ω を

[α, β] と記す．

い保存性必要条件• 真保存的強充足可能性（properly preservably
stepwise strong satisﬁability）
及びその判定手続きを与える．さらに判定問題の計算量上界を示す．
で用いられている「preservably stepwise」の訳とし
て当てる．

†2

[34] で用いられている「stably stepwise」の訳として，本稿では単に「安定的」という用語を当てる．

定義 2 (振舞い) リアクティブシステム r ∈ R の無限入力列 α ∈ (2I )ω に対する振舞いは，各点和集合
列 [α, rω (α)] ∈ (2I∪O )ω である．

■

無限入力列 α ∈ (2I )ω 及び無限出力列 β ∈ (2O )ω
は，それぞれ α = ᾱ· α̂ 及び β = β̄· β̂ であるような（1）
任意有限長の接頭語 ᾱ ∈ (2I )∗ 及び β̄ ∈ (2O )∗ と（2）無限長の接尾語 α̂ ∈ (2I )ω 及び β̂ ∈ (2O )ω に分割で

きる．そこで，有限入力列 ᾱ = a0 · a1 · · · an ∈ (2I )∗s0 · s1 · s2 · · · ∈ Σω の文字 si を先頭から順に読み，に対する，リアクティブシステム r の有限出力列

現在の状態 qi （ただし q0 = qinit ）とその文字 si かO ∗∗r(a0 ) · r(a0 · a1 ) · · · r(a0 · a1 · · · an ) ∈ (2 ) を r (ᾱ)

ら遷移関数 ∆ が与える遷移可能な状態 qi+1 に遷移と記す．

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

2. 2 動作仕様
仕様とは，システムがすべきこと（あるいは逆に，に関して qi+1 ∈ ∆(qi , si ) である．ここで，任意のすべきでないこと）を規定するものである．形式的に状態 q ∈ Q と文字 s ∈ Σ について |∆(q, s)| ≤ 1 では，時相論理（temporal logic） [27] [9] や ω-オートマ

あるとき，その遷移関数及びオートマトンは決定的

トン（ω-automaton） [5] [28] [37] [17] などで与えられ（deterministic）であるという．また，σ に対する実る．それらは振舞いを充足するもの（あるいは受理さ行の集合を Run A (σ) で表す．Run A (σ) は複数の要れるもの）とそれ以外に分ける．通常は，充足するも素をもち得るが，A が決定的ならば 1 つ以下の要素の（あるいは受理されるもの）をシステムに望まれるしかもたない．

振舞いとみなされる．本稿では，リアクティブシステ

実行 ρ = q0 · q1 · q2 · · · ∈ Qω 上に無限にしばしば出現する状態の集合を Inf (ρ) とする．

ム仕様を次のように定義する．

Inf (ρ) = {q ∈ Q | ∀i ∈ N : ∃j ∈ N>i : q = qj }. (1)
定義 3 (仕様) 仕様は，システムに望まれる振舞いのω-正規言語オートマトン A は，無限にしばしば出現

集合 S ⊆ (2I∪O )ω である．

する状態の集合 Inf (ρ) に基づいて実行 ρ の特徴を捉■

2. 2. 1 ω-正規オートマトン
安全性や活性，反応性などの形式的検証における主要な検証性質は ω-正規（ω-regular）と呼ばれるクラスに属する．そのため，振舞いの集合よりも抽象度が高く，ω-正規言語を受理できる ω-正規オートマトン（ω-regular automaton）がしばしば仕様として利用される．
定義 4 (ω-オートマトン) ω-オートマトン A は，5
つ組 ⟨Q, Σ, ∆, qinit , Acc⟩ である．ここで，• Q は有限の状態集合，• Σ は有限のアルファベット，• ∆ : Q × Σ → 2Q は，各状態 qi ∈ Q において文字 si ∈ Σ を読んだ際に遷移可能な状態の集合を返す遷移関数，• qinit ∈ Q は初期状態，• Acc は受理条件を規定するための要素である．■
なお，ω-オートマトンをリアクティブシステム仕様として利用する場合，アルファベット Σ は冪集合 2I∪Oである．
オ ー ト マ ト ン A の 実 行 は ，与 え ら れ た 語 σ =え，受理/不受理を判定する．
定義 5 (ω-正規受理条件) Büchi オートマトン [5] の場合，Acc は受理状態集合 F ⊆ Q であり，以下のBüchi 条件を満たす実行 ρ ∈ Run A (σ) が存在する語
σ を受理する．
Inf (ρ) ∩ F ̸= ∅.

(2)

Rabin オートマトン [28] の場合，Acc は受理状態の対の集合 F ⊆ 2Q×Q であり，以下の Rabin 条件を満たす実行 ρ ∈ Run A (σ) が存在する語 σ を受理する．
∨(Inf (ρ) ∩ Ui ̸= ∅ ∧ Inf (ρ) ∩ Vi = ∅). (3)⟨Ui ,Vi ⟩∈F■

Büchi オートマトンのうち，受理状態集合 F が状態集合全体 Q と等しいものを safety オートマトンと呼ぶ．また，受理状態集合 F が任意の文字に対して自己ループする状態，即ち，以下を満たす状態 qf の単集合からなるものを liveness オートマトンと呼ぶ．

∀s ∈ Σ : ∆(qf , s) = {qf }.

(4)

A が受理する語の集合を A の受理言語といい，
L(A) で記す．L(A) が空集合 ∅ であるか否かを判定することを空判定，L(A) が語全体 Σω に等しいか否

かを判定することを全受理判定と呼ぶ．
以下，オートマトンの種別，Büchi/Rabin/safety/

liveness を B/R/S/L で表し，遷移の決定性/非決定性をそれぞれ D/N で表す．つまり，例えば，非決定性 safety オートマトンを NSA，決定性 Rabin オート
マトンを DRA と表記する．
本稿では，仕様 S は S を受理する NBA として与えられている ω-正規言語と仮定する．任意の線形時
相論理（linear temporal logic; LTL） [27] [9] 式はそれを満たす語の集合を受理言語とする指数オーダーサ
イズのオートマトンに変換できる [36] [15] [16] [7] [3] [24]ため，仕様が LTL 式で与えられている場合の判定手
続きは本稿で与える判定手続きにオートマトン変換工程を加えるだけで容易に拡張可能である．

2. 2. 2 ω-ゲーム
リアクティブシステムと環境の相互作用は，2 人無限展開型ゲーム [17] としてモデル化される．1 より，先手プレイヤは環境，後手プレイヤはリアクティブシ
ステムに対応し，交互にイベントを選択することでゲームが進行し，仕様を満たすときに後手プレイヤが勝利する．
定義 6 (ω-ゲーム) ω-ゲーム G は，8 つ組 ⟨Q1 , Q2 , Σ1 ,

Σ2 , ∆1 , ∆2 , qinit , Acc⟩ である．ここで，• Q1 は先手プレイヤが遷移先を決定する有限の状
態集合，• Q2 は後手プレイヤが遷移先を決定する有限の状態集合，• Σ1 は先手プレイヤが選択するイベントの有限のアルファベット，• Σ2 は後手プレイヤが選択するイベントの有限のアルファベット，• ∆1 : Q1 × Σ1 → 2Q2 は，先手プレイヤの各状
態 qi ∈ Q1 においてイベント si ∈ Σ1 が選択された際に遷移可能な状態の集合を返す遷移関数，

ただし，状態集合 Q1 と Q2 並びにアルファベット Σ1と Σ2 はそれぞれ互いに素であり，また，遷移関数∆1 及び ∆2 は共に決定的であるものとする．

■

リアクティブシステムと環境の相互作用をモデル化する場合，先手イベント集合 Σ1 は入力命題の冪集合

2I ，後手イベント集合 Σ2 は出力命題の冪集合 2O である．
オートマトンの実行に相当するゲームのプレイ

Play G (α, β) は，両プレイヤから与えられたイベント
列 α = a0 ·a1 · · · ∈ (Σ1 )ω 及び β = b0 ·b1 · · · ∈ (Σ2 )ω
に対する無限状態列 q⟨0,1⟩ · q⟨0,2⟩ · q⟨1,1⟩ · q⟨1,2⟩ · · · ∈(Q1 · Q2 )ω で与えられる．ただし，Q⟨0,1⟩ = qinit かつすべての i ∈ N に関して q⟨i,2⟩ ∈ ∆1 (q⟨i,1⟩ , ai ) かつ q⟨i+1,1⟩ ∈ ∆2 (q⟨i,2⟩ , bi ) である．
勝利条件 Acc は，簡略化のため，後手プレイヤのための勝利条件とする．これは ω-オートマトンと同様に与えられ，本稿では定義 5 の条件を用いる．プレイが勝利条件を満たすとき後手プレイヤが勝利し，そうでないときには先手プレイヤが勝利する．各時点においてそれぞれのプレイヤがイベントを選択することでプレイが一意に定まり，延いては勝敗が決まる．このイベントの選択法を戦略と呼ぶ．
定義 7 (戦略) イベント決定関数 π1 : Q1 → Σ1 を先
手プレイヤの戦略，π2 : Q2 → Σ2 を後手プレイヤの戦略と呼ぶ．また，先手プレイヤの戦略の集合を Π1 ，後手プレイヤの戦略の集合を Π2 とする．
そ し て ，先 手 プ レ イ ヤ の 戦 略 π1 と 後 手 プ レ イ
ヤ の 戦 略 π2 の 戦 略 が ら 誘 導 さ れ る 次 の プ レ イ

ρ = q⟨0,1⟩ · q⟨0,2⟩ · q⟨1,1⟩ · q⟨1,2⟩ · · · ∈ (Q1 · Q2 )ω を
Play G (π1 , π2 ) とする．
q⟨0,1⟩ = qinit ,(5)∀i ∈ N : q⟨i,2⟩ ∈ ∆1 (q⟨i,1⟩ , π1 (q⟨i,1⟩ )),(6)∀i ∈ N : q⟨i+1,1⟩ ∈ ∆2 (q⟨i,2⟩ , π2 (q⟨i,2⟩ )).

(7)■• ∆2 : Q2 × Σ2 → 2Q1 は，後手プレイヤの各状
態 qi ∈ Q2 においてイベント si ∈ Σ2 が選択さ

勝利条件が ω-正規であるときには，先手プレイヤかれた際に遷移可能な状態の集合を返す遷移関数，

後手プレイヤのどちらか一方は，自身の勝利を確定付• qinit ∈ Q1 は初期状態，

ける無記憶性の勝利戦略を持ち，その存在をアルゴリ• Acc は勝利条件を規定するための要素である．

ズム的に判定することができる [17]．

定義 8 (勝利戦略) 以下を満たす戦略 π1 を先手プレ

定義 9 (充足可能) 仕様 S が充足可能ならば，かつイヤの勝利戦略と呼ぶ．

そのときに限り，∀π ∈ Π2 : Play G (π1 , π) で先手プレイヤが勝利する.
(8)
また，以下を満たす戦略 π2 を後手プレイヤの勝利戦∃α ∈ (2I )ω , β ∈ (2O )ω :[α, β] ∈ S,

(14)

すなわち，S ̸= ∅．

■

略と呼ぶ．

∀π ∈ Π1 : Play G (π, π2 ) で先手プレイヤが勝利する.
(9)■

手続き 1 (充足可能性判定)
入力：仕様 S を受理言語とする NBA A
出力：「充足可能」又は「充足不能」

1. A の空判定を行い，受理言語が非空ならば「充2. 2. 3 基本操作
リアクティブシステムの実現可能性は，オートマト

足可能」，空ならば「充足不能」と判定する．

■

ン/ゲーム上の操作を通して判定できる．もっとも基本的な操作は，決定化とゲーム化である．

定義 10 (実現可能性 [26] [1] [29]) 仕様 S が実現可能

操作 1 (決定化 [30] [20] [10] [21]) NBAA を DRAA′

ならば，かつそのときに限り，∃r ∈ R :■へ変換する操作を決定化と呼ぶ．

∀α ∈ (2I )ω :[α, rω (α)] ∈ S.

操作 2 (ゲーム化) 決定性オートマトン ⟨Q, 2I∪O , ∆,■qinit , Acc⟩ から以下のようなゲーム ⟨Q∪{qnew1 }, Q2 ∪I

O{qnew2 }, 2 , 2 , ∆1 , ∆2 , qinit , Acc⟩ を生成する操作をゲーム化と呼ぶ．ただし，∆′ は以下を満たす最小の遷移関係とする．

与えられた ω-正規な仕様に対する実現可能判定は構成による証明（proof by construction）の形態で決定可能であり，実現可能ならば，それを実現するリ∆(q, a ∪ b) = {q ′ } ⇒アクティブシステムをアルゴリズム的に生成できるq⟨a⟩ ∈ Q2 ∧ q⟨a⟩ ∈ ∆1 (q, a) ∧ q ′ ∈ ∆2 (q⟨a⟩ , b),[26] [22] [31] [13] [8] [14] [4]．仕様を LTL 式で与えている(10)∆(q, a ∪ b) = ∅ ⇒q⟨a⟩ ∈ Q2 ∧ q⟨a⟩ ∈ ∆1 (q, a) ∧ qnew1 ∈ ∆2 (q⟨a⟩ , b),
(11)
I

(15)

∀a ∈ 2 : qnew2 ∈ ∆1 (qnew1 , a),(12)∀b ∈ 2O : qnew1 ∈ ∆1 (qnew2 , b).

(13)場合，実現リアクティブシステムを生成することをLTL 合成（LTL synthesis）と呼ぶ．また，実現不能
ならば，仕様違反を強制する環境（入力列生成戦略）を構成できる．
判定手法にはいくつかのアプローチがあるが，本稿では素朴なゲーム帰着アプローチを紹介する．

■
なお，ゲーム化に関しては，可逆かつ見かけだけの変換であり，実装上は明示的に行う必要はない．

2. 3 実現可能性
リアクティブシステムは，任意の入力列に対して，仕様を満たす出力を各ステップ毎に決定できなければならない．逆に言えば，リアクティブシステム仕様
は，充足可能なだけでなく，実現可能 [26] [1] [29] でなければならない．

手続き 2 (実現可能性判定)
入力：仕様 S を受理言語とする NBA A
出力：「実現可能」又は「実現不能」

1. A を DRA A′ に決定化（操作 1）する．
2. A′ を RG G にゲーム化（操作 2）する．
3. G のリアクティブシステム側（後手）プレイヤの勝利戦略存在判定を行い，勝利戦略 π2 が存在するならば「実現可能」，存在しないならば「実現不能」と判定する．

■

G = ⟨Q1 , Q2 , 2I , 2O , ∆1 , ∆2 , qinit , Acc⟩ の勝利戦
略 π2 に対して，仕様 S を実現するリアクティブシス∃ᾱ ∈ (2I )∗ , β̄ ∈ (2O )|α̂| :∀α̂ ∈ (2I )ω :テム r は以下のように構成できる．

r(a0 · · · an ) = π2 (q⟨n,2⟩ )∃β̂ ∈ (2O )ω :(16)

[ᾱ · α̂, β̄ · β̂] ∈ S.

ただし，

q⟨0,1⟩ = qinit ,(17)∀i ∈ N≤n : q⟨i,2⟩ ∈ ∆1 (q⟨i,1⟩ , ai ),(18)∀i ∈ N≤n−1 : q⟨i+1,1⟩ ∈ ∆2 (q⟨i,2⟩ , π2 (q⟨i,2⟩ )). (19)(22)■

定義 14 (強充足可能性 [25] [43]) 仕様 S が強充足可能ならば，かつそのときに限り，∀α ∈ (2I )ω :2. 4 実現可能性必要条件∃β ∈ (2O )ω :仕様が実現不能であった場合，その欠陥原因を抽出[α, β] ∈ S.

及び分析し，修正しなければならない．森ら [25] [43]■や冨田ら [45] は，仕様の欠陥を分類できるようにいく
つかの実現可能性必要条件（定義 11,14,16-18）を提案した．それらの実現可能性必要条件は，入力接頭語/入力接尾語/出力接頭語/出力接尾語のそれぞれに対する限量の強さ及び順序によって特徴付けられたも

定義 15 (真強充足可能性 [34]) 仕様 S が真強充足可能ならば，かつそのときに限り，∀ᾱ ∈ (2I )∗ :∃β̄ ∈ (2O )|α̂| :のであった．そのため，冨田ら [34] は限量の強さ及び∀α̂ ∈ (2I )ω :順序を限量行列（quantiﬁcation matrix）として表現∃β̂ ∈ (2O )ω :しその組み合わせを網羅することで実現可能性必要[ᾱ · α̂, β̄ · β̂] ∈ S.

条件を細分化 (定義 11-20) 及び階層定理（図 1）を示

的半強充足可能ならば，かつそのときに限り，

定義 16 (保存的充足可能性 [25] [43] [38]) 仕様 S が保存的充足可能ならば，かつそのときに限り，∃r ∈ R :∀ᾱ ∈ (2I )∗ :∀ᾱ ∈ (2I )∗ :∃α̂ ∈ (2I )ω , β ∈ (2O )ω :[ᾱ · α̂, β] ∈ S.

∃α̂ ∈ (2I )ω , β̂ ∈ (2O )ω :(20)

[ᾱ · α̂, r∗ (ᾱ) · β̂] ∈ S.

■
定義 12 (接尾的半強充足可能性 [34]) 仕様 S が接尾
的半強充足可能ならば，かつそのときに限り，(25)■

定義 17 (保存的強充足可能性 [25] [43] [38]) 仕 様 Sが保存的強充足可能ならば，かつそのときに限り，∀α̂ ∈ (2I )ω :∃r ∈ R :∃ᾱ ∈ (2I )∗ , β ∈ (2O )ω :[ᾱ · α̂, β] ∈ S.

(24)
■

した．
定義 11 (接頭的半強充足可能性 [45]) 仕様 S が接頭

(23)

(21)
■

∀ᾱ ∈ (2I )∗ , α̂ ∈ (2I )ω :∃β̂ ∈ (2O )ω :[ᾱ · α̂, r∗ (ᾱ) · β̂] ∈ S.

■

定義 13 (接尾的半真強充足可能性 [34]) 仕様 S が接尾的半真強充足可能ならば，かつそのときに限り，(26)

定義 18 (真保存的充足可能性 [45]) 仕様 S が真保存的充足可能ならば，かつそのときに限り，

• 入力の接頭語/接尾語に対する ∀ 限量は，出力の∃r ∈ R :接頭語/接尾語に対する ∃ 限量に先立つ．

∀ᾱ ∈ (2I )∗ :• 出力の接頭語/接尾語に対する r 限量は，入力の∃α̂ ∈ (2I )ω :[ᾱ · α̂, r (ᾱ · α̂)] ∈ S.
ω

接頭語/接尾語に対する ∀ 限量に先立つ．

(27)

ただし，接尾的半強充足可能性に関しては，接頭構造■と接尾構造の非対称性に基づいた限量順序に従っていない．

定義 19 (安定的充足可能性 [34]) 仕様 S が安定的充3 実現可能性必要条件判定手続き

足可能ならば，かつそのときに限り，∃r ∈ R, ᾱ ∈ (2I )∗ , β̄ ∈ (2O )|ᾱ| :2. 4 節のリアクティブシステム仕様の実現可能性必∀α̂ ∈ (2I )ω :要条件群も，オートマトン/ゲーム上の操作を通して[ᾱ · α̂, β̄ · rω (α̂)] ∈ S.

判定できる．様々な実現可能性必要条件が存在する(28)■
定義 20 (安定的強充足可能性 [34]) 仕様 S が安定的

が，網羅性，戦略化可能性，保存性，安定性の 4 つの特性 [34] を説明するものであるため，いくつかの操作の組み合わせで判定することができる．
本稿では，既知の手続きも含めてその操作の組み強充足可能ならば，かつそのときに限り，合わせとして再整理するとともに，これまで与えら∃n ∈ N :I m∀m ∈ N≥n , ᾱ ∈ (2 )れていない必要条件にも判定手続きを与える．なお，:

接尾的半強充足可能性に関しては，他の実現可能性必O m∃β̄ ∈ (2 ) , r ∈ R :要条件とは異なり，接頭構造と接尾構造の非対称性に∀α̂ ∈ (2I )ω :[ᾱ · α̂, β̄ · rω (α̂)] ∈ S. (29)■
また，実現可能な仕様が持つべきの 4 つの特性を限量行列から説明している．

• 網羅性（exhaustivity）：入力の接頭語及び接尾語が ∀ 限量であること．

• 戦略化可能性（strategizability）：出力の接頭語及び接尾語が r 限量であること• 保存性（preservability）：入力の接頭語が ∀ 限

基づいた限量順序に従っていないため，他の実現可能性必要条件と類似の手続きでは判定できない．

3. 1 操作各項で実現可能性必要条件判定で共通的に現れる
遷移操作，状態操作，受理状態操作についてそれぞれ説明する．

3. 1. 1 遷移操作
強充足可能性等の実現可能性必要条件判定に対しては，遷移操作として，出力命題除去が用いられる．

量，出力の接頭語が r 限量であること• 安定性（stability）：入力の接尾語が ∀ 限量，出力の接尾語が r 限量であること
なお，2. 1 節で述べたリアクティブシステムの特性から，通常は，接頭構造と接尾構造の非対称性，入力と出力の非対称性に基づいた以下の限量順序に従う．

• 入力の接頭語に対する限量は入力の接尾語の限量に先立つ．

• 出力の接頭語に対する限量は出力の接尾語の ∃限量に先立つ．

操作 3 (出力命題除去) オートマトン ⟨Q, 2I∪O , ∆,qinit , Acc⟩ を非決定性オートマトン ⟨Q, 2I , ∆′ , qinit ,Acc⟩ を生成する．ただし，∆′ は以下を満たす最小の遷移関係とする．

q ′ ∈ ∆(q, a ∪ b) ⇒ q ′ ∈ ∆′ (q, a).

(30)■

この操作により，オートマトン上には「入力命題に対して何かしらの応答が可能である」という情報のみ抽出できる．なお，元のオートマトンが出力命題の差異

∃1

∀2
r1
⇕

∃1
∀2
∃1
r1
定義 19

∀1
∀3
∃2
r2
定義 20

⇐

⇓

∀2
r1
定義 10

⇐

⇓

∃1
∀2
∃1
∃3
定義 13

⇐

∀1
∃2
定義 14

⇐

∀1
∀3
∃2
∃4
定義 15

⇓
⇐

∀2
∀3
r1
∃3
定義 17

⇐

∀2
∀3 /∃3r1∃3 /r1
定義 25

⇓
∃2

∀1
∃2
定義 12

⇓

⇓

⇓

⇓
∃1
∃1
定義 9

∀1
⇐

∃2
∃2
定義 11
図1

⇐

∀2
∃3
r1
∃3
定義 16

∀2
⇐

∃3
r1
定義 18

実現可能性必要条件（限量行列表現）の階層によって遷移先が決定的であった場合には，出力命題を除去することでその決定性を失う．そのため，出力行止状態と呼ぶ．

∃a ∈ 2I : ∀b ∈ 2O : ∆(q ′ , a ∪ b) = ∅.

(34)

命題除去後のオートマトンは非決定的であると想定
定義 23 (弱行止状態) 決定性オートマトン ⟨Q, 2I∪O ,できる．

3. 1. 2 状態操作∆, qinit , Acc⟩ において，以下を満たす状態 q ′ ∈ Q を

オートマトン/ゲーム上には，受理/勝利に強い関

弱行止状態と呼ぶ．

• ⟨Q, 2I∪O , ∆, q ′ , Acc⟩ の出力命題除去（操作 3）連を持つ状態あるいは状態群が存在する．

したオートマトンが全受理でない．
定義 21 (有望状態) 決定性オートマトン ⟨Q, 2I∪O ,■∆, qinit , Acc⟩ において，以下の 2 条件を同時に満た

定義 24 (勝利状態) 決定性オートマトン ⟨Q, 2I∪O ,す状態 q ′ ∈ Q を有望状態と呼ぶ．

∆, qinit , Acc⟩ において，以下を満たす状態 q ′ ∈ Q を• q ′ が初期状態 qinit でない場合，qinit から q ′ へ到達可能である．即ち，∪
Ri (qinit ),
q′ ∈

(31)

勝利状態と呼ぶ．

• ⟨Q, 2I∪O , ∆, q ′ , Acc⟩ をゲーム化した場合に後手プレイヤが勝利戦略を持つ．

■i≥0R0 (q) = {q},(32)

Ri+1 (q) = {q ∈ ∆(q ′′ , s) | q ′′ ∈ Ri (q), s ∈ 2I∪O }.
I∪O• ⟨Q, 2(33)
, ∆, q , Acc⟩ の受理言語が空でない．■

保存的充足可能性等の実現可能性必要条件判定に対しては，これらの状態（あるいは状態群）に対して，
次のような操作が用いられる．

′

操作 4 (除去) オートマトン ⟨Q, Σ, ∆, qinit , Acc⟩ と,指定した状態群 Q′ ⊆ Q からオートマトン ⟨Q \ Q′ , Σ,∆, qinit , Acc⟩ において，以下を満たす状態 q ′ ∈ Q を∆′ , qinit , Acc⟩ を生成する．ただし，∆′ は以下を満た

定義 22 (行止状態) 決定性オートマトン ⟨Q, 2

I∪O

す最小の遷移関係とする．
′′

3. 2 振舞性必要条件

′

′

′

∀q, q ∈ Q \ Q : q ∈ ∆(q, s) ⇒ q ∈ ∆ (q, s). (35)

本節では振舞性の実現可能性必要条件群に対する■判定手続きを与える．また，これまで与えられていな
かった接尾的半強充足可能性，接尾的半真強充足可能

操作 5 (縮退) オートマトン ⟨Q, Σ, ∆, qinit , Acc⟩ と性及び真強充足可能性の判定手続きについては，正指定した状態群 Q′ ⊆ Q からオートマトン ⟨(Q \ Q′ ) ∪当性証明も与える．なお，接尾的半強充足可能性判定{qnew }, Σ, ∆′ , qinit , Acc⟩ を生成する．ただし，∆′ は手続きのみ 3. 1 節の操作以外のオートマトン操作も以下を満たす最小の遷移関係とする．

行う．

∀q, q ′ ∈ Q \ Q′ , s ∈ Σ :q ′ ∈ ∆(q, s) ⇒ q ′ ∈ ∆′ (q, s),
′

(36)

′

∀q ∈ Q, q ∈ Q , s ∈ Σ :′手続き 3 (接頭的半強充足可能性判定 [45])入力：仕様 S を受理言語とする NBA A′q ∈ ∆(q, s) ⇒ qnew ∈ ∆ (q, s),′∀s ∈ Σ : qnew ∈ ∆ (qnew , s).
また，qnew を縮退状態と呼ぶ．

(37)

出力：
「接頭的半強充足可能」又は「接頭的半強充足

(38)

不能」

■

これらの操作は状態集合を変更するものであるため，一般的には間接的に受理条件要素 Acc も変更される．
しかし，実現可能性必要条件判定においては，これらの状態操作の際には後述の受理条件操作が続けて行われることになる．そのため，状態操作に伴う受理条
件要素 Acc の変更はここでは省略する．

1. A の非有望状態を除去（操作 4）し，
2. NSA A′ に safety 化（操作 6）する．
3. さらに出力命題を除去（操作 3）して NSA A′′に変換する．

4. A′ の全受理判定を行い，全受理ならば「接頭的半強充足可能」，全受理でないならば「接頭的半強充足不能」と判定する．

3. 1. 3 受理条件操作

手続き 4 (接尾的半強充足可能性判定)

保存的充足可能性等の実現可能性必要条件判定に

入力：仕様 S を受理言語とする NBA A■

対しては，受理条件操作として，次のような操作が用

出力：「接尾的半強充足可能」又は「接尾的半強充足

いられる．

不能」

操作 6 (Safety 化) オ ー ト マ ト ン ⟨Q, Σ, ∆, qinit ,Acc⟩ を Safety オートマトン ⟨Q, Σ, ∆, qinit , Q⟩ を生成する．

■

操作 7 (Liveness 化) オートマトン ⟨Q, Σ, ∆, qinit ,Acc⟩ と指定した縮退状態 qf ⊆ Q から liveness オー
トマトン ⟨Q, Σ, ∆, qinit , {qf }⟩ を生成する．

■

なお，liveness 化は前述の状態縮退（操作 5）の際に追加した縮退状態 qnew が指定縮退状態 qf であることを前提とする．
これら操作により，前述の受理/勝利に強い関連を持つ状態群（あるいはそれ以外の状態群）への到達性や保持性に焦点を当てたオートマトンを得ることができる．

1. A を DRA A′ に決定化（操作 3）する．
2. A′ の非有望状態を除去（操作 4）し，
3. 出 力 命 題 も 除 去（ 操 作 3）し た NRA A′′ =⟨Q, Σ, ∆, qinit , F⟩ に変換する．
4. さ ら に A′′ を 以 下 を 満 た す NRA A′′′ =′⟨Q′ , Σ, ∆′ , qinit, F ′ ⟩ に変換する．
′• Q′ = {q⟨qi ,qj ⟩ | qi , qj ∈ Q} ∪ {qinit},• 任意の元状態 qi , qj , qk ∈ Q と文字 s ∈ Σ について，– q⟨qi ,qj ⟩ ∈ ∆′ (q⟨qi ,qk ⟩ , s) ⇔ qj ∈∆(qk , s),′– q⟨qi ,qj ⟩ ∈ ∆′ (qinit, s) ⇔ qj ∈ ∆(qi , s)

• 任 意 の Rabin 対 ⟨U, V ⟩ ∈ F に つ い て ，⟨U ′ , V ′ ⟩ ∈ F ′ ⇔ ⟨U, V ⟩ ∈ F ．ただし，– qj ∈ U ⇔ ∀qi ∈ Q : q⟨qi ,qj ⟩ ∈ U ′5. A′′′ の全受理判定を行い，全受理ならば「接尾的半強充足可能」，全受理でないならば「接尾的半強充足不能」と判定する．

■

′′′

′′′

証明 1 (手続き 4 の正当性) Aの構成法から，A′の初期状態 qinit
は A′′ の全状態を模倣する．A′ が決定的であるため，A′′′ が全受理でないならば，かつそのときに限り，その不受理語 α̂ ∈ 2I は，接尾的半強充足可能性の反例となる．すなわち，任意の入力接頭語 ᾱ ∈ (2I )∗ と出力語 β ∈ (2O )ω に対して，[ᾱ · α̂, β]
は仕様 S に含まれない．

□

入力：仕様 S を受理言語とする NBA A
出力：「接尾的半真強充足可能」又は「接尾的半真強充足不能」

1. A を DRA A′ に決定化（操作 3）する．
2. A′ の非弱行止状態を縮退（操作 5）し，
3. その縮退状態を受理状態とする DLA A′′ に
liveness 化（操作 7）する．
4. さらに出力命題を除去（操作 3）した NLA A′′′に変換する．

5. A′′′ の全受理判定を行い，全受理ならば「真強充足可能」，全受理でないならば「真強充足不能」■

証明 3 (手続き 7 の正当性) A′′′ が全受理ならば，かつそのときに限り，任意の有限長入力接頭語 ᾱ ∈ (2I )∗この有限長接頭語 [ᾱ, β̄] によって A′ の非弱行止状態

2. A′ の非弱行止状態を縮退（操作 5）し，
3. その縮退状態を受理状態とする DLA A′′ に
liveness 化（操作 7）する．
4. A′′ の空判定を行い，受理言語が非空ならば「接尾的半真強充足可能」，空ならば「接尾的半真強■

証明 2 (手続き 5 の正当性) A′′ の受理言語が非空ならば，かつそのときに限り，受理状態となっている
縮退状態へ到達させる有限長接頭語 [ᾱ, β̄] ∈ (2I∪O )∗が存在する．[ᾱ, β̄] によって A′ 上ではある非弱行止状態へ到達しているため，それに続く無限長接尾語として，任意の無限長入力接尾語 α̂ ∈ (2I )ω に対して
無限長出力接尾語 β̂ ∈ (2O )ω が存在し，[ᾱ · α̂, β̄ · β̂]□へ到達する．到達した状態が非弱行止状態であるため，それに続く無限長接尾語として，任意の無限長
入力接尾語 α̂ に対する無限長出力接尾語 β̂ が存在し，[ᾱ · α̂, β̄ · β̂] は A′ に受理される，即ち仕様 S に含まれる．

□

手続き 5 における空判定は，対象オートマトンがDLA であるため，実際には受理状態への単純な到達判定である．また，手続き 6 は，初期状態の弱い行止り判定と同値である．
手続き 5 及び手続き 7 においては有限長語が接頭語として与えられた時点で弱い行止りかどうかを確定することができるように決定化が必須である．

3. 3 保存性必要条件
本節では保存性の実現可能性必要条件群に対する手続き 6 (強充足可能性判定 [25] [43])判定手続きを与える．

入力：仕様 S を受理言語とする NBA A
出力：「強充足可能」又は「強充足不能」

1. A の出力命題を除去（操作 3）した NBA A′ に変換する．

2. A′ の全受理判定を行い，全受理ならば「強充足可能」，全受理でないならば「強充足不能」と判
定する．

出力：
「真強充足可能」又は「真強充足不能」

に対してある有限長出力接頭語 β̄ ∈ (2O )∗ が存在し，

1. A を DRA A′ に決定化（操作 3）する．

は A′ に受理される，即ち仕様 S に含まれる．

入力：仕様 S を受理言語とする NBA Aと判定する．

手続き 5 (接尾的半真強充足可能性判定)

充足不能」と判定する．

手続き 7 (真強充足可能性判定)■

手続き 8 (素朴な保存的充足可能性判定)
入力：仕様 S を受理言語とする NBA A
出力：「保存的充足可能」又は「保存的充足不能」

1. A を DRA A′ に決定化（操作 3）する．
2. A′ の非有望状態を除去（操作 4）し，
3. DSA A′′ に safety 化（操作 6）する．

4. さらにそれを SG G にゲーム化（操作 2）する．

手続き 9 と手続き 11 の差異は，除去される状態の

5. G のリアクティブシステム側（後手）プレイヤ

範囲である．手続き 9 では非有望状態を 1 度しか除の勝利戦略存在判定を行い，勝利戦略が存在す

去しないため，行止状態除去後に新たに発生する非有るならば「保存的充足可能」，存在しないならば望状態が A′′ に残存している可能性がある．一方で，■手続き 11 では，行止状態除去後に新たに発生する非「保存的充足不能」と判定する．

有望状態も除去される．
手続き 9 (保存的充足可能性判定 [25] [43] [38])入力：仕様 S を受理言語とする NBA A

3. 4 安定性必要条件

出力：「保存的充足可能」又は「保存的充足不能」

本節では安定性の実現可能性必要条件群に対する

1. A を DRA A′ に決定化（操作 3）する．

判定手続き及び正当性証明を与える．

2. A′ の非有望状態を除去（操作 4）し，
3. さらに行止状態を繰り返し除去（操作 4 を反復）した DRA A に変換する．

4. A′′ に初期状態が残っているならば「保存的充足可能」，残っていないならば「保存的充足不能」と判定する．

手続き 12 (安定的充足可能性判定)
入力：仕様 S を受理言語とする NBA A

′′

■

出力：
「安定的充足可能」又は「安定的充足不能」

1. A を DRA A′ に決定化（操作 3）する．
2. A′ の勝利状態を縮退（操作 5）し，
3. その縮退状態を受理状態とする DLA A′′ に

手続き 10 (保存的強充足可能性判定 [25] [43] [38])liveness 化（操作 7）する．

入力：仕様 S を受理言語とする NBA A

4. A′′ の空判定を行い，受理言語が非空ならば「安出力：「保存的強充足可能」又は「保存的強充足不能」

1. A を DRA A′ に決定化（操作 3）する．

定的充足可能」，空ならば「安定的充足不能」と判定する．

2. A′ の非有望状態を除去（操作 4）し，
3. さらに弱行止状態を除去（操作 4）した DRA■

証明 4 (手続き 12 の正当性) A′′ の受理言語が非空ならば，かつそのときに限り，勝利状態となっている

A′′ に変換する．
4. A′′ に初期状態が残っているならば「保存的強縮退状態へ到達させる有限長接頭語 [ᾱ, β̄] ∈ (2I∪O )∗充足可能」，残っていないならば「保存的強充足が存在する．[ᾱ, β̄] によって A′ 上ではある勝利状態■へ到達しているため，それに続く任意の無限長入力接不能」と判定する．

尾語 α̂ ∈ (2I )ω に適切に応答するリアクティブシス

手続き 11 (真保存的充足可能性判定 [45])テム r ∈ R が存在し，[ᾱ · α̂, β̄ · rω (α̂)] は A′ に受理

入力：仕様 S を受理言語とする NBA A

される，即ち仕様 S に含まれる．

□

出力：「真保存的充足可能」又は「真保存的充足不能」
手続き 13 (安定的強充足可能性判定)

1. A を DRA A′ に決定化（操作 3）する．
2. A′ の非有望状態と行止状態を繰り返し除去（操出力：「安定的真強充足可能」又は「安定的真強充足

作 4 を反復）した DRA A′′ に変換する．

3. A′′ に初期状態が残っているならば「真保存的充足可能」，残っていないならば「真保存的充足不能」と判定する．

■

手続き 9 で行われる非有望状態と行止状態を除去は，
手続き 8 で構成されるゲームの非勝利状態の除去に相当する．

入力：仕様 S を受理言語とする NBA A
不能」

1. A を DRA A′ に決定化（操作 3）する．
2. A′ の勝利状態を縮退（操作 5）し，
3. その縮退状態を受理状態とする DLA A′′ に
liveness 化（操作 7）する．
4. さらに出力命題を除去（操作 3）した NLA A′′′に変換する．

5. A′′′ の全受理判定を行い，全受理ならば「安定保存的強充足可能性では，入力接尾語に網羅的応答で的真強充足可能」，全受理でないならば「安定的きる可能性を維持しつつ，都合が良い入力接尾語に対■しては仕様を満たす応答が可能なことを保証できる．

真強充足不能」と判定する．

判定手続きは，手続き 9 を手続き 11 に拡張するの
証明 5 (手続き 13 の正当性) A′′′ が全受理ならば，ことと同様のアプローチで，手続き 10 を拡張するこ

かつそのときに限り，充分に長い任意の有限長入力とで得ることができる．

接頭語 ᾱ ∈ (2I )∗ に対してある有限長出力接頭語β̄ ∈ (2O )∗ が存在し，この有限長接頭語 [ᾱ, β̄] によっ

手続き 14 (真保存的強充足可能性判定)て A′ の勝利状態へ到達する．到達した状態が勝利状

入力：仕様 S を受理言語とする NBA A態であるため，それに続く任意の無限長入力接尾語

出力：「真保存的強充足可能」又は「真保存的強充足I ωα̂ ∈ (2 ) に適切に応答するリアクティブシステム′r ∈ R が存在し，[ᾱ · α̂, β̄ · r (α̂)] は A に受理され
ωる，即ち仕様 S に含まれる．

□

不能」

1. A を DRA A′ に決定化（操作 3）する．
2. A′ の非有望状態と弱行止状態を繰り返し除去（操作 4 を反復）した DRA A′′ に変換する．

3. A′′ に初期状態が残っているならば「真保存的4 真保存的強充足可能性
保存性必要条件群の判定手続き 9-11 の対称性から，これまで知られていた保存性必要条件群より強い実現可能性必要条件が示唆される．

強充足可能」，残っていないならば「真保存的強充足不能」と判定する．

■

証明 6 (手続き 14 の正当性) A′′ に初期状態が残っ

この必要条件は，限量行列として単純に表現できているならば，かつその時に限り，A′′ は弱い行止りるものではないが，以下のように定義することがででないかつ有望な状態のみから構成されている．このきる．

とき，真保存的充足可能性の根拠となるリアクティブ

定義 25 (真保存的強充足可能性) 仕様 S が真保存的強充足可能ならば，かつそのときに限り，∃r ∈ R :システム構成法 [45] と同じ方法で真保存的強充足不能の根拠となるリアクティブシステムが構成できる．□
なお，接頭構造と接尾構造の非対称性により，この∀ᾱ ∈ (2I )∗ :ような限量の混合による実現可能性必要条件の詳細((∃α̂ ∈ (2I )ω :化は，安定的必要条件群には適用できない．

⟨ᾱ · α̂, r (ᾱ · α̂)⟩ ∈ S)ω

5 考察∧(∀α̂ ∈ (2I )ω :∀β̂ ∈ (2O )ω :⟨ᾱ · α̂, rω (ᾱ) · β⟩ ∈ S)).

5. 1 計算量上界(39)■

真保存的充足可能性では，根拠となるリアクティブシ
ステムは都合が良い入力接尾語に対してのみ仕様を満たす応答が可能なことを保証しているに過ぎない．
一方で，保存的充足可能性では，根拠となるリアク
ティブシステムは入力接尾語に網羅的応答できる可能性のみを維持しているに過ぎず，どのような入力語を与えても仕様を満たす応答できない可能性がある．真

本節では，各実現可能性必要条件判定手続きの計算
量上界について述べる．

NBA の空判定及び全受理判定は，オートマトンのサイズに対してそれぞれ NLOGSPACE 完全及びPSPACE 完全である [37]．また，NBA の決定化は，
オートマトンのサイズに対して EXPTIME であり，構成される DRA は指数オーダーのサイズを持つ [37]．

RA から NBA への変換は，オートマトンのサイズに対して PTIME であり，構成される NRA は多項式オーダーのサイズを持つ [37]．そして，行止状態群と勝利状態群はオートマトンのサイズに対して多項式実現可能性判定の計算量は NBA 仕様に対しては EXPTIME 完全，LTL 式仕様に対しては 2EXP-時間で求めることができる [17]．

TIME 完全である [26] [29]．実現可能性判定より簡単

そのため，以下の定理が成り立つ．

な（あるいは同等の）計算量クラスとなるのは，接頭定理 1 (実現可能性必要条件判定の計算量上界) リア

的半強充足可能性判定と強充足可能性判定しかなく，

クティブシステム仕様が NBA として与えられている

5 つの実現可能性必要条件に至っては実現可能性判定

とき，各実現可能性必要条件判定の計算量クラスは以よりも難しい（あるいは同等の）計算量クラスに属

下の通りである．

する．

• PSPACE：接頭的半強充足可能性判定，強充足可能性判定．

そのため，実現可能性必要条件判定は，高速に実現不能性を確認する手段としては有効とは言い難い．

• EXPTIME：安定的充足可能性判定，真保存的

しかし，多くの手続きに共通操作があることから，実強充足可能性判定，真保存的充足可能性判定．

現可能性必要条件判定を並行して実施することで，時• EXPSPACE：接尾的半強充足可能性判定，接尾間的に効率的な欠陥分類可能ではある．ただし，どの的半真強充足可能性判定，真強充足可能性判定，

実現可能性必要条件判定も空間計算量が大きいため，保存的強充足可能性判定，真保存的強充足可能性

実行可能性は高いとは言えない．

判定，安定的強充足可能性判定．

実現可能性判定や自動合成技術を広く利用できる

また，リアクティブシステム仕様が LTL 式として与ようにするためには，実現可能性及びその必要条件

えられているとき，各実現可能性必要条件判定の計算（あるいは充分条件）の判定を効率的に行うことが可量クラスは以下の通りである．

能であり，かつ，充分な表現力を持った形式仕様記述• EXPSPACE：接頭的半強充足可能性判定，強充体系が必要であろう．

足可能性判定．

• 2EXPTIME：安定的充足可能性判定，真保存的5. 2 接尾的半強充足可能性判定

強充足可能性判定，真保存的充足可能性判定．

接尾的半強充足可能性は他の実現可能性必要条件• 2EXPSPACE：接尾的半強充足可能性判定，接とは異なり，接頭構造と接尾構造の非対称性に基づい

尾的半真強充足可能性判定，真強充足可能性判

た限量順序に従っていない．この特徴により，他の実定，保存的強充足可能性判定，真保存的強充足可

現可能性必要条件と類似の手続きでは判定できない．

能性判定，安定的強充足可能性判定．

一方で，接尾的半強充足可能性は，接頭的強充足可
能性や強充足可能と同様に，これを満たさない仕様が証明 7 (定理 1 の証明) （1）リアクティブシステム
仕様が NBA のとき：手続き中に弱行止状態を求める
必要がない場合は，手続きの構成から明らか．手続き中に弱行止状態群を求める必要がある場合，まずオー
トマトンの決定化が先立つ．そしてオートマトンのサイズに対して高々多項式オーダーだけ全受理判定（PSPACE 完全）を繰り返す．そのため，そのような手続きの計算量は EXPSPACE に属す．
（2）リアクティブシステム仕様が LTL 式のとき：

LTL 式からオートマトンへの変換の計算量及び構成される NBA の状態数，リアクティブシステム仕様がNBA のときの計算量から明らか．

□

持つ特徴を直感的な説明が可能であり，仕様が持つ欠陥を明確に指摘できる．

• 接尾的半強充足可能性の反例：（すべての接頭語
及び出力接尾語に有効な）強い悪性接尾入力語の存在• 接頭的強充足可能性の反例：（すべての接尾語及び出力接頭語に有効な）悪性接頭入力語の存在• 強充足可能性の反例：（すべての出力語に有効な）
悪性入力語の存在
これは safety property [2] [23] の反例が，悪性接頭語（bad preﬁx）であることに似ている．それに対し，接尾的半真強充足可能性は，前述の 3 つの必要条件とは異なり，これを満たさない仕様が持つ特徴は相対的は非常に煩雑で効率化が困難なため，実現可能性判に説明しづらく，仕様が持つ欠陥を理解しづらい．

定/自動合成では Safraless な漸進的有界合成手続き[22] [31] [13] がいくつも提案されており，Unbeast†5 [8]，• 接尾的半真強充足可能性の反例：（各接頭語に対して個別に有効な）弱い悪性接尾入力語群の存在

Acacia+†6 [4]， [42] などの合成器が開発された．これ

そのため，接尾的半強充足可能性は，接頭構造/接らの合成器では，仕様を下方近似した safety property

尾構造の非対称性及び入力/出力の非対称性に基づいを漸進的に元の仕様に近づけでリアクティブシステム

た限量順序に従わないものの，リアクティブシステム

を合成する．なお，これらの漸進的有界近似手法群は仕様の欠陥分類に有用であると考えられる．

仕様の実現可能性に関して保守的である．本稿では，実現可能性そのものではなくその必要条件を取り扱っ

6 関連研究ているが，そのような保守的な漸進的近似に基づく判

6. 1 仕様分析

定は提案しておらず，改善の余地があると言える．

時間論理等で与えられる動作仕様の分析方法とまた，ゲームベースの実現可能性判定及び合成のしては，安全性-活性分解 [2] [23]（safety-liveness de-composition）が代表的である．仕様を安全性（safety

手法とは異なり，SAT/SMT 等の制約ソルバーを利用した合成器として BoSy†7 [12] [11] も開発されていproperty）と活性（liveness property）に分解するこる．本稿で与えた実現可能性必要条件判定も制約ソルとで，仕様の特性を分析できるようにするだけでなく，バーを利活用することで効率的に判定できる可能性

オートマトンへの変換や合成等をし易くであきる．

がある．

リアクティブシステム仕様のための仕様分析法としLTL 合成の場合には，まず LTL 式をオートマトンては，まず森ら [25] [43] [38] が保存的充足可能性，強充足可能性，保存的強充足可能性の 3 つの実現可能に変換する必要がある [36] [15] [16] [7] [3] [24]．変換ツー
ルとしては，SPOT†8 [7]，LTL3BA†9 [3]，Trans†10

性必要条件に基づいた分析を提案している．これら[24] などが開発されている．SPOT や LTL3BA では，の実現可能性必要条件判定の効率化については，安オートマトンをよりコンパクトに構成できることが藤ら [40] の分散計算による効率的な安定充足可能性判見込める遷移ベース受理条件をサポートしている．た定手続きや，島川ら [32] [33] は，SAT ベースの有界強だし，そのような仕組みをもっていたとしても必ず充足可能性判定手続きがある．また，萩原ら [44] [18]

しも小さいオートマトンを構成できるとは限らない．

は，仕様の欠陥箇所を特定する手法として，強充足不本稿で与えた判定手続き群で操作するオートマトン

能の原因となる最小な部分仕様抽出する手法を提案

は状態ベース受理条件であるが，遷移ベース受理条件

している．

にも容易に拡張できる．

一方で，本稿では，より広範な実現可能性必要条件
群に対して系統的な判定手続きを与えた．

6. 3 不完全合成
実現可能性必要条件のうち，保存性必要条件及び保6. 2 リアクティブシステム合成

存性必要条件はある種の不完全リアクティブシステム

素朴な実現可能性判定手続き（手続き 2）では，ス
テップ 1 において，LTL2dstar†3 [20] で実装されている Safra の構成法 [30] や，Rabinizer3†4 で実装されている Esparza-Křetı́nský 法 [10] などを用いた ω-正規オートマトンの決定化が必要である．これらの手法†3 https://www.ltl2dstar.de†4 https://www7.in.tum.de/~kretinsk/
rabinizer3.html†5 https://www.react.uni-saarland.de/tools/
unbeast/†6 http://lit2.ulb.ac.be/acaciaplus/†7 https://www.react.uni-saarland.de/tools/bosy/†8 https://spot.lrde.epita.fr†9 https://sourceforge.net/projects/ltl3ba/†10 https://sites.google.com/site/yonezakilab/
tools

の存在を保証するものである．吉浦ら [39] は保存的充

参 考 文 献足可能性，冨田ら [45] は真保存的充足可能性に基づく[ 1 ] Abadi, M., Lamport, L., and Wolper, P.: Realizable and Unrealizable Speciﬁcations 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 ] Alpern, B. and Schneider, F. B.: Recognizing
safety and liveness, Distributed Computing, Vol. 2,
No. 3(1987), pp. 117–126.
[ 3 ] 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.
[ 4 ] Bohy, A., Bruyére, V., Filiot, E., Jin, N., andRaskin, J.-F.: Acacia+, a Tool for LTL Synthesis,
Computer Aided Veriﬁcation, Madhusudan, P. andSeshia, S.(eds.), Lecture Notes in Computer Science, Vol. 7358, Springer Berlin Heidelberg, 2012,
pp. 652–657.
[ 5 ] Büchi, J. R.: Weak Second-Order Arithmetic
and Finite Automata, Mathematical Logic Quarterly, Vol. 6, No. 1-6(1960), pp. 66–92.
[ 6 ] 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.
[ 7 ] 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.
[ 8 ] Ehlers, R.:
Symbolic Bounded Synthesis,
Formal Methods in System Design, Vol. 40,
No. 2(2012), pp. 232–262.
[ 9 ] Emerson, E. A.: Temporal and Modal Logic,
Handbook of Theoretical Computer Science, Vol. B,
Elsevier, 1995, pp. 995–1072.
[10] Esparza, J. and Křetı́nský, J.: From LTL to Deterministic Automata: A Safraless Compositional
Approach, Computer Aided Veriﬁcation, Biere, A.
and Bloem, R.(eds.), Lecture Notes in Computer
Science, Vol. 8559, Springer International Publishing, 2014, pp. 192–208.
[11] Faymonville, P., Finkbeiner, B., Rabe, M. N.,
and Tentrup, L.: Encodings of Bounded Synthesis, Tools and Algorithms for the Construction
and Analysis of Systems, Legay, A. and Margaria,
T.(eds.), Springer Berlin Heidelberg, 2017, pp. 354–

不完全リアクティブシステム合成手法を与えている．
本稿で新たに導入した真保存的強充足可能性について
は，それに基づく不完全リアクティブシステム合成手法を [45] の手法を利用して行うことができる．また，Damm ら [6] は，強充足可能性の反例となる悪性入力列を許容するような不完全リアクティブシステム合成法を提案している．さらに [45] では，接頭的半強充足可能の反例となる悪性接頭入力列を許容するような不完全リアクティブシステム合成法等も提案している．
そして，平均利得に基づいて不完全な中でも最適な
リアクティブシステムを合成する手法群 [46] [41] [19] [35]も提案されている．これらの手法群では，振舞い群を平均利得によって定量的に優先度付けることで，実現不能な中でも許容されるより望ましい振舞い群を抽象的に特徴付け，リアクティブシステム合成を行う．

7 おわりに本稿では，仕様欠陥分析を実施可能にするために，実現可能性必要条件群に対する判定手続き群をいく
つかの共通的操作の組合せとして与えた．また，共通的操作の組み合わせとして再整理した結果として発見された手続き間の対称性を基に，新しい実現可能性
必要条件である真保存的強充足可能性及びその判定
手続きを与えた．そして判定問題に対する計算量上界を示した．
リアクティブシステム仕様の欠陥分析に効果的に行
うには，示唆性に富んだ検証を効率的に実施可能である必要がある．しかしながら，実現可能性自体が判定困難であるため，詳細な仕様欠陥分析には困難な必要条件（あるいは充分条件）判定が要求されてしまう．不完全合成手法群はそうした困難な問題をある程度隠蔽して「不完全であってもより望ましい」リアク
ティブシステムを試みるが，望ましさを追求するほど計算困難になってしまう．実現可能性判定や自動合成技術を広く利用できるようにするためには，検証/合成の効率性と仕様記述言語の充分な表現力を両立させることが可能な技術的打開策が必要であろう．

370.
[12] Faymonville, P., Finkbeiner, B., and Tentrup,
L.: BoSy: An Experimentation Framework for
Bounded Synthesis, Computer Aided Veriﬁcation,
Majumdar, R. and Kunčak, V.(eds.), Springer International Publishing, 2017, pp. 325–332.
[13] Filiot, E., Jin, N., and Raskin, J.-F.: An
Antichain Algorithm for LTL Realizability, Computer Aided Veriﬁcation, Bouajjani, A. and Maler,O.(eds.), Lecture Notes in Computer Science,Vol. 5643, Springer Berlin Heidelberg, 2009,
pp. 263–277.
[14] Finkbeiner, B. and Schewe, S.: Bounded synthesis, International Journal on Software Tools forTechnology Transfer, Vol. 15, No. 5(2012), pp. 519–
539.
[15] Gastin, P. and Oddoux, D.: Fast LTL to BüchiAutomata Translation, Computer Aided Veriﬁcation, Berry, G., Comon, H., and Finkel, A.(eds.),
Lecture Notes in Computer Science, Vol. 2102,
Springer Berlin Heidelberg, 2001, pp. 53–65.
[16] Giannakopoulou, D. and Lerda, F.: From States
to Transitions: Improving Translation of LTL Formulae to Büchi Automata, Formal Techniques for
Networked and Distributed Systems – FORTE 2002,
Peled, D. and Vardi, M.(eds.), Lecture Notes in
Computer Science, Vol. 2529, Springer Berlin Heidelberg, 2002, pp. 308–326.
[17] Grädel, E., Thomas, W., and Wilke, T.(eds.):
Automata Logics, and Inﬁnite Games, Lecture
Notes in Computer Science, Vol. 2500, Springer
Berlin Heidelberg, 2002.
[18] Hagihara, S., Egawa, N., Shimakawa, M., andYonezaki, N.: Minimal Strongly Unsatisﬁable Subsets of Reactive System Speciﬁcations, Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE ’14,
ACM, 2014, pp. 629–634.
[19] Hagihara, S., Ueno, A., Tomita, T., Shimakawa,M., and Yonezaki, N.: Simple Synthesis of Reactive Systems with Tolerance for Unexpected Environmental Behavior, Proceedings of the 4th FME
Workshop on Formal Methods in Software Engineering, FormaliSE ’16, ACM, 2016, pp. 15–21.
[20] 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.
[21] Komárková, Z. and Křetı́nský, J.: Rabinizer 3:
Safraless Translation of LTL to Small Deterministic
Automata, Automated Technology for Veriﬁcation
and Analysis, Cassez, F. and Raskin, J.-F.(eds.),
Lecture Notes in Computer Science, Vol. 8837,
Springer International Publishing, 2014, pp. 235–
241.
[22] Kupferman, O. and Vardi, M.: Safraless decision procedures, Foundations of Computer Science,
2005. FOCS 2005. 46th Annual IEEE Symposium

on, 2005, pp. 531–540.
[23] Maretić, G. P.: LTL is closed under topologicalclosure, Information Processing Letters, Vol. 114,
No. 8(2014), pp. 408–413.
[24] 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.
[25] 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 Artiﬁcial Intelligence and Applications,Vol. 16, IOS Press, 1993, pp. 407–424.
[26] 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.
[27] Pnueli, A.: The Temporal Logic of Programs,
Foundations of Computer Science, 1977., 18th Annual Symposium on, 1977, pp. 46–57.
[28] Rabin, M. O.: Decidability of second-order theories and automata on inﬁnite trees, Bull. Amer.
Math. Soc., Vol. 74, No. 5(1968), pp. 1025–1029.
[29] Rosner, R.: Modular Synthesis of Reactive Systems, PhD Thesis, Weizmann Institute of Science,
1992.
[30] 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.
[31] Schewe, S. and Finkbeiner, B.: Bounded Synthesis, Automated Technology for Veriﬁcation 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.
[32] Shimakawa, M., Hagihara, S., and Yonezaki, N.:
SAT-Based Bounded Strong Satisﬁability Checkingof Reactive System Speciﬁcations, 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.
[33] Shimakawa, M., Hagihara, S., and Yonezaki, N.:
Complexity of Checking Strong Satisﬁability of Reactive System Speciﬁcations, 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.
[34] Tomita, T., Hagihara, S., Shimakawa, M., andYonezaki, N.: A characterization on necessary con-ditions of realizability for reactive system speciﬁcations, Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2018),
ya Nishizaki, S., Numao, M., Caro, J., and Suarez,
M. T.(eds.), 2019, pp. 33–42.
[35] Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., and Yonezaki, N.: Safraless LTL synthesis
considering maximal realizability, Acta Informatica,
Vol. 54, No. 7(2017), pp. 655–692.
[36] Vardi, M. Y. and Wolper, P.: Reasoning about
Inﬁnite Computations, Information and Computation, Vol. 115(1994), pp. 1–37.
[37] Vardi, M.: An Automata-Theoretic Approach
to Linear Temporal Logic, Logics for Concurrency,
Moller, F. and Birtwistle, G.(eds.), Lecture Notes in
Computer Science, Vol. 1043, Springer Berlin Heidelberg, 1996, pp. 238–266.
[38] Yoshiura, N.: Decision Procedures for Several
Properties of Reactive System Speciﬁcations, 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.
[39] Yoshiura, N. and Yonezaki, N.: Program synthesis for stepwise satisﬁable speciﬁcation of reactive system, Principles of Software Evolution, 2000.
Proceedings. International Symposium on, 2000,
pp. 58–67.

[40] 安藤崇央, 宮本佑樹, 萩原茂樹, 米崎直樹: リアクティ
ブシステム仕様に対する段階的充足可能性判定器の分散オブジェクト技術を利用した実装, コンピュータ ソフト
ウェア, Vol. 28, No. 4(2011), pp. 262–281.
[41] 上野篤史, 冨田尭, 島川昌也, 萩原茂樹, 米崎直樹:
環境許容性のあるリアクティブシステム合成法, 電子
情報通信学会技術研究報告, Vol. 114, No. 510(2015),
pp. 7–12.
[42] 上野篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹:
LTL 式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装に関する研究, 日本ソフト
ウェア科学会第 30 回大会論文集, 2013.
[43] 森亮靖, 友石正彦, 米崎直樹: 時相論理によるリア
クティブシステム仕様の実現可能性に関する分類, コン
ピュータ ソフトウェア, Vol. 15, No. 3(1998), pp. 213–
225.
[44] 萩原茂樹, 江川直毅, 島川昌也, 米崎直樹: 強充足不能なリアクティブシステム仕様における欠陥範囲の特定, ソフトウェア工学の基礎 XX, 日本ソフトウェア科
学会 FOSE 2013, 2013, pp. 143–152.
[45] 冨田尭: 実現可能性の必要条件に基づいた不完全リ
アクティブシステム合成, 日本ソフトウェア科学会第 32
回大会論文集, 2015.
[46] 冨田尭, 山崎徹郎, 萩原茂樹, 米崎直樹: 確率的環境下において平均利得時間論理仕様を実現する最適マル
コフ決定過程の自動合成法, 日本ソフトウェア科学会第30 回大会論文集, 2013.