The goal of this checker will be to determine all possible states of an automata.
First step : Determining in a precise manner the maximal range of possible values for a R^n first order linear differential equation with controlled noize (WIP)
- The dimension is n=1 for the moment. Zonotopes are used to approximate the reachable states.
Second step : Determining when state guards are fulfilled to decide when transitions are possible to other states (TODO)
Authors: Baptiste Pecatte & Julien Piet