非线性系统的抽象计算
Computing abstractions of nonlinear systems
AI总结：
提出一种基于多面体细胞量化、嵌入凸超集和支撑半空间交集逼近可达集的算法，用于构造非线性离散时间与采样系统的有限状态模型，并证明可达集凸性的新充分条件。
摘要：
足够精确的有限状态模型，也称为符号模型或离散抽象，允许应用最初为纯离散系统开发的完全自动化方法，以形式化地推理连续和混合系统，并设计可证明强制实现预定义规范的有限状态控制器。我们提出了一种新的算法来计算非线性离散时间和采样系统的此类有限状态模型，该算法依赖于使用多面体细胞量化状态空间，将这些细胞嵌入到可达集为凸的合适超集中，并通过支撑半空间的交集来过度逼近可达集。我们证明了这些半空间的新颖递归描述，并提出了一个迭代过程来高效计算它们。我们还提供了可达集凸性的新充分条件，这暗示了上述量化器细胞嵌入的存在性。我们的方法产生高度精确的抽象，并在温和假设下适用于非线性系统，对于采样系统，这些假设简化为足够光滑性。通过一个示例，展示了该方法在状态和控制约束下为非线性连续对象设计离散控制器的实用性。
英文摘要：
Sufficiently accurate finite state models, also called symbolic models or discrete abstractions, allow one to apply fully automated methods, originally developed for purely discrete systems, to formally reason about continuous and hybrid systems, and to design finite state controllers that provably enforce predefined specifications. We present a novel algorithm to compute such finite state models for nonlinear discrete-time and sampled systems which depends on quantizing the state space using polyhedral cells, embedding these cells into suitable supersets whose attainable sets are convex, and over-approximating attainable sets by intersections of supporting half-spaces. We prove a novel recursive description of these half-spaces and propose an iterative procedure to compute them efficiently. We also provide new sufficient conditions for the convexity of attainable sets which imply the existence of the aforementioned embeddings of quantizer cells. Our method yields highly accurate abstractions and applies to nonlinear systems under mild assumptions, which reduce to sufficient smoothness in the case of sampled systems. Its practicability in the design of discrete controllers for nonlinear continuous plants under state and control constraints is demonstrated by an example.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
