Unfolding Graph Transformation Systems: Theory and Applications to Verification

  • Paolo Baldan
  • Andrea Corradini
  • Barbara König
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5065)


The unfolding of a system represents in a single branching structure all its possible computations: it is the cornerstone both of semantical constructions and of efficient partial order verification techniques. In this paper we survey the contributions we elaborated in the last decade with Ugo Montanari and other colleagues, concerning the unfolding of graph transformation systems, and its use in the definition of a Winskel style functorial semantics and in the development of methodologies for the verification of finite and infinite state systems.


Graph Transformation Type Graph Graph Grammar Reachable Graph Graph Transformation System 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baldan, P.: Modelling concurrent computations: from contextual Petri nets to graph grammars. PhD thesis, Department of Computer Science, University of Pisa, Available as technical report n. TD-1/00 (2000)Google Scholar
  2. 2.
    Baldan, P., Corradini, A., Esparza, J., Heindel, T., König, B., Kozioura, V.: Verifying Red-Black Trees. In: Proc. of COSMICAH 2005, vol. RR-05-04, pp. 1–15. Queen Mary University, Dept. of Computer Science (2005)Google Scholar
  3. 3.
    Baldan, P., Corradini, A., Heindel, T., König, B., Sobociński, P.: Processes for Adhesive Rewriting Systems. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol. 3921, pp. 202–216. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Baldan, P., Corradini, A., König, B.: A static analysis technique for graph transformation systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 381–395. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Baldan, P., Corradini, A., König, B.: Verifying finite-state graph grammars: an unfolding-based approach. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 83–98. Springer, Heidelberg (2004); Full version as Tech.Rep.CS-2004-10, Dept.of Comp.Sci., University Ca’ Foscari of VeniceGoogle Scholar
  6. 6.
    Baldan, P., Corradini, A., König, B., Schwoon, S.: McMillan’s Complete Prefix for Contextual Nets. In: ToPNoC - Trans. on Petri Nets and Other Models of Concurrency (to appear, 2008); Special Issue from PN 2007 Workshops and TutorialsGoogle Scholar
  7. 7.
    Baldan, P., Corradini, A., Montanari, U.: Unfolding and Event Structure Semantics for Graph Grammars. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 73–89. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures and processes. Information and Computation 171(1), 1–49 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Baldan, P., Corradini, A., Montanari, U., Ribeiro, L.: Unfolding Semantics of Graph Transformation. Information and Computation 205, 733–782 (2007)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Baldan, P., König, B.: Approximating the behaviour of graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 14–29. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  11. 11.
    Baldan, P., König, B., König, B.: A logic for analyzing abstractions of graph transformation systems. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 255–272. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Bruni, R., Melgratti, H.C., Montanari, U.: Event structure semantics for nominal calculi. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 295–309. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Corradini, A., Montanari, U., Rossi, F.: Graph processes. Fundamenta Informaticae 26, 241–265 (1996)zbMATHMathSciNetGoogle Scholar
  14. 14.
    Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg [31]Google Scholar
  15. 15.
    Ehrig, H., Heckel, R., Korff, M., Löwe, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic Approaches to Graph Transformation II: Single Pushout Approach and comparison with Double Pushout Approach. In: Rozenberg [31]Google Scholar
  16. 16.
    Ehrig, H., Kreowski, H.-J., Montanari, U., Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformation: Concurrency, Parallelism and Distribution, vol. 3. World Scientific, Singapore (1999)zbMATHGoogle Scholar
  17. 17.
    Esparza, J.: Model checking using net unfoldings. Science of Computer Programming 23(2–3), 151–195 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20(20), 285–310 (2002)zbMATHCrossRefGoogle Scholar
  19. 19.
    Goltz, U., Reisig, W.: The non-sequential behaviour of Petri nets. Information and Control 57, 125–147 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Howell, R.R., Rosier, L.E., Yen, H.: A taxonomy of fairness and temporal logic problems for Petri nets. Theoretical Computer Science 82, 341–372 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    König, B., Kozioura, V.: Augur 2—a new version of a tool for the analysis of graph transformation systems. In: Bruni, R., Varró, D. (eds.) Proceedings of GT-VMT 2006 (Workshop on Graph Transformation and Visual Modeling Techniques). ENTCS, Elsevier, Amsterdam (2008)Google Scholar
  22. 22.
    Lack, S., Sobociński, P.: Adhesive categories. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 273–288. Springer, Heidelberg (2004)Google Scholar
  23. 23.
    Langerak, R.: Transformation and Semantics for LOTOS. PhD thesis, Department of Computer Science, University of Twente (1992)Google Scholar
  24. 24.
    Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6, 1–35 (1995)CrossRefGoogle Scholar
  25. 25.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  26. 26.
    Meseguer, J., Montanari, U., Sassone, V.: On the semantics of Petri nets. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 286–301. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  27. 27.
    Nielsen, M., Plotkin, G., Winskel, G.: Petri Nets, Event Structures and Domains, Part 1. Theoretical Computer Science 13, 85–108 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  28. 28.
    Pinna, G.M., Poigné, A.: On the nature of events: another perspective in concurrency. Theoretical Computer Science 138(2), 425–454 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    Reisig, W.: Petri Nets: An Introduction. EACTS Monographs on Theoretical Computer Science. Springer, Heidelberg (1985)zbMATHGoogle Scholar
  30. 30.
    Ribeiro, L.: Parallel Composition and Unfolding Semantics of Graph Grammars. PhD thesis, Technische Universität Berlin (1996)Google Scholar
  31. 31.
    Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation: Foundations, vol. 1. World Scientific, Singapore (1997)zbMATHGoogle Scholar
  32. 32.
    Vogler, W., Semenov, A., Yakovlev, A.: Unfolding and finite prefix for nets with read arcs. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 501–516. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  33. 33.
    Winskel, G.: Event Structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Paolo Baldan
    • 1
  • Andrea Corradini
    • 2
  • Barbara König
    • 3
  1. 1.Dipartimento di Matematica Pura e ApplicataUniversità di PadovaItaly
  2. 2.Dipartimento di InformaticaUniversità di PisaItaly
  3. 3.Abt. für Informatik und Ang. KognitionswissenschaftUniversität Duisburg-EssenGermany

Personalised recommendations