Model checking properties with identity binding in space-time

Spatial logics are formalisms for expressing topological properties of structures based on geometrical entities and relations. Their models range from topological spaces to general graphs, and the properties of interest often concern reachability over infinite paths with a wide range of applications. In this thesis, we consider an extension of the logic SLCS, the Spatial Logic for Closure Spaces, providing it with an existential quantifier. We then equip the logic with temporal operators and provide a linear-time semantics over finite traces. The considered models are graphs. In particular, images are interpreted as graphs, thus model checking of spatial logics can be used for image analysis. Such ideas are the theoretical grounds of the model checker VoxLogicA, and of its applications to image analysis. Considered applications are medical image analysis and model checking of video streams, which is made feasible by exploiting GPU acceleration.