タイムペトリネットにおけるCTL記号モデル検査法について

スポンサーリンク

概要

論文の詳細を見る
モデル検査とは状態グラフ等でモデル化されたシステムの振る舞いが,ある時相論理式を満たすかどうかを調べる検証手法である.この際,状態グラフの状態爆発という問題が生じる.その解決法の一つとして,状態の集合,あるいは状態集合間の遷移関係を論理関数を用いて表し,論理関数演算により与えられた式を満たす状態集合を求める記号モデル検査法がある.しかし,リアルタイムシステムの記号モデル検査法については,従来あまり研究されていない.そこで,本研究では,リアルタイムシステムのモデル化にタイムペトリネットを用い,仕様の記述にCTL式を用いた場合の記号モデル検査法について考察する.リアルタイムシステムには状態数が無限個あるという問題があるため,与えられた式の評価値が同じである状態同士を一つの状態クラスにまとめ状態クラス数を有限化する工夫がある.本稿では整数時刻で代表させる手法,region graphを用いる手法について考察した.
1994-10-27

著者

関連論文

もっと見る

スポンサーリンク