Sampling-Based Reactive Synthesis for Nondeterministic Hybrid Systems

被引:1
作者
Ho, Qi Heng [1 ]
Sunberg, Zachary N. [1 ]
Lahijanian, Morteza [1 ]
机构
[1] Univ Colorado, Dept Aerosp Engn Sci, Boulder, CO 80309 USA
关键词
Formal methods in robotics and automation; hybrid logical/dynamical planning and verification; motion andpath planning; planning under uncertainty; FEEDBACK;
D O I
10.1109/LRA.2023.3340029
中图分类号
TP24 [机器人技术];
学科分类号
080202 ; 1405 ;
摘要
This letter introduces a sampling-based strategy synthesis algorithm for nondeterministic hybrid systems with complex continuous dynamics under temporal and reachability constraints. We model the evolution of the hybrid system as a two-player game, where the nondeterminism is an adversarial player whose objective is to prevent achieving temporal and reachability goals. The aim is to synthesize a winning strategy - a reactive (robust) strategy that guarantees the satisfaction of the goals under all possible moves of the adversarial player. Our proposed approach involves growing a (search) game-tree in the hybrid space by combining sampling-based motion planning with a novel bandit-based technique to select and improve on partial strategies. We show that the algorithm is probabilistically complete, i.e., the algorithm will asymptotically almost surely find a winning strategy, if one exists. The case studies and benchmark results show that our algorithm is general and effective, and consistently outperforms state of the art algorithms.
引用
收藏
页码:931 / 938
页数:8
相关论文
共 30 条
  • [11] Kleinbort M., 2019, IEEE Robot. Autom. Lett., V4, pi
  • [12] Synthesis for Robots: Guarantees and Feedback for Robot Behavior
    Kress-Gazit, Hadas
    Lahijanian, Morteza
    Raman, Vasumathi
    [J]. ANNUAL REVIEW OF CONTROL, ROBOTICS, AND AUTONOMOUS SYSTEMS, VOL 1, 2018, 1 : 211 - 236
  • [13] Temporal-Logic-Based Reactive Mission and Motion Planning
    Kress-Gazit, Hadas
    Fainekos, Georgios E.
    Pappas, George J.
    [J]. IEEE TRANSACTIONS ON ROBOTICS, 2009, 25 (06) : 1370 - 1381
  • [14] Model checking of safety properties
    Kupferman, O
    Vardi, MY
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (03) : 291 - 314
  • [15] Lahijanian M, 2014, IEEE INT CONF ROBOT, P3005, DOI 10.1109/ICRA.2014.6907292
  • [16] Randomized kinodynamic planning
    LaValle, SM
    Kuffner, JJ
    [J]. INTERNATIONAL JOURNAL OF ROBOTICS RESEARCH, 2001, 20 (05) : 378 - 400
  • [17] Sufficient Conditions for Optimality in Finite-Horizon Two-Player Zero-Sum Hybrid Games
    Leudo, Santiago J.
    Sanfelice, Ricardo G.
    [J]. 2022 IEEE 61ST CONFERENCE ON DECISION AND CONTROL (CDC), 2022, : 3268 - 3273
  • [18] Luders B., 2010, PROC AIAA GUID NAVIG
  • [19] Dynamical properties of hybrid automata
    Lygeros, J
    Johansson, KH
    Simic, SN
    Zhang, J
    Sastry, SS
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2003, 48 (01) : 2 - 17
  • [20] Monitoring temporal properties of continuous signals
    Maler, O
    Nickovic, D
    [J]. FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2004, 3253 : 152 - 166