Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic (Extended Version)

技術要約：確率的時相論理によるマルコフ・ジャンプ線形システムの安定性検証

問題提起
マルコフ・ジャンプ線形システム（MJLS）は、基礎となる離散時間マルコフ連鎖によって制御される、複数の線形モード間のランダムな切り替えを伴う動的な現象をモデル化する。MJLSに対する古典的な安定性解析は、システムの状態の第1次および第2次のモーメントの漸近的挙動を特徴付ける、平均安定性（MS）や平均二乗安定性（MSS）といったグローバルな概念に依存している。これらの古典的なアプローチは、通常、すべての初期条件に対して安定性の保証を必要とする。著者らは、このグローバルな視点は、実用においては過度に保守的であったり、誤解を招いたりする可能性があると主張している。具体的には、不安定性は極めて限定的な初期状態のサブセット（例：物理的に到達不可能な構成）においてのみ発生する可能性がある一方で、システムは実用的に関連のあるすべての状態に対して安定である場合がある。逆に、システムはすべての初期状態に対して収束するものの、異なる極限値に収束する場合があり、その際、厳密な安定性の定義（通常、共通の値、典型的には原点への収束を要求する）を満たさないことがある。

本論文は、特定の初期状態の集合に関連した安定性特性の検証に関する文献上の空白に対処するものである。これはモデル検査問題として定式化されており、目標は、与えられた状態空間の特定のサブセットに対して、モーメントの収束に関する特定の時相特性が保持されるかどうかを判定することである。

手法
著者らは、安定性解析を確率的計算木論理（PCTL）の枠組みに埋め込むことでこの問題に取り組んでいる。

1. MJLSにおけるPCTLの定式化：
   本論文では、まずMJLSに対する標準的なPCTLを定式化する。状態空間は、$S_J = \mathbb{R}^n \times \{1, \dots, m\}$として定義され、連続的な状態変数と離散的なマルコフ・モードを組み合わせたものである。原子命題は、連続状態に関する凸多面体および離散状態に関する特定のモードの上に定義される。充足関係は無限パスに対して定義され、確率は基礎となるマルコフ連鎖から導出されるシリンダー集合（cylinder sets）に基づいて計算される。

2. 一般的なPCTLモデル検査の限界：
   著者らは、MJLSにおける完全なPCTL論理（無制限の「until」演算子を含む）の決定可能性を分析する。彼らは、MJLSを一般マルコフ過程（GMP）に埋め込めることを確立している。線形動的システム（LDS）がMJLSの決定論的な特殊ケースであることを利用して、MJLSにおけるPCTLの到達可能性問題が、Skolem問題に関連する決定不能性の結果を継承することを証明する。具体的には、LDSにおいて4次元以上の集合に対する到達可能性を判定することは未解決問題であり、これはMJLSにおけるPCTLの一般的なモデル検査問題（ステップ限定の断片である$PCTL^-$を超えたもの）もまた未解決であり、決定不能である可能性が高いことを示唆している。

3. 安定性演算子による拡張：
   グローバルな安定性の定義による制限と、一般的な到達可能性解析の決定不能性を克服するために、著者らは、特定の初期状態に関連するモーメントベースの安定性特性を捉える新しい原子命題を用いてPCTLを拡張する。

• 演算子： 彼らは、ステップ限定型（$E^k_\Pi, V^k_\Xi$）およびステップ無制限型（$E_\Pi, V_\Xi$）の演算子を導入する。
  • $E_\Pi$ および $V_\Xi$ は、第1次モーメント（期待値）および第2次モーメント（中心化されていない分散）のチェザロ極限（Cesàro limit、時間平均極限）が、指定された凸多面体（$\Pi$ または $\Xi$）内に存在するかどうかを判定する。
  • これらの演算子は、点的な極限ではなくチェザロ極限を利用することで、点的に収束しない可能性があるが平均が定義されている振動的な挙動を扱う。
• 代数的アプローチ： これらの新しい演算子の検証は、一般的な到達可能性解析ではなく、線形代数的な手法に依存している。
  • 条件付きモーメントの進化は、第1次モーメントのための線形作用素 $B_J$ および第2次モーメントのための $T_J$ によって支配される。
  • 無制限演算子の充足集合は、これらの作用素のスペクトル特性（固有値および固有ベクトル／ジョルダン細胞）を分析することによって計算される。
  • 対角化可能な作用素の場合、極限は単位円上の固有値に対応する固有空間への初期状態の射影によって決定される。
  • 非対角化可能な作用素の場合、著者らはジョルダン標準形を用いて、項が発散するかキャンセルされるかを処理しながら、記号的に極限を計算する。

主な貢献と結果

• 論理的枠組み： 本論文は、MJLSにおけるPCTLの形式的な意味論を提供し、特定の初期状態集合に関連した安定性を指定するための新しい演算子を拡張する。
• アルゴリズムによる検証：
  • ステップ限定の断片（$PCTL^-$）および新しい安定性演算子（$E_\Pi, V_\Xi$ など）に対する決定手順が提供される。
  • 安定性演算子のアルゴリズムは、検証問題を線形方程式系の求解および凸多面体への所属判定へと帰着させる。これにより、結果となる充足集合が（凸集合またはその和集合として）表現可能であり、固有値が計算可能である限り、計算量的に扱いやすいことが保証される。
  • 著者らは、一般的なPCTLモデル検査問題がSkolem問題との関連から未解決である一方で、モーメントの安定性を扱う特定の断片は、線形代数を通じて決定可能であることを示している。
• 振動の処理： チェザロ極限を使用することにより、提案された演算子は、古典的な定義では失敗する可能性がある（振動する場合がある）場合でも、明確に定義されたままとなる収束の概念を捉えることができる。
• ケーススタディ： 本論文には、例えば $P_{\ge 0.3}(\Lambda \mathcal{U}_{\le 5} E_\Pi)$ のような数式に対する充足集合を可視化する計算例（2つの状態変数を持つ3モードのMJLS）が含まれており、複雑な安定性と到達可能性の要件を満たす状態空間の領域を特定できる能力を示している。

意義と主張
著者らは、自らの研究が、以前は表現も決定も不可能であった「洗練された」MJLSの安定性の視点を可能にすると主張している。この枠組みにより、解析者は以下のことが可能になる：

1. グローバルな解析の保守性を避け、特定の、実用的に関連のある初期条件のサブセットに対して安定性特性を特定する。
2. 安定性特性を、古典的な到達可能性や分岐時間目的関数と単一の論理式内で組み合わせる。
3. 確率的モデル検査を、状態依存の安定性解析のための自然なフレームワークとして利用する。

本論文は、決定可能性の結果の範囲に関して控えめな姿勢を保っている。著者らは、MJLSにおける一般的なステップ無制限のPCTL特性のモデル検査問題が依然として未解決であり、数学における長年の未解決問題（Skolem問題）と密接に関連していることを明示的に認めている。さらに、実装における実用的な制限についても述べており、4次元を超える行列の固有値を厳密に計算することは一般に不可能であるため（アーベル・ルッフィの定理による）、より大規模なシステムにおいては、解析は記号的な厳密解ではなく数値的な近似に依存することになる。結論として、安定性演算子で強化された特定の論理（一般的な無制限のuntilを除く）は、線形代数的な手法を通じて決定可能であるが、逆の入れ子構造（PCTL論理を安定性演算子の内部に埋め込むこと）は現在の枠組みではサポートされておらず、そのモデル検査問題もまた未解決であると述べている。