LTL モデル検査の導入 ハイブリッド制約処理系 HyLaGI への

2015 ^{年度 修士論文}

ハイブリッド制約処理系 HyLaGI ^への LTL ^{モデル検査の導入}

提出日 : 2016 ^年 1 ^月 23 ^日 指導 : ^{上田 和紀 教授}

早稲田大学 基幹理工学研究科 情報理工・情報通信専攻

学籍番号 : 5114F097-1

若槻 祐彰

概要

若槻祐彰 ハイブリッドシステムとは，時間の経過に伴い状態が連続変化したり状態や方程式系が 離散変化したりするシステムを表す．物体の運動や組み込みシステムは，ハイブリッドシ ステムとして表現することができる．

HydLa

は，制約に基づくハイブリッドシステムモ デリング言語である．

HyLaGI

は，

HydLa

の処理系で数式処理により誤差のないシミュ レーションが可能である．また記号実行が可能でパラメーターを含むシステムを扱える．

従来の

HyLaGI

には，有界モデル検査機能があるが，常に条件式が満たされているか

どうかという安全性の判定しかできない．そこで，

HyLaGI

により求められる解軌道が時 間の経過に伴う各変数のふるまいであることを考慮し，時間に関する様相をもつ線形時相

論理

(LTL)

を用いることで，解軌道が満たすべき性質を検証することを考えた．

本研究では，

HyLaGI

への

LTL

モデル検査の導入を目的とし，状態の包含関係に着目 して活性や安全性を検証する手法を提案・実装した．提案手法では

LTL

モデル検査を 行った結果として，性質を満たさない反例か構築した状態空間を出力する．提案手法の特 徴は，状態空間中のループの発見に状態の包含を用いている点である．この包含判定と は，軌道

A

に軌道

B

が包含された場合，軌道

B

の状態は軌道

A

を計算するときにすで に計算されていることを利用し，過去の状態の繰り返しとなることを判定して状態空間で のループを発見する手法である．また非決定的なモデルでは，定性的に異なる軌道ごとに

LTL

モデル検査を行っている．

提案手法では，包含判定のために，

HydLa

プログラムを適切に抽象化する必要がある．

本研究ではさらに，これを支援するための自動抽象化機能について，予備実験を行った．

本論文では自動抽象化手法として初期値の抽象化を行い，結果として簡単な例題に関して 自動抽象化が行えることを確認できた．

abstract

Yoshiaki Wakatsuki Hybrid Systems consist of discrete behaviors and continuous behaviors. Physical phenomena and embeded systems can be described as hybrid systems. HydLa is a hybrid system modeling language based on constrants. HyLaGI is an implementation of HydLa that uses symbolic formula manipulation. This means HyLaGI is free from calculation errors. HyLaGI also allows us to deal with systems with symbolic parameters. HyLaGI featured bounded model checking but this function is very limited. Linear Temporal Logic (LTL) is a logic that has an aspect about time.

Using LTL, we can express a future property by a logical formula. Therefore we propose LTL (Linear Temporal Logic) model checking to HyLaGI.

The purpose of this study is the introduction of LTL model checking to HyLaGI. we propose a method to verify safety or liveness properties expressed by LTL formulas by checking an inclusion relation between states in a trajectory. With our new HyLaGI, we can obtain an LTL model checking result that is a counterexample of an LTL proeprty or information of state space. A feature of our method is that it uses an inclusion relation between states to detect a loop structure. This inclusion relation means that, when one state (trajectory segment) includes another state, the second state is already calculated in the calculation of first state. The trajectory after the second state is a repetition of the trajectory after the first state. In our method, we perform LTL model checking to each trajectory in a nondeterministic model.

For inclusion checking, we need to abstract a model properly. We did preliminary

experiment for automatic abstraction of programs to support this. In this preliminary

experiment, we abstracted an initial value of each variable in a hybrid system. We

could succeed in abstracting simple examples by using this method.

i

目次

第

1

章 はじめに

1

1.1

研究の背景と目的

. . . . 1

1.2

本論文の構成

. . . . 2

第

2

章 ハイブリッド制約処理系

HyLaGI

と

LTL

モデル検査

3 2.1

ハイブリッドシステム

. . . . 3

2.2

ハイブリッド制約言語

HydLa . . . . 3

2.3

ハイブリッド制約処理系

HyLaGI . . . . 4

2.4

線形時相論理

. . . . 5

2.5 LTL

モデル検査

. . . . 8

第

3

章

LTL

モデル検査の導入

9 3.1 HyLaGI

への

LTL

モデル検査の導入手法

. . . . 9

3.2

提案手法の特徴

. . . . 13

3.3

関連する研究

. . . . 19

第

4

章

LTL

モデル検査の実行結果

23 4.1

跳ねる質点

. . . . 23

4.2

センサーによる水量制御

. . . . 33

第

5

章 自動抽象化

39 5.1

初期値の自動抽象化

. . . . 39

5.2

初期値の自動抽象化のまとめ

. . . . 44

第

6

章 まとめと今後の課題

45

6.1

まとめ

. . . . 45

目次

ii 6.2

今後の課題

. . . . 45

謝辞

47

参考文献

48

学会発表

50

Appendix

ソースコードの変更概略

51

iii

図目次

2.1

床を跳ねる質点のモデル

. . . . 4

2.2

跳ねる質点のシミュレーション結果

. . . . 6

2.3

跳ねる質点のシミュレーショングラフ

. . . . 7

2.4 LTL

式の構文

. . . . 7

3.1 HyLaGI

の

LTL

モデル検査アルゴリズム

. . . . 11

3.2 LTLModelChecking

関数アルゴリズム

. . . . 12

3.3

状態同士の比較手法

. . . . 13

3.4

人工的なモデル

. . . . 14

3.5

常に

y

が

3

より小さい

([](y < 3))

から作られる性質オートマトン

. . . . 15

3.6

人工的な例題のシミュレーション結果

. . . . 16

3.7

人工的な例題の実行結果のグラフ

. . . . 17

3.8 PP3

^と

PP5

^の

yy ^′

^{平面のグラフ}

. . . . 17

3.9

常に高さ

y

が

-1

ではない

([]y ̸ = − 1)

から作られる性質オートマトン

. . 18

3.10

床に穴が空いた跳ねる質点プログラム

. . . . 18

3.11

床に穴があいた跳ねる質点の

LTL

^{モデル検査結果}

(

^一部抜粋

) . . . . 20

3.12

床に穴があいた跳ねる質点のグラフ

. . . . 21

3.13

床に穴があいた 跳ねる質点

Case1 . . . . 22

3.14

床に穴があいた 跳ねる質点

Case2 . . . . 22

3.15

床に穴があいた 跳ねる質点

Case3 . . . . 22

3.16

床に穴があいた 跳ねる質点

Case4 . . . . 22

3.17

床に穴があいた 跳ねる質点

Case5 . . . . 22

3.18

床に穴があいた 跳ねる質点

Case6 . . . . 22

3.19

床に穴があいた 跳ねる質点

Case7 . . . . 22

図目次

iv

3.20

床に穴があいた 跳ねる質点

Case8 . . . . 22

3.21

床に穴があいた跳ねる質点の

LTL

モデル検査結果

(Case1–Case8) . . . . 22

4.1

跳ねる質点のプログラム

. . . . 24

4.2

跳ね続ける性質オートマトン

. . . . 25

4.3

跳ねる質点のシミュレーション結果

. . . . 26

4.4

跳ねる質点の解軌道

. . . . 27

4.5

跳ね続ける性質のモデル検査結果

. . . . 28

4.6

常に一定の高さ

(y = 7)

より大きく跳ね上がる性質オートマトン

. . . . . 29

4.7

検証のための跳ねる質点のプログラム

. . . . 29

4.8

跳ねる質点のシミュレーション結果

(Case1

と

Case2) . . . . 30

4.9

^{跳ねる質点の運動}

Case1 . . . . 30

4.10

跳ねる質点運動

Case2 . . . . 30

4.11 Case1

のモデル検査結果

(

深さ

10

打ち切り

) . . . . 31

4.12 Case2

^{のモデル検査結果}

. . . . 31

4.13

一度跳ねた後の跳ねる質点

. . . . 32

4.14

一度跳ねた後の跳ねる質点の実行結果

. . . . 32

4.15

一度跳ねた後の跳ねる質点の

LTL

モデル検査結果

. . . . 33

4.16

センサーによる水量制御のプログラム

. . . . 34

4.17

いつか水量が満タンになる性質から作られる性質オートマトン

. . . . 34

4.18

センサーによる水量制御のグラフ

. . . . 35

4.19

いつか水量が満タンになる性質のモデル検査結果

. . . . 35

4.20

センサーを追加した水量制御のプログラム

. . . . 36

4.21

常に何度も一定の高さ

(y = 6)

の水量がたまる性質から作られる性質 オートマトン

. . . . 37

4.22

センサーを追加した水量制御のグラフ

. . . . 38

4.23

常に何度も一定の高さ

(y = 6)

の水量になる性質のモデル検査結果

. . . 38

5.1

^{跳ねる質点のモデル}

. . . . 40

5.2

跳ねる質点の各変数の初期値

. . . . 40

5.3

跳ねる質点の自動抽象化シミュレーション結果

. . . . 42

5.4

跳ねる質点のモデルの自動抽象化シミュレーション結果のグラフ

. . . . 43

1

第 1 ^章

はじめに

1.1 ^{研究の背景と目的}

ハイブリッド

(

動的

)

システム

[12]

は，時間の経過に伴い状態が連続変化したり，状態 や方程式系が離散変化したりするシステムである．ハイブリッドシステムは，物理学や制 御工学において利用可能である．物理現象をモデリングする際や制御工学においても，コ ンピュータによる離散的な制御と，実際に物理的に動作するという連続的な変化からなる ように，ハイブリッドシステムを用いることで表現できる．

ハイブリッドシステムをモデリングする宣言型言語

HydLa[19]

は，方程式や論理式に よる制約と，制約間の制約階層によってシステムを簡潔に表す事ができる．

HydLa

の数 式処理による実装として

HyLaGI[14]

が存在し，ハイブリッドシステムのシミュレーショ ン，記号実行や有界モデル検査が可能である．

従来の

HyLaGI

には，有界モデル検査機能があるが，常に条件式が満たされているかど

うかという

ASSERT

文による安全性の判定しかできない．また，この有界モデル検査機 能では，シミュレーションを行い，求められた解軌道についての検証しかできないため，

シミュレーション終了時刻以降の無限時間に関して，性質を満たしているかどうかの判定 はできない．このように，従来の

HyLaGI

の検証機能は非常に限定された機能しかない．

線形時相論理

(LTL)

は，時間に関する様相をもつ論理である．

LTL

^{式を用いることで，}

将来の出来事についての性質を論理式で表現可能である．

LTL

式で表現できる性質には，

安全性だけでなく活性といった特性が存在する．

HyLaGI

により求められる解軌道が時 間の経過に伴う各変数のふるまいであることを考慮すると，解軌道が満たすべき安全性や 活性などの性質を表現する際に

LTL

式を用いることができる．本研究では，

HyLaGI

に

LTL

モデル検査を導入することで，解軌道が満たすべき安全性や活性を検証することを

第

1

章 はじめに

2

目的とする．

また，提案手法では包含判定のために，

HydLa

プログラムを適切に抽象化する必要が

ある．

HydLa

プログラムの抽象化においては，抽象化により軌道が包含されるように，

モデルの性質や

HyLaGI

の実行結果を考慮して適切に抽象化する必要がある．そのため プログラマの抽象化を支援するための，自動抽象化機能を考察することを目的とする．

1.2 ^{本論文の構成}

第

2

章では，研究背景となるハイブリッドシステム，

HydLa

，

HyLaGI

，線形時相論理，

LTL

モデル検査に関して述べる．第

3

章では，提案手法である

HyLaGI

^で

LTL

^モデル 検査を行う手法について述べている．第

4

章では，実際にいくつかの例題に関して，実装 した

LTL

モデル検査を行う．第

5

章では，

LTL

モデル検査を支援する自動抽象化に関し て考察する．第

6

章では，本論文のまとめと今後の課題について述べている．

3

第 2 ^章

ハイブリッド制約処理系 HyLaGI ^と LTL ^{モデル検査}

本章では，研究背景となるハイブリッドシステム，ハイブリッド制約言語

HydLa

，ハ イブリッド制約処理系

HyLaGI

，線形時相論理，

LTL

モデル検査に関して説明する．

2.1 ^{ハイブリッドシステム}

まず，ハイブリッド

(

動的

)

システム

[12]

とは，離散変化と連続変化からなるシステム のことである．時間の経過により，状態が連続変化したり，状態や方程式系自体が離散変 化したりする．現実の物理的現象やコンピュータによって制御された多くのものは，ハイ ブリッドシステムとして表現できる．

2.2 ^{ハイブリッド制約言語} HydLa

HydLa[19]

は，制約に基づく宣言型のハイブリッド

(

動的

)

システムのモデリング言語

である．システムを表す微分方程式や論理式を制約という形で記述し，それら制約間に優 先順位を与えて制約階層をつくることでシステムの挙動を表現する．

図

2.1

は，床を跳ねる質点の

HydLa

プログラムとなる．このプログラムでは，質点の 位置を変数

y

で表している．また質点の運動に関する制約

INIT

，

FALL

，

BOUNCE

と それらの制約階層からなっている．これからプログラムの各行に関して詳しく説明して いく．

制約

INIT

は，質点の位置・速度の初期値を表している．まず

y = 10

^{より質点の初期}

第

2

章 ハイブリッド制約処理系

HyLaGI

と

LTL

モデル検査

4 1 INIT <=> y=10 & y’=0.

2 FALL <=> [](y’’=-10).

3 BOUNCE <=> [](y- =0 => y’=-(4/5)*y’-).

4 INIT, (FALL << BOUNCE).

図

2.1:

床を跳ねる質点のモデル

位置

y

^が

10

であると定義している．次に初期速度を定義する部分

y ^′ = 0

^{では，質点の} 位置

y

に

^′

記号がついている．この

^′

記号は変数の時間微分を表し，位置

y

の時間微分の ため

y ^′

は速度となる．そのため

1

行目の制約

INIT

は，質点の位置

y

に関する初期位置

y = 10

，初期速度

y ^′ = 0

を表す制約となる．

2

行目の制約

FALL

は，質点が重力に従って落下していくことを表す．まずこの制約に おいて

[](y ^′′ = − 10)

には

[]

記号がついている．この

[]

記号は

always

記号と言い，時刻

t ≥ 0

について成立する制約を表している．また，

y ^′′ = − 10

より質点の加速度

y ^′′

は

− 10

と定義している

(

ここでは重力加速度を

10

としている

)

．つまり，時刻

t ≥ 0

において質 点は加速度

y ^′′ = − 10

に従って，等加速度運動をすることを表す制約である．

3

行目の制約

BOUNCE

は，質点が床で跳ね返ることを表す．まずプログラムにおい て床は，

0

の位置にある．さらに制約の

y − = 0 => y ^′ = − (4/5) ∗ y ^′ −

^{は，ガード条件} つき制約となる．

y − = 0

が成立した場合に，後件の制約が有効になる．また

y − = 0

や

y ^′ = − (4/5) ∗ y ^′ −

^{には，変数}

y

，

y ^′

に

−

記号がついている部分がある．この

−

^記号は 左極限値を表している，そのためこの制約は，時刻

t ≥ 0

において質点の位置の左極限 値

y −

^{が床の位置}

0

である場合

(y − = 0)

，速度

y ^′

は速度の左極限値

y ^′ − (

直前の速度

)

の

4/5

倍の速度で跳ね返ることを表す制約となる．

最後に

4

行目は，制約階層を用いてモデルの挙動を表現している．

INIT

は

FALL

，

BOUNCE

と 等 価 で あ る と し て い る ．ま た ，

FALL

と

BOUNCE

が 矛 盾 し た 場 合

BOUNCE

を優先して採用するということが書かれている．これによって，

y − = 0

でな

いときは質点は落下していき，

y − = 0

の場合は

BOUNCE

が優先され，質点が跳ね返る．

2.3 ハイブリッド制約処理系 HyLaGI

HyLaGI[14]

は，

HydLa

の数式処理に基づく実装である．バックエンドに数式処理を用

いているため計算誤差のないシミュレーションが可能である．また記号実行が可能でパラ

第

2

章 ハイブリッド制約処理系

HyLaGI

と

LTL

モデル検査

5

メータを含むシステムを扱える．

HyLaGI

には，

ASSERT

文を用いた有界モデル検査機 能が存在する．さらに非決定実行が可能なので，定性的に異なる軌道を場合分けを行い同 時に出力することができる．図

2.1

を

HyLaGI

でシミュレーションした結果は図

2.2

の ようになる．

HyLaGI

の実行結果は，ハイブリッドシステムのシミュレーション結果とし て，システムの各変数がとる離散的なふるまいと連続的なふるまいを交互に計算し，解軌 道として出力する．図

2.2

中の

PP

とは

Point Phase

の事で，システムの離散的なふるま いを表す．同様に

IP

とは

Interval Phase

の事で，システムの連続的なふるまいを表す．

また実行結果のそれぞれのふるまいをフェーズと言う．この図

2.2

^{をグラフにすると次の} 図

2.3

のようになる．

2.4 ^{線形時相論理}

線形時相論理

(Liner Temporal Logic, LTL)

とは，時間に関する様相を持った論理のこ とである．

LTL

式

(ϕ

，

ψ)

は次の図

2.4

からなる．

図

2.4

の各式について説明していく．式

2.1

は，真理値

(True

，

False)

や原子論理式は

LTL

式であることを表している．式

2.2

は，

LTL

式同士の論理結合子による演算も

LTL

式となることを表している．式

2.3

によって表現された

LTL

式は，「次の時刻

(

次の瞬間

)

において

ϕ

が真となる」ことを表している．式

2.4

によって表現された

LTL

式は，「現在 以降常に

ϕ

が真である」ことを表している．式

2.5

によって表現された

LTL

式は，「現在 以降にいつか

ϕ

が真となる」ことを表している．式

2.6

によって表現された

LTL

式は，

「

ψ

が真となるまで

ϕ

が真である」ことを表している．ここで

psi

が真とならなければ式

2.6

は偽となる．式

2.7

によって表現された

LTL

式は，「

ψ

が真となるまで

ϕ

が真である」

ことを表しているが，式

2.6

^{と異なるのは，}

ψ

が真とならなくても，常に

ϕ

^{が真であれば} 式

2.7

が真となる点である．式

2.7

によって表現された

LTL

式は，「

ϕ

が真となるまで

ψ

が真である」ことを表している．これらの

X

，

□

^，

♢

^，

U

，

W

，

R

は時相演算子と言う．

LTL

式ではこれら時相演算子などを用いることで，将来の性質に関して表現することが できる．

LTL

で表現できる性質には，安全性や活性といった特性がある．安全性とは，何 か

(

悪いこと

)

が決しておこらないことを表し，活性とは，何か

(

良いこと

)

がいつかおこ ることを表す．本論文内では，

□ (always)

を

[]

，

♢ (eventually)

を

<>

で表すこととする．

第

2

章 ハイブリッド制約処理系

HyLaGI

と

LTL

モデル検査

6

--- Result of Simulation --- ---Case 1---

---1--- ---PP 1--- unadopted modules: {}

positive : negative : t : 0 y : 10 y’: 0 y’’: -10

---IP 2--- unadopted modules: {}

positive : negative : t : 0->2^(1/2) y : 10+t^2*(-5) y’: t*(-10) y’’: -10

---2--- ---PP 3--- unadopted modules: {FALL}

unsat mod : {BOUNCE, FALL}

unsat cons : {y’’=-10, y’=(-4)/5*y’-}

positive : y-=0=>y’=(-4)/5*y’- negative :

t : 2^(1/2) y : 0 y’: 2^(1/2)*8

---IP 4--- unadopted modules: {}

positive :

negative : y-=0=>y’=(-4)/5*y’- t : 2^(1/2)->2^(1/2)*13/5

y : 2^(1/2)*8*(t+2^(1/2)*(-1))+(t+2^(1/2)*(-1))^2*(-5) y’: 2^(1/2)*8+(t+2^(1/2)*(-1))*(-10)

y’’: -10

---3--- ---PP 5--- unadopted modules: {FALL}

unsat mod : {BOUNCE, FALL}

unsat cons : {y’’=-10, y’=(-4)/5*y’-}

positive : y-=0=>y’=(-4)/5*y’- negative :

t : 2^(1/2)*13/5 y : 0

y’: 2^(1/2)*32/5 ---IP 6--- unadopted modules: {}

positive :

negative : y-=0=>y’=(-4)/5*y’- t : 2^(1/2)*13/5->2^(1/2)*97/25

y : 2^(1/2)*32/5*(t+2^(1/2)*(-13)/5)+(-5)*(t+2^(1/2)*(-13)/5)^2 y’: 2^(1/2)*32/5+(-10)*(t+2^(1/2)*(-13)/5)

y’’: -10

---4--- ---PP 7--- unadopted modules: {FALL}

unsat mod : {BOUNCE, FALL}

unsat cons : {y’’=-10, y’=(-4)/5*y’-}

positive : y-=0=>y’=(-4)/5*y’- negative :

t : 2^(1/2)*97/25 y : 0

y’: 2^(1/2)*128/25 ---IP 8--- unadopted modules: {}

positive :

negative : y-=0=>y’=(-4)/5*y’- t : 2^(1/2)*97/25->2^(1/2)*613/125

y : 2^(1/2)*128/25*(t+2^(1/2)*(-97)/25)+(-5)*(t+2^(1/2)*(-97)/25)^2 y’: 2^(1/2)*128/25+(-10)*(t+2^(1/2)*(-97)/25)

y’’: -10

---5--- ---PP 9--- unadopted modules: {FALL}

unsat mod : {BOUNCE, FALL}

unsat cons : {y’’=-10, y’=(-4)/5*y’-}

positive : y-=0=>y’=(-4)/5*y’- negative :

t : 2^(1/2)*613/125 y : 0

y’: 2^(1/2)*512/125 ---IP 10--- unadopted modules: {}

positive :

negative : y-=0=>y’=(-4)/5*y’- t : 2^(1/2)*613/125->2^(1/2)*3577/625

y : 2^(1/2)*512/125*(t+2^(1/2)*(-613)/125)+(-5)*(t+2^(1/2)*(-613)/125)^2 y’: 2^(1/2)*512/125+(-10)*(t+2^(1/2)*(-613)/125)

y’’: -10

# number of phases reached limit

図

2.2:

跳ねる質点のシミュレーション結果

第

2

章 ハイブリッド制約処理系

HyLaGI

と

LTL

モデル検査

7

図

2.3:

跳ねる質点のシミュレーショングラフ

ϕ, ψ ::= T rue | F alse | Atomic Formula (2.1)

| ¬ ϕ | ϕ ∧ ψ | ϕ ∨ ψ | ϕ ⇒ ψ (2.2)

| Xϕ (2.3)

| □ ϕ (2.4)

| ♢ ϕ (2.5)

| ϕUψ (2.6)

| ϕWψ (2.7)

| ϕRψ (2.8)

図

2.4: LTL

式の構文

第

2

章 ハイブリッド制約処理系

HyLaGI

と

LTL

モデル検査

8

2.5 LTL ^{モデル検査}

モデル検査とは，システムを表すオートマトン

M _A

と性質

ϕ

を表すオートマトン

M _ϕ

を用いる．システムが性質を満たしているとは，システムの実行結果

(

実行経路

)

の集合 すべてが，性質を満たしているものすべての集合の部分集合であるということである．

つまり，システムを表すオートマトン

M _A

が満たす受理列

L(M _A )

の集合が，性質を 表すオートマトン

M _ϕ

が満たす受理列

L(M _ϕ )

の集合の部分集合であるということであ る．したがって，式

2.9

のように，

L(M A )

が

L(M ϕ )

の部分集合であるということは，

L(M A × M _¬ ϕ )

が空集合であることと同値になる．

L(M A ) ⊆ L(M ϕ )

⇐⇒ L(M _A ) ∩ L(M _ϕ ) = ϕ

⇐⇒ L(M A × M _¬ ϕ ) = ϕ (2.9)

つまり，モデル検査では，

M A × M _¬ ϕ

の同期積オートマトンの受理列

L(M A × M _¬ ϕ )

を 探索することにより，モデルが性質を満たしているか判定する手法である．もし受理列が 存在すれば，それは検証している性質を満たさない反例となり，もし受理列が存在しなけ れば，それはシステムの全ての実行結果が性質を満たすことになる．

LTL

式から性質オートマトンを作成する手法は，文献

[15]

^{にて研究されている．}

LTL

モデル検査での探索について簡単に説明していく．性質を表した

LTL

式

ϕ

が安 全性の場合

¬ ϕ

の受理列の探索なので，何か

(

悪いこと

)

がおこるかどうかの検証となる．

そのため受理状態

(

悪い状態

)

に到達するかという到達可能性問題に帰着する．また

LTL

式

ϕ

が活性の場合

¬ ϕ

の受理列の探索なので，何か

(

良いこと

)

が常に起こらないかどう かの検証となる．つまり受理状態

(

良いことが起こらない状態

)

を無限回訪れることがで きるような受理列

(

受理サイクル

)

が存在するかという受理サイクル探索問題となる．本 論文では受理サイクルを検出するため，

SPIN[8]

の

Nested DFS (

二重深さ優先探索

)

を参 考にした．

Nested DFS

は，二つのステップからなり，受理サイクルに関わる受理状態に 訪れたときそこまでの経路を保存しておいて

(step1)

，それ以降の遷移の際に保存した経 路中の状態へのループがないか探索する

(step2)

^{手法である．}

9

第 3 ^章

LTL ^{モデル検査の導入}

本章では，提案した

HyLaGI

への

LTL

モデル検査の導入手法の説明を行う．

3.1 HyLaGI ^への LTL ^{モデル検査の導入手法}

HyLaGI

への実装の際には，次のような理由で幅優先探索での実装を行った．まず，最

悪の場合は深さ優先探索も幅優先探索も全状態空間を探索することになるが，一般的に深 さ優先探索は幅優先探索に比べ空間計算量が小さくなる．しかし，幅優先探索は最短の 深さで目標状態を発見できる．また

HyLaGI

のシミュレーションでは，モデルによって シミュレーションを進めていくにつれて計算が複雑化し，計算に時間がかかる場合があ る．ここで

HyLaGI

で

LTL

モデル検査を行う場合，一段階深く探索しようとすると，現 在の状態から次の状態の生成のために，次の

1

フェーズを計算する必要がある．そのため

「

HyLaGI

のシミュレーションにかかる時間計算量の増大」と「深さ優先探索に比べて幅

優先探索の空間計算量の増大」を比較すると，前者の影響の方が大きいと考え，深さが最 短となる幅優先探索で実装した．

ここで，

HyLaGI

の場合，システム

M _A

の各状態は，採用された制約モジュール，そ

れぞれの変数の値，成立しているガード条件

(

展開済みのガード条件

)

，パラメータ

(

記号 定数

)

の値という情報を持つ．ここでのシステムのオートマトン

M A

は，一般的なハイブ リッドオートマトン

[18]

とは異なり，連続変化と離散変化の両方が状態となる．また，ハ イブリッドオートマトンは遷移可能な場合遷移する場合と遷移しない場合のそれぞれの動 作が考えられるが，今回想定しているオートマトンでは，遷移可能の場合はすぐに遷移す るものとなっている．

性質オートマトン

M _¬f

は検証したい性質なので与えられる

LTL

式から作られている．

第

3

章

LTL

モデル検査の導入

10

性質オートマトン

M _¬ f

の状態は，受理サイクル探索問題に関係する受理状態

(acceptance cycle)

か，到達可能性問題に関係する受理状態

(acceptance state)

か，それらと関係ない 状態なのかといった情報をもつ．今回

LTL

式から性質オートマトンを作成するために，

文献

[15]

を実装したツール

LTL2BA

を用いた．

LTL

式から変換された性質オートマト ンの各エッジは，遷移のためのガード条件によってラベリングされている．

ここで

LTL2BA[15]

による性質オートマトンの作成では，受理サイクル問題の受理状

態

(acceptance cycle)

か到達可能性問題に置ける受理状態

(acceptance state)

かは区別 されない．そこで作成された性質オートマトンにおいて，自分自身をガード条件

true

^で 回るエッジがある受理状態は，任意の回数自分自身を回ることができるので，その状態に 至った時点で受理列を発見できるものであるため，

acceptance state

としている．

2.5

節のようにモデル検査では，システムオートマトンと性質オートマトンからなる同 期積オートマトンの状態空間を作成し，受理列が存在するか探索する．しかし，実際の実 装では，同期積オートマトンの状態空間を構築しながら，受理列が存在するか探索するこ とになる．始めに構築される状態は，

HyLaGI

の実行結果から得られる始めのフェーズの 情報と

LTL

式から作られる性質オートマトンの初期状態，つまり，

PP1

と性質オートマ トンの初期ノード

(

始点ノード

)

から作成される．また，現在の状態から新しいの状態の

作成は，

HyLaGI

から得られる次のフェーズが性質オートマトンの遷移エッジのガード満

たしているか調べ，満たしている場合に次のフェーズと性質オートマトンの遷移先から新 しい状態を作成していく．

実装アルゴリズムは次の図

3.1

のようになる

.

通常の

HyLaGI

実行アルゴリズム

[14]

に加えて，

LTL

モデル検査のために，入力として検証したい性質を表す

LTL

^{式が必要に} なり，

LTL

モデル検査部分の初期化処理

(5

，

6

行目

)

，各

PP

，

IP

の計算終了時に

LTL

モデル検査に関する処理

(14

，

29

行目

)

，次の離散変化時刻計算時に性質オートマトンの エッジを満たしているかという情報から得られる時刻に関する処理

(25

^行目

)

^{が追加され} ている．また出力として

HyLaGI

の実行結果に加えて，

LTL

モデル検査を行った結果と して作成した複数の状態空間が出力される．

アルゴリズムに追加された部分について，それぞれ説明していく．

5

行目は

LTL

式か ら性質オートマトン

PA(Property Automaton)

を作成している．

6

行目は性質オートマ トンとフェーズの初期状態から，

LTL

モデル検査において現在検査しているノード

(

状 態

)

の情報

CN(Checking Nodes)

と，モデル検査の結果

RA(Result Automata)

を初期化 している．

LTLModelChecking

は次の段落で詳しく説明する．

25

行目の

GetEdgeGuard

で得られた条件について最小時刻を計算しているのは，次のフェーズが性質オートマトン

(PA)

の遷移のガード条件を満たしているかいないかで，きちんと場合分けするためであ

第

3

章

LTL

モデル検査の導入

11 Input: HydLa

プログラム

HydLaProgram,

シミュレーション終了時刻

MaxT,

検査し

たい性質

LTL

Output: HydLa

プログラムの実行結果

, LTL

モデル検査の結果

RA

1: MS := TopologicalSort(SolveCH(HydLaProgram))

2: M _all := MaxModuleSet(MS)

3: V := GetVariables(HydLaProgram)

4: T := 0, S := ture, CP := ture

5: PA := LTL2BA(LTL)

6: (CN, RA) := InitializeModelChecking(PA, S, CP, V)

7: while T < CP M axT do

8: S := SubstituteMinTime(S, T)

9: (S, CP, E, , ) := CalculateMCS(S, MS, E, CP, T, CheckConsistencyPP)

10: if S = f alse then

11: break

12: end if

13: (S, CP) := AddParameters(S, CP, V)

14: (CN, RA) := LTLModelChecking(CN, RA, PA, S, MS, E, CP, T)

15: (S, CP, E, A ₊ , A ₋ ) := CalculateMCS(S, MS, E, CP, T, CheckConsistencyIP)

16: S := SolveDifferentialEquation(S)

17: if S = f alse ∨ ¬ IsUnique(S, V) then

18: break

19: end if

20: (MinT, CP) := GetElement(CompareMinTime(

21: { FindMinTime(S ∧ CP ⇒ g) | (g ⇒ c) ∈ A ₋ }

22: ∪{ FindMinTime(S ∧ CP ⇒ ¬ g) | (g ⇒ c) ∈ A ₊ }

23: ∪{ FindMinTime(S ∧ CP ∧ M ₋ ) | M ₋ ∈ (M all \ M) }

24: ∪{ FindMinTime(S ∧ CP ∧ ¬ M + ) | M + ∈ M }

25: ∪{ FindMinTime(S ∧ CP ⇒ g) | g ∈ GetEdgeGuard(PA) }

26: ∪{ (MaxT − T, true) } ))

27: T := MinT + T

28: end while

29: (CN, RA) := LTLModelChecking(CN, RA, PA, S, MS, E, CP, T)

図

3.1: HyLaGI

の

LTL

モデル検査アルゴリズム

第

3

章

LTL

モデル検査の導入

12

る．これは一つのフェーズ中に遷移のガード条件を満たしている場合と満たしていない 場合，両方が混在していると遷移可能かどうかがわからなくて困ったことになるからで ある．

14

，

29

行目の

LTLModelChecking

関数のアルゴリズムは，図

3.2

ようになる．この

Input:

現在検査するノードの情報

CN,

現在のモデル検査結果

RA,

性質オートマトン

PA,

計算したフェーズの各情報

(S,MS,E,CP,T)

Output:

次に検査するノードの情報

CN,

更新されたモデル検査結果

RA

1: NextCheckingNodes := {}

2: for CheckingNode ∈ CN do

3: NextNodeCandidates := MakeNextNodes(PA, S, CP, V, CheckingNode)

4: for NextNode ∈ NextNodeCandidates do

5: (RA, NextNode) := DetectingAcceptanceCycle(NextNode, CheckingNode, RA)

6: (RA, NextNode) := DetectingLoop(NextNode, CheckingNode, RA)

7: NextCheckingNodes := AddCheckingNode(NextCheckingNodes, NextNode)

8: (RA, NextNode) := CheckSafety(NextNode, CheckingNode, RA)

9: NextNode := CheckLiveness(NextNode, CheckingNode, RA)

10: RA := ProcessNodeInResult(RA, NextNode, CheckingNode)

11: end for

12: end for

13: CN := NextCheckingNodes

図

3.2: LTLModelChecking

関数アルゴリズム

LTLModelChecking

関数は，現在検査しているノードに関する情報

CN

，現在のモデル

検査状況

RA

，検査する性質オートマトン

PA

，シミュレーションしたフェーズに関する

情報

(S, MS, E, CP, T)

を入力とする．出力には，次の検査のためのノードの情報

CN

，

更新されたモデル検査状況

RA

が出力される．

1

行目は次の検査のためのノードの情報を格納する変数

NextCheckingNodes

を初期 化している．

2

行目の

for

文では現在検査するノードの情報

CN(CheckingNodes )

から 一つずつ

CheckingNode

を取り出してループを回している．次の

MakeNextNodes

では 取り出したノードから遷移可能なノードの集合

(NextNodeCandidate )

^{を作成する．}

4

行目の

for

文では

NextNodeCandidates

から一つずつ

NextNode

を取り出してループを

第

3

章

LTL

モデル検査の導入

13

回す．ループ内では

NextNode

を用いて，受理サイクルが発見できるかどうか

(5

行目

DetectingAcceptanceCycle

関数，

Nested DFS

の

step2)

，包含関係によって通常のルー プとなるかどうか

(6

行目

DetectingLoop

関数

)

，到達可能性問題の受理状態かどうか

(8

行目

CheckSafety

関数

)

，受理サイクル問題の受理状態かどうか

(9

行目

CheckLiveness

関数，

Nested DFS

の

step1)

，を検査している．また，検査して受理列が発見された場合 や状態空間構築が終了した場合，

10

行目の

ProcessNodeInResult

関数で現在の状態空間 を

RA

に保存し，

CheckingNode

を状態空間から削除して，次の非決定実行によるモデル 検査の準備を行う．最後に

13

行目では次の検査のために，

CN

^を

NextCheckingNodes

^で 更新する．

3.2 ^{提案手法の特徴}

3.2.1 ^{ループ検出}

モデル検査では，状態空間においてループを検出する必要がある．しかし，ハイブリッ ドシステムではシステム中の各変数が時刻に伴い連続して変化するため，全く同じ変化を することでループを検出しようとすると，多くのシステムではループを検出できずに状態 数が無限と発散してしまう．

そこで，状態同士の包含関係を持ちいてループを検出する．状態の包含に関して図

3.3

の

4

つの項目で検査する．この図

3.3

の

1

に関して，性質オートマトンの状態が異なる

1:

性質オートマトンの状態が等しい

2:

採用されたモジュール集合が等しい

3:

展開されたガード条件が等しい

4:

変数値の組の取りうる領域が包含されている

図

3.3:

状態同士の比較手法

と，その性質オートマトンの状態によって，そこから先の状態遷移が変化していく．その ため，性質オートマトンの状態が等しいことは，状態の包含において重要な比較項目と なる．

次に図

3.3

^の

2

^，

3

^，

4

の項目を満たす場合にループと判定できるか理由を説明する．こ れら

(2

，

3

，

4)

はシステムの解軌道における各

phase

が持っている情報に関する判定であ る．もし解軌道中のフェーズ

A

とフェーズ

B

を考えたときに，フェーズ

A

で計算した情

第

3

章

LTL

モデル検査の導入

14

報とフェーズ

B

で計算した情報を比較して，項目

(2

，

3

，

4)

を満たしている場合，フェー ズ

B

で求められた解軌道はフェーズ

A

で計算したときにすでに計算されているというこ とになる．つまり，フェーズ

B

以降の解軌道は，フェーズ

A

以降の解軌道に包含されて いることになる．これによって，フェーズ

B

以降の遷移は，フェーズ

A

以降の遷移と等 しくなると考えて，ループを判定している．

本手法では，変数間に相関がある場合を考慮して，図

3.3

の項目

4

では取りうる値の 領域の包含を用いてループを判定している．領域を比較する二つのフェーズを

L(large)

，

S(small)

^{とする．ここで}

L

^と

S

^{の変数の組をそれぞれ}

l

^，

s

とし，その取りうる領域を

L

^，

S

とする．

L

と

S

のパラメータに関する条件を

l _pm

，

s _pm

とする．このとき次の式

3.1

に よって領域の包含を判定してループを検出する．

∀ s ∃ l, s pm ∧ l pm ∧ { s i = l i , i = 1 . . . n } (3.1)

この式

3.1

は，フェーズ

S

がフェーズ

L

に包含されている場合，フェーズ

S

中の変数の 組

s

が取りうる領域中の全ての値

s i

には，フェーズ

L

中の変数の組

l

が取りうる領域中 の対応するある値

l _i

が存在するということを表す数式となる．

ここで

4

の項目において，各変数ごとに比較した場合は変数間の相関を無視しているた め，正しく判定できない場合がある．どのように正しく判定できないかは，次の項

3.2.2

にて詳しく説明する．

3.2.2 変数間に相関があるモデル

変数間に相関があるモデルの例として，わかりやすいように人工的な例題

3.4

を用いて 説明する．

1 INIT <=> y = -y’*2 & -1 < y’ < 1.

2 MOVE <=> [](y’’=0).

3 TIMER <=> timer=0 & [](timer’=1).

4 CHECK <=> [](timer- = 1 => timer = 0).

5 INIT,MOVE,TIMER<<CHECK.

図

3.4:

人工的なモデル

これは、ある物体が等速運動を行いつつ，タイマーが

1

秒毎に物体の位置を確認してい る例題である．物体の位置

y

は区間

(-2

，

2)

から始まり、ある焦点

(2

秒後に

y=0

の位置

)

第

3

章

LTL

モデル検査の導入

15

を通過するように運動を開始する．

1

秒ごとに切り替わるタイマーが入っているため、

1

秒ごとに離散変化が起こる．ここでは，検査する性質として常に

y

が

3

より小さい，つま り，式

3.2

を検証する．

[](y < 3) (3.2)

式

3.2

から作成される性質オートマトンは，図

3.5

となる．

0 True

1 y>=3

True

図

3.5:

常に

y

が

3

より小さい

([](y < 3))

から作られる性質オートマトン

このモデル

3.4

の実行結果は図

3.6

のようになる．これをグラフにすると，図

3.7

と なる．

ここで図

3.7

^{をみるとフェーズ}

4

^{までで，常に}

y < 3

^なので図

3.5

^のノード

0

^からノー ド

1

へのエッジのガード条件が満たせず，性質オートマトンの遷移経路は，ノード

0

を 周り続けてノード

1

へ出ていけないことになる．このときフェーズ

5

から作られる状態

(Property0 PP5)

^が，

(Property0 PP3)

に包含されているか検査する．すると，

1:

^性質 オートマトンの状態，

2:

採用されている制約モジュール，

3:

展開されているガード条件は，

それぞれ等しくなる．

そこで，もし各変数の取りうる値の比較を行った場合，図

3.6

より

PP3

と

PP5

を比較 すると，時刻を除いた各変数

timer

，

y

，

y ^′

，

y ^′′

の取りうる値は，それぞれ，

PP3

の各変 数

⊇ PP5

の各変数，のように包含されている．そのため，各変数同士を比較した場合

しかし，図

3.7

のように変数の組が取りうる領域は，実際には包含されておらず，図

3.7

の位置

y

が，初期値

-2

から始まる軌道のように，いずれ性質を満たさない状態へ至る経路 が存在する．実際に

y

と

y ^′

平面にそれぞれの取りうる領域を書くと，図

3.8

のようにな る．

PP3(

図

3.8a)

と

PP5(

図

3.8b)

を見比べると，それぞれの軸に射影した場合の領域を 考えると確かに包含されているが，実際に動く領域を考えると包含されていないことがわ かる．

第

3

章

LTL

モデル検査の導入

16

--- Result of Simulation ---

---parameter condition(global)--- p[y, 0, 1] : (-2, 2)

---Case 1--- ---1--- ---PP 1--- unadopted modules: {}

positive : negative : t : 0 timer : 0 y : p[y, 0, 1]

timer’: 1 y’: y*(-1)/2 y’’: 0

---IP 2--- unadopted modules: {}

positive : negative : t : 0->1 timer : t

y : p[y, 0, 1]+t*p[y, 0, 1]*(-1)/2 timer’: 1

y’: p[y, 0, 1]*(-1)/2 y’’: 0

---2--- ---PP 3--- unadopted modules: {TIMER}

unsat mod : {CHECK, TIMER}

unsat cons : {timer’=1, timer=0}

positive : timer-=1=>timer=0 negative :

t : 1 timer : 0 y : p[y, 0, 1]*1/2 y’: p[y, 0, 1]*(-1)/2 y’’: 0

---IP 4--- unadopted modules: {}

positive :

negative : timer-=1=>timer=0 t : 1->2

timer : t+(-1)

y : p[y, 0, 1]+t*p[y, 0, 1]*(-1)/2 timer’: 1

y’: p[y, 0, 1]*(-1)/2 y’’: 0

---3--- ---PP 5--- unadopted modules: {TIMER}

unsat mod : {CHECK, TIMER}

unsat cons : {timer’=1, timer=0}

positive : timer-=1=>timer=0 negative :

t : 2 timer : 0 y : 0

y’: p[y, 0, 1]*(-1)/2 y’’: 0

---IP 6--- unadopted modules: {}

positive :

negative : timer-=1=>timer=0 t : 2->3

timer : t+(-2)

y : p[y, 0, 1]+t*p[y, 0, 1]*(-1)/2 timer’: 1

y’: p[y, 0, 1]*(-1)/2 y’’: 0

---4--- ---PP 7--- unadopted modules: {TIMER}

unsat mod : {CHECK, TIMER}

unsat cons : {timer’=1, timer=0}

positive : timer-=1=>timer=0 negative :

t : 3 timer : 0

y : p[y, 0, 1]*(-1)/2 y’: p[y, 0, 1]*(-1)/2 y’’: 0

---IP 8--- unadopted modules: {}

positive :

negative : timer-=1=>timer=0 t : 3->4

timer : t+(-3)

y : p[y, 0, 1]+t*p[y, 0, 1]*(-1)/2 timer’: 1

y’: p[y, 0, 1]*(-1)/2 y’’: 0

---5--- ---PP 9--- unadopted modules: {TIMER}

unsat mod : {CHECK, TIMER}

unsat cons : {timer’=1, timer=0}

positive : timer-=1=>timer=0 negative :

t : 4 timer : 0 y : (-1)*p[y, 0, 1]

y’: p[y, 0, 1]*(-1)/2 y’’: 0

---IP 10--- unadopted modules: {}

positive :

negative : timer-=1=>timer=0 t : 4->5

timer : t+(-4)

y : p[y, 0, 1]+t*p[y, 0, 1]*(-1)/2 timer’: 1

y’: p[y, 0, 1]*(-1)/2 y’’: 0

---parameter condition(Case1)--- p[y, 0, 1] : (-2, 2)

# number of phases reached limit

図

3.6:

人工的な例題のシミュレーション結果

3.2.3 非決定なモデルへの LTL モデル検査

HyLaGI

はシミュレーションの結果，定性的に異なる軌道を場合分けを行って同時に出

力する．そのため，解軌道が場合分けされたとき，ぞれぞれの軌道ごとに探索を行う必要 が有る．

床に穴のあいた跳ねる質点

床に穴があいていて，質点の初速度によって穴に落ちる場合や落ちない場合がどちらも 起こりうるモデルを考える．質点の高さを

y

，横方向の位置を

x

とする．まず質点は初期 位置

(x, y) = (0, 10)

から運動を始める．

y

軸方向には，初速度

0

から鉛直下向きに重力加 速度

y ^′′ = − 10

^{で落下していく．}

x

軸方向には，初速度がパラメータ

(x ^′ = (2, 5))

^で運動

第

3

章

LTL

モデル検査の導入

17

図

3.7:

人工的な例題の実行結果のグラフ

(a) PP3

の

yy

^′平面のグラフ

(b) PP5

の

yy

^′平面のグラフ 図

3.8: PP3

と

PP5

の

yy

^′平面のグラフ

第

3

章

LTL

モデル検査の導入

18

を開始し等速直線運動を行う．

y

軸方向では床や穴の底にぶつかると

4/5

倍の速度で跳ね 返り，

x

軸方向では穴の壁にぶつかると完全弾性衝突

(

反発係数

1

倍

)

で跳ね返る．また，

穴の内部に

y = − 1

の位置のセンサーがあり，質点が通過した時にセンサーが反応する．

このモデルで，「質点が常にセンサーに反応しない

(y ̸ = − 1)

」性質を検証する．つまり 式

3.3

を検査するとする．

[](y ̸ = − 1) (3.3)

式

3.3

から作成される性質オートマトンは図

3.9

となる．この性質オートマトンにおいて，

0 True

1 y=-1

True

図

3.9:

常に高さ

y

が

-1

ではない

([]y ̸ = − 1)

から作られる性質オートマトン

受理状態のノード

1

^{は自分自身を}

true

で回ることができるため，ノード

1

^を

acceptance

state(

到達可能性問題の受理状態

)

として考える．

例えば，図

3.10

のように場合分けが起こるプログラムを考える．このプログラムは

xy 1 INIT <=> y = 10 & y’ = 0 & x = 0 & 2 < x’ < 5.

2 FALL <=> [](y’’ = -10).

3 XCONST <=> [](x’’ = 0).

4 XBOUNCE <=> []((x-=4|x-=6)&y-<0 => x’=-x’-).

5 BOUNCE <=>

6 [](y-=-7|(x-<=4|x->=6)&y-=0 => y’=-(4/5)*y’-).

7 SENSOR <=> [](y-=-1 => $TRUE).

8 INIT, FALL << BOUNCE, XCONST << XBOUNCE, SENSOR.

図

3.10:

床に穴が空いた跳ねる質点プログラム

の二次元空間を運動する質点を考えている．質点が跳ねる床には，

x

座標

4

から

6

の位置 に深さ

7

の穴があいている．質点は床や穴の底と衝突すると速度が

4/5

倍で跳ね返る運動

第

3

章

LTL

モデル検査の導入

19

をし，穴の壁に衝突すると完全弾性衝突が起こり跳ね返る．穴の内部には質点が落ちたか どうかを判定するセンサーが取り付いていて，センサーのガード条件が反応して離散変化 がおきることにより，質点が通過した時刻や各変数の値を得られるようなモデルである．

この

3.10

の

LTL

モデル検査結果は，図

3.11

のようになる．

x

軸方向の初速度によって

8

つの場合分けが発生する．それぞれの場合分けの詳細は 次のようになる．

Case1

は穴の左側の床にぶつかって穴を飛び越える．

Case2

は床と穴 の左角にぶつかって穴を飛び越える．

Case3

はセンサーに引っかかったあと，穴の底に ぶつかる．

Case4

はセンサーに引っかかったあと，穴の底と右側の壁の角にぶつかる．

Case5

はセンサーに引っかかったあと，穴の右側の壁にぶつかる．

Case6

は穴の右側の

壁とセンサーに同時にぶつかる．

Case7

は穴の右側の壁にぶつかったあと，センサーに 引っかかる．

Case8

は穴を飛び越えて穴の右側の床にぶつかる．このとき

Case1

^から

Case8

をそれぞれ検証すると図

3.21

のようになる，ここでは無限状態となる

Case

が

存在するため深さ

6

までの探索で打ち切っている．受理列が存在するかわからない軌道

(Case1

，

Case2

，

Case8)

と，受理状態に至るような性質を満たさない反例が発見される軌 道

(Case3

，

Case4

，

Case5

，

Case6

，

Case7)

が得られる．このモデルだと，穴に落ちてセン サーが反応するか，穴に落ちないかの二通りに分類できるため，図

3.21

のように

(Case1

，

Case2

，

Case8)

と

(Case3

，

Case4

，

Case5

，

Case6

，

Case7)

の，それぞれ似通った二種類 の探索空間ができているが，一般的にはそれぞれの

case

ごとに異なった結果が出てくる ことが考えられる．このように，定性的に異なる軌道からは，異なる

LTL

モデル検査結 果が得られるため，それぞれの軌道に対して独立に

LTL

モデル検査を行っている．

3.3 ^{関連する研究}

ハイブリッドシステムにおいて，システムの満たす性質を検証する研究は数多く ある．安全性についての検証は，

HyTech[17]

，

PHAVer[9]

，

SpaceEx[10]

，

Ariadne[13]

，

HSolver[16]

^，

FLOW*[20]

^，

d/dt[7]

^，

HybridSAL[4]

などが存在する．これらは全てハイ ブリッドオートマトンをそれぞれモデリングし，入力としている．活性に関する検証も行 えるものは少ないが，

KeYmaera[3]

，

HyCOMP[1]

が存在する．

KeYmaera[3]

はハイブリッドシステムを手続き型の言語

(Hybrid Program)

を用いて モデリングし，事前条件，不変条件，事後条件を用いて記述された性質を論理的分析法に よって検証する検証器である．バックエンドには数式処理を利用していて，誤差のない 計算が可能である．検証する性質によって，証明が自動ではできなくなり，モデルの十 分な理解と証明手法の選択が必要となる．もちろん手動で

LTL

モデル検査の手法を再現

第

3

章

LTL

モデル検査の導入

20

===== Property Automaton =====

digraph g{

"0" [color="#000000"];

"0" -> "0"[color="#000000",label="True"];

"0" -> "1"[color="#000000",label="y=-1"];

"1" [color="#000000",peripheries=2];

"1" -> "1"[color="#000000",label="True"];

}

===== Automaton1 =====

digraph g{

"init" [color="#000000"];

"init" -> "Property0 Phase1"[color="#000000"];

"Property0 Phase1" [color="#000000"];

"Property0 Phase1" -> "Property0 Phase2"[color="#000000"];

"Property0 Phase2" [color="#000000"];

"Property0 Phase2" -> "Property0 Phase3"[color="#000000"];

"Property0 Phase3" [color="#000000"];

"Property0 Phase3" -> "Property0 Phase25"[color="#000000"];

"Property0 Phase25" [color="#000000"];

"Property0 Phase25" -> "Property0 Phase26"[color="#000000"];

"Property0 Phase26" [color="#000000"];

"Property0 Phase26" -> "Property0 Phase27"[color="#000000"];

"Property0 Phase27" [color="#000000"];

"Property0 Phase27" -> "Property0 Phase28"[color="#000000"];

"Property0 Phase28" [color="#000000"];

}. ..

===== Automaton8 =====

digraph g{

"init" [color="#000000"];

"init" -> "Property0 Phase1"[color="#000000"];

"Property0 Phase1" [color="#000000"];

"Property0 Phase1" -> "Property0 Phase22"[color="#000000"];

"Property0 Phase22" [color="#000000"];

"Property0 Phase22" -> "Property0 Phase24"[color="#000000"];

"Property0 Phase24" [color="#000000"];

"Property0 Phase24" -> "Property0 Phase53"[color="#000000"];

"Property0 Phase53" [color="#000000"];

"Property0 Phase53" -> "Property0 Phase54"[color="#000000"];

"Property0 Phase54" [color="#000000"];

"Property0 Phase54" -> "Property0 Phase55"[color="#000000"];

"Property0 Phase55" [color="#000000"];

"Property0 Phase55" -> "Property0 Phase56"[color="#000000"];

"Property0 Phase56" [color="#000000"];

}

--- Result of Simulation ---

---parameter condition(global)--- p[x, 1, 1] : (2, 5)

---Case 1--- ---1--- ---PP 1--- unadopted modules: {}

positive : negative : t : 0 x : 0 y : 10 x’: p[x, 1, 1]

y’: 0 x’’: 0 y’’: -10 .. .

---IP 27--- unadopted modules: {}

positive :

negative : (y-=-7|(x-<=4|x->=6)&y-=0)=>y’=(-(4/5))*y’- t : 2^(1/2)*13/5->2^(1/2)*97/25

x : t*p[x, 1, 1]

y : 2^(1/2)*32/5*(t+2^(1/2)*(-13)/5)+(-5)*(t+2^(1/2)*(-13)/5)^2 x’: p[x, 1, 1]

y’: 2^(1/2)*32/5+(-10)*(t+2^(1/2)*(-13)/5) x’’: 0

y’’: -10

---parameter condition(Case1)--- p[x, 1, 1] : (2, 2^(1+1/2))

# number of phases reached limit ---Case 2--- ..

.

---IP 31--- unadopted modules: {}

positive :

negative : (y-=-7|(x-<=4|x->=6)&y-=0)=>y’=(-(4/5))*y’- t : 2^(1/2)*13/5->2^(1/2)*97/25

x : t*p[x, 1, 1]

y : 2^(1/2)*32/5*(t+2^(1/2)*(-13)/5)+(-5)*(t+2^(1/2)*(-13)/5)^2 x’: p[x, 1, 1]

y’: 2^(1/2)*32/5+(-10)*(t+2^(1/2)*(-13)/5) x’’: 0

y’’: -10

---parameter condition(Case2)--- p[x, 1, 1] : 2^(1+1/2)

# number of phases reached limit ---Case 3--- ..

.

---IP 35--- unadopted modules: {}

positive :

negative : (y-=-7|(x-<=4|x->=6)&y-=0)=>y’=(-(4/5))*y’- t : (17/5)^(1/2)->6*p[x, 1, 1]^(-1)

x : t*p[x, 1, 1]

y : -7+8*(17/5)^(1/2)*(t+(-1)*(17/5)^(1/2))+(-5)*(t+(-1)*(17/5)^(1/2))^2 x’: p[x, 1, 1]

y’: 8*(17/5)^(1/2)+(-10)*(t+(-1)*(17/5)^(1/2)) x’’: 0

y’’: -10

---parameter condition(Case3)--- p[x, 1, 1] : (2^(1+1/2), 6*(5/17)^(1/2))

# number of phases reached limit ---Case 4--- ..

.

---IP 39--- unadopted modules: {}

positive :

negative : (y-=-7|(x-<=4|x->=6)&y-=0)=>y’=(-(4/5))*y’- (x-=4|x-=6)&y-<0=>x’=-x’-

t : (17/5)^(1/2)->(85^(1/2)*9+610^(1/2)*(-1))*1/25

x : p[x, 1, 1]*(17/5)^(1/2)+(-1)*p[x, 1, 1]*(t+(-1)*(17/5)^(1/2)) y : -7+8*(17/5)^(1/2)*(t+(-1)*(17/5)^(1/2))+(-5)*(t+(-1)*(17/5)^(1/2))^2 x’: (-1)*p[x, 1, 1]

y’: 8*(17/5)^(1/2)+(-10)*(t+(-1)*(17/5)^(1/2)) x’’: 0

y’’: -10

---parameter condition(Case4)--- p[x, 1, 1] : 6*(5/17)^(1/2)

# number of phases reached limit ---Case 5--- ..

.

---IP 43--- unadopted modules: {}

positive :

negative : y-=-1=>True t : (11/5)^(1/2)->(17/5)^(1/2)

x : 6+(-1)*p[x, 1, 1]*(t+(-6)*p[x, 1, 1]^(-1)) y : 10+t^2*(-5)

x’: (-1)*p[x, 1, 1]

y’: t*(-10) x’’: 0 y’’: -10

---parameter condition(Case5)--- p[x, 1, 1] : (6*(5/11)^(1/2), 2^(1/2)*3)

# number of phases reached limit ---Case 6--- ..

.

---IP 47--- unadopted modules: {}

positive :

negative : (y-=-7|(x-<=4|x->=6)&y-=0)=>y’=(-(4/5))*y’- t : (17/5)^(1/2)->8*p[x, 1, 1]^(-1)

x : 6+(-1)*p[x, 1, 1]*(t+(-6)*p[x, 1, 1]^(-1))

y : -7+8*(17/5)^(1/2)*(t+(-1)*(17/5)^(1/2))+(-5)*(t+(-1)*(17/5)^(1/2))^2 x’: (-1)*p[x, 1, 1]

y’: 8*(17/5)^(1/2)+(-10)*(t+(-1)*(17/5)^(1/2)) x’’: 0

y’’: -10

---parameter condition(Case6)--- p[x, 1, 1] : 6*(5/11)^(1/2)

# number of phases reached limit ---Case 7--- ..

.

---IP 51--- unadopted modules: {}

positive :

negative : (x-=4|x-=6)&y-<0=>x’=-x’- t : 6*p[x, 1, 1]^(-1)->(17/5)^(1/2)

x : 6+(-1)*p[x, 1, 1]*(t+(-6)*p[x, 1, 1]^(-1)) y : 10+t^2*(-5)

x’: (-1)*p[x, 1, 1]

y’: t*(-10) x’’: 0 y’’: -10

---parameter condition(Case7)--- p[x, 1, 1] : (6*(5/17)^(1/2), 6*(5/11)^(1/2))

# number of phases reached limit ---Case 8--- ..

.

---IP 55--- unadopted modules: {}

positive :

negative : (y-=-7|(x-<=4|x->=6)&y-=0)=>y’=(-(4/5))*y’- t : 2^(1/2)*13/5->2^(1/2)*97/25

x : t*p[x, 1, 1]

y : 2^(1/2)*32/5*(t+2^(1/2)*(-13)/5)+(-5)*(t+2^(1/2)*(-13)/5)^2 x’: p[x, 1, 1]

y’: 2^(1/2)*32/5+(-10)*(t+2^(1/2)*(-13)/5) x’’: 0

y’’: -10

---parameter condition(Case8)--- p[x, 1, 1] : [2^(1/2)*3, 5)

# number of phases reached limit

図

3.11:

床に穴があいた跳ねる質点の

LTL

モデル検査結果

(

一部抜粋

)

第

3

章

LTL

モデル検査の導入

21

図

3.12:

床に穴があいた跳ねる質点のグラフ

して検証することで，

LTL

式で表現できる性質を検証することは可能だが，そのままの

KeYmaera

の検証がサポートしているのは

LTL

式で表現できる性質の部分集合となる．

HyCOMP[1]

は

HyDI

という言語でハイブリッドオートマトンのネットワークをモデリ

ングしていて，不変条件，

LTL

式，シナリオの検証が可能である．このように

HyCOMP

は

LTL

式の検証が可能であるが，検証手法はモデル検査的手法ではなく論理的手法を用 いている点が本論文とは異なる．

HyCOMP

^では，

k-zeno(k-liveness)[2]

^用いて

LTL

^式 の論理的な検証を行う．この

k-zeno(k-liveness)

アルゴリズムとは，簡単に説明すると活 性の検証を不変条件問題の繰り返しに変換して検証する手法である．

HyLaGI

^{の特徴は，}

LTL

モデル検査を行っているため，性質検証には論理的アプロー

チではなくモデル検査的アプローチを用いている点である．また，

LTL

モデル検査自体 はすべて自動で行えるため，モデルを作ったあとはすべて自動で検証が行われる．