Purpose: one of typical cancer among men is the prostate tumour. This is the reason why the screening and the early detection is a crucial task to obtain a diagnosis and a subsequent therapy in the shortest possible time.
Materials and Methods: in this paper, with the aim to help radiologists and pathologists for a prompt diagnosis, a method for detecting prostate cancer is proposed. Our analysis starts from the magnetic resonances images (coronal and axial planes), building a labelled transition system for coronal slices and another one for axial, which takes into account a number of non invasive radiomic features. Thus, a set of formulae in temporal logic characterizing the prostate cancer is verified through the model checking technique, to detect the prostate cancer. The proposed method considers magnetic resonance images without the Region Of Interest. This represents one of the major novelty of the method.
Results: the proposed method is evaluated on a data-set composed of 40 patients, obtaining very interesting performances in the discrimination between affected and not affected prostate cancer patients.
Conclusion: the study confirms the effectiveness of the formal methods to discriminate between cancerous and benign prostate MRIs with a method not requiring the ROI of the cancerous area, by obtaining a sensitivity and a specificity equal to 1.