混杂系统的对称性抽象及其应用
Symmetry Abstractions for Hybrid Systems and their Applications
摘要：
动力系统的对称性是将一个轨迹转换为另一个轨迹的映射。我们介绍了一种新的基于对称性的混合自动机的抽象。抽象将具体自动机A中的不同模式组合成抽象自动机B中的单个模式，具体自动机A的轨迹通过对称性相关。该抽象将抽象边的保护和重置设置为具体边的经仿射变换的保护和重置的并集。我们建立健全的抽象使用正向模拟关系（FSR），并提出了几个例子。我们的抽象结果在更简单的自动机，更适合形式化的分析和设计。我们说明了这种抽象的应用程序，使可达性分析更快，使无限的时间安全验证。我们展示了如何一个不动点的可达集计算的B可以用来回答可达性查询A，即使后者访问一个无限和无界序列的模式。我们提出了我们的实现的抽象建设，定点检查，并在软件工具中的映射，将抽象的可达集到具体的。最后，我们展示了我们的方法比现有的方法的优势，我们的抽象的不同方面，在一系列的实验，包括线性和非线性代理以下的航点的情况。
英文摘要：
A symmetry of a dynamical system is a map that transforms one trajectory to another trajectory. We introduce a new type of abstraction for hybrid automata based on symmetries. The abstraction combines different modes in a concrete automaton A, whose trajectories are related by symmetries, into a single mode in the abstract automaton B. The abstraction 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 present several examples. Our abstraction results in simpler automata, that are more amenable for formal analysis and design. We illustrate an application of this abstraction in making reachability analysis faster and enabling unbounded time safety verification. We show how a fixed point of the reachable set computation of B can be used to answer reachability queries for A, even if the latter visits an infinite and unbounded sequences of modes. We present our implementation of the abstraction construction, the fixed point check, and the map that transforms abstract reachable sets to concrete ones in a software tool. Finally, we show the advantage of our method over existing ones, and the different aspects of our abstraction, in a sequence of experiments including scenarios with linear and nonlinear agents following waypoints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
