Partial-Order Reduction for Multi-core LTL Model Checking
Partial-Order Reduction for Multi-core LTL Model Checking
复制标题
用于多核 LTL 模型检查的偏序约简
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Anton Wijs
中科院分区：
文献类型：
--
作者：
A. Laarman;Anton Wijs
部分降阶（POR）是一种众所周知的，成功的模型检查中动态状态空间减少的技术，正如着名的CAV 2014奖所证明的那样。POR与LTL模型检查的结合长期以来被认为会导致所谓的忽略问题，即相关行为被持续忽略，并且从未被选择用于探索。多年来，这个问题已经通过使用各种忽略附带条件来解决，这些附带条件包括状态空间中沿着循环的所有必要操作。
Partial-Order Reduction (POR) is a well-known, successful technique for on-the-fly state space reduction in model checking, as evidenced by the prestigious CAV 2014 award for its pioneers. The combination of POR with LTL model checking is long known to cause the so-called ignoring problem, i.e. relevant behavior is continuously ignored and never selected for exploration. This problem has been solved with increasing sophistication over the years, using various ignoring provisos, which include all necessary actions along cycles in the state space.