二分決定グラフによる実時間システムのモデルチェッキング検証
スポンサーリンク
概要
- 論文の詳細を見る
実時間システムのモデルチェッキング検証は重要な研究課題であり、近年、多くの研究がなされている。モデルチェッキング検証では、状態空間の組合せ爆発を如何に回避するかが重要である。従来の研究では、リージョングラフの最小化手法やon-the-fly手法が研究されている。本論文では、従来の手法と異なり、二分決定グラフを基礎とするシンボリックモデルチェッキング検証手法を提案する。最後に、計算機実験により、提案手法の有効性を示す。
- 一般社団法人電子情報通信学会の論文
- 1997-03-18
著者
関連論文
- 実時間システムのための近似手法に基づいた記号モデル検査器の開発と評価
- CTL論理式と時間オートマトンに関する実時間記号モデル検査方式の提案
- BDDによるSpeed-Independent回路の形式的検証
- 二分決定グラフによる実時間システムのモデルチェッキング検証
- 二分決定グラフと時間不等式手法に基づく近似解法による実時間シンボリックモデルチェッキング検証
- リージョングラフを用いた時間オートマトンのシンボリックモデルチェッキング検証
- 実時間制約を考慮した開放型分散システムの形式化と階層的な設計手法
- オートマトン理論に基づくリアルタイムソフトウェアの検証システム