Bounded ∈-reachability of linear hybrid automata with a deterministic and transversal discrete transition condition

An ∈-reach set of a hybrid automaton is a set of states such that every state in it is within a distance ∈ of some reachable state.We propose an algorithm to compute a bounded ∈-reach set from a given initial state of a class of deterministic linear hybrid automata that satisfy a certain transversality condition. The proposed algorithm is based on time-sampling. It over-approximates the reachable states at each sampled time instant using polyhedra, and subsequently computes an ∈-reach set for a bounded time interval using these over-approximations, while reducing the sampling period on-the-fly.