My publications are also listed on my DBLP, Google Scholar, and Scopus profiles.
Choreographies are coordination plans for concurrent and distributed systems, which define the roles of the involved participants and how they are supposed to work together. In the paradigm of choreographic programming, choreographies are programs that can be compiled into executable implementations.
In this article, we present Choral, the first choreographic programming language based on mainstream abstractions. The key idea in Choral is a new notion of data type, which allows for expressing that data is distributed over different roles. We use this idea to reconstruct the paradigm of choreographic programming through object-oriented abstractions. Choreographies are classes, and instances of choreographies are objects with states and behaviours implemented collaboratively by roles.
Choral comes with a compiler that, given a choreography, generates an implementation for each of its roles. These implementations are libraries in pure Java, whose types are under the control of the Choral programmer. Developers can then modularly compose these libraries in their programs, to participate correctly in choreographies. Choral is the first incarnation of choreographic programming offering such modularity, which finally connects more than a decade of research on the paradigm to practical software development.
The integration of choreographic and object-oriented programming yields other powerful advantages, where the features of one paradigm benefit the other in ways that go beyond the sum of the parts. On the one hand, the high-level abstractions and static checks from the world of choreographies can be used to write concurrent and distributed object-oriented software more concisely and correctly. On the other hand, we obtain a much more expressive choreographic language from object-oriented abstractions than in previous work. This expressivity allows for writing more reusable and flexible choreographies. For example, object passing makes Choral the first higher-order choreographic programming language, whereby choreographies can be parameterised over other choreographies without any need for central coordination. We also extend method overloading to a new dimension: specialisation based on data location. Together with subtyping and generics, this allows Choral to elegantly support user-defined communication mechanisms and middleware.
@article{GMP24,
author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco},
title = {Choral: Object-oriented Choreographic Programming},
year = {2024},
issue_date = {March 2024},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
journal = {ACM Trans. Program. Lang. Syst.},
volume = {46},
number = {1},
pages = {1:1--1:59},
issn = {0164-0925},
url = {https://doi.org/10.1145/3632398},
doi = {10.1145/3632398},
keywords = {Communication, Higher-Kinded Types, Choreographies}
}
Dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that the operational semantics for programs considered in these logics is tailored on trace reasoning for sequential programs. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL) in which we are able to reason on sets of programs provided with arbitrary operational semantics. We prove cut-elimination and adequacy of a sequent calculus for PDL and we extend these results to OPDL. We conclude by discussing OPDL for Milner’s CCS and Choreographic Programming.
@article{abs-2403-18508,
title = {On Propositional Dynamic Logic and Concurrency},
author = {Acclavio, Matteo and Montesi, Fabrizio and Peressotti, Marco},
journal = {CoRR},
volume = {abs/2403.18508},
year = {2024},
url = {https://arxiv.org/abs/2403.18508},
doi = {10.48550/arXiv.2403.18508},
archiveprefix = {arXiv},
eprint = {2403.18508}
}
Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order – for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs).
In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered or dropped messages as in the UDP transport protocol. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency by overlapping communication with computation.
@article{abs-2401-17403,
title = {Ozone: Fully Out-of-Order Choreographies},
author = {Plyukhin, Dan and Montesi, Fabrizio and Peressotti, Marco},
journal = {CoRR},
volume = {abs/2401.17403},
year = {2024},
url = {https://arxiv.org/abs/2401.17403},
doi = {10.48550/arXiv.2401.17403},
archiveprefix = {arXiv},
eprint = {2401.17403}
}
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically.
Theory of choreographies 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 these proofs has led to important errors being found in published works.
In this work, we formalise the theory of a choreographic programming language in Coq. Our development includes the basic properties of this language, a proof of its Turing completeness, a compilation procedure to a process language, and an operational characterisation of the correctness of this procedure.
Our formalisation experience illustrates the benefits of using a theorem prover: we get both an additional degree of confidence from the mechanised proof, and a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.
@article{CMP23,
author = {Cruz{-}Filipe, Lu{\'{\i}}s and Montesi, Fabrizio and Peressotti, Marco},
title = {A Formal Theory of Choreographic Programming},
journal = {Journal of Automated Reasoning},
volume = {67},
number = {21},
pages = {1--34},
year = {2023},
issn = {1573-0670},
url = {https://doi.org/10.1007/s10817-023-09665-3},
doi = {10.1007/s10817-023-09665-3}
}
We introduce LEMMA2Jolie, a tool for translating domain models of microservice architectures given in LEMMA into concrete APIs of microservices in the Jolie programming language. Our tool combines the state of the art for the design and implementation of microservices: developers can use Domain-Driven Design (DDD) for the construction of the domain models of a microservice architecture, and then automatically transition to a service-oriented programming language that provides native linguistic support for implementing the behaviour of each microservice.
@article{GMPR23a,
author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian},
title = {LEMMA2Jolie: A Tool to Generate Microservice APIs from Domain Models},
journal = {Science of Computer Programming},
volume = {228},
pages = {102956},
year = {2023},
issn = {0167-6423},
doi = {10.1016/j.scico.2023.102956},
url = {https://www.sciencedirect.com/science/article/pii/S0167642323000382}
}
We formally define and implement a translation of domain and service models expressed in the LEMMA modelling ecosystem for microservice architectures to source code in the Jolie microservice programming language. Specifically, our work extends previous efforts on the generation of Jolie code to the inclusion of the LEMMA service modelling layer. We also contribute an implementation of our translation, given as an extension of the LEMMA2Jolie tool, which enables the practical application of our encoding. As a result, LEMMA2Jolie now supports a software development process whereby microservice architectures can first be designed by microservice developers in collaboration with domain experts in LEMMA, and then be automatically translated into Jolie APIs. Our tool can thus be used to enhance productivity and improve design adherence.
@inproceedings{GMPR23b,
author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian},
title = {{Model-Driven Code Generation for Microservices: Service Models}},
booktitle = {Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
pages = {6:1--6:17},
series = {Open Access Series in Informatics (OASIcs)},
isbn = {978-3-95977-306-5},
issn = {2190-6807},
year = {2023},
volume = {111},
editor = {Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022.6},
urn = {urn:nbn:de:0030-drops-194688},
doi = {10.4230/OASIcs.Microservices.2020-2022.6}
}
We present Modular Choreographies, a new choreographic programming language that features modular functions. Modular Choreographies is aimed at simplicity: its communication abstraction follows the simple tradition from the “Alice and Bob” notation. We develop a compiler toolchain that translates choreographies into modular Java libraries, which developers can use to participate correctly in choreographies. The key novelty is to compile through the Choral language, which was previously proposed to define object-oriented choreographies: our toolchain compiles Modular Choreographies to Choral, and then leverages the existing Choral compiler to generate Java code. Our work is the first to bridge the simplicity of traditional choreographic programming languages with the requirement of generating modular libraries in a mainstream language (Java).
@inproceedings{CMMP23,
author = {Cruz-Filipe, Lu{\'\i}s and Madsen, Anne and Montesi, Fabrizio and Peressotti, Marco},
title = {{Modular Choreographies: Bridging Alice and Bob Notation to Java}},
booktitle = {Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
pages = {3:1--3:18},
series = {Open Access Series in Informatics (OASIcs)},
isbn = {978-3-95977-306-5},
issn = {2190-6807},
year = {2023},
volume = {111},
editor = {Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022.3},
urn = {urn:nbn:de:0030-drops-194650},
doi = {10.4230/OASIcs.Microservices.2020-2022.3}
}
Choreographic programming is a paradigm for concurrent and distributed software, whereby descriptions of the intended communications (choreographies) are automatically compiled into distributed code with strong safety and liveness properties (e.g., deadlock-freedom). Recent efforts tried to combine the theories of choreographic programming and higher-order functional programming, in order to integrate the benefits of the former with the modularity of the latter. However, they do not offer a satisfactory theory of compilation compared to the literature, because of important syntactic and semantic shortcomings: compilation is not modular (editing a part might require recompiling everything) and the generated code can perform unexpected global synchronisations. In this paper, we find that these shortcomings are not mere coincidences. Rather, they stem from genuine new challenges posed by the integration of choreographies and functions: knowing which participants are involved in a choreography becomes nontrivial, and divergence in applications requires rethinking how to prove the semantic correctness of compilation. We present a novel theory of compilation for functional choreographies that overcomes these challenges, based on types and a careful design of the semantics of choreographies and distributed code. The result: a modular notion of compilation, which produces code that is deadlock-free and correct (it operationally corresponds to its source choreography).
@inproceedings{CGLMP23,
author = {Cruz{-}Filipe, Lu{\'{\i}}s and Graversen, Eva and Lugovi{\'c}, Lovro and Montesi, Fabrizio and Peressotti, Marco},
editor = {Ali, Karim and Salvaneschi, Guido},
title = {Modular Compilation for Higher-Order Functional Choreographies},
booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
isbn = {978-3-95977-281-5},
issn = {1868-8969},
year = {2023},
volume = {263},
pages = {7:1--7:37},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18200},
urn = {urn:nbn:de:0030-drops-182005},
doi = {10.4230/LIPIcs.ECOOP.2023.7}
}
We present JoT, a testing framework for Microservice Architectures (MSAs) based on technology agnosticism, a core principle of microservices. The main advantage of JoT is that it reduces the amount of work for a) testing for MSAs whose services use different technology stacks, b) writing tests that involve multiple services, and c) reusing tests of the same MSA under different deployment configurations or after changing some of its components (e.g., when, for performance, one reimplements a service with a different technology). In JoT, tests are orchestrators that can both consume or offer operations from/to the MSA under test. The language for writing JoT tests is Jolie, which provides constructs that support technology agnosticism and the definition of terse test behaviours. We present the methodology we envision for testing MSAs with JoT and we validate it by implementing non-trivial test scenarios taken from a reference MSA from the literature (Lakeside Mutual).
@inproceedings{GMPRU23,
author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Unwerawattana, Narongrit},
editor = {Jongmans, Sung{-}Shik and Lopes, Ant{\'{o}}nia},
title = {JoT: {A} Jolie Framework for Testing Microservices},
booktitle = {Coordination Models and Languages},
series = {Lecture Notes in Computer Science},
volume = {13908},
pages = {172--191},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-35361-1\_10},
doi = {10.1007/978-3-031-35361-1\_10},
isbn = {978-3-031-35361-1}
}
Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties.
This paper presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation.
@inproceedings{CGMP23,
author = {Cruz{-}Filipe, Lu{\'{\i}}s and Graversen, Eva and Montesi, Fabrizio and Peressotti, Marco},
editor = {Jongmans, Sung{-}Shik and Lopes, Ant{\'{o}}nia},
title = {Reasoning About Choreographic Programs},
booktitle = {Coordination Models and Languages},
series = {Lecture Notes in Computer Science},
volume = {13908},
pages = {144--162},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-35361-1\_8},
doi = {10.1007/978-3-031-35361-1\_8},
isbn = {978-3-031-35361-1}
}
Bigraphs and bigraphical reactive systems are a well-known meta-model successfully used for formalizing a wide range of models and situations, such as process calculi, service oriented architectures, multi-agent systems, biological systems, etc.. A key problem in both the theory and the implementations of bigraphs is how to compute embeddings, i.e., structure-preserving mappings of a given bigraph (the pattern or guest) inside another (the target or host). In this paper, we present an algorithm for computing embeddings for directed bigraphs, an extension of Milner’s bigraphs which take into account the request directions between controls and names. This algorithm solves the embedding problem by means of a reduction to a constraint satisfaction problem. We first prove soundness and completeness of this algorithm; then we present an implementation in jLibBig, a general Java library for manipulating bigraphical reactive systems. The effectiveness of this implementation is shown by several experimental results. Finally, we show that this algorithm can be readily adapted to find the optimal embeddings in a weighted variant of the embedding problem.
@article{CMP22,
title = {Computing (Optimal) Embeddings of Directed Bigraphs},
author = {Chiapperini, Alessio and Miculan, Marino and Peressotti, Marco},
journal = {Science of Computer Programming},
volume = {221},
pages = {102842},
year = {2022},
issn = {0167-6423},
doi = {10.1016/j.scico.2022.102842},
url = {https://www.sciencedirect.com/science/article/pii/S0167642322000752}
}
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, where developers write the communications that should be enacted and a compiler then automatically generates a distributed implementation. Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and in particular introduced the possibility of expressing higher-order choreographies that are fully distributed. In this article, we introduce Chorλ, the first functional choreographic programming language. It is also the first theory that explains the core ideas of higher-order choreographic programming. We show that bridging the gap between practice and theory requires developing a new evaluation strategy and typing discipline for λ terms that accounts for the distributed nature of computation in choreographies
@inproceedings{CGLMP22,
author = {Cruz{-}Filipe, Lu{\'{\i}}s and Graversen, Eva and Lugovi{\'c}, Lovro and Montesi, Fabrizio and Peressotti, Marco},
editor = {Seidl, Helmut and Liu, Zhiming and Pasareanu, Corina},
title = {Functional Choreographic Programming},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2022},
pages = {212--237},
doi = {10.1007/978-3-031-17715-6_15},
isbn = {978-3-031-17715-6}
}
We formally define and implement a translation from domain models in the LEMMA modelling framework to microservice APIs in the Jolie programming language. Our tool enables a software development process whereby microservice architectures can first be designed with the leading method of Domain-Driven Design (DDD), and then corresponding data types and service interfaces (APIs) in Jolie are automatically generated. Developers can extend and use these APIs as guides in order to produce compliant implementations. Our tool thus contributes to enhancing productivity and improving the design adherence of microservices.
@inproceedings{GMPR22,
author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian},
editor = {ter Beek, Maurice H. and Sirjani, Marjan},
title = {Model-Driven Generation of Microservice Interfaces: From LEMMA Domain Models to Jolie APIs},
booktitle = {Coordination Models and Languages},
year = {2022},
series = {Lecture Notes in Computer Science},
volume = {13271},
pages = {223--240},
publisher = {Springer},
isbn = {978-3-031-08143-9},
url = {https://doi.org/10.1007/978-3-031-08143-9\_13},
doi = {10.1007/978-3-031-08143-9\_13}
}
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},
editor = {Carminati, Barbara and Chang, Carl K. and Daminai, Ernesto and Deng, Shuigung and Tan, Wei and Wang, Zhongjie and Ward, Robert and Zhang, Jia},
title = {Sliceable Monolith: Monolith First, Microservices Later},
booktitle = {{IEEE} International Conference on Services Computing, {SCC} 2021, Chicago, IL, USA, September 5-10, 2021},
pages = {364--366},
publisher = {{IEEE}},
year = {2021},
url = {https://doi.org/10.1109/SCC53864.2021.00050},
doi = {10.1109/SCC53864.2021.00050}
}
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.
@inproceedings{CMP21b,
author = {Cruz{-}Filipe, Lu{\'{\i}}s and Montesi, Fabrizio and Peressotti, Marco},
editor = {Cerone, Antonio and {\"{O}}lveczky, Peter Csaba},
title = {Certifying Choreography Compilation},
booktitle = {Theoretical Aspects of Computing - {ICTAC} 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12819},
pages = {115--133},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-85315-0\_8},
doi = {10.1007/978-3-030-85315-0\_8}
}
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{CMP21a,
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}
}
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}
}
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}
}
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free.
Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and introduced the possibility of expressing higher-order choreographies (choreographies parameterised over choreographies) that are fully distributed. As a consequence, it is unclear if the usual guarantees of choreographies can still hold in the more general setting of higher-order ones.
We introduce Chorλ, the first functional choreographic programming language: it introduces a new formulation of the standard communication primitive found in choreographies as a function, and it is based upon the λ-calculus. Chorλ is the first theory that explains the core ideas of higher-order choreographic programming (as in Choral). Bridging the gap between practice and theory requires developing a new evaluation strategy and typing discipline for λ terms that accounts for the distributed nature of computation in choreographies. We illustrate the expressivity of Chorλ with a series of examples, which include reconstructions of the key examples from the original presentation of Choral. Our theory supports the expected properties of choreographic programming and bridges the gap between the communities of functional and choreographic programming.
@article{abs-2111-03701,
author = {Cruz{-}Filipe, Lu{\'{\i}}s and Graversen, Eva and Lugovi{\'c}, Lovro and Montesi, Fabrizio and Peressotti, Marco},
title = {Functional Choreographic Programming},
journal = {CoRR},
volume = {abs/2111.03701},
year = {2021},
url = {https://arxiv.org/abs/2111.03701},
doi = {10.48550/arXiv.2111.03701},
archiveprefix = {arXiv},
eprint = {2111.03701}
}
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},
doi = {10.48550/arXiv.2106.11818},
archiveprefix = {arXiv},
eprint = {2106.11818}
}
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}
}
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}
}
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}
}
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}
}
@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/}
}
We present Choral, the first language 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 = {Choral: Object-Oriented Choreographic Programming},
journal = {CoRR},
volume = {abs/22005.09520},
year = {2020},
url = {https://arxiv.org/abs/2005.09520},
doi = {10.48550/arXiv.2005.09520},
archiveprefix = {arXiv},
eprint = {2005.09520}
}
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}
}
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}
}
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}
}
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 = {https://arxiv.org/abs/1906.05573},
doi = {10.48550/arXiv.1906.05573},
archiveprefix = {arXiv},
eprint = {1906.05573}
}
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}
}
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}
}
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 = {https://arxiv.org/abs/1803.01049},
doi = {10.48550/arXiv.1803.01049},
archiveprefix = {arXiv},
eprint = {1803.01049}
}
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}
}
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}
}
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 = {https://arxiv.org/abs/1712.05465},
doi = {10.48550/arXiv.1712.05465},
archiveprefix = {arXiv},
eprint = {1712.05465}
}
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}
}
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}
}
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}
}
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{MP16b,
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}
}
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, and propose a simple language to describe RDF documents where separation between data and metainformation is explicitly specified.
@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}
}
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 = {https://arxiv.org/abs/1602.05365},
doi = {10.48550/arXiv.1602.05365},
archiveprefix = {arXiv},
eprint = {1602.05365}
}
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 = {https://arxiv.org/abs/1602.06221},
doi = {10.48550/arXiv.1602.06221},
archiveprefix = {arXiv},
eprint = {1602.06221}
}
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}
}
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}
}
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{MMP14c,
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}
}
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{MMP14a,
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}
}
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}
}
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{MMP14b,
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}
}
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 = {https://arxiv.org/abs/1412.1042},
doi = {10.48550/arXiv.1412.1042},
archiveprefix = {arXiv},
eprint = {1412.1042}
}
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 = {https://arxiv.org/abs/1310.4106},
doi = {10.48550/arXiv.1310.4106},
archiveprefix = {arXiv},
eprint = {1310.4106}
}