Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-12-04T09:25:33.095Z Has data issue: false hasContentIssue false
  • English
  • Français

Graph rewriting for the π-calculus†

Published online by Cambridge University Press:  01 June 2007

FABIO GADDUCCI
FABIO GADDUCCI*
Affiliation:
Dipartimento di Informatica, Universitá di Pisa, largo Pontecorvo 3c, I-56127 Pisa, Italy Email: [email protected].
Get access Rights & Permissions [Opens in a new window]

Abstract

We propose a graphical implementation for (possibly recursive) processes of the π-calculus, encoding each process into a graph. Our implementation is sound and complete with respect to the structural congruence for the calculus: two processes are equivalent if and only if they are mapped into graphs with the same normal form. Most importantly, the encoding allows the use of standard graph rewriting mechanisms for modelling the reduction semantics of the calculus.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 17 , Issue 3 , June 2007 , pp. 407 - 437
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Baldan, P., Corradini, A., Ehrig, H., Löwe, M., Montanari, U. and Rossi, F. (1999) Concurrent semantics of algebraic graph transformation. In: Ehrig, H., Kreowski, H.-J., Montanari, U. and Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation, Volume 3, World Scientific 107–187.Google Scholar
Baldan, P., Gadducci, F. and Montanari, U. (2006) Concurrent rewriting for graphs with equivalences. In: Baier, C. and Hermanns, H. (eds.) Concurrency Theory. Springer-Verlag Lecture Notes in Computer Science 4137 279–294.Google Scholar
Berry, G. and Boudol, G. (1992) The chemical abstract machine. Theoretical Computer Science 96 217–248.Google Scholar
Bonchi, F., Gadducci, F. and König, B. (2006) Process bisimulation via a graphical encoding. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L. and Rozenberg, G. (eds.) Graph Transformation. Springer-Verlag Lecture Notes in Computer Science 4187 168–183.Google Scholar
Bruni, R., Gadducci, F. and Montanari, U. (2002) Normal forms for algebras of connections. Theoretical Computer Science 286 247–292.Google Scholar
Caires, L. (2004) Behavioral and spatial observations in a logic for the π-calculus. In: Walukiewicz, I. (ed.) Foundations of Software Science and Computation Structures. Springer-Verlag Lecture Notes in Computer Science 2987 72–87.Google Scholar
Caires, L. and Cardelli, L. (2003). A spatial logic for concurrency (part I). Information and Computation 186 194–235.Google Scholar
Căzănescu, V.-E. and Ştefănescu, Gh. (1992) A general result on abstract flowchart schemes with applications to the study of accessibility, reduction and minimization. Theoretical Computer Science 99 1–63.Google Scholar
Corradini, A. and Gadducci, F. (1999a) An algebraic presentation of term graphs, via gs-monoidal categories. Applied Categorical Structures 7 299–331.CrossRefGoogle Scholar
Corradini, A. and Gadducci, F. (1999b) Rewriting on cyclic structures: Equivalence between the operational and the categorical description. Informatique Théorique et Applications/Theoretical Informatics and Applications 33 467–493.Google Scholar
Corradini, A., Montanari, U. and Rossi, F. (1994) An abstract machine for concurrent modular systems: CHARM. Theoretical Computer Science 122 165–200.Google Scholar
Corradini, A., Montanari, U. and Rossi, F. (1996) Graph processes. Fundamenta Informaticae 26 241–265.Google Scholar
Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R. and Löwe, M. (1997) Algebraic approaches to graph transformation I: Basic concepts and double pushout approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Volume 1, World Scientific 163–245.Google Scholar
Courcelle, B. (1997) The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Volume 1, World Scientific 313–400.Google Scholar
Drewes, F., Habel, A. and Kreowski, H.-J. (1997) Hyperedge replacement graph grammars. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Volume 1, World Scientific 95–162.Google Scholar
Ehrig, H. and König, B. (2004) Deriving bisimulation congruences in the DPO approach to graph rewriting. In: Walukiewicz, I. (ed.) Foundations of Software Science and Computation Structures. Springer-Verlag Lecture Notes in Computer Science 2987 151–166.Google Scholar
Fu, Y. (1999) Variations on mobile processes. Theoretical Computer Science 221 327–368.CrossRefGoogle Scholar
Gadducci, F. (2003) Term graph rewriting and the π-calculus. In: Ohori, A. (ed.) Programming Languages and Semantics. Springer-Verlag Lecture Notes in Computer Science 2895 37–54.Google Scholar
Gadducci, F., Heckel, R. and Llabrés, M. (1999) A bi-categorical axiomatisation of concurrent graph rewriting. In: Hofmann, M., Pavlovič, D. and Rosolini, G. (eds.) Category Theory and Computer Science. Electronic Notes in Theoretical Computer Science 29.Google Scholar
Gadducci, F. and Lluch Lafuente, A. (2006) Graphical verification of a spatial logic for the π-calculus. In: Heckel, R., König, B. and Rensink, A. (eds.) Graph Transformation for Verification and Concurrency. Electronic Notes in Theoretical Computer Science 154.Google Scholar
Gadducci, F. and Lluch Lafuente, A. (2007) Graphical encoding of a spatial logic for the π-calculus. In: Montanari, U. and Mossakowski, T. (eds.) Algebra and Coalgebra in Computer Science. Springer-Verlag Lecture Notes in Computer Science (to appear).Google Scholar
Gadducci, F. and Montanari, U. (2001) A concurrent graph semantics for mobile ambients. In: Brookes, S. and Mislove, M. (eds.) Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science 45.Google Scholar
Gadducci, F. and Montanari, U. (2002) Comparing logics for rewriting: Rewriting logic, action calculi and tile logic. Theoretical Computer Science 285 319–358.Google Scholar
Gadducci, F. and Montanari, U. (2005) Observing reductions in nominal calculi via a graphical encoding of processes. In: Middeldorp, A.van Oostrom, V., van Raamsdonk, F. and de Vrijer, R. C. (eds.) Processes, terms and cycles (Klop Festschrift). Springer-Verlag Lecture Notes in Computer Science 3838 106–126.Google Scholar
Goguen, J. and Meseguer, J. (1992) Order sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105 217–273.CrossRefGoogle Scholar
König, B. (1999) Generating type systems for process graphs. In: Baeten, J. C. M. and Mauw, S. (eds.) Concurrency Theory. Springer-Verlag Lecture Notes in Computer Science 1664 352–367.Google Scholar
Laneve, C., Parrow, J. and Victor, B. (2001) Solo diagrams. In: Kobayashi, N. and Pierce, B. (eds.) Theoretical Aspects of Computer Science. Springer-Verlag Lecture Notes in Computer Science 2215 127–144.Google Scholar
Leifer, J. and Milner, R. (2000) Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) Concurrency Theory. Springer-Verlag Lecture Notes in Computer Science 1877 243–258.Google Scholar
Milner, R. (1989) Communication and Concurrency, Prentice Hall.Google Scholar
Milner, R. (1993) The polyadic π-calculus: A tutorial. In: Bauer, F. L., Brauer, W. and Schwichtenberg, H. (eds.) Logic and Algebra of Specification. Nato ASI Series F 94 203–246.Google Scholar
Milner, R. (2001) Bigraphical reactive systems. In: Larsen, K.G. and Nielsen, M. (eds.) Concurrency Theory. Springer-Verlag Lecture Notes in Computer Science 2154 16–35.Google Scholar
Montanari, U., Pistore, M. and Rossi, F. (1999) Modeling concurrent, mobile and coordinated systems via graph transformations: Concurrency, parallellism, and distribution. In: Ehrig, H., Kreowski, H.-J., Montanari, U. and Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation, Volume 3, World Scientific 189–268.Google Scholar
Plotkin, G. (1981) A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University.Google Scholar
Plump, D. (2005) Confluence of graph transformation revisited. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F. and de Vrijer, R. C. (eds.) Processes, terms and cycles (Klop Festschrift). Springer-Verlag Lecture Notes in Computer Science 3838 280–308.Google Scholar
Sangiorgi, S. and Walker, D. (2001) The π-calculus: A Theory of Mobile Processes, Cambridge University Press.Google Scholar
Yoshida, N. (1994) Graph notation for concurrent combinators. In: Ito, T. and Yonezawa, A. (eds.) Theory and Practice of Parallel Programming. Springer-Verlag Lecture Notes in Computer Science 907 393–412.Google Scholar