Bisimilarities over stable configuration structures can be divided into three families. In the first one - including interleaving, step, pomset, and forward-reverse bisimilarities - no isomorphism is required between the events matched during the bisimulation game. In the second one - including weak history-preserving, weak history-preserving pomset, and weak hereditary history-preserving bisimilarities - a labeling- and causality-preserving isomorphism is required between matched events, which is specific to each pair of configurations related by the bisimulation relation and hence can vary for a matched event from pair to pair. In the third one - including history-preserving and hereditary history-preserving bisimilarities - a single isomorphism is built incrementally, which is therefore fixed for all matched events. We revisit true concurrency bisimilarities by introducing variants that additionally check that the backward ready multisets of related configurations coincide. While the distinguishing power of the bisimilarities of the second and third families does not change, the power of the revised bisimilarities of the first family is equal to that of the bisimilarities of the second family. The latter bisimilarities can thus be characterized by replacing variable isomorphisms with simply counting incoming transitions. In contrast, backward ready multisets are not enough to characterize the third family in the simultaneous presence of autoconcurrency and non-local conflicts. We show that a further check for the existence of diamond and half-diamond substructures is necessary in that case to achieve the same distinguishing power as incremental isomorphisms.

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.

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

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.