Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
Linus Heck, Filip Macák, Milan Češka, Sebastian Junges
为给定和已知的有限马尔可夫决策过程(MDP)计算奖励最优策略的能力支持了跨规划、控制器合成和验证的各种应用。 然而,我们通常希望政策(1)是稳健的,即,它们对MDP的扰动表现良好,(2)满足有关其表示或实施成本的额外结构性限制。 计算这种强大和受限的策略在计算上确实更具挑战性。 本文提供了第一个使用灵活和高效的框架有效计算受任意结构约束的稳健策略的方法。 我们通过允许在一组MDP上一阶理论中表达我们的限制来实现灵活性,而我们效率的根源在于可满足性求解器的紧密集成,以处理问题的组合性质和概率模型检查算法来处理MDP的分析。 对几百个基准的实验证明了受限和稳健的政策综合的可行性,以及针对问题的各种片段采用最先进的方法的竞争力。
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 chall...
