Model checking combined trust and commitments in Multi-Agent Systems

Basit Öğe Kaydı
dc.authoridBentahar, Jamal/0000-0002-3136-4849
dc.contributor.authorBaharloo, Narges
dc.contributor.authorBentahar, Jamal
dc.contributor.authorDrawel, Nagat
dc.contributor.authorPedrycz, Witold
dc.date.accessioned2024-05-19T14:45:52Z
dc.date.available2024-05-19T14:45:52Z
dc.date.issued2024
dc.departmentİstinye Üniversitesien_US
dc.description.abstractTrust and social commitments have been studied with different objectives for communication in Multi-Agent Systems (MASs) separately. The purpose of this paper is to present the first logical framework to explore the relationship between two key concepts in autonomous MASs, namely trust and commitments among agents, along with its model checking algorithms. An analysis is performed on this relationship, with a specific emphasis on the perspectives of semantics and model checking. The analysis is carried out within the framework of Trust Computation Tree Logic with Commitments (CTLC) logic, an extended logic built on top of the standard branching temporal Computation Tree Logic (CTL) by including modalities for reasoning about commitments and their fulfillment. Moreover, the study employs a trust operator to facilitate trust reasoning. We propose thus Trust Computation Tree Logic with Commitments (TCTLC), a new logic able to express properties about trust and commitments simultaneously. Such rich properties cannot be expressed in other languages. We introduce the semantics using the extended formalism of interpreted systems. We propose some postulates and proofs that show how we can reason about combined trust and commitments in the logic proposed. New Binary Decision Diagram (BDD)-based algorithms for our logic are presented and implemented as additional libraries of the Model Checker for Multi-Agent Systems (MCMAS), the default model checker of MASs. Furthermore, we prove that although TCTLC extends CTL, its model checking algorithm remains polynomial (P-complete) with respect to the size of the model and the length of the formula. Similarly, the space complexity for concurrent programs also remains unchanged, which is polynomial (PSPACE-complete) with respect to the size of the components within these programs. Finally, to evaluate the proposed technique, we report the experimental results using an industrial case study and compare the results with those obtained on relevant benchmarks.en_US
dc.description.sponsorshipNatural Sciences and Engineering Research Council of Canada (NSERC) through the NSERC Discovery Grant program; NSERC Discovery Grant program; Natural Sciences and Engineering Research Council of Canada (NSERC) through the Horizon Discovery Program; NSERCen_US
dc.description.sponsorshipJamal Bentahar would like to thank the Natural Sciences and Engineering Research Council of Canada (NSERC) for their financial support through the NSERC Discovery Grant program and the Horizon Discovery Program. Witold Pedrycz would also like to thank NSERC for their financial support.en_US
dc.identifier.doi10.1016/j.eswa.2023.122856
dc.identifier.issn0957-4174
dc.identifier.issn1873-6793
dc.identifier.scopus2-s2.0-85179627492en_US
dc.identifier.scopusqualityQ1en_US
dc.identifier.urihttps://doi.org10.1016/j.eswa.2023.122856
dc.identifier.urihttps://hdl.handle.net/20.500.12713/5376
dc.identifier.volume243en_US
dc.identifier.wosWOS:001141110600001en_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-Agent Systemsen_US
dc.subjectVerificationen_US
dc.subjectModel Checkingen_US
dc.subjectTrusten_US
dc.subjectSocial Commitmentsen_US
dc.titleModel checking combined trust and commitments in Multi-Agent Systemsen_US
dc.typeArticleen_US

Dosyalar

Koleksiyon

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