The reachability problem for Polynomial Interrupt Timed Automata

Hybrid automata form an expressive model to describe systems combining continuous and discrete evolution modes. However, most verification problems are undecidable for this model.

We recall the particular case of Timed Automata where the reachability problem is PSPACE-complete. We introduce the class of Interrupt Timed Automata featuring special clocks called stopwatches that can be suspended. We show how to decide reachability when these automata are extended with polynomial constraints, using techniques from computer algebra.