دورية أكاديمية

Reduction Model Checking for Multi-Agent Systems of Group Social Commitments.

التفاصيل البيبلوغرافية
العنوان: Reduction Model Checking for Multi-Agent Systems of Group Social Commitments.
المؤلفون: AlFawwaz, Bader M., Al-Saqqar, Faisal, AL-Shatnawi, Atallah
المصدر: Computation; Jun2022, Vol. 10 Issue 6, p84-N.PAG, 19p
مصطلحات موضوعية: SOCIAL groups, SOCIAL systems, MULTIAGENT systems
مستخلص: 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 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. [ABSTRACT FROM AUTHOR]
Copyright of Computation is the property of MDPI and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
قاعدة البيانات: Complementary Index
الوصف
تدمد:20793197
DOI:10.3390/computation10060084