数理解析研究所講究録
第 1744 巻 2011 年 15-24

15

2010 年度冬の LA シンポジウム [3]

動的リアルタイムハイブリッド CEGAR による動的再構成可

能組込みシステムの設計検証
酒井

1

誠

*

山根

2.1

はじめに

智 \dag er

構文

変数評価と制約条件について定義する．
近年，組込みシステムの多機能化により，設計が複雑化している．また，ネットワークや動的再構成 定義 1(クロック評価)
可能プロセッサ等は動作中に構成が変化し，さらにを，非負の実数値を持つクロック変数の有限集合
ハイブリッド性を持つため，シミュレーションで安:$X$とする．このとき，$\nu$

全性を保証することが困難となってきている．この$Xarrow \mathbb{R}_{\geq 0}$を，任意のクロッ

ク変数に非負の実数を割り当てる関数と定義し，こ安全性を保証するためにはモデル検査が有効である$\nu[X’:=0|$ によっ
れをクロック評価と呼ぶ．また，が，モデル検査では，網羅的な探索を行うため状態空 て，集合の要素のクロック変数に対して間が大きくなり，メモリに載り切らないという状態 を，それ以外については と同じ評価値を割り当て
爆発が問題となっている．この問題の解決法として， ることを表す．さらに，$X$ のクロック評価の集合を
EMClarke らの抽象化精錬検証手法 (CEGAR) [2]で表すがある．また，ハイブリッドオートマトンに対する定義 2(サイクル評価)
検証手法 [1] もある．
$X’\subseteq X$

$0$

$\nu$

$\mathcal{V}x$$\square$を，非負の実数値を持つサイクル変数の有限集合
そこで本研究では，動的に構成が変化するモデルをを，任意のサイク
記述することができる動的線形ハイブリッドオートマ とする．このとき， :ル変数に非負の実数を割り当てる関数と定義し，こトンを提案し，また，その検証手法として，CEGARを拡張した動的線形ハイブリッド CEGAR を提案 れをサイクル評価と呼ぶ． のサイクル評価の集合
を碗で表す
する．
$C$

$\mu$

$Carrow \mathbb{R}_{\geq 0}$$C$$\square$2

動的線形ハイブリッドオートマ

定義 3(制約条件)
クロック，サイクル変数の制約条件を以下のように
定義する．

トン

$\phi$

ここでは，本稿で用いる仕様記述言語である動的

ハイブリッドオートマトンとその動作について定義$::=x_{1}\sim d|x_{1}-x_{2}\sim d|c\sim d|\phi_{1}\wedge\phi_{2}|$$c\in C,$
ただし，$==\}$ である．全ての制約条件の集合を$x_{1};x_{2}\in X,$$d\in \mathbb{Z},$$\sim\in\{<,$$\leq,$

true$>,$$\geq$$,$

する．表記のルールとして， を「定義する
$=$

$==$

*

\dag er$(^{d}=^{ef})J$,$:=$ を「代入」の意味で用いる．
を「等しい」，

金沢大学大学院自然科学研究科
金沢大学$\Phi(X\cup C)\square$とする

定義 4(変数の傾き)
各ロケーションへ割り付ける変数の傾きを以下のように定義する．
$f_{x}::=\dot{x}=m$16$m\in\{0,1\},\dot{x}\in\dot{X}$の$f_{x}$

は$x$の導関数 $dx/dt$ である．この集合を $F(X)$ とする．

はガード条件．

-$\phi\in\Phi$-$a!,$ $a?,$ $a_{\tau}\in Act$はアクションである．ただし，遷移とともにアクションを出力するアクションを $a!$$\int_{c};:=\dot{c}=n$$n\in N,\dot{c}\in\dot{C}$は$c$の周波数 $dc/dt$ である．この$f_{c}$

遷移するアクションを $a?$ , 内部アクションのを

集合を $F(C)$ とする．口
-動的線形ハイブリッドオートマトンは動作中の構成変化を生成消滅により表すことができるオート.

マトンである．生成消滅アクションの出力アクショ

ンに対する入カアクションはそれぞれ 1 つずつであ$T_{init}$

-

.
.
.
.
.
.
.

$T_{init},$

ロケーションの有限集合

$L$

.

-

$\phi$$T_{init}\subseteq L$

その要素

は初期ロケーション．

るオートマトンであり，生成アクションがある
オートマトンは，アクションにより生成され動を割り当てる関数

.

$f$

$f$

作し始めるオートマトンである．
$T_{end}\subseteq L\cross\Phi\cross Act_{out}$

その要素は $(l, \phi, a)$ で表される．

{ lowc}. ただし，lowx :flowc: $Larrow F(C)$ である．
$Act_{in}$アクションがない時，

そのオートマトンは既に生成され，動作してい.

. ここで，

そ

生成アクションがないオートマトンの場合は，アクションの有限集合 $Act=Act_{in}\cup Act_{out}\cup$$Act_{\tau}$$T_{init}\subseteq Act_{:n}\cross L$$l\in T_{init}$

各ロケーションに変数の傾きを与える関数$Larrow F(X)$ ,アクションがある時，期ロケーション．

サイクル変数の有限集合 $C$ .

$Flow=\{flowx\}\cup$は，以下のいずれかである．

$*l\in L$ は生成されたオートマトンの初クロック変数の有限集合 $X$ .

$I:Larrow\Phi(X\cup C)$

はリセットされるクロック変数の$T_{end}\rangle$

初期ロケーション $l_{0}\in L$ .

ロケーションに不変条件$\lambda\subseteq X$$*a\in Act_{in}$ は生成アクション．

$H=$
動的ハイブリッドオートマトンの構文 $H$ は，$T,$$X,$ $C,$で表される．
, Flow, Act,
$I$

と表す．

の要素は $(a, l)\in T_{init}$ で表される．

定義 5(動的線形ハイブリッドオートマトンの構文)$l_{0},$$a_{\tau}$

有限集合．

り，1 対 1 対応で生成消滅を行う．

$\langle L,$. 出力アクションを受け取りは入カアクションの有限集

合，Actou は出力アクションの有限集合，

は遷移元のロケーション．

-$l\in L$-$\phi\in\Phi$-$a\in Act_{out}$

はガード条件．

は消滅アクション．

$Act_{\tau}$$t$

これにより，指定されたオートマトンが消滅す

は内部アクションである．特に $Crt_{-}H_{n}\in Act$

る．

を生成するアクション，$Dst_{-}H_{n}\in Act$ はオートマトン
を消滅させはオートマトン$H_{n}$$H_{n}$.

口るアクションとする．

エッジの有限集合 $T\subseteq L\cross\Phi\cross Act\cross 2^{X}\cross L$ .
その要素は $(’ \phi, a, \lambda, l’)\in T$ で表され， はfflJ 1 (動的線形ハイブリッドオートマトンの例)$1$5 つの動的線形ハイブリッドオートマトン$a$$H_{1},$ $H_{2},$ $H_{3},$ $H_{4},$ $H_{5}$$q$$a!,$ $a?,$-$a_{\tau}$$l,$のいずれかである．

の例を図 1 に示す．斜めの. 印が付いたロケーションが初期ロケーションを表$l’\in L$ は遷移元及び遷移先ロケーション． し，生成アクションが付いていないオートマトン$*$

17以下に示すようなロケーション集合である．ま

た，

とする．

$L_{lf_{1}}^{\overline{*}}=L_{H_{1}}\backslash L_{H_{1}}^{*}$-に $Crt_{-}H_{2}$ ? アクションと $Dst_{-}H_{2}!$ ア$H_{2}$

クションがある場合，

は，$L_{H_{1}}$$L_{H_{1}}^{*}$$Crt_{-}H_{2}!$の中でアクションが付いている遷移の遷

移先ロケーションから $Dst_{-}H_{2}$ ? アクションが付いている遷移の遷移元ロケーションの間で到達可能なロケーション集合．
-$H_{2}$に $Crt_{-}H_{2}$ ? アクションがなく $Dst_{-}H_{2}!$アクションがある場合，$L_{H_{1}}^{*}$

で

は， の中
$L_{H_{1}}$から $Dst_{-}H_{2}$ ? アクションが付いて$l_{0H_{1}}$いる遷移の遷移元ロケーションの間で到達可能なロケーション集合．
-$H_{2}$に $Crt_{-}H_{2}$ ? アクションがなく $Dst_{-}H_{2}!$$Crt_{-}H_{2}$ ?
アクションがない場合，または，アクションがあり $Dst_{-}H_{2}!$ アクションがな.
.

図 1: 動的線形ハイブリッドオートマトンの例

は，最初から動作しているオートマトンである．図では$H_{1},$ $H_{2}$が最初から動作しているオートマトン

で，$H_{3},$ $H_{4},$ $H_{5}$は生成アクションにより生成され動

.

い場合，

$L_{H_{1}}^{*}=L_{H_{1}}$$l_{0H_{1}||H_{2}}=l_{0}^{*}$. ただし， は$l_{0}^{*}$$l_{0}^{*}=\{l_{0H_{1}}, l_{0H_{2}}\},$$H_{3},$ $H_{4},$ $H_{5}$にあるように，遷移先のロケーションがなく，遷移に消滅アクションが付いている遷移によりオートマ$X_{H_{1}||H_{2}}=X_{H_{1}}\cup X_{H_{2}}$$\circ C_{H_{1}||H_{2}}=C_{H_{1}}\cup C_{H_{2}}$

.
.

のとき

$l_{0H_{1}}\in L_{H_{1}}^{*}$$l_{0H_{1}}\not\in L_{If_{1}}^{*}$のとき$l_{0}^{*}=l_{0H_{1}}$とする．

$I_{H_{1}||H_{2}}=I^{*}$

.

$|$

.

. ただし． は，$I^{*}$$I^{*}=I_{H_{1}}\cap I_{H_{2}}$

作し始めるオートマトンである．また，

.

,

$F$

$L_{H_{1}}^{*}$$L_{lf_{1}}^{*}$に対しては

こ対しては $I^{*}=I_{H_{1}}$ とする．
$Flow_{H_{1}||H_{2}}=Flow^{*}$. ただし，$Flow*$ は，$L_{H_{1}}^{*}$

トンが消滅する．に対しては $Flow*=\{flow_{H_{1}}\}\cup\{flow_{H_{2}}\}$ ,定義 6 (動的線形ハイブリッドオートマトンの並列合成)

2 つの動的線形ハイブリッドオートマトン$H_{1},$ $H_{2}$の並列合成は，$\langle L_{H_{1}}||H_{2},$$H_{1}||H_{2}$$l0H_{1}|$として $H_{1}||H_{2}$I $H_{2},H_{1}||H_{2},||H_{2},$$IH_{1}|$I$H_{2}$$=$$L_{lf_{1}}^{\overline{*}}$

に対しては $Flow*=flow_{H_{1}}$ とする．

$Act_{H_{1}||H_{2}}$$=$$(Act_{H_{2}} \backslash Act_{in}$$(Ac_{d}t_{H_{1}} \backslash Act_{inoutH_{1}})$$utH_{2})$$\cup$。

,

し，$Act_{inoutH_{1}},$ $Act_{inoutH_{2}}$$Act_{\tau H_{1}||H_{2}}$$\cup$. ただ

は合成対象のオー$Flow_{H_{1}}||H_{2},H_{1}||H_{2},H_{1}||H_{2},initH_{1}||H_{2},endH_{1}||H_{2}$

トマトンに入カアクション及び出力アクション

によって定義される．ここでは， を新たに合成に対応したアクションが存在するアクションのする動的線形ハイブリッドオートマトンとする

有限集合であり，それらは並列合成後，内部ア$H_{2}$.

$L_{H_{1}||H_{2}}=L_{H_{1}}^{\overline{*}}\cup(L_{H_{1}}^{*}\cross L_{H_{2}})$. ただし，$L_{fi_{1}}^{*}$

はクションの有限集合$Act_{\tau H_{1}||H_{2}}$

となる．

18

.

$T_{H_{1}||H_{2}}\subseteq L_{H_{1}||H_{2}}\cross\Phi_{H_{1}||H_{2}}\cross Act_{H_{1}||H_{2}}\cross$$2^{X_{H_{1}||H_{2}}}\cross L_{H_{1}||H_{2}}$素$t$. ただし，$\Phi_{H_{1}||H_{2}}=\Phi_{H_{1}}\cup$$=2^{X_{H_{1}}\cup X_{H_{2}}}$$\Phi_{H_{2}}.2^{X_{H_{1}||H_{2}}}$は 2 つの遷移であり，その要$(l_{H_{1}}, \phi_{H\text{、}}, a_{H_{1}}, \lambda_{H_{1}}, l_{H_{1}}’)$$(l_{H_{2}}, \phi_{H_{2}}, a_{H_{2}}, \lambda_{H_{2}}, l_{H_{2}}’)$とに対して，以下の規則

によって決まる．
-$l_{H_{1}},$$l_{H_{1}}’$$L_{H}^{\overline{*}}$$\in$. のとき，$t$$(l_{H_{1}}, \phi_{H_{1}}, a_{H_{1}}, \lambda_{H_{1}}, l_{H_{1}}’)$-$l_{H_{1}},$$l_{H_{1}}’\in L_{H_{1}}^{*}$.

図 2: 動的線形ハイブリッドオートマトンの並列合

成の例

のとき，

$*a_{H_{1}}\in Act_{\tau H_{1}}$$Act_{inH_{1}}$$=$に $a_{H_{1}}\in$または，$H_{2}$$l_{H_{1}||H_{2}},$ $l_{H_{1}||H_{2}}’\in L_{H_{1}||H_{2}}$-もしくは $a_{H_{1}}\in Act_{outH_{1}}$ に

移先ロケーション．

$t=$
対応するアクションがないとき，$((l_{H_{1}}, l_{H_{2}}), \phi_{H_{1}}, a_{H_{1}}, \lambda_{H_{1}}, (l_{H_{1}}’, l_{H_{2}}))$$*a_{H_{2}}\in Act_{\tau H_{2}}$$Act_{inH_{2}}$

または，

.

$((l_{H_{1}}, l_{H_{2}}), \phi_{H_{2}}, a_{H_{2}}, \lambda_{H_{2}}, (l_{H_{1}}, l_{H_{2}}’))$.

かつそのアクション$*a_{H_{1}}\in Act_{inH_{1}}$に対応した $a_{H_{2}}\in Act_{outH_{2}}$に対応した $a_{H_{2}}\in Act_{inH_{2}}$$a\in Act_{\tau H_{1}||H_{2}}$は消滅アクション．

例 2(動的線形ハイブリッドオートマトンの並列合成の例)
図 1 のオートマトン$H_{1},$ $H_{3}$または，2 に示す．この例では，の並列合成の例を図$\{A_{2}\}$であるため，並列合成した後のロケーション集合$L_{H_{1}||H_{3}}=$

となる

また，ア

$=$

がある時，

$\{A_{1}, (A_{2}, a_{1}), (A_{2}, a_{2}), A_{3}, A_{4}, A_{5}\}$

そのアクションは $a\in Act_{\tau H_{1}||H_{2}}$ とな

り，$t=((l_{H_{1}}, l_{H_{2}}),$ $\phi_{H_{1}}\wedge\phi_{H_{2}},$ $a,$ $\lambda_{H_{1}}\cup$$T_{init}$-はガード条件．

$L_{H_{1}}^{*}$

かつそのアクション$a_{H_{1}}\in Act$ 。
$utH_{1}$.

$\phi_{H_{1}||H_{2}}\in\Phi_{H_{1}||H_{2}}$もしくは $a_{H_{2}}\in Act_{outH_{2}}$ に口$t=$対応するアクションがないとき，$\lambda_{H_{2}},$-に $a_{H_{2}}\in$$H_{1}$

は遷移元及び遷クション $Crt_{-}H_{3}$ , Dst-H3 は内部アクション集合$Act_{\tau H_{1}||H_{3}}$の要素となる．

$(l_{H_{1}}’, l_{H_{2}}’))$

2.2

は以下のいずれかである．

$-T_{1nit}\subseteq L_{H_{1}||H_{2}}\cross Act_{\tau H_{1}||H_{2}}\cross L_{H_{1}||H_{2}}$.

意味

次に，意味について定義する．

定義 7(動的線形ハイブリッドオートマトンの状態)される．動的線形ハイブリッドオートマトンの状態は $q=$

その要素 は $t=(l_{H_{1}||H_{2}}, a, l_{H_{1}||H_{2}}’)$ で表$t$$*l_{-\cdot 1}l’\in L_{H_{1}||H_{2}}$ は遷移先及

び遷移元ロケーション．
$*a\in Act_{\tau H_{1}||H_{2}}$-.

$T_{init}\subseteq L_{H_{1}||H_{2}}$は生成アクション．

その要素 $l_{H_{1}||H_{2}}\in T_{init}$.
.

$(l, \mu, \nu)$である．

$l\in L$ はロケーション．

$\mu$

:

$Carrow \mathbb{R}\geq 0$:
はロケーション．
．
$\nu$$T_{end}$$Act_{\tau H_{1}||H_{2}}$$t$$L_{H_{1}||H_{2}}$$\subseteq$$=$$\cross$$L_{H_{1}||H_{2}}$.

$\cross$$\Phi_{H_{1}||H_{2}}$その要素$(l_{H_{1}||H_{2}}, \phi_{H_{1}||H_{2}}, a, l_{H_{1}||H_{2}}’)$$t$$\cross$$Xarrow \mathbb{R}_{\geq 0}$

はサイクル評価．

はクロック評価．口定義 8(動的線形ハイブリッドオートマトンの意味)

は動的線形ハイブリッドオートマトン

で表さ$\langle L,$$l_{0},$$X,$ $C,$

$I$

れる．は，

, Flow, Act, $T,$$\mathcal{M}=(Q,$$\Rightarrow,$$q_{0}\rangle$$T_{init},$ $T_{end}\rangle$として定義される．

$H$

$=$

の意味

.
.

19
は状態

$Q$

$q$

の集合．意の状態$\Rightarrow$

は時間遷移

-

$\Rightarrow\delta$

と離散遷移

の和集合．

$\Rightarrow d$

在し，$\mu_{1},$

任意の状態
$\in$

$\mathbb{R}\geq 0$$(l, \mu_{)}\nu)$に対し，$\mu+flow_{C}(l)t$

$Q$

$\in$

$l’$

$\in I(l)$

$=$

$l$

$(l_{1}, l_{2})$からの工ツジ $((l_{1}, l_{2}), \phi, a, \lambda, l_{1}’)\in T$ が存

時間遷移

$t$

$((l_{1}, l_{2}), (\mu_{1}, \mu_{2}), (\nu_{1}, \nu_{2}))\in$

に対し，ロケーション$Q$$\mu_{2},$$\nu_{1},$$\nu_{2}$がを満たし，か$\phi$と時間経過

つ $\mu_{1}\in I(l’),$ $\nu_{1}’[\lambda:=0]\in I(l_{1}’)$ とな

かつ

るとき

$=$

$\mu’$

かつ $\nu’=\nu+$$((l_{1}, l_{2}), (\mu_{1}, \mu_{2}), (\nu_{1}, \nu_{2}))\Rightarrow d$である．状態集合$(l_{1}’, \mu_{1}’, \nu_{1}’)$$Q$

は $Q=$

から $Q=Q_{1}$ となる．
flowx $(l)t\in I(l)$ の時かつその時に限りである．ここで，は生成されている動的線$\overline{Q}_{1}^{*}\cup(Q_{1}^{*}\cross Q_{2})$$(l, \mu, \nu)\Rightarrow\delta(l, \mu’, \nu’)$-$Q_{1}$形ハイブリッドオートマトンの状態集

離散遷移

合であり， は消滅する動的時間オー$Q_{2}$

$*$

アクション

$a$

が生成，消滅アクション.

でない時，任意の状態 $(l, \mu, \nu)\in Q$
に対し，ロケーション からの工ッジ$l$$(’ \phi, a, \lambda, l’)\in T$

を満たし，かつが存在し，$\mu,$$\nu$

がトマトンの状態集合を表す．
$q_{0}\in Q$

は初期状態．

初期状態とは，初期ロケーション$\phi$$l_{0}$

において全てのサイクル評価及びクロック評価が$\mu\in 1(l’),$ $\nu’[\lambda:=0]\in$

$0$

の状態

である．

$I(l’)$ となるとき $(l, \mu, \nu)\Rightarrow d(l’, \mu’, \nu’)$

である．
口
$*$

アクション

$a$

が生成アクションの時，任意の状態
に対し，ロケーションッジ$l_{1}$$\nu_{1}$つ$I(l_{1}’),$$\mu_{1},$$\in$$\mu_{1}$

が

となるとき

$I(l_{1}’)$$\phi$

$\in$

$Q$

からの工

遷移系

$)$

$\mathcal{M}=\langle Q,$$q_{0}\rangle$$\Rightarrow,$

上の初期状態$q_{0}$から有限まをパスと定義する．
がたは無限列を満たし，か口$(l_{1}, \phi, a, \lambda, (l_{1}’, l_{2}))$

存在し，定義 9 パス$($$(l_{1,\mu_{1},\nu_{1})}$$\omega=q0\Rightarrow q_{1}\Rightarrow q_{2}\Rightarrow\cdots$

$T$

$\in$

$\nu_{1}’[\lambda := 0]$$(l_{1}, \mu_{1}, \nu_{1})$$\in$$\Rightarrow d$である．こ定義 10 (到達可能性問題)
動的線形ハイブリッドオートマトン

$H$

$=$

こで， は新たに生成された動的線
形ハイブリッドオートマトンの初期ロと望ま, Flow, Act,
しくないロケーションであるターゲットロケー$H$ の遷ションの集合 $L_{target}$ が入力されたとき，ケーションであり，移系$((l_{1}’, l_{2}), (\mu_{1}’, \mu_{2}), (\nu_{1}’, \nu_{2}))$$l_{2}$$\mu_{2},$

評価は

$0$

$\nu_{2}$のすべてのである．状態集合$\overline{Q}_{1}^{*}\cup(Q_{1}^{*}\cross Q_{2})$$Q$

は $Q=$となる．ここで，$Q_{1}^{*}$$\langle L,$$l_{0},$$X,$ $C,$ $I$$T,$ $T_{init},$ $T_{end}\rangle$$\mathcal{M}=\langle Q,$$\Rightarrow,$$q_{0}\rangle$

上でターゲットロケーショ

ン $l_{target}\in L_{target}$ を持つ状態 $q_{target}=(l_{target}, \nu)$に到達するパス$\omega_{ce}$が存在する場合，かつその時は既に生成されている動的線形ハイブに限り，出力は ”reachable” となり，それ以外はリッドオートマトンの生成アクション“not reachable” となる．出力が ”reachable” となが付いている遷移の遷移先の状態から消滅アクションが付いている遷移の遷るときのパス$\omega$$e$。

を反例と呼ぶ．口

移元の状態までの間で到達可能な状態
は
であり，
集合，
は新たに生成された動的線形ハイブリ$\overline{Q}_{1}^{*}=Q_{1}\backslash Q_{1}^{*}$$\overline{Q}_{1}^{*}$$*$$Q_{2}$

3

動的線形ハイブリッド CEGAR

ッドオートマトンの状態集合を表す．動的線形ハイブリッド CEGAR の流れは図 3 のよアクション が消滅アクションの時，任うな図で表される．
$a$20$\alpha((l, \mu, \nu))(i)=(l, \psi_{1}^{l}\mu, \psi_{i}^{l}\nu)$

また，具体化関数$\gamma$:$L\cross Barrow L\cross\Psi c\cup \mathcal{V}x$は以下のように定義される．
$\gamma((l, b))=\{(l, \mu, \nu)$$\in L\cross \mathcal{U}_{C}\cross \mathcal{V}_{X}|I(l)\wedge$

口$\bigwedge_{i=0}^{n-1}\psi_{i}^{l}\mu\equiv b^{l}(i)\wedge\bigwedge_{i=0}^{n-1}\psi_{\dot{\iota}}^{l}\nu\equiv b^{l}(i)\}$$rnM$$’\cdot\infty\alpha l$

抽象化述語と抽象化具体化関数を用いて抽象構造を構築する．抽象構造は，大き目の近似になるよ
うに構築する．大き目の近似とは，具体構造が持つ.

遷移を抽象構造に全て持たせることで，抽象化に健全性を持たせる近似である．

定義 13(抽象動的線形ハイブリッドオートマトン)$X,$ $C,$$H=\langle L,$に対す, Flow, Act,

図 3: 動的線形ハイブリッド CEGAR の流れ

3.1

る抽象動的線形ハイブリッドオートマトン $H^{A}=$

述語抽象化$(Q^{A},$ $q_{0}^{A},$

ここでは，述語抽象化について定義する．述語抽
象化は状態爆発を抑制するために用いられる手法であり，実数変数であるサイクル評価，クロック評価
を述語を用いて抽象化することにより状態爆発を抑制している．

定義 11(抽象化述語)
クロック変数の集合 $X$ に関する抽象化述語$\psi$を$::=true|x_{1}\sim n|x_{1}-x_{2}\sim n|c_{1}\sim n$$\psi$

I

.
.
.
.
.

と定義する．ただし，$u_{1},$ $u_{2}\in \mathbb{Z}\backslash \{0\},$ョン$n\in N,$$l$$\sim\in$$\{<, \leq, >, \geq\}$

抽象状態の有限集合

抽象初期状態$\gamma(l_{0}, b_{0}^{l_{0}})$$\Psi^{l_{n-1}}\}$-

はクロック変数の有限集合であり， は対応する$C$ はサイクル変数の有限集合
クロック評価の集合，であり， は対応するサイクル評価の集合であると$\mathcal{U}_{C}$

する．抽象化述語の有限集合$\Psi^{l}=\{\psi_{0}^{l}, \cdots, \psi_{n-1}^{l}\}$が与えられたとき，タイミング制約抽象化関数$L\cross \mathcal{U}_{C}\cross \mathcal{V}_{X}arrow L\cross \mathcal{B}$$\alpha$:は以下のように定義される．

.

$q^{A},$ $q^{\prime A}\in Q^{A}$. その要素は$a_{\tau}$$(q^{A}, a, q^{\prime A})$のいずれかである．

は遷移元及び遷移先抽象状$a\in Act^{A}$

はアクションである．ただし，遷移とともにアクションを出力するアクショ$\Psi=\{\Psi^{l_{O}}\cup\cdots\cup$$\mathcal{V}_{X}$$q0\in$. ただし，態である．

ンを $a!$ , 出力アクションを受け取り遷移す

とする．口

$X$

$\Psi$

で表され， は $a!,$ $a?,$$=$

定義 12(述語抽象化具体化)

.

とする．

$T^{A}\subseteq Q^{A}\cross Act^{A}\cross Q^{A}$とする．また，全てのロケーション

における抽象化述語の有限集合を$Q^{A}=L\cross \mathcal{B}$アクションの有限集合 $Act^{A}=Act$ .

-$\{\psi_{0}^{l}, \cdots, \psi_{n-1}^{l}\}$は次の要素からな$q_{0}^{A}=(l_{0}, b_{0}^{l_{O}})$

抽象化述語の集合である．ロケーシ$\Psi^{l}$$Act^{A},$ $T^{A},$ $T_{init}^{A},$ $T_{end}^{A}\rangle$$a$$x\in X,$ $c_{1},$ $c_{2}\in$における抽象化述語の有限集合を$\Psi,$

る．

$u_{1}c_{1}+u_{2}c_{2}\sim n|x_{1}+u_{1}c_{1}\sim n|-x_{1}+u_{1}c_{1}\sim n$$C,$$T,$ $T_{1nit},$ $T_{end}\rangle$$I$$l_{0},$るアクションを $a?$.

.

内部アクションを$a_{\tau}$と表す．
$T_{init}$-は以下のいずれかである．

アクションがある時 I
その要素は 2 つ組$*a\in Act_{in}^{A}$$T_{1nit}^{A}\subseteq Act^{A}\cross Q^{A}$$(a, q^{A})$で表される．

は生成アクション．

.

21
定義 14(抽象動的線形ハイブリッドオートマトンの並列合成)
2 つの抽象動的線形ハイブリッドオート

マトンの並列合成は，として$H_{1}^{A}||H_{2}^{A}$$\langle Q_{H_{1}^{A}||H_{2}^{A}}^{A},$ $q_{0H_{1}^{A}||H_{2}^{A}}^{A},$$\Psi_{H_{1}^{A}||H_{2}^{A}},$$T_{initH_{1}^{A}||H_{2}^{A}}^{A},$ $T_{endH_{1}^{A}||H_{2}^{A}}^{A}\rangle$

こでは，$H_{2}^{A}$.

$Act_{H_{1}^{A}||H_{2}^{A}}^{A},$$T_{H_{1}^{A}||H_{2}^{A}}^{A}$によって定義される．こを新たに合成する抽象動的線形ハイブ

リッドオートマトンとする．

. ただし，$Q_{H_{1}^{A}||H_{2}^{A}}^{A}=Q_{H_{1}^{A}}^{\overline{A}*}\cup(Q_{H_{1}^{A}}^{A*}\cross Q_{H_{2}^{A}}^{A})$$Q_{H_{1}^{A}}^{A*}$は以下に示すような抽象状態集合である．

また，

とする．

$Q_{H_{1}^{A}}^{\overline{A}*}=Q_{H_{1}^{A}}^{A}\backslash Q_{H_{1}^{A}}^{A*}$に $Crt_{-}H_{2}$ ? アクションと $Dst_{-}H_{2}!$ ア$H_{2}^{A}$-

クションがある場合$Q_{H_{1}^{A}}^{A*}$は，$Q_{H_{1}^{A}}^{A}$の中で $Crt_{-}H_{2}!$ アクションが付いている遷移の

遷移先抽象状態から $Dst_{-}H_{2}$ ? アクションが付いている遷移の遷移元抽象状態の間で到達可能な抽象状態集合．
に $Crt_{-}H_{2}$ ? アクションがなく $Dst_{-}H_{2}!$$H_{2}^{A}$-

アクションがある場合，$Q_{H_{1}^{A}}^{A*}$中では生成されたオートマトン$H_{2}^{A}$-

一アクションがない時，$T_{init}^{A}\subseteq Q^{A}$.

$q^{A}\in T_{init}^{A}$$T_{end}^{A}\subseteq Q^{A}\cross Act^{A}$. その要

は抽象初期状態．

. その要素は$(q^{A}, a)$

で表さ

れる．
$-$

$q^{A}\in Q^{A}$

は遷移元の抽象状態である．

$-a\in Act_{out}^{A}$

は消滅アクションである．
口から $Dst_{-}H_{2}$ ? アクションが付に $Crt_{-}H_{2}$ ? アクションがなく $Dst_{-}H_{2}!$アクションがあり $Dst_{-}H_{2}!$ アクションがな

.
.

.

い場合

例 3(抽象動的線形ハイブリッドオートマトンの例)
図 1 を述語 true によって述語抽象化すると図 4 のという無限の状態からようになり，動作は$(l, \mu, \nu)$( , true) という有限の状態で表現される．

$Q_{H_{1}^{A}}^{A*}=Q_{H_{1}^{A}}^{A}$$q_{0H_{1}^{A}|I^{H_{2}^{A}}}^{A}=q_{0}^{A*}$

のとき

とき

.

. ただし，$q_{0}^{A*}$$q_{0}^{A*}=\{q_{0H_{1}^{A}}^{A}, q_{0H_{2}^{A}}^{A}.\},$$q_{0}^{A*}=q_{0H_{1}^{A}}^{A}$}は$q_{0H_{1}^{A}}^{A}\in Q_{H_{1}^{A}}^{A*}$$q_{0H_{1}^{A}}^{A}\not\in Q_{H_{1}^{A}}^{A*}$のとする$\Psi_{H_{1}^{A}||H_{2}^{A}}=\Psi_{H_{1}^{A}}\cup\Psi_{H_{2}^{A}}$.

$Act_{H_{1}^{A}||H_{2}^{A}}^{A}=(Act_{H_{1}}^{A}\backslash Act_{inoutH_{1}}^{A})\cup(Act_{H_{2}}^{A}\backslash$$Act_{in}^{A}$$l$の$Crt_{-}H_{2}$ ?
アクションがない場合，または，の抽象初期状態．

素$Q_{H_{1}^{A}}^{A}$

いている遷移の遷移元抽象状態の間で到達可能な抽象状態集合．

図 4: 抽象動的線形ハイブリッドオートマトンの例$*q^{A}\in Q^{A}$$q_{0H_{1}^{A}}^{A}$は，$utH_{2})\cup Act_{\tau H_{1}||H_{2}}^{A}$。

$Act_{in}^{A}$$utH_{2}$。

. ただし，$Act_{inoutH_{1}}^{A}$,

は合成対象のオートマトン中に入力

アクションおよび出力アクションに対応したアクションが存在するアクションの有限集合であり，それらは並列合成後，内部アクションの有となる．
限集合 $Act^{A}$$\tau H_{1}||H_{2}$

,

22

.

.

$T_{H_{1}^{A}||H_{2}^{A}}^{A}\subseteq Q_{H_{1}^{A}||H_{2}^{A}}^{A}\cross Act_{H_{1}^{A}||H_{2}^{A}}^{A}Q_{H_{1}^{A}||H_{2}^{A}}^{A}$

その要素$t^{A}$

は 2 つの遷移て決まる．
$q_{H_{1}^{A}}^{A},$$q_{H_{1}^{A}}^{\prime A}$,$Q_{H_{1}^{A}}^{\overline{A}*}$.

$=$のとき，図 5: 抽象動的線形ハイブリッドオートマトンの例$q_{H_{1}^{A}}^{\prime A}\in Q_{H_{1}^{A}}^{A*}$または，$H_{2}^{A}$$*a_{H_{1}}\in Act_{\tau H_{1}^{A}}$もしくは$Act_{inH_{1}^{A}}$のとき，$t^{A}$$\in$$(q_{H_{1}^{A}}^{A}, a_{H_{1}}A, q_{H_{1}^{A}}^{\prime A})$$-q_{H_{1}^{A}}^{A}$とに対して，以下の規則によっ$(q_{H_{2}^{A}}^{A}, a_{H_{2}^{A}}, q_{H_{2}^{A}}^{\prime A})$-$(q_{H_{1}^{A}}^{A}, a_{H_{1}^{A}}, q_{H_{1}^{A}}^{\prime A})$に $a_{H_{1}}\in$$a_{H_{1}^{A}}\in Act_{outH_{1}^{A}}$に一$((q_{H_{1}^{A}}^{A}, q_{H_{2}^{A}}^{A}),$$(q_{H_{1}^{A}}^{\prime A}, q_{H_{2}^{A}}^{A})$$a_{H_{1}^{A}},$または，$H_{1}^{A}$$*a_{H_{2}^{A}}\in Act_{\tau H_{2}^{A}}$もしくは$Act_{inH_{2}^{A}}$

に

.

$A$

$\in Act_{inH_{1}^{A}}$$*a_{H_{1}^{A}}$$\prime A$$A$$a_{H_{2}^{A}},$ンに対応した$(q_{H_{1}^{A}}, q_{H_{2}^{A}})$.

$Act_{outH_{2}^{A}}$の$a_{H_{1}^{A}}\in Act_{outH_{1}^{A}}$

か

$\in$

とき，または，$Act_{inH_{2}^{A}}$

は

$a$

$\in$

$a_{H_{2}^{A}}\in$がある時，そのアクションとなり，.

$t^{A}$$Act_{\tau H_{1}^{A}||H_{2}^{A}}$$((q_{H_{1}^{A}}^{A}, q_{H_{2}^{A}}^{A}),$ $a,$口例 4(抽象動的線形ハイブリッドオートマトンの並列合成の例)
図 4 のオートマトン$=$の並列合成の例を図 5$H_{1},$ $H_{3}$に示す．この例では，$Q_{A}^{A*}=$$H_{1}${($A_{2}$, true)} である

ため，並列合成した後の抽象状態集合$\{$

つそのアクションに対応したは消滅アクション．

にかつそのアクショ$a_{H_{2}^{A}}$は遷移元$a_{H_{2}^{A}}\in$$a_{H_{2}^{A}}\in Act_{outH_{2}^{A}}$$A$$q_{H_{1}||H_{2}^{A}}^{\prime A_{A}}\in Q_{H_{1}^{A}||H_{2}^{A}}^{A}$$-a_{H_{1}^{A}||H_{2}^{A}}\in Act_{\tau H_{1}^{A}||H_{2}^{A}}^{A}$$t^{A}=$
対応するアクションがないとき，$((q_{H_{1}^{A}}, q_{H_{2}^{A}}),$$q_{H_{1}^{A}||H_{2}^{A}}^{A},$及び遷移先抽象状態．

対応するアクションがないとき，$t^{A}=$(($A_{1}$$A_{4}$, true), (, true), ($Crt_{-}H_{3},$$(A_{2},$ $a_{1})$$A_{5}$, true), true), ($(A_{2},$ $a_{2})$, true), ($A_{3}$, true),となる．また，アクション$\}$

は内部アクション集合$Dst.H_{3}$$Q_{H_{1}^{A}||H_{\theta}^{A}}^{A}=$$Act_{\tau H_{1}^{A}||H_{3}^{A}}^{A}$の要素となる．

$(q_{H_{1}^{A}}^{\prime A}, q_{H_{2}^{A}}^{\prime A})$

定義 15(抽象動的線形ハイブリッドオートマトンの意味)$T_{initH_{1}^{A}||H_{2}^{A}}$は以下のいずれかである$-T^{A}$

動的線形ハイブリッドオートマトン$l_{0},$$\langle L,$

2A その要素$\subseteq Q_{H^{A}||H^{A}}^{A}\cross Act_{H^{A}||H^{A}}^{A}\cross$$Q_{H_{1}^{A}||H_{2}^{A}}^{A}initH_{1}^{A}||H$$q_{H_{1}^{A}||H_{2}^{A}}^{\prime A})$$a_{H_{1}^{A}||H_{2}^{A}},$$t^{A}$

は$t^{A}=(q_{H_{1}^{A}||H_{2}^{A}}^{12}A$,$,$$X,$ $C,$ $I,$ $f$を表す遷移系

low, Act,$\mathcal{M}=\langle Q,$$\Rightarrow,$$q_{0}\rangle$が与えられたとき，抽象動的線形ハイブリッド
としてオートマトンの意味は$\Psi$

で表される．

$q_{H_{1}^{A}||H_{2}^{A}}^{\prime A}\in Q_{H_{1}^{A}||H_{2}^{A}}^{A}lf$

移先及び遷移元抽象状態．
$*a_{H_{1}^{A}||H_{2}^{A}}\in Act_{\tau H_{1}^{A}||H_{2}^{A}}^{A}$$T_{initH_{1}^{A}||H_{2}^{A}}$$\subseteq$

は生成アクシ

$Q_{H_{1}^{A}||H_{2}^{A}}^{A}$$q_{H_{1}^{A}||H_{2}^{A}}^{A}\in T_{initH_{1}^{A}||H_{2}^{A}}$

その要素は抽象状態．

.
.

.

$Q^{A}=L\cross \mathcal{B}$

遷移関係は以下のいずれかである．
-

アクションが生成，消滅アクションでない時，$(l, b^{l})$$\mathcal{U}_{C},$. その要$\not\equiv_{\backslash }^{1}t^{A}AH^{A}||H_{2}^{A}\cross Act_{H||H_{2}^{A}}^{A_{A}}$$t^{A^{1}}=\cross$$T_{endH_{1}^{A}||H_{2}^{A}}^{A}Q_{H_{1}^{A}||H_{2}^{A}}^{A}$$(q_{H_{1}^{A}||H_{2}^{A}}^{A}, a_{H_{1}^{A}||H_{2}^{A}}, q_{H_{1}^{A}||H_{2}^{A}}^{\prime A})$は$\Rightarrow^{\mathcal{A}_{q}},0\rangle$

遷定義される．

ョン．
-

$=$

と抽象化述語の集合$\mathcal{M}^{\mathcal{A}}=(Q^{\mathcal{A}},$$*q_{H_{1}^{A}||H_{2}^{A}}^{A},$

$H$

の動作

$T,$ $T_{lnit},$ $T_{end}\rangle$ョ$\nu’$$\nu,$$\Rightarrow^{A}$$\in$$(l’, b^{l’})iff$$\mathcal{V}_{X}$

$st$

ョ

$\mu,$$\mu’$$\in$$((l, \mu, \nu)$$\in\in$$\gamma((l, b^{l})))$

で表される．

$\wedge$$((l’, \mu’, \nu’)$$\gamma((l’, b^{l’}))).(l, \mu, \nu)\Rightarrow(l’, \mu’, \nu’)$.

23
一アクションが生成アクションの時，$\Rightarrow^{A}$$(l_{1}, b^{l_{1}})$ョ$\mu_{1},$$\mu_{1}’,$$\mu_{2}\in \mathcal{U}_{C},$ョ$\nu_{1},$$\nu_{2}\in \mathcal{V}_{X}s.t$$\nu_{1}’,$$\gamma(\Rightarrow^{A})$

.

.

A

$\gamma(((l_{1}’, l_{2}), (b^{l_{1}’}, b^{l_{2}})))).(l_{1}, \mu_{1}, \nu_{1})\Rightarrow$

ここで，

.

$\in$

$(l’, b^{l’})\wedge(l, \mu, \nu)$$\Rightarrow^{A}$

$\in$

.

$\gamma((l, b))\wedge(l’, \mu’, \nu’)\in\gamma((l_{)}b^{l’}))\}$

アクションが生成アクションの時，$\gamma(\Rightarrow^{A})=$$\{((l_{1}, \mu_{1}, \nu_{1}), ((l_{1}’, l_{2}), (\mu_{1}’, \mu_{2}), (\nu_{1}’, \nu_{2})))\in Q|$ョは新たに生成された抽象$(l_{2}, b^{l_{2}})$$\{((l, \mu, \nu), (l’, \mu’, \nu’))$$=$$Q|\exists b^{l},$ $b^{l’}.(l, b^{l})$$(((l_{1}’, l_{2}), (\mu_{1}’, \mu_{2}), (\nu_{1}’, \nu_{2}))\in$$((l_{1}’, l_{2}), (\mu_{1}’, \mu_{2}), (\nu_{1}’, \nu_{2}))$

アクションが生成，消滅アクションでな

い時，

$iff$

$((l_{1}’, l_{2}), (b^{l_{1}’}, b^{l_{2}}))$$((l_{1}, \mu_{1}, \nu_{1})\in\gamma((l_{1}, b^{l_{1}})))$$\circ$$b^{l_{1}},$$b^{l_{1}’},$$b^{l_{2}}$.

$(l_{1}, b^{l_{1}})\Rightarrow^{A}((l_{1}’, l_{2}), (b^{l_{1}’}, b^{l_{2}}))\wedge(l_{1}, \mu_{1}, \nu_{1})\in$

動的線形ハイブリッドオートマトンの初$\gamma((l_{1}, b^{l_{1}}))$

期状態である．また，抽象状態集合
は $Q^{A}=Q_{1}^{\overline{A}*}\cup(Q_{1}^{A*}\cross Q_{2}^{A})$$Q^{A}$

となる．こ

こで，

は既に生成されている抽象動
的時間オートマトンのせいせアクション$Q_{1}^{A*}$.

$((l_{1}’, l_{2}), (\mu_{1}’, \mu_{2}), (\nu_{1}’, \nu_{2}))$$\wedge$$\in$.

$\gamma(((l_{1}’, l_{2}), (b^{l_{1}’}, b^{l_{2}})))\}$

アクションが消滅アクションの時，$\gamma(\Rightarrow^{A})=$$\{(((l_{1}, l_{2}), (\mu_{1}, \mu_{2}), (\nu_{1}, \nu_{2})), (l_{1}’, \mu_{1}’, \nu_{1}’))\in Q|\Rightarrow^{A}$が付いている遷移の遷移先の状態から消滅アクションが付いている遷移の遷移元の状態までの間で到達可能な状態集合，$Q_{1}^{\overline{A}*}$は$Q_{1}^{\overline{A}*}=Q_{1}^{A}\backslash Q_{1}^{A*}$であり，$Q_{2}^{A}$ョ$b^{l_{1}},$$(l_{1}’, b^{l_{1}’})$$b^{l_{1}’},$$b^{l_{2}}.((l_{1}, l_{2}), (b^{l_{1}}, b^{l_{2}}))$$((l_{1}, l_{2}), (\mu_{1}, \mu_{2}), (\nu_{1}, \nu_{2}))$$\wedge$$\gamma(((l_{1}, l_{2}), (b^{l_{1}}, b^{l_{2}})))$

は$\gamma((l_{1}’, b^{l_{1}’}))\}$$\in$$(l_{1}’, \mu_{1}’, \nu_{1}’)$$\wedge$$\in$.

新たに生成された抽象動的時間オートマ
トンの状態集合を表す．

口一アクションが消滅アクションの時， 定義 17(抽象パス)$\Rightarrow^{A}$$((l_{1}, l_{2}), (b^{l_{1}}, b^{l_{2}}))$

ョ$\mu_{1},$$\mu_{1}’,$$\mu_{2}\in \mathcal{U}_{C},$ョ$\nu_{1},$$\nu_{1}’,$$(l_{1}’, b^{l_{1}’})$

遷移系

$iff$

$\nu_{2}\in \mathcal{V}_{X}s.t$$(((l_{1}, l_{2}), (\mu_{1}, \mu_{2}), (\nu_{1}, \nu_{2}))$有限または無限列.
$\in$$\gamma(((l_{1}, l_{2}), (b^{l_{1}}, b^{l_{2}}))))\wedge((l_{1}’, \mu_{1}’, \nu_{1}’)$$\in$$\gamma((l_{1}’, b^{l_{1}’}))).((l_{1}, l_{2}), (\mu_{1}, \mu_{2}), (\nu_{1}, \nu_{2}))$$\Rightarrow(l_{1}’, \mu_{1}’, \nu_{1}’)$

ここで，.
は消滅する抽象動的時間

オートマトンの状態である．抽象状態集$Q^{A}$

は $Q^{A}=Q_{1}^{\overline{A}*}\cup(Q_{1}^{A*}\cross Q_{2}^{A})$ から$Q^{A}=Q_{1}^{A}$となる．ここで，$Q_{1}^{A}$は生成されている抽象動的時間オートマトンの状態集合であり， は消滅する抽象動的時
間オートマトンの状態集合を表す．
$Q_{2}^{A}$.

$q_{0}^{A}=(l_{0}, b_{0}^{l_{O}})$.

定義 16(遷移関係の具体化)
遷移関係を具体化する関数
うに定義する．
$\Rightarrow^{A}$$\gamma(\Rightarrow^{A})$を以下のよ

上の抽象初期状態から$\omega^{AAAAAAA}=q_{0}\Rightarrow q_{1}\Rightarrow q_{2}\Rightarrow\cdots$を口

定義 18(抽象反例)
動的線形ハイブリッドオートマトン
Flow, Act, $T,$

$T_{ii}nt,$ $Tend\rangle$

$H$

$=$

と タ

–

ゲットロケーションの集合 $Ltarget$ が入力された

とき， の抽象構造$H$$\mathcal{M}^{A}=$$\langle Q^{A},$

ターゲットロケーション ltarget

抽象ターゲットロケーション$q_{target}^{A}=(l_{target}^{A}, b^{l_{targ\epsilon t}^{A}})$象反例と呼ぶ32
口$q_{0}^{A}\rangle$

抽象パスと定義する$(L,$ $l_{0},$ $X,$ $C,$ $I,$$(l_{2}, b^{l_{2}})$合$\mathcal{M}^{A}=\langle Q^{A},$ $\Rightarrow^{A},$$\in$$\Rightarrow^{A},$$q_{0}^{A}\rangle$

上でLtarget を含む$l_{target}^{A}$を持つ状態に到達するパス$\omega_{ce}^{A}$を抽口到達可能性解析

到達可能性解析では，抽象反例が存在するかどうかを深さ優先探索で解析する．解析では，抽象反例が見つかった時点で次で説明する反例解析を行う．

24
3.3

達しないならば ”not reachable”, 到達するならば

反例解析

ここでは，抽象反例が具体モデル上で再現できる”reachable” を出力する．

かを調べる．具体的には，抽象反例
を具体モデ [証明] 抽象構造は大き目の近似になるように構築
ル上で辿り，各抽象状態の具体化がある，すなわち， しているため，到達可能性解析で到達不可能ならば$\omega_{ce}^{A}$$\Rightarrow\in\gamma(\Rightarrow^{A})$となるような元の遷移系における反例

また，到達可能性解析で到達可能となった場合は反. 計算法としては，夕一

例解析で具体構造上で解析を行うため，抽象化を行
口わない場合と等しい結果が得られる$\omega_{ce}=q0\Rightarrow\cdots\Rightarrow q_{i}\Rightarrow\cdots\Rightarrow q_{target}$

定する

$($

ただし $q_{i}=(l_{i},$$\zeta_{i}))$”not reachable’t と判定できる．

が存在するかを 」’$\not\simeq$$|$

ゲットから後方に向かって，現在の状態に遷移可能な状態集合を求めていく．これは最弱前条件 [3] の考
え方に基づいている．また，遷移に生成アクション
まとめがある場合，そのオートマトンは生成される前の構 4成になるため，使用されている変数を削除する．こ
本稿では，動作中に構成が変化するハイブリッドシの時点の領域が削除対象となる変数がすべて 0 といステムに対して有効な動的線形ハイブリッド CEGAR
う領域を含まれなければ抽象反例は再現できない偽の提案を行った．提案法では，現在動作しているオー反例である．遷移に消滅アクションがある場合，そ トマトンのみを並列合成して検証を行えるように動のオートマトンで使用される変数 $X\cup C$ に対して領的線形ハイブリッドオートマトンを提案し，到達可域をとして追加する．これらの操作を行い， 能性解析時に動作中のオートマトンを並列合成でき初期状態を含む集合が得られたら，反例であること るような仕組みを考案した．
が分かる．途中で空集合となったときは，その抽象
今後の課題として実装実験を行い，定量的なデー
反例は具体モデルでは再現できないので，偽反例で タから本稿の有効性を確認することがあげられる．
$\mathcal{V}_{X}\mathcal{U}_{C}$あることが分かる．

3.4

参考文献

精錬

[1] Alur, R., Dang, T., and, F.:Counterexample-guided predicate abstractionof hybrid systems, Theoretical Computer Science, Vol. 354(2006), pp. 250-271.
$Ivan\hat{c}i\acute{c}$ここでは，精錬について説明する．精錬では，反例
解析で偽反例と判定された抽象反例が再び現れない
ように述語を追加し，抽象状態を分割する．例えば以下のような抽象反例$\omega_{ce}^{A}$の$q_{0}^{A}\Rightarrow^{A}\cdots\Rightarrow^{A}q_{j}^{A}\Rightarrow^{A}$について，反例解析によって[2] Clarke, E. M., Grumberg, O., Jha, S., Lu, Y.,という遷移の部分で偽反例になったとする．こand Veith, H.: Counterexample-Guided Ab-$\Rightarrow^{A}q_{last}^{A}$$q_{k+1}^{A}$のとき，$q_{k+1}^{A}$$q_{k}^{A}\Rightarrow^{A}$の状態には， から遷移できる状態$q_{k}^{A}$

集合と遷移できない状態集合が存在すると考えられstraction Refinement, LNCS, Vol. 1855(2000),
pp. 154-169.

る．このことから反例解析で空ゾーンとなる直前の$q_{k+1}^{A}$の状態を分割することで，同一の反例を消すこ [3] Henzinger, T. A., Nicollin, X., Sifakis, J., andとができる．

定理 1(提案 CEGAR の正当性)
動的時間オートマトン群とターゲットロケーションが入力されたとき，提案 CEGAR はターゲットに到

Yovine, S.: Symbolic model checking for realtime systems, Infomation and Computation
111 (2), 1994, pp. 193-244.