一句话：引入 Kripke 结构与 MDP 中路径性质的长期频率/概率，并刻画其最优值与阈值判定问题的复杂度。
论文研究路径性质在长期运行中的满足程度。作者为 Kripke 结构中的路径定义长期频率，并推广为 Markov 决策过程中调度器的长期概率；随后研究在所有路径或调度器上优化这些度量值的问题，以及给定阈值后的判定问题。对于（重复）可达性及其他简单性质，最优长期概率和最优无记忆调度器可在多项式时间内计算。对于约束可达性，无记忆调度器不再充分，即便在非概率场景亦然；但概率场景下最优长期概率可在伪多项式时间计算，Kripke 结构下为多项式时间。对于由 NFA 表达的 co-safety 性质，给出计算最优长期频率的指数时间算法，并证明阈值问题是 PSPACE 完全的。
The paper introduces the concepts of long-run frequency of path properties for paths in Kripke structures, and their generalization to long-run probabilities for schedulers in Markov decision processes. We then study the natural optimization problem of computing the optimal values of these measures, when ranging over all paths or all schedulers, and the corresponding decision problem when given a threshold. The main results are as follows. For (repeated) reachability and other simple properties, optimal long-run probabilities and corresponding optimal memoryless schedulers are computable in polynomial time. When it comes to constrained reachability properties, memoryless schedulers are no longer sufficient, even in the non-probabilistic setting. Nevertheless, optimal long-run probabilities for constrained reachability are computable in pseudo-polynomial time in the probabilistic setting and in polynomial time for Kripke structures. Finally for co-safety properties expressed by NFA, we give an exponential-time algorithm to compute the optimal long-run frequency, and prove the PSPACE-completeness of the threshold problem.
DOI 原文 ·
@inproceedings{paperbot4982,
title = {Long-run Satisfaction of Path Properties},
author = {Christel Baier and Nathalie Bertrand and Jakob Piribauer and Ocan Sankur},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785672}
}