On the automatic verification of systems with continuous variables and unbounded discrete data structures

We address the verification problem of invariance properties for hybrid systems. We consider as general models of hybrid systems finite automata, supplied with (unbounded) discrete data structures and continuous variables. We focus on the case of systems manipulating discrete counters and one pushdown stack, and on the other hand, constant slope continuous variables. The use of unbounded discrete data sturcture allows to consider systems with a powerful control, and to reason about important notions as the number of occurrences of events in some computation. The use of constant slope continuous variables allows to reason for instance about the time separating events and the durations of phases within some computation interval. We present decidability results for several subclasses of such models of hybrid systems; this provides automatic verification procedures for these systems.