近年、科学技術の発達によりハードウェア・ソフトウェアは複雑かつ大規模な ものとなっている。そのため設計段階において誤りが生じる可能性が高くなっ てきている。その結果、設計されたシステムに誤りが無い事を保証するための 論理設計や検証手法の確立が重要な課題となっており、数学的に設計の正しさ を保証することができる検証手法が重要視されてきている。
時相論理はその検証手法でも有効な手段の一つである。しかし検証における計 算量はP-Spaceであることも知られている。しかし、その詳細は対象となる問題や時相 論理の種類、検証法によって異なる。本研究ではLTTL(Linear Time Temporal Logic)、ITL(Interval Temporal Logic)の２つの論 理に対して、 Semantic Tableaux、Resolutionという２つの決定手続きを実装し、 充足性のチェックにかかる計算時間を実測、比較しその違いについて考 察する。
本研究で用いるTemporal operatorは５種類ありLTTLでは□(allways), ◇(sometime) ITL では＆(chop)、｜(bar)を用いる。 またそれぞれの論理で用いるoperatorの○(Next)がある。

LTTLでは時間を直線的で、1クロックづつに分ける離散的な時間を考える。この論理は 終了時間が存在しない無限の時間で考える論理である。

ITLでは真理値は時間区間に対応して決まる。 定義３ ＆を任意な２つの時区間の結合とし、時区間 t でのAの評価を v_t (A) とする。論理式での時区間の結合(chop)も同じ記号＆で表す。 v_t (P ＆ Q) = v_t' (P) ∧ v_t''となり、 t = t' ＆ t''
また、chopの双対であるbar |を次のように定義する。 P ｜ Q = ¬ (¬ P ＆ ¬ Q)
さらに○についてはAより1時区間短い式で考える。
ITLではtableau methodの展開を時間が0であるemptyと0 以外の時間であるmoreに分けて考える[2][3]。
ITLでは終了時間が存在するため、eventualityに関しては、展開終了時刻にその 事象が起こっているなら、その論理式でのeventualityは満たされていると考える ことができるのでチェックを行う必要がない。

これらの論理を実装し、充足性のチェックにかかる時間を計りその結果 をグラフに示した。図１、図２は単純なallways operator、 Sometime operatorのネストにかかった時間をそれぞれに示す。 またいろいろな論理式を実際に展開し、それにかかった平均時間を表３ に示す。かかった時間にある **** は計測したCPUのメモリ 不足のため計測できなかったことを示している。 LTTLのresolutionに関しては、eventualityのチェックが完全でないため、 sometime operatorの入った論理式は展開できないものが数多くあった。

図１ Allways operator の個数

図２ Sometime operator の個数

図１、図２からわかることは、LTTLとITLではallways、sometime operator のネストに関しては対称的な結果となった。それに対し、resolutionでの 展開はtemporal operatorのネストはCNFに変換する時にネストの省略を 行っている。そのためsemantic tableauxよりは高速に展開が行えたと考えられる。

表３ いろいろな論理式の展開にかかった時間[s]

しかし、いろいろな論理式の展開を行った表３で分かるように operatorの組み合わせが増加すると、resolutionでは展開を行うことが できなくなった。それに対し、LTTL、ITLでは時間は増加しているが展開 はほとんど可能であった。
LTTL、ITLは変数やoperatorの数が増加すればかかる時間も指数オーダーでほ とんど増加している。しかし、一部の式では高速に行えるものもあった。
Resolutionについては現在、CNFは線形リストで表している。そのためresolution できないものもリストに入っているのでresolutionの対象を探すのに、時間が かかっている。また、次の時刻に対して展開を行うたびに、リストが 大きくなる可能性があり複雑な式ではメモリ不足の為に展開を行うことが できなくなったと考えられる。
その解決策としてリストをハッシュ化することで、clashed literalを効率的 に探索し、resolutionを行う回数を減らす事ができればより高速に実行でき ると考えられる。

本研究では、各種の時相論理の自動検証を行った。まだどの論理での 充足性のチェックにtemporal operatorが増加すると、時間がかかっ てしまう。そのなかでresolutionはまだ効率が悪く展開を行えない 式がたくさんある。しかし、与える式によってはsemantic tableauxよりも高速 に行えるものもあった。
これからの課題として、まず検証系の実装自体の効率が悪いので高速に行え るようにする。さらにハッシュ化、並列化、BDD化など考慮し高速化を図る。