Kleisli Simulation for Real-Weighted
Automata and its Algorithm

卜部 夏木 （蓮尾研究室）
1

Overview●

Simulation●

Kleisli Simulation●

Contribution
1. Implementation
2. Increasing the Chance of Simulation●

Experimental Results and Comparison

2Overview●

Simulation●

Kleisli Simulation●

Contribution
1. Implementation
2. Increasing the Chance of Simulation●

Experimental Results and Comparison

3Motivation●●

並列システムの形式検証
定量的な性質
例：確率・空間・時間…

4

並列システムの形式検証
ここでの方法・・・

●

Imple

Spec

システムのオートマトン

仕様のオートマトン

システムの「ふるまい」が仕様の「ふるまい」に「含まれる」かどうか調べる5

Trace Semantics
Trace semantics = 線形時間の全体的なふるまい●

非決定性オートマトン●

確率的オートマトン

6

Trace Semantics
Trace semantics = 線形時間の全体的なふるまい●

非決定性オートマトン●

確率的オートマトン

7

Trace Semantics
Trace semantics = 線形時間の全体的なふるまい●

非決定性オートマトン●

確率的オートマトン

8

Trace Inclusion●

Trace inclusion= trace semantics 間の包含関係

9Trace Inclusion●

Trace inclusion= trace semantics 間の包含関係●

非決定性オートマトン → 集合の包含関係

Imple

Spec

10

Trace Inclusion●

Trace inclusion= trace semantics 間の包含関係●

確率的オートマトン → 文字列毎の確率

Imple

Spec

11

Trace Inclusion●

Trace inclusion= trace semantics 間の包含関係●

確率的オートマトン → 文字列毎の確率

Imple

Spec

12

Trace Inclusion●

Trace inclusion= trace semantics 間の包含関係●

確率的オートマトン → 文字列毎の確率

Imple

Spec

13

Trace Inclusion●

Trace inclusion= trace semantics 間の包含関係●

確率的オートマトン → 文字列毎の確率

Imple

Spec

14

目標
●

Trace inclusion を調べたい●

Trace semantics は普通は無限

15

目標
●

Trace inclusion を調べたい●

Trace semantics は普通は無限自動で調べることは難しい
16

Simulation = Stepwise Trace Inclusion●

全体の trace inclusion を調べる代わりにstepwise な trace inclusion を調べる

17

Simulation = Stepwise Trace Inclusion●

全体の trace inclusion を調べる代わりにstepwise な trace inclusion を調べるSimulation

18

Simulation = Stepwise Trace Inclusion●

全体の trace inclusion を調べる代わりにstepwise な trace inclusion を調べる
Simulation
ABs.t.
aa

AからBへのsimulationが存在 19

Simulation
A から B への simulation が存在
A の trace は B の trace に含まれる (trace inclusion)

20

Simulation
A から B への simulation が存在
A の trace は B の trace に含まれる (trace inclusion)

健全性
21Simulation
A から B への simulation が存在
A の trace は B の trace に含まれる (trace inclusion)

健全性
完全性は必ずしも成り立たない22

Overview●Simulation●

Kleisli Simulation●Contribution
1. Implementation
2. Increasing the Chance of Simulation●

Experimental Results and Comparison

23

Coalgebra●State-based な遷移系の圏論的な理論– 例えば並列システム●Jacobs, Rutten, Reichel in 90's

24

Kleisli 圏●

圏 C とモナド T の Kleisli 圏 Kl(T)- 対象 ： Obj (C)-射: f : X → Y in Kl(T) isf : X → TY in C25

Kleisli 圏●

Kleisli 圏で様々なシステムを表現できる●

モナド T ごとに様々なシステム
例：Powerset monad→

非決定性オートマトン
Subdistribution monad→

確率的オートマトン
26

Trace Semantics via Coinduction(Hasuo, Jacobs, and Sokolova, 2006)●Kleisli 圏を用いたtrace semantics の一般的な定義●

様々な遷移系に trace semantics を定義できる

Final Coalgebra

27

Kleisli Simulation （Hasuo, 2006）●

Kleisli 圏を用いたsimulation の一般的な定義●

様々な遷移系に simulation (Kleisli simulation)を定義できる●Forward

Backward28

確率的オートマトンの Kleisli Simulation
定義：

A からB への forward simulation とは f : B → DA s.t.

A

B
y0

1x0a, 2/3a, 1/32/3x1x2b, 1b, 1x3y1

線形不等式(Hasuo, 2010)

a, 1

1/3
1y2b, 129

確率的オートマトンの Kleisli Simulation
定義：
A からB への backward simulation とは b : A → DB s.t.

A

By0

1x0a, 2/3a, 1/3y1

1x1x2b, 1b, 1x3

線形不等式(Hasuo, 2010)a, 1

11y2b, 130

確率的オートマトンのKleisli Simulation●

確率的オートマトンの trace inclusion は決定不能 (Blondel & Canterni, 2003)(Hasuo, 2006)
31

確率的オートマトンのKleisli Simulation●

確率的オートマトンの trace inclusion は決定不能 (Blondel & Canterni, 2003)(Hasuo, 2006)32

Overview●

Simulation●

Kleisli Simulation●

Contribution
1. Implementation
2. Increasing the Chance of Simulation●

Experimental Results and Comparison

33

Contributions
1. 線形不等式を解くことで確率的オートマトンのKleisli simulation を調べるプログラムを実装

34

Contributions
2. Kleisli simulation を存在しやすくする工夫- 確率 → 実数- オートマトンの変形(Hasuo, 2006)35

確率 → 実数重みA

By0

1x0a, 2/3a, 1/32/3

x1x2b, 1b, 1y1a, 1

1/3
1y2b, 1x3●

確率的オートマトンのKleisli sim. は確率分布 [0,1]36確率 → 実数重み
A

B

y0

1x0a, 2/3a, 1/32/3

x1x2b, 1b, 1y1a, 11/3
1y2b, 1x3●

確率的オートマトンのKleisli sim. は確率分布 [0,1]実数分布 [0, ∞) に拡張
37確率 → 実数重みA

By0

1x0a, 2/3a, 1/32/3x1x2b, 1b, 1y1a, 11/3
1y2b, 1x3●

確率的オートマトンのKleisli sim. は確率分布 [0,1]実数分布 [0, ∞) に拡張●

モナド：D → M
システム：確率的オートマトン→重み付きオートマトン38

確率 → 実数重み●

新しく Kleisli simulation が見つかることがある

39

確率 → 実数重み●

新しく Kleisli simulation が見つかることがある

1241

オートマトンの変形●

オートマトンを変形し 、Kleisli simulation を存在しやすく

42

4種の変形
Split Backward

Merge Backward

Split Forward

Merge Forward43

変形の性質●変形は Kleisli simulation の健全性を保つ●

変形は既存の Kleisli simulation を壊さない

44

変形の性質●

これ以上変形できないオートマトンの間のKleisli simulation は完全●

普通は無限回変形できる45

変形の性質●

確率的オートマトンのtrace inclusion は半決定不能

46(Hasuo, 2006)

変形の性質●

確率的オートマトンのtrace inclusion は半決定不能●

何度変形してもKleisli simulationが存在するようにならないことがある

47(Hasuo, 2006)

Overview●

Simulation●

Kleisli Simulation●

Contribution
1. Implementation
2. Increasing the Chance of Simulation●

Experimental Results and Comparison

48

実装
●

Kleisli simulation を探すプログラム- 線形計画問題ソルバを用いて線形不等式を解く- glpk- 単体法●

オートマトンを変形するプログラム

49

実験結果
●

Grade protocol の正しさの検証●

オートマトンの等価性を調べることで検証できる(Kiefer et al. 2011)●Space consuming●

Kieferらの実装より遅い–

Trace inclusionはtrace equivalenceより難しい

50

実験結果
●

Crowds protocol の probable innocence の検証●

Trace inclusion を調べることで検証できる (Hasuo, Kawabe, Sakurada, 2010)●

変形が必要になる場合が発生→変形・探索を繰り返す●

Backward simulation is faster51

他のSimulationとの比較(Hasuo, 2006)(Hughes & Jacobs,2004)
52

他のSimulationとの比較(Hasuo, 2010)(Hasuo, 2006)(Hughes & Jacobs,2004)
53

他のSimulationとの比較(Hasuo, 2010)(Hasuo, 2006)(Hughes & Jacobs,2004)
54

まとめ
●

Kleisli simulationを探すプログラムを実装●

Simulation を存在しやすくする工夫

Future Work●

オートマトンの変形を圏論的に●他のシステムに対するKleisli simulationの実装

55