Zonotope-based Symbolic Controller Synthesis for Linear Temporal Logic Specifications

本文研究了使用zonotope技术解决线性时间逻辑（LTL）规范下的非线性控制系统控制器综合问题。提出了一种局部到全局的控制策略，以LTL公式表示所需规范。首先，开发了一种新的方法将状态空间分为有限的zonotopes和约束zonotopes，称为单元格，并允许与相邻单元格相交。其次，从交集关系生成了所有单元格之间的图形，以验证LTL公式的接受路径的实现。实现验证确定是否需要控制设计，并且导致有限的局部LTL公式。第三，一旦实现接受路径，就会导出一种基于抽象的方法进行控制器设计。特别地，我们仅关注实现验证中的单元格，并由于zonotopes的特性近似每个单元格。基于局部符号模型和局部LTL公式，提出了一种迭代综合算法，用于设计所有局部抽象控制器，其存在和组合建立LTL公式的全局控制器。最后，通过移动机器人的路径规划问题说明了所提出的框架。

本文试图解决非线性控制系统在线性时态逻辑（LTL）规范下的控制合成问题，使用zonotope技术。

本文提出了一种局部到全局的控制策略，将状态空间划分为有限的zonotope，通过交集关系生成所有cell之间的图形来验证LTL公式的接受路径实现。

本文提出了一种新颖的抽象方法，仅关注实现验证中的cell，并利用zonotope的特性逼近每个cell，使用迭代合成算法设计所有局部抽象控制器，这些控制器的存在和组合构成了LTL公式的全局控制器。本文的方法在移动机器人的路径规划问题中得到了证明。

最近的相关研究包括：“Distributed Synthesis of Safe Control Strategies for Markov Decision Processes”和“Robust Control Synthesis for Linear Systems with Temporal Logic Constraints”。