遷移確率が不確かなシステムをオートマトンで検証する
Automata-Theoretic Verification of Interval Markov Decision Processes
この論文をやさしく読む
ひとことで言うと
確率が正確には分からないシステムでも、時間を通じて守るべき性質を検証する理論です。特に、ある遷移が起こる確率としてゼロを許すかどうかが、必要な検証方法を分けます。
何に役立つ？
有限の観測データから学んだ確率モデルを使う際に、不確かさを含めて仕様の成立を評価するための基礎になります。要旨では、そのような学習モデルに対する確率的保証も導いています。
この研究の面白いところ
確率区間を付け加えるだけに見える変更が、通常のMDP解析で済む場合と、相手の選択に対応するゲームとして扱う場合を生みます。その分岐を区間のゼロの扱いとオートマトンの性質で整理しています。
どこまで分かった？
要旨が述べるのは検証アルゴリズムと保証に関する理論的成果です。実システムでの評価値や計算時間は示されておらず、安定な場合の方法をゼロを含む区間へそのまま適用できるとはしていません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
区間マルコフ決定過程（IMDP）は、不確かな遷移確率を確率区間として表し、その区間内の値が敵対的に選ばれる確率システムをモデル化するための自然な枠組みである。このような不確かさは、例えば有限のデータから遷移モデルを学習した場合や、モデルベース強化学習によってモデルを得た場合に自然に生じる。本論文では、すべての線形時相論理（LTL）の仕様を含む豊かな時間的仕様に対するIMDPのオートマトン理論に基づく検証を、より広いω正則目的のクラスを考えることで研究する。 古典的なオートマトン理論による検証技法はIMDPにも拡張できるが、遷移区間の構造によって明確な違いが生じることを示す。上限がゼロであるか、下限が厳密に正である安定なIMDPでは、検証は通常のMDPの解析に帰着し、その設定で用いられる標準的なオートマトン、すなわちgood-for-MDPオートマトンを使用できる。一方、上限が厳密に正でありながら区間がゼロを含み得る不安定なIMDPでは、検証はゲーム的な性質を持ち、非決定性を逐次的に解消できるgood-for-gamesオートマトンが必要になる。 これらの知見に基づき、IMDP上のω正則仕様を検証するアルゴリズムを開発し、標本データから区間モデルを学習する場合の確率的保証を導く。得られた枠組みは、確率モデルの不確かさがある確率システムを原理に基づいて検証できるようにし、オートマトンに基づく検証とデータ駆動の確率モデリングを結び付ける。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-18（UTC）
- 最新改訂
- 2026-09-18 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-18 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Interval Markov decision processes (IMDPs) provide a natural framework for modeling stochastic systems with uncertain transition probabilities, represented by probability intervals and resolved adversarially. Such uncertainty arises naturally, for example, when the transition model is learned from finite data or obtained through model-based reinforcement learning. In this paper, we study the automata-theoretic verification of IMDPs against rich temporal specifications, including all LTL specifications, by considering the broader class of {\omega}-regular objectives. We show that classical automata-theoretic verification techniques extend to IMDPs, but with a sharp distinction determined by the structure of the transition intervals. For stable IMDPs, where either the upper bound is zero or the lower bound is strictly positive, verification reduces to ordinary MDP analysis and can be carried out using the standard automata used in that setting (good-for-MDP automata). For unstable IMDPs, where intervals may include zero while the upper bound is strictly positive, verification becomes game-like and requires automata whose nondeterminism can be resolved on the fly (good-for-games automata). Building on these insights, we develop algorithms for verifying {\omega}-regular specifications over IMDPs and derive probabilistic guarantees when the interval model is learned from sampled data. The resulting framework enables principled verification of stochastic systems under probabilistic model uncertainty, connecting automata-based verification with data-driven stochastic modeling.
著者のコメント
14 pages including appendices, accepted to CDC 2026
arXiv ID: 2609.21966 ／ 要約の誤りについて