Menu:

DynIbex is a plug-in of Ibex library which is a library for constraint processing over real numbers.

DynIbex offers a set of validated numerical integration methods based on Runge-Kutta schemes to solve initial value problem of ordinary differential equations and for DAE in Hessenberg index 1 form.

Contributors

Julien Alexandre dit Sandretto, Alexandre Chapoutot, Olivier Mullier

Sponsors

This research benefited from the support of the "Chair Complex Systems Engineering - Ecole Polytechnique, THALES, DGA, FX, DASSAULT AVIATION, DCNS Research, ENSTA ParisTech, Télécom ParisTech, Fondation ParisTech and FDO ENSTA"

Features

How to cite DynIBEX

You should cite our paper published in Reliable Computing Journal with the following bibtex entry 

@Article{Sandretto:2016:VEI,
  Title                    = {Validated Explicit and Implicit {R}unge--{K}utta Methods},
  Author                   = {Julien Alexandre {dit Sandretto} and Alexandre Chapoutot},
  Journal                  = {Reliable Computing},
  Year                     = {2016},
  Month                    = {Jul},
  Number                   = {1},
  Pages                    = {79--103},
  Volume                   = {22}
}

History on Interval Runge-Kutta

This work on validated Runge-Kutta methods takes its roots in two previous works:
  1. GRKlib by Olivier Bouissou and Matthieu Martel which defined a validated version of the classical RK4 methods
  2. The extension to deal with any explicit Runge-Kutta methods as defined in the article published at NASA Formal Methods 2013 written by Olivier Bouissou, Alexandre Chapoutot and Adel Djoudi.
Note that other tentative to make Runge-Kutta methods guaranteed have been done, mainly:

DOWNLOAD and INSTALLATION

DynIbex is made of two main ingredients: an extension of the affine arithmetic and the validated Runge-Kutta methods. Current version 2.3 (February 2025)

We assume that the following sequence of commands are executed in Ibex directory.

Put the archive into the Ibex directory, then write the following commands: 

	    ~/Ibex/$ tar xvfz dynibex-2.3.tar.gz
	    ~/Ibex/$ cd dynibex-2.3
	    ~/Ibex/dynibex-2.3/$ ./waf configure [options]
	    ~/Ibex/dynibex-2.3/$ sudo ./waf install

Publications on DynIBEX

Theory of validated Runge-Kutta methods

Applications using DynIBEX

Validated Runge-Kutta methods for ODE (Research report and Article)

Description

A Runge-Kutta method, starting from an initial value \(\mathbf{y}_n\) at time \(t_n\) and a finite time horizon \(h\), the step-size, produces an approximation \(\mathbf{y}_{n+1}\) at time \(t_{n+1}\), with \(t_{n+1}-t_n = h\), of the solution \(\mathbf{y}(t_{n+1}; \mathbf{y}_n)\). Furthermore, to compute \(\mathbf{y}_{n+1}\), a Runge-Kutta method computes \(s\) evaluations of \(f\) at predetermined time instants. The number \(s\) is known as the number of stages of a Runge-Kutta method. More precisely, a Runge-Kutta method is defined by \[ \mathbf{y}_{n+1} = \mathbf{y}_n + h \sum_{i=1}^{s}b_i \mathbf{k}_i\enspace, \] with \(\mathbf{k}_i\) defined by \[ \mathbf{k}_i = f\left(t_0 + c_i h, \mathbf{y}_n + h \sum_{j=1}^{s} a_{ij}\mathbf{k}_j \right)\enspace. \] The coefficient \(c_i\), \(a_{ij}\) and \(b_i\), for \(i,j=1,2,\cdots, s\), fully characterize the Runge-Kutta methods and their are usually synthesized in a Butcher tableau of the form as follows: \[ \begin{array}{c|cccc} c_1 & a_{11} & a_{12} & \dots & a_{1s}\\ c_2 & a_{21} & a_{22} & \dots & a_{2s}\\ \vdots & \vdots & \vdots & \ddots & \vdots\\ c_s & a_{s1} & a_{s2} & \dots & a_{ss} \\ \hline & b_1 & b_2 & \dots & b_s\\ \end{array} \] In function of the form of the matrix \(A\), made of the coefficients \(a_{ij}\), a Runge-Kutta method can be To make a Runge-Kutta validated, the local truncation error (LTE) need to be bound, that is \[ \parallel \mathbf{y}\left(t_n; \mathbf{y}_{n-1}\right) - \mathbf{y}_n \parallel \leqslant c h^{p+1} \] \(c\) is a constant depending on the coefficients of the Runge-Kutta methods and \(p\) is the order of the Runge-Kutta method. An analytic form can be defined using the theorems stating the order condition of a Runge-Kutta method see our report for more details.

Example: basic integration

This example shows the simple way to solve IVP with DynIbex.

Validated Runge-Kutta methods for DAE (Article)

Description

The validated numerical integration of DAE in Hessenberg index 1 form can be also based on Runge-Kutta scheme. Nevertheless, it implies the definition of a new operator for the computation of the a priori enclosure. For more details, see the article.

Example: a simple DAE



Towards a contractor programming with differential equations

Description

This example has been written with the help of Gilles Chabert. It demonstrates the ability to embed validated Runge-Kutta methods for ODE into the contractor programming framework. Nevertheless, more work has to be done to have a complete and robust framework of constraint programming techniques with differential equations.

Example: a simple forward-backward operator for ODEs.



Simulation of a car in open loop, continuous-time closed loop and sampled closed loop

Description

We consider a simple nonlinear dynamics of a car given by equations \[ \begin{aligned} \dot{v}(t) & = \frac{ -50.0 v - 0.4 v^2}{m} \\ & \text{with}\quad m \in [990,1010] \end{aligned} \]

Example: open loop system

Example: continuous closed loop system with PI controller

Example: continuous closed loop system with PI controller with safety property

Example: closed loop system with discretized PI controller



Validated Runge-Kutta methods for dynamical systems with state constraints

Description

The validated numerical integration of dynamical systems with state constraints is available. It combines validated Runge-Kutta scheme with contractor operators to ensure the respect of constraints.

Example: a simple Production-Destruction systems



Cosimulation of Dynamical Systems

Description

These examples demonstrate the ability to solve coupled dynamical systems using cosimulation approach. First example is related to the heating of 8 rooms appartment and second example is related to linked springs.

Example 1: 8 rooms

Example 2: Springs



Checking a Signal Temporal Logic (STL) formula

Description

This example shows how to check an STL formula on the result of a simulation. A simple 1D-linear system is simulated and we check if the system stay under a value until it reaches this value.

Example