Model Checking of Spatial Logic

Analysis of spatial behaviors of safety-critical systems attracts more and more attention in the filed of cyber physical systems and image processing. The major problem is expressiveness and verifiability for modeling and analysis of spatial behaviors. In order to verify the satisfiability problem of spatial properties, in this paper, we propose a novel topometric model through inducing a topological space with metric distance. For the spatial logic, we specify spatial properties with S4u in continuous regions, which are encoded S4u formula to RCC-8 relations, and discrete spatial regions, whose evolution is achieved through extending S4u with spatial near and until, named S4u ^e . We present a spatial model checking algorithm to verify if an S4u spatial term or formula satisfies the topometric model. We exemplify the applicability of the approach on obstacle avoidance-based path planning of robots.