5 octobre 2015Mathieu Sassolas (LACL)
Modeling real world systems implies taking into account the continuous elapsing of time along with the discrete set of states the system can operate in, thus yielding so called /hybrid systems/. However, verification of such systems is mostly undecidable, and finding decidable fragments has been an ongoing research topic for the last 25 years. In this work we propose a decidable model of hybrid systems taking into account constraints expressed by polynomials instead of the more widespread linear constraints. The decision procedure relies on the cylindrical decomposition of reals.
This talk is based on joint work with Béatrice Bérard, Serge Haddad, Claudine Picaronny, and Mohab Safey El Din.