Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata

We study linear hybrid automata with dynamics of the form $\sum a_i x_i \leq a$ and $\sum b_i {\dot x_i} \leq b$. We show that verification of safety properties for reasonable classes of such systems can be reduced to invariant checking and bounded model checking and, ultimately, to checking the validity of certain formulae (obtained using a polynomial reduction). We show that the problem of checking the validity of the formulae obtained this way is typically in NP, and identify verification tasks which can be performed in PTIME. These reductions can also be used for parametric systems, both for checking safety properties given constraints on parameters, and for deriving constraints of parameters that guarantee that safety properties hold