Marco Peressotti

Publications

My publications are also listed on my DBLP and Google Scholar profiles.

Journal Articles 6

Conference Proceedings 16

Workshop Proceedings 5

Editorship 1

Informal Publications 9

2021

C16

Montesi, F., Peressotti, M. and Picotti, V. 2021. Sliceable Monolith: Monolith First, Microservices Later. 2021 IEEE International Conference on Services Computing, SCC 2021, Online, September 5-10, 2021 (2021).

AbstractBibtexReport

We propose Sliceable Monolith, a new methodology for developing microservice architectures and perform their integration testing by leveraging most of the simplicity of a monolith: a single codebase and a local execution environment that simulates distribution. Then, a tool compiles a codebase for each microservice and a cloud deployment configuration. The key enabler of our approach is the technology-agnostic service definition language offered by Jolie.

@inproceedings{MPP21,
  author = {Montesi, Fabrizio and Peressotti, Marco and Picotti, Valentino},
  title = {Sliceable Monolith: Monolith First, Microservices Later},
  editor = {},
  booktitle = {2021 {IEEE} International Conference on Services Computing, {SCC}
                 2021, Online, September 5-10, 2021},
  pages = {},
  publisher = {{IEEE}},
  year = {2021},
  pubstate = {forthcoming}
}

C15

Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2021. Certifying Choreography Compilation. Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, September 6-10, 2021, Proceedings. (2021).

AbstractBibtexReport Coq Sources

Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a non-trivial choreographic language supporting recursion.

@article{CMPb,
  author = {Cruz{-}Filipe, Lu{\'{\i}}s and Montesi, Fabrizio and Peressotti, Marco},
  title = {Certifying Choreography Compilation},
  booktitle = {Theoretical Aspects of Computing - {ICTAC} 2021 - 18th International Colloquium, September 6-10, 2021, Proceedings},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  year = {2021},
  pubstate = {forthcoming}
}

C14

Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2021. Formalising a Turing-Complete Choreographic Language in Coq. 12th International Conference on Interactive Theorem Proving (ITP 2021) (Dagstuhl, Germany, 2021), 15:1–15:18.

AbstractBibtexElectronic edition DOI Report Coq Sources

Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our development includes formalising the choreographic language and its basic properties, Kleene’s theory of partial recursive functions, the encoding of these functions as choreographies, and proving this encoding correct. With this effort, we show that theorem proving can be a very useful tool in the field of choreographic languages: besides the added degree of confidence that we get from a mechanised proof, the formalisation process led us to a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.

@inproceedings{CMP21,
  author = {Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio and Peressotti, Marco},
  title = {{Formalising a Turing-Complete Choreographic Language in Coq}},
  booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages = {15:1--15:18},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-188-7},
  issn = {1868-8969},
  year = {2021},
  volume = {193},
  editor = {Cohen, Liron and Kaliszyk, Cezary},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/13910},
  urn = {urn:nbn:de:0030-drops-139109},
  doi = {10.4230/LIPIcs.ITP.2021.15}
}

C13

Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G. and Weisenburger, P. 2021. Multiparty Languages: The Choreographic and Multitier Cases. 35th European Conference on Object-Oriented Programming (ECOOP 2021) (Dagstuhl, Germany, 2021), 22:1–22:27.

AbstractBibtexElectronic edition DOI Distinguished Paper

Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings—respectively process calculi and lambda calculus—the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long. In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.

@inproceedings{GMPRSW21,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Richter, David and Salvaneschi, Guido and Weisenburger, Pascal},
  title = {{Multiparty Languages: The Choreographic and Multitier Cases}},
  booktitle = {35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages = {22:1--22:27},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-190-0},
  issn = {1868-8969},
  year = {2021},
  volume = {194},
  editor = {M{\o}ller, Anders and Sridharan, Manu},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/14065},
  urn = {urn:nbn:de:0030-drops-140658},
  doi = {10.4230/LIPIcs.ECOOP.2021.22}
}

C12

Giallorenzo, S., Montesi, F., Peressotti, M., Rademacher, F. and Sachweh, S. 2021. Jolie and LEMMA: Model-Driven Engineering and Programming Languages Meet on Microservices. Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings (2021), 276–284.

AbstractBibtexElectronic edition DOI Report

In the field of microservices, Model-Driven Engineering has emerged as a powerful methodology for architectural design, and new programming languages have introduced language abstractions to deal with microservice development more effectively. In this article, we present the first preliminary investigation of how the two approaches can be married, taking the LEMMA framework and the Jolie programming language as respective representatives. By developing a conceptual metamodel for Jolie, we elicit a strong link between the two approaches, which shows that there is much to gain. We discuss a few low-hanging fruits that come from our finding and present some interesting future directions that arise from our new viewpoint.

@inproceedings{GMPRS21,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  editor = {Damiani, Ferruccio and Dardha, Ornela},
  title = {Jolie and {LEMMA:} Model-Driven Engineering and Programming Languages
                 Meet on Microservices},
  booktitle = {Coordination Models and Languages - 23rd {IFIP} {WG} 6.1 International
                 Conference, {COORDINATION} 2021, Held as Part of the 16th International
                 Federated Conference on Distributed Computing Techniques, DisCoTec
                 2021, Valletta, Malta, June 14-18, 2021, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {12717},
  pages = {276--284},
  publisher = {Springer},
  year = {2021},
  url = {https://doi.org/10.1007/978-3-030-78142-2\_17},
  doi = {10.1007/978-3-030-78142-2\_17}
}

Montesi, F. and Peressotti, M. 2021. Linear Logic, the π-calculus, and their Metatheory: A Recipe for Proofs as Processes. CoRR. abs/2106.11818, (2021).

AbstractBibtexElectronic edition

Initiated by Abramsky [1994], the Proofs as Processes agenda is to establish a solid foundation for the study of concurrent languages, by researching the connection between linear logic and the π-calculus. To date, Proofs as Processes is still a partial success. Caires and Pfenning [2010] showed that linear propositions correspond to session types, which prescribe the observable behaviour of processes. Further, Carbone et al. [2018] demonstrated that adopting devices from hypersequents [Avron 1991] shapes proofs such that they correspond to the expected syntactic structure of processes in the π-calculus. What remains is reconstructing the expected metatheory of session types and the π-calculus. In particular, the hallmark of session types, session fidelity, still has to be reconstructed: a correspondence between the observable behaviours of processes and their session types, in terms of labelled transitions. In this article, we present πLL, a new process calculus rooted in linear logic. The key novelty of πLL is that it comes with a carefully formulated design recipe, based on a dialgebraic view of labelled transition systems. Thanks to our recipe, πLL offers the expected transition systems of session types, which we use to establish session fidelity. We use πLL to carry out the first thorough investigation of the metatheoretical properties enforced by linear logic on the observable behaviour of processes, uncovering connections with similarity and bisimilarity. We also prove that πLL and our recipe form a robust basis for the further exploration of Proofs as Processes, by considering different features: polymorphism, process mobility, and recursion.

@article{abs-2106-11818,
  author = {Montesi, Fabrizio and Peressotti, Marco},
  title = {Linear Logic, the π-calculus, and their Metatheory: A Recipe for Proofs as Processes},
  journal = {CoRR},
  volume = {abs/2106.11818},
  year = {2021},
  url = {https://arxiv.org/abs/2106.11818},
  archiveprefix = {arXiv},
  eprint = {2106.11818}
}

2020

C11

Miculan, M. and Peressotti, M. 2020. Software Transactional Memory with Interactions. Proceedings of the 21st Italian Conference on Theoretical Computer Science, Ischia, Italy, September 14-16, 2020 (2020), 67–80.

AbstractBibtexElectronic edition Report

Software Transactional memory (STM) is an emerging abstraction for concurrent programming alternative to lock-based synchronizations. Most STM models admit only isolated transactions, which are not adequate in multithreaded programming where transactions need to interact via shared data before committing. To overcome this limitation, in this paper we present Open Transactional Memory (OTM), a programming abstraction supporting safe, data-driven interactions between composable memory transactions. This is achieved by relaxing isolation between transactions, still ensuring atomicity. This model allows for loosely-coupled interactions since transaction merging is driven only by accesses to shared data, with no need to specify participants beforehand.

@inproceedings{MP20,
  author = {Miculan, Marino and Peressotti, Marco},
  editor = {Cordasco, Gennaro and Gargano, Luisa and Rescigno, Adele A.},
  title = {Software Transactional Memory with Interactions},
  booktitle = {Proceedings of the 21st Italian Conference on Theoretical Computer
                 Science, Ischia, Italy, September 14-16, 2020},
  series = {{CEUR} Workshop Proceedings},
  volume = {2756},
  pages = {67--80},
  publisher = {CEUR-WS.org},
  year = {2020},
  url = {http://ceur-ws.org/Vol-2756/paper\_7.pdf}
}

C10

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.

AbstractBibtexElectronic edition DOI Report Tool

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.

AbstractBibtexElectronic edition DOI Report

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}
}

Andersen, J.L., Hellmuth, M., Merkle, D., Nøjgaard, N. and Peressotti, M. 2020. A Graph-Based Tool to Embed the π-Calculus into a Computational DPO Framework. Proceedings of the SOFSEM 2020 Student Research Forum co-located with the 46th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2020) (2020), 121–132.

AbstractBibtexElectronic edition Report Tool

Graph transformation approaches have been successfully used to analyse and design chemical and biological systems. Here we build on top of a DPO framework, in which molecules are modelled as typed attributed graphs and chemical reactions are modelled as graph transformations. Edges and vertexes can be labelled with first-order terms, which can be used to encode, e.g., steric information of molecules. While targeted to chemical settings, the computational framework is intended to be very generic and applicable to the exploration of arbitrary spaces derived via iterative application of rewrite rules, such as process calculi like Milner’s π-calculus. To illustrate the generality of the framework, we introduce EpiM: a tool for computing execution spaces of π-calculus processes. EpiM encodes π-calculus processes as typed attributed graphs and then exploits the existing DPO framework to compute their dynamics in the form of graphs where nodes are π-calculus processes and edges are reduction steps. EpiM takes advantage of the graph-based representation and facilities offered by the framework, like efficient isomorphism checking to prune the space without resorting to explicit structural equivalences. EpiM is available as an online Python-based tool.

@inproceedings{AHMKP20,
  author = {Andersen, Jakob Lykke and Hellmuth, Marc and Merkle, Daniel and N{\o}jgaard, Nikolai and Peressotti, Marco},
  title = {A Graph-Based Tool to Embed the π-Calculus into a Computational {DPO} Framework},
  year = {2020},
  editor = {Manolopoulos, Yannis and Papadopoulos, George Α. and Tzouramanis, Theodoros},
  booktitle = {Proceedings of the SOFSEM 2020 Student Research Forum co-located with the 46th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2020)},
  volume = {2568},
  pages = {121-132},
  publisher = {CEUR-WS.org},
  url = {http://ceur-ws.org/Vol-2568/paper11.pdf}
}

Cruz-Filipe Luı́s, Giallorenzo, S., Montesi, F., Peressotti, M., Rademacher, F. and Sachweh, S. eds. 2020. Joint Post-proceedings of the First and Second International Conference on Microservices, Microservices 2017/2019, October 23-27, 2017, Odense, Denmark / February 19-21, 2019, Dortmund, Germany. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

BibtexElectronic edition

@proceedings{CGMPRS20,
  editor = {Cruz{-}Filipe, Lu{\'{\i}}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  title = {Joint Post-proceedings of the First and Second International Conference on Microservices, Microservices 2017/2019, October 23-27, 2017, Odense, Denmark / February 19-21, 2019, Dortmund, Germany},
  series = {OASIcs},
  volume = {78},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year = {2020},
  isbn = {978-3-95977-137-5},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/11822/}
}

Giallorenzo, S., Montesi, F. and Peressotti, M. 2020. Choreographies as Objects. CoRR. abs/22005.09520, (2020).

AbstractBibtexElectronic edition Tool

We present Choral, the first framework for programming choreographies (multiparty protocols) that builds on top of mainstream programming abstractions: in Choral, choreographies are objects. Given a choreography that defines interactions among some roles (Alice, Bob, etc.), an implementation for each role in the choreography is automatically generated by a compiler. These implementations are libraries in pure Java, which developers can modularly compose in their own programs to participate correctly in choreographies.

@article{abs-2005-09520,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco},
  title = {Choreographies as Objects},
  journal = {CoRR},
  volume = {abs/22005.09520},
  year = {2020},
  url = {http://arxiv.org/abs/2005.09520},
  archiveprefix = {arXiv},
  eprint = {2005.09520}
}

2019

Brengos, T. and Peressotti, M. 2019. Behavioural equivalences for timed systems. Logical Methods in Computer Science. 15, 1 (2019). DOI:10.23638/LMCS-15(1:17)2019.

AbstractBibtexElectronic edition DOI

Timed transition systems are behavioural models that include an explicit treatment of time flow and are used to formalise the semantics of several foundational process calculi and automata. Despite their relevance, a general mathematical characterisation of timed transition systems and their behavioural theory is still missing. We introduce the first uniform framework for timed behavioural models that encompasses known behavioural equivalences such as timed bisimulations, timed language equivalences as well as their weak and time-abstract counterparts. All these notions of equivalences are naturally organised by their discriminating power in a spectrum. We prove that this result does not depend on the type of the systems under scrutiny: it holds for any generalisation of timed transition system. We instantiate our framework to timed transition systems and their quantitative extensions such as timed probabilistic systems.

@article{BP19,
  author = {Brengos, Tomasz and Peressotti, Marco},
  title = {Behavioural equivalences for timed systems},
  journal = {Logical Methods in Computer Science},
  volume = {15},
  number = {1},
  year = {2019},
  url = {https://doi.org/10.23638/LMCS-15(1:17)2019},
  doi = {10.23638/LMCS-15(1:17)2019}
}

Kokke, W., Montesi, F. and Peressotti, M. 2019. Better late than never: a fully-abstract semantics for classical processes. PACMPL. 3, POPL (2019), 24:1–24:29. DOI:10.1145/3290337.

AbstractBibtexElectronic edition DOI Report Slides Presentation

We present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by ⊗ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini’s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.

@article{KMP19,
  author = {Kokke, Wen and Montesi, Fabrizio and Peressotti, Marco},
  title = {Better late than never: a fully-abstract semantics for classical processes},
  journal = {{PACMPL}},
  volume = {3},
  number = {{POPL}},
  pages = {24:1--24:29},
  year = {2019},
  url = {https://doi.org/10.1145/3290337},
  doi = {10.1145/3290337}
}

Gabbrielli, M., Giallorenzo, S., Lanese, I., Montesi, F., Peressotti, M. and Zingaro, S.P. 2019. No More, No Less - A Formal Model for Serverless Computing. Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, 2019, Proceedings (2019), 148–157.

AbstractBibtexElectronic edition DOI Report Slides

Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. The infrastructure takes care of executing the functions whenever requested by remote clients, dealing automatically with distribution and scaling with respect to inbound traffic. While vendors already support a variety of programming languages for serverless computing (e.g. Go, Java, Javascript, Python), as far as we know there is no reference model yet to formally reason on this paradigm. In this paper, we propose the first core formal programming model for serverless computing, which combines ideas from both the λ-calculus (for functions) and the π-calculus (for communication). To illustrate our proposal, we model a real-world serverless system. Thanks to our model, we capture limitations of current vendors and formalise possible amendments.

@inproceedings{GGLMPZ19,
  author = {Gabbrielli, Maurizio and Giallorenzo, Saverio and Lanese, Ivan and Montesi, Fabrizio and Peressotti, Marco and Zingaro, Stefano Pio},
  title = {No More, No Less - {A} Formal Model for Serverless Computing},
  booktitle = {Coordination Models and Languages - 21st {IFIP} {WG} 6.1 International Conference, {COORDINATION} 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, 2019, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {11533},
  pages = {148--157},
  publisher = {Springer},
  year = {2019},
  url = {https://doi.org/10.1007/978-3-030-22397-7\_9},
  doi = {10.1007/978-3-030-22397-7\_9}
}

Brengos, T. and Peressotti, M. 2019. Two modes of recognition: algebra, coalgebra, and languages. CoRR. abs/1906.05573, (2019).

AbstractBibtexElectronic edition

The aim of the paper is to build a connection between two approaches towards categorical language theory: the coalgebraic and algebraic language theory for monads. For a pair of monads modelling the branching and the linear type we defined regular maps that generalize regular languages known in classical non-deterministic automata theory. These maps are behaviours of certain automata (i.e. they possess a coalgebraic nature), yet they arise from Eilenberg-Moore algebras and their homomorphisms (by exploiting duality between the category of Eilenberg-Moore algebras and saturated coalgebras). Given some additional assumptions, we show that regular maps form a certain subcategory of the Kleisli category for the monad which is the composition of the branching and linear type. Moreover, we state a Kleene-like theorem characterising the regular morphisms category in terms of the smallest subcategory closed under certain operations. Additionally, whenever the branching type monad is taken to be the powerset monad, we show that regular maps are described as maps recognized by certain functors whose codomains are categories with all finite hom-sets. We instantiate our framework on classical non-deterministic automata, tree automata, fuzzy automata and weighted automata.

@article{abs-1906-05573,
  author = {Brengos, Tomasz and Peressotti, Marco},
  title = {Two modes of recognition: algebra, coalgebra, and languages},
  journal = {CoRR},
  volume = {abs/1906.05573},
  year = {2019},
  url = {http://arxiv.org/abs/1906.05573},
  archiveprefix = {arXiv},
  eprint = {1906.05573}
}

2018

Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2018. Communications in choreographies, revisited. Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018 (2018), 1248–1255.

AbstractBibtexElectronic edition DOI Report

Choreographic Programming is a paradigm for developing correct-by-construction concurrent programs, by writing high-level descriptions of the desired communications and then synthesising process implementations automatically. So far, choreographic programming has been explored in the monadic setting: interaction terms express point-to-point communications of a single value. However, real-world systems often rely on interactions of polyadic nature, where multiple values are communicated among two or more parties, like multicast, scatter-gather, and atomic exchanges.
We introduce a new model for choreographic programming equipped with a primitive for grouped interactions that subsumes all the above scenarios. Intuitively, grouped interactions can be thought of as being carried out as one single interaction. In practice, they are implemented by processes that carry them out in a concurrent fashion. After formalising the intuitive semantics of grouped interactions, we prove that choreographic programs and their implementations are correct and deadlock-free by construction.

@inproceedings{CMP18,
  author = {Cruz{-}Filipe, Lu{\'{\i}}s and Montesi, Fabrizio and Peressotti, Marco},
  title = {Communications in choreographies, revisited},
  booktitle = {Proceedings of the 33rd Annual {ACM} Symposium on Applied Computing, {SAC} 2018, Pau, France, April 09-13, 2018},
  pages = {1248--1255},
  publisher = {{ACM}},
  year = {2018},
  url = {https://doi.org/10.1145/3167132.3167267},
  doi = {10.1145/3167132.3167267}
}

Kokke, W., Montesi, F. and Peressotti, M. 2018. Taking Linear Logic Apart. Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018. (2018), 90–103.

AbstractBibtexElectronic edition DOI Erratum

Process calculi based on logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the π-calculus: the fundamental operator for parallel composition does not correspond to any rule of linear logic. Kokke et al. (2019) introduced Hypersequent Classical Processes (HCP), which addresses this mismatch using hypersequents (collections of sequents) to register parallelism in the typing judgements. However, the step from CP to HCP is a big one. As of yet, HCP does not have reduction semantics, and the addition of delayed actions means that CP processes interpreted as HCP processes do not behave as they would in CP. We introduce HCP-, a variant of HCP with reduction semantics and without delayed actions. We prove progress, preservation, and termination, and show that HCP- supports the same communication protocols as CP.

@inproceedings{KMP18,
  author = {Kokke, Wen and Montesi, Fabrizio and Peressotti, Marco},
  title = {Taking Linear Logic Apart},
  year = {2018},
  editor = {Ehrhard, Thomas and Fern{\'{a}}ndez, Maribel and de Paiva, Valeria and de Falco, Lorenzo Tortora},
  booktitle = {Proceedings Joint International Workshop on Linearity {\&} Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018.},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {292},
  publisher = {Open Publishing Association},
  pages = {90--103},
  doi = {10.4204/EPTCS.292.5},
  url = {https://doi.org/10.4204/EPTCS.292.5}
}

Montesi, F. and Peressotti, M. 2018. Classical Transitions. CoRR. abs/1803.01049, (2018).

AbstractBibtexElectronic edition

We introduce the calculus of Classical Transitions (CT), which extends the research line on the relationship between linear logic and processes to labelled transitions. The key twist from previous work is registering parallelism in typing judgements, by generalising linear logic judgements from one sequents to many (hypersequents). This allows us to bridge the gap between the structures of operators used as proof terms in previous work and those of the standard π-calculus (in particular parallel operator and restriction). The proof theory of CT allows for new proof transformations, which we show correspond to a labelled transition system (LTS) for processes. We prove that CT enjoys subject reduction and progress.

@article{abs-1803-01049,
  author = {Montesi, Fabrizio and Peressotti, Marco},
  title = {Classical Transitions},
  journal = {CoRR},
  volume = {abs/1803.01049},
  year = {2018},
  url = {http://arxiv.org/abs/1803.01049},
  archiveprefix = {arXiv},
  eprint = {1803.01049}
}

2017

Miculan, M. and Peressotti, M. 2017. Deciding weak weighted bisimulation. Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 IEEE International Workshop on Measurements and Networking (2017 IEEE M&N), Naples, Italy, September 26-28, 2017. (2017), 126–137.

AbstractBibtexElectronic edition

Weighted labelled transition systems are LTSs whose transitions are given weights drawn from a commutative monoid, subsuming a wide range of systems with quantitative aspects. In this paper we extend this theory towards other behavioural equivalences, by considering semirings of weights. Taking advantage of this extra structure, we consider a general notion of weak weighted bisimulation, which coincides with the usual weak bisimulations in the cases of non-deterministic and fully-probabilistic systems. We present a general algorithm for deciding weak weighted bisimulation. The procedure relies on certain systems of linear equations over the semiring of weights hence it can be readily instantiated to a wide range of models. We prove that these systems admit a unique solution for ω-continuous semirings

@inproceedings{MP17,
  author = {Miculan, Marino and Peressotti, Marco},
  editor = {Monica, Dario Della and Murano, Aniello and Rubin, Sasha and Sauro, Luigi},
  title = {Deciding weak weighted bisimulation},
  booktitle = {Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 {IEEE} International Workshop on Measurements and Networking {(2017} {IEEE} M{\&}N), Naples, Italy, September 26-28, 2017.},
  volume = {1949},
  pages = {126--137},
  publisher = {CEUR-WS.org},
  year = {2017},
  url = {http://ceur-ws.org/Vol-1720/full7.pdf}
}

Mansutti, A., Miculan, M. and Peressotti, M. 2017. Loose Graph Simulations. Software Technologies: Applications and Foundations - STAF 2017 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised Selected Papers (2017), 109–126.

AbstractBibtexElectronic edition DOI

We introduce loose graph simulations (LGS), a new notion about labelled graphs which subsumes in an intuitive and natural way subgraph isomorphism (SGI), regular language pattern matching (RLPM) and graph simulation (GS). Being a unification of all these notions, LGS allows us to express directly also problems which are m̈ixed\"instances of previous ones, and hence which would not fit easily in any of them. After the definition and some examples, we show that the problem of finding loose graph simulations is NP-complete, we provide formal translation of SGI, RLPM, and GS into LGSs, and we give the representation of a problem which extends both SGI and RLPM. Finally, we identify a subclass of the LGS problem that is polynomial.

@inproceedings{MMP17,
  author = {Mansutti, Alessio and Miculan, Marino and Peressotti, Marco},
  editor = {Seidl, Martina and Zschaler, Steffen},
  title = {Loose Graph Simulations},
  booktitle = {Software Technologies: Applications and Foundations - {STAF} 2017
                 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised
                 Selected Papers},
  series = {Lecture Notes in Computer Science},
  volume = {10748},
  pages = {109--126},
  publisher = {Springer},
  year = {2017},
  url = {https://doi.org/10.1007/978-3-319-74730-9\_9},
  doi = {10.1007/978-3-319-74730-9\_9}
}

Montesi, F. and Peressotti, M. 2017. Choreographies meet Communication Failures. CoRR. abs/1712.05465, (2017).

AbstractBibtexElectronic edition

Choreographies are global descriptions of communication structures, inspired by the "Alice and Bob" notation of security protocols. They have been successfully employed in the design and implementation of distributed systems. However, there is still limited evidence of the applicability of choreographies in the real-world setting of distributed programming, where communication actions may fail. In this work, we propose the first choreography model that allows for communication failures and the programming of user-defined code to deal with such failures. We validate our model by implementing common strategies for handling communication failures in a robust way, which in turn can be used as a library by choreographies that assume reliable communication. We equip our model with a typing discipline that can statically verify reliability properties, in particular at-most-once and exactly-once delivery. We demonstrate the applicability of our model by defining a semantics-preserving compilation procedure towards a process calculus equipped with unreliable I/O actions.

@article{abs-1712-05465,
  author = {Montesi, Fabrizio and Peressotti, Marco},
  title = {Choreographies meet Communication Failures},
  journal = {CoRR},
  volume = {abs/1712.05465},
  year = {2017},
  url = {http://arxiv.org/abs/1712.05465},
  archiveprefix = {arXiv},
  eprint = {1712.05465}
}

2016

De Nart, D., Degl’Innocenti, D. and Peressotti, M. 2016. Well-Stratified Linked Data for Well-Behaved Data Citation. Bulletin of IEEE Technical Committee on Digital Libraries. 12, 1 (2016), 16–26.

AbstractBibtexElectronic edition Report

In this paper we analyse the functional requirements of linked data citation and identify a minimal set of operations and primitives needed to realise such task. Citing linked data implies solving a series of data provenance issues and finding a way to identify data subsets. Those two tasks can be handled defining a simple type system inside data and verifying it with a type checker, which is significantly less complex than interpreting reified RDF statements and can be implemented in a non data invasive way. Finally we suggest that data citation should be handled outside of the data, possibly with an ad hoc language.

@article{DDP16,
  title = {Well-Stratified Linked Data for Well-Behaved Data Citation},
  author = {De Nart, Dario and Degl'Innocenti, Dante and Peressotti, Marco},
  journal = {{Bulletin of IEEE Technical Committee on Digital Libraries}},
  volume = {12},
  number = {1},
  pages = {16--26},
  year = {2016},
  url = {https://www.ieee-tcdl.org/Bulletin/v12n1/papers/IEEE-TCDL-DC-2016\_paper\_2.pdf}
}

Miculan, M. and Peressotti, M. 2016. Structural operational semantics for non-deterministic processes with quantitative aspects. Theoretical Computer Science. 655, (2016), 135–154. DOI:10.1016/j.tcs.2016.01.012.

AbstractBibtexElectronic edition DOI Report

Recently, unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions) have been proposed with the aim of providing general results and tools. This paper provides two contributions in this respect. First, we present a general GSOS specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the ULTraS model, an extension of the usual LTSs where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function GSOS (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and GSOS formats (e.g. GSOS, Weighted GSOS, Segala-GSOS).
The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric in the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.

@article{MP16,
  author = {Miculan, Marino and Peressotti, Marco},
  title = {Structural operational semantics for non-deterministic processes with quantitative aspects},
  journal = {Theoretical Computer Science},
  volume = {655},
  pages = {135--154},
  year = {2016},
  url = {https://doi.org/10.1016/j.tcs.2016.01.012},
  doi = {10.1016/j.tcs.2016.01.012}
}

Brengos, T. and Peressotti, M. 2016. A Uniform Framework for Timed Automata. 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada (2016), 26:1–26:15.

AbstractBibtexElectronic edition DOI

Timed automata, and machines alike, currently lack a general mathematical characterisation. In this paper we provide a uniform coalgebraic understanding of these devices. This framework encompasses known behavioural equivalences for timed automata and paves the way for the extension of these notions to new timed behaviours and for the instantiation of established results from the coalgebraic theory as well. Key to this work is the use of lax functors for they allow us to model time flow as a context property and hence offer a general and expressive setting where to study timed systems: the index category encodes ḧow step sequences form executions\" (e.g. whether steps duration get accumulated or kept distinct) whereas the base category encodes s̈tep nature and composition\" (e.g. non-determinism and labels). Finally, we develop the notion of general saturation for lax functors and show how equivalences of interest for timed behaviours are instances of this notion. This characterisation allows us to reason about the expressiveness of said notions within a uniform framework and organise them in a spectrum independent from the behavioural aspects encoded in the base category.

@inproceedings{BP16,
  author = {Brengos, Tomasz and Peressotti, Marco},
  editor = {Desharnais, Jos{\'{e}}e and Jagadeesan, Radha},
  title = {A Uniform Framework for Timed Automata},
  booktitle = {27th International Conference on Concurrency Theory, {CONCUR} 2016, August 23-26, 2016, Qu{\'{e}}bec City, Canada},
  series = {LIPIcs},
  volume = {59},
  pages = {26:1--26:15},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year = {2016},
  url = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.26},
  doi = {10.4230/LIPIcs.CONCUR.2016.26}
}

Miculan, M. and Peressotti, M. 2016. On the Bisimulation Hierarchy of State-to-Function Transition Systems. Proceedings of the 17th Italian Conference on Theoretical Computer Science, Lecce, Italy, September 7-9, 2016. (2016), 88–102.

AbstractBibtexElectronic edition

Weighted labelled transition systems (WLTSs) are an established (meta-)model aiming to provide general results and tools for a wide range of systems such as non-deterministic, stochastic, and probabilistic systems. In order to encompass processes combining several quantitative aspects, extensions of the WLTS framework have been further proposed, state-to-function transition systems (FuTSs) and uniform labelled transition systems (ULTraSs) being two prominent examples. In this paper we show that this hierarchy of meta-models collapses when studied under the lens of bisimulation-coherent encodings.

@inproceedings{MP18,
  author = {Miculan, Marino and Peressotti, Marco},
  editor = {Bil{\`{o}}, Vittorio and Caruso, Antonio},
  title = {On the Bisimulation Hierarchy of State-to-Function Transition Systems},
  booktitle = {Proceedings of the 17th Italian Conference on Theoretical Computer Science, Lecce, Italy, September 7-9, 2016.},
  series = {{CEUR} Workshop Proceedings},
  volume = {1720},
  pages = {88--102},
  publisher = {CEUR-WS.org},
  year = {2016},
  url = {http://ceur-ws.org/Vol-1720/full7.pdf}
}

De Nart, D., Degl’Innocenti, D., Peressotti, M. and Tasso, C. 2016. Stratifying Semantic Data for Citation and Trust: An Introduction to RDFDF. Digital Libraries and Multimedia Archives - 12th Italian Research Conference on Digital Libraries, IRCDL 2016, Florence, Italy, February 4-5, 2016, Revised Selected Papers (2016), 104–111.

AbstractBibtexElectronic edition DOI

@inproceedings{DDPT16,
  author = {De Nart, Dario and Degl'Innocenti, Dante and Peressotti, Marco and Tasso, Carlo},
  editor = {Agosti, Maristella and Bertini, Marco and Ferilli, Stefano and Marinai, Simone and Orio, Nicola},
  title = {Stratifying Semantic Data for Citation and Trust: An Introduction to RDFDF},
  booktitle = {Digital Libraries and Multimedia Archives - 12th Italian Research Conference on Digital Libraries, {IRCDL} 2016, Florence, Italy, February 4-5, 2016, Revised Selected Papers},
  series = {Communications in Computer and Information Science},
  volume = {701},
  pages = {104--111},
  year = {2016},
  isbn = {978-3-319-56300-8},
  doi = {10.1007/978-3-319-56300-8_10},
  url = {http://dx.doi.org/10.1007/978-3-319-56300-8_10}
}

Miculan, M. and Peressotti, M. 2016. A Specification of Open Transactional Memory for Haskell. CoRR. abs/1602.05365, (2016).

AbstractBibtexElectronic edition

Transactional memory (TM) has emerged as a promising abstraction for concurrent programming alternative to lock-based synchronizations. However, most TM models admit only isolated transactions, which are not adequate in multi-threaded programming where transactions have to interact via shared data before committing. In this paper, we present Open Transactional Memory (OTM), a programming abstraction supporting safe, data-driven interactions between composable memory transactions. This is achieved by relaxing isolation between transactions, still ensuring atomicity: threads of different transactions can interact by accessing shared variables, but then their transactions have to commit together-actually, these transactions are transparently merged. This model allows for loosely-coupled interactions since transaction merging is driven only by accesses to shared data, with no need to specify participants beforehand. In this paper we provide a specification of the OTM in the setting of Concurrent Haskell, showing that it is a conservative extension of current STM abstraction. In particular, we provide a formal semantics, which allows us to prove that OTM satisfies the \emphopacity criterion.

@article{abs-1602-05365,
  author = {Miculan, Marino and Peressotti, Marco},
  title = {A Specification of Open Transactional Memory for Haskell},
  journal = {CoRR},
  volume = {abs/1602.05365},
  year = {2016},
  url = {http://arxiv.org/abs/1602.05365},
  archiveprefix = {arXiv},
  eprint = {1602.05365}
}

Peressotti, M. 2016. Endofunctors modelling higher-order behaviours. CoRR. abs/1602.06221, (2016).

AbstractBibtexElectronic edition

In this paper we show how the abstract behaviours of higher-order systems can be modelled as final coalgebras of suitable behavioural functors. These functors have the challenging peculiarity to be circularly defined with their own final coalgebra. Our main contribution is a general construction for defining these functors, solving this circularity which is the essence of higher-order behaviours. This characterisation is syntax agnostic. To achieve this property, we shift from term passing to behaviour passing: in the former higher-order is expressed by passing around syntactic objects (such as terms or processes) as representations of behaviours whereas the former ditches the syntactic encoding altogether and works directly with behaviours i.e. semantic objects. From this perspective, the former can be seen as syntactic higher-order whereas the later as semantic higher-order.

@article{abs-1602-06221,
  author = {Peressotti, Marco},
  title = {Endofunctors modelling higher-order behaviours},
  journal = {CoRR},
  volume = {abs/1602.06221},
  year = {2016},
  url = {http://arxiv.org/abs/1602.06221},
  archiveprefix = {arXiv},
  eprint = {1602.06221}
}

2015

Brengos, T., Miculan, M. and Peressotti, M. 2015. Behavioural equivalences for coalgebras with unobservable moves. Journal of Logical and Algebraic Methods in Programming. 84, 6 (2015), 826–852. DOI:10.1016/j.jlamp.2015.09.002.

AbstractBibtexElectronic edition DOI Report

We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on parametrized saturation categories, i.e. categories whose hom-sets are endowed with complete orders and a suitable iteration operators; this structure allows us to provide the abstract definitions of various (weak) behavioural equivalence. We show that the Kleisli categories of many common monads are categories of this kind. This allows us to readily instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences. Moreover, we can provide neatly new weak behavioural equivalences for more complex behaviours, like those definable on topological spaces, measurable spaces, etc.

@article{BMP15,
  author = {Brengos, Tomasz and Miculan, Marino and Peressotti, Marco},
  title = {Behavioural equivalences for coalgebras with unobservable moves},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {84},
  number = {6},
  pages = {826--852},
  year = {2015},
  url = {http://dx.doi.org/10.1016/j.jlamp.2015.09.002},
  doi = {10.1016/j.jlamp.2015.09.002}
}

Miculan, M., Peressotti, M. and Toneguzzo, A. 2015. Open Transactions on Shared Memory. Coordination Models and Languages - 17th IFIP WG 6.1 International Conference, COORDINATION 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings (2015), 213–229.

AbstractBibtexElectronic edition DOI Report

Transactional memory has arisen as a good way for solving many of the issues of lock-based programming. However, most implementations admit isolated transactions only, which are not adequate when we have to coordinate communicating processes. To this end, in this paper we present OCTM, an Haskell-like language with open transactions over shared transactional memory: processes can join transactions at runtime just by accessing to shared variables. Thus a transaction can co-operate with the environment through shared variables, but if it is rolled-back, also all its effects on the environment are retracted. For proving the expressive power of TCCS we give an implementation of TCCS, a CCS-like calculus with open transactions.

@inproceedings{MPT15,
  author = {Miculan, Marino and Peressotti, Marco and Toneguzzo, Andrea},
  editor = {Holvoet, Tom and Viroli, Mirko},
  title = {Open Transactions on Shared Memory},
  booktitle = {Coordination Models and Languages - 17th {IFIP} {WG} 6.1 International Conference, {COORDINATION} 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {9037},
  pages = {213--229},
  publisher = {Springer},
  year = {2015},
  doi = {10.1007/978-3-319-19282-6\_14},
  url = {http://dx.doi.org/10.1007/978-3}
}

2014

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.

AbstractBibtexElectronic edition DOI Report

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}
}

Mansutti, A., Miculan, M. and Peressotti, M. 2014. Multi-agent Systems Design and Prototyping with Bigraphical Reactive Systems. Distributed Applications and Interoperable Systems - 14th IFIP WG 6.1 International Conference, DAIS 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014, Proceedings (2014), 201–208.

AbstractBibtexElectronic edition DOI

Several frameworks and methodologies have been proposed to ease the design of Multi Agent Systems (MAS), but the vast majority of them is tightly tied to specific implementation platforms. In this paper, we outline a methodology for MAS design and prototyping in the more abstract framework of Bigraphical Reactive Systems (BRS). In our approach, components and elements of the application domain are modelled as bigraphs, and their dynamics as graph rewriting rules. Desiderata can be encoded by means of type systems or logical formulae. Then, the BDI agents (i.e., their beliefs, desires and intentions) are identified and extracted from the BRS. This yield a prototype which can be run as distributed bigraphical system, evolving by means of distributed transactional rewritings triggered by cooperating agents depending on their internal intentions and beliefs.
This methodology allows the designer to benefit from the results and tools from the theory of BRS, especially in the requirement analysis and validation phases. Among other results, we mention behavioural equivalences, temporal/spatial logics, visual tools for editing, for simulation and for model checking, etc. Moreover, bigraphs can be naturally composed, thus allowing for modular design of MAS.

@inproceedings{MMP15,
  author = {Mansutti, Alessio and Miculan, Marino and Peressotti, Marco},
  editor = {Magoutis, Kostas and Pietzuch, Peter R.},
  title = {Multi-agent Systems Design and Prototyping with Bigraphical Reactive Systems},
  booktitle = {Distributed Applications and Interoperable Systems - 14th {IFIP} {WG} 6.1 International Conference, {DAIS} 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {8460},
  pages = {201--208},
  publisher = {Springer},
  year = {2014},
  url = {http://dx.doi.org/10.1007/978-3-662-43352-2_16},
  doi = {10.1007/978-3-662-43352-2_16}
}

Miculan, M. and Peressotti, M. 2014. GSOS for non-deterministic processes with quantitative aspects. Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014. (2014), 17–33.

AbstractBibtexElectronic edition DOI Report

General frameworks have been recently proposed as unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions), aiming to provide general results and tools. This paper provides two contributions in this respect. First, we present a general GSOS specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the ULTraS model, an extension of the usual LTSs where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function GSOS (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and GSOS formats (e.g. GSOS, Weighted GSOS, Segala-GSOS, among others). The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric on the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.

@inproceedings{MP14,
  author = {Miculan, Marino and Peressotti, Marco},
  editor = {Bertrand, Nathalie and Bortolussi, Luca},
  title = {{GSOS} for non-deterministic processes with quantitative aspects},
  booktitle = {Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, {QAPL} 2014, Grenoble, France, 12-13 April 2014.},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {154},
  pages = {17--33},
  year = {2014},
  url = {http://dx.doi.org/10.4204/EPTCS.154.2},
  doi = {10.4204/EPTCS.154.2}
}

Mansutti, A., Miculan, M. and Peressotti, M. 2014. Towards distributed bigraphical reactive systems. Proc. GCM (2014), 45.

AbstractBibtexElectronic edition

The bigraph embedding problem is crucial for many resultsand tools about bigraphs and bigraphical reactive systems (BRS). Thereare algorithms for computing bigraphical embedding but these are de-signed to be run locally and assume a complete view of the guest andhost bigraphs, putting large bigraphs and BRS out of their reach. Toovercome these limitations we present adecentralized algorithmfor com-puting bigraph embeddings that allows us to distribute both state andcomputation over several concurrent processes. Among various applica-tions, this algorithm offers the basis for distributed BRS simulationswhere non-interfering reactions are carried out concurrently.

@inproceedings{MMP16,
  title = {Towards distributed bigraphical reactive systems},
  author = {Mansutti, Alessio and Miculan, Marino and Peressotti, Marco},
  booktitle = {Proc.~GCM},
  pages = {45},
  year = {2014},
  editor = {Echahed, Rachid and Habel, Annegre and Mosbah, Mohamed},
  url = {http://gcm2014.imag.fr/proceedingsGCM2014.pdf}
}

Miculan, M. and Peressotti, M. 2014. A CSP implementation of the bigraph embedding problem. CoRR. abs/1412.1042, (2014).

AbstractBibtexElectronic edition Tool

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}
}

2013

Miculan, M. and Peressotti, M. 2013. Weak bisimulations for labelled transition systems weighted over semirings. CoRR. abs/1310.4106, (2013).

AbstractBibtexElectronic edition

Weighted labelled transition systems are LTSs whose transitions are given weights drawn from a commutative monoid. WLTSs subsume a wide range of LTSs, providing a general notion of strong (weighted) bisimulation. In this paper we extend this framework towards other behavioural equivalences, by considering semirings of weights. Taking advantage of this extra structure, we introduce a general notion of weak weighted bisimulation. We show that weak weighted bisimulation coincides with the usual weak bisimulations in the cases of non-deterministic and fully-probabilistic systems; moreover, it naturally provides a definition of weak bisimulation also for kinds of LTSs where this notion is currently missing (such as, stochastic systems). Finally, we provide a categorical account of the coalgebraic construction of weak weighted bisimulation; this construction points out how to port our approach to other equivalences based on different notion of observability.

@article{abs-1310-4106,
  author = {Miculan, Marino and Peressotti, Marco},
  title = {Weak bisimulations for labelled transition systems weighted over semirings},
  journal = {CoRR},
  volume = {abs/1310.4106},
  year = {2013},
  url = {http://arxiv.org/abs/1310.4106},
  archiveprefix = {arXiv},
  eprint = {1310.4106}
}