Model Checking in Medical Imaging for Tumor Detection and Segmentation

Abstract--Recent advancements in model checking have demonstrated significant potential across diverse applications, particularly in signal and image analysis. Medical imaging stands out as a critical domain where model checking can be effectively applied to design and evaluate robust frameworks. These frameworks facilitate automatic and semi-automatic delineation of regions of interest within images, aiding in accurate segmentation. This paper provides a comprehensive analysis of recent works leveraging spatial logic to develop operators and tools for identifying regions of interest, including tumorous and non-tumorous areas. Additionally, we examine the challenges inherent to spatial model-checking techniques, such as variability in ground truth data and the need for streamlined procedures suitable for routine clinical practice. Model checking is the process of verifying whether a given structure satisfies a specified logical formula. This concept is general and applies to a wide range of logics and system designs. A fundamental model-checking problem involves determining whether a propositional logic equation is satisfied by a given structure. Model checking is most commonly applied to hardware designs. For software systems, due to undecidability, the methodology cannot be fully algorithmic and may fail to either prove or disprove a given property. Model checking plays a critical role across various applications, serving purposes such as ensuring the correctness of Figure 1: A typical model-checking workflow system properties and minimizing errors in software under development.