Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a main concept in computing, with applications ranging from debugging and fault tolerance to biological and quantum systems. CCSK, a reversible extension of CCS, is a paradigmatic model of reversible concurrent computation. In this paper, we investigate the encodability of CCSK into classical forward-only concurrent models. We establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the π-calculus, highlighting the strong impact of reversibility on the expressive power. We then present an encoding of CCSK processes with only top-level parallel composition into the internal π-calculus, correct up to strong bisimilarity. We also identify a fundamental limitation: no parallel-preserving encoding of CCSK (with arbitrary parallel composition) into the π-calculus can be correct up to strong bisimilarity. Finally, we provide a parallel-preserving encoding correct under a weaker behavioural correspondence: weak mutual simulation. Our findings extend the literature of encodability results to reversible process calculi.

In the context of CCSK, a reversible extension of CCS, we study different notions of bisimilarity (strong/weak, forward-only/reversible) and highlight their differences and commonalities. In particular, for the weak reversible case, not previously studied in the literature, we propose two variants, dubbed directional and mixed bisimilarity, depending on whether τ actions should be in the same direction (forward/backward) as the action being matched or not. We show, in particular, that mixed bisimilarity is a congruence and completely abstracts away from τ actions.

Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions with concurrency primitives) is not reversible, since it discards information while computing forwards. For instance, it does not satisfy the so-called Loop Lemma, stating that any reduction has an inverse, a main property of reversibility in process calculi, where a small-step semantics is commonly used. We present in this paper a novel small-step semantics which is actually reversible (for well-formed Janus programs), while remaining equivalent to the previous one. In particular, this involves the non-trivial challenge of defining a semantics based on a “program counter” for a high-level programming language.

Modern cloud-native systems require adapting dynamically to changing operational conditions, including service outages, traffic surges, and evolving user requirements. While existing benchmarks provide valuable testbeds for performance and scalability evaluation, they lack explicit support for studying adaptation mechanisms, reconfiguration strategies, and graceful degradation. These limitations hinder systematic research on self-adaptive architectures in realistic cloud environments. To cover this gap, we introduce Adaptable TeaStore, an extension of the renowned TeaStore architecture that incorporates adaptability as a first-class design concern. Our extension distinguishes between mandatory and optional services, supports multiple component versions-with varying resource requirements and functionality levels-considers the outsourcing of functionalities to external providers, and provides local cache mechanisms for performance and resilience. These features enable the systematic exploration of reconfiguration policies across diverse operational scenarios. We discuss a broad catalogue of reference adaptation scenarios centred around Adaptable Tea-Store, useful to evaluate the ability of a given adaptation technology to address conditions such as component unavailability, cyberattacks, provider outages, benign/malicious traffic increases, and user-triggered reconfigurations. Moreover, we present an open-source implementation of the architecture with APIs for metrics collection and adaptation triggers, to enable reproducible experiments.

Current choreography-based approaches to the specification and implementation of distributed systems lack support when it comes to program understanding. In particular, we miss systematic methodologies and algorithms to take a message-passing program written in a mainstream programming language and automatically produce a global description of all its communication behaviors. This helps understanding the program interaction patterns and also highlights possible unexpected behaviors to support debugging. We discuss the requirements and difficulties of the approach we envisage. Through concrete examples we outline the kind of global descriptions we want to obtain.

Distributed systems can be subject to various kinds of partial failures, therefore building fault-tolerance or failure mitigation mechanisms for distributed systems remains an important domain of research. In this paper, we present a calculus to formally model distributed systems subject to crash failures with recovery. The recovery model considered in the paper is weak, in the sense that it makes no assumption on the exact state in which a failed node resumes its execution, only its identity has to be distinguishable from past incarnations of itself. Our calculus is inspired in part by the Erlang programming language and in part by the distributed π-calculus with nodes and link failures (DπF) introduced by Francalanza and Hennessy. In order to reason about distributed systems with failures and recovery we develop a behavioral theory for our calculus, in the form of a contextual equivalence, and of a fully abstract coinductive characterization of this equivalence by means of a labelled transition system semantics and its associated weak bisimilarity. This result is valuable for it provides a compositional proof technique for proving or disproving contextual equivalence between systems.

The use of AI in microservices (MSs) is an emerging field as indicated by a substantial number of surveys. However these surveys focus on a specific problem using specific AI techniques, therefore not fully capturing the growth of research and the rise and disappearance of trends. In our systematic mapping study, we take an exhaustive approach to reveal all possible connections between the use of AI techniques for improving any quality attribute (QA) of MSs during the DevOps phases. Our results include 16 research themes that connect to the intersection of particular QAs, AI domains and DevOps phases. Moreover by mapping identified future research challenges and relevant industry domains, we can show that many studies aim to deliver prototypes to be automated at a later stage, aiming at providing exploitable products in a number of key industry domains.

In the setting of Petri nets, we prove that causal-net bisimilarity , which is a refinement of history-preserving bisimilarity , and the novel hereditary causal-net bisimilarity, which is a refinement of hereditary history-preserving bisimilarity , do coincide. This means that causal-net bisimilarity is a reversible behavioral equivalence, as causal-net bisimilar markings not only are able to match each other's forward transitions, but also backward transitions by undoing performed events. Causal-net bisimilarity can be equivalently formulated as structure-preserving bisimilarity , that is decidable on finite bounded Petri nets . Moreover, place bisimilarity , that we prove to be finer than causal-net bisimilarity, is also reversible and it was proved decidable for finite Petri nets in . These results offer two decidable reversible behavioral equivalences in the true concurrency spectrum, which are alternative to the coarser hereditary history-preserving bisimilarity , that, unfortunately, is undecidable even for safe Petri nets .

In the setting of Petri nets, we prove that {\em causal-net bisimilarity} \cite{G15,Gor22,Gor25a}, which is a refinement of history-preserving bisimilarity \cite{RT88,vGG89,DDM89}, and the novel {\em hereditary} causal-net bisimilarity, which is a refinement of hereditary history-preserving bisimilarity \cite{Bed91,JNW96}, do coincide. This means that causal-net bisimilarity is a {\em reversible behavioral equivalence}, as causal-net bisimilar markings not only are able to match each other's forward transitions, but also backward transitions by undoing performed events. Causal-net bisimilarity can be equivalently formulated as {\em structure-preserving bisimilarity} \cite{G15,Gor25a}, that is decidable on finite bounded Petri nets \cite{CG21a}. Moreover, place bisimilarity \cite{ABS91}, that we prove to be finer than causal-net bisimilarity, is also reversible and it was proved decidable for finite Petri nets in \cite{Gor21decid,Gor25a}. These results offer two decidable reversible behavioral equivalences in the true concurrency spectrum, which are alternative to the coarser hereditary history-preserving bisimilarity \cite{Bed91,JNW96}, that, unfortunately, is undecidable even for safe Petri nets \cite{JNS03}.

Complex coordination protocols are necessary to manage complex organisations. The healthcare management sector is no exception, since different authorities, users, and systems have to interact with each other in order to achieve their organisational goals. In this paper we consider a case study on the authorisation and accreditation of healthcare structures in the Emilia Romagna region in Italy. We specify the case study using global choreographies so to enable the analysis of the correctness of its communication patterns using the tool. This requires to refine and its underlying theoretical framework. First, we extend to support not only asynchronous communication, but also synchronous one. Moreover, in both the cases, we provide a more efficient algorithm to check closure properties ensuring realisability of choreographies. The new algorithm allows us to check realisability of larger pomsets than before, which makes our approach viable for complex systems such as our case study.

The axiomatic approach to causal-consistent reversibility allows one to prove relevant properties of concurrent reversible formalisms, such as causal consistency, causal safety and causal liveness, by checking a few simple axioms. The approach works on Labeled Transition Systems equipped with a notion of Independence (LTSIs). Even if the axioms are quite simple, verifying them on non-trivial LTSIs is time consuming and involves a few subtleties. We present Tallulah, a tool which allows one to automatically verify various axioms on concrete LTSIs, suggests how to patch the LTSI when some axiom does not hold, and colors the transitions to highlight when they belong to the same event.

The Adaptable TeaStore has recently been proposed as a reference model for adaptable microservice architectures. It includes different configurations, as well as scenarios requiring to transition between them. We describe an implementation of the Adaptable TeaStore based on AIOCJ, a choreographic language that allows one to program multiparty systems that can adapt at runtime to different conditions. Following the choreographic tradition, AIOCJ ensures by-construction correctness of communications (e.g., no deadlocks) before, during, and after adaptation. Adaptation is dynamic, and the adaptation scenarios need to be fully specified only at runtime. Using AIOCJ to model the Adaptable TeaStore, we showcase the strengths of the approach and its current limitations, providing suggestions for future directions for refining the paradigm (and the AIOCJ language, in particular), to better align it with real-world Cloud architectures.

According to Landauer’s principle, any non-reversible system can be made reversible -that is, capable of undoing its actions- by keeping information about the past of the computation. In the area of concurrent and distributed systems, this often takes the form of memories. Memories are special devices that keep track of past states of a system execution. Memories can be looked up to restore past states, upon necessity. This paper investigates and lays down ideas on how to achieve reversibility in systems that are subject to events that, as a side effect, erase some memories, creating then holes in the structure of memories. The chosen application area is concurrent and distributed systems, where the events erasing memories are the failure of nodes.

Janus is an imperative, sequential language for reversibility. While heavily studied in the reversibility literature, to the best of our knowledge, no small-step semantics for it exists. Hence, we propose a small-step semantics for Janus and we prove it equivalent to a big-step semantics from the literature, for programs that have no runtime errors and no divergence. Our main motivation is to enable a future extension of Janus with concurrency primitives, which is more easily defined on top of a small-step semantics. As additional feature, a small-step semantics allows one to more easily distinguish between failing and non-terminating computations.

Multiparty Session Types (MPSTs) offer a structured way of specifying communication protocols and guarantee relevant communication properties, such as deadlock-freedom. In this paper, we extend a minimal MPST system with quantum data and operations, enabling the specification of quantum protocols. Quantum MPSTs (QMPSTs) provide a formal notation to describe quantum protocols, both at the abstract level of global types, describing which communications can take place in the system and their dependencies, and at the concrete level of local types and quantum processes, describing the expected behavior of each participant in the protocol. Type-checking relates these two levels formally, ensuring that processes behave as prescribed by the global type. Beyond usual communication properties, QMPSTs also allow us to prove that qubits are owned by a single process at any time, capturing the quantum no-cloning and no-deleting theorems. We use our approach to verify four quantum protocols from the literature, respectively Teleportation, Secret Sharing, Bit-Commitment, and Key Distribution.

Choreographic models in general, and Choreographic Automata (CA) in particular, can be used to analyze and validate communicating systems. We applied CAs to a case study in healthcare management, the procedure for accreditation and authorization of public and private healthcare structures in the Emilia Romagna region (Italy). We formalized the procedure first using a BPMN collaboration diagram as intermediate step, and then using CAs. The tool Corinne showed a few issues in the formalized model, but it turned out that such issues were due to too strict requirements posed by the theory underlying Corinne. This gave us useful feedback for future improvements of Corinne and its underlying theory.

This talk presents the notion of causal-consistent reversible debugging and its instance on Erlang provided by CauDEr. Reversible debugging allows us to explore an execution back and forth looking for a bug. Causal-consistent debugging tailors this approach to concurrent systems so that actions can be undone in any order as long as their consequences, if any, are undone first.

According to Landauer’s principle, any non-reversible system can be made reversible -that is, capable of undoing its actions- by keeping information about the past of the computation. In the area of concurrent and distributed systems, this often takes the form of memories. Memories are special devices that keep track of past states of a system execution. Memories can be looked up to restore past states, upon necessity. This paper investigates and lays down ideas on how to achieve reversibility in systems that are subject to events that, as a side effect, erase some memories, creating then holes in the structure of memories. The chosen application area is concurrent and distributed systems, where the events erasing memories are the failure of nodes.

Reversible computing is a programming paradigm allowing one to execute programs both in the standard, forward direction as well as backwards, recovering past states. A relevant application of reversible computing is causal-consistent reversible debugging, which allows one to explore concurrent computations backwards and forwards to find a bug. The basic idea is that any action can be undone, provided that its consequences are undone beforehand. This approach has been put into practice in CauDEr, a Causal-consistent reversible Debugger for the Erlang programming language. CauDEr provides the ability to explore a concurrent computation back and forward in a step-by-step way as well as to undo an action far in the past including all and only its consequences (rollback), and to replay an action from a log, together with its causes. CauDEr supports the functional, concurrent and distributed fragment of Erlang. However, Erlang also includes imperative primitives to manage a map (shared among all the processes of a same node) associating process identifiers to names. Here we extend CauDEr and the related theory, including rollback and replay, to support such imperative primitives. From a theoretical point of view, the imperative primitives create different causal structures to those derived from the concurrent Erlang fragment previously handled in CauDEr, yet we show that the main results proved for previous versions of CauDEr are still valid. From a practical point of view, this allows one to debug a larger subset of Erlang programs, as shown with a small case study of a server providing mathematical functionalities.