Nick Bezhanishvili ; Vincenzo Ciancia ; David Gabelaia ; Gianluca Grilletti ; Diego Latella et al. - Geometric Model Checking of Continuous Space

lmcs:9060 - Logical Methods in Computer Science, November 22, 2022, Volume 18, Issue 4 -
Geometric Model Checking of Continuous SpaceArticle

Authors: Nick Bezhanishvili ORCID; Vincenzo Ciancia ; David Gabelaia ; Gianluca Grilletti ; Diego Latella ORCID; Mieke Massink

    Topological Spatial Model Checking is a recent paradigm where model checking techniques are developed for the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. Following a recently developed geometric semantics of Modal Logic, we propose an interpretation of SLCS in continuous space, admitting a geometric spatial model checking procedure, by resorting to models based on polyhedra. Such representations of space are increasingly relevant in many domains of application, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We introduce PolyLogicA, a geometric spatial model checker for SLCS formulas on polyhedra and demonstrate feasibility of our approach on two 3D polyhedral models of realistic size. Finally, we introduce a geometric definition of bisimilarity, proving that it characterises logical equivalence.

    Volume: Volume 18, Issue 4
    Published on: November 22, 2022
    Accepted on: October 6, 2022
    Submitted on: February 8, 2022
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,Computer Science - Computer Vision and Pattern Recognition,Computer Science - Graphics,68Q60,F.4.1,D.2.4,I.2.4,I.3.6,I.4.6,I.5.4

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1665 times.
    This article's PDF has been downloaded 430 times.