|
平成8年度の研究結果は、以下の三つの成果にまとめられる。
・実時間論理の研究
実時間システムの検証に適した実時間論理の構築のために、様々な実時間論理を比較検討し、新しい実時間論理RTLを定義した。この言語は単純な時間様相しか持たないが、十分な記述力を持っている。この言語について稠密時間のモデルを許す場合、本質的にどのような要素が決定可能性に影響を与えるかについて検討し、決定可能性を保持するための必要条件について研究を行なった。また、到達可能な部分集合についてその決定手続きを与え、さらにその公理化可能性についても検討を行なった結果、強完全な公理化が行なえないことが判明した。
・リアクティブシステムの検証の研究
リアクティブシステムの仕様記述の途中段階において、その無矛盾性、実現可能性等を判定するときには、それまでに検証された部分の情報を再利用出来ることが望ましい。そこで仕様の追加、削除に応じた段階的検証方法について研究を行ない、そこで用いられるタブロ-の新しいデータ構造を与えた。また、リアクティブシステムの実現可能性について研究を行ない、実現可能でない仕様については、それを実現可能とするための外部環境制約式を求める方法を与えた。
・非標準論理の証明方法の研究
様相論理の一般的証明方法である様相記号列の統一化における失敗情報を証明戦略に応用する方法について研究を行なった。この方法は実時間論理の証明に対しても拡張されるよう考えられている。また、資源を共有する並行システムの検証に有用な線形論理についても研究を行ない、その自動証明法を与えた。
|
