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.