Symmetry-Based Abstractions for Hybrid Automata

A symmetry of a dynamical system is a map that transforms any trajectory to another trajectory. Abstractions have been a key building block in the theory and practice of hybrid automata analysis. We introduce a novel abstraction for hybrid automata based on the symmetries of their modes. The abstraction procedure combines different modes of a concrete automaton A, whose trajectories are related by symmetries, into a single mode of the constructed abstract automaton B. The abstraction procedure sets the invariant of an abstract mode to be the union of the symmetry-transformed invariants of the concrete modes. Similarly, it sets the guard and reset of an abstract edge to be the union of the symmetry-transformed guards and resets of the concrete edges. We establish the soundness of the abstraction using a forward simulation relation and provide a running example. The abstraction achieves an order of magnitude speedup when used for the safety verification of vehicles pursuing reach-avoid tasks.