Controller Synthesis for Linear System With Reach-Avoid Specifications
Controller Synthesis for Linear System With Reach-Avoid Specifications
复制标题
DOI：
10.1109/tac.2021.3069723
复制
发表时间：
2022-04
影响因子：
6.8
通讯作者：
Chuchu Fan;Umang Mathur;Qiang Ning;S. Mitra;Mahesh Viswanathan
中科院分区：
文献类型：
--
作者：
Chuchu Fan;Umang Mathur;Qiang Ning;S. Mitra;Mahesh Viswanathan
我们解决的问题，合成可证明正确的控制器的线性系统达到避免规格。基于离散抽象的控制器综合技术已被开发用于具有各种类型规格的线性和非线性系统。然而，这些方法通常遭受状态空间爆炸问题。我们的解决方案分解成两个更小的，更容易处理的问题的整体综合问题：一个开环控制器的综合问题，它可以产生一个参考轨迹，第二个用于合成跟踪控制器，它可以强制其他轨迹遵循参考轨迹。作为一个关键的积木块的结果，我们表明，一旦一个跟踪控制器是固定的，从初始邻域的可达状态，受到任何干扰，可以overapproximate由一系列的椭球，形状是独立的开环控制器。因此，开环控制器可以独立合成，以满足达到避免规格的初始邻域。此外，我们能够减少开环控制器的综合问题的可满足性问题的量化自由的线性真实的算法。可满足性问题中线性约束的数量与作为多面体障碍和目标集的表面的超平面的数量成线性关系。整体综合算法，计算跟踪控制器，然后迭代地覆盖整个初始集，以找到初始邻域的开环控制器。该算法是健全的，对于一类鲁棒系统，也是完整的。我们实现了这种合成算法的工具RealSyn版本2.0，并使用它的几个基准与多达20个维度。实验结果非常有希望：RealSyn ver 2.0可以在几秒钟内找到大多数基准测试的控制器。
We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Discrete abstraction-based controller synthesis techniques have been developed for linear and nonlinear systems with various types of specifications. However, these methods typically suffer from the state space explosion problem. Our solution decomposes the overall synthesis problem into two smaller, and more tractable problems: one synthesis problem for an open-loop controller, which can produce a reference trajectory, and a second for synthesizing a tracking controller, which can enforce the other trajectories to follow the reference trajectory. As a key building-block result, we show that, once a tracking controller is fixed, the reachable states from an initial neighborhood, subject to any disturbance, can be overapproximated by a sequence of ellipsoids, with shapes that are independent of the open-loop controller. Hence, the open-loop controller can be synthesized independently to meet the reach-avoid specification for an initial neighborhood. Moreover, we are able to reduce the problem of synthesizing open-loop controllers to satisfiability problems over quantifier-free linear real arithmetic. The number of linear constraints in the satisfiability problem is linear to the number of hyperplanes as the surfaces of the polytopic obstacles and goal sets. The overall synthesis algorithm, computes a tracking controller, and then iteratively covers the entire initial set to find open-loop controllers for initial neighborhoods. The algorithm is sound and, for a class of robust systems, is also complete. We implement this synthesis algorithm in a tool RealSyn ver 2.0 and use it on several benchmarks with up to 20 dimensions. Experiment results are very promising: RealSyn ver 2.0 can find controllers for most of the benchmarks in seconds.