技術概要：mstlo – シグナル時相論理の効率的なオンライン監視

1. 問題定義

サイバーフィジカルシステム（CPS）の導入が増加する中、運用中の正しさを保証するための堅牢な手法が必要とされています。ランタイム検証（RV）は、形式仕様に基づいた性質に対してシステムの動作をリアルタイムで監視することで、この課題に対処します。シグナル時相論理（STL）は、実数値連続時間シグナル上のタイミング制約や安全性要件を指定するための標準言語です。

しかし、既存のオンライン監視ツールは以下の重大な課題に直面しています：

• パフォーマンス制約: 監視器は遅延を最小化し、検証プロセスがシステムに追いつかないようにするために、極めて効率的である必要があります。各時間ステップで式を最初から再評価する素朴なアプローチは、式の複雑さやシグナルの長さに対してスケーラビリティが低いです。
• 意味論的制限: ほとんどのツールは、ユーザーに単一の評価戦略（例えば、遅延型定量的意味論のみ）を制限しており、判定の表現力、遅延、パフォーマンス間のトレードオフを可能にする能力が制限されています。
• 使いやすさと統合: 複数の STL 意味論に対する統一インターフェースを提供し、Rust や Python などのモダンなエコシステムへの容易な統合を可能にする埋め込みドメイン固有言語（DSL）による静的構文チェックを提供するツールの不足があります。

2. 手法

著者らは、STL の効率的なオンライン監視のために設計された、Rust で実装され Python バインディングを備えた高性能ライブラリ mstlo（mistletoe）を提示します。

中核的なアルゴリズム的アプローチ

• インクリメンタル監視: 各時間ステップで式全体を再評価するのではなく、mstlo はボトムアップの動的計画法アプローチを採用します。仕様は抽象構文木（AST）として表現され、各演算子は子演算子からの中間結果のキャッシュを維持します。
• 最適化された時相演算子: 移動平均最小値および最大値計算として機能する「常に」（$\square$）および「いつか」（$\diamond$）演算子に対して、実装は Lemire のアルゴリズム のバージョンを組み込んでいます。この最適化により、非 RoSI 意味論におけるメモリフットプリントと計算時間の大幅な削減が実現されます。
• 統合された意味論インターフェース: このライブラリは、ゼロコストの静的ディスパッチのための Rust トレイトを使用して単一の汎用監視コアを通じて、4 つの異なる意味論定義をサポートします：
  1. 遅延型定性的: 時間的深さまでの完全なシグナル解決を必要とする標準的なブール充足。
  2. 遅延型定量的: 実数値スコアを計算する標準的なロバストネス意味論。
  3. 即時型定性的: 単調性を利用して、部分的なトレース上で早期のブール判定（ショートサーキット）を出力します（例：$\square$ 性質の最初の違反発生時に即座に false を返す）。
  4. ロバスト充足区間（RoSI）: 部分的なトレースに対するすべての可能な将来のロバストネス値を包含する区間 $[\rho_{min}, \rho_{max}]$ を計算し、完全な地平線が観測されると単一の値に収束します。

実装機能

• 埋め込み DSL: mstlo は、Rust 用コンパイル時手続きマクロ（stl!）およびランタイムパーサーとして利用可能な DSL を提供します。これにより、静的構文チェック、記号変数（$ プレフィックス付き）を介したパラメータ化された式、および一般的なパターンに対する構文糖衣がサポートされます。
• ビルダーパターン: 監視器は、式、意味論、アルゴリズムモード（Naive 対 インクリメンタル）、変数コンテキスト、および同期戦略（例：非同期シグナル補間の処理）を構成するためにビルダーパターンを使用してインスタンス化されます。
• クロス言語サポート: コアエンジンは Rust で記述されており、Python バインディング（mstlo-python）がエンジンを取り巻くことで、Python エコシステムおよび対話型ワークフロー（例：Jupyter Notebook）での採用を容易にします。

3. 主要な貢献

1. 統合フレームワーク: 単一のアーキテクチャ内で複数の STL 意味論（遅延型定性的/定量的、即時型定性的、および RoSI）をサポートする、最初の専用オンライン監視ツール。
2. 高性能アルゴリズム: 演算子ごとのキャッシングと Lemire のスライディングウィンドウ最適化を利用するインクリメンタル監視アルゴリズムにより、大きな時間的深さを持つ式に対するスケーラビリティを達成。
3. 開発者体験: Rust における静的構文チェックを備えた埋め込み DSL とランタイムパーサー、およびより広範なアクセシビリティのための Python バインディング。
4. 再現可能なベンチマーク: 異なる意味論、式構造、入力シグナルにわたるパフォーマンスを評価する包括的なベンチマークスイート。

4. 実験結果

ベンチマークは、1 Hz でサンプリングされた 20,000 サンプルにわたるチャープ波シグナルを使用して、Apple MacBook M4 Pro 上で実施されました。時間的深さやネストが異なる 3 つの式（$\phi_1, \phi_2, \phi_3$）が評価されました。

• スケーラビリティ:
  • 遅延型および即時型定性的意味論において、$\square$ 演算子の実行時間は Lemire の最適化により、時間的上限 $b$ に関係なく一定でした。
  • $U$（Until）演算子の実行時間は、同じ最適化の恩恵を受けないため、$b$ に比例して線形にスケーリングしました。
  • RoSI 意味論は、区間を維持する高い計算コストを反映し、$\square$ に対して線形スケーリング、$U$ に対して二次スケーリングを示しました。
• パフォーマンス比較:
  • mstlo (Rust) は、C++ バックエンドを持つ主要な Python ベースのツールである RTAMT と比較して、著しく低い実行時間を示しました。
  • 単純な式（$\phi_1$）の場合、mstlo-python は RTAMT よりも 10〜13 倍高速でした。
  • 複雑なネストされた式（$\phi_3$）の場合、mstlo-python は約 39 倍高速でした。
  • このパフォーマンスの差は、mstlo のアルゴリズム的最適化（キャッシング）と浅い Python バインディング、および RTAMT の Python へのより重い依存関係に起因します。
• オーバーヘッド: Python バインディングは、ネイティブ Rust 実装と比較してわずか 1〜1.7 倍の小さなオーバーヘッドしか導入しませんでした。

5. 意義と主張

本論文は、mstlo が以下の点で STL 監視の最先端を進展させると主張しています：

• ギャップの埋め合わせ: 複数の評価意味論をサポートする、Rust と Python の両方向けの使いやすい専用オンラインフレームワークを提供し、オンライン STL 監視に最適化されたツールの不足に対処します。
• アーキテクチャの進展: インクリメンタルアルゴリズムと Lemire の最適化の組み合わせなど、高性能オンライン監視に特化したアーキテクチャ的改善を導入します。
• 使いやすさ: 静的構文チェックとパラメータ化を提供する埋め込み DSL によって使いやすさを向上させ、複雑な時相性質の指定における参入障壁を低下させます。
• 実用的応用: このツールはすでに教育現場（「エンジニアリング・デジタルツイン」コース）で、実践的な環境におけるランタイム検証の教授に成功裏に利用されています。

著者らは、将来の作業として、メモリおよび計算制約が追加の要件を課す組み込みシステムプラットフォームへの実装の拡張を含むと指摘しています。