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启动对话，他们提供了指示来帮助机器人安全地应对意外情况。 该项目的研究计划与一项教育和外展计划融合在一起，其中包括针对大学和高中生的丰富机器人相关活动。该研究项目结合了机器人运动计划，正式验证和控制理论的思想和技术，以对应给出多少机器人自治的问题进行严格的答案。受时间逻辑启发的规范语言用于将任务传达给机器人，该机器人的动作是由层次控制器指示的。在最高级别，使用了自动机游戏技术和两种基于细胞分解的离散方案，另一种是基于随机抽样的。在低级别，输入输出线性化与路径和矢量场相结合，用于实施四型和差速器驱动地面车辆的高级计划。人类机器人谈判过程基于时间逻辑公式的内部表示及其定量语义。该项目虽然致力于机器人技术，但会影响许多关键领域，例如网络物理系统（构造正确设计系统），空中交通管制（设计安全的飞机最小能量路径，用于起飞和降落在拥挤的机场），等等。