区间马尔可夫决策过程的自动机理论验证
Automata-Theoretic Verification of Interval Markov Decision Processes
- University of Liverpool（利物浦大学）
- MPI-SWS（德国马克斯·普朗克软件系统研究所）
- University of Birmingham（伯明翰大学）
- University of Colorado Boulder（科罗拉多大学博尔德分校）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文研究区间马尔可夫决策过程的自动机理论验证，针对ω-正则规范，区分稳定与不稳定区间结构，分别使用适用于MDP和适用于博弈的自动机，并开发算法及概率保证，连接数据驱动建模与形式化验证。
AI中文摘要：
区间马尔可夫决策过程（IMDPs）为建模具有不确定转移概率的随机系统提供了一种自然框架，其中转移概率由概率区间表示并以对抗方式解析。这种不确定性自然产生，例如，当转移模型从有限数据中学习或通过基于模型的强化学习获得时。在本文中，我们通过考虑更广泛的ω-正则目标类别，研究IMDPs针对丰富时间规范（包括所有LTL规范）的自动机理论验证。我们表明，经典的自动机理论验证技术可以扩展到IMDPs，但根据转移区间的结构存在显著区别。对于稳定IMDPs，其中上界为零或下界严格为正，验证简化为普通MDP分析，可以使用该设置中使用的标准自动机（适用于MDP的自动机）进行。对于不稳定IMDPs，其中区间可能包含零而上界严格为正，验证变得类似博弈，需要能够即时解析非确定性的自动机（适用于博弈的自动机）。基于这些见解，我们开发了在IMDPs上验证ω-正则规范的算法，并在区间模型从采样数据中学习时推导出概率保证。所得到的框架能够在概率模型不确定性下对随机系统进行原则性验证，将基于自动机的验证与数据驱动的随机建模联系起来。
英文摘要：
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 ω-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 ω-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.
