Login | Register

Specification and automatic verification of trust-based multi-agent systems


Specification and automatic verification of trust-based multi-agent systems

Drawel, Nagat, Qu, Hongyang, Bentahar, Jamal and Shakshuki, Elhadi (2018) Specification and automatic verification of trust-based multi-agent systems. Future Generation Computer Systems . ISSN 0167739X (In Press)

Text (application/pdf)
bentahar-fgcs-2018.pdf - Accepted Version
Available under License Spectrum Terms of Access.

Official URL: http://dx.doi.org/10.1016/j.future.2018.01.040


We present a new logic-based framework for modeling and automatically verifying trust in Multi-Agent Systems (MASs). We start by refining TCTL, a temporal logic of trust that extends the Computation Tree Logic (CTL) to enable reasoning about trust with preconditions. A new vector-based version of interpreted systems is defined to capture the trust relationship between the interacting parties. We introduce a set of reasoning postulates along with formal proofs to support our logic. Moreover, we present new symbolic model checking algorithms to formally and automatically verify the system under consideration against some desirable properties expressed using the proposed logic. We fully implemented our proposed algorithms as a model checker tool called MCMAS-T on top of the MCMAS model checker for MASs along with its new input language VISPL (Vector-extended ISPL). We evaluated the tool and reported experimental results using a real-life scenario in the healthcare field.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Concordia Institute for Information Systems Engineering
Item Type:Article
Authors:Drawel, Nagat and Qu, Hongyang and Bentahar, Jamal and Shakshuki, Elhadi
Journal or Publication:Future Generation Computer Systems
Date:31 January 2018
  • Natural Sciences and Engineering Research Council of Canada (NSERC)
Digital Object Identifier (DOI):10.1016/j.future.2018.01.040
Keywords:Trust; Multi-agent systems; Temporal logic; Model checking; Reasoning postulates; MCMAS-T; VISPL
ID Code:983457
Deposited On:31 Jan 2018 20:25
Last Modified:31 Jan 2019 01:00


M. Wooldridge, N.R. Jennings Intelligent agents: Theory and practice Knowl. Eng. Rev., 10 (02) (1995), pp. 115–152

P.K. Biswas Towards an agent-oriented approach to conceptualization Appl. Soft Comput., 8 (1) (2008), pp. 127–139

M.J. Wooldridge Agent Technology: Foundations, Applications, and Markets Springer Science & Business Media (1998)

F. Wang, M. Yang, R. Yang Simulation of multi-agent based cybernetic transportation system Simul. Model. Pract. Theory, 16 (10) (2008), pp. 1606–1614

H.-K. Kim Convergence agent model for developing u-healthcare systems Future Gener. Comput. Syst., 35 (2014), pp. 39–48

J. Bentahar, Z. Maamar, D. Benslimane, P. Thiran, Using argumentative agents to manage communities of web services, in: 21st International Conference on Advanced Information Networking and Applications, AINA 2007, Workshops Proceedings, Vol. 2, May 21–23, 2007, Niagara Falls, Canada, 2007, pp. 588–593.

J. Bentahar, M. El-Menshawy, H. Qu, R. Dssouli Communicative commitments: Model checking and complexity analysis Knowl.-Based Syst., 35 (2012), pp. 21–34

M.P. Singh Trust as dependence: a logical approach, The 10th International Conference on Autonomous Agents and Multiagent Systems, Vol. 2, International Foundation for Autonomous Agents and Multiagent Systems (2011), pp. 863–870

E.A. Emerson Temporal and modal logic, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), Vol. 995, (1990), p. 5

N. Drawel, J. Bentahar, E. Shakshuki Reasoning about trust and time in a system of agents, 8th International Conference on Ambient Systems, Networks and Technologies, Procedia Computer Science, Vol. 109, Elsevier (2017), pp. 632–639

L. Zhang, S. Jiang, J. Zhang, W.K. Ng Robustness of trust models and combinations for handling unfair ratings, IFIP International Conference on Trust Management, Springer (2012), pp. 36–51

D. Jelenc, R. Hermoso, J. Sabater-Mir, D. Trček Decision making matters: A better way to evaluate trust models Knowl.-Based Syst., 52 (2013), pp. 147–164

S. Singh, J. Sidhu Compliance-based multi-dimensional trust evaluation system for determining trustworthiness of cloud service providers Future Gener. Comput. Syst., 67 (2017), pp. 109–132

A.J. Bidgoly, B.T. Ladani, Trust modeling and verification using colored petri nets, in: 8th International ISC Conference on Information Security and Cryptology, ISCISC, 2011, pp. 1–8.

A.J. Bidgoly, B.T. Ladani, Quantitative verification of beta reputation system using PRISM probabilistic model checker, in: 10th International ISC Conference on Information Security and Cryptology, ISCISC, 2013, pp. 1–6.

A.J. Bidgoly, B.T. Ladani Modeling and quantitative verification of trust systems against malicious attackers Comput. J., 59 (7) (2016), pp. 1005–1027

A.J. Bidgoly, B.T. Ladani Benchmarking reputation systems: A quantitative verification approach Comput. Hum. Behav., 57 (2016), pp. 274–291

A. Aldini, A formal framework for modeling trust and reputation in collective adaptive systems, in: Proceedings of the Workshop on Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems, FORECAST@STAF, Vienna, Austria, 2016, pp. 19–30.

T. Muller, Y. Liu, S. Mauw, J. Zhang On robustness of trust systems, IFIP International Conference on Trust Management, Springer (2014), pp. 44–60

E.M. Clarke, O. Grumberg, D. Peled Model Checking MIT press (1999)

E.M. Clarke, E.A. Emerson, J. Sifakis Model checking: Algorithmic verification and debugging Commun. ACM, 52 (11) (2009), pp. 74–84

A. Pnueli The temporal logic of programs, Foundations of Computer Science, 1977. 18th Annual Symposium on, IEEE (1977), pp. 46–57

R. Fagin, J.Y. Halpern, Y. Moses, M.Y. Vardi Reasoning About Knowledge MIT Press (1995)

B. Lahno Olli lagerspetz: Trust. The tacit demand Ethical Theory Moral Pract., 2 (4) (1999), pp. 433–435

J.D. Lee, K.A. See Trust in automation: Designing for appropriate reliance Hum. Factors, 46 (1) (2004), pp. 50–80

D. Gambetta, et al. Can we trust trust Trust: Mak. Break. Cooperat. Relat., 13 (2000), pp. 213–237

R. Vijayan, N. Jeyanthi A survey of trust management in mobile ad hoc networks Int. J. Appl. Eng. Res., 11 (4) (2016), pp. 2833–2838

S. Adalı Modeling Trust Context in Networks springer (2013)

C. Castelfranchi, R. Falcone, Principles of trust for MAS: Cognitive anatomy, social importance, and quantification, in: Proceedings of the International Conference on Multi Agent Systems, 1998, pp. 72–79.

A. Herzig, E. Lorini, J.F. Hübner, L. Vercouter A logic of trust and reputation Log. J. IGPL, 18 (1) (2010), pp. 214–244

O.A. Wahab, J. Bentahar, H. Otrok, A. Mourad Towards trustworthy multi-cloud services communities: A trust-based hedonic coalitional game IEEE Trans. Serv. Comput. (2017) in press

Z. Chen, Y. Jiang, Y. Zhao, et al. A collaborative filtering recommendation algorithm based on user interest change and trust evaluation JDCTA, 4 (9) (2010), pp. 106–113

E. Oliveira, H.L. Cardoso, M.J. Urbano, A.P. Rocha Normative monitoring of agents to build trust in an environment for b2b, IFIP International Conference on Artificial Intelligence Applications and Innovations, Springer (2014), pp. 172–181

S.P. Marsh Formalising Trust as a Computational Concept (Ph.D. thesis) University of Stirling (1994)

I. Pinyol, J. Sabater-Mir Computational trust and reputation models for open multi-agent systems: a review Artif. Intell. Rev., 40 (1) (2013), pp. 1–25

C. Liu, M.A. Ozols, M. Orgun A temporalised belief logic for specifying the dynamics of trust for multi-agent systems, Advances in Computer Science-ASIAN 2004. Higher-Level Decision Making, Springer (2004), pp. 142–156

R. Demolombe, E. Lorini, A logical account of trust in information sources, in: Proceedings of the 11th International Workshop on Trust in Agent Societies, 2008.

R. Demolombe To trust information sources: a proposal for a modal logical framework, Trust and Deception in Virtual Societies, Springer (2001), pp. 111–124

D. Harel, D. Kozen, J. Tiuryn Dynamic Logic MIT press (2000)

P.R. Cohen, H.J. Levesque Intention is choice with commitment Artificial Intelligence, 42 (2–3) (1990), pp. 213–261

E. Lorini, R. Demolombe Trust and norms in the context of computer security: A logical formalization, International Conference on Deontic Logic in Computer Science, Springer (2008), pp. 50–64

L. Amgoud, R. Demolombe An argumentation-based approach for reasoning about trust in information sources Argum. Comput., 5 (2–3) (2014), pp. 191–215

C.-J. Liau Belief, information acquisition, and trust in multi-agent systemsa modal logic formulation Artificial Intelligence, 149 (1) (2003), pp. 31–60

R. Montague Universal grammar Theoria, 36 (3) (1970), pp. 373–398

M.P. Singh Semantical considerations on dialectical and practical commitments D. Fox, C.P. Gomes (Eds.), Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13–17, 2008, AAAI Press (2008), pp. 176–181

M. Burrows, M. Abadi, R.M. Needham A logic of authentication ACM Trans. Comput. Syst., 8 (1) (1990), pp. 18–36

H. Alotaibi, H. Zedan, Runtime verification of safety properties in multi-agents systems, in: 10th International Conference on Intelligent Systems Design and Applications, ISDA, 2010, pp. 356–362.

N.A. Bakar, A. Selamat Runtime verification of multi-agent systems interaction quality, Asian Conference on Intelligent Information and Database Systems, Springer (2013), pp. 435–444

A. Bauer, M. Leucker, C. Schallhart Runtime verification for LTL and TLTL ACM Trans. Softw. Eng. Methodol., 20 (4) (2011), p. 14

A. Lomuscio, C. Pecheur, F. Raimondi Automatic verification of knowledge and time with NuSMV, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, IJCAI/AAAI Press (2007), pp. 1384–1389

M. Webster, L. Dennis, M. Fisher Model-Checking Auctions, Coalitions and Trust, Technical Report University of Liverpoo (2009)

M. Leucker, C. Schallhart A brief account of runtime verification J. Log. Algebr. Program., 78 (5) (2009), pp. 293–303

R. De Nicola, F. Vaandrager Action versus state based logics for transition systems , Semantics of Systems of Concurrent Processes, Springer (1990), pp. 407–419

J. El-Qurna, H. Yahyaoui, M. Almulla A new framework for the verification of service trust behaviors Knowl.-Based Syst., 121 (2017), pp. 7–22

R.E. Bryant Graph-based algorithms for boolean function manipulation IEEE Trans. Comput., 100 (8) (1986), pp. 677–691

F. Al-Saqqar, J. Bentahar, K. Sultan, W. Wan, E.K. Asl Model checking temporal knowledge and commitments in multi-agent systems using reduction Simul. Model. Pract. Theory, 51 (2015), pp. 45–68

M. El-Menshawy, J. Bentahar, R. Dssouli Symbolic model checking commitment protocols using reduction in: A. Omicini, S. Sardiña, W.W. Vasconcelos (Eds.), Declarative Agent Languages and Technologies VIII - 8th International Workshop, DALT 2010, Toronto, Canada, May 10, 2010, Revised, Selected and Invited Papers, Lecture Notes in Computer Science, vol. 6619, Springer (2010), pp. 185–203

M. El-Menshawy, J. Bentahar, W. El Kholy, R. Dssouli Reducing model checking commitments for agent communication to model checking ARCTL and GCTL* Auton. Agents Multi-Agent Syst., 27 (3) (2013), pp. 375–418

A. Lomuscio, F. Raimondi MCMAS: A model checker for multi-agent systems , International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer (2006), pp. 450–454

A.S. Bataineh, J. Bentahar, M. El-Menshawy, R. Dssouli Specifying and verifying contract-driven service compositions using commitments and model checking Expert Syst. Appl., 74 (2017), pp. 151–184

W. El Kholy, J. Bentahar, M. El-Menshawy, H. Qu, R. Dssouli Conditional commitments: Reasoning and model checking ACM Trans. Softw. Eng. Methodol., 24 (2) (2014), p. 9

W. El Kholy, J. Bentahar, M. El-Menshawy, H. Qu, R. Dssouli SMC4AC: A new symbolic model checker for intelligent agent communication Fund. Inform., 152 (3) (2017), pp. 223–271
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Back to top Back to top