Arrow Research search

Author name cluster

Jamal Bentahar

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

18 papers
1 author row

Possible papers

18

JAAMAS Journal 2022 Journal Article

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

  • Nagat Drawel
  • Jamal Bentahar
  • Gaith Rjoub

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.

Details DOI

AAMAS Conference 2022 Conference Paper

Quantitative Group Trust: A Two-Stage Verification Approach

  • Jamal Bentahar
  • Nagat Drawel
  • Abdeladim Sadiki

This paper is about modeling and verifying quantitative group trust. We present a formal analysis of this concept that allows us to express and reason about trust in multi-agent systems in a quantitative setting. We introduce GTL, the graded branching temporal logic that includes operators for quantitative aspects of trust within a group. A two-stage verification procedure of the logic is presented. The first stage is a transformation procedure, and the second stage is an indirect procedure that uses an existing model checking algorithm. Theoretical results about the soundness, completeness and complexity of the procedure are presented.

PDF

IJCAI Conference 2020 Conference Paper

Formalizing Group and Propagated Trust in Multi-Agent Systems

  • Nagat Drawel
  • Jamal Bentahar
  • Amine Laarej
  • Gaith Rjoub

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 analyze the satisfiability and model checking problems of this logic using a reduction technique.

PDF Details DOI

KER Journal 2015 Journal Article

Computational logics and verification techniques of multi-agent commitments: survey

  • Mohamed El Menshawy
  • Jamal Bentahar
  • Warda El Kholy
  • Pinar Yolum
  • Rachida Dssouli

Abstract Agent communication languages (ACLs) are fundamental mechanisms that enable agents in multi-agent systems to talk, communicate with each other in order to satisfy their individual and social goals in a cooperative and competitive manner. Social approaches are advocated to overcome the shortcomings of ACL semantics delineated by using mental approaches in the figure of agents’ mental notions. Over the last two decades, social commitments have been the subject of considerable research in some of those social approaches as they provide a powerful representation for modeling and reasoning upon multi-agent interactions in the form of mutual contractual obligations. They particularly provide a declarative, flexible, verifiable, and social semantics for ACL messages while respecting agents’ autonomy, heterogeneity, and openness. In this manuscript, we go through prominent and predominate proposals in the literature to explore the state of the art on how temporal logics can be devoted to define a formal semantics for ACL messages in terms of social commitments and associated actions. We explain each proposal and point out if and how it meets seven crucial criteria, four of them introduced by Munindar P. Singh to have a well-defined semantics for ACL messages. Far from deciding the best proposal, our aim is to present the advantages (strengths) and limitations of those proposals to designers and developers using a concrete running example and to compare between them, so that they can make the best choice with regard to their needs. We explore and evaluate current specification languages and different verification techniques that have been discussed within those proposals to, respectively, specify and verify commitment-based protocols. We also investigate logical languages of actions advocated to specify, model, and execute commitment-based protocols in other contributed proposals. Finally, we suggest some solutions that can contribute to address the identified limitations.

Details DOI

AAMAS Conference 2013 Conference Paper

On the Analysis of Joining Communities of Agent-Based Web Services

  • Jamal Bentahar
  • Babak Khosravifar
  • Kathleen Clacens
  • Christophe Goffart
  • Philippe Thiran

Communities of agent-based web services are virtual groups gathering functionally equivalent web services having different nonfunctional attributes. Building reputable communities hosting reliable web services is still an open challenge. In this paper, we propose a mechanism that web services through associated agents can use to join existing communities. Key components of this mechanism are agents providing information about potential members of communities. Analyzing incentives for these agents to reveal accurate information is the main contribution of this paper.

PDF

AAMAS Conference 2013 Conference Paper

Representing and Reasoning about Communicative Conditional Commitments

  • Warda El Kholy
  • Mohamed El Menshawy
  • Jamal Bentahar
  • Hongyang Qu
  • Rachida Dssouli

Social commitments provide a powerful representation for modeling multi-agent interactions without relinquishing part of agents autonomy and flexibility. However, distinguishing between different but related types of conditional commitments, a natural frame of social commitments, is not considered yet. In this paper, we define a new logical language, CTLcc, which extends CTL with modalities to represent conditional commitments and their fulfillments using the formalism of interpreted systems. Such a language excludes the paradox that plagues the semantics of fulfilling commitments in the literature. We present a set of rules to reason about conditional commitments and their fulfillments.

PDF

TIST Journal 2013 Journal Article

Research directions in agent communication

  • Amit K. Chopra
  • Alexander Artikis
  • Jamal Bentahar
  • Marco Colombetti
  • Frank Dignum
  • Nicoletta Fornara
  • Andrew J. I. Jones
  • Munindar P. Singh

Increasingly, software engineering involves open systems consisting of autonomous and heterogeneous participants or agents who carry out loosely coupled interactions. Accordingly, understanding and specifying communications among agents is a key concern. A focus on ways to formalize meaning distinguishes agent communication from traditional distributed computing: meaning provides a basis for flexible interactions and compliance checking. Over the years, a number of approaches have emerged with some essential and some irrelevant distinctions drawn among them. As agent abstractions gain increasing traction in the software engineering of open systems, it is important to resolve the irrelevant and highlight the essential distinctions, so that future research can be focused in the most productive directions. This article is an outcome of extensive discussions among agent communication researchers, aimed at taking stock of the field and at developing, criticizing, and refining their positions on specific approaches and future challenges. This article serves some important purposes, including identifying (1) points of broad consensus; (2) points where substantive differences remain; and (3) interesting directions of future work.

Details DOI

JAAMAS Journal 2012 Journal Article

Reducing model checking commitments for agent communication to model checking ARCTL and GCTL *

  • Mohamed El Menshawy
  • Jamal Bentahar
  • Rachida Dssouli

Abstract Social commitments have been extensively and effectively used to represent and model business contracts among autonomous agents having competing objectives in a variety of areas (e. g. , modeling business processes and commitment-based protocols). However, the formal verification of social commitments and their fulfillment is still an active research topic. This paper presents CTLC + that modifies CTLC, a temporal logic of commitments for agent communication that extends computation tree logic (CTL) logic to allow reasoning about communicating commitments and their fulfillment. The verification technique is based on reducing the problem of model checking CTLC + into the problem of model checking ARCTL (the combination of CTL with action formulae) and the problem of model checking GCTL * (a generalized version of CTL * with action formulae) in order to respectively use the extended NuSMV symbolic model checker and the CWB-NC automata-based model checker as a benchmark. We also prove that the reduction techniques are sound and the complexity of model checking CTLC + for concurrent programs with respect to the size of the components of these programs and the length of the formula is PSPACE-complete. This matches the complexity of model checking CTL for concurrent programs as shown by Kupferman et al. We finally provide two case studies taken from business domain along with their respective implementations and experimental results to illustrate the effectiveness and efficiency of the proposed technique. The first one is about the NetBill protocol and the second one considers the Contract Net protocol.

Details DOI

AAMAS Conference 2011 Conference Paper

On the Verification of Social Commitments and Time

  • Mohamed El-Menshawy
  • Jamal Bentahar
  • Hongyang Qu
  • Rachida Dssouli

Social commitments have been widely studied to represent business contracts among agents with different competing objectives in communicating multi-agent systems. However, their formal verification is still an open issue. This paper proposes a novel model-checking algorithm to address this problem. We define a new temporal logic, CTLC, which extends CTL with modalities for social commitments and their fulfillment and violation. The verification technique is based on symbolic model checking that uses ordered binary decision diagrams to give a compact representation of the system. We also prove that the problem of model checking CTLC is polynomial-time reducible to the problem of model checking CTLK, the combination of CTL with modalities for knowledge. We finally present the full implementation of the proposed algorithm by extending the MCMAS symbolic model checker and report on the experimental results obtained when verifying the NetBill protocol.

PDF

AAMAS Conference 2010 Conference Paper

An Agent Communication Protocol for Resolving Conflicts

  • Jamal Bentahar

This paper proposes an agent communication protocol specified asa set of dialogue rules for resolving conflicts using assumption-based argumentation. Arguments are built from a set of rules andassumptions using backward deduction. Beyond arguments agentscan handle, we propose the notion of partial arguments along withpartial acceptability. This protocol merges inquiry and persuasion stages and by building and reasoning about partial arguments, agents can jointly find arguments supporting a new solution fortheir conflict, which is not known by any of them individually.

PDF

AAAI Conference 2010 Conference Paper

On the Reputation of Agent-Based Web Services

  • Babak Khosravifar
  • Jamal Bentahar
  • Ahmad Moazin
  • Philippe Thiran

Maintaining a sound reputation mechanism requires a robust control and investigation. In this paper, we propose a game-theoretic analysis of a reputation mechanism that objectively maintains accurate reputation evaluation of selfish agent-based web services. In this framework, web services are ranked using their reputation as a result of provided feedback reflecting consumers’ satisfaction about the offered services. However, selfish web services may alter their public reputation level by managing to get fake feedback. In this paper, game-theoretic analysis investigates the payoffs of different situations and elaborates on the facts that discourage web services to act maliciously.

PDF Details

AAMAS Conference 2010 Conference Paper

Symbolic Model Checking for Agent Interactions

  • Mohamed El-Menshawy
  • Wei Wan
  • Jamal Bentahar
  • Rachida Dssouli

In this paper, we address the issue of the specification andverification of commitment protocols having a social semantics. We begin with developing a new language to formallyspecify these protocols and desirable properties by enhancing $CTL^*$ logic with modalities of commitments and actions on these commitments. We also present a symbolicmodel checking algorithm for commitments and their actions based on OBDDs. Finally, we present an implementation and experimental results of the proposed protocol usingthe NuSMV and MCMAS symbolic model checkers.

PDF

AAMAS Conference 2009 Conference Paper

Maintenance-based Trust for Multi-Agent Systems

  • Babak Khosravifar
  • Maziar Gomrokchi
  • Jamal Bentahar
  • Philippe Thiran

In last years, trust and reputation has been gaining increasing interest in multi-agent systems (MAS). To address this issue, we propose in this paper a maintenance-based trust mechanism for agents operating in multi-agent systems. In the proposed model, a comprehensive trust assessment process is provided to assess the trustworthiness of the participating agents. The main characteristic of this model is the retrospect trust adjustments, which integrate the applicable constraints and modify the involved features with respect to the actual performance of the evaluated agent. Specifically, the retrospect process updates the belief set of the agents in order to adapt them to the social network changes. This paper has two contributions: after describing the architecture of the proposed framework, we provide a theoretical analysis of its assessment and discuss the system implementation, along with simulations comparing it with the broadly known frameworks.

PDF

IS Journal 2007 Journal Article

An Argumentation Framework for Communities of Web Services

  • Jamal Bentahar
  • Zakaria Maamar
  • Djamal Benslimane
  • Philippe Thiran

As the number of Web services continues to increase, so does the opportunities to compose them to build more complex and complete business solutions. To facilitate and speed up Web-services discovery, Web services with similar (or equivalent) functionalities - such as flight booking and travel reservation - can be grouped into communities. Argumentation theory, implemented through a set of software agents that reason about Web services, can improve Web services performance through the notion of communities.

Details DOI
v2026.09.13