Control of dynamical systems with temporal logic specifications

This thesis is motivated by safety-critical applications involving autonomous air, ground, and space vehicles carrying out complex tasks in uncertain and adversarial environments. We use temporal logic as a language to formally specify complex tasks and system properties. Temporal logic specifications generalize the classical notions of stability and reachability that are studied in the control and hybrid systems communities. Given a system model and a formal task specification, the goal is to automatically synthesize a control policy for the system that ensures that the system satisfies the specification. This thesis presents novel control policy synthesis algorithms for optimal and robust control of dynamical systems with temporal logic specifications. Furthermore, it introduces algorithms that are efficient and extend to high-dimensional dynamical systems.

The first contribution of this thesis is the generalization of a classical linear temporal logic (LTL) control synthesis approach to optimal and robust control. We show how we can extend automata-based synthesis techniques for discrete abstractions of dynamical systems to create optimal and robust controllers that are guaranteed to satisfy an LTL specification. Such optimal and robust controllers can be computed at little extra computational cost compared to computing a feasible controller.

The second contribution of this thesis addresses the scalability of control synthesis with LTL specifications. A major limitation of the standard automaton-based approach for control with LTL specifications is that the automaton might be doubly-exponential in the size of the LTL specification. We introduce a fragment of LTL for which one can compute feasible control policies in time polynomial in the size of the system and specification. Additionally, we show how to compute optimal control policies for a variety of cost functions, and identify interesting cases when this can be done in polynomial time. These techniques are particularly relevant for online control, as one can guarantee that a feasible solution can be found quickly, and then iteratively improve on the quality as time permits.

The final contribution of this thesis is a set of algorithms for computing feasible trajectories for high-dimensional, nonlinear systems with LTL specifications. These algorithms avoid a potentially computationally-expensive process of computing a discrete abstraction, and instead compute directly on the system's continuous state space. The first method uses an automaton representing the specification to directly encode a series of constrained-reachability subproblems, which can be solved in a modular fashion by using standard techniques. The second method encodes an LTL formula as mixed-integer linear programming constraints on the dynamical system. We demonstrate these approaches with numerical experiments on temporal logic motion planning problems with high-dimensional (10+ states) continuous systems.

Formal methods for control synthesis in partially observed environments : application to autonomous robotic manipulation

Modern robots are increasingly expected to function in uncertain and dynamically challenging environments, often in proximity with humans. In addition, wide scale adoption of robots requires on-the-fly adaptability of software for diverse application. These requirements strongly suggest the need to adopt formal representations of high level goals and safety specifications, especially as temporal logic formulas. This approach allows for the use of formal verification techniques for controller synthesis that can give guarantees for safety and performance. Robots operating in unstructured environments also face limited sensing capability. Correctly inferring a robot's progress toward high level goal can be challenging.

This thesis develops new algorithms for synthesizing discrete controllers in partially known environments under specifications represented as linear temporal logic (LTL) formulas. It is inspired by recent developments in finite abstraction techniques for hybrid systems and motion planning problems. The robot and its environment is assumed to have a finite abstraction as a Partially Observable Markov Decision Process (POMDP), which is a powerful model class capable of representing a wide variety of problems. However, synthesizing controllers that satisfy LTL goals over POMDPs is a challenging problem which has received only limited attention.

This thesis proposes tractable, approximate algorithms for the control synthesis problem using Finite State Controllers (FSCs). The use of FSCs to control finite POMDPs allows for the closed system to be analyzed as finite global Markov chain. The thesis explicitly shows how transient and steady state behavior of the global Markov chains can be related to two different criteria with respect to satisfaction of LTL formulas. First, the maximization of the probability of LTL satisfaction is related to an optimization problem over a parametrization of the FSC. Analytic computation of gradients are derived which allows the use of first order optimization techniques.

The second criterion encourages rapid and frequent visits to a restricted set of states over infinite executions. It is formulated as a constrained optimization problem with a discounted long term reward objective by the novel utilization of a fundamental equation for Markov chains - the Poisson equation. A new constrained policy iteration technique is proposed to solve the resulting dynamic program, which also provides a way to escape local maxima.

The algorithms proposed in the thesis are applied to the task planning and execution challenges faced during the DARPA Autonomous Robotic Manipulation - Software challenge.

Incremental Control Synthesis for Robotics in the Presence of Temporal Logic Specifications

This thesis presents methods for incrementally constructing controllers in the presence of uncertainty and nonlinear dynamics. The basic setting is motion planning subject to temporal logic specifications. Broadly, two categories of problems are treated. The first is reactive formal synthesis when so-called discrete abstractions are available. The fragment of linear-time temporal logic (LTL) known as GR(1) is used to express assumptions about an adversarial environment and requirements of the controller. Two problems of changes to a specification are posed that concern the two major aspects of GR(1): safety and liveness. Algorithms providing incremental updates to strategies are presented as solutions. In support of these, an annotation of strategies is developed that facilitates repeated modifications. A variety of properties are proven about it, including necessity of existence and sufficiency for a strategy to be winning. The second category of problems considered is non-reactive (open-loop) synthesis in the absence of a discrete abstraction. Instead, the presented stochastic optimization methods directly construct a control input sequence that achieves low cost and satisfies a LTL formula. Several relaxations are considered as heuristics to address the rarity of sampling trajectories that satisfy an LTL formula and demonstrated to improve convergence rates for Dubins car and single-integrators subject to a recurrence task.

室外自主移动机器人AMOR的导航技术

在非结构化环境,移动机器人行驶运动规划和自主导航是非常挑战性的问题。基于实时的动态栅格地图,提出了一个快速的而又实效的轨迹规划算法,实现机器人在室外环境的无碰撞运动导航。AMOR是自主研发的室外运动移动机器人,它在2007年欧洲C-ELROB大赛中赢得了野外自主侦察比赛的冠军。它装备了SICK的激光雷达,用来获取机器人运动前方的障碍物体信息,建立实时动态的环境地图。以A*框架为基础的改造算法,能够在众多的路径中快速地找到最佳的安全行驶路径,实现可靠的自主导航。所有的测试和比赛结果表明所提方案是可行的、有效的。

小型爬壁机器人系统设计与应用

针对一种小型的双足爬壁机器人,设计开发了基于DSP2812处理芯片的控制系统.该机器人系统采用双足真空吸盘式结构和用3个电机驱动5个关节的欠驱动结构.双足真空吸盘式结构使其可以在光滑的墙面和天棚行走,又能够在交接面之间完成跨步行走.而欠驱动结构减少了电机的数目,从而减小了机器人的尺寸和降低了机器人的质量和能量消耗,但它也给机器人的控制和运动规划带来了新的挑战.已完成的系统设计包括运动模式设计、关节控制、通信模块设计和吸盘足控制等.实验结果证明了所提出方案的可行性.

可重构机器人越障运动的规划

提出一种新型的可重构机器人,该机器人在受一个驱动力矩的作用时,在不同约束下表现的输出形式不同.利用机构这一特点,实现了机器人移动中的自主越障运动.主要针对机器人越障运动中越障高度受导轮和手臂影响的问题,提出一种借助环境同时改变手臂姿态的越障规划方法,有效地提高了越障的高度.通过试验样机验证了规划方法的有效性.

动态未知环境下基于相对坐标系的移动机器人实时运动规划

提出了一种简单、新颖的在动态未知环境下的移动机器人运动规划方法．此方法基于相对坐标系，通过传感器信息实时调整机器人的行为来实现规划．在规划过程中，机器人有两种行为：向目标运动和避碰，且避碰行为具有优先权．机器人两种行为的切换是基于加速度空问的，首先解决的是避碰问题，而向目标运动是作为避碰的反问题来考虑的．仿真研究验证了此规划方法的有效性。

基于人工协调场的多移动机器人实时协调避碰规划

为克服传统人工势场在动态未知环境下机器人避碰规划中存在的缺陷,提出人工协调场法(ACF).将场函数与机器人的风险状态相结合,给出并讨论了人工协调场的基本设计.基于人工协调场,考虑机器人的运动约束,实现了多机器人之间以及机器人与环境间的实时协调避碰,提出了一个多移动机器人无死锁实时避碰规划算法.理论分析和仿真试验证明所提方法的有效性.

理性遗传算法及其在运动规划中的应用

为提高理性遗传算法遗传信息的完备性、算法全局收敛性以及算法的整体结构,给出了一个更一般化的理性算子和算法结构,证明了算法的全局收敛性.理论分析和在运动规划问题中的应用结果验证了理性遗传算法的有效性.

仿尺蠖微小型壁面移动机器人运动规划与控制研究

本论文的研究内容是围绕国家“863”计划支持项目“基于探测机器人技术的反恐立体侦察监控示范系统”（编号：2004AA420110）和“微小型反恐侦察移动平台和探测关键技术研究”（编号：2005AA420230）展开的。研究工作以微小型壁面移动机器人的研制为实际背景，主要包括以下五个方面的内容：⑴ 机器人的运动学、动力学分析和控制系统设计；⑵ 机器人的运动步态分析；⑶ 机器人在狭窄空间中的运动规划方法研究，以及在壁面过渡时的运动规划方法研究；⑷ 欠平滑壁面上机器人的自主行为控制和针对动力学特性的重力补偿控制研究；⑸ 论文所提出方法的仿真分析和实验研究。 第一，介绍了微小型壁面移动机器人的欠驱动机构设计和三种运动模式；分别基于D-H坐标变换和拉格朗日方法，对机器人的运动学和动力学特性进行了分析，为接下来的步态分析、运动规划和控制研究奠定了基础；开发了微小型壁面移动机器人的嵌入式DSP控制系统，为论文中的仿真和实验研究提供了物理平台。 第二，对尺蠖的生物特征和运动机制进行了简要介绍，并总结了尺蠖运动的特点；通过理论计算和实验测试，分析了微小型壁面移动机器人的步行稳定性；在机构设计和运动学建模基础上，全面地分析了微小型壁面移动机器人的各种基本步态、派生步态和壁面过渡步态，同时引入用以描述步态之间转换关系的步态算子，为后续的运动规划和控制方法研究做好了理论铺垫。 第三，分析了微小型壁面移动机器人运动规划问题的特殊性；考虑到机器人运动时真空吸附的耗时问题和狭窄空间中步态选择的合理性，通过对局部动态窗口法进行改进，引入可达空间动态局部栅格和遍历搜索算法，提出了基于可行步态的微小型壁面移动机器人在狭窄空间中的运动规划方法；根据壁面过渡的步态分析结果，并考虑到吸盘足的真空吸附载荷和机器人的动力学特性，提出了基于步态参数规划与最小能耗轨迹优化相结合的微小型壁面移动机器人在壁面过渡时的运动规划方法。通过仿真分析和实验研究，验证了上述运动规划方法的合理性和有效性。 第四，针对欠平滑壁面上机器人吸盘足吸附失败时的自主行为控制问题，根据步态分析结果，建立了吸盘足的有限状态机模型，并按“就近”原则设定状态转移优先级，提出了基于有序试探的微小型壁面移动机器人着地点选择控制方法；针对机器人的动力学特性，特别是重力矩变化对机器人运动控制的影响，在采用模糊自适应PID控制的基础上，根据轨迹优化结果，引入前馈重力补偿环节，提出了基于重力补偿的微小型壁面移动机器人模糊自适应PID控制方法。通过仿真分析和实验研究，验证了所提方法在改善系统控制性能，提高机器人自主能力方面的可行性和有效性。 第五，在武警北京特警学院的反劫机训练场，对微小型壁面移动机器人的运动控制能力和越障能力进行了现场实验测试，验证了论文所提出运动规划和控制方法在实际应用中的有效性。

一种欠驱动AUV的三维实时避碰方法

针对以测距声纳为避碰传感器的一类欠驱动型AUV，提出了一种水平面和垂直面相结合的三维实时避碰方法。根据测距声纳和欠驱动AUV 的特殊性，首先从运动规划和路径规划2 个层次提出了AUV 混合型实时避碰结构，并分别设计了基于事件反馈监控的避碰自动机和基于免疫遗传的局部路径规划算法。多种典型障碍场景的半物理仿真实验表明，论文所提方法能够实现AUV 安全、稳定的三维避碰过程。

水下机器人-机械手系统构建与研究

描述了一水下机器人——机械手系统研究平台的搭建,详细介绍了三功能水下电动机械手的设计与实验,给出了载体分系统的设计结果,利用Matlab工具箱和M函数构建了系统仿真模型,可以有效地对系统规划和控制算法进行验证(包括分别对载体分系统和机械手分系统的控制),可为进一步的现场试验提供指导和方法验证。

自治水下机器人-机械手系统运动规划与协调控制研究

过去的五十年，自治水下机器人技术得到迅速发展，在海洋资源调查、海洋科学考察和海洋地质勘探等领域有着广泛的应用，为促进相关领域的发展做出了显著贡献。随着海洋开发和利用的活动增多和水下机器人总体技术水平的提高，利用自治水下机器人进行海洋作业逐渐受到人们的重视。作业型自治水下机器人是为了满足当前海洋领域的需求而提出的一种大深度、大范围潜航并能够自主完成水下科学考察和作业的水下机器人系统，是目前水下机器人的一个发展趋势。自治水下机器人与作业机械手构成浮游基座的多连接体系统，具有运动学冗余、动力学高度耦合等特点，高效安全的运动规划与高精度的协调控制技术是保证其自主作业的一个核心技术。 本文结合 “十五”期间国家863计划“深海作业型自治水下机器人总体方案设计”和中国科学院沈阳自动化研究所知识创新项目“新型ARV关键技术研究”的研究内容，围绕水下机器人自主作业技术，深入研究了自治水下机器人-机械手系统的运动规划与协调控制技术，以实现高精度的机械手末端位置控制与轨迹跟踪，为深海资源开发的特定需求发展具有自主作业能力的水下机器人技术提供理论依据。重点研究针对系统特点的运动规划与运动实现问题；研究基于系统响应特性的机械手控制与载体控制问题；研究基于扰动模型以及不基于扰动模型的载体抗扰动控制问题；在系统运动规划与控制研究的基础上，研究能实现机械手末端精确轨迹跟踪的控制策略问题。本论文研究内容如下： (1)根据自治水下机器人载体特点，研究了适合于载体搭载的水下电动机械手设计与控制问题。设计了谐波传动的紧凑型三功能水下电动机械手系统，包括结构设计、控制系统搭建和控制器设计，根据机械手摆动关节的幅频响应特性，设计了关节角速率PI校正控制器和双环位置控制器，并针对常参数位置控制的电压和角速率突变，研究了基于界估计的机械手位置自适应控制应用问题；实验证明了系统的可靠性和控制算法的有效性，为水下电动机械手的设计开发提供了理论支持，为论文后续研究工作奠定了基础。 (2)研究了自治水下机器人-机械手系统的运动规划问题。建立了系统运动学方程和系统仿真模型；针对系统运动学冗余、载体流线外形、自身携带能源等特点，结合梯度投影法和加权伪逆矩阵法，以机械手末端位置控制及轨迹跟踪为前提，对系统运动分配、关节限位、有无海流下的系统能耗优化等运动规划进行了研究，仿真证明了运动规划算法的有效性。 (3)研究了一自治水下机器人-机械手系统的基本控制问题。利用沈阳自动化研究所的ARV载体，结合本文设计的三功能水下电动机械手，搭建了水下机器人-机械手实验系统；对载体分系统自身的响应特性以及对机械手扰动的响应特性进行了测试和分析；设计了基于输入补偿和机械手扰动补偿的复合校正控制算法，在有限的传感器条件下，通过测量变换获得了两种补偿控制算法中的近似补偿项，水池实验证明了算法的有效性。 (4)针对机械手扰动和载体推进器推力模型的复杂性和不精确性，在基于载体输入补偿控制的基础上，设计了神经网络自适应控制算法，通过自学习的方式用神经网络直接逼近载体控制电压与机械手扰动状态量之间的非线性关系，在机械手不停扰动下逐渐提高载体的控制精度；基于Lyapunov稳定性理论，证明了存在外界干扰和神经网络逼近误差条件下水下机器人-机械手系统载体控制器的闭环稳定性；通过水池实验验证了控制系统的有效性，为水下机器人-机械手系统载体分系统的控制提供了一种新思路。 (5)结合系统控制，通过水池实验分析了离线规划与在线规划下的机械手末端轨迹跟踪特点，针对几种典型情况，提出了自治水下机器人-机械手系统自主作业的几种控制规划策略，通过机械手末端跟踪典型轨迹的水池实验，证明了所提策略的有效性，实现了系统规划、控制共同作用下的机械手末端轨迹跟踪，在配置环境感知传感器的情况下，能够实现一定程度的自主作业。

基于实时障碍物预测的机器人运动规划

本文给出了移动机器人的虚力导航和运动规划系统．这种方法结合最小方差估计算法（ＬＭ ＳＥ）能有效地对机器人进行实时导航和避撞．在预测过程中，根据导航的不同阶段和预测误差的变化情况，采用Ｆｕｚｚｙ 规则动态地调整误差函数中的权重，使预测过程尽可能准确．导航算法的基本思想是首先通过预测算法来获得移动机器人的运动信息，然后虚力系统根据预测信息决定机器人的未来运动，仿真结果表明该方法实时性好，能准确躲避障碍物并且到达目标点

一种多移动机器人避碰规划方法

本文采用集中预规划方法 ,通过调整机器人的运动速度实现多机器人避碰 ,所提算法的基本思想为 :将机器人的运动路径分段 ,然后按避碰要求对机器人通过各段的时间进行约束 ,从而将避碰问题转化为高维线性空间的优化问题 ,并进一步将其转化为线性方程的求解 ,使问题具有明确的解析解 .由于该方法的复杂度较高 ,在实现过程中采用了多种方法降低复杂度 ,简化计算 .本文给出了该算法的基本思路 ,有关定理及证明 ,算法的化简方法 ,最后给出了实验结果及分析 .