-
A Reversible Perspective on Petri Nets and Event Structures
Authors:
Hernán Melgratti,
Claudio Antares Mezzina,
G. Michele Pinna
Abstract:
Event structures have emerged as a foundational model for concurrent computation, explaining computational processes by outlining the events and the relationships that dictate their execution. They play a pivotal role in the study of key aspects of concurrent computation models, such as causality and independence, and have found applications across a broad range of languages and models, spanning r…
▽ More
Event structures have emerged as a foundational model for concurrent computation, explaining computational processes by outlining the events and the relationships that dictate their execution. They play a pivotal role in the study of key aspects of concurrent computation models, such as causality and independence, and have found applications across a broad range of languages and models, spanning realms like persistence, probabilities, and quantum computing. Recently, event structures have been extended to address reversibility, where computational processes can undo previous computations. In this context, reversible event structures provide abstract representations of processes capable of both forward and backward steps in a computation. Since their introduction, event structures have played a crucial role in bridging operational models, traditionally exemplified by Petri nets and process calculi, with denotational ones, i.e., algebraic domains. In this context, we revisit the standard connection between Petri nets and event structures under the lenses of reversibility. Specifically, we introduce a subset of contextual Petri nets, dubbed reversible causal nets, that precisely correspond to reversible prime event structures. The distinctive feature of reversible causal nets lies in deriving causality from inhibitor arcs, departing from the conventional dependence on the overlap between the post and preset of transitions. In this way, we are able to operationally explain the full model of reversible prime event structures.
△ Less
Submitted 27 December, 2023;
originally announced December 2023.
-
A Truly Concurrent Semantics for Reversible CCS
Authors:
Hernán Melgratti,
Claudio Antares Mezzina,
G. Michele Pinna
Abstract:
Reversible CCS (RCCS) is a well-established, formal model for reversible communicating systems, which has been built on top of the classical Calculus of Communicating Systems (CCS). In its original formulation, each CCS process is equipped with a memory that records its performed actions, which is then used to reverse computations. More recently, abstract models for RCCS have been proposed in the…
▽ More
Reversible CCS (RCCS) is a well-established, formal model for reversible communicating systems, which has been built on top of the classical Calculus of Communicating Systems (CCS). In its original formulation, each CCS process is equipped with a memory that records its performed actions, which is then used to reverse computations. More recently, abstract models for RCCS have been proposed in the literature, basically, by directly associating RCCS processes with (reversible versions of) event structures. In this paper we propose a different abstract model: starting from one of the well-known encoding of CCS into Petri nets we apply a recently proposed approach to incorporate causally-consistent reversibility to Petri nets, obtaining as result the (reversible) net counterpart of every RCCS term.
△ Less
Submitted 23 May, 2024; v1 submitted 25 September, 2023;
originally announced September 2023.
-
Behavioural Types for Local-First Software
Authors:
Roland Kuhn,
Hernán Melgratti,
Emilio Tuosto
Abstract:
Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers.
We…
▽ More
Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers.
We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification.
The model we propose elaborates on an existing industrial platform and provides the basis for tool support (sketched here and fully described in a companion artifact paper), wherefore we consider this work to be a viable step towards reasoning about local-first and peer-to-peer software systems.
△ Less
Submitted 8 May, 2023;
originally announced May 2023.
-
Relating Reversible Petri Nets and Reversible Event Structures, categorically
Authors:
Hernán Melgratti,
Claudio Antares Mezzina,
G. Michele Pinna
Abstract:
Causal nets (CNs) are Petri nets where causal dependencies are modelled via inhibitor arcs. They play the role of occurrence nets when representing the behaviour of a concurrent and distributed system, even when reversibility is considered. In this paper we extend CNs to account also for asymmetric conflicts and study (i) how this kind of nets, and their reversible versions, can be turned into a c…
▽ More
Causal nets (CNs) are Petri nets where causal dependencies are modelled via inhibitor arcs. They play the role of occurrence nets when representing the behaviour of a concurrent and distributed system, even when reversibility is considered. In this paper we extend CNs to account also for asymmetric conflicts and study (i) how this kind of nets, and their reversible versions, can be turned into a category; and (ii) their relation with the categories of reversible asymmetric event structures.
△ Less
Submitted 24 January, 2024; v1 submitted 27 February, 2023;
originally announced February 2023.
-
Towards Refinable Choreographies
Authors:
Ugo de'Liguoro,
Hernán Melgratti,
Emilio Tuosto
Abstract:
We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, that is the sufficient conditions that guarantee a protocol to be implementable. We introduce a ty** discipline that enforces well-formed…
▽ More
We investigate refinement in the context of choreographies. We introduce refinable global choreographies allowing for the underspecification of protocols, whose interactions can be refined into actual protocols. Arbitrary refinements may spoil well-formedness, that is the sufficient conditions that guarantee a protocol to be implementable. We introduce a ty** discipline that enforces well-formedness of typed choreographies. Then we unveil the relation among refinable choregraphies and their admissible refinements in terms of an axiom scheme.
△ Less
Submitted 16 September, 2020;
originally announced September 2020.
-
Probabilistic Analysis of Binary Sessions
Authors:
Omar Inverso,
Hernán Melgratti,
Luca Padovani,
Catia Trubiani,
Emilio Tuosto
Abstract:
We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the s…
▽ More
We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.
△ Less
Submitted 23 July, 2020;
originally announced July 2020.
-
Reversible Causal Nets and Reversible Event Structures
Authors:
Hernán Melgratti,
Claudio Antares Mezzina,
Iain Phillips,
G. Michele Pinna,
Irek Ulidowski
Abstract:
One of the well-known results in concurrency theory concerns the relationship between event structures and occurrence nets: an occurrence net can be associated with a prime event structure, and vice versa. More generally, the relationships between various forms of event structures and suitable forms of nets have been long established. Good examples are the close relationship between inhibitor even…
▽ More
One of the well-known results in concurrency theory concerns the relationship between event structures and occurrence nets: an occurrence net can be associated with a prime event structure, and vice versa. More generally, the relationships between various forms of event structures and suitable forms of nets have been long established. Good examples are the close relationship between inhibitor event structures and inhibitor occurrence nets, or between asymmetric event structures and asymmetric occurrence nets. Several forms of event structures suited for the modelling of reversible computation have recently been developed; also a method for reversing occurrence nets has been proposed. This paper bridges the gap between reversible event structures and reversible nets. We introduce the notion of reversible causal net, which is a generalisation of the notion of reversible unfolding. We show that reversible causal nets correspond precisely to a subclass of reversible prime event structures, the causal reversible prime event structures.
△ Less
Submitted 24 October, 2019;
originally announced October 2019.
-
Reversing Place Transition Nets
Authors:
Hernán Melgratti,
Claudio Antares Mezzina,
Irek Ulidowski
Abstract:
Petri nets are a well-known model of concurrency and provide an ideal setting for the study of fundamental aspects in concurrent systems. Despite their simplicity, they still lack a satisfactory causally reversible semantics. We develop such semantics for Place/Transitions Petri nets (P/T nets) based on two observations. Firstly, a net that explicitly expresses causality and conflict among events,…
▽ More
Petri nets are a well-known model of concurrency and provide an ideal setting for the study of fundamental aspects in concurrent systems. Despite their simplicity, they still lack a satisfactory causally reversible semantics. We develop such semantics for Place/Transitions Petri nets (P/T nets) based on two observations. Firstly, a net that explicitly expresses causality and conflict among events, for example an occurrence net, can be straightforwardly reversed by adding a reverse transition for each of its forward transitions. Secondly, given a P/T net the standard unfolding construction associates with it an occurrence net that preserves all of its computation. Consequently, the reversible semantics of a P/T net can be obtained as the reversible semantics of its unfolding. We show that such reversible behaviour can be expressed as a finite net whose tokens are coloured by causal histories. Colours in our encoding resemble the causal memories that are typical in reversible process calculi.
△ Less
Submitted 15 October, 2020; v1 submitted 9 October, 2019;
originally announced October 2019.
-
On Resolving Non-determinism in Choreographies
Authors:
Laura Bocchi,
Hernan Melgratti,
Emilio Tuosto
Abstract:
Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g.…
▽ More
Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g., conditional statements) is necessary to correctly characterise the relationship between choreographies and their implementations with concrete programming languages. We introduce a notion of realisability for choreographies - called whole-spectrum implementation - where choices are still non-deterministic in choreographies, but are deterministic in their implementations. Our notion of whole spectrum implementation rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a non-deterministic choice. We give a type discipline for checking whole-spectrum implementations. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation.
△ Less
Submitted 22 September, 2020; v1 submitted 17 April, 2019;
originally announced April 2019.
-
Unifying Inference for Bayesian and Petri Nets
Authors:
Roberto Bruni,
Hernán Melgratti,
Ugo Montanari
Abstract:
Recent work by the authors equips Petri occurrence nets (PN) with probability distributions which fully replace nondeterminism. To avoid the so-called confusion problem, the construction imposes additional causal dependencies which restrict choices within certain subnets called structural branching cells (s-cells). Bayesian nets (BN) are usually structured as partial orders where nodes define cond…
▽ More
Recent work by the authors equips Petri occurrence nets (PN) with probability distributions which fully replace nondeterminism. To avoid the so-called confusion problem, the construction imposes additional causal dependencies which restrict choices within certain subnets called structural branching cells (s-cells). Bayesian nets (BN) are usually structured as partial orders where nodes define conditional probability distributions. In the paper, we unify the two structures in terms of Symmetric Monoidal Categories (SMC), so that we can apply to PN ordinary analysis techniques developed for BN. Interestingly, it turns out that PN which cannot be SMC-decomposed are exactly s-cells. This result confirms the importance for Petri nets of both SMC and s-cells.
△ Less
Submitted 17 July, 2018;
originally announced July 2018.
-
Event Structures for Petri nets with Persistence
Authors:
Paolo Baldan,
Roberto Bruni,
Andrea Corradini,
Fabio Gadducci,
Hernan Melgratti,
Ugo Montanari
Abstract:
Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures, called prime event structures, where each event has a u…
▽ More
Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures, called prime event structures, where each event has a uniquely determined set of causes. Prime event structures, in turn, can be identified with their domain of configurations. At a categorical level, this is nicely formalised by Winskel as a chain of coreflections.
Contrary to prime event structures, general event structures allow for the presence of disjunctive causes, i.e., events can be enabled by distinct minimal sets of events. In this paper, we extend the connection between Petri nets and event structures in order to include disjunctive causes. In particular, we show that, at the level of nets, disjunctive causes are well accounted for by persistent places. These are places where tokens, once generated, can be used several times without being consumed and where multiple tokens are interpreted collectively, i.e., their histories are inessential. Generalising the work on ordinary nets, Petri nets with persistence are related to a new subclass of general event structures, called locally connected, by means of a chain of coreflections relying on an unfolding construction.
△ Less
Submitted 27 September, 2018; v1 submitted 11 February, 2018;
originally announced February 2018.
-
Concurrency and Probability: Removing Confusion, Compositionally
Authors:
Roberto Bruni,
Hernán Melgratti,
Ugo Montanari
Abstract:
Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we propose a general solution based on a recursive, static decomposition of (occurrence) nets in loci of decision, called structural branching cells (s-cells). Each s-c…
▽ More
Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we propose a general solution based on a recursive, static decomposition of (occurrence) nets in loci of decision, called structural branching cells (s-cells). Each s-cell exposes a set of alternatives, called transactions. Our solution transforms a given Petri net into another net whose transitions are the transactions of the s-cells and whose places are those of the original net, with some auxiliary structure for bookkee**. The resulting net is confusion-free, and thus conflicting alternatives can be equipped with probabilistic choices, while nonintersecting alternatives are purely concurrent and their probability distributions are independent. The validity of the construction is witnessed by a tight correspondence with the recursively stopped configurations of Abbes and Benveniste. Some advantages of our approach are that: i) s-cells are defined statically and locally in a compositional way; ii) our resulting nets faithfully account for concurrency.
△ Less
Submitted 18 December, 2019; v1 submitted 12 October, 2017;
originally announced October 2017.
-
Multiparty testing preorders
Authors:
Rocco de Nicola,
Hernán Melgratti
Abstract:
Variants of the must testing approach have been successfully applied in service oriented computing for analysing the compliance between (contracts exposed by) clients and servers or, more generally, between two peers. It has however been argued that multiparty scenarios call for more permissive notions of compliance because partners usually do not have full coordination capabilities. We propose tw…
▽ More
Variants of the must testing approach have been successfully applied in service oriented computing for analysing the compliance between (contracts exposed by) clients and servers or, more generally, between two peers. It has however been argued that multiparty scenarios call for more permissive notions of compliance because partners usually do not have full coordination capabilities. We propose two new testing preorders, which are obtained by restricting the set of potential observers. For the first preorder, called uncoordinated, we allow only sets of parallel observers that use different parts of the interface of a given service and have no possibility of intercommunication. For the second preorder, that we call individualistic, we instead rely on parallel observers that perceive as silent all the actions that are not in the interface of interest. We have that the uncoordinated preorder is coarser than the classical must testing preorder and finer than the individualistic one. We also provide a characterisation in terms of decorated traces for both preorders: the uncoordinated preorder is defined in terms of must-sets and Mazurkiewicz traces while the individualistic one is described in terms of classes of filtered traces that only contain designated visible actions and must-sets.
△ Less
Submitted 4 January, 2023; v1 submitted 9 December, 2016;
originally announced December 2016.
-
Connector algebras for C/E and P/T nets' interactions
Authors:
Roberto Bruni,
Hernan Melgratti,
Ugo Montanari,
Pawel Sobocinski
Abstract:
A quite flourishing research thread in the recent literature on component-based systems is concerned with the algebraic properties of different classes of connectors. In a recent paper, an algebra of stateless connectors was presented that consists of five kinds of basic connectors, namely symmetry, synchronization, mutual exclusion, hiding and inaction, plus their duals, and it was shown how the…
▽ More
A quite flourishing research thread in the recent literature on component-based systems is concerned with the algebraic properties of different classes of connectors. In a recent paper, an algebra of stateless connectors was presented that consists of five kinds of basic connectors, namely symmetry, synchronization, mutual exclusion, hiding and inaction, plus their duals, and it was shown how they can be freely composed in series and in parallel to model sophisticated 'glues'. In this paper we explore the expressiveness of stateful connectors obtained by adding one-place buffers or unbounded buffers to the stateless connectors. The main results are: i) we show how different classes of connectors exactly correspond to suitable classes of Petri nets equipped with compositional interfaces, called nets with boundaries; ii) we show that the difference between strong and weak semantics in stateful connectors is reflected in the semantics of nets with boundaries by moving from the classic step semantics (strong case) to a novel banking semantics (weak case), where a step can be executed by taking some 'debit' tokens to be given back during the same step; iii) we show that the corresponding bisimilarities are congruences (w.r.t. composition of connectors in series and in parallel); iv) we show that suitable monoidality laws, like those arising when representing stateful connectors in the tile model, can nicely capture concurrency (in the sense of step semantics) aspects; and v) as a side result, we provide a basic algebra, with a finite set of symbols, out of which we can compose all P/T nets with boundaries, fulfilling a long standing quest.
△ Less
Submitted 14 September, 2013; v1 submitted 30 June, 2013;
originally announced July 2013.
-
Contracts for Abstract Processes in Service Composition
Authors:
Maria Grazia Buscemi,
Hernán Melgratti
Abstract:
Contracts are a well-established approach for describing and analyzing behavioral aspects of web service compositions. The theory of contracts comes equipped with a notion of compatibility between clients and servers that ensures that every possible interaction between compatible clients and servers will complete successfully. It is generally agreed that real applications often require the ability…
▽ More
Contracts are a well-established approach for describing and analyzing behavioral aspects of web service compositions. The theory of contracts comes equipped with a notion of compatibility between clients and servers that ensures that every possible interaction between compatible clients and servers will complete successfully. It is generally agreed that real applications often require the ability of exposing just partial descriptions of their behaviors, which are usually known as abstract processes. We propose a formal characterization of abstraction as an extension of the usual symbolic bisimulation and we recover the notion of abstraction in the context of contracts.
△ Less
Submitted 25 January, 2011;
originally announced January 2011.