Yazar "Bentahar, Jamal" seçeneğine göre listele

Listeleniyor 1 - 5 / 5
  • Küçük Resim Yok
    Öğe
    A comprehensive survey on applications of transformers for deep learning tasks
    (Pergamon-Elsevier Science Ltd, 2024) Islam, Saidul; Elmekki, Hanae; Elsebai, Ahmed; Bentahar, Jamal; Drawel, Nagat; Rjoub, Gaith; Pedrycz, Witold
    Transformers are Deep Neural Networks (DNN) that utilize a self-attention mechanism to capture contextual relationships within sequential data. Unlike traditional neural networks and variants of Recurrent Neural Networks (RNNs), such as Long Short-Term Memory (LSTM), Transformer models excel at managing long dependencies among input sequence elements and facilitate parallel processing. Consequently, Transformer -based models have garnered significant attention from researchers in the field of artificial intelligence. This is due to their tremendous potential and impressive accomplishments, which extend beyond Natural Language Processing (NLP) tasks to encompass various domains, including Computer Vision (CV), audio and speech processing, healthcare, and the Internet of Things (IoT). Although several survey papers have been published, spotlighting the Transformer's contributions in specific fields, architectural disparities, or performance assessments, there remains a notable absence of a comprehensive survey paper that encompasses its major applications across diverse domains. Therefore, this paper addresses this gap by conducting an extensive survey of proposed Transformer models spanning from 2017 to 2022. Our survey encompasses the identification of the top five application domains for Transformer-based models, namely: NLP, CV, multi -modality, audio and speech processing, and signal processing. We analyze the influence of highly impactful Transformer-based models within these domains and subsequently categorize them according to their respective tasks, employing a novel taxonomy. Our primary objective is to illuminate the existing potential and future prospects of Transformers for researchers who are passionate about this area, thereby contributing to a more comprehensive understanding of this groundbreaking technology.
  • Küçük Resim Yok
    Öğe
    Model checking combined trust and commitments in Multi-Agent Systems
    (Pergamon-Elsevier Science Ltd, 2024) Baharloo, Narges; Bentahar, Jamal; Drawel, Nagat; Pedrycz, Witold
    Trust 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.
  • Küçük Resim Yok
    Öğe
    Multi-valued model checking IoT and intelligent systems with commitment protocols in multi-source data environments
    (Elsevier, 2024) Alwhishi, Ghalya; Bentahar, Jamal; Elwhishi, Ahmed; Pedrycz, Witold; Drawel, Nagat
    In today's world of connectivity, various domains use different multi-sensor Internet of Things (IoT) and Intelligent Systems (IS) applications. These applications involve extensive interactions between thousands or millions of components in open environments, which challenges verifying their reliability and efficiency. This paper introduces the first investigation in verifying IoT applications and intelligent systems in multi-source data settings with multi-agent commitment protocols in uncertain or inconsistent environments. Specifically, we present original and efficient solutions for modeling and verifying these systems with conditional and unconditional commitment protocols under uncertain or inconsistent settings. We introduce 4v-CTLc and 4v-CTLcc, multi-valued logics of commitment for reasoning about inconsistency over these systems that expand 3v-CTLc and 3v-CTLcc for reasoning about uncertainty. Moreover, we introduce new reduction algorithms for reducing our multi-valued model checking problems to the two-valued ones. To implement these algorithms, we develop two new automatic verification tools. The first tool translates the multi-valued logics to CTL and automatically interacts with the NuSMV model checker. The second tool translates these logics to the two-valued versions, CTLc and CTLcc, and automatically interacts with the MCMAS+ model checker. We apply our verification approaches to a Smart Home, a Smart Hospital and a Smart Mortgage system with multi-source data as case studies using sets of properties, including safety, liveness and reachability. The experimental results obtained by the proposed multi-valued model checking techniques proved these techniques' high efficiency and applicability to modeling and verifying intelligent and autonomous multi-source data systems.
  • Küçük Resim Yok
    Öğe
    MV-Checker: A software tool for multi-valued model checking intelligent applications with trust and commitment
    (Pergamon-Elsevier Science Ltd, 2024) Alwhishi, Ghalya; Bentahar, Jamal; Elwhishi, Ahmed; Pedrycz, Witold
    Intelligent applications are highly susceptible to uncertainty and inconsistency due to the intense and intricate interactions among their autonomous components (or agents), making their verification theoretically and practically challenging. This paper presents the design and implementation of a new open -source and scalable software tool for modeling and verifying intelligent applications with commitment and trust protocols under both uncertainty and inconsistency settings, using reduction -based multi -valued model checking techniques. The proposed tool is equipped with original and novel algorithms that transform our logics of multi -valued commitment (mv-CTLC) and multi -value trust (mv-TCTL) that we recently introduced to their classical twovalued commitment (CTLC) and trust (TCTL) logic versions as well as to Computational Tree Logic (CTL). Moreover, the tool transforms the mv-CTL to CTL, and it is applicable for the classical model checking by transforming the classical logics of trust and commitment to CTL. To demonstrate the practicality and applicability of the proposed tool in real settings, we present and report experimental results over two blockchain-based applications in the healthcare domain. Finally, we provide discussions and comparisons between the proposed approaches regarding scalability and efficiency. Moreover, we provide packages of more than 11 experiments, including the ones we conduct in this paper and enhanced experiments from previous works. Our findings ensure that the proposed approaches and the software tool that implements them are highly efficient and scalable, giving accurate results under varying conditions.
  • Küçük Resim Yok
    Öğe
    Verifying trust over IoT-ad hoc network-based applications under uncertainty
    (Elsevier, 2024) Baharloo, Narges; Bentahar, Jamal; Alwhishi, Ghalya; Drawel, Nagat; Pedrycz, Witold
    The rapid integration of the Internet of Things (IoT) with ad hoc networks offers significant advantages for revolutionizing smart environments. However, ensuring trust and reliability within these interconnected systems remains a significant challenge. To address this challenge, this paper introduces an innovative three valued (3v) trust model customized specifically for IoT-ad hoc systems. The model employs three-valued logic to evaluate trust in social commitments within ambiguous scenarios, where commitments serve as the foundation of the business logic. Our aim is to enhance the effectiveness and economic feasibility of IoT in smart environments. To advance this initiative, we introduce the 3v-TCTLC, a distinctive modeling language that extends the conventional two-valued logic by introducing a third value to accommodate uncertainty. This novel approach facilitates the assessment of trust in commitments within uncertain IoT-ad hoc environments. Additionally, we improve the functionality of the MACMAS-interactor tool, incorporating new features to support our 3v-TCTLC logic. Through two case studies in the domains of smart health monitoring and smart home systems, we validate our model against specific requirements in uncertain contexts. These case studies highlight the robustness and practicality of our proposed tools and methodologies. Compared to prevalent trust management strategies employed in IoT and ad-hoc networks, our methodology stands out distinctly. While many current solutions propose trust-centered protocols, with some even harnessing advanced technologies, they frequently overlook the crucial element of model checking. Our approach not only incorporates this critical component but also ensures the integrity of the system. Furthermore, even though the field of multi-valued model checking has seen advancements like chi CTL, our research contributes significantly by integrating trust and commitment verification specifically designed for IoT-ad hoc environments. Our empirical assessments in the domains of smart health and home systems confirm that our tool and strategies demonstrate superior performance in terms of time and space usage and better adaptability and scalability in uncertain scenarios, representing a noteworthy advancement over existing techniques and tools.