参数化马尔可夫决策过程的超鞅证书

中文摘要 AI 辅助

我们考虑具有一般可测状态和动作空间的参数化马尔可夫决策过程（MDPs）中的形式验证与综合问题。我们方法的核心是一种参数展平变换，它使我们能够将参数化MDPs转换为语义等价的非参数化MDPs。基于这一变换，我们引入了参数化超鞅证书的新概念，它将用于非参数化MDPs的传统超鞅证书推广到参数化设置。我们使用参数化超鞅证书来设计用于多项式算术参数化MDPs的验证和近似综合算法。这导致了针对具有一般状态和动作空间的参数化MDPs的首个验证和综合算法。我们实现了我们的算法，并在几个连续参数化随机游走基准上进行了实验评估。

英文摘要

We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.

发表机构

• IMDEA Software Institute（IMDEA软件研究所）
• Nanyang Technological University（南洋理工大学）

机构由 AI 辅助整理，请以论文原文为准。