田戴荧，方 浩，杨庆凯

（北京理工大学自动化学院，北京 100081）

1 引 言

近年来，时序逻辑理论作为计算机领域中用来进行正则化检验的一套方法[1]，被应用于机器人规划与控制中，取得了极大的应用成果。时序逻辑理论的主要思想是将时序逻辑任务约束转换为可以处理的约束形式，从而在规划时考虑这些约束，生成满足任务的路径。其中，线性时序逻辑（Linear Temporal Logic, LTL）将时序逻辑约束转换为Buchi˙˙ 自动机[2]，而对于信号时序逻辑（Signal Temporal Logic, STL），由于其处理的主要是连续系统，不能找到一个合适的图来作为其约束集。

针对连续系统中信号时序逻辑的控制方法，近年来有越来越多的学者进行了研究。伯克利大学的Raman 等人[3]将信号时序逻辑编码为离散值的组合作为整数约束，之后结合模型预测控制，将信号时序逻辑约束下的规划问题建模为混合整数线性规划问题。Bapinar 等人[4]将混合整数线性规划方法用到了多无人机系统的规划与控制中。Farahani 等人[5]在混合整数线性规划方法的基础上，针对自动系统所处的不确定性环境研究了控制的鲁棒性问题，对最坏情况下的模型预测控制问题进行了求解，从而得到了一个反应式的控制器。舒新峰等人[6]提出了一种命题投影时序逻辑的分布式模型检测方法，缓解模型检测的状态空间爆炸问题。此外，为了给STL 约束构建一个光滑的约束函数，Haghighi 等人[7]提出了一种新的光滑可微STL 量化语义来累积鲁棒性，并通过策略上升方法求解一系列光滑优化问题有效地计算控制策略。……