具有公平性目标的图与马尔可夫决策过程的符号算法

给定一个模型与一个规约，基本的模型检测问题要求算法验证模型是否满足该规约。我们考虑图与马尔可夫决策过程（MDPs），它们是反应式系统的基本模型。在反应式系统验证中出现的最基本规约之一是强公平性（又称Streett）目标。给定不同类型的请求与相应授权，该目标要求对每一类型，若请求事件无限频繁发生，则相应的授权事件也必须无限频繁发生。所有$\omega$-正则目标均可表示为Streett目标，因此它们在验证中是典范性的。为处理状态空间爆炸，需要符号算法在系统简洁的隐式表示上操作，而非显式访问系统。虽然针对具有Streett目标的图与MDP的显式算法已被广泛研究，但基本符号算法一直未有改进。基本符号算法所需的最坏情况符号步数如下：图是二次的，MDP是三次的。在本工作中，我们提出首个针对具有Streett目标的图的亚二次符号算法，且我们的算法即便对MDP也是亚二次的。基于我们的算法见解，我们给出了新符号方法的实现，并表明在若干学术基准示例上它改进了现有方法。