马尔可夫决策过程中多目标查询的证书与见证

certifying verification 算法不仅返回给定属性是否成立，还提供一个可独立检查的证书和相应的见证。证书可用于轻松验证结果的正确性，而见证则提供了有用的诊断信息，例如用于调试目的。因此，证书和见证大大增加了验证过程的可信度和可理解性。在本工作中，我们考虑马尔可夫决策过程（MDP）中多目标可达性-不变性和平均收益查询的证书和见证，即可达性和不变性或平均收益谓词的 conjunction 或 disjunction，无论是普遍量化还是存在量化。通过将已知的线性规划技术转化为 certifying 算法，显示可以获得形式为调度器和子系统的见证。作为概念证明，我们报告了 certifying verification 算法的实现和实验结果。