連立不等式に基づくタイムペトリネットのCTLモデル検査
スポンサーリンク
概要
- 論文の詳細を見る
モデル検査法はモデル化されたシステムの振る舞いが、与えられた時相論理式を満たすかどうかを調べる検証手法である。本稿ではタイムペトリネットのCTLモデル検査をする場合の有限状態グラフを、連立不等式を用いた状態数有限化手法に基づき生成する方法について考察する。
- 社団法人電子情報通信学会の論文
- 1996-03-11
著者
関連論文
- 多値非同期式回路の形式的検証に関する研究
- プロセス代数に基づく非同期式論理回路の設計検証 (非同期式回路/システム設計論文小特集)
- 非同期式回路の検証におけるIivenessクラスに関する考察
- 非同期式回路の検証におけるlivenessクラスに関する考察
- ハードウェアによるZBDD処理の実現に関する研究
- ハードウェアによるZBDD処理の実現に関する研究
- ハードウェアによるZBDD処理の実現に関する研究
- Net Unfoldingによるタイムペトリネットの効率的解析
- 有限遅延幅モデルにおける非同期式回路の検証について (テストと設計検証論文特集)
- 時間トレース理論に基づく非同期式回路の検証について
- Failure trace解析に基づくGasP回路の形式的検証
- 星状抽象ペトリネットの解析に関する研究
- 星状抽象ペトリネットの解析に関する研究
- 星状抽象ペトリネットの解析に関する研究
- ZBDDとpartial order reductionに基づく非同期式回路検証方式について
- ゼロサプレスBDDによるペトリネットのCTL記号モデル検査
- 非同期式回路検証のためのレベル指向モデルとその効率的解析法について
- 非同期式回路検証のためのレベル指向モデルとその効率的解析法について
- データパスを含む非同期式回路の検証について
- ZBDDに基づく非同期式回路の検証方式
- ZBDDを用いた検証方式におけるpartial order reductionの適用について
- 高速タイミング検証方式の実現とその効率評価
- ZBDDに基づく非同期回路の検証方式
- 非同期式回路検証器における使用記憶域削減について
- 非同期式回路検証器における使用記憶域削減について
- 非同期式回路検証器における使用記憶域削減について
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Implementing Fast Boolean QDI Function Blocks
- Implementing Fast Boolean QDI Function Blocks
- Implementing Fast Boolean QDI Function Blocks
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- Self-Timed Implementation of Boolean Functions
- n 安全タイムペトリネットの発火規則について
- n安全タイムペトリネットの発火規則について
- ステートチャートのシンボリックな検証方式について
- シミュレーションを利用した形式的検証システム
- シミュレーションを利用した形式的検証システム
- 論理シミュレーションに基づくプロセッサの自動検証
- タイムペトリネットにおけるCTL記号モデル検査法について
- タイムペトリネットにおけるCTL記号モデル検査法について
- 線形時相論理の為の効率的記号モデル検査方式
- 線形時相論理の為の効率的記号モデル検査方式
- 連立不等式に基づくタイムペトリネットのCTLモデル検査
- タイムペトリネットの拡張とスケジューラビリティーの検証への応用
- 対称性及び抽象化を利用した検証方式の効率化 (テストと設計検証論文特集)
- 正規表現を利用したスケーラブル環状回路の検証
- 正規表現を利用したスケーラブル環状回路の検証
- 対称性及び抽象化を利用した検証方式の効率化
- 有限幅遅延モデルに基づく非同期式回路検証方式とその効率化(ペトリネットの応用特集号)