Symbolic Computation of Strongly Connected Components Using Saturation
Yang Zhao, Gianfranco Ciardo · NASA STI Repository (National Aeronautics and Space Administration) · 2010
Finding strongly connected components (SCCs) in discrete-state models is a critical task in formal verification concerning LTL and fair CTL properties, the potentially huge number of reachable states and SCCs constitute a formidable challenge. This paper is devoted to computing the sets of states in SCCs and terminal SCCs in asynchronous systems. Motivated by its clear advantages in many applications, the idea of saturation is employed on two previously proposed approaches: Lockstep and transitive closure. First, saturation speeds up state-space exploration when computing each SCC in Lockstep. Then, our main contribution is a novel algorithm to compute the transitive closure using saturation. The experimental results indicate that our improved algorithms achieve a clear speedup over their original implementations. With the help of the new transitive closure computation algorithm, up to 10 150 SCCs can be explored within a few seconds. 1