19 citations · 96 across the 34 of their papers we have counts for
22 papers · 1 filter
Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker
We present a library-level formalisation of Hennessy-Milner Logic (HML) - a foundational logic for labelled transition systems (LTSs) - for the Lean Computer Science Library (CSLib…
On Propositional Dynamic Logic and Concurrency
Matteo Acclavio, Fabrizio Montesi, Marco Peressotti
Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as…
A Formal Theory of Choreographic Programming
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised impleme…
Linear Logic, the -calculus, and their Metatheory: A Recipe for Proofs as Processes
Fabrizio Montesi, Marco Peressotti
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…
Formalising a Turing-Complete Choreographic Language in Coq
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
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…
A CSP implementation of the directed bigraph embedding problem
Alessio Chiapperini, Marino Miculan, Marco Peressotti
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 tha…
Towards a Formal Model for Composable Container Systems
Fabio Burco, Marino Miculan, Marco Peressotti
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 appl…
A Graph-Based Tool to Embed the π-Calculus into a Computational DPO Framework
Jakob Lykke Andersen, Marc Hellmuth, Daniel Merkle +2
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 m…
Two modes of recognition: algebra, coalgebra, and languages
Tomasz Brengos, Marco Peressotti
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 mo…
Taking Linear Logic Apart
Wen Kokke, Fabrizio Montesi, Marco Peressotti
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 ru…
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Wen Kokke, Fabrizio Montesi, Marco Peressotti
We present Hypersequent Classical Processes (HCP), a revised interpretation of the "Proofs as Processes" correspondence between linear logic and the π-calculus initially proposed b…
Classical Transitions
Fabrizio Montesi, Marco Peressotti
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 twi…
Behavioural equivalences for timed systems
Tomasz Brengos, Marco Peressotti
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…
On the trade-off between labels and weights in quantitative bisimulation
Marco Peressotti
Reductions for transition systems have been recently introduced as a uniform and principled method for comparing the expressiveness of system models with respect to a range of prop…
Loose Graph Simulations
Alessio Mansutti, Marino Miculan, Marco Peressotti
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 m…
Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation
Marino Miculan, Marco Peressotti
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, stocha…
Endofunctors modelling higher-order behaviours
Marco Peressotti
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…
A CSP implementation of the bigraph embedding problem
Marino Miculan, Marco Peressotti
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 i…
Behavioural equivalences for coalgebras with unobservable moves
Tomasz Brengos, Marino Miculan, Marco Peressotti
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…
Structural operational semantics for non-deterministic processes with quantitative aspects
Marino Miculan, Marco Peressotti
General frameworks have been recently proposed as unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed…
GSOS for non-deterministic processes with quantitative aspects
Marino Miculan, Marco Peressotti
Recently, some general frameworks have been proposed as unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically…
Weak bisimulations for labelled transition systems weighted over semirings
Marino Miculan, Marco Peressotti
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…