Three Behavioural Equivalences for Chemical Reaction Networks

Chemical reaction networks (CRNs) can be seen a compact language for parallel computation, where the output of an algorithm is given by the concentration of the species at some point in time according to an underlying semantics based on continuous-time Markov chains (CTMCs) or on ordinary differential equations (ODEs).

Using a species-as-process analogy, we study behavioural equivalences over species of a CRN inspired by traditional approaches in established models of computation such as labelled transition systems. We define three equivalences in the Larsen-Skou style of probabilistic bisimulation that identify a partition of the species such that the dynamics of a CRN can be described only in terms of the equivalence classes. In Exact Fluid Lumpability, equivalent species have the same ODE solutions when starting from identical initial conditions. In Differential Species Bisimulation, each equivalence class represents the exact sum of the ODE trajectories of its member species. In Markovian Species Bisimulation, a partition over species identifies an exact aggregation in terms of ordinary lumpability over the states of the underlying CTMC.

For each equivalence relation we develop an efficient partition-refinement algorithm for computing the coarsest aggregations. Using a prototypal implementation, we find significant reductions in a number of models of biological processes available in the literature.

This is joint work with Luca Cardelli, Max Tschaikowski, and Andrea Vandin.