A-005
仕様に基づいたペトリネットのトランジション優先発火によるon-the-flyモデル検査の効率化

○張江洋次朗・和﨑克己（信州大）

ペトリネットは，離散事象システムを表現・解析が可能な数学的手法の一つである．モデル検査の効率化として，システムの振る舞いを表す状態空間の生成と同時に，状態空間が与えられた仕様を満たすか否かを検査するon-the-fly実行がある．並列処理やデータ構造の改善などによる状態空間の生成に関する効率化とともに，状態空間の生成順序に関する戦略について提案する．具体的には，事前に仕様(時相論理式)から得られる観測したいアクション集合に基づき，ペトリネットの次段マーキングの非決定的選択時，仕様に現れるトランジション発火を優先した状態空間の生成を行う．検査に関する重要な状態は全状態空間中の一部であるため，on-the-fly検査時には提案手法による観測アクション列の早期生成による効率化が見込まれる．