抄録
A-003
拡張被覆グラフを用いたL2/L3活性判定器のペトリネットツールHiPSへの実装
三井雄太・張江洋次朗・和崎克己(信州大)
ペトリネットは,離散事象システムの設計検証を目的としたモデル化手法で,解析を行うことで対象システムの様々な性質を知ることができる.ペトリネットの動的性質の解析として活性(liveness)判定がある.活性は,初期マーキングからの得られる全ての可達マーキングから,ネット内の任意のトランジションを一回以上発火可能にする.従来から活性条件を緩めたレベルが定義されており,任意の自然数回/無限回トランジションを発火可能とするL2/L3活性がある.これらの活性レベル判定のためには本質的に非有界ネットのための被覆解析が必要となるが,従来からの被覆性を利用したωマーキングによるグラフ生成の有限化では,特にトークンの減少に関する情報欠落の問題があった.このため筆者らはL2/L3活性の判定に必要な情報を,従来の被覆グラフに付与した拡張被覆グラフ(ECG)を提案した.対象ネットから生成した拡張被覆グラフ内のループを解析することで,L2/L3活性判定器を構成した.本解析器は,本学で開発しているペトリネット設計ツールHiPSに実装する.