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.


    Access

    Download


    Export, share and cite



    Title :

    Multi-Robot Motion Planning: A Timed Automata Approach



    Publication date :

    2004-01-01


    Remarks:

    Quottrup , M M , Bak , T & Izadi-Zamanabadi , R 2004 ' Multi-Robot Motion Planning: A Timed Automata Approach ' .


    Type of media :

    Paper


    Type of material :

    Electronic Resource


    Language :

    English


    Classification :

    DDC:    629



    Simulation of Cyber-Physical Intelligent Mechatronic Component Behavior Using Timed Automata Approach

    Santos, Adriano A. / da Silva, António Ferreira / Pereira, Filipe | Springer Verlag | 2022


    Methods for Modeling Urban Road Traffic Using Timed Automata

    Avram, Camelia / Machado, Jose / Astilean, Adina | TIBKAT | 2020


    Approach to analyzing AADL end-to-end flow latency based on timed automata

    Lian, Xiaoli / Zhang, Li | British Library Online Contents | 2015


    An Innovative Approach for Modelling Urban Road Traffic Using Timed Automata and Formal Methods

    Eduardo Valente / Camelia Avram / José Machado et al. | DOAJ | 2018

    Free access

    Runtime Verification of Railway Interlocking Software with Parametric Timed Automata

    Chai, Ming / Wang, Haifeng / Zhang, Jian et al. | IEEE | 2018