SAT技術を用いたペトリネットのデッドロック検出手法の提案

• Item type: Journal(1)
• 公開日: 2018-09-15
• タイトル: SAT技術を用いたペトリネットのデッドロック検出手法の提案
• タイトル / 言語: en
• タイトル: Proposal of SAT-based Method to Detect Deadlock of Petri Nets
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [一般論文（特選論文）] ペトリネット，デッドロック検出，SAT技術，有界モデル検査
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 神戸大学大学院システム情報学研究科
• 著者所属: 神戸大学情報基盤センター
• 著者所属: 神戸大学情報基盤センター
• 著者所属: 神戸大学情報基盤センター
• 著者所属: 国立情報学研究所情報学プリンシプル研究系
• 著者所属(英): en
• 著者所属(英): Graduate School of System Informatics, Kobe University
• 著者所属(英): en
• 著者所属(英): Information Science and Technology Center, Kobe University
• 著者所属(英): en
• 著者所属(英): Information Science and Technology Center, Kobe University
• 著者所属(英): en
• 著者所属(英): Information Science and Technology Center, Kobe University
• 著者所属(英): en
• 著者所属(英): Principles of Informatics Research Division, National Institute of Informatics
• 著者名: 寸田, 智也; 宋, 剛秀; 番原, 睦則; 田村, 直之; 井上, 克巳
• 著者名(英): Tomoya, Sunda; Takehide, Soh; Mutsunori, Banbara; Naoyuki, Tamura; Katsumi, Inoue
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，トークン数が整数値である一般のペトリネットを対象とし，そのデッドロック検出についてSAT技術を用いた手法を提案する．提案手法では，非負整数値であるトークン数を表現するために順序符号化を採用することで，既存のSAT型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した．また，既存SAT型手法で採用されていたモデル（連続発火モデルと呼ぶ）よりも短いステップ長でデッドロック検出が可能となる多重発火モデルを提案し，性能向上を実現した．評価実験では，Model Checking Contest 2017のベンチマーク問題を用いて，連続発火モデルと多重発火モデルを比較した．ほぼすべての問題で多重発火モデルのほうが優れていたが，特に初期マーキングのトークン数が比較的多い問題に対する効果が大きかった．また，Model Checking Contest 2017デッドロック検出部門での優勝ソルバLoLAおよび準優勝ソルバTapaalとの比較を行った．提案手法は，デッドロックを検出できた問題数ではLoLA，Tapaalより少なかったが，LoLAおよびTapaalを含めたすべてのソルバがデッドロック検出に失敗した問題での検出に成功し，提案手法の有効性が確認できた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 59, 号 9, p. 1749-1760, 発行日 2018-09-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764