Cluster-Based LTL Model Checking of Large Systems
Cluster-Based LTL Model Checking of Large Systems
复制标题
基于集群的大型系统零担模型检查
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
I. Cerná
中科院分区：
文献类型：
--
作者：
J. Barnat;L. Brim;I. Cerná
近年来，出现了一系列并行和分布式的有限状态系统验证算法。我们调查分布式内存枚举LTL模型检测算法设计的网络工作站通过MPI通信。在基于自动机的LTL模型检测方法中，该问题被简化为图中的接受循环检测问题。分布式算法，在相反的顺序，不能依赖于深度优先搜索后序，这是必不可少的有效检测接受周期。因此，为了提出有效和实用的分布式算法，必须采用各种条件来证明图中存在圈。我们比较这些算法的理论和实验，并确定特定的算法可以成功的情况下。
In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed-memory enumerative LTL model checking algorithms designed for networks of workstations communicating via MPI. In the automata-based approach to LTL model checking the problem is reduced to the accepting cycle detection problem in a graph. Distributed algorithms, in opposite to sequential ones, cannot rely on depth-first search postorder which is essential for efficient detection of accepting cycles. Therefore, diverse conditions that characterise the existence of cycles in a graph have to be employed in order to come up with efficient and practical distributed algorithms. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be successful.