This paper studies the controller synthesis problem for nonlinear control systems under linear temporal logic (LTL) specifications using zonotope techniques. A local-to-global control strategy is proposed for the desired specification expressed as an LTL formula. First, a novel approach is developed to divide the state space into finite zonotopes and constrained zonotopes, which are called cells and allowed to intersect with the neighbor cells. Second, from the intersection relation, a graph among all cells is generated to verify the realization of the accepting path for the LTL formula. The realization verification determines if there is a need for the control design, and also results in finite local LTL formulas. Third, once the accepting path is realized, a novel abstraction-based method is derived for the controller design. In particular, we only focus on the cells from the realization verification and approximate each cell thanks to properties of zonotopes. Based on local symbolic models and local LTL formulas, an iterative synthesis algorithm is proposed to design all local abstract controllers, whose existence and combination establish the global controller for the LTL formula. Finally, the proposed framework is illustrated via a path planning problem of mobile robots.

翻译：本文研究利用zonotope技术对非线性控制系统进行线性时序逻辑（LTL）规范下的控制器综合问题。针对以LTL公式表达的目标规范，提出了一种局部到全局的控制策略。首先，开发了一种新方法将状态空间划分为有限个zonotope和约束zonotope（称为单元），并允许与相邻单元相交。其次，根据交叠关系生成所有单元间的图结构，用于验证LTL公式可接受路径的实现性。该实现性验证不仅确定是否需要控制设计，同时产生有限个局部LTL公式。第三，一旦可接受路径得以实现，推导出基于抽象的新型控制器设计方法。具体而言，我们仅关注实现性验证中的单元，并利用zonotope的性质对每个单元进行近似。基于局部符号模型与局部LTL公式，提出迭代综合算法设计所有局部抽象控制器，其存在性与组合构建了满足LTL公式的全局控制器。最后，通过移动机器人路径规划问题验证了所提框架的有效性。