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.
Multi-Robot Motion Planning: A Timed Automata Approach
2004-01-01
Quottrup , M M , Bak , T & Izadi-Zamanabadi , R 2004 ' Multi-Robot Motion Planning: A Timed Automata Approach '
Paper
Electronic Resource
English
DDC: | 629 |
Methods for Modeling Urban Road Traffic Using Timed Automata
TIBKAT | 2020
|Approach to analyzing AADL end-to-end flow latency based on timed automata
British Library Online Contents | 2015
|An Innovative Approach for Modelling Urban Road Traffic Using Timed Automata and Formal Methods
DOAJ | 2018
|