The goal of this study is to early diagnose AC through medical image analysis. The perspective is to provide medical professionals with tools that can assist them in an early diagnosis of the disease and evaluate the effectiveness of the provided tools. The context of the study are 55 MRI scans belonging to 55 patients, out of which 32 are affected by AC and 23 are not.At this point, we address the following two research questions (RQs):\({\textbf {RQ}}_1\) Can AC be diagnosed using Model Checking and radiomic features? We are interested in studying if it is possible to diagnose AC using automatic methodology. More precisely, we want to investigate whether radiomic features can be used to model a patient and can be used as a vector to detect the presence of AC in medical images. This research question aims to develop an automatic approach that extracts radiomic features from MRI and uses these features to create a formal model, then this model is used to verify if a patient is affected by AC or not using the Model Checking technique and formal properties.\({\textbf {RQ}}_2\) To what extent does the proposed approach for AC diagnosis perform in terms of accuracy when compared to traditional diagnostic modalities? We want to evaluate the effectiveness of the proposed tool when compared to traditional diagnostic modalities, i.e., traditional diagnostics performed by radiologists with different levels of experience. This research question aims to assess the effectiveness of our tool and identify possible usages.We answer our research questions in three steps. First, we collected Digital Imaging and Communications in Medicine (DICOM) images from 55 patients, i.e., 32 affected by AC and 23 negatives. Second, we develop an automatic approach using radiomic features and Model Checking to automatically detect patients affected by AC. We also compute evaluation metrics to estimate the effectiveness of our approach in the categorization of patients into healthy and afflicted groups. Third, we ask radiologists to determine, using MRI images, whether patients were affected by AC or not and we compare the results with those obtained by our tool to assess its effectiveness and potential applications.DatasetIn this retrospective study, we used a dataset provided by Professor Marcello Zappia. This dataset consists of DICOM images from 55 patients who faced MRIs between 2022 and 2024. All MRI scans were carried out at the “Istituto Diagnostico Varelli SRL” and the Bioethics Committee of the University of Molise approved the study and waived the requirement for informed consent and the further need of guidelines (prot. no. 27789 of 12.06.2024). We enrolled 55 patients who arrived at our hospital with acute shoulder pain and limited movement, 32 were affected by AC and 23 were not.Inclusion criteria:Exclusion criteria:
Other etiologies of shoulder pain;
Other etiologies of limited shoulder movement;
Denied consent to share data;
Artifacts during MRI acquisition;
Previous adhesive capsulitis.
Note that comorbidites, i.e., diabetes, cancer, or trauma, were not considered exclusion criteria, but they were not used to build the model.On MRI images we evaluated:
The increased signal intensity of the inferior glenohumeral ligament on fat-saturated T2-weighted sequences;
Axillary pouch thickening over 4 mm;
Thickening of the coracohumeral ligament and capsule at the rotator cuff interval;
Obliteration of the triangular fat pad inferior to the coracohumeral ligament;
Poor capsular distension;
Synovial hypertrophy;
Tissue scarring at the rotator interval.
MRI dataset was composed of: Coronal STIR, Sagittal STIR, Sagittal T2, Coronal T1, Axial PD FS. All the sequences were acquired with thickness of 3,5 mm and FOV 160-180. Thus, based on this criterion, patients were categorized as either “capsulitis” or “non-capsulitis”, i.e. affected/not affected by AC disease.For this retrospective study, we did not perform a Region of Interest (ROI) analysis on the images; rather, we examined the entire slice. On average, 22 slices per patient were analyzed, covering both coronal and sagittal acquisitions.Methodology to automatically diagnose adhesive capsulitisFigure 1Workflow of our methodology.We define a Model Checking-based methodology to diagnose AC using medical images. Figure 1 shows the workflow of our methodology consisting of three stages: (i) Model Building, (ii) Properties Definition & Translation, and (iii) Formal Verification. In the following, we provide a detailed overview of each stage in our methodology describing the steps linked to each respective stage.Feature extraction. To build the formal model of a patient we need to collect radiomics features from a DICOM image. To do so, we use PyRadiomics25, an open-source Python package, to extract radiomics features from medical imaging. It aligns with the directives established by the Image Biomarker Standardization Initiative (IBSI)26 and facilitates the processing and extraction of radiomics features from medical imaging data using a wide range of engineered formulas and algorithms26. The available features are divided into six primary groups:
First-order features (FIRST). These describe the distribution of voxel intensities within the considered image region. Within this group, one can distinguish features based on intensity and features based on the histogram, in total this group contains 19 different features;
Gray-level co-occurrence matrix features (GLCM). These are part of textural features and provide spatial information about the distribution of gray levels. Specifically, they represent the number of times a combination of two levels occurs in two pixels in the image separated by a distance of \(\delta\) pixels along an angle \(\alpha\). It groups 24 different features;
Gray-level dependence matrix features (GLDM). Gray-level dependence is defined as the number of connected voxels within the distance \(\delta\) that depend on the central voxel. This group contains 14 features;
Gray-level run length matrix features (GLRLM). Sequences are defined as the length, in the number of pixels, of consecutive pixels with the same gray value, in total it collects 16 features;
Gray-level size zone matrix features (GLSZM). A zone is defined as the number of connected voxels that share the same gray intensity, in total this group contains 16 different features;
Neighborhood gray-tone difference matrix features (NGTDM). It quantifies the difference between a gray-level value and the mean value of neighboring voxels. It contains 5 different features.
Initially, all the features of each class were computed. In total, we have 94 features for each patient for each sequence (coronal and sagittal). Due to the high number of features for each patient, we decided to perform Feature Selection to list all significant features not redundant. Successively, we carried out Feature Selection, analyzing radiomics features through Weka27, which is an open-source software developed in New Zealand under the General Public License. This reduction process yielded 30 features, categorized into the six classes defined in the radiomic standards. Feature Selection and the Model Building Step will be solved in single-class mode, i.e. features are studied by Feature Class and no connections between different classes are analyzed. Tables 1 and 2 list all features for each class involved in our experimentation.Table 1 Most relevant features for FIRST, GLCM and GLDM classes.Table 2 Most relevant features for GLRLM, GLSZM and SHAPE classes.Model building. Before creating the formal model, we need to discretize the features. To do so, we used three levels of values: low L, medium M, and high H. Then, the discretized values were used to build the formal model. Basically, we model each slice of the DICOM image as a process that combines all relevant features. At the end of these steps, the formal model representing the patient is built.Our formal model mimics how extracted features appear in each slice of a given medical exam. More in detail, using the Calculus of Communicating System (CCS)28, we can write models in which there are as many processes as there are radiological examination slices. In each process, there is a discretized level for each feature. An example of the CCS formal model is provided in Table 3. The operator nil determines the termination of the model. Also present in each process is the \(+\) operator with which all alternating combinations of features are concatenated. If between two features F1, and F2, the process is F1.F2, the other combination will be F2.F1. Thus interleaving between features is implemented, i.e. their simultaneous execution. This means that the order in which features appear in a process does not matter.To check whether a formal model of a patient exposes AC we need to define formal properties able to identify this disease over the image features.Table 3 Example of CCS model of a patient.Properties definition & translation. To define formal properties identifying AC, we ask radiologists to select patients with evident disease symptoms. Starting from this subgroup of 6 patients, Formal Methods experts, and radiologists defined possible composition of features and discretization level eligible to identify the disease. Then, these compositions are translated into temporal logic formulae which aim to merge commonalities among patients in identical health states enhancing the visibility of their health condition and highlighting patterns indicating healthiness/disease.Formal verification. The last stage of our methodology involves formal verification. To do so, a Model Checker tool is used to automatically verify formal properties against the patient models. This tool is able to explore the state space and verify the properties at each state. The Model Checker takes as input both the formal model and the properties. Following an assessment of whether the model fulfills the given property or not, it yields a binary truth value as its output: TRUE if the model meets the property, FALSE if it does not. In our specific case, if the Model Checker returns TRUE it means that the patient under analysis is affected by AC. Instead, an output equal to FALSE indicates that the patient does not present disease.Participants’ selection and demographicsGiven the study context, selecting a broader range of participants would not have been feasible, since our aim was to involve professionals with sufficient expertise in MSK. Hence, we selected participants through a convenience sampling process, among radiologists experienced with MSK. More in detail, we extended invitations to a total of 11 professional radiologists asking them to participate in the diagnostic task. We sent them an invitation message explaining the goals of our study and clarifying that (i) the participation in the experimentation is voluntary, (ii) personal data will be treated as strictly confidential, (iii) the approximate time to categorize patients was estimated to be about 20 min and a participant can withdraw at any time. The survey has been administered through e-mails. The whole process of participants’ selection, invitation, and collecting responses took about 1 month.In the end, we gathered 11 responses as each selected participant completed the diagnostic task. The MSK radiology experience of respondents varies as follows:
1 radiologist with 20 years of experience in musculoskeletal radiology;
3 specialists in radiology with an average of 5–7 years of experience in MSK;
3 specialists in radiology with an average of 2 years of experience in MSK;
4 radiology residents with no years of experience in MSK.
For the sake of ease, we grouped participants into 3 levels of experience: 4 of the participants had a Beginner Level (Radiology Residents), 3 an Intermediate Level (Early Professionals), and 4 an Expert Level (Professionals Radiologists). Thus, to answer RQ\(_2\) we involve three groups of radiologists categorized by their experience. Participants were asked to determine, based on anonymized MRI images complete of both coronal and sagittal planes, whether patients were affected by AC or not.Analysis methodologyTo address RQ\(_1\), we report results achieved by our methodology on the dataset described in the Dataset Section. It should be underlined that, for each patient, we build a formal model considering both the two different orientations of the imaging plane, i.e., sagittal and coronal sequences. In particular, the model creation requires on average 0.11 seconds per patients having about 22 slices in its medical examination. Thus, for each patient, we extract and select features from both sequences to build the formal patient model as described in Model Building step.Then, according to Properties Definition & Translation step, we define formal properties able to catch the distinctive disease marks. We define properties for both sagittal and coronal sequences, i.e., we combine properties for both imaging planes with the logical “OR” operator, hence the overall result is true if at least one of the individual plans is true. Note that to analyze a patients, i.e., to verify the formal property on the patient model, our approach requires 2.62 seconds per patients having about 22 slices. The execution times were recorded using a machine equipped with 13\(^{th}\) Gen Intel(R) Core(TM) i9-13900HX (2.20 GHz) processor and 32GB RAM. As operating system it was equipped with Windows 11.To address RQ\(_2\), we show and compare results achieved by our methodology with those collected with administration through the diagnostic task survey, and we discuss them.