Automatic exact reduction of Chemical Reaction Networks
CRNReducer is a Java tool for the automatic reduction of chemical reaction networks (CRN).
It exploits two novel reduction techniques, the Forward and Backward Bisimulations for CRNs, bringing to the chemical context well-established reduction techniques for models of computation based on the notion of bisimulation.
The tool supports the continuous-state semantics of CRNs based on the law of mass action, providing a system of ordinary differential equations (ODEs).
A Forward CRN bisimulation (FB) is an equivalence among species of a CRN inducing an ordinary lumpable partition of its ODEs. An FB-reduced CRN can be automatically computed, containing a species per block of FB-equivalent species of the original CRN. The solution of the ODEs of such reduced CRN gives the exact sum of the concentrations of the species belonging to each equivalence class.
A Backward CRN bisimulation (BB) is similar, but equivalent species have the same solution at all time points; in other words, a Backaward CRN bisimulation relates species whose ODE solutions are equal whenever they start from identical initial conditions. A BB-reduced CRN can as well be automatically computed, containing a representative species per block of BB-equivalent species of the original CRN.
The tool supports
- CRNs given in the .net format generated with the well-established tool BioNetGen version 2.2.5-stable.
- Continuous Time Markov chains in the .tra/.lab format of the state-of-the-art model checker MRMC.
- A compact CSV-like representation of Ax = b problems generated from Matlab matrices using a simple Matlab script.
This allowed us to validate our CRN bisimulations against a wide set of existing models in the literature. For the latter two classes of models we use the CRN encoding discussed here.
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Efficient Syntax-driven Lumping of Differential Equations (TR with proofs), 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Forward and Backward Bisimulations for Chemical Reaction Networks, 26th International Conference on Concurrency Theory (CONCUR 2015).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Satisfiability Modulo Differential Equivalence Relations, 43rd Annual Symposium on Principles of Programming Languages (POPL’16).
The current version of the tool can be found here: CRNReducer.
Currently, the tool has to be intended only as accompanying material for the paper presenting our novel efficient algorithm for computing CRN bisimulations submitted at TACAS 2016: Efficient Syntax-driven Lumping of Differential Equations, Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin. More features will follow.
For the sake of reproducibility, CRNReducer comes with all the models treated in the draft, stored in the folders “BNGNetworks” (M1-M13), “CompactMatrices” (F1-F5), and “MRMCMarkovChains” (C1-C3).
Our CRN bisimulations can be applied by just running the following command
java -Xmx8136M -jar CRNReducer.jar technique fileIn fileOut
where technique is either FB or BB to apply our Forward or Backward CRN reduction, respectively. We also allow for the two additional techniques FB_old and BB_old, meaning that the previous implementation used for the above CONCUR paper will be used.
For CTMCs, species/states are always pre-partitioned according to the provided labelling function. Instead, for BioNetGen files, in case the BB technique is used, then species are pre-partitioned in blocks of species with same initial conditions.
The parameter fileIn specifies the file containing the model to be reduced up to our CRN bisimulations, while fileOut is the file where to store the reduced CRN.
The latter file also contains information about the computed partition of species, preceding each species with a comment listing all the species of the corresponding block.
Example: reducing the running example of the paper up to forward bisimulation
java -Xmx8136M -jar CRNReducer.jar FB ./BNGNetworks/runningExample.net ./BNGNetworks/runningExampleFB.net Importing: ./BNGNetworks/runningExample.net Read parameters: 2, read species: 5, read CRNreactions: 4. FB partitioning ./BNGNetworks/runningExample.net ... (after FB pre-partitioning we have 4 blocks in 0.003 (s)) ... completed. From 5 species to 4 blocks. Time necessary: 0.009 (s). Reducing the CRN with respect to the obtained partition ... completed. Time necessary 0.003 (s). The original CRN: ./BNGNetworks/runningExample.net: 4 reactions, 5 species. The FB reduced CRN: 3 reactions, 4 species. The current CRN is updated with the reduced one. Writing the CRN in file ./BNGNetworks/runningExampleFB.net ... completed
Where the species of runningExample.net are
begin species 1 xA 1.0 2 xC 1.0 3 xE 1.0 4 xB 1.0 5 xD 1.0 end species
while the ones in runningExampleFB.net are (where // denotes comments)
begin species //Representative of block (with 2 species): // xA // xB 1 xA 2.0 //Representative of block (with 1 species): // xC 2 xC 1.0 //Representative of block (with 1 species): // xE 3 xE 1.0 //Representative of block (with 1 species): // xD 4 xD 1.0 end species
For suggestions, remarks, bugs or requests please do not hesitate to contact any of us.