本研究の成果は、時間論理式の構文的な特徴からプログラム化可能性の性質の一種である強充足可能性や段階的充足可能性の判定が可能となるかを検討し、論理式の構造によりこれら2つの性質が一致することがあることを示した。また、これらの性質を効率よく判定することができることを明らかにした。しかし、構造が限定的であった。そこで、ネットワーク機器のソフトウェア、ロボット、自動車制御のネットワークシステムなどの検証すべき性質を記述してその構造を分析した。その結果、論理式の構造よりも、システムの動作を表す原子命題と利用者やシステムの外界の動作を表す原子命題の論理式の中の位置が重要であることを明らかにした。
|