日本ソフトウェア科学会第 33 回大会 (2016 年度) 講演論文集

SAT 技術を用いた正規ペトリネットのデッドロック検出手法の提案
寸田 智也

宋 剛秀

番原 睦則

田村 直之

本論文では，SAT 技術を用いた正規ペトリネット (各プレイスのトークン数が整数値，アークの多重度が 1) のデッ
ドロック検出について述べる．与えられたペトリネットは整数上の制約充足問題として表現され，順序符号化法を用いて SAT 問題に変換される．また，デッドロックの検出には有界モデル検査の手法を用いる．ペトリネットの制約モデルとしては，まず基本モデルを提案し，次にトークン数の変化量に制限を加えた制限モデルと，多重発火を可能にした多重発火モデルを提案する．制限モデルは，基本モデルに比べデッドロック検出までの遷移回数が多くなる
が，より少ない節数で表現することができる．一方，多重発火モデルは，基本モデルに比べ節数が多くなるが，より少ない遷移回数でデッドロックを検出できる．これら 3 種類の制約モデルに関し，Model Checking Contest 2015
デッドロック検出部門の問題を用いて提案手法を評価した．既存のツールがいずれもデッドロック検出に失敗した問題でデッドロックを検出でき，提案手法の有効性が示せた．

られるようになった．SAT ソルバーでは，直接的に

1 はじめには整数変数を扱うことができないため，既存の SAT

C. A. Petri によって提唱されたペトリネットは，型ペトリネット検証手法の多くは，各プレイスのトー

コンピュータ・通信システムなどの並行的，非同期クン数が 1 以下の安全ペトリネットのみを対象にし的，分散的，非決定的，確率的な動作をする一般的なている [12] [14]．

情報・制御システムの記述・設計・解析・検証に有用である [13]．

そこで本論文では，順序符号化 [17] を用いて整数上の制約を SAT 符号化することで，各プレイスのトー命題論理式の充足可能性判定 (SAT) は，与えられクン数が整数値となる正規ペトリネットのデッドロッ

た命題論理式が真になる値割り当てが存在するかど

ク検出を行う．順序符号化は，整数変数上の制約充足うかを判定する問題である [7]．この SAT を解くアル問題を SAT 問題に符号化する手法の 1 つで，多くのゴリズムおよびそれを実装したソルバーに関して，半問題に対してよい性能を示している．

世紀前からこれまでに膨大な研究がなされており，近デッドロック検出には有界モデル検査の手法を用い

年，SAT ソルバーの性能は飛躍的に向上した．それる [1] [2] [3]．有界モデル検査では，動的なシステムにを受けて，SAT ソルバーはさまざまな分野に応用さついて，遷移長 k の状態遷移と検証すべき性質を命れるようになっており，ペトリネットの検証にも用い題論理式で表し，その命題論理式を SAT ソルバーで検証する．この手法でデッドロックを効率的に検出す

Proposal of a SAT-based Method to Detect Deadlocksof Ordinary Petri Nets.
Tomoya Sunda, 神戸大学大学院システム情報学研究
科, Graduate School of System Informatics, Kobe
University.
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.

るために考慮すべき点として，SAT 問題として表した場合の節数と検証する遷移長 k の長さがある．そこで本論文では，ペトリネットを制約充足問題として定式化した制約モデルを 3 種類提案し比較する．最
初に基本モデルを提案し，次に節数を抑えるように基本モデルを改良した制限モデルと，遷移長 k を抑えるように基本モデルを改良した多重発火モデルを提2. 2 SAT 符号化

案する．制限モデルは，基本モデルにトークン数の変与えられた制約式をすべて満たすことができるよ

化量に制限を加えた制約モデルである．多重発火モデ

うな変数の値の割当てを決定する問題を, 制約充足

ルは，基本モデルに多重発火を可能にした制約モデル

問題 (Constraint Satisfaction Problem; CSP) といである．

う．SAT 型制約ソルバーは与えられた制約充足問題

以下，2 節では，SAT と SAT 型制約ソルバーについて説明する．3 節では，ペトリネット，およびそのデッドロック検出，Model Checking Contest について説明する．4 節では，ペトリネットの 3 つの制を SAT に符号化し，SAT ソルバーを用いて与えられた制約充足問題の解を求めるシステムである．
制約充足問題から SAT への符号化法には以下のよ
うなものがある．

約モデルと，デッドロック状態の制約式，デッドロッ• 直接符号化法 [4] [18]クの探索手法について説明する．5 節では，Model• 支持符号化法 [6] [9]Checking Contest 2015 デッドロック検出部門の問題• 対数符号化法 [5] [8]を用いて，3 種類の制約モデルの特徴を比較する．ま• 順序符号化法 [17]た，既存手法との比較を行う．既存のツールがいずれ中でも順序符号化法はショップ・スケジューリング問

もデッドロック検出に失敗した問題でデッドロックを

題および２次元ストリップパッキング問題で未知だっ検出でき，提案手法の有効性が示せた．最後に，6 節

た最適値決定に成功する等，有望な手法であることがで結論をまとめる．

示されている [16] [15]．

2 SAT と SAT 符号化

3 ペトリネットのデッドロック検出

2. 1 SAT

本節では，正規ペトリネットとデッドロックについ充 足 可 能 性 判 定 (Satisfiability testing problem;て説明する．また，ペトリネットの検証のコンテスト

SAT) 問 題 と は ，与 え ら れ た 命 題 論 理 式 を 真 に すである Model Checking Contest や，既存の SAT 型

るような命題変数の値割り当てが存在するかどうか

ペトリネット検証手法について述べる．

を判定する問題である [7]．与えられた命題論理式を真にするような値割り当てが存在する場合，命題論理

3. 1 ペトリネット

式は充足可能 (SAT) であるといい，一方命題論理式

正規ペトリネットは，トークン数が整数値，アークのを真とする値割り当てが存在しないとき，充足不能多重度が 1 のペトリネットであり，組 (P, T, A, M0 )(UNSAT) であるという．

で表される．ここで，P = {p1 , p2 , ..., pm } はプレ

SAT 問題を解くソルバーは SAT ソルバーと呼ばイスの集合，T = {t1 , t2 , ..., tn } はトランジション

れる．SAT ソルバーは連言標準形 (CNF) の命題論理の集合，A ⊆ (P × T) ∪ (T × P) はアークの集合，

式を受け取って，SAT か UNSAT かを判定する．近年

M0 : P → N は初期マーキングである．また，•p はの SAT ソルバーは求解過程で発生する矛盾から得ら

プレイス p の入力トランジションの集合を表し，p•れる学習節を利用し，解を探索する CDCL アルゴリ

はプレイス p の出力トランジションの集合を表す．同ズムなどの高速化技術が取り入れられており，その性様に，•t はトランジション t の入力プレイスの集合，能は飛躍的に向上している [10]．これに伴い，与えらt• はトランジション t の出力プレイスの集合を表す．

れた問題を SAT 問題に変換し，SAT ソルバーを用い

ペトリネットの状態はマーキング M : P → N でて求解する SAT 型手法が用いられるようになってお表される．また，常に M : P → {0, 1} となるペトリ

り，システム検証にも用いられている [1]．

ネットを安全ペトリネットという．図 1 にペトリネッ
トの例を示す．

State Space generation では，初期状態から到達可能な状態数やトランジションの発火回数，各プレイスのトークン数の最大値，各マーキングのトークン数の最大値を求める．Reachability analysis では初期マーキングから，与えられた条件を満たすような状態に到達できるかどうかを検証する．LTL (CTL) analysis
では，LTL (CTL) の形式で与えられた性質をペトリ
ネットが満たすかどうかを検証する．
図1

ペトリネットの例

この例は，P = {p1 , p2 , p3 , p4 }，T = {t1 , t2 }，M0 (p1 ) = 2 M0 (p2 ) = 3

M0 (p3 ) = 0

M0 (p4 ) = 0となる．

3. 2 デッドロック検出あるマーキングにおいて，トランジション t のすべての入力プレイスがトークンを持つとき，トランジ
ション t は発火可能になる．
ペトリネットにおけるデッドロックとは，すべてのトランジションが発火不可能である状態を言う．
つまり，すべてのトランジション t ∈ T について，

M (p) = 0 となるプレイス p ∈ •t が存在することを言う．
あるペトリネット PN でデッドロックが検出できるとは，PN がデッドロック状態になるような発火系列が存在することを言う．

また，これらの部門はさらに細かいいくつかのサブカテゴリーに分かれる．Reachability analysis 部門
は以下のサブカテゴリーからなる．

• ReachabilityComputeBounds• ReachabilityBounds• ReachabilityCardinality• ReachabilityFireability• ReachabilityFireabilitySimple• ReachabilityDeadlock
ReachabilityComputeBounds では，各プレイスのトークン数の上限に関する制約を満たすかどうかを調べる．ReachabilityBounds では，プレイスのトークン数が有界であるかどうかを調べる．Reachability-

Cardinality では，プレイスのトークン数に関する制
約が常に成り立つ，または成り立つ可能性があるかどうかを調べる．ReachabilityFireability では，トランジションの発火に関する制約が常に成り立つ，または成り立つ可能性があるかどうかを調べる．Reachabili-

tyFireabilitySimple では，あるトランジションが常に発火する，または発火する可能性があるかどうかを調

3. 3 Model Checking Contest
Model Checking Contest †1 は同期システムの検べる．本論文では，このうち，ReachabilityDeadlock
での評価を行う．

証ツールの評価を行うコンテストである．同期シス
テムのモデルはすべてペトリネットとして与えられる．Model Checking Contest は以下の 4 つの部門からなる．

1. State Space generation
2. Reachability analysis
3. LTL analysis
4. CTL analysis

4 提案手法
本節では，ペトリネットのデッドロック検出の提案
手法について述べる．提案手法は，正規ペトリネット

PN(P, T, A, M0 ) を入力とし，デッドロックが見つかれば処理を終了する半決定的手続きである．
提案手法では，有界モデル検査 [1] [2] [3] の手法を用いて，与えられたペトリネットのデッドロックを検出する．あるトークン数の上限 N と，遷移長 k の中で，†1 Model Checking Contest http://mcc.lip6.fr/

正規ペトリネット PN が初期状態からデッドロック

状態に到達するという条件を制約充足問題として表し，それを順序符号化を用いて SAT 問題に変換したに等しい．このことを表す以下の制約を加える．
∑ i
αpi =
ft
(p ∈ P, 0 ≤ i < k)

∑

t∈p•

後，SAT ソルバーで求解する．SAT ソルバーが SAT

βpi =を返した場合，与えられたペトリネットのトークン数(p ∈ P, 0 ≤ i < k)

fti

(4)

t∈•p

の上限 N と，デッドロックを探索する遷移回数 k の中で，デッドロック状態に到達する発火系列があるこステップ i から i + 1 への遷移で p から減るトークとを示す．UNSAT を返した場合，N , k の上限の中でン数は，ステップ i での p のトークン数以下である必は，デッドロックを検出できないことを表す．このと要があるので，以下の制約を加える．

αip ≤ mip

き，N , k の値を増加させた SAT 問題を生成し，再(p ∈ P, 0 ≤ i < k)(5)

び SAT ソルバーで求解する．一般的には N と k を共に増加させるべきだが，多くのペトリネットでは
トークン数が有限個となるため，後述する本論文での実装は k のみを増加させている．

ステップ i からステップ i + 1 への遷移があるとき，すべてのプレイス p に対して，以下が成り立つ．

1. ステップ i で発火した p の出力トランジション
数は，p から減るトークン数と等しい．

4. 1 正規ペトリネットの制約モデル

2. ステップ i で発火した p の入力トランジション

あるトークン数の上限 N と，遷移長 k の中で，正規ペトリネット PN が初期状態からデッドロック状態に到達することを表す制約モデルについて説明する．
まず，基本モデルについて説明し，次にトークン数

数は，p で増えるトークン数と等しい．
したがって，ペトリネット PN が初期マーキングから k 回状態遷移することは，以下の制約で表される．

∧の変化量に制限を加えた制限モデルと，多重発火を可p∈P能にした多重発火モデルについて説明する．

(mip = M0 (p)) ∧

k−1
∧ ∧

(mi+1
= mip − αip + βpi )p

i=0 p∈P(6)

4. 1. 1 基本モデル
ステップ i でのペトリネットの状態はマーキングで表される．ステップ i でのプレイス p のトークン数を表す変数 mip を導入する．

mip ∈ {0..N }(p ∈ P, 0 ≤ i ≤ k)(1)

また，ステップ i でトランジション t が発火することを表す変数 fti を導入する．

fti ∈ {0, 1}(t ∈ T, 0 ≤ i < k)例として，図 1 のペトリネットに対応する制約モデ
ルを示す．N = 3, k = 1 での制約モデルは以下のようになる．
(m0p1 = 2) ∧ (m0p2 = 3) ∧ (m0p3 = 0) ∧ (m0p4 = 0)

∧ (α0p1 = ft01 ) ∧ (αp02 = ft01 + ft02 )∧ (α0p3 = 0) ∧ (αp04 = 0)(2)

ステップ i で，プレイス p の出力トランジションのう∧ (βp01 = 0) ∧ (βp02 = 0)
∧ (βp03 = ft01 ) ∧ (βp04 = ft02 )ち発火するトランジション数を表す変数 αip と，入力

∧ (α0p1 ≤ m0p1 ) ∧ (αp02 ≤ m0p2 )トランジションのうち発火するトランジション数を表∧ (α0p3 ≤ m0p3 ) ∧ (αp04 ≤ m0p4 )す βpi を導入する．

∧ (m1p1 = m0p1 − αp01 + βp01 )αpi ∈ {0..|p • |}(p ∈ P, 0 ≤ i < k)βpi ∈ {0..| • p|}(p ∈ P, 0 ≤ i < k)(3)

∧ (m1p2 = m0p2 − αp02 + βp02 )∧ (m1p3 = m0p3 − αp03 + βp03 )∧ (m1p4 = m0p4 − αp04 + βp04 )(7)

これらの元で制約モデルを考える．

fti

プレイス p の発火する出力トランジション数 αpi は，

図 1 のペトリネットの基本モデルでのデッドロッ(t ∈ p•) の和に等しい．また，プレイス p の発火ク状態までの状態遷移は，図 2 の実線または点線(t ∈ •p) の和で表した遷移が許される．この制約モデルでは，多する入力トランジション数 βpi も，fti

図2

各制約モデルでの状態遷移

重発火ができないため，二重線で表した遷移 (トラ表1

各制約モデルでの SAT 問題の節数

ンジション t1 が 2 回発火) はできない．すなわち，

制約モデル

節数

Mo → M1 → M2 → M3 あるいは M0 → M2 → M3

基本モデル

O(|A| · N + |P| · N 2 )の遷移が許される．したがって，k = 2 でデッドロッ

制限モデル

O(|A| + |P| · N )クを検出できるが，k = 1 では検出できない．

多重発火モデルO(|A| · N 2 + |P| · N 2 )4. 1. 2 制限モデル
制限モデルでは，各プレイスのトークン数の変化量
を 1 個以内に制限する．制限モデルは，基本モデルに，以下の制約を加えることで表せる．

αpi ≤ 1(p ∈ P, 0 ≤ i < k)(8)

ことで表せる．

fti ∈ {0..N }(t ∈ T, 0 ≤ i < k)(2′ )多重発火を許したことにより，デッドロック状態に到達するまでの遷移長 k は少なく済む可能性がある．

制限モデルは，基本モデルに比べて一度の遷移で発

図 1 のペトリネットの制限モデルでのデッドロック状

火できるトランジションが限られる．そのため，デッド態までの状態遷移は，図 2 の実線または点線またはロック状態に到達するには，基本モデルより長い遷移

二重線で表した遷移が許される．この制約モデルで長 k が必要となる場合がある．例えば，図 1 のペトリ

は，多重発火を許したことにより，t1 が一度の遷移

ネットの制限モデルでのデッドロック状態までの状態

で 2 回発火することができる．すなわち，基本モデ

遷移は，図 2 の点線で表した遷移のみが許される．こルでの遷移に加えて，M0 → M3 の遷移が許される．

の制約モデルでは，各プレイスのトークン数の変化量

したがって，k = 1 でデッドロックを検出できる．

が 1 以下に制限しているため，実線や二重線で表した

各制約モデルを制約充足問題として表し，順序符号遷移はできない．すなわち，M0 → M1 → M2 → M3化を用いて SAT 問題に変換した時の節数を表 1 に示の遷移のみが許される．したがって，k = 3 でデッドす． 表 1 での節数は，各ステップごとの節数である．

ロックを検出できるが，k = 2 では検出できない．

同じ遷移長 k での節数では，制限モデルが最も少な

4. 1. 3 多重発火モデル

くなり，多重発火モデルが最も多くなる．

多重発火モデルでは，トランジションの多重発火を許す．多重発火とは，一つのトランジションが同時に

4. 2 デッドロック状態の制約モデル

複数回発火することである． 多重発火モデルは，基i ステップ目でデッドロック状態となる条件は以下

本モデルの変数 fti のドメインを 0 ≤ fti ≤ N にする

表2

各制約モデルに対応する式

Algorithm 1 デッドロック検出手続き

制約モデル

対応する制約式

基本モデル(1)-(6), (10)

入力: ペトリネット PN，トークン数の上限 N
1: k = 1

制限モデル(1)-(6), (8), (10)2: loop

多重発火モデル(1), (3)-(6), (2′ ), (10)3:

ψ = ϕk (PN, N ) を順序符号化した CNF 式

4:if ψ が充足可能 thenのように表せる．

∧ ∨5:(mip = 0)(9)t∈T p∈•t

この条件は，すべてのトランジションが発火不可能，
すなわち，トークンを持たない入力プレイスが存在す

break /* デッドロック検出 */6:

end if7:

k = next(k)8: end loop

ることを表している．
この条件を用い，k 回以内の遷移でデッドロック状

まず，k = 1 と与えられた PN と N に対する制約態に到達する発火系列があることを表す制約を与え式 ϕk (PN, N ) を生成し，それを順序符号化を用いてる．i 回以内の遷移でデッドロック状態に到達する発SAT 問題 ψ に変換する．その ψ を SAT ソルバーに

火系列があることを表す命題変数 Di を導入する．こ与え，充足可能かどうかを判定する．もし，ψ が充足のとき，k 回以内の遷移でデッドロック状態に到達す

可能ならば，k ，N のなかでデッドロックが検出できる制約は以下のように表すことができる．
∧ ∨
(D0 →
(m0p = 0))

たとして，この手続きを終了する．もし，ψ が充足不能ならば，k ，N のなかではデッドロックを検出できt∈T p∈•t∧k∧{Di → (Di−1 ∨

i=1

∧ ∨

なかったので，k の値を増加させ，再度同様の処理を(mip = 0))}(10)t∈T p∈•t∧Dk
4. 3 デッドロックの探索手法
有界モデル検査の手法を用いて，与えられたペト行う．ここで，next(k) は次にデッドロックを探索すべき遷移長を返す関数である．なお，実装では N の値は初期状態のマーキングにおける最大のトークン数とした．

next(k) の定義について，以下の 3 通りを考えた．

リネットのデッドロックを検出する．Algorithm 1 に

1. next(k) = k + 1

デッドロック検出の手順を示す．ϕk (PN, N ) は，ペト

2. next(k) = 1.5k

リネット PN が各プレイスのトークン数上限 N ，遷3. next(k) = 2k

移長 k のなかでデッドロック状態となることを表す

予備実験として，この 3 通りについて実験をしたと制約式である (ϕk (PN, N ) の詳細は表 2 を参照)．

ころ，next(k) = 2k のときが最も良い結果となった．
以下では，next(k) = 2k を用いる．

5 性能評価提案手法の有効性を検証するため，Model Check-ing Contest 2015 のデッドロック検出部門の問題 267問のうち，正規ペトリネットでデッドロックがあることが分かっている問題 83 問を用いて性能評価を行った．ベンチマークは Ubuntu 14.04 (Xeon 3.5GHz,
メモリ 8GB) 上で計測した．

5. 1 提案する制約モデル 3 つの比較表5提案した 3 つの制約モデル (基本モデル，制限モ
デル，多重発火モデル) がデッドロックを検出できた問題数を表 3，4 に示す．表 3 では，各制約モデルでデッドロックを検出できた問題数と，CPU 時間の平既存手法との比較
提案

Ogata+

Cunf

LoLA2

安全 (52 問)

40

44

27

47

安全でない (31 問)

29

—

—

30

合計 (83 問)

69

44

27

77

均を N の値ごとに示す．表 3 での CPU 時間の平均は，時間内に解けなかった問題の CPU 時間を 600 秒(Ogata+) [12] の 手 法 と Cunf [14]，そ し て ，Modelとして計算した平均である．表 4 では，各制約モデ

Checking Contest 2015 デッドロック検出部門で優勝

ルでデッドロックを検出できた問題数と，デッドロッ

したツール LoLA2 [11] を用いた．提案手法と既存手ク検出に必要な遷移長 k の平均を N の値ごとに示す．

法で，デッドロックを検出できた問題数を比較した

なお， 表 4 の k の平均値は，デッドロックを検出で結果を表 5 に示す．提案手法は LoLA2 がデッドロッ

きた問題のみに対する平均値である．

クを検出できなかった問題 2 問 (Angiogenesis-PT-

まず，基本モデルと制限モデルについて比較する．

50, Philosophers-PT-010000) のデッドロック検出に

表 3 を見ると，N = 11 ∼ 20，N = 21 ∼ 49 では基成功した．このうち Angiogenesis-PT-50 は Model

本モデルがデッドロックを検出できなかった問題を 1

Checking Contest 2015 に参加したいずれのツール

問ずつ制限モデルで検出している．この理由について

もデッドロックを検出できなかった問題である．表はまだ考察が必要であるが，デッドロック検出に必要

6 は Angiogenesis-PT での提案手法と LoLA2 の結果な遷移長が同程度の時は制限モデルの方がよい性能(CPU 時間と使用メモリサイズ) を示す．

を示す可能性がある．

Angiogenesis-PT-50 は初期状態から到達可能な状

次に，多重発火モデルと他の制約モデルについて態数が非常に多い問題である．LoLA2 では被覆グラ比較する．表 3 を見ると，N が大きくなるにつれて，フを用いてデッドロックに到達するかどうかを調べて多重発火モデルが他の制約モデルより短い CPU 時間

いるが，Angiogenesis-PT-50 では状態数多いためメでデッドロックを検出できている．特に，N ≥ 50 のモリーオーバーを起こしている．一方，SAT 型検証

問題では，多重発火モデルのみがデッドロックを検出手法では，他の方法に比べ状態空間爆発が起こりにくできている．表 4 を見ると，基本モデルや制限モデル

いという特徴があり，Angiogenesis-PT-50 のデッド

では，N が大きくなるにつれ，デッドロック検出に

ロック検出に成功している．

必要な遷移長 k が大きくなっているが，多重発火モ
デルでは N が大きくなっても比較的小さい k でデッ

6 まとめと今後の課題

ドロックを検出できており，それが CPU 時間の短縮

本論文では，SAT 技術を用いて，正規ペトリネッにつながっている．多重発火モデルは各ステップでのトのデッドロック検出を行った．正規ペトリネットの節数は最も多くなるが，k が短いことで UNSAT の判

3 つの制約モデル，基本モデル，制限モデル，多重発定回数が少なくて済むことが理由と考えられる．

火モデルを提案し，実験により，それぞれの特徴を確

本実験では多重発火モデルが最もよい性能を示した

かめた．制限モデルは，他 2 つの制約モデルに比べ，が，多重発火が起こりにくいようなペトリネットの場

少ない節数で表現できるため，大きなサイズのペト

合，制限モデルの方がよい性能を示す可能性がある．

リネットに対して有効であることが確かめられた．一方，多重発火モデルは，他 2 つの制約モデルに比べ，5. 2 既存手法との比較

一度の遷移でプレイス中のトークン数を大きく変化

提案手法 (多重発火モデル) と既存手法を比較すできるため，トークン数の上限が大きい問題に対し，る．比較に用いる既存手法としては，SAT 型検証手法

より少ない遷移回数でデッドロックを検出できることである SAT-based Verification of Safe Petri Nets

が確かめられた．

表3

各制約モデルで検出できた問題数と CPU 時間の平均値検出できた問題数N

CPU 時間の平均 (秒)

基本モデル

制限モデル

多重発火モデル

基本モデル

制限モデル

多重発火モデル

1

(54)

41

41

41

62.99

55.50

63.35

2〜5

(8)

8

8

8

6.15

8.38

5.87

6〜10

(6)

6

6

6

19.24

60.75

19.98

11〜20

(6)

5

6

6

119.32

69.89

15.20

21〜49

(4)

3

4

4

154.76

30.00

15.86

50〜500

(5)

0

0

4

—

—

153.59

合計

(83)

63

65

69

93.95

81.83

51.21

表4

各制約モデルで検出できた問題数と k の平均値検出できた問題数

N

k の平均

基本モデル

制限モデル

多重発火モデル

基本モデル

制限モデル

多重発火モデル

1

(54)

41

41

41

11.7

11.7

11.7

2〜5

(8)

8

8

8

8.3

10.0

8.3

6〜10

(6)

6

6

6

13.0

20.0

7.3

11〜20

(6)

5

6

6

14.0

24.0

9.0

21〜49

(4)

3

4

4

4.7

26.0

7.5

50〜500

(5)

0

0

4

—

—

16.0

合計

(83)

63

65

69

11.17

14.25

10.67

表6

Angiogenesis-PT での比較

提案手法

LoLA2

instanceN

CPU 時間メモリ

CPU 時間メモリ

Angiogenesis-PT-10

10

11.37

4979764

1.90

176952

Angiogenesis-PT-15

15

18.94

498674815.86

1020700

Angiogenesis-PT-20

20

15.38

5094012165.397925784

Angiogenesis-PT-25

25

22.21

509292066.433703676

Angiogenesis-PT-50

50

178.925115492

M.O.

M.O.

既存手法との比較では，SAT 型検証手法である

デルを組み合わせたデッドロックの探索手法が挙げら

SAT-based Verification of Safe Petri Nets の手法とれる．また，P/T ネット (アークの多重度が整数値)

Cunf ，そして，Model Checking Contest 2015 デッのペトリネットでのデッドロック検出や，デッドロッ

ドロック検出部門で優勝したツール LoLA2 と比較しク検出よりも一般的な性質の検証である，LTL 式でた．デッドロックを検出できた問題数では LoLA2 が表された性質の検証が挙げられる．

最も良い結果となったが，既存手法がいずれもデッド
ロックを検出できなかった問題でのデッドロック検出

参 考 文 献に成功した．

[ 1 ] 番原睦則, 田村直之: SAT によるシステム検証, 人
工知能学会誌, Vol. 25, No. 1(2010), pp. 122–129.

今後の研究課題としては，制限モデルと多重発火モ

[ 2 ] Biere, A.: Bounded Model Checking, Handbookof Satisfiability, IOS Press, 2009, pp. 457–481.
[ 3 ] Biere, A., Cimatti, A., Clarke, E. M., and Zhu,
Y.: Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on
Tools and Algorithms for Construction and Analysis of Systems (TACAS 1999), LNCS 1579, 1999,
pp. 193–207.
[ 4 ] de Kleer, J.: A Comparison of ATMS and CSP
Techniques, Proceedings of the 11th International
Joint Conference on Artificial Intelligence (IJCAI1989), 1989, pp. 290–296.
[ 5 ] Gelder, A. V.: Another Look at Graph Coloring via Propositional Satisfiability, Discrete Applied
Mathematics, Vol. 156, No. 2(2008), pp. 230–243.
[ 6 ] Gent, I. P.: Arc Consistency in SAT, Proceedings of the 15th European Conference on Artificial
Intelligence (ECAI 2002), 2002, pp. 121–125.
[ 7 ] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知能学会誌, Vol. 25(2010), pp. 57–67.
[ 8 ] Iwama, K. and Miyazaki, S.: SAT-Variable
Complexity of Hard Combinatorial Problems,Proceedings of the IFIP 13th World Computer
Congress, 1994, pp. 253–258.
[ 9 ] Kasif, S.: On the Parallel Complexity of Discrete
Relaxation in Constraint Satisfaction Networks, Artificial Intelligence, Vol. 45, No. 3(1990), pp. 275–
286.
[10] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 68–76.
[11] Niewiadomski, A. and Wolf, K.: LoLA as Abstract Planning Engine of PlanICS, Proceedingsof the International Workshop on Petri Nets andSoftware Engineering, Tunis, Tunisia, June 23-24,
2014., 2014, pp. 349–350.
[12] Ogata, S., Tsuchiya, T., and Kikuno, T.: SATBased Verification of Safe Petri Nets, AutomatedTechnology for Verification and Analysis: Second
International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings, 2004, pp. 79–92.
[13] 奥川峻史: ペトリネットの基礎, 共立出版, 1995.
[14] Rodrı́guez, C. and Schwoon, S.: Cunf: A Toolfor Unfolding and Verifying Petri Nets with Read
Arcs, Automated Technology for Verification andAnalysis - 11th International Symposium, ATVA
2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, 2013, pp. 492–495.
[15] Soh, T., Inoue, K., Tamura, N., Banbara, M.,
and Nabeshima, H.: A SAT-based Method for Solving the Two-dimensional Strip Packing Problem,
Fundam. Inform., Vol. 102, No. 3-4(2010), pp. 467–
487.
[16] 田村直之, 多賀明子, 番原睦則, 宋剛秀, 鍋島英知, 井上克巳: ショップ・スケジューリング問題の SAT 変換
による解法, スケジューリング・シンポジウム 2007 講
演論文集, 2007, pp. 97–102.
[17] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[18] Walsh, T.: SAT v CSP, Proceedings of the 6thInternational Conference on Principles and Practice of Constraint Programming (CP 2000), 2000,
pp. 441–456.