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 business applications is increasingly explored concerning multi-agent systems? group
social commitments. This study explains a novel extended reduction verification method to modelcheck business applications? critical specification rules using action restricted computation tree logic
(ARCTL). In particular, we aim to conduct the verification process for the CTLGC 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 CTLGC model to an ARCTL model and the CTLGC 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 ? 1014 states MASs, which shows its effectiveness when applied to
real-world applications.