Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Karen Godary-Dejean Connect in order to contact the contributor
Submitted on : Monday, September 25, 2017 - 10:37:39 AM
Last modification on : Friday, August 5, 2022 - 3:03:31 PM
Long-term archiving on: : Tuesday, December 26, 2017 - 12:48:14 PM


Files produced by the author(s)



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⟩



Record views


Files downloads