NRI: Formal Methods for Motion Planning and Control with Human-in-the-Loop

NRI：人在环运动规划和控制的形式化方法

• 批准号: 1426907
• 负责人: Calin Belta
• 金额: $ 48.86万
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-08-01 至 2019-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1426907&HistoricalAwards=false
• 关键词: NRI; Formal; Methods; Motion; Planning

How much autonomy should a robotic system have in a safety critical application? The proposed project addresses this fundamental question. Consider a disaster relief scenario in which an autonomous aerial vehicle (a robot) is required to monitor some areas of interest, while fighting fires and searching for survivors. The survivors should be provided medical assistance and the fires should be extinguished, with priority given to stabilizing and extracting survivors. During the mission, the aerial vehicle should stay away from areas where explosions are likely, so it can continue to do its job. An emergency medical technician (EMT) and firefighter specify the robot?s mission in a way that can be easily understood by the robot. During the execution, depending on what is discovered, the robot makes decisions on its own as long as the high-level specification is not violated. If this is not the case (e.g., there is an obstacle blocking the access to a survivor), the system initiates a dialog with the firefighter and EMT, who provide instructions to help the robot safely cope with the unexpected situation. The research plan of this project is integrated with an education and outreach plan that includes a rich spectrum of robotic-related activities for university and high-school students. This research project combines ideas and techniques from robot motion planning, formal verification, and control theory to provide a rigorous answer to the question of how much autonomy a robot should be given. A specification language inspired by temporal logics is used to communicate the mission to the robot, whose motions are directed by a hierarchical controller. At the top level, automata game techniques and two discretization schemes, one based on cellular decomposition and the other one on randomized sampling, are used. At the low level, input-output linearization combined with path and vector field following are used to implement the high level plans in quadrotors and differential drive ground vehicles. The human-robot negotiation process is based on the internal representation of temporal logic formulas and their quantitative semantics. While directed at robotics, the project impacts a number of safety critical areas, such as cyber physical systems (construction of correct-by-design systems), air traffic control (design of safe minimum-energy paths for airplanes taking off and landing in a crowded airport), etc.

在安全关键应用中，机器人系统应该有多大的自主权？拟议的项目解决了这一根本问题。考虑一个灾难救援场景，其中需要一个自主飞行器（机器人）来监视一些感兴趣的区域，同时灭火和搜索幸存者。应向幸存者提供医疗援助，并应扑灭大火，优先稳定和救出幸存者。在执行使命期间，飞行器应远离可能发生爆炸的区域，以便继续执行任务。紧急医疗技术人员（EMT）和消防员指定机器人？的使命的方式，可以很容易地理解的机器人。 在执行过程中，根据发现的内容，只要不违反高级规范，机器人就会自己做出决定。如果不是这种情况（例如，有障碍物阻挡了接近幸存者的通道），系统启动与消防员和EMT的对话，他们提供指令以帮助机器人安全地科普意外情况。 该项目的研究计划与教育和推广计划相结合，其中包括为大学和高中学生提供的丰富的机器人相关活动。该研究项目结合了机器人运动规划、形式验证和控制理论的思想和技术，为机器人应该拥有多大的自主权提供了严格的答案。受时序逻辑启发的规范语言用于将使命传达给机器人，机器人的运动由分层控制器指导。在顶层，自动机游戏技术和两个离散化方案，一个基于细胞分解和随机抽样，被使用。在低层，输入输出线性化结合路径和矢量场跟踪被用来实现四旋翼和差动驱动地面车辆的高级别计划。人-机器人协商过程基于时态逻辑公式的内部表示及其定量语义。虽然该项目针对机器人技术，但它影响了许多安全关键领域，例如网络物理系统（构建正确的设计系统），空中交通管制（为飞机在拥挤的机场起飞和降落设计安全的最低能量路径）等。