## Algebraic invariants for linear hybrid automata

*Rupak Majumdar*,
*Joël
Ouaknine*, *Amaury Pouly*, and *James Worrell*
We exhibit an algorithm to compute the strongest algebraic (or
polynomial) invariants that hold at each location of a given guard-free
linear hybrid automaton (i.e., a hybrid automaton having only
unguarded transitions, all of whose assignments are given by affine
expressions, and all of whose continuous dynamics are given by linear
differential equations). Our main tool is a control-theoretic result
of independent interest: given such a linear hybrid automaton, we show
how to discretise the continuous dynamics in such a way that the
resulting automaton has precisely the same algebraic invariants.

*Proceedings of CONCUR 20*, LIPIcs 171, 2020. 17 pages.

PDF
© 2020 Rupak Majumdar, Joël Ouaknine, Amaury Pouly, and James Worrell.

Imprint / Data Protection