情報処理学会 第78回全国大会講演要旨

本稿では，ペトリネットより生成される状態空間を対象に，LTL式によるon-the-flyモデル検査器の設計について記す．筆者らの研究グループによって開発・公開されているペトリネット設計・検証ツールHiPSがある．HiPSでは，発火系列により構成される，ペトリネットの初期マーキングを根とするプロセス木を生成する機能が備わっている．HiPSは外部ツールと連携することで，状態空間に対するモデル検査を行うことができる．現状ではモデル検査を適用するためには全ての状態空間の生成を行わなくてはならず，時間的制約から大規模モデルへの適用は難しい．今回，モデル検査の効率化のため，on-the-fly手法を用いたLTLモデル検査器のHiPSツールへの組み込みを行った．