I am an Assistant Professor of Computer Science at the Department of Mathematics and Computer Science of the University of Southern Denmark, member of the Concurrency and Logic research group.

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.

Office: Ø16-601a-2
Address: Campusvej 55, 5230 Odense M, Denmark"
Email: [email protected]
Phone: +45 65 50 90 26


Gave a lecture about Formal Methods and a tutorial on TLA+ at the Danish Summer School on CyberSecurity.
Exited to be invited to the International Conference on The Future of Standards in CyberSecurity. I will talk about programming multiparty protocols with Choral.
Released the first beta of Choral, a Java-like programming language for type-safe multiparty protocols. Choral is based on my paper "Choreographies as Objects".
Released a new version of jLibBig, a Java library for Bigraphical Reactive Systems. This release introduces support for directed bigraphs based on my paper "Computing embeddings of directed bigraphs" and completes the migration to the new API of CHOCO-Solver.
Gave the talk "A logical reconstruction of the π-calculus and its behavioural theory" as part of my research visit to the Formal Analysis, Theory & Algorithms section at Glasgow University, UK.

All news

Selected publications

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

All publications


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.