Formal Methods for Robot Motion Planning with Time and Space Constraints (Extended Abstract)
2021 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature , 2021, p. 1-14Conference paper, Published paper (Refereed)
Abstract [en]
Motion planning is one of the core problems in a wide range of robotic applications. We discuss the use of temporal logics to include complex objectives, constraints, and preferences in motion planning algorithms and focus on three topics: the first one addresses computational tractability of Linear Temporal Logic (LTL) motion planning in systems with uncertain non-holonomic dynamics, i.e. systems whose ability to move in space is constrained. We introduce feedback motion primitives and heuristics to guide motion planning and demonstrate its use on a rover in 2D and a fixed-wing drone in 3D. Second, we introduce combined motion planning and hybrid feedback control design in order to find and follow trajectories under Metric Interval Temporal Logic (MITL) specifications. Our solution creates a path to be tracked, a sequence of obstacle-free polytopes and time stamps, and a controller that tracks the path while staying in the polytopes. Third, we focus on motion planning with spatio-temporal preferences expressed in a fragment of Signal Temporal Logic (STL). We introduce a cost function for a of a path reflecting the satisfaction/violation of the preferences based on the notion of STL spatial and temporal robustness. We integrate the cost into anytime asymptotically optimal motion planning algorithm RRT ⋆ and we show the use of the algorithm in integration with an autonomous exploration planner on a UAV.
Place, publisher, year, edition, pages
Springer Nature , 2021. p. 1-14
Keywords [en]
Feedback control, Motion planning, MTL, RRT, STL, Temporal logic, Computer circuits, Cost functions, Feedback, Fixed wings, Formal methods, Robots, Time sharing systems, Topology, Unmanned aerial vehicles (UAV), Asymptotically optimal, Autonomous exploration, Computational tractability, Hybrid feedback control, Interval temporal logic, Linear temporal logic, Motion planning algorithms, Robot motion planning, Robot programming
National Category
Robotics and automation
Identifiers
URN: urn:nbn:se:kth:diva-311761DOI: 10.1007/978-3-030-85037-1_1ISI: 000884760800001Scopus ID: 2-s2.0-85115185235OAI: oai:DiVA.org:kth-311761DiVA, id: diva2:1655731
Conference
19th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2021, Virtual, Online, 24-26 August 2021
Note
Part of proceedings: ISBN 978-3-030-85036-4
QC 20220503
2022-05-032022-05-032025-02-09Bibliographically approved