Multi-Robot Motion Planning: A Timed Automata Approach

Michael Melholt Quottrup, Thomas Bak, Roozbeh Izadi-Zamanabadi

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskning

Resumé

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 feed-back 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.
OriginalsprogEngelsk
TitelProceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004
Publikationsdato2004
Sider4417-4422
StatusUdgivet - 2004
BegivenhedMulti-Robot Motion Planning: A Timed Automata Approach -
Varighed: 19 maj 2010 → …

Konference

KonferenceMulti-Robot Motion Planning: A Timed Automata Approach
Periode19/05/2010 → …

Citer dette

Quottrup, M. M., Bak, T., & Izadi-Zamanabadi, R. (2004). Multi-Robot Motion Planning: A Timed Automata Approach. I Proceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004 (s. 4417-4422)
Quottrup, Michael Melholt ; Bak, Thomas ; Izadi-Zamanabadi, Roozbeh. / Multi-Robot Motion Planning: A Timed Automata Approach. Proceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004. 2004. s. 4417-4422
@inproceedings{88c38490416811da8d54000ea68e967b,
title = "Multi-Robot Motion Planning: A Timed Automata Approach",
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 infra-structure of robots with feed-back 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.",
author = "Quottrup, {Michael Melholt} and Thomas Bak and Roozbeh Izadi-Zamanabadi",
year = "2004",
language = "English",
pages = "4417--4422",
booktitle = "Proceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004",

}

Quottrup, MM, Bak, T & Izadi-Zamanabadi, R 2004, Multi-Robot Motion Planning: A Timed Automata Approach. i Proceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004. s. 4417-4422, Multi-Robot Motion Planning: A Timed Automata Approach, 19/05/2010.

Multi-Robot Motion Planning: A Timed Automata Approach. / Quottrup, Michael Melholt; Bak, Thomas; Izadi-Zamanabadi, Roozbeh.

Proceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004. 2004. s. 4417-4422.

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskning

TY - GEN

T1 - Multi-Robot Motion Planning: A Timed Automata Approach

AU - Quottrup, Michael Melholt

AU - Bak, Thomas

AU - Izadi-Zamanabadi, Roozbeh

PY - 2004

Y1 - 2004

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 feed-back 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 feed-back 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.

M3 - Article in proceeding

SP - 4417

EP - 4422

BT - Proceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004

ER -

Quottrup MM, Bak T, Izadi-Zamanabadi R. Multi-Robot Motion Planning: A Timed Automata Approach. I Proceedings of the IEEE 2004 International Conference on Robotics and Automation, New Orleans, LA. April 2004. 2004. s. 4417-4422