一句话:证明任意 Borel 目标在未知非马尔可夫随机环境中存在支配序极大的随机尽力而为策略,并给出 LTL 合成复杂度。
本文研究在概率分布未知、仅知转移支持的非马尔可夫随机环境中运行的反应式系统,其目标为 Borel 集合。作者关注支配序下极大的策略:不存在另一策略在所有环境中达到目标的概率都不更低、且在某环境中更高,这类策略被称为 stochastic best-effort。主要理论结果是对任意 Borel 目标都存在此类策略;他们利用历史处目标达成概率的三值抽象给出局部刻画,并用几何测度论中的 Lebesgue 密度定理证明该刻画正确。针对线性时序逻辑(LTL)目标,论文还确定合成此类策略的计算复杂度,并表明其难度不超过在概率已知固定域中合成最优策略。
We study reactive systems with Borel goals operating in a possibly non-Markovian stochastic environment. Moreover, the specific environment is not known, only its support is, i.e., at each step one knows which transitions are possible and which are impossible, but the probability distribution amongst the possible transitions is unknown. We consider system strategies that are maximal in the dominance order, i.e., no other strategy achieves the goal with at least the same probability in all environments, and with a higher probability in some environment. We call such strategies "stochastic best-effort". We prove the very general result that stochastic best-effort strategies exist for any Borel goal. We do this by providing local characterizations in terms of a three-valued abstraction of the probability of achieving the goal at a history. The correctness of the characterization is shown using a version of the Lebesgue Density Theorem from geometric measure theory. On the more practical side, we consider goals given in linear temporal logic. We establish the computational complexity of synthesizing a stochastic best-effort strategy, and show that it is not harder than synthesizing an optimal strategy in a domain with fixed known probabilities.