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

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

https://hdl.handle.net/20.500.14094/90006798

このアイテムのアクセス数:228件（2025-07-04 17:59 集計）

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
90006798 (fulltext)	pdf	387 KB	57

メタデータ

ファイル出力

メタデータID	90006798
アクセス権	open access
出版タイプ	Version of Record
タイトル	SAT技術を用いたペトリネットのデッドロック検出手法の提案
著者	寸田, 智也 ; 宋, 剛秀 ; 番原, 睦則 ; 田村, 直之 ; 井上, 克巳
著者名寸田, 智也
著者ID A0011 研究者ID 1000000625121 KUID https://kuid-rm-web.ofc.kobe-u.ac.jp/search/detail?systemId=be19a5fd36bdbe87520e17560c007669 著者名宋, 剛秀 Soh, Takehide ソウ, タケヒデ所属機関名情報基盤センター
著者ID A1730 研究者ID 1000080290774 著者名番原, 睦則 Banbara, Mutsunori バンバラ, ムツノリ所属機関名情報基盤センター
著者ID A0899 研究者ID 1000060207248 KUID https://kuid-rm-web.ofc.kobe-u.ac.jp/search/detail?systemId=64672be7ad29e33a520e17560c007669 著者名田村, 直之 Tamura, Naoyuki タムラ, ナオユキ所属機関名情報基盤センター
著者名井上, 克巳
言語	Japanese (日本語)
収録物名	情報処理学会論文誌
巻(号)	59(9)
ページ	1749-1760
出版者	情報処理学会
刊行日	2018-09-15
公開日	2020-02-27
抄録	本論文では，トークン数が整数値である一般のペトリネットを対象とし，そのデッドロック検出についてSAT 技術を用いた手法を提案する．提案手法では，非負整数値であるトークン数を表現するために順序符号化を採用することで，既存のSAT 型手法では対応できなかった一般のペトリネットでのデッドロック検出を実現した．また，既存SAT 型手法で採用されていたモデル（連続発火モデルと呼ぶ）よりも短いステップ長でデッドロック検出が可能となる多重発火モデルを提案し，性能向上を実現した．評価実験では，Model Checking Contest 2017 のベンチマーク問題を用いて，連続発火モデルと多重発火モデルを比較した．ほぼすべての問題で多重発火モデルのほうが優れていたが，特に初期マーキングのトークン数が比較的多い問題に対する効果が大きかった．また，Model Checking Contest 2017 デッドロック検出部門での優勝ソルバーLoLA および準優勝ソルバーTapaal との比較を行った．提案手法は，LoLA およびTapaal を含めたすべてのソルバーがデッドロック検出に失敗した問題での検出に成功し，提案手法の有効性が確認できた．
抄録	In this paper, we proposed 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 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, we confirmed the effectiveness of the proposed method with some instances for which all tools including LoLA and Tapaal failed to detect deadlock.
キーワード	ペトリネット
	デッドロック検出
	SAT 技術
	有界モデル検査
	Petri nets
	Deadlock detection
	SAT technologies
	Bounded model checking
カテゴリ	情報基盤センター
カテゴリ	学術雑誌論文
権利	©2018 the Information Processing Society of Japan. Notice for the use of this material:The copyright of this material is retained by the Japan Society for Software Science and Technology (JSSST). This material is published on this web site with the agreement of the JSSST. Please complywith Copyright Law of Japan if any users wish to reproduce, make derivative work, distribute or make available to the public any part or whole thereof.
権利	ここに掲載した著作物の利用に関する注意本著作物の著作権は日本ソフトウェア科学会に帰属します．本著作物は著作権者である日本ソフトウェア科学会の許可のもとに掲載するものです．ご利用に当たっては「著作権法」に従うことをお願いいたします．
関連情報	NAID 170000149759　CiNiiで表示

資源タイプ	journal article
eISSN	0387-5806　OPACで所蔵を検索　 CiNiiで学外所蔵を検索
NCID	AN00116647　OPACで所蔵を検索　 CiNiiで表示

閲覧可能ファイル

メタデータ

詳細を表示