ERODE

Evaluation and Reduction of Ordinary Differential Equations

Quick Links

Summary
ERODE

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).

Publications
Artifact Evaluated at POPL

A tutorial-like overview of the theory at the basis of ERODE can be found here:

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:

  1. ERODE manual;
  2. ERODE examples.

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.).

ERODE

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 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.

Explicit ODE format
Reaction Network format

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
  • andrea.vandin@imtlucca.it

Acknowledgments

We thank Lavinia Mariotti, MArch, for the design of ERODE’s logo.