Language:   Search:   Contact
Zentralblatt MATH has released its new interface!
For an improved author identification, see the new author database of ZBMATH.

Query:
Fill in the form and click »Search«...
Format:
Display: entries per page entries
Zbl 1245.68227
Koo, T.John; Li, Rongqing; Quottrup, Michael M.; Clifton, Charles A.; Izadi-Zamanabadi, Roozbeh; Bak, Thomas
A framework for multi-robot motion planning from temporal logic specifications.
(English)
[J] Sci. China, Inf. Sci. 55, No. 7, 1675-1692 (2012). ISSN 1674-733X; ISSN 1869-1919/e

Summary: 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 $\mu$-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 purposes, 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.
MSC 2000:
*68T40 Robotics
68T20 Problem solving
68T27 AI logics
68Q60 Specification and verification of programs

Keywords: motion planning; multi-robot systems; temporal logic; hybrid automata; discrete abstraction

Highlights
Master Server

### Zentralblatt MATH Berlin [Germany]

© FIZ Karlsruhe GmbH

Zentralblatt MATH master server is maintained by the Editorial Office in Berlin, Section Mathematics and Computer Science of FIZ Karlsruhe and is updated daily.

Other Mirror Sites

Copyright © 2013 Zentralblatt MATH | European Mathematical Society | FIZ Karlsruhe | Heidelberg Academy of Sciences