Abstract
The paper presents a case study on the synthesis of labelled transition systems (ltss) for process calculi, choosing as testbed Milner’s Calculus of Communicating System (ccs). The proposal is based on a graphical encoding: each ccs process is mapped into a graph equipped with suitable interfaces, such that the denotation is fully abstract with respect to the usual structural congruence.
Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (bcs), proposed by Ehrig and König (which are an instance of relative pushouts, originally introduced by Milner and Leifer). The bc mechanism allows the effective construction of an lts that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence.
Our paper focuses on the analysis of the lts distilled by exploiting the encoding of ccs processes: besides offering some technical contributions towards the simplification of the bc mechanism, the key result of our work is the proof that the bisimilarity on processes obtained via bcs coincides with the standard strong bisimilarity for ccs.
Research partially supported by the DFG project sands, the EU RTN 2-2001-00346 SegraVis and IST 2004-16004 SEnSOria, and the MIUR PRIN 2005015824 ART.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Baldan, P., Corradini, A., Ehrig, H., Löwe, M., Montanari, U., Rossi, F.: Concurrent semantics of algebraic graph transformation. In: Ehrig, H., Kreowski, H.-J., Montanari, U., Rozenberg, G. (eds.) Handbook of Graph Grammars and Computing by Graph Transformation, vol. 3, pp. 107–187. World Scientific, Singapore (1999)
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. LNCS, vol. 3921, pp. 202–216. Springer, Heidelberg (2006)
Baldan, P., Ehrig, H., König, B.: Composition and decomposition of DPO transformations with borrowed context. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 153–167. Springer, Heidelberg (2006)
Berry, G., Boudol, G.: The chemical abstract machine. Theor. Comp. Sci. 96, 217–248 (1992)
Bonchi, F., Gadducci, F., König, B.: Process bisimulation via a graphical encoding. Technical Report TR-06-07, Dipartimento di Informatica, Università di Pisa (2006)
Corradini, A., Gadducci, F.: An algebraic presentation of term graphs, via gs-monoidal categories. Applied Categorical Structures 7, 299–331 (1999)
Corradini, A., Montanari, U., Rossi, F.: Graph processes. Fundamenta Informaticae 26, 241–265 (1996)
Ehrig, H., König, B.: Deriving bisimulation congruences in the DPO approach to graph rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 151–166. Springer, Heidelberg (2004)
Engelfriet, J., Gelsema, T.: Multisets and structural congruence of the π-calculus with replication. Theor. Comp. Sci. 211, 311–337 (1999)
Gadducci, F.: Term graph rewriting and the π-calculus. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 37–54. Springer, Heidelberg (2003)
Gadducci, F., Heckel, R.: An inductive view of graph transformation. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 219–233. Springer, Heidelberg (1998)
Gadducci, F., Montanari, U.: A concurrent graph semantics for mobile ambients. In: Brookes, S., Mislove, M. (eds.) Mathematical Foundations of Programming Semantics. Electr. Notes in Theor. Comp. Sci., vol. 45. Elsevier Science, Amsterdam (2001)
Gadducci, F., Montanari, U.: Observing reductions in nominal calculi via a graphical encoding of processes. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 106–126. Springer, Heidelberg (2005)
Jensen, O.H., Milner, R.: Bigraphs and transitions. In: Morriset, G. (ed.) Principles of Programming Languages, pp. 38–49. ACM Press, New York (2003)
Leifer, J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 243–258. Springer, Heidelberg (2000)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: The polyadic π-calculus: A tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. Nato ASI Series F, vol. 94, pp. 203–246. Springer, Heidelberg (1993)
Milner, R.: Pure bigraphs: Structure and dynamics. Information and Computation 204, 60–122 (2006)
Parrow, J., Victor, B.: The fusion calculus: Expressiveness and simmetry in mobile processes. In: Pratt, V. (ed.) Logic in Computer Science, pp. 176–185. IEEE Computer Society Press, Los Alamitos (1998)
Sassone, V., Sobociński, P.: Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing 10, 163–183 (2003)
Sassone, V., Sobociński, P.: Reactive systems over cospans. In: Logic in Computer Science, pp. 311–320. IEEE Computer Society Press, Los Alamitos (2005)
Sewell, P.: From rewrite rules to bisimulation congruences. Theor. Comp. Sci. 274, 183–230 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonchi, F., Gadducci, F., König, B. (2006). Process Bisimulation Via a Graphical Encoding. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds) Graph Transformations. ICGT 2006. Lecture Notes in Computer Science, vol 4178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11841883_13
Download citation
DOI: https://doi.org/10.1007/11841883_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-38870-8
Online ISBN: 978-3-540-38872-2
eBook Packages: Computer ScienceComputer Science (R0)