Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a fundamental 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 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.

Undoing computations of a concurrent system is beneficial in many situations, such as in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation, including process calculi such as CCS, languages like Erlang, and abstract models such as prime event structures and occurrence nets. However, it has not been settled as to what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between various reversibility properties. In particular, we show how all properties we consider are derivable from a set of axioms. Our intention is that when establishing properties of some formalism, it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new properties related to causal-consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all of the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.

Inspired by the biological evolution, this paper proposes an evolutionary synthesis mechanism to automatically evolve DenseNet towards high sparsity and efficiency for medical image classification. Unlike traditional automatic design methods, this mechanism generates a sparser offspring in each generation based on its previous trained ancestor. Concretely, we use a synaptic model to mimic biological evolution in the asexual reproduction. Each generation’s knowledge is passed down to its descendant, and an environmental constraint limits the size of the descendant evolutionary DenseNet, moving the evolution process towards high sparsity. Additionally, to address the limitation of ensemble learning that requires multiple base networks to make decisions, we propose an evolution-based ensemble learning mechanism. It utilises the evolutionary synthesis scheme to generate highly sparse descendant networks, which can be used as base networks to perform ensemble learning in inference. This is specially useful in the extreme case when there is only a single network. Finally, we propose the MEEDNets (Medical Image Classification via Ensemble Bio-inspired Evolutionary DenseNets) model which consists of multiple evolutionary DenseNet-121s synthesised in the evolution process. Experimental results show that our bio-inspired evolutionary DenseNets are able to drop less important structures and compensate for the increasingly sparse architecture. In addition, our proposed MEEDNets model outperforms the state-of-the-art methods on two publicly accessible medical image datasets. All source code of this study is available at https://github.com/hengdezhu/MEEDNets.

We have demonstrated in previous work that the Calculus of Covalent Bonding (CCB) can be used to simulate higher-level biochemical processes. This is significant since CCB was originally devised to model lower-level organic chemical reactions. In this paper we extend the use of the calculus to model an important gene repair pathway, namely DNA Mismatch Repair (MMR). This complex pathway involves four helper proteins and needs a distinction between the two chains in a DNA strand. In order to achieve this, we extend the calculus by allowing prefixing with collections of bonding sites.

Abstract Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between these properties. In particular, we show how they are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.

In this paper we introduce Event Identifier Logic (EIL), which extends Hennessy–Milner logic by the addition of: (1) reverse as well as forward modalities; and (2) identifiers to keep track of events. We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particular true-concurrency model, namely, stable configuration structures. We also show how natural sublogics of EIL correspond to coarser equivalences. In particular, we provide logical characterisations of weak-history- preserving (WH) and history-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation have been given previously, but none, as far as we are aware, corresponding to WH bisimulation (when autoconcurrency is allowed). We also present characteristic formulas that characterise individual structures with respect to history-preserving equivalences.

Van Glabbeek and Goltz (and later Fecher) have investigated the relationships between various equivalences on stable configuration structures, including interleaving bisimulation (IB), step bisimulation (SB), pomset bisimulation and hereditary history-preserving (H-H) bisimulation. Since H-H bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate these and other forms of bisimulations where both forward and reverse transitions are allowed. Bednarczyk asked whether SB with reverse steps is as strong as H-H bisimulation. We answer this question negatively. We give various characterisations of SB with reverse steps, showing that forward steps do not add power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as H-H bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration. We consider several other forms of observations of reversible behaviour and define a wide range of bisimulations by mixing the forward and reverse observations. We investigate the power of these bisimulations and represent the relationships between them as a hierarchy with IB at the bottom and H-H at the top.

The finest observable and implementable equivalence on concurrent processes is sought as part of a larger program to develop a theory of observable processes where semantics of processes are based on locally and finitely observable process behavior and all process constructs are allowed, provided their operational meaning is defined by realistically implementable transition rules. The structure of transition rules is examined, and several conditions that all realistically implementable rules should satisfy are proposed. It is shown that the ISOS contexts capture exactly the observable behavior of processes. This leads to the result that copy plus refusal equivalence is the finest implementable equivalence.>