Hernán Melgratti

Florian Furbach, Lucas Clorius, Roland Kuhn et al.

Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.

Hernán Melgratti, Claudio Antares Mezzina, G. Michele Pinna

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.

Ugo de'Liguoro, Hernán Melgratti, Emilio Tuosto

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