電子情報通信学会総合大会講演要旨
A-10-8
プリエンプティブ制御時間付きペトリネットのSMT論理式表現
◎前田佳樹・潮 俊光(阪大)
発火継続時間規則を用いた時間付きペトリネット(TPN) は非同期並行システムのモデルとして提案された.一方で,トランジションの発火の制御に外部入力プレースが用いられる.さらに,発火の中断(プリエンプション)を表現できる発火規則が提案されている.本稿では,プリエンプションを制御する制御プレースを導入したプリエンプティブ制御TPNを提案
し,その挙動を記述するSatisfiability Modulo Theories(SMT)論理式表現を導出する.