文献

J-GLOBAL ID：201802286194544294   整理番号：18A2203548

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

Proposal of SAT-based Method to Detect Deadlock of Petri Nets

著者 (5件)： 寸田智也 (神戸大 大学院システム情報学研究科) ,  宋剛秀 (神戸大 情報基盤セ) ,  番原睦則 (神戸大 情報基盤セ) ,  田村直之 (神戸大 情報基盤セ) ,  井上克巳 (国立情報学研)
資料名： 情報処理学会論文誌ジャーナル(Web)
巻： 59  号： 9  ページ： 1749-1760 (WEB ONLY)  発行年： 2018年09月15日 
JST資料番号： U0452A  ISSN： 1882-7764  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本論文では,トークン数が整数値である一般のペトリネットを対象とし,そのデッドロック検出についてSAT技術を用いた手法を提案する。提案手法では,非負整数値であるトークン数を表現するために順序符号化を採用することで,既存のSAT型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した。また,既存SAT型手法で採用されていたモデル(連続発火モデルと呼ぶ)よりも短いステップ長でデッドロック検出が可能となる多重発火モデルを提案し,性能向上を実現した。評価実験では,Model Checking Contest2017のベンチマーク問題を用いて,連続発火モデルと多重発火モデルを比較した。ほぼすべての問題で多重発火モデルのほうが優れていたが,特に初期マーキングのトークン数が比較的多い問題に対する効果が大きかった。また,Model Checking Contest2017デッドロック検出部門での優勝ソルバLoLAおよび準優勝ソルバTapaalとの比較を行った。提案手法は,デッドロックを検出できた問題数ではLoLA,Tapaalより少なかったが,LoLAおよびTapaalを含めたすべてのソルバがデッドロック検出に失敗した問題での検出に成功し,提案手法の有効性が確認できた。(著者抄録)

シソーラス用語： *Petriネット ,  *検出 ,  *充足可能性問題 ,  トークン ,  整数 ,  符号化 ,  モデル検査
準シソーラス用語： *デッドロック検出 ,  順序符号化 ,  有界モデル検査

分類 (1件)： グラフ理論基礎  (IA02020S)

引用文献 (27件)：

• 番原睦則,鍋島英知:SAT 技術の進化,情報処理,Vol.57, No.8, pp.704-709 (2016).
• 番原睦則,田村直之:SAT によるシステム検証,人工知能学会誌,Vol.25, No.1, pp.122-129 (2010).
• Biere, A.: Bounded Model Checking, Handbook of Satisfiability, pp.457-481, IOS Press (2009).
• Biere, A., Cimatti, A., Clarke, E.M. and Zhu, Y.: Symbolic Model Checking without BDDs, Proc. 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 1999 ), LNCS, Vol.1579, pp.193-207 (1999).
• Eén, N. and Sörensson, N.: Temporal Induction by Incremental SAT Solving, Electronic Notes in Theoretical Computer Science, Vol.89, No.4 (2003).

タイトルに関連する用語 (5件)： SAT ,  ペトリネット ,  デッドロック検出 ,  手法 ,  提案