Variations on parallel explicit emptiness checks for generalized Büchi automata
Variations on parallel explicit emptiness checks for generalized Büchi automata
复制标题
广义 Büchi 自动机的并行显式空性检查的变体
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
D. Poitrenaud
中科院分区：
文献类型：
--
作者：
E. Renault;A. Duret;F. Kordon;D. Poitrenaud
提出了一种新的用于LTL模型检测的并行显式空性检测方法。与现有的并行清空检查不同，这些检查基于强连接分量(SCC)枚举，支持广义Büchi接受，不需要同步点或重新计算过程。我们算法的一个显著特征是使用全局联合查找数据结构，其中多个线程共享有关被检查自动机的结构信息。除了这些基本算法外，我们还提出了一个架构变体，用于隔离写入Union-Find的线程，以及一个扩展，该扩展基于自动机的SCC强度来分解自动机，以使用更优化的空性检查。我们的算法及其变体的广泛实验结果显示出令人鼓舞的性能，特别是在使用分解技术的情况下。
We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a strongly connected component (SCC) enumeration and support generalized Büchi acceptance, and require no synchronization points or recomputing 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 checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.
DOI：
10.4230/drops.memics.2009.2349
发表时间：
2009-10
期刊：
ArXiv
影响因子：
--
作者：
Andreas Gaiser;Stefan Schwoon
通讯作者：
Andreas Gaiser;Stefan Schwoon