University of Molise, Campobasso (ITALY)
University of Campania "Luigi Vanvitelli", Napoli (ITALY)
AOU Careggi University Hospital, Firenze (ITALY)
University Politecnica delle Marche, Ancona (ITALY)
CADP (Construction and Analysis of Distributed Processes)
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.
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
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
Department of Engineering
University of Sannio
RCOST - Ex Post Office Building
Via Traiano 1
Tel: +39 0824 305552
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|