A picture of Marco

About

I am Marco Peressotti and I am an Associate Professor of Computer Science at the Department of Mathematics and Computer Science of the University of Southern Denmark where I am member of the Section of Artificial Intelligence, Cybersecurity, and Programming Languages. I also serve as member of the Communication Group of the Microservices Community, an international community of researchers, professionals, and students interested in the software paradigm of Microservices. I received my Ph.D. Degree in Computer Science from the University of Udine in 2017.

My research mission is to make it more effective and robust to program and analyse concurrent systems. An overarching theme of my research approach is the use of formal methods and programming languages techniques as well as the aim for a unifying mathematical perspective rooted in Logic and Category Theory.

Highlights

Mar'23
I will attend the Dagstuhl Seminar Next Generation Protocols for Heterogeneous Systems.
Jan'23
I am starting a new position as Associate Professor of Computer Science at the Department of Mathematics and Computer Science of the University of Southern Denmark.
Dec'22
On March 24, I will hold an online training session about Software Verification with TLA+ for the the Danish Cyber Championships. You can find more details at the registration page.
Aug'22
I gave a lecture about Formal Methods and a tutorial on TLA+ at the Danish Summer School on CyberSecurity.
Feb'22
I will serve in the PC of the Doctoral Symposium at ECOOP 2022.
Feb'22
I will serve in the PC of the 3rd International Workshop on Agility with Microservices Programming (AMP 2022) at XP 2022.

All news

Selected publications

Chiapperini, A., Miculan, M. and Peressotti, M. 2022. Computing (Optimal) Embeddings of Directed Bigraphs. Science of Computer Programming. 221, (2022), 102842. DOI:10.1016/j.scico.2022.102842.

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

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

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

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

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

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

All publications

Reviewing

I am generally happy to act as an external reviewer for papers which match my research interests, provided I can see reviews and participate in the discussion after submitting my review.