CTL論理式と時間オートマトンに関する実時間記号モデル検査方式の提案

スポンサーリンク

概要

論文の詳細を見る
実時間システムのモデルチェッキング検証は重要な研究課題であり、近年、多くの研究がなされている。モデルチェッキング検証では、状態空間の組合せ爆発を如何に回避するかが重要である。従来の研究では、リージョングラフの最小化手法やon-the-fly 手法が研究されている。本論文では、従来の手法と異なり、二分決定グラフを基礎とする完全なCTL論理式のシンボリックモデルチェッキング検証手法を提案する。最後に、計算機実験により、提案手法の有効性を示す。
社団法人電子情報通信学会の論文
1998-02-13

著者

関連論文

スポンサーリンク