Prostate gleason score detection and cancer treatment through real-time formal verification

Currently, there are 3.1 million American men affected by prostate cancer. Early detection represents the only way to safe lives. To evaluate a prostate cancer, the most widespread rank is the so-called Gleason score, based on the microscopic cancer appearance. Once assigned to the diagnosed prostate cancer its relative Gleason score, the correct therapy to be adopted must be promptly defined. To support pathologists and radiologists in timely diagnosis, in this paper we propose a method aimed to infer the Gleason score and the prostate cancer therapy exploiting formal methods. We consider a set of radiomic features directly obtained from magnetic resonance images. For this reason the proposed method is non invasive, since it does not require a biopsy. We model magnetic resonance images of patients as timed automata networks and we assign the Gleason score and the relative treatment, exploiting a set of temporal logic properties. In the experimental analysis, the properties are verified on 36 different patients, confirming the effectiveness of the proposed method with a sensitivity and a specificity equal to 1 for all the evaluated cases in Gleason score inference, and a sensitivity equal to 0.94 and a specificity equal to 1 in treatment prediction.