意味的潜在表現を用いた仕様変更可能なビジョンベース実行時監視
本論文は、部分観測下での視覚観測に基づく過去時間信号時相論理(ptSTL)の認証済み実行時監視を研究する。監視器は画像から安全関連量を推定し、有限標本保証を提供するとともに、再利用可能性（一度の学習と較正で対象断片内の任意の式を認証）を要求する。有限時相原子辞書から導出される断片に対し、意味的基底（原子ロバストネススコアのベクトル）が単調1-リプシッツ再利用可能インタフェースクラス内の最小予測ターゲットであることを証明。また、現在の述語値のみを予測しオンラインで時相履歴を再構成するローリング予測監視器も導入。歩行者交差点ベンチマークでは、ローリングが短い地平線でより厳しい認証境界を提供し、意味的基底監視器は長い地平線で最大4倍厳しい。実世界のWaymo運転データで検証し、両監視器が経験的に共形被覆保証を満たすことを確認。
自動運転などの安全重要システムでは、システムの動作が安全仕様を満たすことをリアルタイムで監視することが不可欠である。しかし、センサーノイズや部分観測性のため、視覚入力から安全特性を監視することは困難を伴う。本論文では、変化する安全仕様に対応可能で、統計的保証を提供するビジョンベースの実行時監視フレームワークを提案する。
核となるアイデアは、意味的潜在表現——すなわち、事前定義された時相原子のロバストネススコアのベクトル——を監視インタフェースとして利用することである。著者らは、有限の時相原子辞書から生成される任意の式断片に対して、この表現が最小かつ最適な予測ターゲットであることを証明した。すなわち、一度の共形較正で断片内のすべての式を認証でき、式ごとの再学習が不要となる。この再利用可能性により、導入コストが大幅に削減される。
意味的基底監視器に加えて、ローリング予測監視器も導入された。こちらは現在時刻の述語値のみを予測し、履歴をオンラインで再構成するため学習が容易である。しかし、実験の結果、予測地平線が長くなると保守性が増すことが示された。歩行者交差点のシミュレーションベンチマークでは、短い地平線（例：5ステップ）ではローリング監視器の方が厳しい認証境界を提供したが、長い地平線（例：20ステップ）では意味的基底監視器が最大4倍厳しい境界を示した。
実際のWaymo運転データセットを用いた検証では、両監視器が共形被覆保証を経験的に満たし、実用可能性が確認された。本研究は、視覚ベースの安全重要システムに対して、効率的でスケーラブルな検証手法を提供するものである。特に、仕様が頻繁に変更される自動運転シナリオへの応用が期待される。今後の課題として、より複雑な時相論理や動的環境への拡張が挙げられている。