NLTOOLBOX: A C++ Library for Reachability Computation of Non-linear Dynamical Systems


Objectives

This library provides an algorithmic infrastructure for reachability computation of non-linear dynamical systems. The user can write a simple program to
- solve specific analysis problems (beyond reachability analysis)
- develop and test different exploration strategies
- be integrated in other tools to increase their scope

Major functionalities

Reachability analysis for 2 types of dynamical systems:
- Polynomial systems (using the Bernstein expansion technique)
- More general nonlinear systems (using hybridization)

Authors

Thao Dang, mail  CNRS/VERIMAG
Romain Testylier, mail  Currently research engineer at INRIA

Download and Documentation

Related Publications

Romain Testylier and Thao Dang.
ATVA 2013, LNCS, Springer-Verlag, 2013. [pdf]

Reachability analysis for polynomial dynamical systems using the Bernstein expansion.
T. Dang and R. Testylier.
Reliable Computing Journal, Special issue: Bernstein Polynomials in Reliable Computing, ISSN 1573-1340, 2012 pdf.

Reachability analysis using the Bernstein expansion over polyhedra.
Romain Testylier and Thao Dang.
Fifth International Workshop on Numerical Software Verification NSV, June 2012. [pdf]

Hybridization Methods for the Analysis of Non-Linear Systems.
Eugene Asarin, Thao Dang, and Antoine Girard
Acta Informatica, 43(7):451-476, 2007. [pdf]