Multi-valued model checking IoT and intelligent systems with commitment protocols in multi-source data environments

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.contributor.authorDrawel, Nagat
dc.date.accessioned2024-05-19T14:45:54Z
dc.date.available2024-05-19T14:45:54Z
dc.date.issued2024
dc.departmentİstinye Üniversitesien_US
dc.description.abstractIn today's world of connectivity, various domains use different multi-sensor Internet of Things (IoT) and Intelligent Systems (IS) applications. These applications involve extensive interactions between thousands or millions of components in open environments, which challenges verifying their reliability and efficiency. This paper introduces the first investigation in verifying IoT applications and intelligent systems in multi-source data settings with multi-agent commitment protocols in uncertain or inconsistent environments. Specifically, we present original and efficient solutions for modeling and verifying these systems with conditional and unconditional commitment protocols under uncertain or inconsistent settings. We introduce 4v-CTLc and 4v-CTLcc, multi-valued logics of commitment for reasoning about inconsistency over these systems that expand 3v-CTLc and 3v-CTLcc for reasoning about uncertainty. Moreover, we introduce new reduction algorithms for reducing our multi-valued model checking problems to the two-valued ones. To implement these algorithms, we develop two new automatic verification tools. The first tool translates the multi-valued logics to CTL and automatically interacts with the NuSMV model checker. The second tool translates these logics to the two-valued versions, CTLc and CTLcc, and automatically interacts with the MCMAS+ model checker. We apply our verification approaches to a Smart Home, a Smart Hospital and a Smart Mortgage system with multi-source data as case studies using sets of properties, including safety, liveness and reachability. The experimental results obtained by the proposed multi-valued model checking techniques proved these techniques' high efficiency and applicability to modeling and verifying intelligent and autonomous multi-source data systems.en_US
dc.identifier.doi10.1016/j.inffus.2023.102048
dc.identifier.issn1566-2535
dc.identifier.issn1872-6305
dc.identifier.scopus2-s2.0-85173609384en_US
dc.identifier.scopusqualityQ1en_US
dc.identifier.urihttps://doi.org10.1016/j.inffus.2023.102048
dc.identifier.urihttps://hdl.handle.net/20.500.12713/5386
dc.identifier.volume102en_US
dc.identifier.wosWOS:001159372200001en_US
dc.identifier.wosqualityN/Aen_US
dc.indekslendigikaynakWeb of Scienceen_US
dc.indekslendigikaynakScopusen_US
dc.language.isoenen_US
dc.publisherElsevieren_US
dc.relation.ispartofInformation Fusionen_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.subjectIot'sen_US
dc.subjectIntelligent Systems (Is) Commitmenten_US
dc.subjectLattice-Valued Propositional Logicsen_US
dc.subjectUncertaintyen_US
dc.subjectInconsistencyen_US
dc.titleMulti-valued model checking IoT and intelligent systems with commitment protocols in multi-source data environmentsen_US
dc.typeArticleen_US

Dosyalar

Koleksiyon

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