Radiomic features for prostate cancer grade detection through formal verification

Aim: Prostate cancer represents the most common cancer afflicting men. It may be asymptomatic at the early stage. In this paper, we propose a methodology aimed to detect the prostate cancer grade by computing non-invasive shape-based radiomic features directly from magnetic resonance images. Materials and methods: We use a freely available dataset composed by coronal magnetic resonance images belonging to 112 patients. We represent magnetic resonance slices in terms of formal model, and we exploit model checking to check whether a set of properties (formulated with the support of pathologists and radiologists) is verified on the formal model. Each property is related to a different cancer grade with the aim to cover all the cancer grade groups. Results: An average specificity equal to 0.97 and an average sensitivity equal to 1 have been obtained with our methodology. Conclusion: The experimental analysis demonstrates the effectiveness of radiomics and formal verification for Gleason grade group detection from magnetic resonance.