Thomas A. Henzinger

IST Austria

A hybrid system is a system whose state evolves by discrete changes, called jumps, as well as continuous changes, called flows. We view such a system as a symbolic transition system defined by pre and post operators on regions, where a region R is a possibly infinite set of states, pre(R) is the region of all states that may jump or flow into R, and post(R) is the region of all states into which the states in R may jump or flow. We present timed and hybrid automata as a specification language for hybrid systems. We then provide semi- algorithms that verify these systems by computing with pre, post, and boolean operators on regions. Finally we give termination arguments for these algorithms which depend on properties of the underlying transition systems.