Multi-robot planning : a timed automata approach
- 1 January 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 5, 4417-4422 Vol.5
- https://doi.org/10.1109/robot.2004.1302413
Abstract
This paper describes how a network of interacting timed automata can be used to model, analyze, and verify motion planning problems in a scenario with multiple robotic vehicles. The method presupposes an infrastructure of robots with feedback controllers obeying simple restriction on a planar grid. The automata formalism merely presents a high-level model of environment, robots and control, but allows composition and formal symbolic reasoning about coordinated solutions. Composition is achieved through synchronization, and the verification software UPPAAL is used for a symbolic verification against specification requirements formulated in computational tree logic (CTL). In this way, all feasible trajectories that satisfy specifications and which moves the robots from a set of initial positions to a set of desired goal positions may be algorithmically analyzed. The trajectories can then subsequently be used as a high-level motion plan for the robots. This paper reports on the timed automata framework, results of two verification experiments, promise of the approach, and gives a perspective for future research.Keywords
This publication has 12 references indexed in Scilit:
- Sold!: auction methods for multirobot coordinationIEEE Transactions on Robotics and Automation, 2002
- Hybrid control of formations of robotsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A formalism for the composition of concurrent robot behaviorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A hybrid control approach to action coordination for mobile robotsAutomatica, 2002
- Discrete abstractions of hybrid systemsProceedings of the IEEE, 2000
- Multi-robot cooperation in the MARTHA projectIEEE Robotics & Automation Magazine, 1998
- Uppaal in a nutshellInternational Journal on Software Tools for Technology Transfer, 1997
- The algorithmic analysis of hybrid systemsTheoretical Computer Science, 1995
- Model-checking for real-time systemsLecture Notes in Computer Science, 1995
- Temporal and Modal LogicPublished by Elsevier ,1990