混合系统的对称性抽象及其应用

动力系统的对称性是将一条轨迹映射为另一条轨迹的映射。我们基于对称性引入了一种用于混合自动机的新型抽象。该抽象将具体自动机A中轨迹由对称性相关联的不同模式合并为抽象自动机B中的单一模式。该抽象将抽象边的守卫与重置设为具体边的对称性变换守卫与重置之并。我们利用前向模拟关系（FSR）确立了该抽象的可靠性并给出若干示例。我们的抽象产生了更简单的自动机，更适于形式化分析与设计。我们展示了该抽象在加速可达性分析并实现无界时间安全性验证中的应用。我们说明了如何利用B的可达集计算的不动点来回答A的可达性查询，即便后者经历了无限且无界模式序列。我们在软件工具中实现了抽象构造、不动点检查以及将抽象可达集映射为具体可达集的映射。最后，我们通过包括线性与非线性智能体沿航点运动场景在内的一系列实验，展示了我们的方法相较现有方法的优势及我们抽象的不同方面。