線形時相論理式からイベントベースオートマトンへの変換を利用したペトリネット検証ツールHiPS向けon-the-flyモデル検査器

摘要

本稿では，ペトリネットより生成される状態空間を対象に，線形時相論理式によるon-the-flyモデル検査器の設計について記す．筆者らの研究グループによって開発·公開されているペトリネット設計·検証ツールHiPSがある．HiPSには，発火系列により構成される，ペトリネットの初期マーキングを根とする状態空間を生成する機能が備わっている．HiPSは外部ツールと連携することで，状態空間に対するモデル検査を行うことができる．現状ではモデル検査を適用するためには全ての状態空間の生成を行わなくてはならず，物理的，時間的制約から大規模モデルへの適用は難しい．そうした状態爆発に対するモデル検査の効率化として，on-the-fly手法が挙げられる．on-the-fly手法とは，状態空間構築と並列して検査を実行する手法である．モデル検査時にHiPSの機能である状態空間生成プロセスとのIPCチャンネルを用いたプロセス間通信を行う．検査部と状態空間生成部を互いに独立して動作をさせることでon-the-fly検証を実現した．