jLibBig

A Java library for Bigraphs and Bigraphical Reactive Systems.

repository

Description

Bigraphs and Bigraphical Reactive Systems are a modern, graphical calculus for the description of the syntax and semantics of systems in terms of the orthogonal notions of connectivity and locality. Since they introduction by Robin Milner, bigraphs have been successfully applied to model complex, concurrent, context-​dependent, or ubiquitous systems in a variety of fields beyond computer science like biology and databases.

Papers

Chiapperini, A., Miculan, M. and Peressotti, M. 2020. Computing Embeddings of Directed Bigraphs. Graph Transformation - 13th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25-26, 2020, Proceedings (2020), 38–56.
Directed bigraphs are a meta-model which generalises Milner’s bigraphs by taking into account the request flow between controls and names. A key problem about these bigraphs is that of bigraph embedding, i.e., finding the embeddings of a bigraph inside a larger one. We present an algorithm for computing embeddings of directed bigraphs, via a reduction to a constraint satisfaction problem. We prove soundness and completeness of this algorithm, and provide an implementation in jLibBig, a general Java library for manipulating bigraphical reactive systems, together with some experimental results.
@inproceedings{CMP20,
  author = {Chiapperini, Alessio and Miculan, Marino and Peressotti, Marco},
  editor = {Gadducci, Fabio and Kehrer, Timo},
  title = {Computing Embeddings of Directed Bigraphs},
  booktitle = {Graph Transformation - 13th International Conference, {ICGT} 2020, Held as Part of {STAF} 2020, Bergen, Norway, June 25-26, 2020, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {12150},
  pages = {38--56},
  publisher = {Springer},
  year = {2020},
  url = {https://doi.org/10.1007/978-3-030-51372-6\_3},
  doi = {10.1007/978-3-030-51372-6\_3}
}
Burco, F., Miculan, M. and Peressotti, M. 2020. Towards a Formal Model for Composable Container Systems. Proceedings of the 35rd Annual ACM Symposium on Applied Computing, SAC 2020, Brno, Czech Republic, March 29-April 03, 2020 (2020), 173–175.
In modern cloud-based architectures, containers play a central role: they provide powerful isolation mechanisms such that developers can focus on the logic and dependencies of applications while system administrators can focus on deployment and management issue. In this work, we propose a formal model for container-based systems, using the framework of Bigraphical Reactive Systems (BRSs). We first introduce local directed bigraphs, a graph-based formalism which allows us to deal with localized resources. Then, we define a signature for modelling containers and provide some examples of bigraphs modelling containers. These graphs can be analysed and manipulated using techniques from graph theory: properties about containers can be formalized as properties of the corresponding bigraphic representations. Moreover, it turns out that the composition of containers as performed by e.g. docker-compose, corresponds precisely to the composition of the corresponding bigraphs inside an “environment bigraph” which in turn is obtained directly from the YAML file used to define the composition of containers.
@inproceedings{BMP20,
  author = {Burco, Fabio and Miculan, Marino and Peressotti, Marco},
  title = {Towards a Formal Model for Composable Container Systems},
  booktitle = {Proceedings of the 35rd Annual {ACM} Symposium on Applied Computing, {SAC} 2020, Brno, Czech Republic, March 29-April 03, 2020},
  pages = {173--175},
  publisher = {{ACM}},
  year = {2020},
  url = {https://doi.org/10.1145/3341105.3374121},
  doi = {10.1145/3341105.3374121}
}
Mansutti, A., Miculan, M. and Peressotti, M. 2014. Distributed execution of bigraphical reactive systems. Electronic Communications of the EASST. 71, (2014). DOI:10.14279/tuj.eceasst.71.994.
The bigraph embedding problem is crucial for many results and tools about bigraphs and bigraphical reactive systems (BRS). Current algorithms for computing bigraphical embeddings are centralized, i.e. designed to run locally with a complete view of the guest and host bigraphs. In order to deal with large bigraphs, and to parallelize reactions, we present a decentralized algorithm, which distributes both state and computation over several concurrent processes. This allows for distributed, parallel simulations where non-interfering reactions can be carried out concurrently; nevertheless, even in the worst case the complexity of this distributed algorithm is no worse than that of a centralized algorithm.
@article{MMP14,
  author = {Mansutti, Alessio and Miculan, Marino and Peressotti, Marco},
  title = {Distributed execution of bigraphical reactive systems},
  journal = {{Electronic Communications of the EASST}},
  volume = {71},
  year = {2014},
  url = {https://doi.org/10.14279/tuj.eceasst.71.994},
  doi = {10.14279/tuj.eceasst.71.994}
}
Miculan, M. and Peressotti, M. 2014. A CSP implementation of the bigraph embedding problem. CoRR. abs/1412.1042, (2014).
A crucial problem for many results and tools about bigraphs and bigraphical reactive systems is bigraph embedding. An embedding is more informative than a bigraph matching, since it keeps track of the correspondence between the various components of the redex (guest) within the agent (host). In this paper, we present an algorithm for computing embeddings based on a reduction to a constraint satisfaction problem. This algorithm, that we prove to be sound and complete, has been successfully implemented in LibBig, a library for manipulating bigraphical reactive systems. This library can be used for implementing a wide range of tools, and it can be adapted to various extensions of bigraphs.
@article{abs-1412-1042,
  author = {Miculan, Marino and Peressotti, Marco},
  title = {A {CSP} implementation of the bigraph embedding problem},
  journal = {CoRR},
  volume = {abs/1412.1042},
  year = {2014},
  url = {http://arxiv.org/abs/1412.1042},
  archiveprefix = {arXiv},
  eprint = {1412.1042}
}