Parallel Explicit Model Checking for Generalized Büchi Automata
Parallel Explicit Model Checking for Generalized Büchi Automata
复制标题
DOI：
10.1007/978-3-662-46681-0_56
复制
发表时间：
2015-04
期刊：
影响因子：
--
通讯作者：
E. Renault;A. Duret-Lutz;F. Kordon;D. Poitrenaud
中科院分区：
文献类型：
--
作者：
E. Renault;A. Duret-Lutz;F. Kordon;D. Poitrenaud
我们提出了新的并行空检查LTL模型检测。与现有的并行空检查不同，这些检查基于SCC枚举，支持广义Büchi接受，并且不需要同步点也不需要修复过程。我们的算法的一个显着特点是使用一个全球性的联合查找数据结构，其中多个线程共享结构信息的自动机被检查。我们的原型实现具有令人鼓舞的性能：新的空检查有更好的加速比现有的算法在我们的实验的一半。
We present new parallel emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on an SCC enumeration, support generalized Büchi acceptance, and require no synchronization points nor repair procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton being checked. Our prototype implementation has encouraging performances: the new emptiness checks have better speedup than existing algorithms in half of our experiments.