Computing Abstractions of Nonlinear Systems
Computing Abstractions of Nonlinear Systems
复制标题
非线性系统的计算抽象
DOI：
--
复制
发表时间：
2009
影响因子：
6.8
通讯作者：
Gunther Reissig
中科院分区：
文献类型：
--
作者：
Gunther Reissig
足够精确的有限状态模型，也称为符号模型或离散抽象，允许人们应用最初为纯离散系统开发的全自动方法，对连续和混合系统进行正式推理，并设计可证明执行预定义规范的有限状态控制器。我们提出了一种新颖的算法来计算非线性离散时间和采样系统的有限状态模型，该算法依赖于使用多面体单元量化状态空间，将这些单元嵌入到可达到集是凸的合适的超集中，并通过支持半空间的交集来过度逼近可达到集。我们证明了这些半空间的新颖递归描述，并提出了一种迭代过程来有效地计算它们。我们还为可达到的集合的凸性提供了新的充分条件，这意味着上述量化器单元嵌入的存在。我们的方法产生高度准确的抽象，并适用于温和假设下的非线性系统，在采样系统的情况下降低到足够的平滑度。通过算例证明了其在状态和控制约束下的非线性连续对象离散控制器设计中的实用性。
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.