Formal methods for prostate cancer Gleason score and treatment prediction using radiomic biomarkers

Prostate cancer is a significant public health burden and a major cause of morbidity and mortality among men worldwide. Only in 2018 were reported 1.3 million of new diagnosed patients. Usually an invasive trans-perineal biopsy is the way to diagnose prostate cancer grade by prostate tissue removal. In this paper we propose a non invasive method to detect the prostate cancer grade (the so-called Gleason score) by computing radiomic biomarkers from magnetic resonance images. Furthermore, the proposed method predicts whether the cancer is suitable for the surgery treatment basing on the pathologist and surgeon suggestions. We represent patient magnetic resonances in terms of formal models and, through an algorithm designed by authors, we infer a set of properties aimed to predict the Gleason score and the treatment. By exploiting a formal verification environment, the properties are verified on two different real-world data-sets, the first one is composed of 36 patients, while the second one of 26, confirming the effectiveness of the proposed method.