A Framework for Multi-Robot Motion Planning from Temporal Logic Specifications

T. John Koo, Rongqing Li, Michael Melholt Quottrup, Charles Clifton, Roozbeh Izadi-Zamanabadi, Thomas Bak

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

9 Citationer (Scopus)
1033 Downloads (Pure)

Resumé

We propose a framework for the coordination of a network of robots with respect to formal requirement specifications expressed in temporal logics. A regular tessellation is used to partition the space of interest into a union of disjoint regular and equal cells with finite facets, and each cell can only be occupied by a robot or an obstacle. Each robot is assumed to be equipped
with a finite collection of continuous-time nonlinear closed-loop dynamics to be operated in. The robot is then modeled as a hybrid automaton for capturing the finitely many modes of operation for either staying within the current cell or reaching an adjacent cell through the corresponding facet. By taking the motion capabilities into account, a bisimilar discrete abstraction of the hybrid automaton can be constructed. Having the two systems bisimilar, all properties that are expressible in temporal logics such as Linear-time Temporal Logic, Computation Tree Logic, and -calculus can be preserved. Motion planning can then be performed at a discrete level by considering the parallel composition of discrete abstractions of the robots with a requirement specification given in a suitable temporal logic. The bisimilarity ensures that the discrete planning solutions are executable by the robots. For demonstration purpose, a finite automaton is used as the abstraction and the requirement specification is expressed in Computation Tree Logic. The model checker Cadence SMV is used to generate coordinated verified motion planning solutions.
Two autonomous aerial robots are used to demonstrate how the proposed framework may be applied to solve coordinated motion planning problems.
OriginalsprogEngelsk
TidsskriftScience in China. Series F: Information Sciences
Vol/bind55
Udgave nummer7
Sider (fra-til)1675-1692
Antal sider18
ISSN1009-2757
DOI
StatusUdgivet - 2012

Fingerprint

Temporal logic
Motion planning
Robots
Specifications
Finite automata
Demonstrations
Antennas
Planning
Chemical analysis

Citer dette

Koo, T. John ; Li, Rongqing ; Quottrup, Michael Melholt ; Clifton, Charles ; Izadi-Zamanabadi, Roozbeh ; Bak, Thomas. / A Framework for Multi-Robot Motion Planning from Temporal Logic Specifications. I: Science in China. Series F: Information Sciences. 2012 ; Bind 55, Nr. 7. s. 1675-1692.
@article{6ac2d860b04111dda82d000ea68e967b,
title = "A Framework for Multi-Robot Motion Planning from Temporal Logic Specifications",
abstract = "We propose a framework for the coordination of a network of robots with respect to formal requirement specifications expressed in temporal logics. A regular tessellation is used to partition the space of interest into a union of disjoint regular and equal cells with finite facets, and each cell can only be occupied by a robot or an obstacle. Each robot is assumed to be equippedwith a finite collection of continuous-time nonlinear closed-loop dynamics to be operated in. The robot is then modeled as a hybrid automaton for capturing the finitely many modes of operation for either staying within the current cell or reaching an adjacent cell through the corresponding facet. By taking the motion capabilities into account, a bisimilar discrete abstraction of the hybrid automaton can be constructed. Having the two systems bisimilar, all properties that are expressible in temporal logics such as Linear-time Temporal Logic, Computation Tree Logic, and -calculus can be preserved. Motion planning can then be performed at a discrete level by considering the parallel composition of discrete abstractions of the robots with a requirement specification given in a suitable temporal logic. The bisimilarity ensures that the discrete planning solutions are executable by the robots. For demonstration purpose, a finite automaton is used as the abstraction and the requirement specification is expressed in Computation Tree Logic. The model checker Cadence SMV is used to generate coordinated verified motion planning solutions.Two autonomous aerial robots are used to demonstrate how the proposed framework may be applied to solve coordinated motion planning problems.",
author = "Koo, {T. John} and Rongqing Li and Quottrup, {Michael Melholt} and Charles Clifton and Roozbeh Izadi-Zamanabadi and Thomas Bak",
year = "2012",
doi = "10.1007/s11432-012-4605-8",
language = "English",
volume = "55",
pages = "1675--1692",
journal = "Science China Information Sciences",
issn = "1674-733X",
publisher = "Zhongguo Kexue Zazhishe",
number = "7",

}

A Framework for Multi-Robot Motion Planning from Temporal Logic Specifications. / Koo, T. John; Li, Rongqing; Quottrup, Michael Melholt; Clifton, Charles; Izadi-Zamanabadi, Roozbeh; Bak, Thomas.

I: Science in China. Series F: Information Sciences, Bind 55, Nr. 7, 2012, s. 1675-1692.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - A Framework for Multi-Robot Motion Planning from Temporal Logic Specifications

AU - Koo, T. John

AU - Li, Rongqing

AU - Quottrup, Michael Melholt

AU - Clifton, Charles

AU - Izadi-Zamanabadi, Roozbeh

AU - Bak, Thomas

PY - 2012

Y1 - 2012

N2 - We propose a framework for the coordination of a network of robots with respect to formal requirement specifications expressed in temporal logics. A regular tessellation is used to partition the space of interest into a union of disjoint regular and equal cells with finite facets, and each cell can only be occupied by a robot or an obstacle. Each robot is assumed to be equippedwith a finite collection of continuous-time nonlinear closed-loop dynamics to be operated in. The robot is then modeled as a hybrid automaton for capturing the finitely many modes of operation for either staying within the current cell or reaching an adjacent cell through the corresponding facet. By taking the motion capabilities into account, a bisimilar discrete abstraction of the hybrid automaton can be constructed. Having the two systems bisimilar, all properties that are expressible in temporal logics such as Linear-time Temporal Logic, Computation Tree Logic, and -calculus can be preserved. Motion planning can then be performed at a discrete level by considering the parallel composition of discrete abstractions of the robots with a requirement specification given in a suitable temporal logic. The bisimilarity ensures that the discrete planning solutions are executable by the robots. For demonstration purpose, a finite automaton is used as the abstraction and the requirement specification is expressed in Computation Tree Logic. The model checker Cadence SMV is used to generate coordinated verified motion planning solutions.Two autonomous aerial robots are used to demonstrate how the proposed framework may be applied to solve coordinated motion planning problems.

AB - We propose a framework for the coordination of a network of robots with respect to formal requirement specifications expressed in temporal logics. A regular tessellation is used to partition the space of interest into a union of disjoint regular and equal cells with finite facets, and each cell can only be occupied by a robot or an obstacle. Each robot is assumed to be equippedwith a finite collection of continuous-time nonlinear closed-loop dynamics to be operated in. The robot is then modeled as a hybrid automaton for capturing the finitely many modes of operation for either staying within the current cell or reaching an adjacent cell through the corresponding facet. By taking the motion capabilities into account, a bisimilar discrete abstraction of the hybrid automaton can be constructed. Having the two systems bisimilar, all properties that are expressible in temporal logics such as Linear-time Temporal Logic, Computation Tree Logic, and -calculus can be preserved. Motion planning can then be performed at a discrete level by considering the parallel composition of discrete abstractions of the robots with a requirement specification given in a suitable temporal logic. The bisimilarity ensures that the discrete planning solutions are executable by the robots. For demonstration purpose, a finite automaton is used as the abstraction and the requirement specification is expressed in Computation Tree Logic. The model checker Cadence SMV is used to generate coordinated verified motion planning solutions.Two autonomous aerial robots are used to demonstrate how the proposed framework may be applied to solve coordinated motion planning problems.

UR - http://www.scopus.com/inward/record.url?scp=84862610821&partnerID=8YFLogxK

U2 - 10.1007/s11432-012-4605-8

DO - 10.1007/s11432-012-4605-8

M3 - Journal article

VL - 55

SP - 1675

EP - 1692

JO - Science China Information Sciences

JF - Science China Information Sciences

SN - 1674-733X

IS - 7

ER -