概率可达性约束的 Farkas 证书与极小见证
计算机科学中的逻辑
2020-02-06 v2 最优化与控制
摘要
本文针对马尔可夫决策过程（MDP）中极小与极大可达概率的下界和上界引入了 Farkas 证书，其由 Farkas 引理的 MDP 变体推导而来。证明了所有此类证书的集合构成一个多面体，其点与模型和性质的见证子系统相对应。利用该对应关系，我们可以将寻找极小见证的问题转化为寻找具有最多零值顶点的问题。尽管一般而言计算此类顶点在计算上是困难的，我们从我们的表述中推导出了新的启发式方法，其与最先进技术相比表现出有竞争力的性能。作为无法期望渐近更优算法的论据，我们证明了即便对于无环马尔可夫链，寻找极小见证的判定版本也是 NP-complete 的。
引用
@article{arxiv.1910.10636,
title = {Farkas certificates and minimal witnesses for probabilistic reachability constraints},
author = {Florian Funke and Simon Jantsch and Christel Baier},
journal= {arXiv preprint arXiv:1910.10636},
year = {2020}
}
备注
41 pages, 7 figures (including appendix), to appear in TACAS 2020