利用伴随在属性导向可达性分析中的应用
摘要：基于格论的两种新算法，受到Bradley的性质导向可达性算法的启发。对于寻找安全不变量或反例，第一种算法利用了前向和后向转换关系的过度逼近，并通过上确界的概念在抽象层面上表示。在没有上确界的情况下，可以使用第二种算法，该算法利用了下界集合及其原则。作为一个值得注意的应用例子，我们考虑了马尔科夫决策过程的定量可达性问题。 标题：基于格论的算法及其应用
作者：Mayuko Kori, Flavio Ascari, Filippo Bonchi, Roberto Bruni, Roberta Gori, Ichiro Hasuo
论文ID：2307.02817
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-07