線形時相論理の為の効率的記号モデル検査方式

スポンサーリンク

概要

論文の詳細を見る
設計されたシステムが与えられた仕様どうりに動作するかどうかを確かめる設計検証はシステムの大規模化、複雑化により重要な役割を担うようになっている。一方、検証対象システムが大きくなると検証に要する計算量が急激に増加するという、いわゆる状態爆発という問題がある。この問題を解決する一つの方法として二分決定木(Binary Desicion Diagram)を利用した論理関数処理に基づく記号モデル検査法が提案されている。本報告では、システムがペトリネットによって記述され、検証すべき性質が線形時相論理(Liner-time Temporal Logic)で表されている場合に、記号モデル検査法を効率的に行う方法を提案する。
1993-10-29

著者

関連論文

もっと見る

スポンサーリンク