Multi-Robot Motion Planning: A Timed Automata Approach

Michael Melholt Quottrup, Thomas Bak, Roozbeh Izadi-Zamanabadi

Publikation: Working paperForskning

211 Downloads (Pure)

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
Udgiver<Forlag uden navn>
StatusUdgivet - 2004

Citer dette

@techreport{312a9fe09c2d11db8ed6000ea68e967b,
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",
publisher = "<Forlag uden navn>",
type = "WorkingPaper",
institution = "<Forlag uden navn>",

}

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

<Forlag uden navn>, 2004.

Publikation: Working paperForskning

TY - UNPB

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 - Working paper

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

PB - <Forlag uden navn>

ER -