TY - GEN
T1 - Multi-robot planning
T2 - Proceedings- 2004 IEEE International Conference on Robotics and Automation
AU - Quottrup, Michael Melholt
AU - Bak, Thomas
AU - Izadi-Zamanabadi, Roozbeh
PY - 2004/7/5
Y1 - 2004/7/5
N2 - 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 infra-structure 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.
AB - 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 infra-structure 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.
UR - http://www.scopus.com/inward/record.url?scp=3042601420&partnerID=8YFLogxK
U2 - 10.1109/ROBOT.2004.1302413
DO - 10.1109/ROBOT.2004.1302413
M3 - Article in proceeding
AN - SCOPUS:3042601420
SN - 0-7803-8232-3
VL - 2004
T3 - Proceedings - IEEE International Conference on Robotics and Automation
SP - 4417
EP - 4422
BT - IEEE International Conference on Robotics and Automation, 2004. Proceedings. ICRA '04. 2004
PB - IEEE
Y2 - 26 April 2004 through 1 May 2004
ER -