Model checking agent-based communities against uncertain group commitments and knowledge
In recent years, the use of Multi-Agent Systems (MASs) to solve complex problems has grown rapidly. Social communicative commitments have been widely employed in such systems as a means of communication allowing heterogeneous agents to cooperate. However, to prevent undesirable outcomes, communicati...
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | , , |
| Published: |
2021
|
| Online Access: | https://dspace.auk.edu.kw/handle/11675/8262 https://www.sciencedirect.com/science/article/abs/pii/S0957417421002335 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1870679719709507584 |
|---|---|
| author | Sultan, Khalid |
| author2 | Bentahar, Jamal Yahyaoui, Hamdi Mizouni, Rabeb |
| author2_role | author author author |
| author_facet | Sultan, Khalid Bentahar, Jamal Yahyaoui, Hamdi Mizouni, Rabeb |
| author_role | author |
| dc.creator.none.fl_str_mv | Sultan, Khalid Bentahar, Jamal Yahyaoui, Hamdi Mizouni, Rabeb |
| dc.date.none.fl_str_mv | 2021-12-22T08:28:06Z 2021-12-22T08:28:06Z 2021-03-10 |
| dc.identifier.none.fl_str_mv | Sultan, K., Bentahar, J., Yahyaoui, H., & Mizouni,R. (2021). Model checking agent-based communities against uncertain groupcommitments and knowledge. Expert Systems with Applications, 177.https://doi.org/10.1016/j.eswa.2021.114792 https://dspace.auk.edu.kw/handle/11675/8262 https://www.sciencedirect.com/science/article/abs/pii/S0957417421002335 |
| dc.publisher.none.fl_str_mv | Expert Systems with Applications |
| dc.relation.none.fl_str_mv | College of Engineering and Applied Sciences |
| dc.title.none.fl_str_mv | Model checking agent-based communities against uncertain group commitments and knowledge |
| dc.type.none.fl_str_mv | Journal Article Peer-Reviewed info:eu-repo/semantics/publishedVersion |
| description | In recent years, the use of Multi-Agent Systems (MASs) to solve complex problems has grown rapidly. Social communicative commitments have been widely employed in such systems as a means of communication allowing heterogeneous agents to cooperate. However, to prevent undesirable outcomes, communicative commitments and their interactions with agents’ knowledge need to be verified. This paper aims at verifying MASs where agents have knowledge and communicate through manipulating uncertain social commitments, especially when the scope of commitments moves beyond the common agent-to-agent scheme. We introduce a model checking method for verifying those systems and capitalize on the interaction between not only individual but also group communicative commitments and knowledge in the presence of uncertainty. System’s properties are expressed using the Probabilistic Computation Tree Logic of Knowledge and Commitment ( PCTLkc+ ). In the proposed approach, model checking PCTLkc+ is reduced to model checking the probabilistic branching-time logic PCTL. This is achieved by transforming PCTLkc+ model to a Markov Decision Process (MDP), and reducing PCTLkc+ formulae into PCTL formulae compatible with PRISM, a reference model checking tool for probabilistic temporal systems. Thereafter, we provide the soundness and completeness proofs of the reduction technique, and compute its time complexity. The effectiveness of the proposed approach is evaluated by implementing it on top of PRISM using two concrete applications, namely Online Shopping System from the business domain, and Insurance Claim Processing from the industrial domain. The obtained results of the two case studies underscore the scientific value of our proposed framework and confirm that verifying commitment-based probabilistic epistemic MASs has become attainable by utilizing this approach. The presented work outperforms existing proposals because it considers the problem of modeling and verifying MASs where group social commitments are interacting with participating agents’ knowledge in the presence of uncertainty, which has not been addressed yet in the literature. |
| id | AUKR_04ca31d7d3cc49d81406f489ba8d984f |
| identifier_str_mv | Sultan, K., Bentahar, J., Yahyaoui, H., & Mizouni,R. (2021). Model checking agent-based communities against uncertain groupcommitments and knowledge. Expert Systems with Applications, 177.https://doi.org/10.1016/j.eswa.2021.114792 |
| network_acronym_str | AUKR |
| network_name_str | AU Kuwait Rep |
| oai_identifier_str | oai:dspace.auk.edu.kw:11675/8262 |
| publishDate | 2021 |
| publisher.none.fl_str_mv | Expert Systems with Applications |
| repository.mail.fl_str_mv | |
| repository.name.fl_str_mv | |
| repository_id_str | |
| spelling | Model checking agent-based communities against uncertain group commitments and knowledgeSultan, KhalidBentahar, JamalYahyaoui, HamdiMizouni, RabebIn recent years, the use of Multi-Agent Systems (MASs) to solve complex problems has grown rapidly. Social communicative commitments have been widely employed in such systems as a means of communication allowing heterogeneous agents to cooperate. However, to prevent undesirable outcomes, communicative commitments and their interactions with agents’ knowledge need to be verified. This paper aims at verifying MASs where agents have knowledge and communicate through manipulating uncertain social commitments, especially when the scope of commitments moves beyond the common agent-to-agent scheme. We introduce a model checking method for verifying those systems and capitalize on the interaction between not only individual but also group communicative commitments and knowledge in the presence of uncertainty. System’s properties are expressed using the Probabilistic Computation Tree Logic of Knowledge and Commitment ( PCTLkc+ ). In the proposed approach, model checking PCTLkc+ is reduced to model checking the probabilistic branching-time logic PCTL. This is achieved by transforming PCTLkc+ model to a Markov Decision Process (MDP), and reducing PCTLkc+ formulae into PCTL formulae compatible with PRISM, a reference model checking tool for probabilistic temporal systems. Thereafter, we provide the soundness and completeness proofs of the reduction technique, and compute its time complexity. The effectiveness of the proposed approach is evaluated by implementing it on top of PRISM using two concrete applications, namely Online Shopping System from the business domain, and Insurance Claim Processing from the industrial domain. The obtained results of the two case studies underscore the scientific value of our proposed framework and confirm that verifying commitment-based probabilistic epistemic MASs has become attainable by utilizing this approach. The presented work outperforms existing proposals because it considers the problem of modeling and verifying MASs where group social commitments are interacting with participating agents’ knowledge in the presence of uncertainty, which has not been addressed yet in the literature.Expert Systems with Applications2021-12-22T08:28:06Z2021-12-22T08:28:06Z2021-03-10Journal ArticlePeer-Reviewedinfo:eu-repo/semantics/publishedVersionSultan, K., Bentahar, J., Yahyaoui, H., & Mizouni,R. (2021). Model checking agent-based communities against uncertain groupcommitments and knowledge. Expert Systems with Applications, 177.https://doi.org/10.1016/j.eswa.2021.114792https://dspace.auk.edu.kw/handle/11675/8262https://www.sciencedirect.com/science/article/abs/pii/S0957417421002335College of Engineering and Applied Sciencesoai:dspace.auk.edu.kw:11675/82622022-01-13T09:22:07Z |
| spellingShingle | Model checking agent-based communities against uncertain group commitments and knowledge Sultan, Khalid |
| status_str | publishedVersion |
| title | Model checking agent-based communities against uncertain group commitments and knowledge |
| title_full | Model checking agent-based communities against uncertain group commitments and knowledge |
| title_fullStr | Model checking agent-based communities against uncertain group commitments and knowledge |
| title_full_unstemmed | Model checking agent-based communities against uncertain group commitments and knowledge |
| title_short | Model checking agent-based communities against uncertain group commitments and knowledge |
| title_sort | Model checking agent-based communities against uncertain group commitments and knowledge |
| url | https://dspace.auk.edu.kw/handle/11675/8262 https://www.sciencedirect.com/science/article/abs/pii/S0957417421002335 |