Reduction Model Checking for Multi-Agent Systems of Group Social Commitments
Innumerable industries now use multi-agent systems (MASs) in various contexts, including healthcare, security, and commercial deployments. It is challenging to select reliable business protocols for critically important safety-related systems (e.g., in healthcare). The verification and validation of...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-05-01
|
| Series: | Computation |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2079-3197/10/6/84 |
| _version_ | 1797488685666533376 |
|---|---|
| author | Bader M. AlFawwaz Faisal Al-Saqqar Atallah AL-Shatnawi |
| author_facet | Bader M. AlFawwaz Faisal Al-Saqqar Atallah AL-Shatnawi |
| author_sort | Bader M. AlFawwaz |
| collection | DOAJ |
| description | Innumerable industries now use multi-agent systems (MASs) in various contexts, including healthcare, security, and commercial deployments. It is challenging to select reliable business protocols for critically important safety-related systems (e.g., in healthcare). The verification and validation of business applications is increasingly explored concerning multi-agent systems’ group social commitments. This study explains a novel extended reduction verification method to model-check business applications’ critical specification rules using action restricted computation tree logic (ARCTL). In particular, we aim to conduct the verification process for the CTL<sup>GC</sup> logic using a reduction algorithm and show its effectiveness to handle MASs with huge models, thus, showing its importance and applicability in large real-world applications. To do so, we need to transform the CTL<sup>GC</sup> model to an ARCTL model and the CTL<sup>GC</sup> formulas into ARCTL formulas. Thus, the developed method was verified with the model-checker new symbolic model verifier (NuSMV), and it demonstrated effectiveness in the safety-critical specification rule support provision. The proposed method can verify up to 2.43462 × 10<sup>14</sup> states MASs, which shows its effectiveness when applied to real-world applications. |
| first_indexed | 2024-03-10T00:05:50Z |
| format | Article |
| id | doaj.art-fd0e6c3e8f044d7db70b985181ed4ecc |
| institution | Directory Open Access Journal |
| issn | 2079-3197 |
| language | English |
| last_indexed | 2024-03-10T00:05:50Z |
| publishDate | 2022-05-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Computation |
| spelling | doaj.art-fd0e6c3e8f044d7db70b985181ed4ecc2023-11-23T16:09:29ZengMDPI AGComputation2079-31972022-05-011068410.3390/computation10060084Reduction Model Checking for Multi-Agent Systems of Group Social CommitmentsBader M. AlFawwaz0Faisal Al-Saqqar1Atallah AL-Shatnawi2Information Systems Department, Prince Hussein Bin Abdullah Faculty for Information Technology, Al al-Bayt University, Mafraq 25113, JordanComputer Science Department, Prince Hussein Bin Abdullah Faculty for Information Technology, Al al-Bayt University, Mafraq 25113, JordanInformation Systems Department, Prince Hussein Bin Abdullah Faculty for Information Technology, Al al-Bayt University, Mafraq 25113, JordanInnumerable industries now use multi-agent systems (MASs) in various contexts, including healthcare, security, and commercial deployments. It is challenging to select reliable business protocols for critically important safety-related systems (e.g., in healthcare). The verification and validation of business applications is increasingly explored concerning multi-agent systems’ group social commitments. This study explains a novel extended reduction verification method to model-check business applications’ critical specification rules using action restricted computation tree logic (ARCTL). In particular, we aim to conduct the verification process for the CTL<sup>GC</sup> logic using a reduction algorithm and show its effectiveness to handle MASs with huge models, thus, showing its importance and applicability in large real-world applications. To do so, we need to transform the CTL<sup>GC</sup> model to an ARCTL model and the CTL<sup>GC</sup> formulas into ARCTL formulas. Thus, the developed method was verified with the model-checker new symbolic model verifier (NuSMV), and it demonstrated effectiveness in the safety-critical specification rule support provision. The proposed method can verify up to 2.43462 × 10<sup>14</sup> states MASs, which shows its effectiveness when applied to real-world applications.https://www.mdpi.com/2079-3197/10/6/84group social commitmentsmodel-checkingmodelingmulti-agent systemssocial commitmentsvalidation |
| spellingShingle | Bader M. AlFawwaz Faisal Al-Saqqar Atallah AL-Shatnawi Reduction Model Checking for Multi-Agent Systems of Group Social Commitments Computation group social commitments model-checking modeling multi-agent systems social commitments validation |
| title | Reduction Model Checking for Multi-Agent Systems of Group Social Commitments |
| title_full | Reduction Model Checking for Multi-Agent Systems of Group Social Commitments |
| title_fullStr | Reduction Model Checking for Multi-Agent Systems of Group Social Commitments |
| title_full_unstemmed | Reduction Model Checking for Multi-Agent Systems of Group Social Commitments |
| title_short | Reduction Model Checking for Multi-Agent Systems of Group Social Commitments |
| title_sort | reduction model checking for multi agent systems of group social commitments |
| topic | group social commitments model-checking modeling multi-agent systems social commitments validation |
| url | https://www.mdpi.com/2079-3197/10/6/84 |
| work_keys_str_mv | AT badermalfawwaz reductionmodelcheckingformultiagentsystemsofgroupsocialcommitments AT faisalalsaqqar reductionmodelcheckingformultiagentsystemsofgroupsocialcommitments AT atallahalshatnawi reductionmodelcheckingformultiagentsystemsofgroupsocialcommitments |