Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning

  • Gianfranco Ciardo
  • Andy Jinqing Yu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


We propose a new saturation-based symbolic state-space generation algorithm for finite discrete-state systems. Based on the structure of the high-level model specification, we first disjunctively partition the transition relation of the system, then conjunctively partition each disjunct. Our new encoding recognizes identity transformations of state variables and exploits event locality, enabling us to apply a recursive fixed-point image computation strategy completely different from the standard breadth-first approach employing a global fix-point image computation. Compared to breadth-first symbolic methods, saturation has already been empirically shown to be several orders more efficient in terms of runtime and peak memory requirements for asynchronous concurrent systems. With the new partitioning, the saturation algorithm can now be applied to completely general asynchronous systems, while requiring similar or better run-times and peak memory than previous saturation algorithms.


Model Check Transition Relation Reduction Rule Symbolic Model Check Redundant Node 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic reachability analysis based on SAT-solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 411–425. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  2. 2.
    Barner, S., Rabinovitz, I.: Efficient symbolic model checking of software using partial disjunctive partitioning. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 35–50. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: DAC, pp. 29–34 (2000)Google Scholar
  4. 4.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp. 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  5. 5.
    Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 78–97. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Ciardo, G., Luettgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  8. 8.
    Ciardo, G., Miner, A.S.: A data structure for the efficient Kronecker solution of GSPNs. In: PNPM, pp. 22–31 (1999)Google Scholar
  9. 9.
    Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  11. 11.
    Derisavi, S., Kemper, P., Sanders, W.H.: Symbolic state-space exploration and numerical analysis of state-sharing composed models. In: NSMC, pp. 167–189 (2003)Google Scholar
  12. 12.
    Dolev, D., Klawe, M., Rodeh, M.: An O(n logn) unidirectional distributed algorithm for extrema finding in a circle. J. of Algorithms 3(3), 245–260 (1982)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Asp. of Comp. 8(5), 607–616 (1996)zbMATHCrossRefGoogle Scholar
  14. 14.
    Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley, Reading (2003)Google Scholar
  15. 15.
    Jin, H., Kuehlmann, A., Somenzi, F.: Fine-grain conjunction scheduling for symbolic reachability analysis. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 312–326. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI, pp. 49–58 (1991), IFIPGoogle Scholar
  17. 17.
    McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)zbMATHGoogle Scholar
  18. 18.
    Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1–2), 9–62 (1998)zbMATHMathSciNetGoogle Scholar
  19. 19.
    Kimura, S., Clarke, E.M.: A parallel algorithm for constructing binary decision diagrams. In: ICCD, pp. 220–223 (1990)Google Scholar
  20. 20.
    Miner, A.S.: Saturation for a general class of models. In: QEST, pp. 282–291 (2004)Google Scholar
  21. 21.
    Moon, I.-H., Hachtel, G.D., Somenzi, F.: Border-block triangular form and conjunction schedule in image computation. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 73–90. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  22. 22.
    Moon, I.-H., Kukula, J.H., Ravi, K., Somenzi, F.: To split or to conjoin: the question in image computation. In: DAC, pp. 23–28 (2000)Google Scholar
  23. 23.
    Narayan, A., Isles, A.J., Jain, J., Brayton, R.K., Sangiovanni-Vincentelli, A.: Reachability analysis using partitioned-ROBDDs. In: ICCAD, pp. 388–393 (1997)Google Scholar
  24. 24.
    Pastor, E., Roig, O., Cortadella, J., Badia, R.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416–435. Springer, Heidelberg (1994)Google Scholar
  25. 25.
    Plateau, B.: On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In: SIGMETRICS, pp. 147–153 (1985)Google Scholar
  26. 26.
    Solé, M., Pastor, E.: Traversal techniques for concurrent systems. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 220–237. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Gianfranco Ciardo
    • 1
  • Andy Jinqing Yu
    • 1
  1. 1.Dept. of Computer Science and EngineeringUniv. of CaliforniaRiverside

Personalised recommendations