/w=3840,quality=90,fit=scale-down)
※本記事は、Stanford University の講義「Stanford AA228V I Validation of Safety Critical Systems I Property Specification 2」の内容を基に作成されています。
この講義は Sydney Katz 氏（Stanford University のポストドクトラルスカラー）と Mykel Kochenderfer 氏（Stanford University の航空宇宙工学准教授および計算機科学の兼任教授）によるものです。講義の詳細情報は https://aa228v.stanford.edu/ でご覧いただけ、教科書は https://algorithmsbook.com/validation/ で入手可能です。
本記事では講義の内容を要約しております。なお、本記事の内容は講義の内容を正確に反映するよう努めていますが、要約や解釈による誤りがある可能性もありますので、正確な情報や文脈については、オリジナルの講義動画や教材をご参照いただくことをお勧めいたします。
講師についての詳細は Sydney Katz 氏（https://sydneymkatz.com/ ）および Mykel Kochenderfer 氏（https://mykel.kochenderfer.com/ ）のウェブサイトでご確認いただけます。また、このコースの詳細や登録については Stanford Online（https://online.stanford.edu/ ）をご参照ください。
1. 複合メトリクスの復習
1.1. パレート最適性とトレードオフ
Sydney Katz: 前回の講義では複合メトリクスについて説明しました。簡単に復習しましょう。安全性クリティカルシステム、例えば航空機衝突回避システムでは、複数のメトリクスが重要になります。具体的には、衝突率とアラート率の両方を考慮する必要があります。
理想的には両方のメトリクスがゼロであることが望ましいですが、それは通常達成不可能です。そこでトレードオフが発生します。このグラフの各点は異なる設計を表しています。パレート最適性とは、一方のメトリクスを改善すると、必ず他方が悪化するような状態を指します。
例えば、このポイントはパレート最適ではありません。なぜなら、衝突率とアラート率の両方を改善できる他の設計が存在するからです。一方、このポイントはパレート最適です。一方のメトリクスを改善しようとすると、必ず他方が悪化してしまいます。
私たちが「パレートフロンティア」と呼ぶものは、これらのパレート最適な設計の集合です。しかし、フロンティア上の点はすべて同等に「良い」とみなされるため、フロンティア上の特定の点を選ぶためには複合メトリクスを導入する必要があります。
学生: パレートフロンティア上では、どのようにして特定の設計を選ぶのですか？
Sydney Katz: それこそが複合メトリクスの役割です。例えば、重み付け和法では各メトリクスに重みを付けます。アラート率に0.8、衝突率に0.2の重みを与えると、重み付け和が最大となる点を選ぶことができます。
他にも目標距離法があり、これは理想点（この場合はゼロアラートとゼロ衝突のユートピア点）からの距離が最小となる点を選びます。また、重み付き指数和メトリクスのような他の手法も考えられますが、これは基本的に距離測定に重みを組み合わせたアプローチです。
パレート最適性の概念は、複数の競合する目標を持つシステムの設計において非常に重要です。航空機の衝突回避だけでなく、様々な安全性クリティカルシステムの設計に応用できます。各メトリクスの重要度は状況によって異なるため、適切な複合メトリクスを選択することで、特定の要件に最適な設計を特定できるのです。
1.2. 複合メトリクス手法（重み付け和、目標距離、重み付き指数和）
Sydney Katz: ここで、パレートフロンティア上から最適な設計を選ぶための複合メトリクス手法についてさらに詳しく説明しましょう。先ほど少し触れましたが、まず重み付け和法から始めます。
重み付け和法では、各メトリクスに重みを割り当てます。例えば、アラート率と衝突率の相対的な重要度を表す重みベクトルを作成します。通常、これらの重みの合計が1になるように設定します。具体的な例として、アラート率に0.8、衝突率に0.2の重みを与えると、各設計点の値と重みの積の合計が最大となるポイントを選択します。
この方法のポイントは、メトリクス間の相対的な重要性を明示的に定義できることです。ただし、どのようにして適切な重みを決定するかという問題が残ります。これについては後ほど詳しく説明します。
次に目標距離法ですが、これは理想的な目標点からの距離を測定するアプローチです。安全性クリティカルシステムでは通常、「ユートピア点」と呼ばれる理論上の理想点を目標とします。航空機衝突回避システムの場合、これはゼロアラートとゼロ衝突の点になります。現実的には達成不可能ですが、各設計ポイントとこの理想点との距離を計算し、最も近いものを選びます。
最後に紹介する重み付き指数和は、前述の二つの方法を組み合わせたようなものです。基本的には距離測定に重みを導入したアプローチです。数学的には次のように表現されます：
重み付き指数和 = Σ(wi × |fi - gi|^p)^(1/p)
ここでwiは各メトリクスfiの重み、giは目標値、pは距離の測定方法を定義するパラメータです。
これら三つの方法はそれぞれ長所と短所がありますが、システムの要件やステークホルダーの優先事項に応じて適切な方法を選択することが重要です。特に、重み付け和法は直感的で実装が容易なため、多くの実践的なアプリケーションで使用されています。
ただし、重み付け和法を使用する際の課題は、「重みをどのように決定するか」という点です。専門家に直接「アラート率と衝突率の間の重みは何ですか？」と尋ねるのは少し奇妙な質問になります。より自然なアプローチとしては、「この設計とこの設計、どちらを好みますか？」といった形で選好を尋ね、そこから重みを導き出す方法があります。これについては次のセクションで実際のデモンストレーションを通して説明します。
1.3. 重み付けベクトルの学習実験（キャンディ選択デモ）
Sydney Katz: それでは、重み付けベクトルをどのように学習するかについて実験をしてみましょう。キャンディを使ったデモンストレーションを行います。専門家に「M&M's、サワーパッチキッズ、スキットルズに対する重みベクトルを1になるように指定してください」と尋ねるのではなく、対比較によって学習する方法を示します。
この実験では、異なる種類のキャンディを含む袋を用意しました。目標は、ボランティアのキャンディに対する重みベクトルを推定することです。重みベクトルを(W1, W2, W3)と表現し、それぞれM&M's、サワーパッチキッズ、スキットルズに対する重みを表します。この重みベクトルは合計が1になるという制約があります。
このグラフでは、X軸がW1、Y軸がW2を表しています。W3はW1とW2から自動的に決まるため、表示していません。グラフの灰色の部分は制約を満たさない領域で、白い三角形の部分が可能な重みベクトルの領域です。
では、ボランティアの方に質問していきます。最終的に、1個のM&M's、4個のサワーパッチキッズ、5個のスキットルズが入った袋と、5個のM&M's、3個のサワーパッチキッズ、2個のスキットルズが入った袋のどちらかをプレゼントします。しかし、その前に重みベクトルを推定するための質問をします。
最初の質問です。1個のM&M's、3個のサワーパッチキッズ、6個のスキットルズが入った袋Aと、7個のM&M's、1個のサワーパッチキッズ、2個のスキットルズが入った袋Bでは、どちらを選びますか？
ボランティア: 袋Aを選びます。
Sydney Katz: 袋Aを選んだということは、Aの重み付け価値がBより大きいということを意味します。これは私たちの仮定に基づいています。つまり、このボランティアの方は頭の中で重みベクトルを持っており（意識していなくても）、それに基づいて決定を下しているという仮定です。これは必ずしも真実ではないかもしれませんが、今はこの仮定で進めましょう。
Aが好ましいということは、1×W1 + 3×W2 + 6×W3 > 7×W1 + 1×W2 + 2×W3 ということになります。代数的に整理すると、-6W1 + 2W2 + 4W3 > 0 となります。また、W1 + W2 + W3 = 1という制約から、W3 = 1 - W1 - W2 と表せます。これを代入して整理すると、5W1 + W2 < 2 という半空間が得られます。
このグラフでは、線5W1 + W2 = 2より下の部分が、ボランティアの可能な重みベクトルの領域になります。
学生: 半空間とは何ですか？
Sydney Katz: 半空間とは、この形の不等式によって空間が分割され、半分が不等式を満たし、もう半分が満たさない状態を指します。この場合、線の片側では不等式5W1 + W2 < 2を満たし、もう片側では満たしません。「半分」という言葉にあまり拘らなくても大丈夫です。要は可能値の空間を線で区切っているということです。
次の質問に進みましょう。6個のM&M's、1個のサワーパッチキッズ、3個のスキットルズが入った袋と、5個のM&M's、2個のサワーパッチキッズ、3個のスキットルズが入った袋では、どちらを選びますか？
ボランティア: 袋Bを選びます。
Sydney Katz: 同じような計算を行うと、さらに領域が制限されます。次の質問です。2個のM&M's、7個のサワーパッチキッズ、1個のスキットルズが入った袋と、6個のM&M's、2個のサワーパッチキッズ、2個のスキットルズが入った袋では？
ボランティア: 袋Aを選びます。
Sydney Katz: 最後の質問です。より難しいものです。
ボランティア: 袋Bを選びます。
Sydney Katz: これで十分な情報が得られました。これ以上質問を続けることもできますが、現時点で可能な重みベクトルの範囲がかなり絞り込まれています。この段階では、残った領域の中心点を取るなど、様々な方法で最終的な重みベクトルを選ぶことができます。
目視で判断すると、W1=0.2、W2=0.6、W3=0.2が良さそうです。これを使って、最初に言及した最終選択を予測すると、ボランティアの方は袋Aを好むと予測できます。どうでしょうか？
ボランティア: はい、正解です。
Sydney Katz: 素晴らしい！これが重み付けベクトルを学習する方法の一例です。
学生: 質問を選ぶ際に、領域を効率的に狭めるように選んだのですか？また、矛盾する回答が出た場合はどうなりますか？
Sydney Katz: 非常に良い質問です。今回は事前に質問を選んでいましたが、より効率的なアプローチとしては、最初の回答を見てから、残った空間を最大限に分割するような次の質問を選ぶ「アクティブラーニング」という方法があります。これは興味深い研究分野ですが、このクラスの範囲を超えています。
矛盾する回答については、確かにそれは起こり得ます。例えば、ある時点で重みベクトルの可能な領域がなくなってしまう場合です。これは矛盾した選好のセットを得たことを意味します。私たちは人間が完全に合理的で、常に私たちのモデルに従って最適化していると仮定していましたが、それは間違っているかもしれません。
実際、十分な質問を行えば、人間は最終的に不整合な回答をするかもしれません。そのため、多くの研究者はこの仮定を緩和し、重みの確率分布を計算し、人間の選択を確率的にモデル化します。これは大規模言語モデルの強化学習からのヒューマンフィードバック（RLHF）の基本的な考え方にも通じています。
これで複合メトリクスについての説明を終え、次は仕様（スペシフィケーション）について説明します。
2. 論理仕様
2.1. 命題論理
Sydney Katz: さて、次はいよいよ論理仕様に入ります。この部分は正直に言うと、私はいつも少し退屈だと思っていました。しかしながら、これは非常に重要なトピックで、この講座の残りの部分で使用していきますので、なるべく興味深く説明していきます。
論理仕様とは、システムの動作要件を論理式を用いて形式的に定義するものです。論理式とは、真または偽のいずれかに評価される精密な表現です。論理式を定義するにはいくつかの方法がありますが、まず「命題論理」から始めましょう。
命題論理は「命題」で構成されています。命題とは真または偽のいずれかに評価される文です。命題はさらに「原子命題」から構成されることがあります。原子命題とはこれ以上分解できない命題のことです。
私が初めてこれを学んだ時、「原子命題」という言葉と「原子」との関連性がなぜか頭の中でつながりませんでした。しかし、それこそが要点なのです。文字通り、これ以上分解できないということです。科学的に原子はさらに分解できることがわかっていますが、ここでは原子命題を基本単位として、より複雑な命題を構築していくというイメージです。
例えば、これが命題の一例です。まだ記号の意味については心配する必要はありませんが、これは命題であり、これらの原子命題で構成されています。基本的には、AとBが真で、Cが偽である必要があるということを表しています。
命題に適用できる演算子について説明します。最も単純な演算子は「否定」です。命題Pがあるとします。Pは真または偽のいずれかです。「否定P」（not P）はその反対になります。Pが真なら、not Pは偽。Pが偽なら、not Pは真です。これらの真理値表を見ると理解しやすいでしょう。
次の演算子は「論理積」（conjunction）です。これは二つの命題P, Qに適用され、日常言語では「かつ」と考えることができます。これは、PとQの両方が真である場合にのみ真となります。それ以外の組み合わせではすべて偽になります。
また「論理和」（disjunction）もあります。これは「または」のようなものです。PまたはQのいずれかが真、あるいは両方が真である場合に真となります。PとQの両方が偽である場合にのみ偽になります。
学生: すみません、スライドの記号が論理積と同じに見えますが...
Sydney Katz: 良い指摘です。ここで訂正しましょう。論理和の記号は∨で、逆さまのくさび形です。ありがとうございます。
次に「含意」（implication）があります。P implies Qと表記し、「もしPならばQ」と読みます。Pが真でQも真なら、この含意は真です。Pが真でQが偽なら、含意は偽です。しかし、Pが偽の場合は、Qがどうであれ含意は常に真になります。これは条件が成立しない場合、その結果については何も主張していないということです。
最後に「双条件」（biconditional）があります。これは「if and only if（当且つ必要条件）」のようなもので、PとQが同じ値を持つ場合にのみ真になります。つまり、両方真か両方偽の場合に真となります。
具体例を見てみましょう。「エージェントが安全な状態にある場合、エージェントは衝突状態ではない」という文を命題論理で表現したいとします。
まず、論理式を構築するための原子命題を定義する必要があります。最初に原子命題Sを定義し、「エージェントが安全な状態にある場合に真」とします。次に原子命題Cを定義し、「エージェントが衝突状態にある場合に真」とします。
学生: どの演算子を使うべきでしょうか？
Sydney Katz: 含意ですね、正解です。「もし安全な状態にあるならば、衝突状態ではない」という文は、S implies not C と表現できます。ここでは含意演算子と否定演算子の両方を使用しています。
これが命題論理の基本です。非常にシンプルではありますが、形式的な仕様を記述する基盤となります。次回はこれをさらに拡張した一階述語論理について学んでいきましょう。
2.2. 一階述語論理（変数、述語、限量子）
Sydney Katz: 命題論理を理解したところで、次はこれを拡張した「一階述語論理」に進みましょう。一階述語論理は、命題論理に変数、述語、そして限量子を追加することで、より表現力豊かな論理体系となります。
まず「変数」ですが、これは単にドメイン内のオブジェクトを表します。例えば、変数xをエージェントの状態を表すものとして定義できます。
次に「述語」は、変数に対して命題を評価する関数です。例えば、述語P(x)を「エージェントの状態xが安全である場合に真を返す」と定義できます。先ほど変数xはエージェントの状態を表すと言いましたから、P(x)を適用すると、その状態が安全なら真、安全でなければ偽を返すということになります。
同様に、別の述語Q(x)を「状態xが衝突状態である場合に真を返す」と定義することもできます。
この枠組みを使って、前回の例「エージェントが安全な状態にある場合、エージェントは衝突状態ではない」を再表現してみましょう。今回は前回と少し異なるP、Qという文字を使いましたが、本質的には同じことを述べています。命題論理では原子命題S、Cを使いましたが、一階述語論理では述語と変数を使って表現します。
最後に「限量子」について説明しましょう。限量子により、複数の変数に対して述語を評価することができます。二種類の限量子があります。
まず「全称限量子」です。記号は逆さまのAのような形で、「すべての～について」と読みます。この限量子を使うと、ドメイン内のすべての変数が述語を満たす必要があることを表現できます。例えば、「すべての状態が安全状態である必要がある」という要件は、∀x P(x) と書けます。つまり、「すべてのxについて、P(x)が真でなければならない」という意味です。
次に「存在限量子」です。これは後ろ向きのEのような形で、「存在する～がある」と読みます。この限量子は、ドメイン内に述語を満たす変数が少なくとも1つ存在することを表します。例えば、「少なくとも1つの状態が安全状態である」という要件は、∃x P(x) と書けます。「xが存在して、P(x)が真である」という意味です。
具体例を見てみましょう。このグリッドワールドでは、エージェントがセル間を移動でき、赤いセルで示された障害物を避ける必要があります。ここで表現したい仕様は「軌道内のすべての状態において、エージェントは障害物に衝突しない」です。
この仕様を形式化するために、まず述語関数O(x)を定義し、「xが障害物状態である場合に真」とします。そして、「すべての状態において、エージェントは障害物に衝突しない」という要件は、∀x ¬O(x) と表現できます。つまり、「すべてのxについて、O(x)が真ではない」という意味です。
左側の軌道はこの仕様を満たしています。障害物に衝突していないからです。右側の軌道は障害物に衝突しているので、仕様を満たしていません。
もう一つ例を見てみましょう。今度はグリッドワールドに緑色のゴールを追加し、「エージェントはゴール状態に到達し、障害物状態を避ける必要がある」という仕様を考えます。
先ほどと同じくO(x)を「xが障害物状態」を表す述語とし、新たにG(x)を「xがゴール状態」を表す述語として定義します。
この仕様は二つの要件を組み合わせたものです。まず「すべての状態において障害物を避ける」という要件は∀x ¬O(x)で表現できます。次に「ゴールに到達する」という要件は∃x G(x)、つまり「ゴール状態であるような状態xが存在する」と表現できます。
これらを論理積（AND）で結合すると、最終的な仕様は (∀x ¬O(x)) ∧ (∃x G(x)) となります。
学生: 左側の軌道では、ゴールが軌道の中間にあっても、この式は真になりますか？
Sydney Katz: はい、その通りです。この仕様ではゴールに到達することだけを要求しており、到達した後も進み続けても構いません。このケースでは軌道の中間でゴールに到達し、その後別の場所に移動しても、「ゴール状態であるような状態が存在する」という条件は満たされます。
ただし、このクラスで示す例では通常、ゴールや障害物は「終端状態」として扱っています。つまり、いったんゴールに到達すると、システムの動力学上、そこにとどまることを前提としています。しかし、仮にゴール通過後も移動できるシステムであれば、あなたの言う通り、仕様は依然として満たされます。
これが一階述語論理の基本です。変数と述語、そして限量子を導入することで、命題論理よりもはるかに表現力豊かな仕様を記述できるようになりました。次は、この論理をさらに拡張して時間的特性を扱う「時相論理」に進みましょう。
2.3. 時相論理
Sydney Katz: ここからさらに一階述語論理を拡張し、時間的な特性を扱うための「時相論理」について説明します。この講座では主に逐次システムを扱うため、時相論理は私たちにとって非常に重要なツールとなります。
最初に扱う時相論理は「線形時相論理」（Linear Temporal Logic: LTL）と呼ばれるものです。線形時相論理は、状態の線形シーケンス上でのプロパティを指定するための論理体系です。これは単純に、時間軸に沿って一つずつ順番に並んだ状態の集合に対してプロパティを定義するということです。
この講座で主に扱う線形時相論理の演算子は3つあります。教科書にはさらに他の演算子も紹介されていますが、ここでは最も重要な3つに焦点を当てます。
最初の演算子は「Always」（常に）です。これは□（四角）の記号で表され、□P と書きます。LaTeXやJuliaで記述する場合は、「\square」で入力できます。この演算子は「Pが未来のすべての時点で真でなければならない」ことを表します。
これらの図を理解するために、少し丁寧に説明します。X軸は時間を表し、異なる論理式（PとAlways P）を示しています。青い点は、その時点でその論理式が真であることを示し、点がない場合は偽であることを示しています。
例えば、時間ステップ1を見ると、私たちは「そこから未来のすべての時点」を考慮します。このケースでは、時間ステップ1から4まではPが偽ですが、5から10までは真です。しかし「常に」という条件は未来のすべての時点で真でなければならないため、時間ステップ1での「Always P」は偽となります。
同様に、時間ステップ2でも未来にPが偽になる時点があるため「Always P」は偽です。これが続き、時間ステップ5に達すると、そこから先はPが常に真となるため、「Always P」も真になります。これは終わりまで続きます。
学生: 時間ステップ4でも「Always P」は真になりませんか？
Sydney Katz: 時間ステップ4もここでは偽となります。なぜなら、その時点（4）自体ではPが偽だからです。「Always P」が真になるためには、その時点を含む未来のすべての時点でPが真でなければなりません。
次の演算子は「Eventually」（いずれ）です。これは◇（ダイヤモンド）の記号で表され、◇P と書きます。LaTeXでは「\lozenge」で入力できます。この演算子は「Pが未来のある時点で真になる」ことを表します。すべての時点ではなく、少なくとも1つの時点で真であればよいのです。
例えば、時間ステップ1では、未来（具体的には時間ステップ5、6、7）でPが真になる時点があるため、「Eventually P」は真です。同様に時間ステップ2でも真です。しかし、時間ステップ8に達すると、それ以降にPが真になる時点はないため、「Eventually P」は偽となります。
最後の演算子は「Until」（～まで）です。これはU（筆記体のU）で表され、P U Q と書きます。これは少し複雑ですが、次のように解釈します：「未来のある時点tでQが真になり、それまでの間（tを含まない）はPが真である」。
例を見てみましょう。時間ステップ1では、確かに未来にQが真になる時点がありますが、それまでの間、Pが常に真というわけではありません。実際、最初の数ステップではPが偽なので、「P Until Q」も偽です。
しかし、時間ステップ3を見ると、Qは未来のある時点で真になり、それまでの間Pは真なので、「P Until Q」は真となります。これは時間ステップ9まで続きます。時間ステップ10では、それ以降にQが真になる時点がないため、「P Until Q」は偽です。
学生: PとQが時間ステップ6で重なっていますが、これは必要なのですか？
Sydney Katz: 良い質問です。はい、Pは「少なくともQが真になるまで」真である必要があります。そのため、Qが真になる時点でもPが真である必要があります。この小さな重複が必要なのです。
これらの演算子を使って、より複雑な例を見てみましょう。グリッドワールドに青い四角のチェックポイントを追加しました。新しい仕様は「チェックポイントを通過した後にゴールに到達し、常に障害物を避ける」というものです。
ここで、s(t)を時間tでの状態とし、f(s(t))は「時間tでの状態が障害物を含む場合に真」、g(s(t))は「時間tでの状態がゴールである場合に真」、c(s(t))は「時間tでの状態がチェックポイントである場合に真」という述語を定義します。
これらの述語を使って仕様を表現すると、◇g ∧ (¬g U c) ∧ □¬f となります。この式は3つの部分から成り立っています：
- ◇g：いずれゴールに到達する
- ¬g U c：チェックポイントに到達するまではゴールに到達しない
- □¬f：常に障害物を避ける
これらを組み合わせることで、「チェックポイントを通過した後にゴールに到達し、常に障害物を避ける」という要件を形式的に表現しています。
学生: ゴールに到達した後にチェックポイントに行き、再びゴールに戻る軌道は、この仕様を満たしますか？
Sydney Katz: それは興味深い質問です。現在の仕様では、最初にゴールに到達し、その後チェックポイントを通過して再びゴールに戻る軌道は満たしません。なぜなら、「¬g U c」という部分が「チェックポイントに到達するまではゴールに到達しない」ことを要求しているからです。
そのような軌道を許容するには、異なる仕様が必要になるでしょう。即座に答えは思いつきませんが、信号時相論理を使えば表現できるかもしれません。
以上が線形時相論理の基本です。時間的な性質を形式的に指定するための強力なツールとなります。次は、これをさらに拡張した「信号時相論理」に進みましょう。
3. 線形時相論理（LTL）
3.1. 基本演算子（Always, Eventually, Until）
Sydney Katz: 先ほど時相論理について簡単に紹介しましたが、ここではより詳しく線形時相論理（LTL）の基本演算子について説明します。線形時相論理は、時間を線形的なシーケンスとして捉え、その上でプロパティを定義します。
線形時相論理で最も重要な3つの演算子を見ていきましょう。他にも演算子はありますが、この講座では主にこの3つに焦点を当てます。
最初の演算子は「Always」（常に）です。これは四角（□）の記号で表され、式としては「□P」と書きます。これを読む時は「Always P」または「常にP」と読みます。LaTeXやJuliaで記述する場合は、「\square」コマンドでこの記号を入力できます。この演算子の意味は「Pが未来のすべての時点で真でなければならない」というものです。
この演算子の動作を理解するために、時間軸上での評価を見てみましょう。このグラフでは、X軸が時間を表し、命題PとAlways Pの真偽を示しています。青い点は、その時点でその命題が真であることを示しています。点がない場合は、その命題がその時点で偽であることを意味します。
例えば、時間ステップ1を考えてみましょう。「Always P」を評価するには、時間ステップ1以降のすべての時点でPが真かどうかを確認します。このケースでは、時間ステップ1から4まではPが偽ですので、「Always P」も時間ステップ1では偽になります。
同様に、時間ステップ2でも、未来にPが偽になる時点があるため、「Always P」は偽です。これが続き、時間ステップ5に達すると、そこから先はPが常に真となるため、「Always P」も真になります。これは終わりまで続きます。
次の演算子は「Eventually」（いずれ）です。これはダイヤモンド（◇）の記号で表され、「◇P」と書きます。LaTeXでは「\lozenge」で入力できます。この演算子の意味は「Pが未来のある時点で真になる」というものです。すべての時点ではなく、少なくとも1つの時点で真であればよいのです。
例えば、時間ステップ1では、未来（具体的には時間ステップ5、6、7）でPが真になる時点があるため、「Eventually P」は真です。時間ステップ2や6でも同様に真です。しかし、時間ステップ8に達すると、それ以降にPが真になる時点はないため、「Eventually P」は偽となります。
最後の演算子は「Until」（～まで）です。これはU（筆記体のU）で表され、「P U Q」と書きます。これは次のように解釈します：「未来のある時点でQが真になり、かつPはQが真になるまで（その時点を含めて）真である」。
この演算子は少し複雑なので、例を使って説明します。時間ステップ1では、確かに未来にQが真になる時点がありますが、それまでの間（時間ステップ1から4）、Pが常に真というわけではありません。実際、これらの時点ではPが偽なので、「P Until Q」も偽です。
時間ステップ3を見ると、未来にQが真になる時点があり、それまでの間（時間ステップ3から4）Pは真なので、「P Until Q」は真となります。これは時間ステップ9まで続きます。しかし、時間ステップ10では、それ以降にQが真になる時点がないため、「P Until Q」は偽です。
学生: PとQが時間ステップ6で重なっていますが、これは必要なのですか？
Sydney Katz: そうですね、Pは「少なくともQが真になるまで」真である必要があります。この条件では、Qが真になる時点まではPが真である必要がありますので、この重複は必要なのです。
これらの3つの基本演算子を理解することで、非常に多様な時間的性質を表現できるようになります。Alwaysは「安全性」、Eventuallyは「活性」、そしてUntilは「順序性」のような性質を表現するのに役立ちます。
例えば、自動運転車では「常に他の車両との安全距離を保つ」という安全性プロパティを□(safe_distance)と表現できます。また、「最終的に目的地に到達する」という活性プロパティは◇(at_destination)と表現できます。「燃料が尽きるまで走行を続ける」という性質は(running) U (no_fuel)のように表現できます。
これらの演算子を組み合わせることで、より複雑な時間的プロパティを表現することが可能です。次のセクションでは、これらの演算子をグリッドワールドの例に適用して、具体的な使用方法を見ていきます。
3.2. グリッドワールド例題
Sydney Katz: 線形時相論理の基本演算子を理解したところで、具体的な例題を通してその応用を見ていきましょう。ここでは、グリッドワールドというシンプルな環境を使います。このグリッドワールドでは、エージェントがセル間を移動することができ、特定のセルが障害物やゴールなどの特別な意味を持ちます。
まず最初の例として、赤いセルで示された障害物を含むグリッドワールドを考えてみましょう。この環境でエージェントに課したい要件は「軌道内のすべての状態において、エージェントは障害物に衝突しない」というものです。
これを線形時相論理で表現するために、述語関数O(x)を定義しましょう。O(x)は「状態xが障害物状態である場合に真」を返します。次に「すべての状態において障害物に衝突しない」という要件は、□¬O(x)と表現できます。つまり、「常に（Always）、障害物状態でない」ということです。
この図の左側には、仕様を満たす軌道の例を示しています。この軌道では、エージェントは障害物を避けながら移動しています。右側には、仕様を満たさない軌道の例があります。この軌道ではエージェントが障害物に衝突しているため、□¬O(x)が偽となります。
次に、より複雑な例を見てみましょう。グリッドワールドに緑色のゴールセルを追加します。新しい要件は「エージェントはゴール状態に到達し、かつ障害物状態を避ける必要がある」というものです。
この要件を表現するために、O(x)に加えて新たな述語G(x)を定義します。G(x)は「状態xがゴール状態である場合に真」を返します。「ゴール状態に到達する」という要件は◇G(x)、つまり「いずれ（Eventually）ゴール状態になる」と表現できます。「障害物状態を避ける」という要件は先ほどと同じく□¬O(x)です。
これらを組み合わせると、最終的な仕様は(◇G(x)) ∧ (□¬O(x))となります。これは「いずれゴール状態に到達し、常に障害物状態を避ける」ことを意味します。
図の左側はこの仕様を満たす軌道の例です。エージェントは障害物を避けながらゴールに到達しています。右側の軌道は障害物は避けていますが、ゴールに到達していないため、仕様の一部(◇G(x))を満たしておらず、全体としても仕様を満たしていません。
学生: ゴール状態が軌道の途中にあり、その後もエージェントが移動を続ける場合も、この仕様は満たされますか？
Sydney Katz: 良い質問です。はい、その通りです。この仕様では「いずれゴール状態に到達する」ことのみを要求しており、到達した後に他の状態に移動することを禁止していません。従って、軌道の途中でゴールに到達し、その後も移動を続ける場合でも仕様は満たされます。
さらに、もう一つ複雑な例を考えてみましょう。今度はグリッドワールドに青いチェックポイントセルを追加します。新しい要件は「チェックポイントを通過した後にゴールに到達し、常に障害物を避ける」というものです。
この要件を表現するために、時間tにおける状態をs(t)と表し、次の述語を定義します：
- f(s(t)): 時間tでの状態が障害物を含む場合に真
- g(s(t)): 時間tでの状態がゴールである場合に真
- c(s(t)): 時間tでの状態がチェックポイントである場合に真
これらの述語を使って仕様を表現すると、◇g ∧ (¬g U c) ∧ □¬f となります。この式は3つの部分から成り立っています：
- ◇g：いずれゴールに到達する
- ¬g U c：チェックポイントに到達するまではゴールに到達しない（つまり、チェックポイントを通過した後にゴールに到達する）
- □¬f：常に障害物を避ける
この例では、エージェントはまずチェックポイントを通過し、その後でゴールに到達する必要があります。また、常に障害物を避ける必要もあります。
図の軌道はこの仕様を満たしています。エージェントはまず青いチェックポイントを通過し、その後緑のゴールに到達し、全過程で赤い障害物を避けています。
学生: 最初にゴールに到達し、その後チェックポイントを通過して再びゴールに戻るような軌道は、この仕様を満たしますか？
Sydney Katz: いいえ、そのような軌道はこの仕様を満たしません。なぜなら、¬g U c の部分は「チェックポイントに到達するまではゴールに到達しない」ことを要求しているからです。最初にゴールに到達してしまうと、この条件に違反することになります。
このように、線形時相論理を使うことで、エージェントの行動に関する様々な時間的要件を形式的に表現することができます。これらの表現は後でシステムの検証や設計に活用されます。
次のセクションでは、これをさらに拡張して実数値信号を扱える「信号時相論理」（Signal Temporal Logic: STL）について学んでいきます。
4. 信号時相論理（STL）
4.1. 実数値信号への拡張
Sydney Katz: ここからは「信号時相論理」（Signal Temporal Logic: STL）について説明します。信号時相論理は、線形時相論理を拡張して実数値の信号に対するプロパティを指定できるようにしたものです。このセクションでは特に、実数値信号への拡張について説明します。
まず「信号」とは何かを定義しましょう。信号とは、時間の経過とともに値が変化するものです。グラフ上で表現すると、横軸に時間、縦軸に値をとり、ある時点における信号の値を点で表します。信号を定義するには、各測定点の時間と、その時点での値を指定する必要があります。
重要なポイントとして、信号の測定は必ずしも一定の時間間隔で行われる必要はありません。必要なのは、時間の集合と対応する実数値の集合だけです。
信号時相論理が線形時相論理を超えて提供する新しい機能は主に2つあります。
1つ目は、時間間隔に対するプロパティの指定です。例えば、時間aからbまでの間にプロパティPがいずれ成立する必要がある、という要件を指定できます。これは◇[a,b] P と表記します。これは「時間aからbの間にいずれPが成立する」という意味です。
この時間間隔の指定により、「システムは起動後10秒以内に準備完了状態になる」といった具体的な時間制約を持つ要件を表現できるようになります。
学生: これは通常の「Eventually」と何が違うのでしょうか？
Sydney Katz: 良い質問です。通常の「Eventually」（◇P）は「いつか将来のある時点でPが成立する」ことを要求しますが、時間的な制約はありません。対して◇[a,b] P は「時間aからbの間でPが成立する」ことを要求します。これにより、いつPが成立する必要があるかを明確に制限できます。例えば、「システムは10秒以内に応答する」といった具体的な時間制約を表現できるのです。
2つ目の拡張は、実数値信号を真理値（真または偽）にマッピングするための仕組みです。これにより、連続的な値を持つセンサーデータなどに対して論理的なプロパティを定義できるようになります。
信号時相論理では、新しい形式の述語関数μc(s)を導入します。この関数は、状態sに何らかの関数μを適用し、その結果がある定数値cより大きいかどうかをチェックします。つまり、μ(s) > c であれば真、そうでなければ偽となります。
例えば、自動運転車のブレーキ圧力を表す信号があるとします。μ(s) = s と定義し、c = 5 とすれば、ブレーキ圧力が5を超えているときに真となる述語ができます。これにより「ブレーキ圧力が常に5を超えている」といった要件を□(μ5(s))のように表現できます。
また、航空機の高度を表す信号に対して、μ(s) = s、c = 10000 とすれば、高度が10000フィート以上であるときに真となる述語ができます。これにより「離陸後5分以内に高度10000フィート以上に達する」といった要件を◇0,300のように表現できます。
このグラフは実数値信号の例を示しています。信号の値が閾値cを超えている部分では述語μc(s)が真となり、それ以外の部分では偽となります。このような形で、連続的な値を持つ信号に対して離散的な論理判断を行うことができます。
信号時相論理の大きな利点は、実世界の物理システムで一般的に扱われる連続値データに対して、形式的な検証手法を適用できることです。例えば、温度センサーの値が特定の閾値を超えないことや、車両が安全な速度範囲内で走行することなど、現実的な制約を形式的に表現し検証できます。
次のセクションでは、信号時相論理における時間間隔の指定について、より詳しく説明します。これにより、「特定の時間帯にのみ成立すべき性質」などを精密に表現できるようになります。
4.2. 時間間隔でのプロパティ指定
Sydney Katz: 信号時相論理（STL）のもう一つの重要な拡張機能は、時間間隔に対するプロパティの指定です。これにより、特定の時間帯に限定したプロパティを表現できるようになります。
時間間隔の指定は[a,b]のように表され、aからbまでの閉区間を意味します。例えば、◇[a,b] P と表記すると、「時間間隔[a,b]の間にいずれPが成立する」ことを表します。同様に、□[a,b] P は「時間間隔[a,b]の間、常にPが成立する」ことを意味します。
この機能の重要性を理解するために、具体例を見てみましょう。通常の線形時相論理では、「いずれPが成立する」（◇P）という表現はできますが、「特定の時間内にPが成立する」という時間的制約を加えることはできません。信号時相論理を使えば、「システムは起動後10秒以内に応答する」（◇[0,10] response）といった具体的な時間制約を持つ要件を表現できます。
学生: 時間間隔[a,b]の間にEventuallyが成立するとはどういう意味ですか？bの時点でも成立する必要がありますか？
Sydney Katz: 良い質問です。◇[a,b] P という表現は、時間間隔[a,b]のどこかの時点でPが成立することを要求します。つまり、aからbの間（両端を含む）の少なくとも1つの時点でPが真になればよいのです。必ずしもbの時点で成立する必要はありません。
例えば、時間a=5, b=10でのEventuallyを考えると、時間5から10の間のどこかでPが真になれば、◇[5,10] P は満たされます。これは「5秒から10秒の間に少なくとも一度、条件Pが満たされる」ことを意味します。
学生: 時間間隔の表記で、開区間と閉区間を区別できますか？例えば、bを含まない場合など。
Sydney Katz: 技術的には可能です。通常、STLでは閉区間[a,b]（aとbを含む）を使用することが一般的な規約ですが、開区間(a,b)（aとbを含まない）や半開区間[a,b)（aを含むがbを含まない）、(a,b]（aを含まないがbを含む）を使用することも可能です。
ただし、実装上は閉区間[a,b]を使用するのが標準的な慣習となっています。これは離散的なサンプリングを行う多くの実際のシステムでは、厳密な開区間と閉区間の区別があまり意味を持たないためです。
時間間隔の指定は、実世界のシステムで特に重要です。例えば、航空機の衝突回避システムでは「水平方向の分離が失われる40秒から41秒の間、常に垂直方向の分離が50m以上ある」という要件を□40,41のように表現できます。
また、自動運転車では「交差点に接近している間（時間間隔[t1,t2]）、速度は30km/h未満である」という要件を□t1,t2のように表現できます。
さらに、医療機器では「薬剤投与後30分以内に患者の血圧が正常範囲に戻る」という要件を◇0,30のように表現できます。
時間間隔の指定により、STLは実世界の時間制約を持つシステムの仕様をより精密に表現できるようになります。これは特に安全性クリティカルなシステムで重要です。なぜなら、「いつか」条件が満たされるだけでなく、「特定の時間内に」条件が満たされることが求められるからです。
次のセクションでは、STLのもう一つの重要な概念である「ロバストネス」について説明します。これは単にプロパティが満たされるか否かだけでなく、どの程度の余裕を持って満たされるか（または満たされないか）を数値化する概念です。
4.3. ロバストネスの概念
Sydney Katz: 信号時相論理（STL）の非常に興味深い概念として「ロバストネス」があります。これはプロパティが単に真か偽かを判定するだけでなく、どれだけの余裕をもって満たしている（あるいは満たしていない）かを数値化するものです。
この概念を説明するために、シンプルな例から始めましょう。信号の一時点t、その値s(t)、そして述語μc(s(t))を考えます。この述語は、s(t)の値が定数cより大きいかどうかを判定します。
簡単にするために、μ(s(t)) = s(t)と定義してみましょう。つまり、この述語はs(t) > cを判定するだけです。
ここで、いくつかのケースを比較してみましょう。それぞれの場合に自分の直感がどうかを考えてみてください。
- まず、信号値がしきい値をはるかに上回るケース。プロパティは満たされていますが、かなりの余裕があります。
- 次に、信号値がしきい値をわずかに上回るケース。プロパティは満たされていますが、かろうじて満たしているという感じです。
- 信号値がしきい値をわずかに下回るケース。プロパティは満たされておらず、あと少しで満たされるところでした。
- 最後に、信号値がしきい値をはるかに下回るケース。プロパティはまったく満たされていません。
これらのケースでは、同じプロパティでも私たちの直感的な感覚は異なります。伝統的な二値論理では、1と2は単に「真」、3と4は単に「偽」となり、その差は表現できません。しかし、STLのロバストネスを使うと、これらの違いを数値化できるのです。
ロバストネスは、プロパティをどの程度の余裕をもって満たしているかを測る値です。具体的には：
- ロバストネスが正の値（>0）の場合、プロパティは満たされている
- ロバストネスが負の値（<0）の場合、プロパティは満たされていない
- ロバストネスの絶対値が大きいほど、満たす（または満たさない）余裕が大きい
先ほどの例に戻ると、1番目のケースではロバストネスは大きな正の値、2番目のケースではわずかに正の値、3番目のケースではわずかに負の値、4番目のケースでは大きな負の値となります。
このシンプルな述語μc(s(t))のロバストネスは、単にμ(s(t)) - cで計算できます。例えば、c = 5でs(t) = 10であれば、ロバストネスは10 - 5 = 5となります。反対に、s(t) = 3であれば、ロバストネスは3 - 5 = -2となります。
学生: ロバストネスの値は無限に大きくなる可能性がありますが、どの程度の値が「十分に堅牢」と判断すればよいのでしょうか？
Sydney Katz: とても良い質問です。確かにロバストネスは理論上は無限に大きくなる可能性があります。何が「十分」かという判断は、アプリケーションの性質によって異なります。
一般的な目安としては、ロバストネスが0に近い場合、システムは「ぎりぎり」でプロパティを満たしており、わずかな変動でプロパティを満たさなくなる可能性があると考えられます。
実際のアプリケーションでは、ロバストネスは元の信号と同じ単位を持つことがよくあります。例えば、航空機の安全間隔が50メートル以上という要件のロバストネスは、メートル単位で表されます。その場合、ロバストネス値5は「安全マージンが5メートル」という意味になり、これが十分かどうかはアプリケーションの文脈で判断できます。
また、ロバストネスは最適化の目的関数としても非常に役立ちます。例えば、システムの故障を見つけたい場合、ロバストネスを最小化する入力を探します。ロバストネスが負になると、プロパティが満たされていない故障ケースを見つけたことになります。このような最適化の文脈では、ロバストネスの絶対的な値よりも、それを最大化または最小化することが重要になります。
ロバストネスの概念は、単に「システムが仕様を満たすか否か」という二値的な判断を超えて、「どの程度の余裕をもって満たすか」を定量的に評価できるようにします。これにより、システム設計の早い段階で潜在的な問題を特定したり、設計の堅牢性を向上させたりすることが可能になります。
次のセクションでは、より複雑な論理式に対するロバストネス計算の方法について詳しく説明します。命題演算子や時相演算子を含む式のロバストネスをどのように計算するかを見ていきましょう。
5. STLロバストネス
5.1. ロバストネス計算方法
Sydney Katz: ここからは信号時相論理（STL）におけるロバストネスの計算方法について詳しく説明します。ロバストネスは、システムが仕様をどの程度の余裕をもって満たしているか（または満たしていないか）を数値化する重要な概念です。
まず、最も基本的なケースから始めましょう。一つの時間ステップtにおける信号値s(t)と、μc(s(t))という形式の述語を考えます。前回説明したように、この述語はs(t)に関数μを適用した結果が定数cより大きいかどうかを判定します。
簡単にするために、μ(s(t)) = s(t)と定義します。つまり、s(t) > cという単純な条件になります。このようなシンプルな述語のロバストネスは、μ(s(t)) - cで計算できます。これは直感的に「信号値がしきい値を超える余裕」を表しています。
例えば、c = 5とし、異なる信号値でロバストネスを計算してみましょう：
- s(t) = 10の場合：ロバストネス = 10 - 5 = 5（正の値なので、プロパティを満たし、余裕も十分）
- s(t) = 6の場合：ロバストネス = 6 - 5 = 1（正の値だが小さいので、かろうじて満たしている）
- s(t) = 4の場合：ロバストネス = 4 - 5 = -1（負の値なので、プロパティを満たさず、あと少しで満たせる）
- s(t) = 1の場合：ロバストネス = 1 - 5 = -4（大きな負の値なので、プロパティを大きく満たしていない）
このように、ロバストネスの値は単にプロパティが満たされるか（正の値）、満たされないか（負の値）を示すだけでなく、その程度も表します。値が0に近いほど、条件の境界に近いことを意味します。
実際のアプリケーションでは、ロバストネスは元の信号と同じ単位を持つことが多いです。例えば、航空機の高度に関する条件のロバストネスはメートル単位で表されます。これにより、ロバストネス値の解釈が直感的になります。例えば、「安全間隔のロバストネスが10メートル」という情報は、「現在の間隔は必要最小限より10メートル多い」という意味に直接対応します。
ロバストネスの計算は、より複雑な述語にも拡張できます。例えば、μ(s(t))がs(t)を直接返すのではなく、より複雑な関数である場合でも、基本的な計算方法は同じです。例えば、μ(s(t)) = |s(t)|（絶対値）やμ(s(t)) = s(t)²（二乗）などの場合でも、ロバストネスはμ(s(t)) - cで計算されます。
また、述語の条件が「より大きい」（>）ではなく「より小さい」（<）の場合は、ロバストネスの計算が反転します。つまり、s(t) < cという条件のロバストネスはc - μ(s(t))となります。
しかし、実用的なシステムでは、単一の述語だけでなく、複数の述語を論理演算子や時相演算子で組み合わせた複雑な式を扱うことがほとんどです。例えば、「速度が安全範囲内にあり、かつ障害物との距離が十分である」といった複合条件です。
このような複合条件のロバストネスを計算するためには、各演算子（論理積、論理和、否定など）に対応するロバストネス計算規則を定義する必要があります。次のセクションでは、これらの命題演算子に対するロバストネス計算方法について詳しく説明します。
ロバストネスの概念は、システムの検証や最適化に非常に役立ちます。例えば、設計の初期段階でロバストネスを計算することで、仕様をかろうじて満たす「危ない」ケースを特定し、設計を改善することができます。また、ロバストネスを最大化する制御戦略を求めることで、より堅牢なシステムを設計することも可能です。
5.2. 命題演算子に対するロバストネス
Sydney Katz: ここからは、複数の述語を組み合わせた論理式のロバストネスを計算する方法を説明します。特に命題論理演算子（否定、論理積、論理和、含意）に対するロバストネス計算規則を見ていきましょう。
まず、最も単純な演算子である「否定」から始めます。命題Pに対する否定（not P）のロバストネスは、Pのロバストネスの負の値として定義されます：
ρ(¬P) = -ρ(P)
これは直感的にも理解できます。Pを満たす余裕が大きい（正のロバストネス）ほど、¬Pを満たすことからは遠くなります（大きな負のロバストネス）。逆に、Pを満たさない度合いが大きい（負のロバストネス）ほど、¬Pを満たす余裕が大きくなります（正のロバストネス）。
例えば、先ほどの例でc = 5、s(t) = 10のとき、P（s(t) > 5）のロバストネスは5でした。このとき、¬P（s(t) ≤ 5）のロバストネスは-5となります。これは、現在の値が条件を満たすには5単位分減少する必要があることを意味します。
次に「論理積」（AND、∧）を考えます。命題PとQの論理積（P ∧ Q）のロバストネスは、PとQのロバストネスの最小値として定義されます：
ρ(P ∧ Q) = min(ρ(P), ρ(Q))
これは両方の条件を満たす必要があるため、最も満たしにくい条件（ロバストネスが最も小さい条件）が全体のロバストネスを決定するという考え方です。チェーンの強さはその最も弱いリンクによって決まるのと同じ原理です。
例えば、P（s(t) > 5）のロバストネスが2で、Q（s(t) > 3）のロバストネスが4の場合、P ∧ Qのロバストネスはmin(2, 4) = 2となります。これは直感的に正しいです。なぜなら、s(t)が両方の条件を満たさなくなるまでに減少できる最大量は2だからです。
同様に「論理和」（OR、∨）は、どちらか一方の条件を満たせばよいため、最も満たしやすい条件（ロバストネスが最も大きい条件）を選びます：
ρ(P ∨ Q) = max(ρ(P), ρ(Q))
先ほどの例でP（s(t) > 5）のロバストネスが2、Q（s(t) > 3）のロバストネスが4の場合、P ∨ Qのロバストネスはmax(2, 4) = 4となります。これはs(t)が少なくともどちらかの条件を満たさなくなるまでに減少できる最大量が4であることを意味します。
最後に「含意」（P → Q）ですが、これはやや複雑です。含意のロバストネスは次のように定義されます：
ρ(P → Q) = max(-ρ(P), ρ(Q))
これは含意P → Qが¬P ∨ Qと論理的に等価であることから導かれます。実際、教科書には含意のロバストネス計算を導出する演習問題があります。興味がある方はぜひ取り組んでみてください。
これらのルールを組み合わせることで、任意の複雑さを持つ命題論理式のロバストネスを計算できます。例えば、複合条件(P ∧ Q) ∨ ¬Rのロバストネスは、max(min(ρ(P), ρ(Q)), -ρ(R))として計算できます。
学生: P ∧ Qのような複合条件の例はどのようなものがありますか？
Sydney Katz: 良い質問です。例えば、航空機の安全要件として「高度が200メートル以上であり、かつ500メートル以下である」という条件を考えましょう。これをP ∧ Qと表現すると、P（高度 > 200）とQ（高度 < 500）の両方を満たす必要があります。
現在の高度が300メートルの場合、Pのロバストネスは300 - 200 = 100、Qのロバストネスは500 - 300 = 200となります。P ∧ Qのロバストネスはmin(100, 200) = 100です。つまり、高度が100メートル減少するか、200メートル増加すると、安全条件を満たさなくなります。このうち小さい方の100が全体のロバストネスとなります。
学生: 含意P → Qの具体例はどのようなものですか？
Sydney Katz: 含意の例としては、「システムが安全状態にある場合、衝突状態ではない」という条件が考えられます。これをP → Qと表現すると、P（安全状態）を満たすならQ（非衝突状態）も満たす必要があります。
安全状態の定義をセンサー値s(t) > 5とし、非衝突状態の定義をs(t) < 10としましょう。現在のs(t) = 7の場合、Pのロバストネスは7 - 5 = 2、Qのロバストネスは10 - 7 = 3となります。P → Qのロバストネスはmax(-2, 3) = 3となります。
これは直感的には少し理解しづらいかもしれませんが、含意P → Qが¬P ∨ Qと等価であることを考えると理解しやすくなります。¬Pのロバストネスは-2、Qのロバストネスは3なので、¬P ∨ Qのロバストネスはmax(-2, 3) = 3となります。
このように、命題演算子に対するロバストネス計算規則を使うことで、複雑な論理条件のロバストネスを体系的に計算できます。これにより、システムが仕様をどの程度の余裕をもって満たしているかを定量的に評価できるのです。
次のセクションでは、時間的な要素を含む時相演算子（Always、Eventually、Until）に対するロバストネス計算方法を説明します。これにより、時間の経過とともに変化する信号に対する性質のロバストネスを評価できるようになります。
5.3. 時相演算子に対するロバストネス
Sydney Katz: 命題演算子に対するロバストネス計算を理解したところで、次は時相演算子（Always、Eventually、Until）に対するロバストネス計算方法を説明します。これらの演算子は時間的な要素を含むため、単一の時点だけでなく、軌道全体を考慮する必要があります。
これまでの例では一つの時間ステップtについて考えていましたが、今度は時間の経過に伴う信号の軌道全体を考えます。例として、cが0に設定されている場合を考えましょう。つまり、信号値がプラスならその時点でその述語が真、マイナスなら偽ということになります。
まず「Eventually」（◇）演算子から始めましょう。「Eventually P」は、将来のある時点でPが成立することを要求します。ロバストネスの観点からは、最も「良い」時点でのPのロバストネスを選ぶことになります。つまり：
ρ(◇P) = max_{t∈[t_current,∞)} ρ(P, t)
これは「現在から未来のすべての時点におけるPのロバストネスの最大値」を意味します。なぜこれが適切かというと、少なくとも1つの時点でPが成立すればよいからです。最もPを満たしやすい（ロバストネスが最大の）時点を選べばよいのです。
グラフで具体例を見てみましょう。この軌道で最もロバストネスが大きい点（つまり信号値が最も高い点）を選ぶと、これが「Eventually P」のロバストネスとなります。
次に「Always」（□）演算子を考えます。「Always P」は、すべての将来の時点でPが成立することを要求します。ロバストネスの観点からは、最も「悪い」時点でのPのロバストネスを選ぶことになります。つまり：
ρ(□P) = min_{t∈[t_current,∞)} ρ(P, t)
これは「現在から未来のすべての時点におけるPのロバストネスの最小値」を意味します。すべての時点でPが成立する必要があるため、最も満たしにくい（ロバストネスが最小の）時点がボトルネックとなるからです。
グラフで見ると、この軌道で最もロバストネスが小さい点（つまり信号値が最も低い点）が「Always P」のロバストネスとなります。
最後に「Until」（U）演算子ですが、これはやや複雑です。「P Until Q」は「将来のある時点でQが成立し、それまではPが成立する」ことを要求します。このロバストネスは次のように定義されます：
ρ(P U Q) = max{t'∈[t_current,∞)} min(ρ(Q, t'), min{t∈[t_current,t']} ρ(P, t))
これは一見複雑ですが、直感的には次のように理解できます：まずQが成立する各時点t'を考え、「t'でのQのロバストネスと、t_currentからt'までのすべての時点でのPのロバストネスの最小値」を計算します。これをすべてのt'について計算し、その最大値を取ります。
つまり、「P Until Q」のロバストネスは、「Qが最も強く成立し、かつその時点までのPの成立の度合いが最も弱い部分があまり弱くない」ような時点に対応します。
学生: この式は複雑ですね。もう少し直感的に説明していただけますか？
Sydney Katz: 確かに「Until」のロバストネス計算式は複雑です。もう少し直感的に説明しましょう。
「P Until Q」が成立するためには、(1)いずれQが成立する必要があり、(2)Qが成立するまでの間はずっとPが成立している必要があります。ロバストネスの観点からは、Qが成立する各可能な時点について、「その時点でのQのロバストネスと、それまでのすべての時点でのPのロバストネスの最小値」のペアを考えます。
このペアの中で最も小さい値がその時点での「P Until Q」の「候補となるロバストネス」です。なぜなら、チェーンの強さはその最も弱いリンクによって決まるからです。そして、すべての可能な時点についてこの「候補となるロバストネス」を計算し、その中で最大のものを選びます。
このように、「P Until Q」のロバストネスは「Qが十分に強く成立し、かつその時点までのPの成立も十分に強い」ような最適な時点を探す問題と見ることができます。
これらの時相演算子に対するロバストネス計算方法を理解することで、時間的に変化する信号に対する複雑な要件のロバストネスを評価できるようになります。例えば「システムは常に安全状態を維持し、最終的に目標状態に到達する」といった要件のロバストネスを計算できます。
このロバストネスの計算は、システムの検証や最適化に非常に役立ちます。例えば、設計のどの側面が最もクリティカルか（ロバストネスが最小となる部分）を特定したり、ロバストネスを最大化するような制御戦略を見つけたりすることができます。
しかし、これらのロバストネス計算には一つの大きな課題があります。min関数とmax関数は微分不可能な点を持つため、最適化アルゴリズムで重要な勾配計算が難しくなります。この問題を解決するために、次のセクションでは「スムースロバストネス」という概念を導入します。
6. スムースロバストネス
6.1. 勾配計算の問題
Sydney Katz: これまでSTLロバストネスについて説明してきましたが、このセクションではロバストネスを最適化に使用する際の重要な課題と、その解決策である「スムースロバストネス」について説明します。
講座の後半で詳しく見ていきますが、ロバストネスはシステムの検証や最適化において非常に有用です。例えば、システムの欠陥を見つけるためにロバストネスを最小化したり、システムの堅牢性を高めるためにロバストネスを最大化したりする問題を解くことがあります。
これらの最適化問題を効率的に解くためには、多くの場合、ロバストネスの勾配（微分）が必要になります。勾配は最適化の方向を示す重要な情報です。しかし、先ほど説明したロバストネス計算には、min関数やmax関数が含まれており、これらの関数は微分不可能な点を持つため、勾配計算に問題が生じます。
具体的な例を見てみましょう。再び、cが0に設定されている軌道を考えます。「Eventually P」（◇P）のロバストネスは、軌道上のすべての時点でのPのロバストネスの最大値として計算されます。この例では、時間ステップ5での値が最大なので、ロバストネスはs(5)となります。
ここで、各時間ステップでの状態s(t)に関するロバストネスの勾配を考えてみましょう。s(1)を少し変えた場合、ロバストネスにどのような影響があるでしょうか？答えは「何の影響もない」です。なぜなら、ロバストネスはs(5)にのみ依存しており、s(1)には依存していないからです。したがって、s(1)に関する勾配は0です。
同様に、s(2)、s(3)、s(4)に関する勾配も0です。s(5)に関する勾配は1です（s(5)がロバストネスそのものなので）。そして、s(6)以降に関する勾配も再び0になります。
このように、勾配は極めて「スパース」になり、ほとんどの状態変数に関して0になります。これは最適化アルゴリズムにとって非常に問題です。勾配が0の領域では、アルゴリズムはどの方向に進むべきか判断できないからです。
図示すると、勾配は時間ステップ5でのみ非ゼロで、他のすべての時点ではゼロになります。これは、最大値を与える点が変わるまでは、他の点を変更してもロバストネスに影響しないためです。
学生: この問題は実際のシステム最適化でどのような影響がありますか？
Sydney Katz: 良い質問です。実際のシステム最適化では、この「スパース」な勾配が原因で、勾配ベースの最適化アルゴリズムが非効率になったり、局所最適解に陥りやすくなったりします。
例えば、自動運転車の軌道最適化を考えてみましょう。「常に障害物と安全距離を保つ」という要件のロバストネスを最大化したいとします。通常のロバストネス計算を使うと、最も危険な時点（ロバストネスが最小の時点）でのみ勾配が非ゼロになります。つまり、アルゴリズムはその特定の時点での衝突回避のみに焦点を当て、軌道全体の改善には効果的ではありません。
また、勾配が突然変化する（あるポイントが最大/最小を与える点から別のポイントに切り替わる）ため、最適化プロセスが不安定になることもあります。これは収束を遅くしたり、場合によっては発散させたりする原因になります。
この問題を解決するためには、ロバストネス関数をより滑らかなものにする必要があります。つまり、特定の状態変数だけでなく、複数の状態変数がロバストネスに寄与するようにするのです。それが「スムースロバストネス」の基本的な考え方です。
スムースロバストネスでは、min関数とmax関数を、それらの滑らかな近似であるソフトミン（softmin）とソフトマックス（softmax）で置き換えます。これにより、勾配はより多くの状態変数に広がり、最適化アルゴリズムはより効率的に動作できるようになります。
実際、この手法は強化学習やモデル予測制御など、多くの最適化ベースの制御アプローチで採用されています。スムースな目的関数は、より効率的で安定した最適化を可能にするのです。
次のセクションでは、このソフトミンとソフトマックスの関数について詳しく説明し、実際にどのように通常のロバストネス計算を「スムース化」するかを見ていきます。
6.2. ソフトミンとソフトマックス
Sydney Katz: 先ほど説明した勾配計算の問題を解決するために、「ソフトミン」と「ソフトマックス」という概念を導入します。これらは通常のmin関数とmax関数の滑らかな近似で、勾配計算を容易にします。
ソフトマックス関数は次のように定義されます：
softmax_w(s₁, ..., sₙ) = (Σᵢ sᵢ · e^(w·sᵢ)) / (Σᵢ e^(w·sᵢ))
同様に、ソフトミン関数は次のように定義されます：
softmin_w(s₁, ..., sₙ) = (Σᵢ sᵢ · e^(-w·sᵢ)) / (Σᵢ e^(-w·sᵢ))
これらの関数には、スムース化の度合いを制御するパラメータwが含まれています。wの値によって、関数がどの程度通常のmin/max関数に近いか、あるいは平均に近いかが決まります。
ここで、wの効果について詳しく説明します。スライドと実際のコードでの定義に不一致があるようですが、私の理解では：
- w = 0のとき：ソフトマックス/ソフトミンは単なる入力値の算術平均になります。つまり、すべての入力値が均等に寄与します。
- wが大きくなるにつれて：ソフトマックス/ソフトミンは通常のmax/min関数に近づきます。wが無限大に近づくと、ソフトマックスは通常のmax関数と同じ振る舞いをし、ソフトミンは通常のmin関数と同じ振る舞いをします。
学生: スライドとコードでの定義が逆になっているように見えますが...
Sydney Katz: 鋭い指摘ありがとうございます。実は私もそれに気付きました。スライドとコードでの定義に不一致があるようです。おそらく一方が間違っているのでしょう。後で確認して訂正します。基本的な考え方としては、wを0から大きくしていくにつれて、ソフトマックス/ソフトミンは平均から通常のmax/min関数に近づくと考えてください。
これらの関数の重要な特性は、滑らかであり（微分可能であり）、かつすべての入力値がある程度結果に寄与することです。つまり、どの入力値に関する勾配も完全にゼロにはならないのです。
例として、「Eventually P」のロバストネス計算を考えてみましょう。通常のロバストネス計算では、max関数を使用して軌道上のすべての時点でのPのロバストネスの最大値を取ります。これをソフトマックスで置き換えると：
ρ_smooth(◇P) = softmax_w(ρ(P, t₁), ρ(P, t₂), ..., ρ(P, tₙ))
となります。各時点でのPのロバストネスが結果に寄与する度合いは、その値の大きさとwの値によって決まります。値が大きいほど、また、wが大きいほど、その時点の寄与度は大きくなります。
これがスムースロバストネスの計算方法です。すべての時相演算子と命題演算子について、対応するmin/max関数をソフトミン/ソフトマックスで置き換えます。
以下のPlutoノートブックの例で、スムース化パラメータwの効果を視覚的に確認できます。wが0の場合、勾配はほぼ均等に分布しています。wを大きくしていくと、勾配は徐々に通常のロバストネス計算に近づき、最大値を与える点の周辺に集中していきます。
ロバストネス値自体も変化していることに注目してください。w = 0では、ロバストネス値は信号の平均値に近くなります。wが大きくなるにつれて、ロバストネス値は通常の計算（この場合は最大値）に近づきます。
学生: スムース化された勾配のグラフが元の信号のような形になっているように見えますが、これは偶然ですか？
Sydney Katz: 良い観察です。スムース化された勾配が元の信号の形状をある程度反映しているのは偶然ではありません。ソフトマックス関数は各時点の寄与度を、その時点の値に基づいて重み付けするからです。
例えば、「Eventually P」の場合、信号値が高い時点はロバストネスに大きく寄与し、対応する勾配も大きくなります。信号値が低い時点は寄与度が小さく、勾配も小さくなります。そのため、スムース化された勾配のプロファイルは元の信号のプロファイルと似た形状になることがあります。
ただし、完全に同じ形状になるわけではなく、wの値や具体的な信号の形状によって異なります。wが大きい場合、勾配は最大値を与える点の周辺にのみ集中するようになります。
スムースロバストネスの導入により、ロバストネスを目的関数とした最適化問題を効率的に解くことができるようになります。これは、システムの検証や制御戦略の最適化など、多くの応用に役立ちます。例えば、STLロバストネスを目的関数とする強化学習や、モデル予測制御などに活用できます。
次のセクションでは、スムース化パラメータwの効果をさらに詳しく分析し、実際のアプリケーションでの選択方法について説明します。
6.3. スムースパラメータWの効果
Sydney Katz: ここでは、ソフトミン/ソフトマックス関数のスムース化パラメータWがロバストネス計算とその勾配にどのような影響を与えるか、より詳しく分析します。
スムース化パラメータWは、通常のmin/max関数（完全に「クリスプ」な計算）と単純な平均（完全に「スムース」な計算）の間のトレードオフを制御します。実際の例を通してこの効果を見てみましょう。
Plutoノートブックを使って、同じ信号に対して異なるWの値でのスムースロバストネスとその勾配を可視化します。この例では、「Eventually P」演算子を考え、通常のロバストネス計算では最大値を取ります。
まず、W = 0の場合を見てみましょう。この場合、ソフトマックスは単純な平均になります。グラフを見ると、勾配がすべての時点に分散していることがわかります。各時点の寄与度はほぼ均等で、特に大きな値を持つ点でもあまり突出していません。ロバストネス値自体も信号の平均値に近くなります。
Wの値を少し大きくすると（例えばW = 1）、勾配の分布が変化し始めます。信号値が大きい時点の寄与度が増加し、小さい時点の寄与度は減少します。ロバストネス値も平均値から最大値の方向にシフトし始めます。
Wをさらに増加させると（例えばW = 5）、勾配は大きな値を持つ時点周辺に急速に集中し始めます。低い値を持つ時点の寄与度はほとんど無視できるレベルになります。ロバストネス値も通常の計算（最大値）に近づきます。
最終的に、Wを非常に大きな値（例えばW = 10以上）に設定すると、勾配はほぼ完全に最大値を与える時点に集中し、他の時点では事実上ゼロになります。ロバストネス値も通常の計算とほぼ同じになります。
このように、Wの値を調整することで、スムース化の度合いを制御できます。W = 0では完全にスムースな関数（すべての点が均等に寄与）、W → ∞では通常のmin/max関数（一点のみが寄与）となります。
学生: 実際のアプリケーションでは、どのようにWの値を選べばよいのでしょうか？
Sydney Katz: 実用的な観点からは、Wの選択は最適化問題の性質とトレードオフに依存します。以下に、選択の指針をいくつか挙げます：
- 最適化の初期段階では小さなW（例えばW = 1～3）を使用し、勾配情報をより広く分散させることで、広い探索を促進します。
- 最適化が進むにつれてWを大きくし（例えばW = 5～10）、より正確なロバストネス計算に近づけます。これは「アニーリング」のような戦略で、最初は広く探索し、徐々に正確な解に収束させます。
- 問題が局所最適解に陥りやすい場合は、小さめのWを維持して探索性を確保します。
- 最終的な解の精度が重要な場合は、最適化の最終段階で大きなWを使用して、通常のロバストネス計算に近づけます。
- 計算効率とのバランスも考慮します。Wが大きいほど、指数関数の計算で数値的な問題（オーバーフローやアンダーフロー）が発生しやすくなります。
実際には、問題ごとに適切なWの値を実験的に決定することが多いです。複数のWの値で試行し、最適化の収束性と解の質のバランスを取ります。
学生: スムース化によってロバストネス値自体が変化しますが、これは問題にならないのですか？
Sydney Katz: 鋭い質問です。確かに、スムース化によってロバストネス値自体が変化するため、厳密な検証にはスムースロバストネスではなく、通常のロバストネスを使用する必要があります。
実際のワークフローとしては、最適化にはスムースロバストネスを使用し、最終的な解の評価には通常のロバストネスを使用するというアプローチが一般的です。つまり：
- スムースロバストネス（適切なWの値）を目的関数として使用し、効率的に最適化を行う。
- 得られた解に対して、通常のロバストネス計算を適用し、本当の性能を評価する。
これにより、最適化の効率性と評価の正確性の両方を確保できます。
スムースロバストネスの導入は、STLを実際のシステム設計や最適化に応用する上で非常に重要なブレークスルーでした。これにより、形式的な仕様を目的関数として直接使用し、勾配ベースの最適化手法を効率的に適用できるようになりました。
次のセクションでは、これまで学んだSTLとロバストネスの概念を実際のアプリケーション例に適用し、様々なシステムの要件をどのように形式化するかを見ていきます。
7. アプリケーション例
7.1. 連続世界（Continuum World）問題
Sydney Katz: ここまで学んできた信号時相論理（STL）とロバストネスの概念を、実際のアプリケーション例に適用してみましょう。まずは「連続世界（Continuum World）」と呼ばれる問題から始めます。
連続世界問題は、2次元の連続空間内でエージェントが移動するシンプルな環境です。この環境には、緑色で示されたゴール領域と赤色で示された障害物領域があります。エージェントの目標は、障害物を避けながらゴールに到達することです。
この問題に対する要件を形式的に表現するために、STLを使用しましょう。まず、状態に関する述語関数を定義します：
- goal(s): 状態sがゴール領域内にある場合に真
- obstacle(s): 状態sが障害物領域内にある場合に真
次に、これらの述語を使って要件を表現します。「障害物に衝突せずにゴールに到達する」という要件は、STLを使うと次のように表現できます：
φ = (◇goal) ∧ (□¬obstacle)
この式は2つの部分から構成されています：
- ◇goal: いずれゴール領域に到達する（Eventuallyゴール）
- □¬obstacle: 常に障害物領域を避ける（Always not obstacle）
この形式的な仕様は、エージェントの軌道が満たすべき条件を明確に定義しています。任意の軌道に対して、この仕様を満たすかどうかを評価できます。
さらに、ロバストネスの概念を適用することで、軌道がこの仕様をどの程度の余裕をもって満たしているかを定量的に評価できます。ロバストネスは次のように計算されます：
ρ(φ) = min(ρ(◇goal), ρ(□¬obstacle))
ここで：
- ρ(◇goal) = max_t(ρ(goal, t)): すべての時点tにおけるgoal述語のロバストネスの最大値
- ρ(□¬obstacle) = min_t(ρ(¬obstacle, t)): すべての時点tにおける¬obstacle述語のロバストネスの最小値
goal述語のロバストネスは、状態とゴール領域の境界との距離として計算できます。同様に、¬obstacle述語のロバストネスは、状態と障害物領域の境界との距離として計算できます。
例えば、ある軌道について考えてみましょう：
- この軌道はゴールに到達し、最もゴールに近い点はゴール境界から2単位内側にある
- この軌道は常に障害物を避け、最も障害物に近づいた点は障害物境界から1.5単位離れている
この場合、ρ(◇goal) = 2、ρ(□¬obstacle) = 1.5となり、全体のロバストネスはρ(φ) = min(2, 1.5) = 1.5です。
このロバストネス値は、軌道が仕様を満たす「余裕」を表しています。この例では、軌道のどの点も障害物から少なくとも1.5単位離れており、これが全体のロバストネスを決定しています。
連続世界問題でのSTLとロバストネスの応用は、次のような利点があります：
- 形式的な検証: 任意の軌道が要件を満たすかどうかを厳密に検証できます。
- 定量的な評価: ロバストネスにより、異なる軌道の品質を比較できます。
- 最適化目標: ロバストネスを最大化することで、より堅牢な軌道を生成できます。
- 反例の発見: ロバストネスを最小化することで、仕様を満たさない軌道を効率的に見つけられます。
実際のアプリケーションでは、この形式的な仕様とロバストネスを使用して、最適制御問題を解いたり、強化学習のための報酬関数を設計したりすることができます。例えば、STLロバストネスを報酬として使用した強化学習により、仕様を満たす制御方策を学習させることが可能です。
このように、連続世界問題はSTLの基本的な適用例として非常に有用です。次のセクションでは、より複雑な倒立振子システムへの応用を見ていきます。
7.2. 倒立振子システム
Sydney Katz: 次のアプリケーション例として、倒立振子システムについて説明します。倒立振子は制御理論の古典的な問題で、棒の下端を台車に取り付け、棒が垂直上向きの状態（不安定な平衡点）を維持するように制御するものです。
このシステムでは、振子の角度θが主要な状態変数です。θ = 0のとき振子は完全に垂直を向いており、これが目標の平衡点です。通常、制御の目標は振子をこの不安定な平衡点の周りに保つことです。
このシステムに対する要件を信号時相論理（STL）で表現しましょう。「振子のバランスを保つ」という要件は、振子の角度が特定の範囲内に保たれることを意味します。具体的には、角度θの絶対値が一定の閾値（例えばπ/4ラジアン、つまり45度）以下であることを要求します。
この要件を形式化するために、まず次の述語関数を定義します：
balanced(θ) = (|θ| < π/4)
この述語は、振子の角度の絶対値がπ/4未満の場合に真となります。グラフィカルに表現すると、緑色の領域（-π/4 < θ < π/4）内にある状態が「バランスが取れている」状態、赤色の領域（|θ| > π/4）にある状態が「バランスが崩れている」状態です。
次に、この述語をSTL式で表現します。振子のバランスを「常に」保つことが要求されるため、Always演算子（□）を使用します：
φ = □balanced(θ)
この式は「すべての時点で振子はバランスが取れている状態を維持する」ことを意味します。
このSTL式のロバストネスは次のように計算できます：
ρ(φ) = ρ(□balanced(θ)) = min_t(ρ(balanced(θ), t))
各時点tでのbalanced述語のロバストネスρ(balanced(θ), t)は、現在の角度θと許容範囲の境界との距離として計算できます：
ρ(balanced(θ), t) = π/4 - |θ(t)|
例えば：
- θ = 0（完全に垂直）の場合、ロバストネスはπ/4（約0.785ラジアン）
- θ = π/8（22.5度傾いている）の場合、ロバストネスはπ/4 - π/8 = π/8（約0.393ラジアン）
- θ = π/4（45度傾いている）の場合、ロバストネスは0（境界上にある）
- θ = π/3（60度傾いている）の場合、ロバストネスはπ/4 - π/3 = -π/12（約-0.262ラジアン、負なので要件を満たしていない）
全体のロバストネスρ(φ)は、すべての時点でのbalanced述語のロバストネスの最小値です。つまり、振子が最も許容範囲の境界に近づいた（または超えた）ときのロバストネスが、全体のロバストネスを決定します。
倒立振子システムへのSTLの応用には、次のような利点があります：
- 明確な成功基準: バランスを保つという要件が数学的に厳密に定義されます。
- 定量的な性能評価: ロバストネスにより、制御器の性能を定量的に評価できます。
- 安全マージンの評価: ロバストネスが大きいほど、システムは外乱に対してより堅牢であることを意味します。
- 制御器設計の目標: ロバストネスを最大化するような制御器を設計できます。
実際のアプリケーションでは、このSTL式を使用して様々な制御アプローチを評価できます。例えば、PID制御器、LQR制御器、モデル予測制御などの性能を、STLロバストネスという共通の指標で比較できます。
また、より複雑な要件も表現可能です。例えば：
- 「システム起動後5秒以内に振子をバランス状態に持っていき、その後バランスを維持する」 φ = ◇0,5
- 「振子が倒れた場合、10秒以内に再びバランス状態に戻す」 φ = □(¬balanced(θ) → ◇[0,10]balanced(θ))
このように、STLは倒立振子のような古典的な制御問題に対しても、要件を形式的に表現し評価するための強力なツールとなります。次のセクションでは、より複雑な航空機衝突回避問題へのSTLの応用を見ていきます。
7.3. 航空機衝突回避問題
Sydney Katz: 最後のアプリケーション例として、航空機衝突回避問題について説明します。これは実際の安全性クリティカルシステムの例で、私たちが前の講義で少し触れたものです。
航空機衝突回避システムは、航空機同士の衝突を防ぐための重要な安全システムです。この問題では、2機の航空機が接近しているシナリオを考えます。システムは、両機が安全に通過できるように適切な回避マヌーバを生成する必要があります。
この問題の興味深い点は、航空機が水平方向の分離を失う（つまり、真上または真下に位置する）特定の時間帯に、十分な垂直方向の分離を確保する必要があることです。具体的には、水平方向の分離が失われる時間（例えば接近開始から40〜41秒後）に、垂直方向の分離が特定の閾値（例えば50メートル）以上であることを要求します。
この要件を信号時相論理（STL）で表現するために、まず次の述語関数を定義します：
separated(h) = (|h| ≥ 50)
ここで、hは2機の航空機間の相対高度（垂直方向の分離）です。この述語は、相対高度の絶対値が50メートル以上の場合に真となります。
次に、この述語を使ってSTL式を表現します。ここで重要なのは、特定の時間間隔[40, 41]での要件を指定することです。STLの時間間隔の機能を使って：
φ = □[40,41]separated(h)
この式は「時間40秒から41秒の間、常に航空機間の垂直方向の分離が50メートル以上である」ことを意味します。
このSTL式のロバストネスは次のように計算できます：
ρ(φ) = ρ(□[40,41]separated(h)) = min_{t∈[40,41]}(ρ(separated(h), t))
各時点tでのseparated述語のロバストネスρ(separated(h), t)は：
ρ(separated(h), t) = |h(t)| - 50
これは、現在の相対高度の絶対値と最小安全間隔（50メートル）との差を表します。
例えば：
- h = 100メートル（一方が他方より100メートル上）の場合、ロバストネスは|100| - 50 = 50メートル
- h = 75メートルの場合、ロバストネスは|75| - 50 = 25メートル
- h = 50メートルの場合、ロバストネスは|50| - 50 = 0メートル（境界上）
- h = 30メートルの場合、ロバストネスは|30| - 50 = -20メートル（負なので要件を満たしていない）
全体のロバストネスρ(φ)は、時間間隔[40, 41]内のすべての時点でのseparated述語のロバストネスの最小値です。つまり、この時間間隔内で航空機が最も接近した瞬間のロバストネスが、全体のロバストネスを決定します。
実際のJuliaコードでは、このSTL式は次のように実装できます：
# 述語関数の定義
s = (h) -> abs(h) >= 50
# STL式の定義
φ = always(s, 40, 41)航空機衝突回避問題へのSTLの応用には、次のような利点があります：
- 時間的制約の明確な表現: 特定の時間間隔での安全性要件を正確に表現できます。
- 安全マージンの定量的評価: ロバストネスにより、回避マヌーバの安全マージンを定量的に評価できます。
- 認証と検証: 形式的な仕様を使うことで、システムの安全性を厳密に検証し、認証プロセスをサポートできます。
- 最適化目標: ロバストネスを最大化するような回避マヌーバを設計できます。
実際のアプリケーションでは、より複雑な要件も考慮する必要があります。例えば：
- 複数の航空機の存在
- 低高度飛行や気象条件などの運用制約
- 乗客の快適性（急な垂直方向の加速を避ける）
- 燃料効率
これらの追加要件も、STLを使って形式的に表現し、複合的な評価指標を構築することができます。例えば、「安全性を確保しながら、できるだけ燃料消費を最小化する」といった多目的最適化問題として定式化できます。
航空機衝突回避問題は、STLの時間間隔指定機能が特に有用なアプリケーション例です。実際の航空交通管制システムでは、このような形式的手法が安全性クリティカルシステムの検証と設計に不可欠です。
これらの3つのアプリケーション例（連続世界、倒立振子、航空機衝突回避）は、STLとロバストネスの概念がさまざまな領域の問題に適用できることを示しています。形式的な仕様を用いることで、システムの要件を明確に定義し、その性能を定量的に評価することができるのです。
8. 到達可能性（上級トピック）
8.1. 到達可能性プロパティ
Sydney Katz: このセクションでは、上級トピックとして「到達可能性」について簡単に紹介します。このトピックは本講義の範囲を超えており、クイズや課題の対象にはなりませんが、非常に興味深いので簡単に触れておきます。
到達可能性プロパティとは、システムが特定の状態に到達できるかどうかを検証するためのものです。形式的には、「システムの初期状態から出発して、特定の目標状態に到達する軌道が存在するか」という問いに答えるものです。
到達可能性は安全性検証において非常に重要な概念です。例えば、「システムが危険な状態に決して到達しない」という安全性プロパティは、「危険な状態に到達可能性がない」ということと同値です。
到達可能性プロパティを表現するためには、状態空間内の領域を指定します：
- 初期状態の集合 X₀
- 目標状態の集合 X_goal
そして、到達可能性プロパティは「X₀内のある初期状態から出発して、有限時間内にX_goal内の状態に到達する軌道が存在するか」という形で表現されます。
これを論理的に表現すると：
∃x₀ ∈ X₀, ∃T > 0, ∃τ ∈ [0,T] : ξ(τ; x₀) ∈ X_goal
ここで、ξ(τ; x₀)は初期状態x₀から時間τだけ経過した後のシステムの状態を表します。
到達可能性プロパティの検証は、一般的に難しい問題です。特に連続状態空間や非線形ダイナミクスを持つシステムでは計算が複雑になります。しかし、いくつかの手法が開発されています：
- 直接シミュレーション: サンプリングした初期状態からシステムをシミュレーションし、目標状態に到達するか確認します。ただし、この方法では完全な検証はできません。
- 到達可能集合の計算: 初期状態集合から時間の経過とともにシステムが到達できるすべての状態の集合（到達可能集合）を計算し、これが目標集合と交わるか確認します。
- 逆方向解析: 目標状態から逆方向に到達可能集合を計算し、これが初期状態集合と交わるか確認します。
- 抽象化とモデル検査: システムを離散的な遷移システムに抽象化し、モデル検査手法を適用します。
これらの到達可能性解析は、自動運転、航空機の衝突回避、ロボット制御など多くの安全性クリティカルシステムの検証に応用されています。
例えば、自動運転車が特定の交通状況で事故を起こす可能性があるかどうかを検証するために、「車両が障害物と衝突する状態に到達可能かどうか」を解析することができます。
また、到達可能性解析はシステムの性能検証にも使えます。例えば、「ロボットが与えられた初期条件から目標位置に到達できるか」や「倒立振子システムが倒立状態に安定化できるか」などを検証できます。
到達可能性プロパティは、これまで学んだLTLやSTLで表現する時相的プロパティとは異なる性質を持ちますが、非常に重要な検証対象です。次のセクションでは、一般的な時相プロパティを到達可能性プロパティに変換する手法について簡単に説明します。
この分野は安全性クリティカルシステムの検証において活発な研究領域となっています。より詳しく知りたい方は、教科書の関連章を参照してください。
8.2. 他の性質の到達可能性への変換
Sydney Katz: 最後に、一般的な時相プロパティ（LTLやSTLで表現されるもの）を到達可能性プロパティに変換する方法について簡単に説明します。この変換は非常に興味深い概念で、私の教科書では最も美しい図の一つを含んでいます。
時相プロパティと到達可能性プロパティは一見すると非常に異なるように見えますが、驚くべきことに、任意の時相プロパティは到達可能性問題に変換することができます。この変換により、時相プロパティの検証に到達可能性解析の手法を適用できるようになります。
変換の鍵となるのは「オートマトン」という概念です。オートマトンは状態と遷移からなる数学的モデルで、言語や時相パターンを認識するために使用されます。特に、任意のLTLプロパティφは、そのプロパティを満たす軌道のみを受理する「ビューキオートマトン（Büchi automaton）」に変換できます。
変換の主な手順は次のとおりです：
- LTLプロパティφをビューキオートマトンAφに変換します。このオートマトンは、φを満たす軌道のみを受理します。
- 検証対象のシステムのモデルとオートマトンAφの「積（product）」を取ります。これにより、システムの状態とオートマトンの状態の両方を追跡する新しいシステム（積システム）が得られます。
- 積システム内での到達可能性問題を解きます。具体的には、「初期状態から出発して、オートマトンの受理状態を無限回訪れることができるか」を検証します。
これは実質的に、「システムがプロパティφを満たす軌道を生成できるか」という問題に相当します。
例えば、「Eventually到達して、Alwaysそこにとどまる」（◇□P）というLTLプロパティを考えましょう。このプロパティをオートマトンに変換し、システムモデルと積を取ることで、「システムがPを満たす状態に到達し、その後永久にPを満たし続ける軌道を生成できるか」という到達可能性問題に帰着させることができます。
この変換アプローチは、単に理論的に美しいだけでなく、実用的にも非常に重要です。なぜなら、多くのシステム検証ツールやアルゴリズムが到達可能性解析に基づいているからです。LTLやSTLで表現された複雑な要件を到達可能性問題に帰着させることで、これらの既存ツールやアルゴリズムを活用できます。
教科書に載っている図は、このような変換の例を視覚的に表したものです。オートマトンの状態や遷移、そしてシステムとの積がどのように形成されるかを示しています。この図は非常に美しく、時相論理と到達可能性の深い関係を表現しています。
変換アプローチのもう一つの利点は、反例の生成です。プロパティが満たされない場合、到達可能性解析は具体的な反例（プロパティを違反する軌道）を生成できます。これはシステム設計者にとって非常に価値のある情報です。
到達可能性への変換は、さまざまなツールや検証フレームワークで実装されています。例えば、SPIN、NuSMV、TLCなどの有名なモデル検査ツールは、この変換アプローチを用いて時相論理式の検証を行っています。
この上級トピックは本講義の範囲を超えていますが、形式的検証の美しさと強力さを示す重要な例です。興味のある方は、教科書の関連章を参照するか、計算論理や形式的検証に関する上級コースで詳しく学ぶことをお勧めします。
これで本日の講義を終了します。今回は信号時相論理（STL）とロバストネスという強力な概念を学びました。これらの概念は、次の講義からの安全性クリティカルシステムの検証と設計の基盤となるものです。
