CPS の形式検証——超準解析によるアプローチz蓮尾 一郎 （東京大学 情報理工学系研究科）
sm ，末永 幸平 （京都大学 情報学研究科）

2014 年 8 月

離散的形式検証「ジャンプ」
ダイナミクス??と

図 1: ハイブリッドシステムの例．加速度 a0 で直線運??

動する列車が，z = m の位置にあるカベに安全距離 s より近づくと加速度 −b で減速する．

1

連続的「フロー」ダイナミクス

制御理論・力学系理論

図 2: ハイブリッドシステム研究における 2 つのア

はじめにプローチ．形式検証は元来，プログラム実行結果に代表多くのサイバーフィジカルシステム（以下 CPS） される離散ダイナミクスを解析対象としてきた．その諸成は物理系としての連続的「フロー」と，計算機によ果がハイブリッドシステムに応用されつつある．

る離散的「ジャンプ」の 2 種類のダイナミクスを持ち，特にこの側面に注目した場合ハイブリッドシスとなり，サイバーフィジカルシステムの品質保証問テムとよばれる．

題の（初歩的な）一例になっている．この問いに答

最初に例を挙げておこう．正の定数 a0 , b, s のもと

えるには，ダイナミクスに現れるフロー（等加速度で図 1 のダイナミクスを考える．これは（位置 z =運動）及びジャンプ（加速度のスイッチング）の両m − s でのスイッチングにより）ハイブリッドシステムとなり，正確には次の微分方程式で表現される．
żv̇

= v{a0 （m − z ≥ s のとき）=−b （m − z < s のとき）方を解析する必要がある．
ハイブリッドシステムは「離散，ジャンプ」と「連続，フロー」のハイブリッドであるから，その研究(1)には大きく 2 つのアプローチ——離散からスタート，または，連続からスタート——が自然に存在する（図この例において「列車はカベにぶつからずに停止す2）．読者の多くの背景は制御理論であると思われるるか？」という自然な問題を考えよう．より正確にが，本解説はこのうち前者のアプローチ——フロー問題を述べると，から始める制御理論的アプローチとは逆の，ジャンプから始めるアプローチ——の解説である．特に本列車がカベにぶつからずに停止するために，解説では，筆者らによる超準解析を用いた論理的ア位置及び速度の初期値 z0 , v0 がみたすべきプローチ——数学的・論理的に厳密な形でフローを条件は？

ジャンプに変換する——に重点をおいて解説する．

1

n := N;// := は変数への値の代入をあらわす 在産業界で多く用いられるのはは「いくつかの入力
k := 1;をテストケースとしてシステムを実行してみて，間while (n > 0) {違いがないかチェックする」というテストの手法であk := k * n;n := n - 1 }る．しかしながらテストではテストケース以外の入

1
2
3
45

力に対しては「正しさの状況証拠」しか得られない．
図 3: プログラムの例．N の階乗 N ! を計算することは対照的に，「システムがあらゆる入力に対して正しく直感的には明らかだが，そのことを数学的に「証明」でき動作する」ことを数学的に証明しようというのが形るだろうか？

式検証 (formal verification) という営みである 1 ．
形式検証における数学的な議論及び証明のために

本解説の構成は以下のとおりである．まず，離散は，登場人物——対象となるシステム，そのふるまダイナミクスの品質保証法としての形式検証とよばい，及び要請される「正しさ」——をすべて形式的れるトピックについて，理論計算機科学の立場からに記述する 2 必要がある．特に「正しさ」が何を指す概説する．実感をもってもらうため，特にプログラのかを形式的に記述したものを仕様 (specification)

ム論理によるプログラム検証を具体的に説明する． とよぶ．
次に，形式検証を「ハイブリッド化」するためのい本節冒頭の例に戻ろう．図 3 のプログラムに対し，くつかの試みを紹介した後（これらは陽に微分方程そのふるまいは明らかなものとして，仕様としては式を導入する），著者らによる超準解析によるアププログラムの実行終了後の変数 k の値は N ! (2)ローチを述べる（ここではフローをジャンプに変換してしまうため，微分方程式があらわれない）．そという性質を考えよう．この形式検証問題を解きたいの数学的・論理的正当性を解説するための十分な紙のだが，ここではもう少し欲ばって，他の同種の形式幅はないが，最後に超準解析の入門も兼ねて概略の検証問題にも適用可能であるような「スジのよい」や説明を試みる．

り方——実世界の巨大な計算機システムにもスケールするようなやり方——を追求したい．さらにすす2

めて証明を自動生成してくれるようなアルゴリズム

形式検証——プログラム論理をができれば，計算機システムの品質保証における（人例に的）コストを劇的に圧縮することができる．これを可能にするのが，ループ不変性質 (loop invariant) と

図 3 のプログラムが N の階乗 N ! = N · (N − 1) ·いうアイデアであり，またホーア論理というプログ· · · · 1 を計算することは直感的には明らかであろう．
ラム検証のための論理体系——プログラム論理——
しかしこのことに対して，（たとえば幾何学の証明である．のような）数学的な証明を与えることはできるだろうか？
図 3 のような小さな例はともかく，計算機が社会3のあらゆる場面で重要な役割を果たす現代においてループ不変性質

は，設計した計算機システム——単体のプログラム

図 3 のような while ループを含むプログラムの検のような小さな例から，多数のサーバが協調して並証における最大の問題は，ループの中身の実行回数列に動作する大規模ネットワークまで——が期待通の見積もりの困難さである．図 3 では簡単であるがり動作するかという問題は，人命や大きな経済的損

1 この文脈での「形式 formal」という言葉は，正確には「記号列の操作に基づいた」という意味だが，おおざっぱに「数学的な，数学的に正確な」と読みかえてもよい．
2 前注と同様，「数学的に定義する」の意．

失に関わる非常に重要な問題である．
この問題（計算機システムの品質保証）に対し，現2一般にはとてもむずかしく，特にループ実行が停止という事実が得られる．この事実 (8) がループ不変するかどうか（停止問題）は計算機に判定できない

性質の定義 (3) から従うことは明らかであろう．

決定不能問題の代表例になっている．

最後に，ループ不変性質 (4) を用いて，図 3 のプ

この際に用いられるのがループ不変性質とよばれログラムの仕様 (2) に対する検証——すなわち，仕る概念である．ループ不変性質とは，ループの中身様をみたすことの数学的証明——を行う．ループのの実行の前後で保存される性質，すなわち実行開始前（2 行目の後）では n = N かつ k = 1 ゆえ等式 (4) が成立する．等式 (4) はループ不変性質「ループの中身の実行の前に成立するならば，であるから，(8) より同じ等式がループの実行終了実行後にも成立する」ことが保証されている

後（5 行目の後）でも成立する．ループの実行終了後(3)にはループの実行条件 n > 0 が成立しないはずであような性質のことをよび，これによってループの中る——そうでなければループ実行が終了しない——

身の実行回数に依存しないプログラムの解析が可能

ゆえに n = 0 が成立する 3 ．よって等式 (4) においになる．て n = 0 とすると，0! = 1 ゆえ k = N! が成立する．

さっそく例をあげよう．図 3 中のループに対して証明終．

は，等式k · (n!) = N!

(4)

4がループ不変性質である．等式 (4) がループ不変性質になることはすぐに確かめられる： 実際，ルー

読者は前節の証明を見てどのように感じられただ

プの中身の実行前・実行後の k と n の値をそれぞれろうか．ループ不変性質 (4) が天下り的に与えられkold , nold , knew , nnew とし，実行前に等式 (4) が成立すると仮定すると，kold · (nold !) = N!

ホーア論理

たことをのぞけば 4 ，議論は本質的に単純で機械的であるという印象を持たれたのではないだろうか．こ(5)の機械的推論を，記号のパターンマッチと書き換え

knew = kold · nold （ループの中身より）による論理体系として整理したのが，計算機科学者(6)

C.A.R. Hoare によって 1969 年に提案されたホーア（仮定より）

nnew = nold − 1

論理 (Hoare logic) である．

（ループの中身より）ホーア論理の系統だった記述は教科書 [4] などにゆ(7)

ずるとして，まず前節の証明をホーア論理で形式化したものを見てみよう（図 4）．この例を用いてホーがそれぞれ成立し，これらから次を得る．

ア論理の形式的証明について説明する．

()
(6,7)
knew · (nnew !) = (kold · nold ) · (nold − 1)!
簡単な計算=• ホーア論理の形式的証明は，各頂点にホーアトリプル (Hoare triple){ } { }A c B があり，各辺が導出規(5)kold · (nold !) = N!

を得る．ゆえに等式 (4) はループ不変性質となる．

則の適用であるような木である．

性質 A がループ不変性質であることの重要な帰結

たとえば図 4 の形式的証明のもつとして，木構造は右の通り

ループの実行開始前（図 3 の 2 行目の後）に成立すれば，ループの中身の実行回数にかかわらず，ループの実行終了後（5 行目

3 変数の値が常に非負整数であることを暗黙の仮定として用いた．
4 実際，プログラム検証においてはループ不変性質の発見が最大の問題であり，数多くのヒューリスティックスが研究されている．

(8)の後）でも成立する

3

{


k · (n!) = N!
 ∧n>0 ⇒
k · n · (n − 1)! = N!

{
[k=1∧n=N⇒ k · (n!) = N!

]{{(代入)}
k · n · (n − 1)! = N!
{ k := k ∗ n}k · (n − 1)! = N!

k · n · (n − 1)! = N!

k · (n!) = N! ∧ n > 0

k · (n!) = N!
{{(代入)}k · (n − 1)! = N!
{ n := n − 1 }k · (n!) = N!

} k := k ∗ n; {}k · (n!) = N!
n := n − 1} k := k ∗ n; {}k · (n!) = N!
n := n − 1} while(n > 0){{}k · (n!) = N! ∧ ¬(n > 0)
k := k ∗ n; n := n − 1}k=1∧n=N(逐次合成)(単調性)(While)[k · (n!) = N!
∧¬(n > 0)⇒ k = N!

} while(n > 0){{}k = N!
k := k ∗ n; n := n − 1}{ } { }

図 4: ホーア論理による形式的証明の例．各頂点にホーアトリプル A c B があり，各辺が導出規則の適用であるような「木」になっている．

である．
（ただし大括弧 [· · · ] で囲まれた論理式

以下，ホーア論理の「キモ」であるところの導出規は付帯条件であり，ここでは木の頂点としては則について説明しよう．まず，図 4 で 2 回適用され数えない．後で (単調性) 規則と一緒に詳しくている (単調性) 規則は次のようなものである．

説明する．
）

A ⇒ A′• ホーアトリプルとは，性質 A, B とプログラム{ } { }
c を中括弧で区切って書いた 3 つ組 A c B{} { }A′ c B ′{ } { }A c B

B′ ⇒ B(単調性)

ここで A ⇒ A′ は「性質 A が A′ を含意する」ことのことをいう．その意味するところはを意味する付帯条件であり 5 ，プログラムの事前・事

性質 A が成立する状態からプログラ

後条件について言明する（動的な）ホーアトリプル

ム c を実行すると，停止後には性質とは違い，静的な事実の言明である．図 4 で用いらB が成立する

れる 3 つの付帯条件がすべて真であることは明らかであろう．

であり，ゆえに A を事前条件 (precondition) ，B導出規則はすべて上から下に読む．ゆえに (単調を事後条件 (postcondition) とよぶ．たとえば{}{}n = 3 n := n + 1 n = 4性) 規則の直感的な意味は次のようになる．
{ } { }
ホーアトリプル A′ c B ′ がすでに証明(9)は真であるホーアトリプルの例である．

• 図 4 の形式的証明では，導出規則を（機械的に）適用することで，真であるホーアトリプルを上から次々に導出して，最後に一番下の頂点（木できていれば，その事前条件を強め，また{ } { }事後条件を弱めた A c B は真であると結論できる
次に， (逐次合成) 規則の一般形は{ } { }{ } { }
A c1 CC c2 B(逐次合成){ }{ }
A c1 ; c2 Bの根）において目標とする言明——図 3 のプログラムの実行後に k = N! となること——を導出している．

であり，その正当性——上の 2 つのホーアトリプル• 導出規則の適用は横線 ———— であらわされ，がともに真であれば，下のホーアトリプルも真であ
その右側に記された (単調性)，(While)，（代入)5′より正確には： 含意の論理式 A ⇒ A が恒真であるという条件．などは適用された規則の名前をあらわす．

4](単調性)る——は簡単に納得できるだろう．この規則の名前

一般にホーア論理によるプログラムの形式検証はは，結論となるホーアトリプルがプログラム c1 , c2次のようなワークフローをとる．の逐次合成 c1 ; c2 に関するものであるという理由に

1. システム（ここではプログラム）と仕様を，ホー{ } { }アトリプル A c B として形式化する．

よる．

2 か所の葉で用いられる (代入) 規則は，仮定を持たない（すなわち横線の上にホーアトリプルがない）規則である．
{

A[a/x]}

2. このホーアトリプルを根とする形式的証明（証明木）をつくる．これは木を下から上に生やしていくようなものであり，仮定がすべて（(代{ } (代入)x := a A入) 規則のような仮定のない規則によって）閉じたら，それで成功である．人間が紙とペンで

ここで A[a/x] は，性質（をあらわす記号列として行うこともあれば，証明木を書くためのソフトの論理式）A において，変数 x を a に置き換えたもウェア（証明支援系 (proof assistant) ，Coq やのをあらわす．

Isabell がよく知られている）の上で人間が行ったり，さらには全自動で証明を検索する定理証
明器 (theorem prover) を用いることもある．

この規則の正当性については少し考える必要があるだろう．たとえば A を n = 4，x を n，a を n + 1とすると，次の (代入) 規則の適用が得られる．
{n+1=4}

このワークフローはさまざまな例に適用可能であり，{} (代入)n := n + 1 n = 4

このような論理的検証は，全数探索によるモデル検査 (model checking) とならびシステム検証の主要な得られたホーアトリプルの事前条件は，実際 (9) の手法の一つである．

それと同値である．すなわち，(9) が真であることを示すには，人間がアタマを使ってひねり出さなくても，実は記号の置き換えだけで十分だったのである． 5
最後に while ループに関する導出規則を述べる．
{} { }c A{ }{} (While)
A while(b){c} A ∧ ¬bA∧b

離散ダイナミクスからハイブリッドシステムへ——微分方程式の導入

これはどういう意味だろうか？ 仮定であるホーアト

ここで 1 節に戻り，興味の対象をサイバーフィジ

リプルは A がループ不変性質であることを主張してカルシステム——特にハイブリッドシステム——にいる——その意味は (3) の条件ほぼそのままであり， 戻す．
以上に見てきたホーア論理による形式検証手法が事前条件にループ実行条件 b が加わることにより実は (3) の条件をリファインしている．そしてまた，結離散的「ジャンプ」ダイナミクスを対象とするのは論となるホーアトリプルは (8) の条件ほぼそのまま明らかだろう．このような離散的な形式検証の諸手である（ループ実行が終了したということは，事後法をハイブリッドシステムに拡張するにあたり，自において b は偽のはず）．すなわち，上記のホーア然なやり方は「微分方程式を『プログラム』として論理の (While) 規則は 3 節で行った数学的議論の本認める」ことであろう．たとえば質を導出規則として形式化したものである．

while(v ≥ 0)(v̇ = a0 ; ż = v)

ホーア論理の導出規則を説明したところで，再度(10)

図 4 の型式証明を見てほしい．3 節の（形式的でなというようにプログラム中に明示的に微分方程式をい，自然言語による）証明がほぼそのまま形式的に書けるようにすれば，システムに連続的「フロー」木として表現されていることが見てとれるだろう．

を導入することができる．この自然なアイデアにも5while (v > 0) {if (m - z >= s) {a = a0} else {a = -b};z := z + v * dt;
v := v + a * dt}

1とづいてプログラム論理を拡張しハイブリッドシス
2テム検証手法を得たのが Platzer らの最近の成果で3あり [2]6 ，注目を集めている．

4

また，モデル検査による形式検証の手法のハイブ
56リッドシステムへの拡張はより早くに行われ，モデ
7
ル検査の基礎となるオートマトンの拡張——ハイブ89
リッド・オートマトン (hybrid automaton)——の理論は 1990 年代にかなり整備された．ここでも基本的なアイデアは，離散ダイナミクスをあらわすオー

図 5: 超準解析的プログラムの例 ctrain ．式 (1) のダイ

トマトンの各状態に微分方程式を書くことにより連ナミクスの，超準解析的プログラムによる表現．無限小値続ダイナミクスを導入するというものである．

をあらわす定数 dt を用いて，連続ダイナミクスを while
ループとして表現する．

6

ハイブリッドシステムの形式検というものであり，離散的な形式検証手法——たとえば 4 節のホーア論理の導出規則のレパートリー—

証： 超準解析を用いてフローを—を何ら拡張することなくそのままの形で適用するジャンプにことを可能にする．本解説の残りで，この超準解析的アプローチを概説する．

前節で紹介したような「微分方程式を陽に持ち込

図 5 を見てみよう．これは 1 節に例示した列車のむ」ハイブリッドシステムの解析手法は，形式検証ダイナミクス（(1) の微分方程式で定義される）の超におけるさまざまなテクニック——形式的証明の検準解析的プログラムによる表現であり，値 z と v の索とループ不変性質生成，時相論理式による仕様記

連続的な変化が while ループによって表現されてい述，状態空間の抽象化，· · · ——を適用することで大る．たとえば 7 行目の代入文は (znew − zold )/dt = v

きな成功を収めている．一方で (10) のように微分方から導かれることに注意されたい．

程式によって言語を拡張すると，それに対応した形式検証手法の拡張が必要になることも明らかである．
具体的にたとえば 4 節のホーア論理で言うと，while

読者の中には「dt を小さな値（たとえば 10−3 ）にとって，離散化による微分方程式の数値近似をしようとしているだけではないか？」と思われた方もおや逐次合成など，プログラムの構成要素のそれぞれられるかもしれない．本アプローチのポイントは dtに対応する導出規則があるように，(10) のような微が本当の無限小値 (infinitesimal) を表現することで分方程式に対しても新たに導出規則を考案し，そのあり，ゆえに図 5 は列車のダイナミクスの数値近似正当性を示す必要がある．

ではなく，正確な，任意精度 (exact) のモデリング

これとは対照的に，筆者らが最近の論文 [3, 1] でになっていることである．

提案したアプローチはハイブリッドシステムの形式検証に対する超準解析的アプローチのワークフローは以下のとおりである．

「フロー」を（無限個の，それぞれは無限に小さい）「ジャンプ」に変換することで，1. 検証対象のハイブリッドシステムを，無限小をハイブリッドシステムに離散的形式検証手あらわす定数 dt を含むプログラムとしてモデ法を文字通りそのまま適用するリングする．
例： 1 節の列車に対する図 5 のプログラム ctrain ．

6 Platzer はホーア論理でなくダイナミック論理 (dynamiclogic) をハイブリッドシステムに拡張したのであるが，これら 2つのプログラム論理のスタイルに本質的な違いはない．

2. システムへの仕様をホーアトリプルとして表現
6

する．

7

例：列車の初期位置，初期速度がそれぞれ z0 , v0

論理学の成果たる超準解析とその応用であれば列車はカベにぶつからず停止する，と{いう仕様を次のように表現： z = z0 ∧ v =}{}v0 ctrain z < m

ライプニッツらによる解析学の定式化は無限小値の概念に依っていたが，無限小値——他の任意の正の値よりも小さな正の値——の存在は実数の理論に
3. 得られたホーアトリプルに対し，4 節と全く同じ 矛盾をきたすため，解析学の定式化は ε-δ 論法による導出規則を用いて証明木をつくることを試みる．
ものに改められた．これに対し A. Robinson は 1960
年代に超準解析 (nonstandard analysis) の理論を樹

4 節の（離散的な）形式検証の枠組は，立し，無限小値を実体として矛盾なく扱う枠組を与• while ループを含むプログラミング言語 While

えた．以下本節では，（少し込み入るが）超準解析の• 事前・事後条件など，性質 (assertion) を記述す できるだけ直感的な解説を試みる．
超準解析においては実数全体及び無限小値などを含るための述語論理 Assn
んだ超実数 (hyperreal) の集合 ∗R を考える．最初は• ホーア論理の導出規則のレパートリー Hoare おおざっぱに，超実数とは実数の無限列 (a0 , a1 , . . . )のことと考える．
（普通の）実数 r は定数列 (r, r, . . . )の 3 つ組からなるが，ハイブリッドシステムのためによって超実数とみなされ，超実数上の加法や乗法なに用いる拡張 (Whiledt , Assndt , Hoaredt ) は次のよ

どは要素ごとに定義される： (ai )i +(bi )i = (ai +bi )i ．

うになる．

ポイントは超実数上の述語の定義であり，たとえば• プログラミング言語 Whiledt は，While に新 大小関係 (ai )i∈N < (bi )i∈N はたな定数 dt を付け加えた（だけの）ものである．
(ai )i < (bi )i(11)• 述語論理 Assndt も同様 7 ．
def.
⇐⇒ 「ほとんどすべての i に対して」 ai < bi
• 論理体系 Hoaredt の導出規則は，もとの Hoare(12)のそれと全く同じ．
⇐= 有限個の i ∈ N を除いて a < b(13)i

すなわち，微分方程式を陽に持ち込んだり，それに対iと定義される．すると超実数 (1, 12 , 31 , . . . ) が無限小する新たな導出規則を導入したりすることなく，定値であることが簡単にわかる：任意の正の実数 r > 0数 dt を加えるだけで，離散的枠組をハイブリッド

は超実数としては (r, r, . . . ) であり，有限個の n を除システムに応用可能としたのである．dt によって拡いて常に n1 < r となるから (1, 12 , 31 , . . . ) < (r, r, . . . )張された枠組はもとの枠組と同じ位「よい性質」をが成立するのである．

もつ [3]．すなわち健全性 (soundness)——ホーア論

しかし，なぜ (13) の条件は必要十分でなく ⇐ の理で導出されるホーアトリプルは確かに真である—

みなのだろうか？ 超実数 (1, −1, 1, −1, . . . ) を考える

—及び相対完全性 (relative completeness)——真であるホーアトリプルはすべてホーア論理で導出できる 8 ——が，もとの離散的枠組と同様に成立する．と，これは (13) の定義のもとでは 0 よりも大きくも小さくもない．すると超実数は全順序集合をなさなくなり，何かと都合が悪い．そのために超準解析では，7 正確には Assndt における量化子 ∀, ∃ は実数でなく超実数(12) の「ほとんどすべて」を超フィルタ (ultrafilter)上を動く，という違いがある．この事情は移転原理（後述）と同じ．
8「相対」完全性とよばれるのは，(単調性) 規則の付帯条件——すなわち論理式の含意 A ⇒ B の真偽——が機械的に判定できないことによる．文献 [4] を参照されたい．

F を用いて正確に定義する．この正確な定義のもとでは，超実数 (1, −1, 1, −1, . . . ) は実数 1 または −1

7のいずれかに等しい 9 ．また超実数の定義は，正確というのは本手法に限らず理論計算機科学の基本でには実数の無限列の F による適切な同値類である． ある．
以上のもとで，次の「超準解析の基本定理」が得られる．
移転原理 (transfer principle)8

ある適当なクラスの述語論理式 A について，A が実数 R のもとで恒真でまとめ産業的・社会的に重要性をいや増すサイバーフィ∗あることと，A が超実数 R のもとで恒真であるこジカルシステムの品質保証について，元来離散ダイとは同値．

ナミクスを対象とする形式検証手法の応用を，ホー超実数が全順序集合をなすという上述の問題も，論ア論理を具体例として手短に解説した．連続的「フ理式 ∀x, y.(x ≤ y ∨ y ≤ x) を「移転」する——R でロー」を導入するために微分方程式がしばしば陽に真なので，∗R でも真である——ことですぐさま証明用いられるが，超準解析を用いて離散的枠組を「論できる．このように超準解析は（形式）論理学の成理的にアップグレード」することもできる．

果であり，6 節で紹介したホーア論理の超準解析拡

筆者らの研究は今のところプログラム論理による

張は「述語論理に対して成立する移転原理を，プロ形式検証のアップグレードにとどまるが，モデル検グラム論理という動的な状況に拡張したもの」とと査など他の形式検証手法のアップグレードについてらえることもできる．

も現在研究をすすめている——原則的には，述語論

以下，6 節の内容に超準解析の視点から補足を加理でその理論を書き下せる形式検証手法はすべて移えておく．最初に，図 5 を「プログラム」とよんだ転原理によってアップグレード可能である．また超がこれは実際には実行できない： dt は無限小値であ

準解析アプローチにおいては，ダイナミクスすべてるため，図 5 の while ループは有限回では停止しなをジャンプとみなすことにより統一的な取り扱いといのである．一方で，そのプログラムの実行結果をさまざまな離散的テクニックの応用が可能となるが，超準解析の言葉で数学的に定義することはでき（プこれは微分方程式の有用性を否定するものでは全くログラムの形式意味論 (formal semantics) ），そのない．微分方程式に対する諸知見も同時に活用でき（計算できないが定義は可能な）実行結果に照らしるようなシームレスな枠組を確立することにより，サて，正しいホーアトリプルがホーア論理により導出イバーフィジカルシステム研究における 2 つのアプされることが（健全性定理の形で）保証されている， ローチ——制御理論・力学系理論と，形式検証——というわけである．今述べたことは不思議に思える の一座建立をめざしたい．
筆者らの研究 [3, 1] は科研費 24680001，25730040

かもしれないが，及び FIRST 合原最先端数理モデルプロジェクトの• （有限の）プログラムが生成する（無限の）ふ助成を受けた．

るまいを検証する際に，• （無限の）ふるまいそのものを相手にするのは（有限の寿命しかない）人間には不可能なので， 参考文献
• もともとの（有限の）プログラムをもとに検証[1] Ichiro Hasuo and Kohei Suenaga. Exercises in

した上で，その結果が（無限の）ふるまいにつ

Nonstandard Static Analysis of hybrid systems.
In Proc. CAV, 2012.

いて有効であることを（健全性定理として）数学的帰納法により示す[2] André Platzer. Logical Analysis of Hybrid
Systems—Proving Theorems for Complex Dy-9 が，具体的にどちらに等しいかはふつうわからない： 答えは超フィルタ F の選び方に依存するのだが，F は選択公理を用いて非構成的に定義されるのでその実体は知れないのである．

namics. Springer, 2010.
8

[3] Kohei Suenaga and Ichiro Hasuo. Programmingwith infinitesimals: A while-language for hybrid
system modeling. In Proc. ICALP , 2011.
[4] Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.

9