著者

寸田 智也 宋 剛秀 番原 睦則 田村 直之 井上 克巳

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.59, no.9, pp.1749-1760, 2018-09-15

---

本論文では,トークン数が整数値である一般のペトリネットを対象とし,そのデッドロック検出についてSAT技術を用いた手法を提案する.提案手法では,非負整数値であるトークン数を表現するために順序符号化を採用することで,既存のSAT型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した.また,既存SAT型手法で採用されていたモデル(連続発火モデルと呼ぶ)よりも短いステップ長でデッドロック検出が可能となる多重発火モデルを提案し,性能向上を実現した.評価実験では,Model Checking Contest 2017のベンチマーク問題を用いて,連続発火モデルと多重発火モデルを比較した.ほぼすべての問題で多重発火モデルのほうが優れていたが,特に初期マーキングのトークン数が比較的多い問題に対する効果が大きかった.また,Model Checking Contest 2017デッドロック検出部門での優勝ソルバLoLAおよび準優勝ソルバTapaalとの比較を行った.提案手法は,デッドロックを検出できた問題数ではLoLA,Tapaalより少なかったが,LoLAおよびTapaalを含めたすべてのソルバがデッドロック検出に失敗した問題での検出に成功し,提案手法の有効性が確認できた.In this paper, we propose a SAT-based method to detect deadlock of general Petri nets in which more than one tokens are allowed for each place. In our approach, the transition relation of a Petri net is represented as constraints on integers and they are translated into SAT by order encoding, so that the deadlock of general Petri nets can be detected by a SAT solver, while existing SAT-based methods cannot be applied for them. Furthermore, in order to improve the performance, we introduced multiple firing model, which can detect deadlock with shorter steps than the model used in an existing SAT-based method, called successive firing model. We evaluated the successive firing model and the multiple firing model through a benchmark set of Model Checking Contest 2017. The multiple firing model showed better performance for almost all instances, and was especially effective for the instances in which there are many tokens at the initial marking. Through the comparison with the winner tool LoLA and the second place tool Tapaal of the contest, although the number of detected deadlocks are fewer than LoLA and Tapaal, we confirmed the effectiveness of the proposed method with some instances for which all tools including LoLA and Tapaal failed to detect deadlock.