Abstract
This paper describes how interacting timed automata can be used to model, analyze, and verify motion planning problems for systems with multiple mobile robots. The method assumes an infra-structure of simple unicycle type robots, moving on a planar grid. The motion of the robots, including simple kinematics, is captured in an automata formalism that allows formal composition and symbolic reasoning. The verification software UPPAAL is used to verify specification requirements formulated in computational tree logic (CTL), generating all feasible trajectories that satisfy specifications. The results of the planning are demonstrated in a testbed that allows execution of the planned paths and motion primitives by synchronizing the planning results from UPPAAL with actual robotic vehicles. The planning problem may be modified online by moving obstacles in the physical environment, which causes a re-planning and modified execution.
Original language | English |
---|---|
Book series | IFAC Proceedings Volumes (IFAC-PapersOnline) |
Volume | 37 |
Issue number | 8 |
Pages (from-to) | 597-602 |
Number of pages | 6 |
ISSN | 1474-6670 |
Publication status | Published - 1 Jan 2004 |
Event | IFAC/EURON Symposium on Intelligent Autonomous Vehicles - Lisbon, Portugal Duration: 5 Jul 2004 → 7 Jul 2004 |
Conference
Conference | IFAC/EURON Symposium on Intelligent Autonomous Vehicles |
---|---|
Country/Territory | Portugal |
City | Lisbon |
Period | 05/07/2004 → 07/07/2004 |
Keywords
- Automata
- Formal verification
- Mobile robots
- Planning