Bigraph: Difference between revisions

Content deleted Content added

Inline

Revision as of 13:05, 18 January 2021

A bigraph (often used in the plural bigraphs) can be modelled as the superposition of a graph (the link graph) and a set of trees (the place graph).^[1]^[2]

Each node of the bigraph is part of a graph and also part of some tree that describes how the nodes are nested. Bigraphs can be conveniently and formally displayed as diagrams.^[1] They have applications in the modelling of distributed systems for ubiquitous computing and can be used to describe mobile interactions. They have also been used by Robin Milner in an attempt to subsume Calculus of Communicating Systems (CCS) and π-calculus.^[2] They have been studied in the context of category theory.^[3]^[4]

Anatomy of a bigraph

Aside from nodes and (hyper-)edges, a bigraph may have associated with it one or more regions which are roots in the place forest, and zero or more holes in the place graph, into which other bigraph regions may be inserted. Similarly, to nodes we may assign controls that define identities and an arity (the number of ports for a given node to which link-graph edges may connect). These controls are drawn from a bigraph signature. In the link graph we define inner and outer names, which define the connection points at which coincident names may be fused to form a single link.

Foundations

A bigraph is a 5-tuple:

$(V,E,ctrl,prnt,link):\langle k,X\rangle \to \langle m,Y\rangle ,$

where $V$ is a set of nodes, $E$ is a set of edges, $ctrl$ is the control map that assigns controls to nodes, $prnt$ is the parent map that defines the nesting of nodes, and $link$ is the link map that defines the link structure.

The notation $\langle k,X\rangle \to \langle m,Y\rangle$ indicates that the bigraph has $k$ holes (sites) and a set of inner names $X$ and $m$ regions, with a set of outer names $Y$ . These are respectively known as the inner and outer interfaces of the bigraph.

Formally speaking, each bigraph is an arrow in a symmetric partial monoidal category (usually abbreviated spm-category) in which the objects are these interfaces.^[5] As a result, the composition of bigraphs is definable in terms of the composition of arrows in the category.

Extensions and variants

A directed bigraph modelling a container system.^[6]

Directed Bigraphs

Directed Bigraphs^[7] are a generalisation of bigraphs where hyper-edges of the link-graph are directed. Ports and names of the interfaces are extended with a polarity (positive or negative) with the requirement that the direction of hyper-edges goes from negative to positive.

Directed bigraphs were introduced as a meta-model for describing computation paradigms dealing with locations and resource communication where a directed link-graph provides a natural description of resource dependencies or information flow. Examples of areas of applications are security protocols,^[8] resource access management,^[9] and cloud computing.^[6]

Bigraphs with sharing

Example bigraph with sharing in which the node of control M is shared by the two nodes of control S. This is represented by M being in the intersection of the two S-nodes.

Bigraphs with sharing^[10] are a generalisation of Milner's formalisation that allows for a straightforward representation of overlapping or intersecting spatial locations. In bigraphs with sharing, the place graph is defined as a directed acyclic graph (DAG), i.e. $prnt$ is a binary relation instead of a map. The definition of link graph is unaffected by the introduction of sharing. Note that standard bigraphs are a sub-class of bigraphs with sharing.

Areas of application of bigraphs with sharing include wireless networking protocols,^[11] real-time management of domestic wireless networks^[12] and mixed reality systems.^[13]

Tools and Implementations

jLibBig is a Java library providing efficient and extensible implementation of bigraphical reactive systems for both bigraphs and directed bigraphs.^[14]
BigraphER is a modelling and reasoning environment for bigraphs consisting of an OCaml library and a command-line tool providing an efficient implementation of rewriting, simulation, and visualisation for both bigraphs and bigraphs with sharing.^[15]

No longer actively developed:

BigMC is model checker for bigraphs which includes a command line interface and visualisation.^[16]
Big Red is a graphical editor for bigraphs with easily extensible support for various file formats.^[17]
SBAM is a stochastic simulator for bigraphs, aimed at simulation of biological models.^[18]
DBAM is a distributed simulator for bigraphical reactive systems.^[19]
DBtk is a toolkit for directed bigraphs that provides calculation of IPOs, matching, and visualisation.^[20]

Bibliography

Milner, Robin (2009). The Space and Motion of Communicating Agents. Cambridge University Press. ISBN 978-0521738330.
Milner, Robin (2001). "Bigraphical reactive systems, (invited paper)". CONCUR 2001 – Concurrency Theory, Proc. 12th International Conference. Lecture Notes in Computer Science. Vol. 2154. Springer-Verlag. pp. 16–35. doi:10.1007/3-540-44685-0_2.
Milner, Robin (2002). "Bigraphs as a Model for Mobile Interaction (invited paper)". ICGT 2002: First International Conference on Graph Transformation. Lecture Notes in Computer Science. Vol. 2505. Springer-Verlag. pp. 8–13. doi:10.1007/3-540-45832-8_3.
Debois, Søren; Damgaard, Troels Christoffer (2005). "Bigraphs by Example". IT University Technical Report Series TR-2005-61. Denmark: IT University of Copenhagen. CiteSeerX 10.1.1.73.176. ISBN 978-87-7949-090-1.
Sevegnani, Michele; Calder, Muffy (2015). "Bigraphs with sharing". Theoretical Computer Science. 577: 43–73. doi:10.1016/j.tcs.2015.02.011.

References

^ ^a ^b A Brief Introduction To Bigraphs, IT University of Copenhagen, Denmark.
^ ^a ^b Milner, Robin. The Bigraphical Model, University of Cambridge Computer Laboratory, UK.
^ Milner, Robin (2008). "Bigraphs and Their Algebra" (PDF). Electronic Notes in Theoretical Computer Science. 209: 5–19. doi:10.1016/j.entcs.2008.04.002.
^ Miculan, Marino; Peressotti, Marco (2013). Bigraphs reloaded: a presheaf presentation (PDF).
^ Milner, Robin (2009). "Bigraphical Categories". CONCUR 2009 - Concurrency Theory. Lecture Notes in Computer Science. Vol. 5710. Springer-Verlag. pp. 30–36. doi:10.1007/978-3-642-04081-8_3.
^ ^a ^b Burco, Fabio; Miculan, Marino; Peressotti, Marco (2020-03-30). "Towards a formal model for composable container systems". Proceedings of the 35th Annual ACM Symposium on Applied Computing. Brno Czech Republic: ACM: 173–175. doi:10.1145/3341105.3374121. ISBN 978-1-4503-6866-7.
^ Grohmann, Davide; Miculan, Marino (2007). "Directed Bigraphs". Electronic Notes in Theoretical Computer Science. 173: 121–137. doi:10.1016/j.entcs.2007.02.031.
^ Grohmann, Davide (2008), Ehrig, Hartmut; Heckel, Reiko; Rozenberg, Grzegorz; Taentzer, Gabriele (eds.), "Security, Cryptography and Directed Bigraphs", Graph Transformations, vol. 5214, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 487–489, doi:10.1007/978-3-540-87405-8_41, ISBN 978-3-540-87404-1, retrieved 2021-01-11
^ Grohmann, Davide; Miculan, Marino (2008-07-13). "Controlling resource access in Directed Bigraphs". Electronic Communications of the EASST: Volume 10: Graph Transformation and Visual Modeling Techniques 2008. doi:10.14279/TUJ.ECEASST.10.142.
^ Sevegnani, Michele; Calder, Muffy (2015). "Bigraphs with sharing". Theoretical Computer Science. 577: 43–73. doi:10.1016/j.tcs.2015.02.011.
^ Calder, Muffy; Sevegnani, Michele (2014). "Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing". Formal Aspects of Computing. 26 (3): 537–561. doi:10.1007/s00165-012-0270-3.
^ Calder, Muffy; Koliousis, Alexandros; Sevegnani, Michele; Sventek, Joseph (2014). "Real-time verification of wireless home networks using bigraphs with sharing". Science of Computer Programming. 80: 288–310. doi:10.1016/j.scico.2013.08.004.
^ Benford, Steve; Calder, Muffy; Rodden, Tom; Sevegnani, Michele (2016-05-01). "On Lions, Impala, and Bigraphs: Modelling Interactions in Physical/Virtual Spaces" (PDF). ACM Trans. Comput.-Hum. Interact. 23 (2): 9:1–9:56. doi:10.1145/2882784. ISSN 1073-0516.
^ Chiapperini, Alessio; Miculan, Marino; Peressotti, Marco (2020). Gadducci, Fabio; Kehrer, Timo (eds.). "Computing Embeddings of Directed Bigraphs". Graph Transformation. Lecture Notes in Computer Science. Cham: Springer International Publishing: 38–56. doi:10.1007/978-3-030-51372-6_3. ISBN 978-3-030-51372-6. PMC 7314702.{{cite journal}}: CS1 maint: PMC format (link)
^ Sevegnani, Michele; Calder, Muffy (2016-07-17). Chaudhuri, Swarat; Farzan, Azadeh (eds.). Computer Aided Verification (PDF). Lecture Notes in Computer Science. Springer International Publishing. pp. 494–501. doi:10.1007/978-3-319-41540-6_27. ISBN 9783319415390.
^ Perrone, Gian; Debois, Søren; Hildebrandt, Thomas T. (2012). "A model checker for Bigraphs". Proceedings of the 27th Annual ACM Symposium on Applied Computing - SAC '12. Trento, Italy: ACM Press: 1320. doi:10.1145/2245276.2231985. ISBN 978-1-4503-0857-1.
^ Faithfull, Alexander John; Perrone, Gian; Hildebrandt, Thomas T. (2013-06-25). "Big Red: A Development Environment for Bigraphs". Electronic Communications of the EASST: Volume 61: Graph Computation Models 2012. doi:10.14279/TUJ.ECEASST.61.835.
^ Krivine, Jean; Milner, Robin; Troina, Angelo (2008-10-22). "Stochastic Bigraphs". Electronic Notes in Theoretical Computer Science. Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV). 218: 73–96. doi:10.1016/j.entcs.2008.10.006. ISSN 1571-0661.
^ Mansutti, Alessio; Miculan, Marino; Peressotti, Marco (2015-09-06). "Distributed execution of bigraphical reactive systems". Electronic Communications of the EASST: Volume 71: Graph Computation Models 2014. doi:10.14279/TUJ.ECEASST.71.994.
^ Bacci, Giorgio; Grohmann, Davide; Miculan, Marino (2009), Kurz, Alexander; Lenisa, Marina; Tarlecki, Andrzej (eds.), "DBtk: A Toolkit for Directed Bigraphs", Algebra and Coalgebra in Computer Science, vol. 5728, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 413–422, doi:10.1007/978-3-642-03741-2_28, ISBN 978-3-642-03740-5, retrieved 2021-01-18

External links

Bibliography on Bigraphs

[intro-1] A Brief Introduction To Bigraphs, IT University of Copenhagen, Denmark.

[milner-2] Milner, Robin. The Bigraphical Model, University of Cambridge Computer Laboratory, UK.

[3] Milner, Robin (2008). "Bigraphs and Their Algebra" (PDF). Electronic Notes in Theoretical Computer Science. 209: 5–19. doi:10.1016/j.entcs.2008.04.002.

[4] Miculan, Marino; Peressotti, Marco (2013). Bigraphs reloaded: a presheaf presentation (PDF).

[5] Milner, Robin (2009). "Bigraphical Categories". CONCUR 2009 - Concurrency Theory. Lecture Notes in Computer Science. Vol. 5710. Springer-Verlag. pp. 30–36. doi:10.1007/978-3-642-04081-8_3.

[burco2020-6] Burco, Fabio; Miculan, Marino; Peressotti, Marco (2020-03-30). "Towards a formal model for composable container systems". Proceedings of the 35th Annual ACM Symposium on Applied Computing. Brno Czech Republic: ACM: 173–175. doi:10.1145/3341105.3374121. ISBN 978-1-4503-6866-7.

[7] Grohmann, Davide; Miculan, Marino (2007). "Directed Bigraphs". Electronic Notes in Theoretical Computer Science. 173: 121–137. doi:10.1016/j.entcs.2007.02.031.

[8] Grohmann, Davide (2008), Ehrig, Hartmut; Heckel, Reiko; Rozenberg, Grzegorz; Taentzer, Gabriele (eds.), "Security, Cryptography and Directed Bigraphs", Graph Transformations, vol. 5214, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 487–489, doi:10.1007/978-3-540-87405-8_41, ISBN 978-3-540-87404-1, retrieved 2021-01-11

[9] Grohmann, Davide; Miculan, Marino (2008-07-13). "Controlling resource access in Directed Bigraphs". Electronic Communications of the EASST: Volume 10: Graph Transformation and Visual Modeling Techniques 2008. doi:10.14279/TUJ.ECEASST.10.142.

[10] Sevegnani, Michele; Calder, Muffy (2015). "Bigraphs with sharing". Theoretical Computer Science. 577: 43–73. doi:10.1016/j.tcs.2015.02.011.

[11] Calder, Muffy; Sevegnani, Michele (2014). "Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing". Formal Aspects of Computing. 26 (3): 537–561. doi:10.1007/s00165-012-0270-3.

[12] Calder, Muffy; Koliousis, Alexandros; Sevegnani, Michele; Sventek, Joseph (2014). "Real-time verification of wireless home networks using bigraphs with sharing". Science of Computer Programming. 80: 288–310. doi:10.1016/j.scico.2013.08.004.

[13] Benford, Steve; Calder, Muffy; Rodden, Tom; Sevegnani, Michele (2016-05-01). "On Lions, Impala, and Bigraphs: Modelling Interactions in Physical/Virtual Spaces" (PDF). ACM Trans. Comput.-Hum. Interact. 23 (2): 9:1–9:56. doi:10.1145/2882784. ISSN 1073-0516.

[14] Chiapperini, Alessio; Miculan, Marino; Peressotti, Marco (2020). Gadducci, Fabio; Kehrer, Timo (eds.). "Computing Embeddings of Directed Bigraphs". Graph Transformation. Lecture Notes in Computer Science. Cham: Springer International Publishing: 38–56. doi:10.1007/978-3-030-51372-6_3. ISBN 978-3-030-51372-6. PMC 7314702.{{cite journal}}: CS1 maint: PMC format (link)

[15] Sevegnani, Michele; Calder, Muffy (2016-07-17). Chaudhuri, Swarat; Farzan, Azadeh (eds.). Computer Aided Verification (PDF). Lecture Notes in Computer Science. Springer International Publishing. pp. 494–501. doi:10.1007/978-3-319-41540-6_27. ISBN 9783319415390.

[16] Perrone, Gian; Debois, Søren; Hildebrandt, Thomas T. (2012). "A model checker for Bigraphs". Proceedings of the 27th Annual ACM Symposium on Applied Computing - SAC '12. Trento, Italy: ACM Press: 1320. doi:10.1145/2245276.2231985. ISBN 978-1-4503-0857-1.

[17] Faithfull, Alexander John; Perrone, Gian; Hildebrandt, Thomas T. (2013-06-25). "Big Red: A Development Environment for Bigraphs". Electronic Communications of the EASST: Volume 61: Graph Computation Models 2012. doi:10.14279/TUJ.ECEASST.61.835.

[18] Krivine, Jean; Milner, Robin; Troina, Angelo (2008-10-22). "Stochastic Bigraphs". Electronic Notes in Theoretical Computer Science. Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV). 218: 73–96. doi:10.1016/j.entcs.2008.10.006. ISSN 1571-0661.

[19] Mansutti, Alessio; Miculan, Marino; Peressotti, Marco (2015-09-06). "Distributed execution of bigraphical reactive systems". Electronic Communications of the EASST: Volume 71: Graph Computation Models 2014. doi:10.14279/TUJ.ECEASST.71.994.

[20] Bacci, Giorgio; Grohmann, Davide; Miculan, Marino (2009), Kurz, Alexander; Lenisa, Marina; Tarlecki, Andrzej (eds.), "DBtk: A Toolkit for Directed Bigraphs", Algebra and Coalgebra in Computer Science, vol. 5728, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 413–422, doi:10.1007/978-3-642-03741-2_28, ISBN 978-3-642-03740-5, retrieved 2021-01-18

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

@@ Line 93: / Line 93: @@
-== Implementations ==
+== Tools and Implementations ==
-* [http://www.dcs.gla.ac.uk/~michele/bigrapher.html BigraphER] is a modelling and reasoning environment for bigraphs consisting of an [[OCaml]] library and a command-line tool providing an efficient implementation of rewriting, simulation, and visualisation for both bigraphs and bigraphs with sharing.<ref>{{Cite book|title=Computer Aided Verification|last=Sevegnani|first=Michele|last2=Calder|first2=Muffy|date=2016-07-17|publisher=Springer International Publishing|isbn=9783319415390|editor-last=Chaudhuri|editor-first=Swarat|series=Lecture Notes in Computer Science|pages=494–501|language=en|doi=10.1007/978-3-319-41540-6_27|editor-last2=Farzan|editor-first2=Azadeh|url = http://eprints.gla.ac.uk/119384/13/119384.pdf}}</ref>
+* '''[https://bigraphs.github.io/jlibbig/ jLibBig]''' is a [[Java]] library providing efficient and extensible implementation of bigraphical reactive systems for both bigraphs and directed bigraphs.<ref>{{Cite journal|last=Chiapperini|first=Alessio|last2=Miculan|first2=Marino|last3=Peressotti|first3=Marco|date=2020|editor-last=Gadducci|editor-first=Fabio|editor2-last=Kehrer|editor2-first=Timo|title=Computing Embeddings of Directed Bigraphs|url=https://link.springer.com/chapter/10.1007%2F978-3-030-51372-6_3|journal=Graph Transformation|series=Lecture Notes in Computer Science|language=en|location=Cham|publisher=Springer International Publishing|pages=38–56|doi=10.1007/978-3-030-51372-6_3|isbn=978-3-030-51372-6|pmc=PMC7314702}}</ref>
+* '''[http://www.dcs.gla.ac.uk/~michele/bigrapher.html BigraphER]''' is a modelling and reasoning environment for bigraphs consisting of an [[OCaml]] library and a command-line tool providing an efficient implementation of rewriting, simulation, and visualisation for both bigraphs and bigraphs with sharing.<ref>{{Cite book|title=Computer Aided Verification|last=Sevegnani|first=Michele|last2=Calder|first2=Muffy|date=2016-07-17|publisher=Springer International Publishing|isbn=9783319415390|editor-last=Chaudhuri|editor-first=Swarat|series=Lecture Notes in Computer Science|pages=494–501|language=en|doi=10.1007/978-3-319-41540-6_27|editor-last2=Farzan|editor-first2=Azadeh|url = http://eprints.gla.ac.uk/119384/13/119384.pdf}}</ref>
+No longer actively developed:
+* '''[http://bigraph.org/bigmc/ BigMC]''' is [[model checker]] for bigraphs which includes a command line interface and visualisation.<ref>{{Cite journal|last=Perrone|first=Gian|last2=Debois|first2=Søren|last3=Hildebrandt|first3=Thomas T.|date=2012|title=A model checker for Bigraphs|url=http://dl.acm.org/citation.cfm?doid=2245276.2231985|journal=Proceedings of the 27th Annual ACM Symposium on Applied Computing - SAC '12|language=en|location=Trento, Italy|publisher=ACM Press|pages=1320|doi=10.1145/2245276.2231985|isbn=978-1-4503-0857-1}}</ref>
+* '''[http://bigraph.org/big-red Big Red]''' is a graphical editor for bigraphs with easily extensible support for various file formats.<ref>{{Cite journal|last=Faithfull|first=Alexander John|last2=Perrone|first2=Gian|last3=Hildebrandt|first3=Thomas T.|date=2013-06-25|title=Big Red: A Development Environment for Bigraphs|url=http://journal.ub.tu-berlin.de/eceasst/article/view/835|journal=Electronic Communications of the EASST|language=en|pages=Volume 61: Graph Computation Models 2012|doi=10.14279/TUJ.ECEASST.61.835}}</ref>
+* '''SBAM''' is a stochastic simulator for bigraphs, aimed at simulation of biological models.<ref>{{Cite journal|last=Krivine|first=Jean|last2=Milner|first2=Robin|last3=Troina|first3=Angelo|date=2008-10-22|title=Stochastic Bigraphs|url=http://www.sciencedirect.com/science/article/pii/S1571066108004003|journal=Electronic Notes in Theoretical Computer Science|series=Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV)|language=en|volume=218|pages=73–96|doi=10.1016/j.entcs.2008.10.006|issn=1571-0661}}</ref>
+* '''DBAM''' is a distributed simulator for bigraphical reactive systems.<ref>{{Cite journal|last=Mansutti|first=Alessio|last2=Miculan|first2=Marino|last3=Peressotti|first3=Marco|date=2015-09-06|title=Distributed execution of bigraphical reactive systems|url=http://journal.ub.tu-berlin.de/eceasst/article/view/994|journal=Electronic Communications of the EASST|language=en|pages=Volume 71: Graph Computation Models 2014|doi=10.14279/TUJ.ECEASST.71.994}}</ref>
+* '''DBtk''' is a toolkit for directed bigraphs that provides calculation of IPOs, matching, and visualisation.<ref>{{Citation|last=Bacci|first=Giorgio|title=DBtk: A Toolkit for Directed Bigraphs|date=2009|url=http://link.springer.com/10.1007/978-3-642-03741-2_28|work=Algebra and Coalgebra in Computer Science|volume=5728|pages=413–422|editor-last=Kurz|editor-first=Alexander|place=Berlin, Heidelberg|publisher=Springer Berlin Heidelberg|doi=10.1007/978-3-642-03741-2_28|isbn=978-3-642-03740-5|access-date=2021-01-18|last2=Grohmann|first2=Davide|last3=Miculan|first3=Marino|editor2-last=Lenisa|editor2-first=Marina|editor3-last=Tarlecki|editor3-first=Andrzej}}</ref>
 ==See also==