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.
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal-lirmm.ccsd.cnrs.fr/lirmm-01592588
Contributor : Karen Godary-Dejean <>
Submitted on : Monday, September 25, 2017 - 10:37:39 AM
Last modification on : Tuesday, October 29, 2019 - 10:19:42 AM
Long-term archiving on: Tuesday, December 26, 2017 - 12:48:14 PM

File

IFAC_2017_VersionFinale.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

455

Files downloads

276