PrIC3：面向 MDP 的性质导向可达性分析
计算机科学中的逻辑
2020-05-19 v2
摘要
IC3 在符号模型检验中是一个重大飞跃。本文提出 PrIC3（读作 pricy-three），作为 IC3 向 MDP 符号模型检验的保守扩展。我们的主要焦点是发展 PrIC3 背后的理论。同时，我们给出了 PrIC3 的首次实现，包含 IC3 的关键要素如泛化、重推与传播。
引用
@article{arxiv.2004.14835,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
journal= {arXiv preprint arXiv:2004.14835},
year = {2020}
}