paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Life is Random, Time is Not: Markov Decision Processes with Window Objectives

生命是随机的,时间不是:具有窗口目标的马尔可夫决策过程
LMCS vol.Volume 16, Issue 42020匹配度 3/10 · 论文属于形式化方法与程序合成中的随机博弈/MDP窗口目标研究,与用户关注的静态分析、LLM/Agent 交叉、浮点程序分析、贝叶斯程序分析均无直接关联;仅在形式化验证/合成这一大方向上有边缘交集。引用 15 inbox
Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, Mickael Randour
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:将窗口机制扩展到马尔可夫决策过程,解决窗口目标的阈值概率问题并给出通用策略综合方法。

经典博弈目标通常只关注无限执行的极限行为,而窗口机制通过引入可配置时间框架强化目标,要求系统在整个无限运行中反复在时限内满足可接受行为。本文将该框架从双人零和博弈推广到随机环境,研究马尔可夫决策过程中的窗口目标。核心问题是阈值概率问题:给定目标与概率阈值,综合策略使满足目标的运行概率不低于阈值。作者针对时间框架作为参数、或询问是否存在这样的时间框架两类变体进行求解,提出一种面向窗口目标的通用方法,并将其实例化到 mean-payoff 与 parity 目标,这些目标已在博弈中被研究。该工作为在随机模型中广泛使用窗口机制铺平了道路。

问题
传统博弈目标只在极限意义上要求正确性,难以推理系统运行中的时间界限;本文要在随机环境 MDP 中处理窗口目标,并解决其阈值概率策略综合问题。
方法
作者提出一种适用于基于窗口目标的通用方法,统一处理时间框架给定为参数或要求存在时间框架的变体,并将其实例化到 mean-payoff 和 parity 目标。
评估
在马尔可夫决策过程中对常用窗口目标变体求解阈值概率问题,覆盖参数化时间框架与存在性时间框架,并实例化到经典 mean-payoff 和 parity 目标。
原文摘要(Abstract)

The window mechanism was introduced by Chatterjee et al. to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games because it enables reasoning about such time bounds in system specifications, but also thanks to the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering Markov decision processes. A fundamental problem in this context is the threshold probability problem: given an objective it aims to synthesize strategies that guarantee satisfying runs with a given probability. We solve it for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-1901-03571,
  title = {Life is Random, Time is Not: Markov Decision Processes with Window Objectives},
  author = {Thomas Brihaye and Florent Delgrange and Youssouf Oualhadj and Mickael Randour},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 4},
  year = {2020},
  doi = {10.23638/lmcs-16(4:13)2020}
}