抄録A-015
ペトリネット設計検証ツールHiPSにおけるOn-the-fly LTLモデル検査器
ペトリネット設計検証ツールHiPSにおけるOn-the-fly LTLモデル検査器
◎張江洋次朗・和崎克己（信州大）
離散事象システムのモデリングに有用なツールとしてペトリネットがある．HiPSは，ペトリネット設計ツールとして筆者らの研究グループによって開発・公開されている．ネットが表している遷移関係・状態値を元に動的な性質の検証を効率よく行うことは重要である．線形時相論理で記述した仕様についてon-the-fly実行する検査器の上ツールへの組み込みを本研究で行った．既研究の状態空間生成器によって初期マーキングから出発したトランジション発火系列が得られる．論理式からBüchiオートマトンを生成し，逐次的に得られた発火系列に対する監視を行う．受理した発火系列は反例トレースでありHiPSツール上に可視化される．
