Decomposing the model-checking of mobile robotics actions on a grid - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Conference Papers IFAC-PapersOnLine Year : 2017

Decomposing the model-checking of mobile robotics actions on a grid

Abstract

Mobile automated systems, such as robots or machinery for precision agriculture, may be designed to perform actions that vary in space according to information from sensors or to a mission map. To be reliable, the design process of such systems should involve the combined verification of spatial and dynamic properties. We consider here CTL model-checking of a mobile robot's behavior, using the UppAal Timed Automata verifier. We consider reachability properties including path finding. Space is modeled as a 2D grid and the mobile robot path is unknown a priori. In this case, the exhaustive state space exploration of model-checking leads to the generation of many possible movements. This exposes such model-checking to combinatorial issues depending on the grid size and the complexity of system dynamics. In this paper, we propose a decomposition methodology reducing the memory requirements for the verification task. The decomposition is twofold. The grid is decomposed in sub-grids and the model-checking query on the whole grid is decomposed in a set of queries on the sub-grids. A set of test cases and check the validity of the decomposition concept. The decomposition methodology is compared to a simpler method that verifies the reachability property without proceeding to decomposition.
Fichier principal
Vignette du fichier
IFAC_2017_VersionFinale.pdf (354.17 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

lirmm-01592588 , version 1 (25-09-2017)

Identifiers

Cite

Rim Saddem-Yagoubi, Olivier Naud, Karen Godary-Dejean, Didier Crestani. Decomposing the model-checking of mobile robotics actions on a grid. 20th IFAC World Congress, Jul 2017, Toulouse, France. pp.11156-11162, ⟨10.1016/j.ifacol.2017.08.1236⟩. ⟨lirmm-01592588⟩
333 View
260 Download

Altmetric

Share

More