A Symbolic Symbolic State Space Representation

  • Yann Thierry-Mieg
  • Jean-Michel Ilié
  • Denis Poitrenaud
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3235)


Symmetry based approaches are known to attack the state space explosion problem encountered during the analysis of distributed systems. In another way, BDD-like encodings enable the management of huge data sets. In this paper, we show how to benefit from both approaches automatically. Hence, a quotient set is built from a coloured Petri net description modeling the system. The reachability set is managed under some explicit symbolic operations. Also, data representations are managed symbolically based on a recently introduced data structure, called Data Decisions Diagrams, that allow flexible definition of application specific operators. Performances yielded by our prototype are reported in the paper.


Decision Diagrams Symbolic Model-checking Symbolic Reachability Graph Well-Formed Petri Nets Symmetry Detection 


  1. 1.
    Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed colored nets and symmetric modeling applications. IEEE Transactions on Computers 42(11), 1343–1360 (1993)CrossRefGoogle Scholar
  2. 2.
    Ciardo, G., Lüttgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1-2), 77–104 (1996)CrossRefGoogle Scholar
  4. 4.
    Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.-A.: Data decision diagrams for Petri net analysis. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 101–120. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Couvreur, J.-M., Paviot-Adet, E.: New structural invariant for Petri net analysis. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 199–218. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  6. 6.
    Haddad, S., Ilié, J.-M., Ajami, K.: A model checking method for partially symmetric systems. In: Proc. of FORTE/PSTV 2000, pp. 121–136. Kluwer, Dordrecht (2000)Google Scholar
  7. 7.
    Jensen, K.: Coloured Petri nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 254, pp. 248–299. Springer, Heidelberg (1987)Google Scholar
  8. 8.
    Junttila, T.: New canonical representative marking algorithms for place/transition-nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 258–277. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Klai, K.: Réseaux de Petri: Vérification Symbolique et Modulaire (chapter 3). PhD thesis, Laboratoire d’Informatique de Paris 6 (December 2003)Google Scholar
  10. 10.
    Thierry-Mieg, Y., Dutheillet, C., Mounier, I.: Automatic symmetry detection in wellformed nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol. 2679, pp. 82–101. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Yang, B., Bryant, R.E., O’Hallaron, D.R., Biere, A., Coudert, O., Janssen, G., Ranjan, R.K., Somenzi, F.: A performance study of BDD-based model checking. In: Proc. of FMCAD 1998, pp. 255–289 (1998)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • Yann Thierry-Mieg
    • 1
  • Jean-Michel Ilié
    • 1
  • Denis Poitrenaud
    • 1
  1. 1.SRC - LIP6 - UMR 7606Université Paris 6Paris cedex 05France

Personalised recommendations