A bisimulation-like algorithm for abstracting control systems
A bisimulation-like algorithm for abstracting control systems
复制标题
一种用于抽象控制系统的类互模拟算法
DOI：
10.1109/allerton.2016.7852282
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
N. Ozay
中科院分区：
文献类型：
--
作者：
Andrew J. Wagenmaker;N. Ozay
出于最近的兴趣在抽象为基础的正确的建设控制综合，在本文中，我们提出了一种新的算法来构建有限的抽象“大”，可能是无限的，过渡系统。与创建状态空间分区的标准互模拟算法相反，新算法使用状态空间的重叠子集作为抽象的状态。我们表明，新的bisimulation-like算法的输出保持线性时间属性的可实现性。几个有趣的性能的算法进行了分析。特别是，当一个有限的互模拟的原始系统存在，新的算法总是在有限数量的步骤终止。此外，我们用一个例子表明，即使当原系统没有一个有限的互模拟，新算法可以导致一个有限的过渡系统，其无限的痕迹是等价的原系统。在本文的第二部分中，我们专注于该算法的应用，构造有限的离散时间线性控制系统的抽象，并讨论了它的几个优势，比标准的互模拟算法。最后，通过数值算例将新算法与已有算法进行了比较.
Motivated by the recent interest in abstraction-based correct-by-construction control synthesis, in this paper we propose a new algorithm to construct finite abstractions for “large”, possibly infinite, transition systems. As opposed to the standard bisimulation algorithms that create a partition of the state space, the new algorithm uses overlapping subsets of the state space as the states of the abstraction. We show that the output of the new bisimulation-like algorithm preserves realizability of linear-time properties. Several interesting properties of the algorithm are analyzed. In particular, when a finite bisimulation of the original system exists, the new algorithm is shown to always terminate in a finite number of steps. Moreover, we show with an example that even when the original system does not have a finite bisimulation, the new algorithm can result in a finite transition system whose infinite traces are equivalent to those of the original system. In the second part of the paper, we focus on the application of this algorithm to construct finite abstractions for discrete-time linear control systems and discuss several of its advantages over the standard bisimulation algorithm. Finally, the new algorithm is compared to the existing algorithms with some numerical examples.