VoxLogicA: a spatial model checker for declarative image analysis

Belmonte G., Ciancia V., Latella D., Massink M.

Image analysis  Medical imaging  Spatial model checking  Spatial logics  VoxLogicA 

Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis.We explore a new domain, namely (semi-)automatic contouring in Medical Imaging, introducing the tool VoxLogicA which merges the state-of-the-art library of computational imaging algorithms ITK with the unique combination of declarative specification and optimised execution provided by spatial logic model checking. The result is a rapid, logic based analysis development methodology. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA analysis can reach state-of-the-art accuracy, competing with best-in-class algorithms, with the advantage of explainability and easy replicability. Furthermore, due to a two-orders-of-magnitude speedup compared to the existing generalpurpose spatio-temporal model checker topochecker, VoxLogicA enables interactive development of analysis of 3D medical images, which can greatly facilitate the work of professionals in this domain.

Source: TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 281–298, Prague, Czech Republic, 06-11 April 2019

Publisher: Springer International Publishing, New York, USA

Metrics