Abstract:We present an optimization-based framework for robust permissive synthesis for Interval Markov Decision Processes (IMDPs). While robust IMDP controller synthesis typically yields a single policy and most permissive-synthesis methods assume exact transition models, we synthesize multi-strategies that retain multiple actions while guaranteeing satisfaction of probabilistic reachability or expected-reward specifications under all admissible transition probabilities. We formulate the problem as a mixed-integer linear program (MILP) that maximizes the number of enabled state--action pairs subject to robust Bellman constraints. We develop two encodings: a direct vertex-enumeration formulation and a dualization-based formulation that avoids explicit enumeration of uncertainty-polytope vertices and has size linear in the number of successor transitions. Experiments on four benchmark domains show that both encodings achieve the same optimal permissiveness and scale to IMDPs with hundreds of thousands of states. Compared with standard robust single-policy synthesis, the resulting multi-strategies retain substantially more action choices.
From: Khang V. Huynh [view email]
[v1]
Fri, 3 Oct 2025 19:57:43 UTC (381 KB)
[v2]
Mon, 16 Mar 2026 16:33:00 UTC (380 KB)
[v3]
Thu, 10 Sep 2026 23:14:24 UTC (376 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。