提出首个高效求解带约束的鲁棒策略合成方法。
Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
- 用一阶逻辑表达任意结构约束，结合约束求解与概率模型检验。
- 在数百个基准上验证可行性，性能优于现有方法。
- 适合需要高可靠性与可实现性约束的控制系统设计。
已知有限马尔可夫决策过程（MDPs）下计算最优奖励策略是规划、控制器合成和验证等应用的基础。然而，我们常需要策略具备鲁棒性（对MDP扰动表现良好）及满足特定结构约束（如表示形式或实现成本）。这类鲁棒且受约束的策略合成在计算上更具挑战性。本文首次提出一种灵活高效的框架，用于计算满足任意结构约束的鲁棒策略。通过在一组MDPs上以一阶逻辑表达约束，并融合约束求解器处理组合复杂性，以及概率模型检验算法分析MDPs，实现高效求解。在数百个基准上的实验表明该方法在各类问题片段中均具可行性，且性能媲美最先进方法。
原文摘要 · Abstract (English)
The ability to compute reward-optimal policies for given and known finite Markov decision processes (MDPs) underpins a variety of applications across planning, controller synthesis, and verification. However, we often want policies (1) to be robust, i.e., they perform well on perturbations of the MDP and (2) to satisfy additional structural constraints regarding, e.g., their representation or implementation cost. Computing such robust and constrained policies is indeed computationally more challenging. This paper contributes the first approach to effectively compute robust policies subject to arbitrary structural constraints using a flexible and efficient framework. We achieve flexibility by allowing to express our constraints in a first-order theory over a set of MDPs, while the root for our efficiency lies in the tight integration of satisfiability solvers to handle the combinatorial nature of the problem and probabilistic model checking algorithms to handle the analysis of MDPs. Experiments on a few hundred benchmarks demonstrate the feasibility for constrained and robust policy synthesis and the competitiveness with state-of-the-art methods for various fragments of the problem.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。