View article

Hybrid automata model systems with both digital and analog components, such az embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify the precise boundary between decidability and undecidability of the reachability problem for hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on a translation of an initialized rectangular automaton into a timed automaton that defines the same timed language. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures …