Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
复制标题
线性系统和安全线性时间时序逻辑的规范引导控制器综合
DOI：
10.1145/2461328.2461378
复制
发表时间：
2013
影响因子：
6.8
通讯作者：
P. Tabuada
中科院分区：
文献类型：
--
作者：
M. Rungger;M. Mazo;P. Tabuada
在本文中，我们介绍并分析了一种新型算法，以合成在离散时间线性系统上执行线性时间逻辑规范的控制器。这种方法中的中心步骤是计算可能非凸安全集中包含的最大控制不变集。尽管已知如何计算最大控制不变集的近似值，但其确切的计算仍然是一个空旷的问题。我们提供了一种算法，该算法计算一个受控的不变集，该集合可以保证是对最大控制不变集的不足。此外，我们保证我们的近似值至少与任何不变式集合一样好，该集合的距离与安全集的边界是限制的。所提出的算法建立在适合动力学和二进制决策图的集合的概念上。与大多数执行时间逻辑规格的控制器合成方案相反，我们不计算连续动力学的离散抽象。取而代之的是，我们仅抽象与最大控制不变集的计算相关的连续动力学的一部分。因此，我们称我们的方法规范为指导。我们描述了初步实施的理论基础和技术基础，并报告了一些实验，包括合成自动巡航控制器。我们的初步实现可处理多达五个连续的维度和规格，其中包含多达160个谓词在大约30分钟内定义为多面体，小于1 GB的内存。
In this paper we present and analyze a novel algorithm to synthesize controllers enforcing linear temporal logic specifications on discrete-time linear systems. The central step within this approach is the computation of the maximal controlled invariant set contained in a possibly non-convex safe set. Although it is known how to compute approximations of maximal controlled invariant sets, its exact computation remains an open problem. We provide an algorithm which computes a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invariant set. Moreover, we guarantee that our approximation is at least as good as any invariant set whose distance to the boundary of the safe set is lower bounded. The proposed algorithm is founded on the notion of sets adapted to the dynamics and binary decision diagrams. Contrary to most controller synthesis schemes enforcing temporal logic specifications, we do not compute a discrete abstraction of the continuous dynamics. Instead, we abstract only the part of the continuous dynamics that is relevant for the computation of the maximal controlled invariant set. For this reason we call our approach specification guided. We describe the theoretical foundations and technical underpinnings of a preliminary implementation and report on several experiments including the synthesis of an automatic cruise controller. Our preliminary implementation handles up to five continuous dimensions and specifications containing up to 160 predicates defined as polytopes in about 30 minutes with less than 1 GB memory.