面向随机奇偶博弈的可执行策略证书

中文摘要 AI 辅助

我们提出了一种新方法，用于在具有定量目标的随机奇偶博弈（2.5人博弈）中综合大量获胜策略。我们不计算单个完全指定的获胜策略，而是引入可执行策略证书（ASCerts），作为系统玩家一大类获胜策略的局部且宽松的表示。为此，我们将已知的随机不变量证书扩展到博弈的设定中。我们的证书证明，综合出的策略以至少λ∈[0,1]的概率保持在博弈的安全区域内。因此，这些证书增强了综合策略的可信度。我们方法的关键在于将证书重新解释并利用为（可能无限多个）策略的简洁、局部且宽松的表示。通过将我们的随机不变量证书与几乎必然获胜的策略模板仔细结合，我们获得了随机奇偶博弈中定量获胜策略的一种新颖的局部表示。这实现了高效的综合、自适应和运行时策略提取，使ASCerts非常适合不确定和对抗性环境中的逻辑控制。我们提供了一个概念验证实现，并在一个案例研究中展示了ASCerts在运行时自适应中的应用潜力。

英文摘要

We propose a new approach for synthesizing large sets of winning strategies in stochastic parity games (2.5-player games) with quantitative objectives. Instead of computing a single, fully specified winning strategy, we introduce Actionable Strategy Certificates (ASCerts) as a local and permissive representation of a large class of system player winning strategies. To this end, we extend known certificates for stochastic invariants to the setting of games. Our certificates prove that synthesized strategies remain within a safe region of the game with probability at least $λ\in [0,1]$. As such, the certificates enhance the trustworthiness of synthesized strategies. The crux of our approach is to reinterpret and leverage the certificates as concise, local, and permissive representation of (possibly infinitely many) strategies. By carefully combining our certificates for stochastic invariants with strategy templates for almost-sure winning, we obtain a novel local representation of quantitatively winning strategies in stochastic parity games. This enables efficient synthesis, adaptation, and runtime strategy extraction, making ASCerts well suited for logical control in uncertain and adversarial environments. We provide a proof-of-concept implementation and demonstrate the potential of applying ASCerts in runtime adaptation in a case study.

发表机构

• Technische Universität Dresden（德累斯顿工业大学）
• ENS Paris-Saclay（巴黎萨克雷高等师范学院）
• Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）

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