论文标题
全局窗口pctl的策略综合
Strategy Synthesis for Global Window PCTL
论文作者
论文摘要
给定马尔可夫决策过程（MDP）$ m $和公式$φ$，策略综合问题询问是否存在策略$σ$ S.T.由此产生的马尔可夫链$ m [σ] $满足$φ$。已知该问题对于概率的时间逻辑PCTL是不可决定的。我们研究一类公式，可以看作是PCTL的片段，其中始终执行了局部有限的地平线属性。此外，我们允许概率不平等的线性表达式。这种逻辑是可决定性的边界，具体取决于所考虑的策略类型。特别是，当策略是确定性的，而一般问题是不可确定的，策略综合是可以决定的。
Given a Markov decision process (MDP) $M$ and a formula $Φ$, the strategy synthesis problem asks if there exists a strategy $σ$ s.t. the resulting Markov chain $M[σ]$ satisfies $Φ$. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.
