Symbolic Computation of Strongly Connected Components Using Saturation
Symbolic Computation of Strongly Connected Components Using Saturation
复制标题
使用饱和度的强连通分量的符号计算
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Gianfranco Ciardo
中科院分区：
文献类型：
--
作者：
Yang Zhao;Gianfranco Ciardo
在离散状态模型的状态空间中寻找强连通分量（SCC）是LTL和公平CTL性质形式化验证的关键任务，但潜在的大量可达状态和SCC构成了一个艰巨的挑战。本文研究异步系统SCC或终端SCC中状态集的计算问题。由于它在许多应用中的优势，我们采用了两个以前提出的方法：谢-Beerel算法和传递闭包。首先，在Xie-Beerel算法中计算每个SCC时，饱和加速了状态空间探索。然后，我们的主要贡献是一个新的算法来计算传递闭包使用饱和。实验结果表明，在某些情况下，我们的改进算法实现了明显的加速比以前的算法。借助新的传递闭包计算算法，可以在几秒钟内探索多达10 150个SCC。传统的深度优先搜索，激励SCC的符号计算的研究。在本文中，我们的目标是建立在非平凡SCC的状态集。图中SCC的结构可以通过其SCC商图来捕获，通过将每个SCC折叠成单个节点来获得。这个结果图是非循环的，因此定义了SCC上的偏序。终端SCC是SCC商图中的叶节点。在大规模马尔可夫链分析中，一个有趣的问题是将状态空间划分为属于终端SCC的递归状态和不递归的瞬态。SCC计算中的主要困难是：必须探索巨大的状态空间，并且可能必须处理大量的（终端）SCC。第一个问题是由于计算资源的明显限制，形式化验证的主要障碍。传统的基于BDD的方法在状态空间探索上采用镜像和前镜像计算，虽然在完全同步的系统中非常有效，但它们在异步系统中不起作用。第二个问题构成了一个瓶颈一类以前的工作，枚举SCC一个接一个。第2.3节更详细地讨论了这个问题。本文讨论了SCC和终端SCC中的状态计算。我们提出了两个基于前两个思想的方法：Xie-Beerel算法和传递闭包。饱和度，它根据事件的局部性来调度事件的触发，以克服状态空间探索的复杂性。指向第二个困难，我们的努力是致力于一个算法的基础上的传递闭包，它不遭受大量的SCC，但如前所述，往往需要大量的运行时间和内存。然后，我们提出了使用基于饱和度的算法来计算传递闭包，使其成为一个实用的方法SCC计算复杂的系统。我们还提出了一个算法计算递归状态的基础上的传递闭包。
Finding strongly connected components (SCCs) in the state-space of discrete-state models is a critical task in formal verification of LTL and fair CTL properties, but the potentially huge number of reachable states and SCCs constitutes a formidable challenge. This paper is concerned with comput- ing the sets of states in SCCs or terminal SCCs of asynchronous systems. Because of its advantages in many applications, we employsaturationon two previously proposed approaches: the Xie-Beerel algorithm and transitive closure. First, saturation speeds up state-space exploration when computing each SCC in the Xie-Beerel algorithm. Then, our main contribution is a novel algorithm to compute the transitive closure using saturation. Experimental results indicate that our improved algorithms achieve a clear speedup over previous algorithms in some cases. With the help of the new transitive closure computation algorithm, up to 10 150 SCCs can be explored within a few seconds. traditional depth-first search, motivating the study of symbolic computation of SCCs. In this paper, the objective is to build the set of states in non-trivial SCCs. The structure of SCCs in a graph can be captured by itsSCC quotient graph, obtained by collapsing each SCC into a single node. This resulting graph is acyclic, and thus defines a partial order on the SCCs.Terminal SCCsare leaf nodes in the SCC quotient graph. In the context of large scale Markov chain analysis, an interesting problem is to partition the state space intorecurrentstates, which belong to terminal SCCs, andtransientstates, which are not recurrent. The main difficulties in SCC computation are: having to explore huge state spaces and, potentially, having to deal with a large number of (terminal) SCCs. The first problem is the primary obstacle to formal verification due to the obvious limitation of computational resources. Traditional BDD-based approaches employimageandpreimagecomputations on state-space exploration and, while quite suc- cessful in fully synchronous systems, they do not work as well for asynchronous systems. The second problem constitutes a bottleneck for one class of previous work, which enumerates SCCs one by one. Section 2.3 discusses this problem in more detail. This paper addresses the computation of states in SCCs and terminal SCCs. We propose two ap- proaches based on two previous ideas: theXie-Beerel algorithmandtransitive closure. Saturation, which schedules thefiring of events according to their locality, is employed to overcome the complexity of state- space exploration. Pointing to the second difficulty, our efforts are devoted to an algorithm based on the transitive closure, which does not suffer from a huge numbers of SCCs but, as previously proposed, often requires large amounts of runtime and memory. We then propose to use a saturation-based algorithm to compute the transitive closure, enabling it to be a practical method of SCC computation for complex systems. We also present an algorithm for computing recurrent states based on the transitive closure.