Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Autonomous Agents and Multi-Agent Systems
Published in: Autonomous Agents and Multi-Agent Systems 1/2022

01-04-2022

Formal verification of group and propagated trust in multi-agent systems

Authors: Nagat Drawel, Jamal Bentahar, Amine Laarej, Gaith Rjoub

Published in: Autonomous Agents and Multi-Agent Systems | Issue 1/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

While modeling trust in multi-agent systems provides a fundamental basis for promoting safe interactions and imitating agents reasoning mechanisms, exploiting model checking techniques to govern the trust relationships between group of agents and other agents is yet to be investigated. In this paper, we present a formal framework that allows individual and group of agents to reason about their trust toward other agents. In particular, we propose a branching time temporal logic BT which includes operators that express concepts such as everyone trust, distributed trust and propagated trust. We develop efficient and scalable reduction algorithms by which model checking BT logic is feasible at design time. We analyze the satisfiability and model checking problems of this logic. Moreover, we present in this manuscript BTT, a new BT Transformation tool, which is developed to automate the verification process. Finally, we demonstrate extensive experimental results, which confirm the theoretical findings and make our approach practical.
previous article The complexity of election problems with group-separable preferences
next article Representing and reasoning about auctions

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
Footnotes
Literature
1.
Al-Saqqar, F., Bentahar, J., & Sultan, K. (2016). On the soundness, completeness and applicability of the logic of knowledge and communicative commitments in multi-agent systems. Expert Systems with Applications, 43, 223–236.CrossRef
2.
Al-Saqqar, F., Bentahar, J., Sultan, K., Wan, W., & Asl, E. K. (2015). Model checking temporal knowledge and commitments in multi-agent systems using reduction. Simulation Modelling Practice and Theory, 51, 45–68.CrossRef
3.
Bataineh, A. S., Bentahar, J., El Menshawy, M., & Dssouli, R. (2017). Specifying and verifying contract-driven service compositions using commitments and model checking. Expert Systems with Applications, 74, 151–184.CrossRef
4.
Bentahar, J., Drawel, N., & Sadiki, A. (2022). Quantitative group trust: A two-stage verification approach. In The International Conference on Autonomous Agents and Multiagent Systems, (pp. 20–20).
5.
Bentahar, J., El-Menshawy, M., Qu, H., & Dssouli, R. (2012). Communicative commitments: Model checking and complexity analysis. Knowledge-Based Systems, 35, 21–34.CrossRef
6.
Benthem, J. (1984). Correspondence theory. In D. Gabbay & F. Guenthner (Eds.), Handbook of Philosophical Logic (Vol. 2, pp. 167–247). Springer.CrossRef
7.
Castelfranchi, C., & Falcone, R. (1998). Principles of trust for MAS: cognitive anatomy, social importance, and quantification. In The Third International Conference on Multiagent Systems, ICMAS, (pp. 72–79).
8.
Chakraborty, P. S., & Karform, S. (2012). Designing trust propagation algorithms based on simple multiplicative strategy for social networks. Procedia Technology, 6, 534–539.CrossRef
9.
Christianson, B., & Harbison, W.S. (1996). Why isn’t trust transitive? In International Workshop on Security Protocols, (pp. 171–176). Springer.
10.
Clarke, E. M., Emerson, A., & Sifakis, J. (2009). Model checking: Algorithmic verification and debugging. Communications of the ACM, 52(11), 74–84.CrossRef
11.
Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model Checking. MIT Press.MATH
12.
Cohen, P. R., & Levesque, H. J. (1990). Intention is choice with commitment. Artificial Intelligence, 42(2–3), 213–261.MathSciNetCrossRef
13.
Desai, N., Mallya, A. U., Chopra, A. K., & Singh, M. P. (2005). Interaction protocols as design abstractions for business processes. IEEE Transactions on Software Engineering, 31(12), 1015–1027.CrossRef
14.
Drawel, N., Bentahar, J., El-Menshawy, M., & Laarej, A. (2018). Verifying temporal trust logic using CTL model checking. In The 20th International Trust Workshop co-located with AAMAS/IJCAI/ECAI/ICML, (pp. 62–74).
15.
Drawel, N., Bentahar, J., & Shakshuki, E. (2017). Reasoning about trust and time in a system of agents. In The 8th International Conference on Ambient Systems, Networks and Technologies (ANT),Procedia Computer Science, (Vol. 109, pp. 632–639).
16.
Drawel, N., Qu, H., Bentahar, J., & Shakshuki, E. M. (2020). Specification and automatic verification of trust-based multi-agent systems. Future Generation Computer Systems, 107, 1047–1060.CrossRef
17.
El Kholy, W., Bentahar, J., El Menshawy, M., Qu, H., & Dssouli, R. (2014). Modeling and verifying choreographed multi-agent-based web service compositions regulated by commitment protocols. Expert Systems with Applications, 41(16), 7478–7494.CrossRef
18.
El Kholy, W., Bentahar, J., El Menshawy, M., Qu, H., & Dssouli, R. (2017). SMC4AC: A new symbolic model checker for intelligent agent communication. Fundamenta Informaticae, 152(3), 223–271.MathSciNetCrossRef
19.
El-Menshawy, M., Bentahar, J., & Dssouli, R. (2010). Symbolic model checking commitment protocols using reduction. In The 8th International Workshop on Declarative Agent Languages and Technologies VIII, DALT. Lecture Notes in Computer Science, (Vol. 6619, pp. 185–203).
20.
El Menshawy, M., Bentahar, J., El Kholy, W., & Laarej, A. (2018). Model checking real-time conditional commitment logic using transformation. Journal of Systems and Software, 138, 189–205.CrossRef
21.
Emerson, A. (1990). Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, (pp. 995–1072). MIT Press.
22.
Emerson, A., & Halpern, J. Y. (1985). Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1), 1–24.MathSciNetCrossRef
23.
Fagin, R., Halpern, J. Y., Vardi, M. Y., & Moses, Y. (1995). Reasoning about knowledge. MIT Press.MATH
24.
25.
Herzig, A., Lorini, E., & Moisan, F. (2012). A simple logic of trust based on propositional assignments. In F. Paglieri, L. Tummolini, & R. Falcone (Eds.), The Goals of Cognition. Essays in Honour of Cristiano Castelfranchi, Tributes (pp. 407–419). College Publications.
26.
Huang, X., Kwiatkowska, M., & Olejnik, M. (2019). Reasoning about cognitive trust in stochastic multiagent systems. ACM Transactions on Computational Logic, 20(4), 21:1-21:64.MathSciNetCrossRef
27.
Jamali, M., & Ester, M. (2010). A matrix factorization technique with trust propagation for recommendation in social networks. In The ACM Conference on Recommender Systems, RecSys, (pp. 135–142). ACM.
28.
Kafalı, O., Ajmeri, N., & Singh, M.P. (2017). Kont: Computing tradeoffs in normative multiagent systems. In Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, (pp. 3006–3012). AAAI’17.
29.
Kholy, W. E., Bentahar, J., Menshawy, M. E., Qu, H., & Dssouli, R. (2014). Conditional commitments: Reasoning and model checking. ACM Transactions on Software Engineering and Methodology (TOSEM), 24(2), 1–49.CrossRef
30.
Kong, J., & Lomuscio, A. (2017). Model checking multi-agent systems against LDLK specifications. In IJCAI, pp. 1138–1144.
31.
Kouvaros, P., Lomuscio, A., Pirovano, E., & Punchihewa, H. (2019). Formal verification of open multi-agent systems. In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, (pp. 179–187).
32.
Kupferman, O., Vardi, M. Y., & Wolper, P. (2000). An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2), 312–360.MathSciNetCrossRef
33.
Liu, F., & Lorini, E. (2017). Reasoning about belief, evidence and trust in a multi-agent setting. In International Conference on Principles and Practice of Multi-agent Systems, (pp. 71–89)
34.
Lomuscio, A., & Michaliszyn, J. (2016). Model checking multi-agent systems against epistemic HS specifications with regular expressions. In Fifteenth International Conference on the Principles of Knowledge Representation and Reasoning
35.
Lomuscio, A., & Michaliszyn, J. (2016). Verification of multi-agent systems via predicate abstraction against ATLK specifications. In AAMAS
36.
Lomuscio, A., Pecheur, C., & Raimondi, F. (2007). Automatic verification of knowledge and time with NuSMV. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, (pp. 1384–1389). IJCAI/AAAI Press.
37.
Marsh, S. (1994). Formalising trust as a computational concept. Ph.D. thesis, University of Stirling
38.
Nayak, A., Chhogyal, K., Ghose, A., & Hoa, D. (2019). A value based trust assessment model for multi-agent systems. In 28th International Joint Conference on Artificial Intelligence, IJCAI.
39.
Parr, T. (2013). The Definitive ANTLR 4 Reference (1st ed.). The Pragmatic Programmers: The Pragmatic Bookshelf.
40.
Parr, T., & Fisher, K. (2011). LL(*): The foundation of the ANTLR parser generator. In: M.W. Hall, D.A. Padua (eds.) In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, June 4–8, 2011, (pp. 425–436). ACM
41.
Parr, T., Harwell, S., & Fisher, K. (2014). Adaptive LL(*) parsing: The power of dynamic analysis. In: A.P. Black, T.D. Millstein (eds.) In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland October 20–24, 2014, (pp. 579–598). ACM
42.
Penczek, W., & Lomuscio, A. (2003). Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2), 167–185.MathSciNetMATH
43.
Pnueli, A. (1977). The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, (pp. 46–57)
44.
Primiero, G. (2016). A calculus for distrust and mistrust. In: Trust Management X-10th IFIP WG 11.11 International Conference, IFIPTM. IFIP Advances in Information and Communication Technology, (Vol. 473, pp. 183–190).
45.
46.
Primiero, G., & Raimondi, F. (2014). A typed natural deduction calculus to reason about secure trust. In Twelfth Annual International Conference on Privacy, Security and Trust, (pp. 379–382). IEEE Computer Society.
47.
Sardana, N., Cohen, R., Zhang, J., & Chen, S. (2018). A Bayesian multiagent trust model for social networks. IEEE Transactions on Computational Social Systems, 5(4), 995–1008.CrossRef
48.
Schnoebelen, P. (2002). The complexity of temporal logic model checking. In: The 4th conference on Advances in Modal Logic, (pp. 393–436).
49.
Singh, M. P. (2008). Semantical considerations on dialectical and practical commitments. In: AAAI (Vol. 8, pp. 176–181).
50.
Singh, M.P. (2008). Semantical considerations on dialectical and practical commitments. In: D. Fox, C.P. Gomes (eds.) In Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI, Chicago, July 13–17, (pp. 176–181). AAAI Press.
51.
Singh, M.P. (2011). Trust as dependence: A logical approach. In: The 10th International Conference on Autonomous Agents and Multiagent Systems, (pp. 863–870)
52.
Sultan, K., Bentahar, J., Wan, W., & Al-Saqqar, F. (2014). Modeling and verifying probabilistic multi-agent systems using knowledge and social commitments. Expert Systems with Applications, 41(14), 6291–6304.CrossRef
53.
Telang, P. R., Kalia, A. K., & Singh, M. P. (2015). Modeling healthcare processes using commitments: An empirical evaluation. PLoS ONE, 10(11), e0141202.CrossRef
54.
Troquard, N. (2014). Reasoning about coalitional agency and ability in the logics of “bringing-it-about’’. Autonomous Agents and Multi-agent Systems, 28(3), 381–407.CrossRef
55.
Viganò, F., & Colombetti, M. (2009). Verifying organizations regulated by institutions. In V. Dignum (ed.) Handbook of Research on Multi-Agent Systems-Semantics and Dynamics of Organizational Models, (pp. 367–396). IGI Global.
56.
Wahab, O. A., Bentahar, J., Otrok, H., & Mourad, A. (2018). Towards trustworthy multi-cloud services communities: A trust-based hedonic coalitional game. IEEE Transactions on Services Computing, 11(1), 184–201.CrossRef
Metadata
Title
Formal verification of group and propagated trust in multi-agent systems
Authors
Nagat Drawel
Jamal Bentahar
Amine Laarej
Gaith Rjoub
Publication date
01-04-2022
Publisher
Springer US
Published in
Autonomous Agents and Multi-Agent Systems / Issue 1/2022
Print ISSN: 1387-2532
Electronic ISSN: 1573-7454
DOI
https://doi.org/10.1007/s10458-021-09542-6

Other articles of this Issue 1/2022

Autonomous Agents and Multi-Agent Systems 1/2022 Go to the issue

OriginalPaper

Candidate selections with proportional fairness constraints

OriginalPaper

An explainable assistant for multiuser privacy

OriginalPaper

Redividing the cake

OriginalPaper

Exploring the influence of a user-specific explainable virtual advisor on health behaviour change intentions

OriginalPaper

Fair allocation of conflicting items

OriginalPaper

Combining quantitative and qualitative reasoning in concurrent multi-player games

Premium Partner

    Image Credits