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