Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata
Werner Damm, Carsten Ihlemann, Viorica Sofronie-Stokkermans · 2011
This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of safety properties with exhaustive entry conditions can be done in polynomial time and time-bounded reachability with exhaustive entry conditions can be decided in nondeterministic polynomial time for non-parametric verification and in exponential time for parametric verification. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.