Bigraphs and transitions

ABSTRACT

A bigraphical reactive system (BRS) involves bigraphs, in which the nesting of nodes represents locality, independently of the edges connecting them. BRSs represent a wide variety of calculi for mobility, including λ-calculus and ambient calculus. A labelled transition system (LTS) for each BRS is here derived uniformly, adapting previous work of Leifer and Milner, so that under certain conditions the resulting bisimilarity is automatically a congruence. For an asynchronous λ-calculus, this LTS and its bisimilarity agree closely with the standard.

REFERENCES

• 1: Gérard Berry , Gérard Boudol, The chemical abstract machine, Theoretical Computer Science, v.96 n.1, p.217-248, 6 April 1992
• 2: Boudol, G. (1992), Asynchrony and the λ-calculus. Rapport de Recherche RR-1702, INRIA Sophia-Antipolis.
• 3: Luca Cardelli , Andrew D. Gordon, Mobile Ambients, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure, p.140-155, March 28-April 04, 1998
• 4: Cattani, G.L., Leifer, J.J. and Milner, R. (2000), Contexts and Embeddings for closed shallow action graphs. University of Cambridge Computer Laboratory, Technical Report 496. {Submitted for publication.} Available at http://pauillac.inria.fr/~leifer.
• 5: Frank Drewes , Berthold Hoffmann , Detlef Plump, Hierarchical Graph Transformation, Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, p.98-113, March 25-April 02, 2000
• 6: Hartmut Ehrig, Introduction to the Algebraic Theory of Graph Grammars (A Survey), Proceedings of the International Workshop on Graph-Grammars and Their Application to Computer Science and Biology, p.1-69, October 30-November 03, 1978
• 7: Ehrig, H. (2002) Bigraphs meet double pushouts. EATCS Bulletin 78, October 2002, pp72--85.
• 8: Philippa Gardner, From Process Calculi to Process Frameworks, Proceedings of the 11th International Conference on Concurrency Theory, p.69-88, August 22-25, 2000
• 9: Philippa Gardner , Lucian Wischik, Explicit Fusions, Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science, p.373-382, September 01, 2000
• 10: Fabio Gadducci , Reiko Heckel, An inductive view of graph transformation, Selected papers from the 12th International Workshop on Recent Trends in Algebraic Development Techniques, p.223-237, July 01, 1997
• 11: Dan Hirsch , Ugo Montanari, Synchronized Hyperedge Replacement with Name Mobility, Proceedings of the 12th International Conference on Concurrency Theory, p.121-136, August 20-25, 2001
• 12: Kohei Honda , Mario Tokoro, On Asynchronous Communication Semantics, Proceedings of the Workshop on Object-Based Concurrent Computing, p.21-51, July 15-16, 1991
• 13: Leifer, J.J. (2001), Operational congruences for reactive systems. PhD Dissertation, University of Cambridge Computer Laboratory. Distributed in revised form as Technical Report 521. Available from http://pauillac.inria.fr/~leifer.
• 14: Jensen, O.H. and Milner, R. (2002), Bigraphs and process calculi. To appear as a Technical Report, University of Cambridge Computer Laboratory (2002).
• 15: James J. Leifer , Robin Milner, Deriving Bisimulation Congruences for Reactive Systems, Proceedings of the 11th International Conference on Concurrency Theory, p.243-258, August 22-25, 2000
• 16: Milner, R. (1996), Calculi for interaction. Acta Informatica 33, pp707--737.
• 17: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 18: Robin Milner, Bigraphical Reactive Systems, Proceedings of the 12th International Conference on Concurrency Theory, p.16-35, August 20-25, 2001
• 19: Milner, R. Bigraphical reactive systems: basic theory. Technical Report 503, University of Cambridge Computer Laboratory (2001). Available from http://www.cl.cam.ac.uk/~rm135.
• 20: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 21: Robin Milner , Davide Sangiorgi, Barbed Bisimulation, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.685-695, July 13-17, 1992
• 22: Park, D.M.R. (1980), Concurrency and automata on infinite sequences. LNCS 104, Springer Verlag.
• 23: J. Parrow , B. Victor, The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.176, June 21-24, 1998
• 24: Davide Sangiorgi , David Walker, PI-Calculus: A Theory of Mobile Processes, Cambridge University Press, New York, NY, 2001
• 25: Sassone, V. and Sobocinski, P. (2002), Deriving bisimulation congruences: a 2-categorical approach. Electronic Notes in Theoretical Computer Science, Vol 68 (2), 19pp.
• 26: Peter Sewell, From rewrite rules to bisimulation congruences, Theoretical Computer Science, v.274 n.1-2, p.183-230, March 6, 2002 [doi>10.1016/S0304-3975(00)00309-1]
• 27: Pawel T. Wojciechowski , Peter Sewell, Nomadic Pict: Language and Infrastructure Design for Mobile Agents, Proceedings of the First International Symposium on Agent Systems and Applications Third International Symposium on Mobile Agents, p.2, October 03-06, 1999

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Theory

Keywords:
λ-calculus, bigraph, bisimilarity, mobile computation, reactive system, transition system