MV-Checker: A software tool for multi-valued model checking intelligent applications with trust and commitment

Basit Öğe Kaydı
dc.authoridBentahar, Jamal/0000-0002-3136-4849
dc.contributor.authorAlwhishi, Ghalya
dc.contributor.authorBentahar, Jamal
dc.contributor.authorElwhishi, Ahmed
dc.contributor.authorPedrycz, Witold
dc.date.accessioned2024-05-19T14:45:54Z
dc.date.available2024-05-19T14:45:54Z
dc.date.issued2024
dc.departmentİstinye Üniversitesien_US
dc.description.abstractIntelligent applications are highly susceptible to uncertainty and inconsistency due to the intense and intricate interactions among their autonomous components (or agents), making their verification theoretically and practically challenging. This paper presents the design and implementation of a new open -source and scalable software tool for modeling and verifying intelligent applications with commitment and trust protocols under both uncertainty and inconsistency settings, using reduction -based multi -valued model checking techniques. The proposed tool is equipped with original and novel algorithms that transform our logics of multi -valued commitment (mv-CTLC) and multi -value trust (mv-TCTL) that we recently introduced to their classical twovalued commitment (CTLC) and trust (TCTL) logic versions as well as to Computational Tree Logic (CTL). Moreover, the tool transforms the mv-CTL to CTL, and it is applicable for the classical model checking by transforming the classical logics of trust and commitment to CTL. To demonstrate the practicality and applicability of the proposed tool in real settings, we present and report experimental results over two blockchain-based applications in the healthcare domain. Finally, we provide discussions and comparisons between the proposed approaches regarding scalability and efficiency. Moreover, we provide packages of more than 11 experiments, including the ones we conduct in this paper and enhanced experiments from previous works. Our findings ensure that the proposed approaches and the software tool that implements them are highly efficient and scalable, giving accurate results under varying conditions.en_US
dc.description.sponsorshipMinistry of Higher Education (Libya); Natural Sciences and Engineering Research Council of Canada (NSERC); Concordia University; Khalifa Universityen_US
dc.description.sponsorshipWe would like to thank the Ministry of Higher Education (Libya), the Natural Sciences and Engineering Research Council of Canada (NSERC, Discovery Grant), Concordia University, and Khalifa Univer-sity for their financial support.en_US
dc.identifier.doi10.1016/j.eswa.2023.123113
dc.identifier.issn0957-4174
dc.identifier.issn1873-6793
dc.identifier.scopus2-s2.0-85182892896en_US
dc.identifier.scopusqualityQ1en_US
dc.identifier.urihttps://doi.org10.1016/j.eswa.2023.123113
dc.identifier.urihttps://hdl.handle.net/20.500.12713/5385
dc.identifier.volume245en_US
dc.identifier.wosWOS:001152787400001en_US
dc.identifier.wosqualityN/Aen_US
dc.indekslendigikaynakWeb of Scienceen_US
dc.indekslendigikaynakScopusen_US
dc.language.isoenen_US
dc.publisherPergamon-Elsevier Science Ltden_US
dc.relation.ispartofExpert Systems With Applicationsen_US
dc.relation.publicationcategoryMakale - Uluslararası Hakemli Dergi - Kurum Öğretim Elemanıen_US
dc.rightsinfo:eu-repo/semantics/closedAccessen_US
dc.snmz20240519_kaen_US
dc.subjectMulti-Valued Model Checkingen_US
dc.subjectIntelligent Systems (Is)en_US
dc.subjectTrusten_US
dc.subjectLattice-Valued Propositional Logicsen_US
dc.subjectUncertaintyen_US
dc.subjectInconsistencyen_US
dc.titleMV-Checker: A software tool for multi-valued model checking intelligent applications with trust and commitmenten_US
dc.typeArticleen_US

Dosyalar

Koleksiyon

WoS İndeksli Yayınlar Koleksiyonu
Scopus İndeksli Yayınlar Koleksiyonu