Evaluation and Reduction of Ordinary Differential Equations
Quick Links
Summary
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 selfconsistent 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 wellknown 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 partitionrefinement 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 wellestablished tool BioNetGen version 2.2.5stable;
This allowed us to validate our techniques against a wide set of existing models in the literature (see our publication list below).
Publications
 Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, Maximal aggregation of polynomial dynamical systems, Proceedings of the National Academy of Sciences (PNAS).
 Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective, Theoretical Computer Science (TCS).
 Stefano Tognazzi, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, Backward Invariance for Linear Differential Algebraic Equations, (CDC’18)
 Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, Guaranteed Error Bounds on Approximate Model Abstractions through Reachability Analysis (QEST’18).
 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).
 Stefano Tognazzi, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin, EGAC: a genetic algorithm to compare chemical reaction networks The Genetic and Evolutionary Computation Conference (GECCO’17).
 Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin, Syntactic Markovian Bisimulation for Chemical Reaction Networks, Kim Larsen’s Festschrift, 2017 (KimFest).
 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 Syntaxdriven 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).
Tutoriallike overviews of the ERODE and of the theory on which it is based
 Mirco Tribastone, and Andrea Vandin, Speeding up Stochastic and Deterministic Simulation by Aggregation: an Advanced Tutorial, 51st Winter Simulation Conference (WSC’18). [SLIDES]
 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). [SLIDES PART1 PART2]
Download and Installation
ERODE is a multiplatform 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 fullyfeatured 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.
ERODE’s language
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 reactionnetwork style. With the latter, by simple static analysis it is possible to enable the faster reductions up to forward/backward bisimulation (see our PNAS, 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.
About
For suggestions, remarks, bugs or requests please do not hesitate to contact any of us (in alphabetical order):
 mirco.tribastone@imtlucca.it
 max.tschaikowski@imtlucca.it
 anvan@dtu.dk
Acknowledgments
We thank Lavinia Mariotti, MArch, for the design of ERODE’s logo.