Symmetry-Based Abstractions for Hybrid Automata.
IEEE Trans. Autom. Control.(2024)
摘要
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
$\mathcal {A}$
, whose trajectories are related by symmetries, into a single mode of the constructed abstract automaton
$\mathcal {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 (FSR) 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.
更多查看译文
关键词
hybrid systems,abstraction,symmetry,formal methods,reachability analysis
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要