Evaluation and Reduction of Ordinary Differential Equations
ERODE is a software tool for the solution and exact reduction of systems of ordinary differential equations (ODEs).
The tool supports two recently introduced, complementary, equivalence relations over ODE variables: forward differential equivalence partitions ODE variables into blocks for which a self-consistent aggregate ODE system can be obtained; each aggregate ODE gives the cumulative dynamics of the sum of the original variables in the respective equivalence class. Backward differential equivalence identifies variables that have identical solutions whenever starting from the same initial conditions.
ERODE uses a backend based on the well-known Z3 SMT solver to compute the coarsest equivalence that refines a given initial partition. In the special case of ODEs with polynomial derivatives of degree at most two, covering elementary chemical reaction networks (CRNs) and continuous time Markov chains (CTMCs), it implements a more efficient partition-refinement algorithm.
The tool supports ODE systems or chemical reaction networks written in a proprietary format, but also supports a number of existing formats. Examples are:
- Matlab‘s ODE systems;
- CRNs in the .net format generated with the well-established tool BioNetGen version 2.2.5-stable;
- CTMCs in the explicit .tra format generated by the model checkers MRMC and PRISM.
This allowed us to validate our techniques against a wide set of existing models in the literature (see our publication list below).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations, 23rd Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective, 35th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS’16).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Symbolic Computation of Differential Equivalences, 43rd Annual Symposium on Principles of Programming Languages (POPL’16).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Efficient Syntax-driven Lumping of Differential Equations, 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Forward and Backward Bisimulations for Chemical Reaction Networks, 26th International Conference on Concurrency Theory (CONCUR’15).
- Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, Syntactic Markovian Bisimulation for Chemical Reaction Networks, Kim Larsen’s Festschrift, 2017 (KimFest).
A tutorial-like overview of the theory at the basis of ERODE can be found here:
- Andrea Vandin, and Mirco Tribastone, Quantitative Abstractions for Collective Adaptive Systems, 16th International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM’16).
Download and Installation
ERODE is a multi-platform application based on the Eclipse framework. It does not require any installation process, apart from a working installation of Java 8.
Manual and Examples
Detailed information about installation and usage of ERODE, as well as a collection of ERODE models are available at:
ERODE at a glance
ERODE‘s architecture is organised in three layers. The presentation layer, concerned with the user interface, features the following components: a fully-featured text editor based on the Xtext framework (supporting syntax highlighting, and content assist); a plot view to display ODE solutions; and a console view to display diagnostic information (warnings, model reduction statistics, etc.).
The core layer implements the data structures and the model reduction algorithms, including a wrapper to Z3 via its Java bindings. The analysis layer supports ODE numerical solution by means of the Apache Commons Maths library.
An ERODE specification (with file extension .ode) is made of six blcoks: (i) parameters (e.g., reaction rates); (ii) variable names and their (optional) initial conditions; (iii) initial partition of variables; (iv) ODE system; (v) observables, called views; (vi) commands for ODE reduction and numerical solution, and to export in other formats.
Notably, ERODE supports two formats for the specification of an ODE system: directly as a list of equations, or in a reaction-network style. With the latter, by simple static analysis it is possible to enable the faster reductions up to forward/backward bisimulation (see our TACAS’16 and CONCUR’15 papers).
The two alternative specification formats are shown below as separate (commented) examples below. They describe the same model, which corresponds to an idealised biochemical interaction between two molecules, A and B, where A can be in two states (u for unphosphorylated and p for phosphorylated) undergoing binding/unbinding with B. This results in five biochemical species: Au, Ap, B, AuB, and ApB. Each species corresponds to one ODE variable, which models its concentration as a function of time.
For suggestions, remarks, bugs or requests please do not hesitate to contact any of us (in alphabetical order):
We thank Lavinia Mariotti, MArch, for the design of ERODE’s logo.