※本記事は、Stanford大学のAA228V「Validation of Safety Critical Systems」コースにおける「Reachability for Linear Systems」の講義内容を基に作成されています。コースの詳細情報はhttps://aa228v.stanford.edu でご覧いただけます。教科書としてhttps://algorithmsbook.com/validation が使用されています。本記事では、講義の内容を要約しております。なお、本記事の内容は原講義の内容を正確に反映するよう努めていますが、要約や解釈による誤りがある可能性もありますので、正確な情報や文脈については、オリジナルの講義をご覧いただくことをお勧めいたします。
講師はStanford大学のポスドク研究員であるSydney Katz氏です。Sydney Katz氏についての詳細はhttps://sydneymkatz.com でご覧いただけます。
コースの受講方法や詳細情報についてはStanford Onlineのウェブサイト（https://online.stanford.edu/courses/a... ）をご参照ください。
1. イントロダクション
1.1 講義の位置づけと前回までの内容の振り返り
シドニー・カッツ：今日は少し方向転換をします。これまでの約3週間は主に失敗分析（failure analysis）について話してきました。具体的には、偽造（falsification）、失敗分布（failure distribution）、失敗確率の推定（failure probability estimation）に焦点を当ててきました。
今回からは形式手法（formal methods）というまったく異なるトピックに移行します。これまでは失敗を見つけたり、失敗の確率を推定したりする手法を見てきましたが、今回は形式的にシステムの保証を得る方法を学びます。つまり、失敗の不在を証明することを目指します。
特に、ある一連の前提条件の下でシステムが決して失敗しないことを証明できるかという問いに取り組みます。この証明には主に「リーチャビリティ（reachability）」と呼ばれる手法を使用します。
これまでの手法にはほとんど保証がありませんでした。例えば、長時間にわたって失敗を検索しても失敗が見つからなかったとしても、それはシステムが決して失敗しないことを意味するわけではなく、単に私たちが失敗を見つけられなかっただけかもしれません。そういった意味では、これまでの方法は不十分かもしれないと感じた方もいるでしょう。そこで今日からは、システムの振る舞いに関して実際に保証を得ることができる形式手法の世界に移行します。
1.2 形式手法とリーチャビリティの概要
シドニー・カッツ：リーチャビリティとは具体的に何かというと、システムが時間の経過とともに到達可能な状態の集合を計算する手法です。まず初めに、これまでの講義とは少し雰囲気を変えて冗談から始めたいと思います。四半期の間ずっと皆さんを面白いジョークで楽しませようとしてきましたが、いつかネタが尽きる日が来るんじゃないかと心配していました。そして今、「リーチャビリティ（reachability）」というトピックに到達しましたが、本当に今はジョークを「手を伸ばして届かせる（reaching）」のが難しい状況です。
さて、本題に入りましょう。これまで行ってきた手法にはほとんど保証がありませんでした。例えば、失敗を長時間探して見つからなかったとしても、システムが決して失敗しないという意味ではなく、単に私たちが失敗を見つけられなかっただけかもしれません。これは不満足かもしれませんね。
そこで今日から、形式手法（formal methods）の世界に入ります。ここではシステムの振る舞いについて実際に保証を得ることができます。特にリーチャビリティを使用すると、システムが時間の経過とともに到達可能な状態の集合を計算することができます。つまり、ある前提条件の下で、システムが危険な状態に到達する可能性があるかどうかを証明することができるのです。
私たちは非常にシンプルなシステム、つまり質量-ばね-ダンパーシステムを使用して、リーチャビリティの概念を説明していきます。このシステムは制御理論や動力学の授業を取ったことのある方には馴染みがあるかもしれません。このシステムを使って、リーチャビリティ解析を通じてシステムの安全性を証明する方法を学んでいきます。
1.3 失敗分析から形式的保証へのシフト
シドニー・カッツ：これまでの講義で扱ってきた失敗分析とは異なり、形式手法では失敗の不在を証明することを目指します。失敗分析では、システムの失敗を見つけたり、失敗の確率を推定したりしていましたが、実際にシステムが安全であるという保証は得られませんでした。例えば、長時間失敗を探索しても見つからなかったとしても、それはシステムが本当に安全であることを意味するわけではなく、単に私たちが失敗を見つけられなかっただけかもしれません。
形式手法、特にリーチャビリティ解析では、ある前提条件の下でシステムが決して失敗状態に到達しないことを数学的に証明します。つまり、これは「失敗の可能性がある」から「失敗の可能性がない」への転換、あるいは「失敗を見つける」から「失敗の不在を証明する」への転換と言えるでしょう。
この形式的保証を得るためには、いくつかの前提条件を設ける必要があります。例えば、初期状態の集合や各ステップで適用される外乱の集合に制約を設けます。これらの前提条件の下で、システムが時間の経過とともに到達し得る状態の集合を計算し、それが「避けるべき状態」の集合と交差しないことを証明できれば、システムが安全であると結論付けることができます。
もちろん、無償で保証が得られるわけではありません。形式的保証を得るためには、いくつかの仮定を設ける必要があります。しかし、これらの仮定の下で、システムが決して失敗しないという確固たる保証を得ることができるのです。これは、これまでの失敗分析アプローチでは得られなかった重要な進展です。
2. リーチャビリティの概念
2.1 リーチャビリティの基本的な説明
シドニー・カッツ：リーチャビリティとは、システムが時間の経過とともに到達可能な状態の集合を計算することです。この概念を理解するために、まず質量-ばね-ダンパーシステムという非常にシンプルなシステムを考えてみましょう。
このシステムでは、質量が壁につながれており、ばねとダンパーが取り付けられています。ばねは皆さんが日常で見るような普通のばねとして機能し、ダンパーは空気抵抗のようなものをモデル化しています。このモデルは一見単純に見えるかもしれませんが、実は自動車のサスペンションなど、多くの物理システムでよく使われる非常に一般的なモデルです。
さて、質量は前後に動くことができますが、重力は無視します。このシステムでは、質量が壁に近づきすぎたり、逆に遠すぎたりすると「失敗」と定義します。これが我々が避けたい状態です。
リーチャビリティの考え方を視覚的に説明するために、位置と速度のグラフを見てみましょう。横軸は質量の位置、縦軸は質量の速度を表しています。私たちは初期状態として、位置が-0.2から0.2の間、速度が0という状態からスタートすることを想定しています。
これらの初期状態からサンプルをたくさん取り、システムの動力学を適用して次の時間ステップでどこに到達するかを計算することができます。さらに時間ステップを進めていくと、4ステップ目までにシステムが到達し得る状態を見ることができます。
しかし、これはただ多くのサンプルを実行しただけで、システムが決して失敗しないという保証はありません。これはほとんど偽造（falsification）と同じようなものです。失敗を見つけられなかったからといって、失敗が絶対に起こらないという意味ではないのです。
リーチャビリティ解析では、サンプルをたくさん取る代わりに、完全なリーチャブル集合を計算します。つまり、初期状態の集合から出発し、有界の外乱を時間とともに適用した場合に到達し得る状態の全集合を計算するのです。これが背景に表示されている形状です。時間ステップ1での初期リーチャブル集合は、私たちが始めた初期集合です。時間ステップ2、3、4と進むにつれて、システムが到達し得るすべての状態を含む形状が得られます。
リーチャビリティ解析の目的は、これらのリーチャブル集合が「避けるべき状態」の集合と交差するかどうかを判断することです。交差しなければ、システムは安全であると証明できます。
2.2 質量-ばね-ダンパーシステムの例
シドニー・カッツ：リーチャビリティの概念を説明するために、質量-ばね-ダンパーシステムを使います。このシステムは非常にシンプルですが、多くの物理的なシステムをモデル化するのに適しています。具体的には、壁に取り付けられた質量があり、それにばねとダンパーが接続されています。
この質量は前後に動くことができ、ばねは通常のばねのように機能し、ダンパーは空気抵抗のようなものをモデル化しています。一見すると少し奇妙に見えるかもしれませんが、実は自動車のサスペンションなど、多くの物理システムでよく使われる非常に一般的なモデルです。
このシステムでは、質量が特定の領域に入ると失敗と定義します。具体的には、質量が壁に近づきすぎる（位置が-0.3未満）か、あるいは遠すぎる（位置が0.3を超える）場合に失敗とします。これが私たちが「避けるべき状態」として定義する領域です。
このシステムの動作を見てみましょう。例えば、質量がばねの自然な位置から引き伸ばされた状態から始めるとします。この状態から質量を解放すると、ばねの力によって質量は前後に振動します。しかし、この振動の程度や減衰の速度に満足できない場合があります。
そこで、制御を追加することができます。つまり、このクラスの用語で言えば「エージェント」を追加します。このエージェントは質量に力を加えることができ、ばねとダンパーの作用に対抗することができます。理想的には、これにより振動が少なくなるはずです。
エージェントを追加すると、質量はより早く安定化します。しかし、現実の問題をより反映させるために、さらにセンサーノイズを加えてみましょう。これにより、質量に力を加えるエージェントは、質量の正確な位置を観測できず、ノイズの入った観測値しか得られません。
少量のセンサーノイズを追加しても、エージェントはまだ質量を中央付近に保つことができますが、ノイズが多すぎると、システム全体が不安定になり、失敗する可能性があります。
この例から生じる重要な質問は、「最大可能なノイズに制限を設けた場合、システムが決して失敗しないことを証明できるか？」あるいは「失敗が可能であることを示す反例を提供できるか？」というものです。リーチャビリティ解析を使用すると、これらの質問に答えることができます。
2.3 制御とセンサーノイズの影響
シドニー・カッツ：質量-ばね-ダンパーシステムの動作を考えてみましょう。まず、質量がばねの自然な静止位置からある程度引き伸ばされた状態を想像してください。引き伸ばした状態から質量を解放すると、どうなると思いますか？
予想通り、質量は前後に振動します。これが基本的なシステムの挙動ですが、この振動を早く収束させたり、振幅を小さくしたりしたい場合があります。そこで、制御を加えることができます。または、このクラスの用語で言えば「エージェント」を追加します。
このエージェントは質量に力を加えることができ、ばねとダンパーの作用に対抗することができます。理想的には、これにより振動の大きさが小さくなり、より早く安定化するはずです。エージェントを追加した場合の動作を見ると、確かに質量はより早く静止位置に戻っていきます。
しかし、このシステムをより現実的にするために、さらに複雑さを加えましょう。クラスのこれまでのモデルに従って、センサーノイズを導入します。つまり、質量に力を加えるエージェントは、質量の正確な位置を観測できず、ノイズの入った観測値しか得られません。
少量のセンサーノイズを追加した場合、エージェントはまだうまく機能し、質量を中央付近に保つことができます。しかし、問題は「大量のセンサーノイズを追加するとどうなるか？」です。
大量のセンサーノイズがあると、システム全体が不安定になり、質量が「失敗領域」に入る可能性が高まります。実際、ノイズが非常に大きい場合、質量は遠くに行きすぎて、画面に表示されないこともあります。つまり、ノイズが一定量を超えると、システムは失敗する可能性があるのです。
そこで興味深い質問が生じます：「どの程度のノイズまでなら許容できるのか？」「最大可能なノイズに制限を設けた場合、システムが決して失敗しないことを証明できるか？」あるいは「失敗が可能であることを示す反例を提供できるか？」
これらの質問に答えるために、リーチャビリティ解析を使用します。これは、与えられた前提条件の下で、システムが時間の経過とともに到達し得る状態の集合を計算し、それが「避けるべき状態」の集合と交差するかどうかを判断する手法です。
2.4 リーチャビリティ解析の目標と前提条件
シドニー・カッツ：リーチャビリティ解析を使用して、「最大可能なノイズの制限が与えられた場合、システムが決して失敗しないことを証明できるか？」あるいは「失敗が可能であることを示す反例を提供できるか？」という問いに答えることができます。
しかし、「無料のランチはない」という言葉があるように、保証を得るためには何らかの前提条件を設ける必要があります。これまでの講義では失敗分析を行い、保証は得られませんでしたが、今回は保証を得るために前提条件を設けます。
質量-ばね-ダンパーシステムの場合、以下の前提条件を設定します：
- 質量は常に静止位置から-0.2から0.2の間の位置からスタートします。ここでは静止位置を0と定義します。つまり、質量を-0.2まで押し込むか、0.2まで引き出した状態からスタートします。
- 初期速度は常に0です。これは、質量を押し込んだり引き出したりした状態で静止させてから解放する状況を想定しています。
- 位置と速度に関する観測ノイズの最大絶対値は1です。つまり、観測値は実際の値から最大で±1ずれる可能性があります。これは、センサーの精度に関する仮定です。
これらの前提条件は、より一般的に言えば、「有界初期状態集合」と「有界外乱集合」を指定していることになります。リーチャビリティ解析では、このような前提条件に基づいて、システムが時間の経過とともに到達し得る状態の集合を計算します。
例えば、質量-ばね-ダンパーシステムでは、初期位置が-0.2から0.2の間、初期速度が0というのが初期状態集合です。外乱に関しては、このシステムではエージェントや環境に外乱は考慮しませんが、センサーには最大±1のノイズが加わるという外乱集合を設定しています。
これらの前提条件の下で、システムが時間の経過とともに到達し得る状態の集合を計算し、それが「避けるべき状態」（位置が-0.3未満または0.3を超える領域）と交差するかどうかを判断することで、システムの安全性を証明する、あるいは失敗の可能性を示す反例を提供することができます。
3. リーチャビリティの数学的表現
3.1 有界初期状態集合と外乱集合
シドニー・カッツ：リーチャビリティ解析で重要なのは、前提条件としての有界集合の設定です。黄色のスライドで注意を引きますが、リーチャビリティ解析では主に2つの前提条件を設けます。
まず、初期状態は有界集合から来るという前提です。質量-ばね-ダンパーシステムでは、質量の初期位置が-0.2から0.2の間、初期速度が0という初期状態集合を設定しました。
次に、各時間ステップでの外乱も有界集合から来るという前提です。これは、システムに影響を与える不確実性（ノイズなど）が一定の範囲内に収まることを意味します。
数学的には、この集合は以下のように表現できます： 外乱集合X = (Xa, Xe, Xs)
ここで、Xaはエージェントに関する外乱集合、Xeは環境に関する外乱集合、Xsはセンサーに関する外乱集合です。
集合とは単に点の集まりであることを思い出してください。それは無限個の点を含むこともあります。例えば、長方形は無限個の点を含む有界閉集合です。あるいは、単に点の集合として定義することもできます。
質量-ばね-ダンパーシステムの場合、初期集合Sは位置が-0.2から0.2の間、速度が0の全ての状態です。外乱集合については、エージェントや環境には外乱がないので、これらは「ゼロ集合」と呼ばれるものになります。これは単なる表記上の便宜で、実質的にはこれらの外乱は使われないことを意味します。センサーに関しては、外乱集合Xsは-1から1の間の全てのノイズ値です。
ところで、これまでのクラスでは、初期状態や外乱に関する確率分布を扱ってきましたが、これらの分布を有界集合に変換することができます。その方法は、分布の「台（support）」を取ることです。つまり、確率密度が非ゼロとなる全ての点を集合に含めます。
例えば、-1から1の間の一様分布の台は、まさに-1から1の区間です。ただし、ガウス分布の場合、その台は無限大に広がるため、有界集合を得るには工夫が必要です。一つの方法は、確率質量のほとんどを含む領域を選択することです。例えば、平均から3、4、5標準偏差までの範囲を切り取り、それを「十分」とみなすことができます。
これらの前提条件を設けることで、リーチャビリティ解析は、システムが時間の経過とともに到達し得る状態の集合を正確に計算し、システムの安全性を証明することができるのです。
3.2 深さdでのリーチャブル集合の定義
シドニー・カッツ：これらの前提条件（有界初期状態集合と有界外乱集合）を設定したら、次に特定の深さまたは時間ステップでのリーチャブル集合を計算します。これを数学的に定義してみましょう。
深さdでのリーチャブル集合（スクリプト体のRにサブスクリプトdがついたもの）は、有界初期状態集合からスタートし、各時間ステップで有界外乱集合から外乱を選択した場合に、深さdで到達し得る状態の集合として定義されます。
数学的には、これは次のように表現できます：
R_d = {s' ∈ S | ∃s ∈ S_0, ∃x_1,...,x_d ∈ X_1,...,X_d : s' = reach(s, [x_1,...,x_d], d)}
この数式の意味を説明すると、R_dは次の条件を満たす全ての状態s'の集合です：ある初期状態s（S_0から）と、ある外乱列[x_1,...,x_d]（それぞれX_1,...,X_dから）が存在し、初期状態sからこれらの外乱を適用して深さdで到達する状態がs'となる。
ここで、reach関数は、初期状態sから外乱列[x_1,...,x_d]を適用してロールアウトを行い、深さdでの最終状態を返す関数です。
これに関して質問はありますか？
質問：「ロールアウトを行う」とはどういう意味ですか？
回答：基本的には、初期状態集合の中の可能な全ての点から深さdまでロールアウトを行い、どの状態に到達するかを計算することです。ただし、初期集合に無限個の点がある場合、無限個のロールアウトを行う必要があり、それは計算上不可能です。そこで今日の講義と次回の講義のポイントは、それをより効率的に処理する方法を学ぶことです。
質問：「深さ」の概念を説明してください。
回答：深さは単に軌道またはタイムステップの数です。例えば、時間ステップ4での状態集合を知りたい場合、それはR_4となります。
質問：これは、各集合内に有限個の要素があることを前提としていますか？
回答：S（状態空間）とX（外乱集合）は有界集合である必要があります。
質問：そうすると、素朴にこれを計算することは不可能ということですね？
回答：はい、そのとおりです。多数のロールアウトを行うことは計算上不可能です。
質量-ばね-ダンパーシステムに戻ると、R_1（深さ1でのリーチャブル集合）は単に初期集合です。これは、位置が-0.2から0.2の間、速度が0の線分となります。R_2は時間ステップ2で到達し得る状態の集合であり、以下同様に続きます。
このように、リーチャブル集合の定義を用いて、時間の経過とともにシステムが到達し得る状態を正確に特定することができます。
3.3 時間地平線を考慮したリーチャビリティ
シドニー・カッツ：多くの場合、特定の深さでのリーチャブル集合だけでなく、ある時間地平線までのリーチャブル集合に関心があります。例えば、「時間ステップ4でのみシステムの状態を気にして、他の時間ステップでは気にしない」というのはあまり現実的ではありません。通常は、「現在から時間ステップ4までの間にシステムがどのような状態になるか」を知りたいものです。
そこで、時間地平線Hまでのリーチャブル集合を定義します。これをR₁:Hと表記し、深さ1からHまでの各リーチャブル集合の合併として定義します。
数学的には、これは以下のように表現できます：
R₁:H = R₁ ∪ R₂ ∪ ... ∪ RH
これは、深さ1からHまでの各リーチャブル集合を「重ね合わせる」ようなイメージです。この合併集合により、システムが時間ステップ1からHまでの間に到達し得るすべての状態を把握することができます。
例えば、質量-ばね-ダンパーシステムの場合、R₁:₄は時間ステップ1から4までの間にシステムが到達し得るすべての状態を表します。この集合を使って、システムが「避けるべき状態」（位置が-0.3未満または0.3を超える領域）に入るかどうかを判断できます。
質問：前の時間ステップの状態は、後の時間ステップのリーチャブル集合の部分集合ではないように見えますが、そうなのでしょうか？
回答：その通りです。深さが増えるにつれて、必ずしも以前のリーチャブル集合が新しいリーチャブル集合の部分集合になるとは限りません。
質問：この合併操作では、すべてを含んでいますか？
回答：はい、すべてを含んでいます。例えば、「システムが時間ステップ1から4の間にこの赤い集合に入らないことを確認したい」場合、1つの時間ステップだけを見るのではなく、すべての時間ステップを一緒に見て、合併集合が避けるべき集合と交差するかどうかを確認する必要があります。
時間地平線を考慮したリーチャビリティの概念は、システムの安全性を一定期間にわたって保証するために不可欠です。システムが特定の時間ステップでは安全でも、その前後の時間ステップでは危険な状態に入る可能性があるため、時間の範囲全体を考慮することが重要なのです。
3.4 避けるべき状態集合と目標領域
シドニー・カッツ：リーチャブル集合を計算したら、次に何をすべきでしょうか？既に少し話しましたが、基本的には、リーチャブル集合が「避けるべき状態集合」と交差するかどうかを確認します。交差しなければ、避けるべき状態に決して到達しないと言えるので、システムは安全です。
このクラスでは、避けるべき状態集合を「avoid set」と呼びます。これは、システムが避けるべき状態の集合を意味します。安全性の仕様や条件を、避けるべき状態の集合として表現する必要があります。これは常に可能とは限りませんが、以前の講義「プロパティ仕様」でリーチャビリティについて少し触れました。
質量-ばね-ダンパーシステムの場合、避けるべき状態集合は赤い領域で示されています。具体的には、位置が-0.3未満（壁に近すぎる）または0.3を超える（遠すぎる）領域です。これらの領域は二つの帯（バー）として表現され、これらが避けるべき状態集合を構成しています。
しかし、常に状態を避けることだけが目標とは限りません。時には、特定の「目標領域」に到達したいと思うこともあるでしょう。これは安全性よりも活性（liveness）に関係しています。システムが目標領域に到達するかどうかを確認するには、リーチャブル集合が目標領域に含まれているかどうかを確認します。つまり、到達可能なすべての状態が目標に終わるかどうかを検証します。
このクラスや教科書では、目標領域に到達する場合についてはあまり詳しく扱いませんが、避けるべき領域ではなく目標領域に到達したい場合にも同様の手法を適用できることは覚えておいてください。
リーチャビリティ解析の主な利点は、特定の前提条件の下で、システムの安全性に関する確かな保証を提供できることです。リーチャブル集合が避けるべき状態集合と交差しないことを証明できれば、システムは安全であると結論づけることができます。これは、以前の失敗分析手法では得られなかった強力な保証です。
同様に、システムが特定の目標に確実に到達することを証明したい場合も、リーチャビリティ解析を用いて、リーチャブル集合が目標領域に含まれることを示すことができます。
4. 線形システム
4.1 線形システムの定義
シドニー・カッツ：ここまでリーチャビリティの基本概念について説明してきました。次に、実際にリーチャブル集合を計算する方法について話しましょう。具体的には、線形システムに対するリーチャブル集合の計算の数学的背景に焦点を当てます。次の講義では、非線形システムに対する手法を扱います。
今日の講義の構成としては、まず「線形システム」とは何かを定義し、次に「集合伝播技法」という手法にかなりの時間を費やします。線形システムに対するリーチャビリティ解析には複数の方法がありますが、一つは集合伝播で、最後に少し触れる予定なのが最適化を使う方法です。
まず、線形システムとは何かを定義しましょう。線形システムとは、センサー、エージェント、環境がすべて状態、アクション、観測、外乱の線形関数として表現されるシステムのクラスです。つまり、これらはすべて入力の線形関数です。
以前は、観測モデル、エージェント、遷移モデルを一般的に定義していましたが、今回はこれらが特定の関数形式を持つことを指定します。例えば、観測モデルは状態と観測外乱の関数です。線形であるためには、これは状態と観測外乱の線形関数である必要があります。つまり、状態にある行列を掛けたものと、観測外乱の線形関数を足したものとなります。
同様に、エージェント（制御器）も観測値に行列を掛けた線形関数となります。遷移モデルについても同じです。
これが線形システムの定義です。線形システムは多くの物理現象をモデル化するのに広く使われており、数学的に扱いやすいという利点があります。次に、具体的な例として質量-ばね-ダンパーシステムがどのように線形システムとして表現されるかを見ていきましょう。
4.2 質量-ばね-ダンパーシステムの線形表現
シドニー・カッツ：質量-ばね-ダンパーシステムは線形システムの一例です。実は、このシステムを導入した理由の一つは、それが線形システムだからです。それでは、このシステムが線形システムとしてどのように表現されるかを見ていきましょう。
まず、観測モデルから説明します。このシステムでは、観測は単に状態にノイズが加わったものです。数学的には、観測モデルは恒等行列となります。つまり、大文字の「O」で表される行列は恒等行列で、これに状態を掛けて、さらに観測ノイズを加えます。
次に、制御器（コントローラー）について見てみましょう。この質量-ばね-ダンパーシステムでは、比例制御器（proportional controller）を使用しています。この制御理論や動力学の詳細については理解する必要はありませんが、大文字のπとoで表される行列は特定の値を持つ行列となります。これが私たちのエージェント（制御器）です。
また、先ほど述べたように、このシステムではエージェントと環境は決定論的です。つまり、これらには外乱がありません。
最後に、遷移モデルは状態とアクションに掛けられる行列として表現されます。これも単に与えられたものとして考えてください。これらの行列の導出方法を知る必要はありません。
これで線形システムの定義は終わりです。短いセクションでしたが、重要なポイントは、センサー（観測モデル）、エージェント（制御器）、環境（遷移モデル）がすべて状態、アクション、観測、外乱の線形関数として表現されるということです。
質量-ばね-ダンパーシステムの場合、観測モデルは恒等行列、制御器は特定の行列、遷移モデルも特定の行列で表現されます。これらの線形関数を用いることで、システムの動作を数学的に記述することができ、リーチャビリティ解析を効率的に行うことができるのです。
線形システムは多くの物理現象を良く近似でき、数学的に扱いやすいという利点があります。次のセクションでは、これらの線形関数を用いてリーチャブル集合を計算する「集合伝播技法」について詳しく見ていきます。
4.3 センサー、エージェント、環境の線形関数としての表現
シドニー・カッツ：線形システムでは、センサー、エージェント、環境がすべて状態、アクション、観測、外乱の線形関数として表現されます。これを質量-ばね-ダンパーシステムに適用して、具体的に見ていきましょう。
まず、センサー（観測モデル）については、このシステムでは観測は単に状態にノイズが加わったものです。数学的には、次のように表現されます：
O(s, xₛ) = Os + xₛ
ここで、Oは観測行列で、この場合は恒等行列です。sは状態ベクトル、xₛはセンサーノイズです。つまり、観測値は実際の状態にノイズが加わったものになります。
次に、エージェント（制御器）について見てみましょう。エージェントは観測値に基づいて行動を決定します：
a = π(o) = πₒo
ここで、πₒは制御行列で、特定の値を持ちます。このシステムでは比例制御器を使用していますが、その詳細は制御理論や動力学の授業で学ぶことができます。重要なのは、制御入力aが観測値oの線形関数として表現されることです。
また、先ほど述べたように、このシステムではエージェントと環境は決定論的です。つまり、これらには外乱がありません。数学的には、エージェントと環境の外乱項はゼロとなります。
最後に、環境（遷移モデル）は状態とアクションの線形関数として表現されます：
T(s, a, xₑ) = Tₛs + Tₐa + xₑ
ここで、Tₛは状態に関する遷移行列、Tₐはアクションに関する遷移行列、xₑは環境の外乱（この場合はゼロ）です。この式は、次の状態が現在の状態とアクションの線形関数であることを意味します。
質量-ばね-ダンパーシステムの場合、これらの行列は次のような具体的な値を持ちます（詳細な値はスライドに示されています）。これらの値がどのように導出されるかは重要ではなく、単にこのシステムの動力学を表現する数学的なパラメータだと考えてください。
これらの線形関数を組み合わせることで、システムの動作を完全に記述することができます。次の状態は現在の状態とアクション（制御入力）の線形関数であり、アクションは観測値の線形関数であり、観測値は状態とノイズの線形関数です。
この線形性が、リーチャビリティ解析をこのタイプのシステムに対して効率的に行うことを可能にします。線形システムは多くの物理現象を良く近似でき、数学的に扱いやすいという利点があります。次のセクションでは、これらの線形関数を用いてリーチャブル集合を計算する「集合伝播技法」について詳しく見ていきます。
5. 集合伝播技法
5.1 単一時間ステップでの次状態の計算
シドニー・カッツ：集合伝播技法について話しましょう。先ほど定義した線形システムの方程式を使って、単一の時間ステップでの次状態を計算する方法を見ていきます。
まず、現在の状態sと外乱xに基づいて次状態s'を表現します。遷移モデルの定義から、次状態は次のように表されます：
s' = T(s, a, xₑ)
しかし、ここでaはアクションですが、これは状態sと外乱xの関数です。私たちはs'をsとxだけの関数として表現したいのです。そこで、aを制御方策（ポリシー）関数で置き換えます：
s' = T(s, π(o), xₑ)
ここで、oは観測値ですが、これも状態と外乱の関数です。そこで、oを観測モデルで置き換えます：
s' = T(s, π(O(s, xₛ)), xₑ)
これで、s'は入れ子になった関数として表現されましたが、すべて状態sと外乱xの関数になりました。次に、線形システムの定義から各関数を代入します：
O(s, xₛ) = Os + xₛ π(o) = πₒo T(s, a, xₑ) = Tₛs + Tₐa + xₑ
これらを元の式に代入し、整理すると：
s' = Tₛs + Tₐπₒ(Os + xₛ) + xₑ s' = Tₛs + Tₐπₒ(Os) + Tₐπₒ(xₛ) + xₑ s' = Tₛs + TₐπₒOs + Tₐπₒxₛ + xₑ
これをさらに整理して、次の形にまとめることができます：
s' = (Tₛ + TₐπₒO)s + Tₐπₒxₛ + xₑ
この式は複雑に見えるかもしれませんが、ここで重要なのは、次状態s'が現在の状態sと外乱xの線形関数として表現されるということです。具体的には、いくつかの行列を掛け合わせ、ベクトルを掛け、それらを足し合わせることで計算できます。
ここまでは単一の点（状態と外乱）に対する計算でした。しかし、リーチャビリティ解析の目的は、状態の集合と外乱の集合が与えられたとき、次の状態の集合を計算することです。つまり、単一の点ではなく、集合全体に対してこれらの操作を適用する必要があります。
これが集合伝播の主なアイデアです。次に、集合に対してこれらの操作をどのように適用するか、そしてそれがどのような意味を持つのかを見ていきます。
5.2 集合演算：行列乗算と加算
シドニー・カッツ：さて、線形システムの次状態を計算するには、主に2種類の演算が必要です。1つは行列乗算（線形変換とも呼ばれます）、もう1つは加算です。これらの演算を単一の点ではなく集合全体に適用するにはどうすればよいのでしょうか。
まず、集合に対する行列乗算（線形変換）について定義します。数学的な定義は次のようになります：
A × P = {Ap | p ∈ P}
ここで、Pは集合、Aは行列です。この定義は、集合P内の各点pに行列Aを掛け、その結果得られる新しい点の集合が、行列Aと集合Pの積になることを表しています。
視覚的に説明しましょう。例えば、ある集合Pと行列Aがあるとします。集合Pの各点に行列Aを掛けると、新しい点が得られます。例えば、Pのある点を取り、それにAを掛けると新しい点が得られ、これがA×Pという新しい集合の一部になります。Pのすべての点に対してこのプロセスを繰り返すと、A×Pという新しい集合が得られます。
ただし、P内に無限個の点がある場合、すべての点に対してこの計算を行うことは不可能です。しかし、長方形など多くの一般的な集合表現では、集合P内のすべての点を個別に扱わなくても、この変換を効率的に計算する方法があります。この講義の後半でその方法について説明します。
次に、2つの集合の加算（ミンコフスキー和）について定義します。数学的な定義は次のようになります：
P ⊕ Q = {p + q | p ∈ P, q ∈ Q}
ここで、Pと Qは集合です。この定義は、集合P内の各点と集合Q内の各点を加えて得られるすべての点の集合が、PとQのミンコフスキー和になることを表しています。
視覚的に説明しましょう。例えば、集合Pと集合Qがあるとします。Pからある点を取り、Qからある点を取り、それらのベクトル表現を加えると、新しい点が得られます。これがP⊕Qという新しい集合の一部になります。PとQのすべての点の組み合わせに対してこのプロセスを繰り返すと、P⊕Qという新しい集合が得られます。
しかし、これも実際には無限個の組み合わせが存在するため、非現実的です。ただし、長方形などの多くの一般的な集合表現では、すべての個別の点を扱わなくても、この計算を効率的に行う方法があります。
このように、集合に対する行列乗算と加算を定義することで、線形システムの次状態を集合全体に対して計算することができます。これが集合伝播技法の基本的なアイデアです。次のセクションでは、これらの集合演算を用いて実際にリーチャブル集合を計算する方法について詳しく見ていきます。
5.3 線形変換とミンコフスキー和
シドニー・カッツ：集合に対する行列乗算と加算の定義ができたので、先ほどの次状態計算の式に戻りましょう。以下の式をもう一度見てみます：
s' = (Tₛ + TₐπₒO)s + Tₐπₒxₛ + xₑ
これは単一の状態と外乱に対する式でした。今度はこれを集合全体に適用します。つまり、行列乗算を集合に対する線形変換に、そして加算をミンコフスキー和に置き換えます。
これにより、初期状態の集合S₀と外乱集合Xが与えられた場合、可能な次状態の集合S₁を計算することができます。集合に対する式は次のようになります：
S₁ = (Tₛ + TₐπₒO) × S₀ ⊕ Tₐπₒ × Xₛ ⊕ Xₑ
ここで、×は集合に対する線形変換、⊕はミンコフスキー和を表します。これが線形システムに対する集合伝播の主要な式です。
この式をコードで実装する例を見てみましょう。教科書では次のように実装しています：
function propagate(𝒮::System, S, X)
Tₛ, Tₐ, πₒ, O = get_matrices(𝒮)
return (Tₛ + Tₐ*πₒ*O)*S ⊕ Tₐ*πₒ*X.xₛ ⊕ X.xₑ
endこのコードでは、まずget_matrices関数を使って線形システムから各行列を取得し、次に上記の式を実装しています。ここでJuliaの宣伝をさせてください。Juliaでは⊕のような数学的な記号をそのままコードで使うことができ、非常に便利です。これは素晴らしい「LazySet.jl」というJuliaパッケージのおかげです。多くの方がプロジェクトでこのパッケージを使うことになるでしょう。
このパッケージを使うと、集合に対する通常の演算子（乗算や加算など）をそのまま使用でき、⊕演算子もミンコフスキー和を計算してくれます。これは本当に素晴らしいパッケージで、今後の講義でもこのパッケージの機能をさらに紹介していきます。LazySetの開発者がこの講義を見ているなら、素晴らしいパッケージをありがとうございます。
さて、単一時間ステップでの集合伝播の方法がわかりました。次に、これを複数の時間ステップに拡張する方法を見ていきましょう。単純に考えると、初期集合から次の集合を計算し、その結果を新たな初期集合として同じプロセスを繰り返せばよいことがわかります。
数学的には次のように表現できます：
Rₖ₊₁ = (Tₛ + TₐπₒO) × Rₖ ⊕ Tₐπₒ × Xₛ ⊕ Xₑ
ここで、Rₖは深さkでのリーチャブル集合、Rₖ₊₁は深さk+1でのリーチャブル集合です。この式を繰り返し適用することで、時間経過に伴うリーチャブル集合を計算できます。
この方法を使って、質量-ばね-ダンパーシステムのリーチャブル集合をPlutoノートブックで可視化してみましょう。
5.4 複数時間ステップでのリーチャブル集合の計算
シドニー・カッツ：単一時間ステップでの集合伝播の方法がわかったので、これを複数の時間ステップに拡張する方法を見ていきましょう。基本的なアイデアは非常にシンプルで、単一ステップの計算を繰り返し適用するだけです。
数学的には、以下のように表現できます：
Rₖ₊₁ = (Tₛ + TₐπₒO) × Rₖ ⊕ Tₐπₒ × Xₛ ⊕ Xₑ
ここで、Rₖは深さkでのリーチャブル集合、Rₖ₊₁は深さk+1でのリーチャブル集合です。初期集合Rₒを出発点として、この式を繰り返し適用することで、連続した時間ステップにおけるリーチャブル集合を計算できます。
これをPlutoノートブックで実際に見てみましょう。このプロットは、前に示したものと同じです。青い点はサンプル（実行結果）で、緑の大きな長方形は今は無視してください。最初の時間ステップでは、リーチャブル集合は単に初期集合です。これは位置が-0.2から0.2の間、速度が0の線分です。
次の時間ステップに進むと、リーチャブル集合は形を変えます。3番目の時間ステップでは、リーチャブル集合はこのような形状になります。青い点（サンプル）がこのリーチャブル集合の中に含まれていることがわかります。これは、サンプルベースのアプローチで実行された軌道がすべてリーチャブル集合内にあることを確認するための一種の検証です。
このプロセスを続けると、時間の経過とともにシステムが到達し得る状態の集合を理解することができます。このような視覚化とリーチャビリティ計算は、プロジェクト3で実際に体験することになります。
ここで興味深いのは、21番目の時間ステップまで計算してもリーチャブル集合が「避けるべき状態集合」（赤い領域）と交差しないことです。これは、現在のノイズレベルでシステムが安全であることを意味します。
しかし、ノイズの大きさを増やすとどうなるでしょうか？ノイズを徐々に大きくしていくと、システムはより不安定になり、最終的には20数ステップ目あたりでリーチャブル集合が避けるべき集合と交差するようになります。
これは非常に重要な観察結果です。サンプルベースのアプローチだけでは、すべてのサンプル（青い点）が避けるべき集合と交差していないように見えるため、システムが安全であると誤って結論づける可能性があります。しかし、正確なリーチャビリティ解析では、ある軌道において避けるべき集合に入る可能性があることがわかりました。
つまり、リーチャビリティ解析は、サンプルだけでは検出できない潜在的な安全上の問題を明らかにする強力なツールなのです。これにより、システムが安全であるという強い保証を得ることができる場合もあれば、より注意深い設計や制御が必要であることを示す場合もあります。
質問：リーチャブル集合は、サンプルの凸包ではないのですか？
回答：いいえ、サンプルの凸包ではありません。リーチャブル集合は、初期状態の最大集合から計算されます。サンプルは計算方法とは完全に独立しています。これらのサンプルは単に一連のロールアウトの結果であり、リーチャブル集合がすべての可能な到達可能な状態を含む必要があるため、すべてのサンプルはその内部になければなりません。ありがとうございます、良い指摘です。
6. 集合表現
6.1 集合表現の望ましい特性
シドニー・カッツ：実際にリーチャブル集合の計算方法について話す前に、どのような集合表現が望ましいかを考えてみましょう。リーチャビリティ解析において効率的な計算を行うためには、集合表現が特定の特性を持っていることが重要です。
まず、「有限表現」が望ましい特性の一つです。これは、集合内のすべての点を一つ一つ列挙することなく、集合を指定できることを意味します。例えば、「1.1は集合に含まれる、1.2は集合に含まれる、3は集合に含まれる」というように全ての点を列挙するのではなく、長方形ならばその角だけを指定すれば、その長方形内のすべての点を表現できます。このように、集合を有限の情報で表現できることが重要です。
次に、「効率的な集合演算」が望ましい特性です。先ほど説明した線形変換やミンコフスキー和、さらには交差や合併などの演算を、集合内の各点に個別に適用することなく効率的に計算できる必要があります。
最後に、「集合演算の下での閉包性」も時に便利な特性です。これは、ある型の集合に演算を適用した結果も同じ型の集合になることを意味します。具体例を挙げると、二つの長方形の交差はまた長方形になります。例えば、2つのピンクの長方形があり、その交差部分を考えると、その交差もまた長方形です。このような特性があると、演算後も同じ表現方法を使い続けることができます。
ここで少しテストです。長方形は合併演算の下で閉じていますか？
いいえ、長方形は合併演算の下で閉じていません。2つの長方形の合併は、必ずしも長方形にはなりません。この例では、2つの長方形の合併全体を考えると、それは長方形ではなく、より複雑な形状になります。
これらの望ましい特性を持つ集合として、凸集合、特にポリトープと呼ばれる集合が重要です。凸集合とは、集合内の任意の2点を結ぶ線分が完全に集合内に含まれるような集合です。ポリトープはその特殊な形で、リーチャビリティ解析で広く使われています。次のセクションでは、これらの集合表現についてより詳しく見ていきます。
6.2 凸集合の特性
シドニー・カッツ：先ほど挙げた望ましい特性を持つ集合の一つが「凸集合」です。凸集合は数学的には次のように定義されます：
集合Cが凸であるとは、任意の2点x, y ∈ Cとすべての0 ≤ λ ≤ 1に対して、λx + (1-λ)y ∈ Cが成立することです。
この数式は少し複雑に見えるかもしれませんが、視覚的な意味はとても直感的です。凸集合とは、集合内の任意の2点を取り、それらを結ぶ線分を引いたとき、その線分が完全に集合内に含まれるような集合です。
例えば、円や楕円、三角形、長方形などは凸集合です。これらの形状から任意の2点を選び、それらを結ぶ線を引くと、その線は常に形状の内部にとどまります。
一方、C字型やドーナツ型（中が空いている円）などは非凸集合です。これらの形状では、2点を結ぶ線分が形状の外部を通過することがあります。例えば、C字型の開いている両端から点を取ると、それらを結ぶ線分はC字型の外部を通ることになります。
凸集合が特に重要なのは、リーチャビリティ解析で必要となる多くの演算（線形変換、ミンコフスキー和など）が凸集合に対して効率的に計算でき、また結果も凸集合になるためです。
このクラスでは特に「ポリトープ」と呼ばれる凸集合に焦点を当てます。他にも楕円や円などの凸集合がありますが、このクラスでは主にポリトープを扱います。もし他の種類の凸集合に興味があれば、スティーブン・ボイド教授の凸最適化のクラスを取ることをお勧めします。ちなみに、今日はボイド教授の誕生日です。彼に会う機会があれば、お誕生日おめでとうとお伝えください。
凸集合、特にポリトープは、リーチャビリティ解析において非常に重要な役割を果たします。というのも、これらは先ほど挙げた望ましい特性をすべて備えており、効率的な計算が可能だからです。次のセクションでは、ポリトープの具体的な表現方法について詳しく見ていきます。
6.3 ポリトープの表現：H-ポリトープとV-ポリトープ
シドニー・カッツ：このクラスでは、凸集合の一種である「ポリトープ」に焦点を当てます。ポリトープを定義するために、まずは「線形不等式」から始めましょう。
線形不等式は次の形式を持ちます：a^T x ≤ b
ここで、aとxはベクトル、bは定数です。この不等式が表す空間を視覚的に見ると、a^T x = bという線（または高次元では超平面）と、その線の一方の側にある全ての点の集合になります。この半空間（half-space）と呼ばれる領域は無限に広がっています。
複数の線形不等式の交差を取ると、「ポリヘドロン（polyhedron）」が得られます。例えば、2つの線形不等式a₁^T x ≤ b₁とa₂^T x ≤ b₂の交差は、2つの半空間が重なった領域を表します。これはまだ無限に広がる領域ですが、2つの不等式によって制約されています。
さらに多くの線形不等式を加えて交差を取り、それが有界になると、「ポリトープ（polytope）」が得られます。ポリトープは、有界な半空間の交差として定義される凸集合です。
ポリトープを表現する方法として、このクラスでは主に2つの表現を扱います。
1つ目は「H-ポリトープ」です。Hは「half-space（半空間）」を表しています。H-ポリトープは、線形不等式の集合として表現されます：
Ax ≤ b
ここで、Aは行列、bはベクトル、xは変数です。この表現では、各不等式（半空間）の交差としてポリトープを定義します。
2つ目は「V-ポリトープ」です。Vは「vertices（頂点）」を表しています。V-ポリトープは、頂点の集合の凸包（convex hull）として表現されます：
conv({v₁, v₂, ..., vₙ})
この表現では、ポリトープの頂点を明示的に指定し、それらの凸包としてポリトープを定義します。凸包とは、与えられた点の集合を含む最小の凸集合です。
例えば、いくつかの点が与えられたとき、その凸包は点を囲む最小の凸多角形（または高次元では凸多面体）になります。V-ポリトープを記述する際、実際には凸包の頂点だけを指定すれば十分です。つまり、凸包の境界上にある点だけを列挙します。
これら2つの表現（H-ポリトープとV-ポリトープ）は数学的には等価で、一方から他方への変換が可能です。ただし、特定の演算においては、一方の表現が他方よりも効率的なことがあります。特に、V-ポリトープは線形変換とミンコフスキー和の計算に適しています。
次のセクションでは、これらのポリトープ表現を用いて、どのように効率的に集合演算を行うかを見ていきます。
6.4 ポリトープの集合演算
シドニー・カッツ：V-ポリトープを使用すると、線形変換とミンコフスキー和を効率的に計算することができます。それぞれの演算について、すべての点を個別に扱うのではなく、頂点だけを考慮することでどのように計算できるかを見ていきましょう。
まず、ポリトープに対する線形変換について考えます。集合Pを行列Aで変換する場合、数学的には次のように表現されます：
A × P = conv({Av | v ∈ vertices(P)})
視覚的に説明すると、ポリトープPの各頂点v₁, v₂, v₃, v₄に行列Aを掛け、新しい頂点の集合を得ます。そして、これらの新しい頂点の凸包を取ることで、変換後のポリトープA×Pが得られます。
つまり、ポリトープ内の無限個の点すべてに行列Aを掛ける必要はなく、頂点だけに掛けて新しい頂点を得た後、それらの凸包を取るだけで済みます。これにより、計算が非常に効率的になります。
次に、ミンコフスキー和についても同様のアプローチが取れます。2つのポリトープPとQのミンコフスキー和は、数学的には次のように表現されます：
P ⊕ Q = conv({v₁ + v₂ | v₁ ∈ vertices(P), v₂ ∈ vertices(Q)})
視覚的に説明すると、ポリトープPの各頂点とポリトープQの各頂点のすべての組み合わせの和を考えます。これは、Qの各頂点にPを「移動」させるようなイメージです。例えば、Pの頂点をQの各頂点に移動させ、その結果として得られるすべての点の凸包を取ります。
この方法では、ポリトープPがv₁, v₂, v₃, v₄の4つの頂点を持ち、ポリトープQも4つの頂点を持つ場合、合計16の候補頂点が生成されます。最終的なミンコフスキー和の頂点の数は、これらの候補頂点のうちいくつかが凸包の内部に含まれるため、16以下になります。一般的には、ミンコフスキー和の頂点の数は、元のポリトープの頂点数の積以下になります。
質問：スライドの左上のひし形の頂点は間違っていませんか？
回答：はい、スライドに誤りがありました。左下の頂点が正しい位置に示されていません。正しいミンコフスキー和の形は異なります。ありがとうございます、指摘していただいて。
これらの操作を線形リーチャビリティに適用すると、各時間ステップでのリーチャブル集合の頂点数がどのように変化するかを分析できます。線形変換は頂点数を変えませんが、ミンコフスキー和は頂点数を増加させる可能性があります。
私たちのリーチャビリティ方程式では、各時間ステップで3つの線形変換と3つのミンコフスキー和を適用します。線形変換は頂点数に影響しませんが、ミンコフスキー和は頂点数を大幅に増加させる可能性があります。具体的には、前の時間ステップのリーチャブル集合の頂点数をv(R_d-1)、センサー外乱集合の頂点数をv(X_s)、エージェント外乱集合の頂点数をv(X_a)、環境外乱集合の頂点数をv(X_e)とすると、次の時間ステップのリーチャブル集合の頂点数は最大で次のようになります：
v(R_d) ≤ v(R_d-1) × v(X_s) × v(X_a) × v(X_e)
さらに、初期リーチャブル集合から深さdまで計算すると、頂点数は次のように指数関数的に増加する可能性があります：
v(R_d) ≤ v(R_0) × (v(X_s) × v(X_a) × v(X_e))^d
この指数関数的な成長は、特に高次元システムでは計算上の課題をもたらします。メモリ制約や計算効率の観点から、これは問題となる可能性があります。
この課題に対処するための一つの方法が、次のセクションで説明する「ゾノトープ（zonotope）」と呼ばれる特殊なポリトープの使用です。ゾノトープは、ミンコフスキー和の計算が効率的で、頂点数の爆発的増加を避けることができます。
7. ゾノトープ
7.1 ゾノトープの定義と構築方法
シドニー・カッツ：ポリトープの頂点数が指数関数的に増加するという問題に対処するために、「ゾノトープ」という特殊なポリトープを紹介します。ゾノトープはポリトープの一種ですが、すべてのポリトープがゾノトープであるわけではありません。
ゾノトープは、あるセンター点（中心点）からの一連の線分のミンコフスキー和として表現されます。数学的には、次のように定義されます：
Z = c ⊕ {[-g₁, g₁]} ⊕ {[-g₂, g₂]} ⊕ ... ⊕ {[-gₙ, gₙ]}
ここで、cはセンター点、g₁, g₂, ..., gₙは「生成子（generators）」と呼ばれるベクトルです。各生成子g_iは、センターcを中心とする線分[-g_i, g_i]（つまり、-g_iからg_iまでの線分）を表します。ゾノトープは、これらの線分のミンコフスキー和として構築されます。
私が初めてゾノトープを見たとき、「これは一体何だろう？」と混乱したことを覚えています。理解を助けるために、ゾノトープの構築過程を視覚的に説明しましょう。
例えば、3つの生成子g₁（青）、g₂（ピンク）、g₃（緑）を持つゾノトープを考えます。まず、センター点cを置きます。次に、最初の生成子g₁を考えます。ゾノトープの定義では、生成子の正と負の両方向（つまり、g₁と-g₁）を考慮します。センター点cに生成子g₁と-g₁を加えると、センターを通る線分が得られます。
次に、2番目の生成子g₂を考えます。現在の集合（線分）とg₂のミンコフスキー和を計算します。これは、線分の各端点に生成子g₂と-g₂を加え、その結果得られる点の凸包を取ることで計算できます。結果として、平行四辺形が得られます。
最後に、3番目の生成子g₃を加えます。同様に、現在の集合（平行四辺形）の各頂点に生成子g₃と-g₃を加え、その凸包を取ります。結果として、6角形のゾノトープが得られます。
生成子を追加する順序は関係なく、同じゾノトープが得られます。また、この例では2次元の生成子を使用しましたが、生成子は任意の次元で定義できます。
ゾノトープは視覚化するのが難しいかもしれませんが、その数学的性質は非常に有用です。特に、ゾノトープに対する線形変換とミンコフスキー和の計算が非常に効率的であることが、リーチャビリティ解析において重要な利点となります。
質問：生成子の対称性は定義の一部ですか、それとも必要な仮定ですか？
回答：ゾノトープの数学的定義を見ると、αg_iという形式で、αが-1から1の間の値を取ります。つまり、中心に対する対称性はゾノトープの定義の一部です。そのため、すべてのゾノトープは中心に対して対称になります。これがすべてのポリトープがゾノトープになれない理由の一つです。
次のセクションでは、ゾノトープに対する集合演算がいかに効率的に計算できるかを見ていきます。
7.2 ゾノトープの集合演算の効率性
シドニー・カッツ：ゾノトープの特筆すべき利点は、線形変換とミンコフスキー和の演算が非常に効率的に計算できることです。一般的なポリトープと比較して、ゾノトープの演算はより単純で計算コストが低くなります。
まず、ゾノトープに対する線形変換について考えましょう。ゾノトープZを行列Aで変換する場合、数学的には次のように表現されます：
A × Z = Ac ⊕ {[-Ag₁, Ag₁]} ⊕ {[-Ag₂, Ag₂]} ⊕ ... ⊕ {[-Agₙ, Agₙ]}
つまり、センター点cと各生成子g_iに行列Aを掛けるだけです。これにより、新しいセンター点Acと新しい生成子Ag₁, Ag₂, ..., Agₙが得られ、それらから新しいゾノトープが構築されます。
重要なのは、線形変換を適用しても生成子の数は変わらないことです。元のゾノトープがn個の生成子を持っていれば、変換後のゾノトープも同じn個の生成子を持ちます。
次に、ゾノトープのミンコフスキー和について考えましょう。2つのゾノトープZ₁とZ₂のミンコフスキー和は、次のように計算されます：
Z₁ ⊕ Z₂ = (c₁ + c₂) ⊕ {[-g₁₁, g₁₁]} ⊕ ... ⊕ {[-g₁ₙ, g₁ₙ]} ⊕ {[-g₂₁, g₂₁]} ⊕ ... ⊕ {[-g₂ₘ, g₂ₘ]}
ここで、c₁とc₂はそれぞれのゾノトープのセンター点、g₁₁, ..., g₁ₙは最初のゾノトープの生成子、g₂₁, ..., g₂ₘは2番目のゾノトープの生成子です。
ミンコフスキー和の計算では、2つのゾノトープのセンター点を加算し、両方のゾノトープの生成子を組み合わせた新しい生成子のリストを作成します。つまり、2つのゾノトープの生成子を単に連結するだけです。
この方法のすばらしい点は、ミンコフスキー和によって生成子の数が線形に増加することです。Z₁がn個の生成子を持ち、Z₂がm個の生成子を持つ場合、Z₁⊕Z₂はn+m個の生成子を持ちます。これは、一般的なポリトープの場合のように、頂点数が掛け算で増える（最大n×m個の頂点）のではなく、加算で増えることを意味します。
これにより、リーチャビリティ解析において、深さが増えるにつれて頂点数が指数関数的に爆発するという問題を回避できます。具体的には、各時間ステップでの生成子の数の増加は、以前のステップの生成子数に外乱集合の生成子数を加えただけになります。
例えば、質量-ばね-ダンパーシステムでリーチャビリティ方程式を適用する場合、各ステップで生成子の数は次のように増加します：
g(R_d) = g(R_d-1) + g(X_s) + g(X_a) + g(X_e)
ここで、g(・)はそれぞれの集合の生成子の数を表します。深さdまで計算すると、生成子の数は次のようになります：
g(R_d) = g(R_0) + d × (g(X_s) + g(X_a) + g(X_e))
これは、以前の指数関数的な増加と比較して、はるかに管理しやすい線形増加です。このため、ゾノトープはリーチャビリティ解析において計算上非常に効率的な表現方法となります。
次のセクションでは、ゾノトープの特殊な例として、ハイパーレクタングルについて見ていきます。
7.3 ハイパーレクタングルとゾノトープの関係
シドニー・カッツ：ゾノトープについてもう一つ素晴らしい点は、私たちが馴染みのある「ハイパーレクタングル」がゾノトープの特殊な場合であるということです。具体的には、生成子が座標軸に沿っている場合、ゾノトープはハイパーレクタングルになります。
ハイパーレクタングルとは、各次元で区間によって定義される直方体の高次元版です。1次元ではハイパーレクタングルは単なる線分、2次元では長方形、3次元では直方体になります。4次元以上では直感的な視覚化は難しくなりますが、数学的な定義は同じです。
ゾノトープの生成子がすべて座標軸に沿っている場合、つまり各生成子が単一の次元にのみ非ゼロの成分を持つ場合、結果として得られるゾノトープは各次元で独立した区間を持つハイパーレクタングルになります。
これは、集合表現の階層関係を示しています。最も一般的なのはポリトープで、その特殊な場合としてゾノトープがあり、さらにその特殊な場合としてハイパーレクタングルがあります。
すべてのハイパーレクタングルはゾノトープであり、すべてのゾノトープはポリトープですが、逆は必ずしも成り立ちません。つまり、すべてのポリトープがゾノトープであるわけではなく、すべてのゾノトープがハイパーレクタングルであるわけでもありません。
この階層関係は、リーチャビリティ解析において重要です。なぜなら、どの表現を使用するかによって、計算効率とリーチャブル集合の正確さのトレードオフが変わるからです。
ハイパーレクタングルは最も単純で計算効率が良いですが、複雑な形状を正確に表現できない場合があります。一方、一般的なポリトープは複雑な形状を正確に表現できますが、計算コストが高くなります。ゾノトープはその中間に位置し、ある程度の複雑さを持ちながらも計算効率を維持します。
実際のリーチャビリティ解析では、初期集合と外乱集合の性質、必要な計算精度、利用可能な計算リソースなどに基づいて、適切な集合表現を選択する必要があります。多くの場合、ゾノトープは良いバランスを提供し、そのため広く使用されています。
ハイパーレクタングルがゾノトープの特殊な場合であることを理解することで、既存のゾノトープベースのアルゴリズムやツールを、ハイパーレクタングルを扱う必要がある場合にも適用できることがわかります。
まとめると、ゾノトープはリーチャビリティ解析において非常に有用な集合表現であり、その特殊な場合としてハイパーレクタングルがあります。これにより、効率的な計算と十分な表現力のバランスを取ることができます。
8. 過大近似手法
8.1 頂点数の指数的増加問題
シドニー・カッツ：ポリトープを使ったリーチャビリティ解析において、大きな課題となるのが頂点数の指数的増加問題です。このセクションでは、この問題を詳細に検討し、それに対処するための方法を探ります。
リーチャビリティ方程式を再確認すると、各時間ステップで3つの線形変換と3つのミンコフスキー和を適用しています。線形変換は頂点数に影響しませんが、ミンコフスキー和は頂点数を大幅に増加させる可能性があります。
具体的には、リーチャブル集合R_{d-1}、センサー外乱集合X_s、エージェント外乱集合X_a、環境外乱集合X_eのミンコフスキー和を計算する場合、結果のリーチャブル集合R_dの頂点数は最大で次のようになります：
v(R_d) ≤ v(R_{d-1}) × v(X_s) × v(X_a) × v(X_e)
ここで、v(・)はそれぞれの集合の頂点数を表します。これは、深さ1からdまで計算する場合、頂点数が次のように指数関数的に増加する可能性があることを意味します：
v(R_d) ≤ v(R_0) × [v(X_s) × v(X_a) × v(X_e)]^d
この指数関数的な増加は、特に高次元システムや深い時間地平線では、非常に大きな問題となります。例えば、初期集合が10個の頂点を持ち、各外乱集合が5個の頂点を持つ場合、深さ10でのリーチャブル集合は理論上、最大10 × (5 × 5 × 5)^10 = 10 × 125^10 ≈ 10 × 10^21の頂点を持つ可能性があります。これは、現実的な計算リソースでは処理できない規模です。
この問題に対処する一つの方法として、前のセクションで説明したゾノトープの使用があります。ゾノトープを使用すると、ミンコフスキー和による生成子の増加は線形であり、指数関数的ではありません。しかし、すべてのポリトープがゾノトープとして表現できるわけではありません。特に、初期集合や外乱集合が一般的なポリトープである場合、ゾノトープに変換するには何らかの近似が必要になります。
また、時間ステップが増えるにつれて、リーチャブル集合の形状が複雑になり、多くの頂点を持つようになる場合もあります。例えば、質量-ばね-ダンパーシステムのリーチャブル集合は、時間の経過とともに複雑な形状になっていきます。
これらの課題に対処するもう一つの方法が、過大近似（over-approximation）手法です。過大近似では、正確なリーチャブル集合の代わりに、それを包含するより単純な集合（頂点数が少ない）を使用します。これにより、計算効率を大幅に向上させることができますが、代わりに精度が犠牲になる可能性があります。
次のセクションでは、過大近似の定義と利用法について詳しく見ていきます。
8.2 過大近似の定義と利用法
シドニー・カッツ：頂点数の指数的増加問題に対処するもう一つの方法は、過大近似（over-approximation）を使用することです。ゾノトープを使えない場合や、ゾノトープでも生成子の数が多くなりすぎる場合に特に有用です。
過大近似とは、ある集合を完全に含む、より単純な（例えば頂点数が少ない）集合を見つけることです。数学的には、集合Pの過大近似P̄は、PがP̄の部分集合（P ⊆ P̄）となるような集合です。過大近似を表記する際は、元の集合の上にバーを付けることが多いです。
視覚的な例を見てみましょう。例えば、青い集合Pがあり、その過大近似として紫の集合P̄を考えます。過大近似の定義により、青い集合のすべての点は紫の集合にも含まれます。つまり、P̄はPを完全に「包含」しています。
ポリトープのリーチャビリティ解析において、頂点数が多くなりすぎた場合、少ない頂点数を持つポリトープで過大近似することで計算を効率化できます。例えば、100個の頂点を持つ複雑なポリトープを、10個の頂点を持つより単純なポリトープで近似することができます。
しかし、過大近似を使用することで得られる計算効率の向上には、精度の低下というトレードオフが伴います。過大近似されたリーチャブル集合は元のリーチャブル集合よりも大きいため、安全性の保証が弱まる可能性があります。
具体的には、元のリーチャブル集合が「避けるべき状態集合」と交差しない場合、その過大近似も交差しなければ、システムは安全であると結論づけることができます。しかし、過大近似が「避けるべき状態集合」と交差する場合、元のリーチャブル集合は交差するかもしれないし、しないかもしれません。つまり、過大近似が「避けるべき状態集合」と交差する場合、システムの安全性について確かな結論を出すことができません。
過大近似の実用的な利用法としては、リーチャビリティ計算の各ステップで正確な計算を行い、頂点数が閾値を超えた場合にのみ過大近似を適用するという方法があります。例えば、数ステップごとに過大近似を適用することで、頂点数の増加を管理可能なレベルに抑えることができます。
また、過大近似の方法も様々あります。例えば、元のポリトープを包含する最小の長方形（または高次元では直方体）を計算する方法や、元のポリトープを包含する凸多面体で、指定された精度を満たす最小のものを計算する方法などがあります。
過大近似は、計算効率と精度のバランスを取るための重要なツールです。特に、高次元システムや長い時間地平線でのリーチャビリティ解析では、適切な過大近似手法を選択することが不可欠です。
次のセクションでは、過大近似がリーチャビリティ解析の保証にどのような影響を与えるかを詳しく見ていきます。
8.3 過大近似がもたらす保証への影響
シドニー・カッツ：過大近似を使用することで計算効率を向上させることができますが、それはシステムの安全性に関する保証にどのような影響を与えるのでしょうか。ここでは、過大近似されたリーチャブル集合から得られる結論と、その限界について考えます。
まず、過大近似されたリーチャブル集合が「避けるべき状態集合」と交差しない場合を考えましょう。この場合、元のリーチャブル集合も「避けるべき状態集合」と交差しないことを保証できます。なぜなら、元のリーチャブル集合は過大近似の部分集合であるため、過大近似が避けるべき集合と交差しなければ、その部分集合である元のリーチャブル集合も交差しないからです。
例えば、青いリーチャブル集合の過大近似として紫の集合があり、これが赤い「避けるべき状態集合」と交差しない場合、青いリーチャブル集合も赤い集合と交差しないことがわかります。したがって、システムは安全であると結論づけることができます。
次に、過大近似されたリーチャブル集合が「避けるべき状態集合」と交差する場合を考えましょう。この場合、元のリーチャブル集合が「避けるべき状態集合」と交差するかどうかは不明です。過大近似の部分だけが「避けるべき状態集合」と交差している可能性もあれば、元のリーチャブル集合自体が交差している可能性もあります。
例えば、紫の過大近似が赤い「避けるべき状態集合」と交差する場合、青いリーチャブル集合が赤い集合と交差するかどうかはこの情報だけでは判断できません。青い集合が赤い集合と交差する部分を含んでいるかもしれませんし、含んでいないかもしれません。
したがって、過大近似が「避けるべき状態集合」と交差する場合は、システムの安全性について確かな結論を出すことができません。この場合、より精密な計算（例えば、過大近似の程度を減らす）を行うか、あるいは別のアプローチ（例えば、反例の探索）を試みる必要があるかもしれません。
まとめると、過大近似がもたらす保証への影響は次のようになります：
- 過大近似されたリーチャブル集合が「避けるべき状態集合」と交差しない場合：
- システムは安全であると保証できます。
- これは「負の結果」（安全でないことを示せない）という強い保証です。
- 過大近似されたリーチャブル集合が「避けるべき状態集合」と交差する場合：
- システムが安全かどうかは不明です。
- これは結論を導けないという弱い結果です。
つまり、過大近似を用いたリーチャビリティ解析は、システムが安全であることを証明するには有用ですが、システムが安全でないことを証明するには追加の分析が必要です。
過大近似の程度（元のリーチャブル集合にどれだけ近いか）は、このトレードオフに大きく影響します。より精密な過大近似（元のリーチャブル集合により近い）は、より強い保証を提供しますが、計算コストが高くなります。一方、より粗い過大近似（元のリーチャブル集合からより離れている）は計算が効率的ですが、保証が弱くなります。
適切な過大近似の選択は、システムの要件（必要な安全性の保証のレベル）と利用可能な計算リソースのバランスに依存します。
8.4 実践的な過大近似の実装
シドニー・カッツ：過大近似の概念を理解したところで、リーチャビリティ解析における実践的な過大近似の実装方法を見ていきましょう。
リーチャビリティ計算では、時間ステップが増えるにつれてポリトープの頂点数が指数関数的に増加するという問題に対処するために、いくつかのステップごとに過大近似を適用するアプローチが一般的です。例えば、3ステップごとに過大近似を適用することで、頂点数の増加を管理可能なレベルに抑えることができます。
実装のコードを見てみましょう。教科書のアルゴリズムでは、以下のような行が含まれています：
if mod(d, recalculation_interval) == 0
R = overapproximate(R, ε)
endここでは、特定の間隔（recalculation_interval）ごとに、リーチャブル集合Rを誤差パラメータεで過大近似しています。この誤差パラメータは、過大近似の精度を制御するものです。値が小さいほど、より正確な過大近似が得られますが、計算コストが高くなります。
実装面でのもう一つの素晴らしい点は、Julia言語のLazySet.jlパッケージが、この過大近似機能をすでに提供していることです。overapproximate関数に集合と誤差パラメータを渡すだけで、指定された誤差範囲内でその集合の過大近似を返してくれます。
この過大近似アルゴリズムの詳細を知りたい場合は、教科書の該当セクションを参照することをお勧めします。基本的には、元のポリトープを包含し、指定された誤差範囲内で最も近い単純なポリトープ（例えば、頂点数の少ないポリトープ）を見つけるアルゴリズムが使用されています。
実践的な過大近似の実装における重要な考慮事項は以下の通りです：
- 過大近似の頻度：頂点数が管理不能になる前に過大近似を適用する必要がありますが、あまり頻繁に適用すると精度が低下します。アプリケーションの要件に基づいて適切な間隔を選択する必要があります。
- 誤差パラメータの選択：誤差パラメータ
εは、過大近似の精度と計算効率のトレードオフを制御します。小さな値はより正確ですが計算コストが高く、大きな値は効率的ですが精度が低くなります。 - 過大近似の方法：さまざまな過大近似手法があり、それぞれ異なる特性を持ちます。例えば、軸に沿った（axis-aligned）ボックスによる過大近似は非常に効率的ですが、元の集合の形状を粗く近似します。一方、支持超平面（supporting hyperplanes）を使用した過大近似は、より正確ですが計算コストが高くなります。
時間が限られているため、このセクションを短く終えますが、次回の講義では過大近似の方法についてさらに詳しく説明する予定です。特に、集合を過大近似するための基本的な方法について掘り下げていきます。
実践的な過大近似の実装は、リーチャビリティ解析を高次元システムや長い時間地平線に対して実行可能にするために不可欠です。適切な過大近似手法と誤差パラメータを選択することで、計算効率と精度のバランスを取りながら、システムの安全性に関する有用な保証を得ることができます。
9. 個人的エピソード
9.1 コロナ禍での椅子購入のエピソード
シドニー・カッツ：前提条件の重要性を強調するために、個人的なエピソードを共有したいと思います。コロナウイルスが発生したとき、今から振り返るとほぼ5年前になりますが、多くの皆さんと同様に、私も何が起こっているのか全く分かりませんでした。
当時、付き合って8ヶ月だった彼氏（現在の夫）のアパートに移ることになりました。「2週間だけだから大丈夫」と思って引っ越したのですが、結局それが永遠になってしまいました。彼のワンルームアパートで一緒に暮らし始め、二人とも在宅勤務をしなければならなくなりました。
彼はベッドの近くにデスクを持っていたので、そこで仕事をしていました。私はキッチンの小さなテーブルで作業することになりました。コロナ前、彼はほとんどオフィスで生活していて、朝食、昼食、夕食まですべてオフィスで食べていたので、そのアパートは実際には「住むため」ではなく、ただ寝に帰るだけの場所でした。
そのため、彼が持っていた小さなキッチンテーブル用の椅子は、パーティーなどで予備の席が足りないときに出すような折りたたみ椅子だけでした。「この折りたたみ椅子で毎日何時間も働くのは無理だ、もう背中が痛くなり始めている」と思いました。
そこで、Amazonで椅子を注文することにしました。特にこの椅子を選びました。当時はすっかり独身男性のバチェラーパッドのような雰囲気だったので、「アパートの真ん中にホットピンクの椅子を置いて、少しおしゃれにしよう」と思いました。
デスクチェアの適正価格がわからなかったのですが、これを見て「すごく安い！これを注文しよう」と思いました。2020年3月17日、かなり大変な時期に注文しました。
数日後、椅子が届いたという通知が来て、すごく興奮しました。「やった、もうこの terrible折りたたみ椅子を使わなくて済む！」と思って階下に走っていきました。そこで見つけたのは、このくらいの大きさの箱でした。「あれ、変だな。椅子がこんな箱に入るはずがない」と思いましたが、「たぶん多くのパーツに分かれているんだろう」と考えました。
箱を持ち上げると、「この椅子はすごく軽いな。何か本当に素晴らしい軽量椅子を買ったんだ」と思いました。階上に戻って箱を開けると、まだ椅子だと信じていたのですが...椅子ではありませんでした。実際には、これら2つの布切れだけでした。
箱の大きさはこのくらいで、明らかに椅子が入るようなサイズではありませんでした。結局、椅子ではなく、おそらく20ドルくらいのホットピンクの布カバーを買ってしまったのです。
しかも面白いことに、このカバーは今でも夫のデスクチェアに付いています。彼はそれが気に入って、自分用に取っておいたのです。
とにかく、これは残念な出来事でした。数日後に実際の椅子が届くまで、あの折りたたみ椅子を使い続けなければなりませんでした。次回は本当に確認することにしました。
ここでの教訓は、商品の写真が椅子に見えるからといって、それが実際に椅子であるとは限らないということです。常に前提条件を確認することが大切です。あるいはこの場合は、非常に大きくて明らかな文字を読むことさえすれば、そのような状況に陥ることはなかったでしょう。何かしらの文章を読んでいれば、椅子ではなくカバーを買っていることがわかったはずです。
前提条件の重要性を常に念頭に置いておいてください。
9.2 前提条件の重要性についての教訓
シドニー・カッツ：この椅子カバーのエピソードは単なる面白い話ではなく、実際にはリーチャビリティ解析における重要な教訓を含んでいます。その教訓とは、「前提条件は非常に重要である」ということです。
リーチャビリティ解析において、私たちは強力な保証—システムが決して失敗しないことの証明—を得ることができます。しかし、これらの保証は私たちが設定した前提条件に依存しています。初期状態の集合や外乱の集合に関する前提条件が正確でなければ、得られる保証も信頼できません。
椅子を購入した例では、私は「商品の写真が椅子であれば、その商品は椅子である」という前提条件を立てていました。この前提条件が間違っていたため、予期しない結果（椅子ではなく椅子カバーが届くこと）につながりました。
同様に、リーチャビリティ解析では、「センサーノイズは常に±1の範囲内である」といった前提条件を設定するかもしれません。しかし、実際のセンサーノイズがこの範囲を超える場合、私たちの安全性の保証は無効になります。
重要なのは、前提条件を常に明示し、検証することです。私の場合、商品説明を読むという簡単な作業を行っていれば、誤解を避けることができました。同様に、リーチャビリティ解析では、前提条件が現実的であり、システムの実際の動作条件と一致しているかを確認する必要があります。
前提条件を確認する—椅子の例では説明文を読む、リーチャビリティ解析では初期条件や外乱モデルを検証する—という単純なステップを踏まずに、結論を急いでしまうと、誤った結果につながる可能性があります。
また、このエピソードは、モデルと現実の乖離についても教えてくれます。リーチャビリティ解析では、システムのモデルを用いて計算を行いますが、そのモデルが実際のシステムを正確に表現しているかを確認する必要があります。モデルが不正確であれば、いくら精密な計算を行っても、得られる保証は現実のシステムには適用できません。
結局のところ、リーチャビリティ解析であれオンラインショッピングであれ、前提条件を明確に理解し、検証することが成功への鍵です。「常に細字を読む」—または、この場合は「極めて大きな明らかな文字を読む」—ことで、多くの問題を避けることができるのです。
次回からの講義で非線形システムのリーチャビリティについて学ぶ際も、この教訓を心に留めておいてください。前提条件の重要性は、より複雑なシステムになるほど高まります。
10. 今後の内容
10.1 非線形システムへの拡張への言及
シドニー・カッツ：これまで、線形システムに対するリーチャビリティ解析について説明してきました。線形システムは数学的に扱いやすく、多くの物理現象を近似できる便利なモデルですが、世の中のシステムのほとんどは本質的に非線形です。次回の講義では、非線形システムへとこの考え方を拡張していきます。
非線形システムに対するリーチャビリティ解析は、線形システムの場合よりもはるかに複雑になります。線形システムでは、集合の線形変換やミンコフスキー和といった操作を用いて、リーチャブル集合を効率的に計算することができました。しかし、非線形システムでは、これらの操作だけでは不十分です。
非線形システムでは、状態空間のある領域でのシステムの振る舞いが、別の領域での振る舞いと大きく異なる可能性があります。これにより、リーチャブル集合の形状が非常に複雑になり、単純なポリトープやゾノトープでは正確に表現できなくなります。
次回の講義では、非線形システムに対するリーチャビリティ解析のアプローチとして、以下のような手法を紹介する予定です：
- 線形化手法：非線形システムを局所的に線形化し、線形システムの手法を適用する方法
- 区分的な手法：状態空間を複数の領域に分割し、各領域で適切な近似を行う方法
- テイラー級数展開：非線形ダイナミクスをテイラー級数で近似する方法
- 微分包含：不確かさを持つシステムの振る舞いを捉える方法
非線形システムのリーチャビリティ解析は、自動運転車、航空機制御システム、ロボット工学など、多くの実世界の安全クリティカルなシステムの検証に不可欠です。これらのシステムは通常、複雑な非線形ダイナミクスを持っており、その安全性を保証するためには、非線形リーチャビリティ解析の手法が必要です。
また、非線形システムでは過大近似の重要性がさらに高まります。非線形性によって生じる複雑な形状のリーチャブル集合を扱うために、効率的な過大近似手法が必要となります。次回の講義では、非線形システムに特化した過大近似テクニックについても詳しく説明します。
時間の制約があるため、今回の講義ではこれ以上詳細には踏み込みませんが、次回は過大近似の方法から始めて、非線形システムのリーチャビリティへと進んでいく予定です。皆さんが次回の内容も楽しみにしてくれることを願っています。
10.2 最適化を用いたリーチャビリティ計算の予告
シドニー・カッツ：線形システムに対するリーチャビリティ解析のもう一つのアプローチとして、最適化を用いた方法があります。今回の講義では主に集合伝播技法に焦点を当てましたが、次回以降の講義では最適化ベースのアプローチについても触れる予定です。
最適化を用いたリーチャビリティ計算では、リーチャブル集合を直接伝播するのではなく、最適化問題を解くことでリーチャブル集合の特性を調べます。例えば、ある方向にリーチャブル集合がどこまで広がるかを知りたい場合、その方向に対する支持超平面を見つける最適化問題を解くことができます。
最適化ベースのアプローチの利点は、一般的に非線形システムにも適用しやすいことです。線形計画法（LP）、二次計画法（QP）、あるいはより一般的な非線形最適化手法を用いることで、様々な複雑なシステムのリーチャビリティ解析が可能になります。
また、最適化ベースのアプローチは、反例の生成にも役立ちます。先ほどの質問にあったように、「どのような初期状態と外乱の列が失敗につながるか」を見つけるためには、最適化問題を解くことが効果的です。この方法では、安全性条件に違反するような軌道を見つけるために、目的関数を適切に設定した最適化問題を解きます。
さらに、最適化ベースの手法は、リーチャブル集合の特定の部分（例えば、安全性検証に重要な境界領域）に計算リソースを集中させることができるため、効率的な計算が可能になる場合があります。
次回の講義では、これらの最適化ベースのリーチャビリティ解析手法について、より詳細に説明する予定です。特に、線形システムと非線形システムの両方に対して、どのように最適化問題を定式化し、解くかについて掘り下げていきます。
最終的には、集合伝播技法と最適化ベースの手法を組み合わせることで、より強力なリーチャビリティ解析ツールを構築できることを示します。これらの手法は相補的であり、システムの特性や検証の目的に応じて、適切な方法を選択したり組み合わせたりすることが重要です。
時間の関係でここまでとなりますが、次回の講義で過大近似の方法から始めて、非線形システムのリーチャビリティと最適化ベースのアプローチへと進んでいきます。木曜日にお会いしましょう。
