In addition to forward computations, a reversible system also features backward computations along which the effects of forward ones can be undone. This is accomplished by reverting executed actions starting from the last one. Since the last performed action may not be uniquely identifiable in a concurrent setting, Danos and Krivine proposed causal reversibility: an executed action can be undone provided that all of its consequences have been undone already. Phillips and Ulidowski then showed how to define nondeterministic process calculi that meet causal reversibility by construction. Lanese, Phillips, and Ulidowski subsequently classified the basic properties that ensure causal reversibility. In this paper we investigate the extent to which those techniques apply to reversible nondeterministic process calculi that include quantitative aspects. Firstly, we consider the introduction of time described via numeric delays with action execution separated from time passing like in the calculus of Moller and Tofts, where actions can be lazy or eager and time is subject to time determinism and time additivity. Secondly, we address the introduction of probabilities like in the calculus of Hansson and Jonsson, in which action execution and probabilistic choices alternate. We show that both resulting reversible calculi satisfy causal reversibility provided that suitable variants of the aforementioned techniques are developed to guarantee the proper forward and backward interplay of nondeterminism and quantitative aspects. The use of the former calculus is illustrated on a timeout mechanism, whereas the use of the latter is exemplified on quantum teleportation.

We provide two alternative characterizations of hereditary history-preserving bisimilarity: a denotational one, on stable configuration structures, and an operational one, on a reversible process calculus. The characterizing equivalence is forward-reverse bisimilarity extended with a check for backward ready multiset equality. Unlike previous approaches, the focus is thus on counting identically labeled events rather than uniquely identifying them. We also investigate the relationships between event identifier logic, characterizing the former bisimilarity, and backward ready multiset logic, characterizing the latter bisimilarity.

Information flow theory aims at guaranteeing the absence of covert channels among different security levels. As for the verification of noninterference via equivalence checking, in nondeterministic and probabilistic settings weak bisimilarity is adequate only for forward-computing systems, while branching bisimilarity has turned out to be appropriate for reversible systems too. In this paper we investigate noninterference for deterministically timed systems based on the model of Moller and Tofts. After recasting a selection of noninterference properties via timed variants of weak and branching bisimilarities, we analyze their preservation and compositionality aspects, establish their taxonomy, and compare it with the nondeterministic taxonomy for (ir)reversible systems. We illustrate the adequacy of our proposal on real-time database transactions.

We devise two complementary characterizations of hereditary history-preserving bisimilarity (HHPB): a denotational one, based on stable configuration structures, and an operational one, formulated in a reversible process calculus. Our characterizations rely on forward-reverse bisimilarity augmented with backward ready multiset equality. This shifts the emphasis from uniquely identifying events, as done in previous characterizations, to counting occurrences of identically labeled events associated with incoming transitions, which yields a more lightweight behavioral equivalence than HHPB. We show that our characterizations correctly distinguish between autoconcurrency and autocausation, but are valid only in the absence of non-local conflicts. We then study the logical foundations of these characterizations by relating event identifier logic, which captures the classical view of HHPB, and backward ready multiset logic, developed for our new equivalence.

Blockchains are widely recognized for their immutability, which provides robust guarantees of data integrity and transparency. However, this same feature poses significant challenges in real-world situations that require regulatory compliance, correction of erroneous data, or removal of sensitive information. Redactable blockchains address the limitations of traditional ones by enabling controlled, auditable modifications to blockchain data, primarily through cryptographic mechanisms such as chameleon hash functions and alternative redaction schemes. This report examines the motivations for introducing redactability, surveys the cryptographic primitives that enable secure edits, and analyzes competing approaches and their shortcomings. Special attention is paid to the practical deployment of redactable blockchains in private settings, with discussions of use cases in healthcare, finance, Internet of drones, and federated learning. Finally, the report outlines further challenges, also in connection with reversible computing, and the future potential of redactable blockchains in building law-compliant, trustworthy, and scalable digital infrastructures.

Information and communication technologies are by now employed in most activities, including economics and finance. Despite the extraordinary power of modern computers and the vast amount of memory, some results of theoretical computer science imply the impossibility of certifying software quality in general. With the exception of safety-critical systems, this has primarily concerned the information processed by confined systems, with limited socio-economic consequences. In the emerging era of technologies for exchanging digital money and tokenized assets over the Internet - such as central bank digital currencies (CBDCs) - even a minor bug could trigger a financial collapse. Although the aforementioned impossibility results cannot be overcome in an absolute sense, there exist formal methods that can provide assertions of computing systems correctness. We advocate their use to validate the operational resilience of software infrastructures enabling CBDCs, with special emphasis on offline payments as they constitute a very critical issue.

The theory of noninterference supports the analysis of information leakage and the execution of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on weak bisimulation semantics. We show that this approach is not sufficient to identify potential covert channels in the presence of reversible computations. As illustrated via a database management system example, the activation of backward computations may trigger information flows that are not observable when proceeding in the standard forward direction. To capture the effects of back-and-forth computations, it is necessary to switch to a more expressive semantics, which has been proven to be branching bisimilarity in a previous work by De Nicola, Montanari, and Vaandrager. In this paper we investigate a taxonomy of noninterference properties based on branching bisimilarity along with their preservation and compositionality features, then we compare it with the taxonomy of Focardi and Gorrieri based on weak bisimilarity.

Noninterference theory aims at ensuring the absence of covert channels among different security levels. As far as the verification of information-flow properties via equivalence checking is concerned, in nondeterministic and probabilistic settings weak bisimilarity has turned out to be adequate only for standard systems, while branching bisimilarity has proven to be appropriate for reversible systems too. In this paper we investigate noninterference for stochastically timed systems represented in the interactive Markov chain model of Hermanns. After recasting a selection of noninterference properties via Markovian variants of weak and branching bisimilarities, we study their preservation and compositionality aspects, build their taxonomy, and compare it with the nondeterministic and probabilistic taxonomies. We show the adequacy of our proposal through some examples about a database management system.

In the decentralized finance landscape, algorithmic stablecoins offer a promising solution for stabilizing the value of cryptocurrencies without relying on centralized collaterals. However, models like the dual-token system are vulnerable to depeg events, as demonstrated by the catastrophic collapse of the Terra-Luna ecosystem in 2022, which saw over 50 billion dollars in market capitalization evaporate in just a few days. This work proposes DualTokenSim, a Python simulator designed to analyze the behavior of cryptocurrencies based on the dual-token model under both normal and panic scenarios. The simulator uses automated market makers and a stochastic process to simulate price dynamics and user behavior. The aim is to offer an environment in which to explore and analyze solutions for improving the resilience of algorithmic stablecoins during periods of market instability.

The theory of noninterference supports the analysis of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on bisimilarity. In a nondeterministic setting, assessing noninterference through weak bisimilarity is adequate for irreversible systems, whereas for reversible ones branching bisimilarity has been recently proven to be more appropriate. In this paper we address the same two families of systems with the difference that probabilities come into play in addition to nondeterminism according to the alternating model of Hansson and Jonsson. For irreversible systems we extend the results of Aldini, Bravetti, and Gorrieri developed in a generative-reactive probabilistic setting, while for reversible systems we extend the results of Esposito, Aldini, Bernardo, and Rossi developed in a purely nondeterministic setting. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities for irreversible and reversible systems, respectively. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with earlier taxonomies. The adequacy of the extended noninterference theory is illustrated via a probabilistic smart contract lottery.

Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake consensus via cryptographic self-sortition and binary Byzantine agreement. In this paper, we present a process algebraic model of the Algorand consensus protocol with the aim of enabling rigorous formal verification. Our model captures the behavior of participants with respect to the structured alternation of consensus steps toward a committee-based agreement by means of a probabilistic process calculus. We validate the correctness of the protocol in the absence of adversaries and then extend our model to capture the influence of coordinated malicious nodes that can force the commit of an empty block instead of the proposed one. The adversarial scenario is analyzed by using an equivalence-checking-based noninterference framework that we have implemented in the CADP verification toolkit. In addition to highlighting both the robustness and the limitations of the Algorand protocol under adversarial assumptions, this work illustrates the added value of using formal methods for the analysis of blockchain consensus algorithms.

Reversible systems exhibit both forward computations and backward computations, where the aim of the latter is to undo the effects of the former. Such systems can be compared via forward-reverse bisimilarity as well as its two components, i.e., forward bisimilarity and reverse bisimilarity. The congruence, equational, and logical properties of these equivalences have already been studied in the setting of sequential processes. In this paper we address concurrent processes and investigate compositionality and axiomatizations of forward bisimilarity, which is interleaving, and reverse and forward-reverse bisimilarities, which are truly concurrent. To uniformly derive expansion laws for the three equivalences, we develop encodings based on the proved trees approach of Degano & Priami. In the case of reverse and forward-reverse bisimilarities, we show that in the encoding every action prefix needs to be extended with the backward ready set of the reached process.

Noninterference theory supports the analysis of secure computations in multi-level security systems. In the nondeterministic setting, the approach to noninterefence based on weak bisimilarity has turned out to be inadequate for reversible systems. This drawback can be overcome by employing a more expressive semantics, which has been recently proven to be branching bisimilarity. In this paper we extend the result to reversible systems that feature both nondeterminism and probabilities. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with the nondeterministic taxonomy. The adequacy of the resulting noninterference theory for reversible systems is illustrated via a probabilistic smart contract example.

A reversible system features not only forward computations, but also backward computations along which the effects of forward ones can be undone by starting from the last performed action. According to causal reversibility, an executed action can be undone provided that all the actions it caused have been undone already. We investigate causal reversibility in a nondeterministic and probabilistic setting by adapting the framework of Phillips and Ulidowski to define a reversible calculus in which action transitions and probabilistic transitions alternate in the style of Hansson and Jonsson. We show that the calculus meets causal reversibility through a suitable variant of the technique of Lanese, Phillips, and Ulidowski that ensures the proper forward and backward interplay of nondeterminism and probabilities. The use of the calculus is illustrated on a quantum computing example.

Reversible systems feature both forward computations and backward computations, where the latter undo the effects of the former in a causally consistent manner.The compositionality properties and equational characterizations of strong and weak variants of forward-reverse bisimilarity as well as of its two components, i.e., forward bisimilarity and reverse bisimilarity, have been investigated on a minimal process calculus for nondeterministic reversible systems that are sequential, so as to be neutral with respect to interleaving vs. truly concurrent semantics of parallel composition.In this paper we provide logical characterizations for the considered bisimilarities based on forward and backward modalities, which reveals that strong and weak reverse bisimilarities respectively correspond to strong and weak reverse trace equivalences.Moreover, we establish a clear connection between weak forward-reverse bisimilarity and branching bisimilarity, so that the former inherits two further logical characterizations from the latter over a specific class of processes.

The theory of noninterference supports the analysis and the execution of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on weak bisimulation semantics. We show that this approach is not sufficient to identify potential covert channels in the presence of reversible computations. As illustrated via a database management system example, the activation of backward computations may trigger information flows that are not observable when proceeding in the standard forward direction. To capture the effects of back and forth computations, it is necessary to move to a sufficiently expressive semantics that, in an interleaving framework, has been proven to be branching bisimilarity in a previous work by De Nicola, Montanari, and Vaandrager. In this paper we investigate a taxonomy of noninterference properties based on branching bisimilarity along with their preservation and compositionality features, then we compare it with the classical hierarchy based on weak bisimilarity.

In higher education two key factors for achieving resilience during an emergency are the presence of a teaching and learning center, in charge of supervising all the switchover activities and providing daily assistance to lecturers and students, and the adoption of a variety of technological tools, each with a specific purpose but used in a coordinated way. In this paper we illustrate the rapid transition in the second half of the academic year 2019/2020 to massive distance learning and online exams guided by the teaching and learning center of the University of Urbino. The toolset featured the learning management system Moodle and the webconference tool Blackboard Collaborate, both employed for online lectures and oral exams, together with the e-proctoring tool Smowl for computer monitoring and the webconference tool Google Meet used on students smartphones for environmental monitoring, additionally employed for online written exams. We finally present the outcome of a survey of students opinions on massive distance learning.

A reversible computing system features backward computations along which the effects of forward ones are undone when needed. This is accomplished by reverting executed actions from the last one. Since the last performed action may not be uniquely identifiable in a concurrent system, causal reversibility is considered: an executed action can be undone provided that all of its consequences have been undone already. We investigate causal reversibility in a timed setting by defining a reversible calculus in the style of Phillips and Ulidowski in which action execution is separated from time passing, actions can be lazy or eager, and time is described via numeric delays subject to time additivity. We show that the calculus meets causal reversibility through an adaptation of the technique of Lanese, Phillips, and Ulidowski that ensures a proper treatment of action laziness/eagerness as well as time-additive delays.

Causal reversibility blends reversibility and causality for concurrent systems. It indicates that an action can be undone provided that all of its consequences have been undone already, thus making it possible to bring the system back to a past consistent state. Time reversibility is instead considered in the field of stochastic processes, mostly for efficient analysis purposes. A performance model based on a continuous-time Markov chain is time reversible if its stochastic behavior remains the same when the direction of time is reversed. We bridge these two theories of reversibility by showing the conditions under which causal reversibility and time reversibility are both ensured by construction. This is done in the setting of a stochastic process calculus, which is then equipped with a variant of stochastic bisimilarity accounting for both forward and backward directions.