◎太田淳也・和崎克己（信州大）

並列かつ非同期に動作するシステムの設計・検証は一般的に難しいとされている．一方で，離散事象システムの設計・検証に有用なツールとしてペトリネットがある．筆者らはペトリネットでの設計を行うため，援用ツールHiPSを開発している．HiPSにはモデルの動作解析機能が実装されているが，モデルの大規模化に伴い解析結果が膨大になり，扱いにくくなる問題がある．そこで，モデル検査器を利用し，網羅的な動作の中から特定の動作について検証を行う．しかし，実システム規模のモデルの場合，状態空間爆発の問題がある．そこで，本論文では効率的に状態空間生成を行うためのアルゴリズムの提案及び実装を行い，生成器の性能を評価した．