リアクティブシステム仕様の実現可能性に関する検証は,仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが,一般に煩雑で計算コストの高い処理を伴う.本研究では,リアクティブシステム仕様の実現可能性判定の高速化を目的として,以下の事項に取り組んだ.(1) 部分的にBDDを利用して効率的に実現可能性判定手続きを実装する手法(部分シンボリック技法と呼ぶ)を開発した.この手法の最大の特長は,非近似的な実現可能性判定にも適用できることである.(2) 実現可能性判定を行う際に用いるωオートマトンをon-the-flyに簡約する手法を開発した.
|