论文标题
在时间逻辑约束下，无抽象控制合成的控制屏障函数
Control Barrier Functions for Abstraction-Free Control Synthesis under Temporal Logic Constraints
论文作者
论文摘要
时间逻辑已被广泛用于表达针对网络物理系统（CPSS）的复杂任务规格。在时间逻辑约束下合成CP的控制器的一种方法是首先将CPs抽象为离散过渡系统，然后应用正式方法。但是，这种方法在计算要求上是由于维度的诅咒而受到的可伸缩性。在本文中，我们提出了一种控制屏障函数（CBF）方法，以在线性时间逻辑（LTL）约束下进行无抽象控制合成。我们首先构建规范的确定性Rabin自动机并计算接受运行。然后，我们计算一系列LTL公式，每个公式必须在特定时间间隔内满足每个公式，并证明满足公式的顺序足以满足LTL规范。最后，我们通过构建适当的CBF来计算一个控制策略，以满足每个公式。我们提出了一个二次程序来计算控制器，并显示使用拟议方法合成的控制器保证系统以满足LTL规范，前提是二次程序在每个时间步骤中都是可行的。提出了一项数值案例研究以证明所提出的方法。
Temporal logic has been widely used to express complex task specifications for cyber-physical systems (CPSs). One way to synthesize a controller for CPS under temporal logic constraints is to first abstract the CPS as a discrete transition system, and then apply formal methods. This approach, however, is computationally demanding and its scalability suffers due to the curse of dimensionality. In this paper, we propose a control barrier function (CBF) approach to abstraction-free control synthesis under a linear temporal logic (LTL) constraint. We first construct the deterministic Rabin automaton of the specification and compute an accepting run. We then compute a sequence of LTL formulae, each of which must be satisfied during a particular time interval, and prove that satisfying the sequence of formulae is sufficient to satisfy the LTL specification. Finally, we compute a control policy for satisfying each formula by constructing an appropriate CBF. We present a quadratic program to compute the controllers, and show the controllers synthesized using the proposed approach guarantees the system to satisfy the LTL specification, provided the quadratic program is feasible at each time step. A numerical case study is presented to demonstrate the proposed approach.
