Atlas / Learn / Papers / 20100018551
NASA NTRS · Conference Paper
Symbolic Computation of Strongly Connected Components Using Saturation
Attribution
This is the abstract and citation. Full text lives at NASA NTRS — we link out rather than host. All credit to the authors and Langley Research Center.
Abstract
Verbatim from NASA NTRS. Not paraphrased, not summarized.
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 computing the sets of states in SCCs or terminal SCCs of asynchronous systems. Because of its advantages in many applications, we employ saturation on 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(exp 150) SCCs can be explored within a few seconds.
Authors
- Zhao, Yang California Univ.
- Ciardo, Gianfranco California Univ.
Citation: Zhao, Yang, Ciardo, Gianfranco (2019). Symbolic Computation of Strongly Connected Components Using Saturation. Langley Research Center. NASA NTRS ID 20100018551. https://ntrs.nasa.gov/citations/20100018551 ↗