Abstract
The computation of strongly connected components (SCCs) in discrete-state models is a critical step in formal verification of LTL and fair CTL properties, but the potentially huge number of reachable states and SCCs constitutes a formidable challenge. We consider the problem of computing the set of states in SCCs or terminal SCCs in an asynchronous system. We employ the idea of saturation, which has shown clear advantages in symbolic state-space exploration (Ciardo et al. in Softw Tools Technol Transf 8(1):4–25, 2006; Zhao and Ciardo in Proceedings of 7th international symposium on automated technology for verification and analysis, pp 368–381, 2009), to improve two previously proposed approaches. We use saturation to speed up state exploration when computing each SCC in the Xie-Beerel algorithm, and we compute the transitive closure of the transition relation using a novel algorithm based on saturation. Furthermore, we show that the techniques we developed are also applicable to the computation of fair cycles. Experimental results indicate that the improved algorithms using saturation achieve a substantial speedup over previous BFS algorithms. In particular, with the new transitive closure computation algorithm, up to 10150 SCCs can be explored within a few seconds.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Ábrahám E, Jansen N, Wimmer R, Katoen J-P, Becker B (2010) DTMC model checking by SCC reduction. In: QEST, pp 37–46
Bloem R, Gabow HN, Somenzi F (2000) An algorithm for strongly connected component analysis in n log n symbolic steps. In: Formal methods in computer aided design. Springer, Berlin, pp 37–54
Bollig B, Wegener I (1996) Improving the variable ordering of OBDDs is NP-complete. IEEE Trans Comput 45(9): 993–1002
Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8): 677–691
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98: 142–170
Ciardo G et al (2003) SMART: Stochastic Model checking Analyzer for Reliability and Timing, User Manual. http://www.cs.ucr.edu/~ciardo/SMART/.
Ciardo G, Jones RL, Miner AS, Siminiceanu R (2006) Logical and stochastic modeling with SMART. Perf Eval 63: 578–608
Ciardo G, Marmorstein R, Siminiceanu R (2006) The saturation algorithm for symbolic state space exploration. Softw Tools Technol Transf 8(1): 4–25
Ciardo G, Siminiceanu R (2003) Structural symbolic CTL model checking of asynchronous systems. In: Hunt WA Jr, Somenzi F (eds) Proceedings of CAV, Boulder, CO. LNCS, vol 2725. Springer, Berlin, pp 40–53
Ciesinski F, Baier C, Grösser M, Klein J (2008) Reduction techniques for model checking Markov decision processes. In: Proceedings of the 2008 5th international conference on quantitative evaluation of systems. IEEE Computer Society, Washington, DC, pp 45–54
Cimatti A, Clarke E, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model checker. http://nusmv.irst.itc.it/
Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA
Emerson EA, Lei C-L (1986) Efficient model checking in fragments of the propositional mu-Calculus. In: Proceedings, symposium on logic in computer science, 16–18 Jun 1986. IEEE Computer Society, Cambridge, MA, pp 267–278
Fisler K, Fraer R, Kamhi G, Vardi MY, Yang Z (2001) Is there a best symbolic cycle-detection algorithm? In: Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2001, London, UK. Springer, Berlin, pp 420–434
Hachtel G, Macii E, Pardo A, Somenzi F (1996) Markovian analysis of large finite state machines. IEEE Trans CAD Integr Circ Syst 15(12): 1479–1493
Hardin RH, Kurshan RP, Shukla SK, Vardi MY (2001) A new heuristic for bad cycle detection using bdds. Formal Methods Syst Des 18(2): 131–140
Hojati R, Touati HJ, Kurshan RP, Brayton RK (1992) Efficient ω-regular language containment. In: CAV, pp 396–409
Kam T, Villa T, Brayton RK, Sangiovanni-Vincentelli A (1998) Multi-valued decision diagrams: theory and applications. Multiple Valued Logic 4(1–2): 9–62
Kesten Y, Pnueli A, Raviv L-o (1998) Algorithmic verification of linear temporal logic specifications. In: ICALP ’98: Proceedings of the 25th international colloquium on automata, languages and programming, London, UK. Springer, Berlin, pp 1–16
Matsunaga Y, McGeer PC, Brayton RK (1993) On computing the transitive closure of a state transition relation. In: Proceedings of the 30th international design automation conference, pp 260–265
Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4): 541–579
Ravi K, Bloem R, Somenzi F (2000) A comparative study of symbolic algorithms for the computation of fair cycles. In: FMCAD ’00: Proceedings of the 3rd international conference on formal methods in computer-aided design, London, UK. Springer, Berlin, pp 143–160
Safra S, Vardi MY (1989) On omega-automata and temporal logic. In: Proceedings of the 21st annual ACM symposium on theory of computing. ACM, Seattle, pp 127–137
Somenzi F, Ravi K, Bloem R (2002) Analysis of symbolic SCC hull algorithms. In: FMCAD ’02: Proceedings of the 4th international conference on formal methods in computer-aided design, London, UK. Springer, Berlin, pp 88–105
Stewart WJ (1994) Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton
Tarjan R (1971) Depth-first search and linear graph algorithms. In: Proceedings of the 12th annual symposium on switching and automata Theory (swat 1971). IEEE Computer Society, Washington, DC, pp 114–121
Wan M, Ciardo G (2009) Symbolic state-space generation of asynchronous systems using extensible decision diagrams. In: Nielsen M et al (eds) Proceedings of 35th international conference on current trends in theory and practice of computer science (SOFSEM), Špindlerův Mlýn, Czech Republic. LNCS, vol 5404. Springer, Berlin, pp 582–594
Xie A, Beerel PA (1998) Efficient state classification of finite-state Markov chains. IEEE Trans CAD Integr Circuit Syst 17(12): 1334–1339
Xie A, Beerel PA (2000) Implicit enumeration of strongly connected components and an application to formal verification. IEEE Trans CAD Integr Circuit Syst 19(10): 1225–1230
Zhao Y, Ciardo G (2009) Symbolic CTL model checking of asynchronous systems using constrained saturation. In: Liu Z, Ravn AP (eds) Proceedings of 7th international symposium on automated technology for verification and analysis (ATVA), Macao SAR, China. LNCS, vol 5799. Springer, Berlin, pp 368–381
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Zhao, Y., Ciardo, G. Symbolic computation of strongly connected components and fair cycles using saturation. Innovations Syst Softw Eng 7, 141–150 (2011). https://doi.org/10.1007/s11334-011-0146-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-011-0146-3