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.

翻译：可逆系统兼具前向计算与后向计算，其中后向计算以前因后果一致的方式撤销前向计算的效果。本文针对顺序型非确定性可逆系统中强/弱变体的正向-反向互模拟及其两个组成成分（即正向互模拟与反向互模拟）的组合性质与等式特征进行了研究，在最小进程演算框架下展开分析，从而保持对并行组合的交替语义与真并发语义的中立性。我们基于前向与后向模态词为所考察的互模拟关系提供了逻辑刻画，揭示出强反向互模拟与弱反向互模拟分别对应于强反向迹等价与弱反向迹等价。此外，我们建立了弱正向-反向互模拟与分支互模拟之间的明确关联，使得前者在特定进程类上继承了后者的两种进一步逻辑特征刻画。