数理解析研究所講究録902 巻 1995 年 145-155

145

時相論理によるプログラム生成は実用的か?
河野真治 (Shinji Kono)-mail: kon’o@csl.sony.co.jp
Sony Computer Science Laboratory Inc.
3-14-13, Higashi-gotanda, Shinagawa-ku, Tokyo 141, Japan$\mathrm{e}$September 28, 1994

1

時相論理を使って GUI を設計してみる

X-Window や Windows などの GUI を使った Application は、 Button, Menu, Entry などの User が入力する Event と、 User に対して表示をおこなう Tools Kit からなる。 Tool kit が状態を持たなけ
れば、 Event ごとに関数を定義すれば、全体は状態を持たない関数型プログラミング構造となる。
このような場合はプログラミングは容易である。例えば; メニューからファイルを選んで見る (変更しない) ような場合に相当する。
しかし、実際には Toolkit の状態に依存した Programming が必要である。
Print 中には Cancel Button だけが有効という簡単かつ良くある例でも Print 中かどうかという状態に依存する。 Interface Builder などによって、 このような状態に依存するような処理を合成することは今はできない。

実は、 このような記述は時相論理的な記述であり、以下のように簡単に記号的な形で記述することができる。
$\square$( $Printarrow(ButtonEvent=$ Cancel${ }$ButtonEvent $=N_{on}e)$ )このような方法で GUI Program を時相論理を使って設計する手法を考えよう。。
GUI Application は次のように三つの部分に分けて記述する。
命題論理 Event の相互関係を定義する
述語論理 Toolkit の処理と Data Dependency を記述する
スクリプト Toolkit の見かけを定義する

今の場合は、
命題論理 Propositional Interval Temporal Logic
述語論理 First Order Interval Temporal Logic (Tokio [6])スクリプト$\mathrm{T}\mathrm{c}\mathrm{l}/\mathrm{T}\mathrm{k}$146$\mathrm{p}_{\mathrm{r}\mathrm{o}\mathrm{t}_{O\mathrm{C}}\mathrm{O}}]/\mathrm{E}\mathrm{v}\mathrm{e}\mathrm{n}\mathrm{t}$Mult-Linear Time Specification
(LITE

)

$\mathrm{v}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{i}\mathrm{e}\mathrm{r}/\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{s}\mathrm{i}\mathrm{Z}\mathrm{e}\mathrm{r}$Figure 1: GUI Application の分割記述を使う。 .
Toolkit は非常に再利用性が高い Unit だが、簡単な状態処理しかできない。 ここでは意図的にToolkit での Event の相互関係処理をおこなわない。つまり、 Toolkit は次のような関数であるとする。

Toolkit 現在の状態$arrow$

次の状態

この関数を述語論理で記述する。
Event を生成する可能性のある Button, Entry, Menu などは、命題論理値を生成する。この Eventの値は時間によって異なる真理値を持つ。例えば、時刻 3 には真、時刻 5 には偽などとなる。 Eventには入力 Event と出力 Event の二つがある。 Button などは入力であり、 Button の色などが出力となる。出力 Event はユーザによって直接操作されることはない。
それを時相論理式で組み合わせた入力条件を乃Button などの Event をとしよう。 によってその条件に対応する Toolkit の処理を表す。
次の状態という関数であり、実際には次の時刻を表す@ という演算子のみ
五は、現在の状態
を含む –階述語論理式を使って記述する。
には様相論理演算子を含まない普通の論理式を使う。例えば、「青ボタンが押されていればボールがはずむ」などという記述を意図している。
$\mathrm{E}_{\mathrm{V}}\mathrm{e}\mathrm{n}\mathrm{t}_{1},$$\mathrm{E}_{\mathrm{V}\mathrm{e}\mathrm{n}}\mathrm{t}2\cdots \mathrm{E}\mathrm{V}\mathrm{e}\mathrm{n}\mathrm{t}_{n}$$f_{i}$$arrow$$p_{i}$

Toolkiti$\equiv p_{i1}$A$\wedge$$p_{i2}$(($p_{im}$$\mathrm{E}\mathrm{V}\mathrm{e}\mathrm{n}\mathrm{t}_{2},$$\mathrm{E}\mathrm{V}\mathrm{e}\mathrm{n}\mathrm{t}_{1},$$\ldots,$EVen,$\mathrm{E}\mathrm{v}\mathrm{e}\mathrm{n}\mathrm{t}_{1},$($\mathrm{E}\mathrm{v}\mathrm{e}\mathrm{n}\mathrm{t}_{1},$$\mathrm{t}_{2},$$\ldots,$

Event)nEvent)n$\mathrm{E}\mathrm{v}\mathrm{e}\mathrm{n}\mathrm{t}2,$$\ldots,$

Event)n$arrow f_{i1}$$arrow f_{i2}$$arrow f_{im}$このように記述された Toolkit はオートマトンとして容易に実装することができる。
このように記述された Toolkit を複数同時に動作させる。そのためには「いつも が成り立つこと」, Event2.. Everという演算子を使う。Event の相互作用を表す時相論理式をを表すとすると GUI Application は以下のような時相論理式で表すことができる。
$\mathrm{p}$$SChedu\iota_{e(\mathrm{E}\mathrm{t}_{1}}\mathrm{v}\mathrm{e}\mathrm{n}$$\square$$P$

schedule ($\mathrm{E}\mathrm{V}\mathrm{e}\mathrm{n}\mathrm{t}_{1},$$\mathrm{E}\mathrm{v}\mathrm{e}\mathrm{n}\mathrm{t}2,$$\ldots,$

Eventn) A$\square \mathrm{T}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{k}\mathrm{i}\mathrm{t}_{1}$A$\square \mathrm{T}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{k}\mathrm{i}\mathrm{t}_{2}$A... A$\square \mathrm{T}_{\mathrm{o}\mathrm{O}}1\mathrm{k}\mathrm{i}\mathrm{t}_{m,-}$147

schedule には例えばbutton が押されてから stop button が押されるまで青である」などという条件が来る。 このスケジューラ部分は状態間の制約が来るので自明な実装は存在しない。
・この部分を自働検証系を使ってサポートしょうというのが今回の狙いである。
このような分割は–種のプログラミング方法論であり、 -意的に分割されるわけではない。出力
Event の Button の色などは–階述語部分で記述しても良いし、命題論理部分で記述してもよい。
$\lceil_{\mathrm{S}}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}$2Interval Temporal Logic

ここで使う時相論理は離散時間 (descrete time) と時区間の概念を持っている区間時相論理 (Interval
Temporal Logic) というもので、普通の論理演算子や命題変数/述語変数の他に以下のような演算子を持っている。

chop 二つの時区間を–つの時刻を重ねてつなげる。 p& で表す。
$q$next 次の時刻から始まる時区間を表す。時区間の長さが の時に無条件に真となる定義するものを O で表す。時区間の長さが の時に無条件に偽となる定義するものを@P で表す。
$0$

$0$

$P$

empty 長さ$0$の時区間を表す。

proi 単位時間の変更を表す。単位時間を$q$を定義する時 PProi

$q$

$P$

という時区間とする、 より coarse grained な時間区間と表す。

この論理は命題変数が時刻にだけ依存する場合 (命題変数が local という性質を持つという) は決定可能であることが知られている。ただし、計算量は変数の数に対して指数的、時相論理式の長さ対して指数的とかなり大きい。量化記号を入れても計算量は増えるが決定可能である。 しかし 逆にいえば変数の数と式の大きさが小さければ比較的簡単に検証できるともいえる。
量化記号が入ると –階述語論理に近いと考える人もいるだろう。実際、 このまま –階述語論理にも tableau method を適応できる場合もあるが、その場合は限られている。 もっと弱い時相論理、
例えば、 Linear Time Temporal Logic に関しては多項式オーダの決定手続きが知られている [5]。
$\sqrt$さらに以下のような演算子を定義する。

more$\equiv$$\text{◇}P$$\equiv$$\square P$$\equiv$

skip$\iota_{engt}h(n)$less $(n)$

P&&Q
$*P$

$\equiv$$\equiv$$P$$P$$\neg\text{◇}\neg P$$\text{長さ}\mathrm{n}$$\ldots$$\equiv\underline{\mathrm{O}\mathrm{O}^{n}\cdots \mathrm{O}}F$$\equiv$$\equiv$$+P$$\equiv$

fin $(P)$$\equiv$

keep $(P)$stable $(P)$halt $(P)$% 空でない時区間
% いっか
T&P
% いつも
% 単位時間@empty\sim @@-empty%$\neg empty$$\equiv$$\equiv$$\equiv$%$\text{長さ_{}\mathrm{n}1_{-}\perp_{\Gamma}}\backslash -$(P\wedge \neg empty)&Q% 必ず時間の進む chop
( $P$ proi ) $\vee(empty \wedge P)$ %closure 繰り返し
% 一回以上の繰り返し
P&* P.
% 最後で になる
% 最後を除いて になる%-つの時区間で が安定
keep(@P $=P$ )% で最後になる$T$$\square (em_{P^{ty}}\Rightarrow P)$$\mathrm{P}$$\square (\neg em_{P}ty\Rightarrow P)$$\mathrm{P}$$\mathrm{P}$$empty\Leftrightarrow P$$\mathrm{P}$

これらの時相論理式は命題変数の真偽の時系列\mbox{\boldmath $\sigma$}(有限でなくてもいいが終端がなければならない) を与えると真理値が決まる。正式には時系列を使って時相論理演算子の定義をおこなう。例えは が真である状態を任意の長さつなげた時系列に対して真である。
ば、決定手続きは Tableau method の拡張であり、時相論理式が受け入れる時系列集合をオートマト$\square p$$P$ンの形で出力することができる。

148

3

-階述語論理と命題論理の組み合わせ

最初に述べた GUI Application の記述のうち命題論理の部分は自動検証系によってオ一トマトンに変換される。 この時、入力である Event と出力となる Event を区別する必要がある。時相論理式

レベルでは入出力は区別されない。オートマトンは@演算子を使って述語論理で容易に記述できる
し、命題論理変数の状態を Toolkit を記述する–階述語論理式に余分な引数として付け加えてやる
ことによって、 すべての記述を述語論理に落すことができる。
階述語時相論理の実行は Prolog と同じようにおこなわれる。時相論理演算子については不動点演算子つまり再帰と同じように取扱う。従って、 このままでは否定の実行や無限に続く再帰に関しては完全には実行されない。
このシステム $[3, 2]$ は時相論理だけなく、状態遷移記述を直接に入力に使うことができるので、などだけでなく、 SIS などの CAD ツールなどにも接続できる。
X-Window の$\mathrm{T}\mathrm{c}\mathrm{l}/\mathrm{T}\mathrm{k}$路記述
犬態遷移記述$\mathrm{Q}$

Figure 2: 時相論理プログラム合成システムに遡るが GUI に使えること、 projection を持った ITL を使っている
この枠組は古くはこと、証明図が直接出力できることなどが新しい。実際のシステムでは内平, 本位田らのという Petri-Net と命題時相論理を結合するものがあり、 このシステムはその Petri-Net 部分を述
語時相論理に置き換えたものと見ることもできる。
$\mathrm{W}\mathrm{o}\mathrm{l}\mathrm{p}\mathrm{e}\mathrm{r}[5]$$\mathrm{M}\mathrm{E}\mathrm{N}\mathrm{D}\mathrm{E}\mathrm{L}[4]$

149

4

簡単な生成例

この例は勝手に動いているボールを Run と Stop の二つのボタンによって制御する例である。時相論理部分は以下のようになる。

Figure 3: Toy Example($[_{\mathrm{S}}\backslash$$\mathrm{p},\mathrm{S}\mathrm{t}\mathrm{a}_{\mathrm{F}4}\sqrt[\backslash ]{}i\grave{\grave{\mathrm{a}}};t^{\mathrm{r}}\mathrm{t}\mathrm{g}’\ovalbox{\tt\small REJECT} \mathrm{u}_{4T}\mathrm{i}\mathrm{t}]$$|/.*_{\text{、}}\prime\dagger^{\backslash }\text{、タ\sqrt[\backslash ]{}\mathrm{s}\mathrm{t}_{-^{\mathrm{V}\mathrm{a}\mathrm{r}}}\mathrm{a}\mathrm{b}1k_{5’}^{\Rightarrow}+^{\backslash }\mathrm{e}\mathrm{S}$タ.

[red,gree,movel)$[]$((red, not (green); not (red) , green)) ,/.

赤は止まれ、 青は動け$[]$$((_{\mathrm{g}-}\mathrm{r}\mathrm{e}\mathrm{e}\mathrm{n}>\mathrm{m}\mathrm{o}\mathrm{v}\mathrm{e}))$

,

$[]$

(

$(\mathrm{r}\mathrm{e}\mathrm{d}->\mathrm{n}\mathrm{o}\mathrm{t}$$)$.

(move))) ,.

stop から、ずっと赤stop- keep(red)/.
start から、ずっと青
start- keep(green)
繰り返しは+で表す

$|/$

$>$

.

$>$

$|/$

$+(($

(
keep (red)) ,(start- keep (green)) ,$\mathrm{s}\mathrm{t}\mathrm{o}\mathrm{p}^{-}>$

.
.

$>$

時間の区間の区切りは stop または start または quit
; start; quit)))next (halt$))$ ,
quit ボタンが押されたら終り
halt (quit).
$|/$$((\mathrm{s}\mathrm{t}\mathrm{o}\mathrm{p}$

$|/$

4.1

動作記述の例

ツールキット部分は Tokio によって記述される。ここで出て来る時相論理演算子は次の時刻を表す@ と、 いつもを表す だけである。ボールの動作等は–階述語で記述されているのがわかる。
$\square$/. ツールキットを $[]$ (いつも)..

$\mathrm{t}\mathrm{o}\mathrm{y}\mathrm{l}(\mathrm{w},\mathrm{R},\mathrm{G})$$\mathrm{s}1$

$[]$

$|/$

((

を使ってプロセスとして起動する$:-$

generated scheduler$\mathrm{b}\mathrm{u}\mathrm{t}\mathrm{t}\mathrm{o}\mathrm{n}_{-^{\mathrm{r}}}\mathrm{e}\mathrm{d}(\mathrm{R})$button-red(Out)$*\mathrm{r}\mathrm{e}\mathrm{d}=0$, button-green (G) , bounce:, out (Out,$||’|$, red).

$(\mathrm{W})$

)).

.

$|/$

output

150.
. View.

button-red(Out)$*\mathrm{r}\mathrm{e}\mathrm{d}=1$

bounce($[_{-}$:, red).
out (Out,Obj, -Xout, X, -Yout,$||\mathrm{R}\mathrm{e}\mathrm{d}’|$$*\mathrm{m}\mathrm{o}\mathrm{v}\mathrm{e}=1.*\mathrm{q}\mathrm{u}\mathrm{i}\mathrm{t}=0$.

,
is, X. Y) ,moveto (View,( , Xd, Xdl, Xlim) ,$Y1$).
calc-yd(Y.
Ytl,
Xdl,
OX

$Y1$

$Y$

, Xd, Yd, Ydd. Xlim, -]) :-$Y+Y\mathrm{d}$$\mathrm{o}\mathrm{b}\mathrm{j}$$\mathrm{c}\mathrm{a}\mathrm{l}\mathrm{C}_{-}\mathrm{x}\mathrm{d}$$\mathrm{X}$$Y\mathrm{d}\mathrm{t}$$Y\mathrm{d},$$=\mathrm{X}+\mathrm{X}\mathrm{d},\mathrm{Q}\mathrm{x}\mathrm{d}=$. .

$Y\mathrm{t}1$$\mathrm{Q}Y=$$@Y\mathrm{d}=\mathrm{Y}\mathrm{d}\mathrm{t}+\mathrm{Y}\mathrm{d}\mathrm{d}$.

タイミング記述の例 (2)4.2

この動作記述をそのまま使って、同さタイミングだけを変更することもできる。 ここでは、信号が勝手に点滅する例を記述しよう。

..

$|/$

$|/$

$\mathrm{s}\mathrm{t}$$\mathrm{s}\mathrm{t}$$|/_{0}$

状態遷移記述を入力とすることもできる
信号は勝手に点滅する(($\mathrm{S}0$$\mathrm{s}1$, (green,not (red)),, (not (green) ,red),$\mathrm{s}1$$\mathrm{s}0$

..

).

$|/$

).

$|/$

状態
状態 sl

$\mathrm{s}0$

projectin によって状態遷移のクロックを長く (length 5) する
proj
クロックの定義(length(5),/. 大きなクロックの間、信号は変わらない)(red) , stable(
大きなクロックでの状態遷移の実行,(
halt (quit)
st

.

$($

$|/$

.

$(\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}$$(\mathrm{g}\mathrm{r}\mathrm{e}\mathrm{e}\mathrm{n}))\ \mathrm{s}\mathrm{k}\mathrm{i}\mathrm{p}$

$|/$

$)$

$(\mathrm{s}\mathrm{O}),$

$)$

.

$|/$

$)$

start で動く((
keep (not (move))),(start- keep (move)) ,next (halt ((: start; quit))) $))$

stop で止ま$+($$\gamma_{)_{\backslash }}$$\mathrm{s}\mathrm{t}\mathrm{o}\mathrm{p}-\rangle$$>$$\mathrm{s}\mathrm{t}_{\mathrm{O}}\mathrm{p}$

4.3

利点

命題論理との組み合わせで改善されるのは否定の実行の部分である。命題論理パートに関しては時相論理演算子と否定と自由に組み合わせることができる。従って実行可能な部分が述語論理を直接実行する場合よりも広がる。実行可能な範囲内でも前もってオートマトンを展開する分だけ高速に実行できる可能性がある。つまり余計なバックトラックを減らすことができる。
最終的には時間を含まない述語論理に落ちているので Prolog のプログラム理論的な利点をそのまま引き継いでいる。例えば、プログラムの意味を集合として与えることができる。特に有限時間内ならば全ての可能なスケジュールを試すことができる。

述語論理部分のプログラミングは再帰がループに書きかわっている分だけ容易になっている。
矛盾した仕様に対しては空のオートマトンが前もって出力される。 また、失敗する状態に関しては前もって枝苅りをして状態を減らすことができる。

151

命題論理部分に関して述語論理部分とは独立にテストすることができる。実際、 自動検証系をフルに使ってテストすることができる。テスト条件をオートマトンで記述したり時相論理を使って記述することもできる。

4.4

欠点

プログラミングという視点から見ると二つの部分に分けて記述するのは冗長な気がする。特に自明な部分に関しても他の記述との整合牲を考えて二重に記述する必要がある。何もしない Toolkit に関しては何もしないことを@A $=A$ のような形で明示的にしていしないといけない。
’Prolog に較べて命題論理パートは合成結果を予測することが難しい。 もちろん、論理式通りの結果が合成されるわけだが、 それが実際にどういう意味なのかを理解することが難しい。

合成に余計な時間がかかるのはうれしくない。命題変数が多い場合は状態遷移数が増える。記述が非決定性を多く含む場合は状態数が多くなる。

4.5

生成されたプログラムの質

合成された結果は仕様を満たす可能な実行をすべて含んでいる。 ということは、非常に効率の悪い結果も効率の良い結果も均等に合成されている。可能な実行の内、 どれを実行するかは述語論
理/Prolog に落した時に決まる。実際には depth first に実行される。
depth first に実行されると分かっていれば生成されたオートマトンをさらに小さくすることができる。例えば、 リアルタイムスケジューリングが特定の決まった繰り返しで実現できるならば、 その繰り返しを実現するオートマトンだけを使えば良い。 しかし、 これには次に述べるような入出力に関する問題がある。
一般的にいって生成されるプログラムは馬鹿であるが、 それを depth first に実行すると実用的な結果を与えることが多い。そのような特殊な実行のみを生成するオートマトンを採用すると 結
果的にオートマトンを小さくすることができる。 ということは、最初から効率を考えて合成してい$\text{、}$く方法をとることによってより大きなプログラムを合成できる可能性があることがわかる。

4.6

入出力の区別が必要な理由生成されたオートマトンは入出力の時系列に対して真偽を返すだけである。 これは特性関数 (characteristic function) と呼ばれる。
入力列く出力列$arrow \mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}/\mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$

これをプログラムと見るためには入力を与えて出力を返すようなオートマトンを作らなくてはなら
ない。

入力列

$arrow$

出力列

一般的にすべての入力列に対して出力列が存在するとは限らない。
それは、入力列を でくくることで検証することができる。 しかし、仕様そのものをすべての入力列に対して記述すること自身がかなり冗長であり難しい。 もちろん、すべての入力列に対して仕様を満たす出力を要求することは論理的な視点からは正しいのだが、大抵の場合、 tribial な出力列を付け加えることが搭要なだけなので単にめんどくさい作業になる。例えば、停止ボタンと作動
ボタンと二つあったとする。停止ボタンと作動ボタンが排他的であるという仮定を入力に対して置
くと仕様記述を小さくすることができる。 しかも、その生成された結果に対して停止ボタンと作動
ボタンを同時に押した入力に対しておこなうべきことは、 どちらかだけが押されるという条件を満たすまで実行を遅らせるだけである。
$\forall$152

また出力列が存在する場合も、複数可能な出力列から–つを選択する必要がある。 ところが、ある特定の出力を選択した場合には将来の入力列に対して特定の仮定を設けることになる場合がある。例えば「5 秒実行」ボタンに対して 10 秒実行する時系列を選択することは、その時点では正し
いが 5 秒後以降は間違う可能性がある。Prolog にコンパイルする場合はバックトラックが使えるので条件は若干緩いが本質的にはこの問題は残っている。つまり、$\forall$

入力列$\forall$

途中までの入出力列$arrow\exists$

出力列を保証するようなオートマトンを実際には構築しなくてはならない。 これはやさしくない問題だ
が、入力列が状態依存しないような仕様の場合は自明になる。つまり 5 秒実行するか 10 秒実行す
るかをユーザにその時点で教えなければ破綻することはない。実際には「ユーザに状態を覚えておいてもらうような仕様」は普通作らないので大抵の場合は、 この条件は満たされている。 Real-time
Scheduling のような問題は 「どう頑張っても間に合わない入力列」 というのは残るのが許される立場 (Soft Real-time) と許さない立場 (Hard Real-time) がある。 Hard Rea-time では実現できる仕様
や入力列に対して仮定を置くことが許されているのが普通であるので少しは救いがある。

4.7

生成されたプログラムの量

今回作成した検証系は決定性オートマトンを生成する。従って非決定性をたくさん含むような仕様に対しては巨大なオートマトンを生成してしまう。 また運良く小さい場合でも生成されたオートマ
トンは冗長性を含んでいる。例えば仕様の中に「同等だが異なる項」があると冗長性が入る。通常は仕様には組み合わせると同等になる項は多量にあるので生成された結果には–般的に冗長性が
ある。

$–$

.

ここで要求されているのは単なる状態数の最小ではなくて前節で述べたような実行系列の探索をおこなう時に便利なように最小化しなくてはならない。表現自身が決定性オートマトンであることも必要ない。蓄積量が少なければ非決定性オートマトンを使っても良い。 しかし、 この場合は可.
能な実行系列を探すことが難しくなる可能性がある。
現時点で有効であるとわかっているのは時相論理式の sub term に対する BDD (Binary Decision
term の組み合
Diagram) であり、状態遷移をそのまま格納するのに較べて有利である。 これはわせに依存する状態数に較べて変数の指数乗に依存する状態遷移数の方が多いからである。通常、入力変数に対してはすべての可能な遷移があるのが普通なので状態遷移数がどうしても多くなる。
状態遷移は状態から生成することができるので格納する必要はない。 しかも入力状態が決まっていれば状態から–般的な場合よりもより少ない状態遷移を生成することができる。ただし、実験はしてないが、 これを実行時におこなうのが望ましいとは思えない。
BDD は状態圧縮の–つの手段であり他の圧縮技術があればそれを採用することを妨げるものは$\backslash$$\mathrm{s}\mathrm{u}$なにもない。

しかしより圧縮を可能にするのはオートマトンの分割である。合成をおこなう際にもより小さな仕様から合成する方が圧倒的に有利なわけであり、最初から適切に分割してある仕様から合成をおこないたい。オブジェクト指向プログラミングは、そういう視点から見て正しい部分と正しくない部分がある。単なる分割では生成されたタイミング制御部分が小さくなるとは限らない。通信変数が増える分だけ大きくなる場合もある。頻繁に通信する部分と疎に通信する部分とを分割するよ
うなプログラミングが望ましい。実際、 自動検証が容易なプログラムが良いプログラムだと考えることもできるし、実際にわかりやすいプログラムになる。 しかし、具体的にどういう分割が望まし
いかは良く分かっていない。 また、 BDD をうまく圧縮するような分割を見つけるアルゴリズムも分かってない。

153

4.8

生成された特性関数の実際

比較的制約のきつい Real-time scheduling の例を考えよう。

% 非同期プロセス((( proj (length(5)\wedge (dc)))\wedge length(l5))&T)\triangle% 繰り返しプロセス( $(\iota_{e}ngth(3)$ proj @◇ (ac))\wedge \tau )\wedge(( $\iota_{e}ngth(5)proj$ @◇ (bc))\wedge T)\wedge((length (5) $proj$ @◇ (cc))
)
%排他制御
$T$

$\square$$\wedge T$$\square ($(( $ac$ A $\neg(bC)$ A$\neg(cc)$$\wedge$

A $\neg(dC)$ )(A
A $\neg(cc)$ A $\neg(dC)$ )( $\neg(ac)$ A
A
A $\neg(dC)$ )( $\neg(ac)$ A $\neg(bC)$ A $\neg(cc)$ A $dc$ )( $\neg(ac)$ A
A $\neg(cc)$ A $\neg(dc)$ )$\neg(ac)$$bc$$\urcorner(bC)$

${ }$

${ }$

$CC$

${ }$

$\vee$$\neg(b_{C})$$))$は以下のような特性関数を生成する。 ここで横軸は入力状態、縦軸は出力状態を表す。点は遷移可能な状態の組を表す。 特徴的なのは直線が現れることで、 これが非決定性の少ない逐次的な実行

Figure 4: Real-time scheduling の特性関数を示している。並べ方を変えれば図も代わるが、状態を depth-first に生成した順に並べることによる逐次プロセスが直線となる。同じような図形が繰り返しているのは特性関数の冗長性を示して
いる。

154

次に非決定性を多く含む例として Dining Philosopher をあげよう。
%five philosophers$more\wedge$*(( ((\neg al\wedge mar))&@(al \wedge \neg ar\wedge @(al \wedge ar\wedge @(ar*(( ((\neg bl\wedge br))&@(bl \wedge \neg br\wedge @(bl \wedge br\wedge @(br\wedge cr\wedge @(cr*(( ((\neg cl\wedge cr))&@(cl*(( ((\neg dl\wedge dr))&@(dl \wedge \neg dr\wedge @(dl \wedge dr\wedge @(dr\wedge @(er*(( ((\neg el\wedge er))&@(el \wedge \neg er\wedge @(el%shared resources$\square$)$em_{\mathrm{P}^{t}y))\wedge}$) $em_{P^{t}y))\wedge}$) $))empty)$ )) $))empty)$ )) $))empty)$ )$\wedge\square (\neg bl)))$$\square$$\square$$\wedge\square (\neg al)))$$\wedge\square (\neg Cl)$$\wedge\urcorner cr\wedge@(cl$$\square$$\wedge er$$\square$$\wedge\square (\neg dl)$$\wedge\square (\neg el)$$\wedge$$\wedge$$\wedge$$\square (\neg(ar\wedge bl))\wedge\square (\neg(br\wedge cl))\wedge\square (\neg(cr\wedge dl))\wedge$$\square (\neg(dr\wedge el))\wedge\square (\neg(er\wedge al))$

これが生成する特性関数は以下のようになる。 ところどころにある黒い島が非決定性の固まり

Figure 5: 5 Dining Philosopher の特性関数である。何人かがデッドロックすると非決定性が少なくなり -点に収束する。 ここでも冗長性を示

す繰り返しを観察することができる。

5

プログラミングツールとして) 時相論理$\dot{\mathit{0}}$時相論理の良い点は複雑な仕様をコンパクトに記述できる点であるが、 これは–面欠点でもある。
ある程度の長さの時相論理の仕様を–部修正すると驚くような大きな変化がある場合がある。 -つの方法は前節で述べたように変更しやすいような仕様の分割方法を考えることである。 しかし、その分割方法は自明ではない。実際、プログラムを作る時に、 どのように構造化あるいはオブジェク
トを作っていくかは自明でない。
もう –つ、別な方法として時相論理を直接的な仕様記述ツールとして使うのではなく、オートマ
トン変更/特性関数変更演算として使うことが考えられる。 この視点から見ると ITL の演算子は次のように見 . ことができる。
$\text{る}$155chop 二つのオ一トマトンを直列結合する。

and 二つのオ一トマトンを並列結合する。

or 二つのオートマトンを非決定的に結合する。

next オ一トマトンを–つずらす。
proi オートマトンを拡大する。 オートマトンの繰り返しを作る。
この変更演算でどのような性質が保存されるかを研究していく方向が–つ考えられる。このような演算は直接オートマトンを計算していけば良いと考えるかも知れない。実際、そのような方法で時相論理を検証する方法もある [1]。しかし、 その方法は指数オーダのオートマトンの決定化を繰り返しおこなうために非常に高くついてしまう。Tableau method は指数オーダを要求するが– 回で済むという利点がある。実際、変数が少ない場合は–般にオートマトン合成よりも速く結果を得る
ことができる。

あと、多少、強引で無理な方法だが、 これらの時相論理演算子と量化記号を組み合わせて既存のプログラムのパッチ当てをおこなうこともできる。 この方法の欠点は、パッチ当てをおこなう際にもとのプログラムの–部を弱くする必要がある。 これは量化記号を用いるか状態遷移の–部を取り除くことで可能だが、 どちらの方法もプログラムに不規則な非決定性を導入してしまう。 これは特性関数という表現を使う場合には特性関数を巨大にする原因となる。

References[1] Gjalt G. de Jong. An Automata Theroretic Approach to Temporal Logic. In Computer Aided.
Verification. Springer-Verlag, July 1991. 3rd International Workshop,$\mathrm{C}\mathrm{A}\mathrm{V}’ 91$[2] Masahiro Fujita and Shinji Kono. Synthesis of Contrllers from Interval Temporal Loigc Specification. In International Conference on Computer Design, October 1993.
[3] Shinji Kono. A Combination of Clasual and Non Clausal Temporal Logic Program. IJCAI-93
Workshop on Executable Modal and Temporal Logics, Aug, 1993.

[4] N. Uchihira. A petri-net-based programming environment and its design methodology for cooperating discrete event systems. IEICE Trans. Fundamentals, Vol. E75-A, No. 10, pp. 1335-1347,
1992.
[5] P. Wolper. Synthesis of mmunicating processes from temporal logic specifications. Technical
Report STAN-CS-82-925, Stanford University, 1982.
$\mathrm{c}o$[6] 河野真治, 青柳龍也, 藤田昌宏, 田中英彦. 時相論理型言語 Tokio の実装. In Logic Programming
Conference ’85, 1985.