The control paradigm of physical processes being supervised by digital programs has lead to the development of a theory of hybrid systems combining finite state automata with differential equations. One of the most important problems in the verification of hybrid systems is the reachability problem. Even though the computation of reachable spaces for finite state machines is well developed, computing the reachable space of a differential equation is difficult.
展开▼