logo SBA

ETD

Digital archive of theses discussed at the University of Pisa

 

Thesis etd-04172024-113158


Thesis type
Tesi di dottorato di ricerca
Author
BUSSI, LAURA
URN
etd-04172024-113158
Thesis title
Model checking properties with identity binding in space-time
Academic discipline
INF/01
Course of study
INFORMATICA
Supervisors
tutor Prof. Gadducci, Fabio
correlatore Dott. Ciancia, Vincenzo
Keywords
  • GPU acceleration
  • model checking
  • Spatial logics
Graduation session start date
06/05/2024
Availability
Full
Summary
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.
File