Radiomic Features for Prostate Cancer Grade Detection through Formal Verification

Organisation:	University of Molise, Campobasso (ITALY) University of Campania "Luigi Vanvitelli", Napoli (ITALY) AOU Careggi University Hospital, Firenze (ITALY) University Politecnica delle Marche, Ancona (ITALY)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Medical Systems
Period:	2021
Size:	n/a
Description:	Prostate cancer is commonly diagnosed by prostate biopsy or during trans-urethral resection for prostatic hyperplasia. The grade group describes the aggressiveness, and determines whether the patient undergoes definitive treatment or active surveillance. When the cancer is found, the pathologist assigns to the cancer a grade, called Gleason grade group. To assign the cancer grade, the pathologist checks the prostate tissue samples to see how much the tumour tissue is like the normal prostate tissue and to find the two main cell patterns. Each pattern is given a grade (minimum grade close to the normal prostate tissue and maximum grade close to the most abnormal). The two grades are then added to obtain a Gleason grade group. This work proposes the use of formal verification techniques, where the domain experts (pathologists and radiologists) formulate a series of properties to be verified. Therefore, the decision of the system is not based on algorithms, but on the knowledge of domain experts. Moreover, unlike AI-based techniques, formal veriication does not require a great amount of data and also avoids the introduction of bias in the training set. The proposed method takes as input a magnetic resonance image (MRI) and generates a formal model in LOTOS from the MRI slices after discretization. Then, with the support of experts, for each prostate Gleason grade group, a property is formulated to detect it. The properties are then expressed in modal mu-calculus and verified on the model using the EVALUATOR model checker of CADP. If a property holds on the model, the original MRI is marked with the corresponding Gleason grade group. The proposed method obtains an average sensitivity of 0.97 and a specificity value of 1 for all grade groups.
Conclusions:	This work illustrates the usefulness of formal methods and verification tools in detecting the prostate cancer grade groups. The proposed method paves the way to the detection of other kinds of cancers, and may potentially be exploited in the precision medicine context, a promising research field allowing doctors to select treatments that are most likely to help patients based on a genetic understanding of their disease.
Publications:	[Santone-Brunese-Donnarumma-et-al-21] Antonella Santone, Maria Chiara Brunese, Federico Donnarumma, Pasquale Guerriero, Francesco Mercaldo, Alfonso Reginelli, Vittorio Miele, Andrea Giovagnoni, and Luca Brunese. "Radiomic Features for Prostate Cancer Grade Detection through Formal Verification". La Radiologia Medica 126:688-697, 2021. Available on-line at: https://pubmed.ncbi.nlm.nih.gov/33394366/ or from the CADP Web site in PDF or PostScript
Contact:	Antonella Santone Department of Engineering University of Sannio RCOST - Ex Post Office Building Via Traiano 1 I-82100 Benevento ITALY Email: santone@unisannio.it Tel: +39 0824 305552
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page