Symmetry-Based Abstractions for Hybrid Automata

• 成果类型: Article
• 署名作者: Sibai, Hussein; Mitra, Sayan
• 署名单位: Washington University (WUSTL); University of Illinois System; University of Illinois Urbana-Champaign
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2023.3327329
• 发表日期: 2024
• 页码: 3357-3364
• 关键词: trajectory; Automata; safety; Transforms; Heuristic algorithms; dynamical systems; Behavioral sciences; abstraction; formal methods; hybrid systems; reachability analysis; symmetry

摘要

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.