| Summary: | 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.
|
|---|