有界モデル検査の高速化を指向した差分論理に基づく時間ペトリネットの論理式表現

摘要

著者らはこれまでに，SMTソルバを用いて時間ペトリネットの有界モデル検査を行うための手法を開発してきた．SMTソルバは線形制約を扱うことができるため，時間ペトリネットにおける時間制約を線形制約上の不等式によって表現することで，SMTソルバによる有界モデル検査が実現できる．ここで，「x-y＜＞＜＞C」という形式の不等式のみで表現される差分論理（Difference Logic）上の制約に対しては，高速な充足可能性判定アルゴリズムが存在することが知られている．そこで本稿では，時間ペトリネットの時間制約を差分論理によって表現することで，充足可能性判定に基づく有界モデル検査を高速化するための手法を提案する．