Search

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 two-valued 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. • Design and implementation of an open-source scalable tool for systems model checking. • System modeling with multi-valued logic capturing uncertainty and inconsistency. • Practical demonstration using blockchain-based applications in healthcare domain. • Extensive experiments showing scalability, efficiency and reliability of the tool. [ABSTRACT FROM AUTHOR]

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. • We introduce a new logical language combining trust and social commitments. • We introduce a new model checking algorithm for the new trust and commitment logic. • We propose reasoning postulates and proofs to reason about trust and commitments. • We implement the new algorithm and report its practical efficiency on a case study. [ABSTRACT FROM AUTHOR]

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-CTL c and 4v-CTL c c , multi-valued logics of commitment for reasoning about inconsistency over these systems that expand 3v-CTL c and 3v-CTL c c 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, CTL c and CTL c c , 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. • New multi-valued logics to reason about inconsistency in multi-source data settings. • Modeling IoT and IS applications using different multi-valued commitment logics. • New reduction-based model checking algorithms for multi-source data applications. • Implementing two new model checking tools: MCMAS-interactor and NuSMV-interactor. [ABSTRACT FROM AUTHOR]

Federated learning is a distributed machine learning approach that enables a large number of edge/end devices to perform on-device training for a single machine learning model, without having to share their own raw data. We consider in this paper a federated learning scenario wherein the local training is carried out on IoT devices and the global aggregation is done at the level of an edge server. One essential challenge in this emerging approach is IoT devices selection (also called scheduling), i.e., how to select the IoT devices to participate in the distributed training process. The existing approaches suggest to base the scheduling decision on the resource characteristics of the devices to guarantee that the selected devices would have enough resources to carry out the training. In this work, we argue that trust should be an integral part of the decision-making process and therefore design a trust establishment mechanism between the edge server and IoT devices. The trust mechanism aims to detect those IoT devices that over-utilize or under-utilize their resources during the local training. Thereafter, we introduce DDQN-Trust, a double deep Q learning-based selection algorithm that takes into account the trust scores and energy levels of the IoT devices to make appropriate scheduling decisions. Finally, we integrate our solution into four federated learning aggregation approaches, namely, FedAvg, FedProx, FedShare and FedSGD. Experiments conducted using a real-world dataset show that our DDQN-Trust solution always achieves better performance compared to two main benchmarks: the DQN and random scheduling algorithms. The results also reveal that FedProx outperforms the competitor aggregation models in terms of accuracy when integrated into our DDQN-Trust solution. [ABSTRACT FROM AUTHOR]

Promoting recommender systems in real-world applications requires deep investigations with emphasis on their next generation. This survey offers a comprehensive and systematic review on recommender system development lifecycles to enlighten researchers and practitioners. The paper conducts statistical research on published recommender systems indexed by Web of Science to get an overview of the state of the art. Based on the reviewed findings, we introduce taxonomies driven by the following five phases: initiation (architecture and data acquisition techniques), design (design types and techniques), development (implementation methods and algorithms), evaluation (metrics and measurement techniques) and application (domains of applications). A layered framework of recommender systems containing market strategy, data, recommender core, interaction, security and evaluation is proposed. Based on the framework, the existing advanced humanized techniques emerged from computational intelligence and some inspiring insights from computational economics and machine learning are provided for researchers to expand the novel aspects of recommender systems. [ABSTRACT FROM AUTHOR]

Smart contracts struggle with the major limitation of operating on data that is solely residing on the blockchain network. The need of recruiting third parties, known as oracles, to assist smart contracts has been recognized with the emergence of blockchain technology. Oracles could be deviant and commit ill-intentioned behaviors, or be selfish and hide their actual available resources to gain optimal profit. Current research proposals employ oracles as trusted entities with no robust assessment mechanism, which entails a risk of turning them into centralized points of failure. The need for an effective method to select the most economical and rewarding oracles that are self-interested and act independently is somehow neglected. Thus, this paper proposes a Bayesian Bandit Learning Oracles Reliability (BLOR) mechanism to identify trustless and cost-efficient oracles. Within BLOR, we learn the behavior of oracles by formulating a Bayesian cost-dependent reputation model and utilize reinforcement learning (knowledge gradient algorithm) to guide the learning process. BLOR enables all the blockchain validators to verify the obtained results while running the algorithm at the same time by dealing with the randomness issue within the limited blockchain structure. We implement and experiment with BLOR using Python and the Solidity language on Ethereum. BLOR is benchmarked against several models where it proved to be highly efficient in selecting the most reliable and economical oracles with a fair balance. • We propose BLOR, a Bayesian Bandit Learning model for Oracles Reliability. • BLOR identifies trustless and cost-efficient oracles. • BLOR integrates reinforcement learning to a Bayesian cost-driven reputation model. • BLOR is implemented in Ethereum and benchmarked against several algorithms. • BLOR shows a steady performance even in low to high noisy dynamic environments. [ABSTRACT FROM AUTHOR]

The paper proposes a novel model checking-based approach towards verifying the compliance of intelligent agent-based web services with contracts regulating their compositions specified in the Business Process Execution Language (BPEL). Unlike the existing approaches in the literature, the main contribution and impact of the introduced approach is the ability to verify intelligent and autonomous composite web services by capturing and describing in details both compliance and violation behaviors, how the system can distinguish between them, and how the system reacts and can be recovered after each violation. The approach encompasses three contributing parts, namely: 1) the marking process of an extended BPEL; 2) the transformation of the extended and marked BPEL to an automata model; and 3) the encoding of the resulting automata model into the Interpreted Systems Programming Language (ISPL), the input language of the MCMAS model checker for intelligent and autonomous multi-agent systems. In the first part, we extend BPEL that specifies the business process of the composition by creating custom activities called labels. We use those labels as means to represent the specifications and mark the points the developer aims to verify. A significant advantage of this labeling is the ability to highlight specific points in the design to be verified and to distinguish compliance behaviors from violations, which makes this verification focused and highly efficient. In the second part, we introduce new transformation rules to transform the extended and marked BPEL to an automata model. This transformation requires a prior modeling of agent-based web services composition using automata definitions. In the third part, we introduce algorithmic translation rules encoding the resulting automata model into ISPL. This translation makes model checking the behavior of our contract-driven compositions possible. A novel characteristic of the proposed approach is the automatic generation of the properties against which the system is verified from the composition’s implementation, which is technically challenging. The verification properties are expressed in the Computation Tree Logic of Commitments (CTLC). Technically, CTLC provides a powerful representation to formally model 1) interactions among multi-agent based web services and 2) compliance and violation behaviors within composite business contracts by making use of communicative commitment operators. CTLC also includes a fulfillment operator which helps formally check the compliance with business contracts and specify the system recovery. A detailed case study from expert and intelligent systems domain along with experimental results are also reported in the paper. Finally, the main impact and significance of the paper on expert and intelligent systems is the ability to use these systems safely since there is a way to verify if the intelligent components behave according to and in compliance with the underlying regulating contracts. [ABSTRACT FROM AUTHOR]

Social approaches have been put forward to define semantics for intelligent agent communication messages and to tackle the shortcomings of mental approaches. Formal semantics of those social approaches can be model checked as they are focused on public behaviors instead of private mental states. Social conditional commitments are essential concepts in social approaches that can effectively model agent communications. However, conditional commitments exclusively are not able to model agent communication actions, the cornerstone of the fundamental agent communication theory, namely speech act theory. These actions provide mechanisms for dynamic interactions and enable designers to track the evolution of active conditional commitments. From the perspective of model checking, we need to define a formal and computationally grounded semantics for relevant social actions that can directly be applied to active conditional commitments. This manuscript describes a new symbolic model checker, SMC4AC, developed and implemented to automate the verification of interaction among intelligent agents. SMC4AC is the result of developing a new symbolic model checking algorithm devoted to CTLCα, a combination of CTL and new temporal modalities to represent and reason about conditional commitments and common commitment actions. The core of this paper consists of a new logical language, a detailed description of the symbolic algorithms needed for commitments and their action modalities, complexity analysis, implementation and application. The implementation of our algorithm and its graphical user interface is built on top of the MCMAS symbolic model checker tailored for checking intelligent multi-agent systems. We select business processes and multi-agent interaction protocols as application domains to test and validate the effectiveness and scalability of SMC4AC. We report extensive experimental results, which confirm the theoretical findings and make SMC4AC practical. [ABSTRACT FROM AUTHOR]

With the advent of cloud computing and the rapid increase in the number of deployed services, the competition between functionally-similar Web services is increasingly governing the markets of services. For example, Amazon and Google are in an intense competition to dominate the market of cloud-based Web services. Such a highly competitive environment motivates and sometimes obliges services to abandon their pure competitive strategies and adopt a cooperative behavior in order to increase their business opportunities and survive in the market. Several approaches have been advanced in the literature to model the cooperation among Web services in a community-based environment. However, the existing approaches suffer from two main drawbacks that limit their effectiveness in the real-world services market. First, they rely on a centralized architecture wherein a master entity is responsible for regulating the community formation process, which creates a single point of failure. Second, they ignore the business potential of the services and treat all of those services in the same way, which demotivates the participation of the well-positioned ones in such communities. To tackle these problems, we distinguish in this paper between two types of services: leaders and followers . Leaders are those services that enjoy high reputation, market share, and capacity of handling requests; whereas followers are those services that cannot compete against the leaders. Thereafter, we model the community formation problem as a virtual trading market between these two types of services and propose a distributed Stackelberg game for this purpose. Promisingly, the proposed model gives guidance to a cooperative model that can be applied in the real markets of Web services in order to achieve higher performance, efficient services compositions, and better resources utilization. The performance of the model is analyzed using a real-life flight booking dataset that includes 2507 services operating on the Web. Simulation results show that the proposed model is able to increase the satisfaction of Web services in terms of gained payoff and reputation and the satisfaction of users in terms of quality of service provided to their requests compared to the existing models, namely the one-stage game theoretical model and a heuristic model. [ABSTRACT FROM AUTHOR]

Benthem’s correspondence theory is one of the most important tools of the theory of modal logics developed in the last three decades. Correspondence theory, a subfield of the model theory, reflects a systematic study of relations between classes of frames and modal language. In this paper, we use correspondence theory for modal logics to solve a problem not addressed yet in the literature, namely the soundness and completeness of a logic combining two different, yet related modalities: agents’ knowledge and commitments. The paper proves the soundness and completeness of this logic called CTLKC + . This work is highly significant as it proves that combining the two agents’ modalities resulted in a consistent logic that can be used to design reliable systems. The methodology is as follows: we develop a set of reasoning postulates (axioms) that reflect the interaction between agents’ knowledge and social commitments in multi-agent system (MAS) using the CTLKC + logic and correspond them to certain classes of frames. In particular, we first give a name, formalization and meaning for each postulate. Then, we correspond the postulates to certain classes of frames and provide the required proofs. Thereafter, we present a discussion that illustrates the importance of the proposed postulates in MASs using a concrete application example called the NetBill protocol taken from the business domain. Finally, we show how the postulates were addressed in the literature. The existence of such a correspondence allows us to prove that the logic generated by any subset of these postulates is sound and complete with respect to models that are based on the corresponding frames. The ultimate goal of this paper is to further assess the logic of knowledge and commitments (CTLKC + ) from a new perspective (i.e., the soundness and completeness). Consequently, this work advances the literature of logics in MASs and closes a gap that has not been explored before. [ABSTRACT FROM AUTHOR]

Though modeling and verifying Multi-Agent Systems (MASs) have long been under study, there are still challenges when many different aspects need to be considered simultaneously. In fact, various frameworks have been carried out for modeling and verifying MASs with respect to knowledge and social commitments independently. However, considering them under the same framework still needs further investigation, particularly from the verification perspective. In this article, we present a new technique for model checking the logic of knowledge and commitments (CTLKC + ). The proposed technique is fully-automatic and reduction-based in which we transform the problem of model checking CTLKC + into the problem of model checking an existing logic of action called ARCTL. Concretely, we construct a set of transformation rules to formally reduce the CTLKC + model into an ARCTL model and CTLKC + formulae into ARCTL formulae to get benefit from the extended version of NuSMV symbolic model checker of ARCTL. Compared to a recent approach that reduces the problem of model checking CTLKC + to another logic of action called GCTL ∗ , our technique has better scalability and efficiency. We also analyze the complexity of the proposed model checking technique. The results of this analysis reveal that the complexity of our reduction-based procedure is PSPACE-complete for local concurrent programs with respect to the size of these programs and the length of the formula being checked. From the time perspective, we prove that the complexity of the proposed approach is P-complete with regard to the size of the model and length of the formula, which makes it efficient. Finally, we implement our model checking approach on top of extended NuSMV and report verification results for the verification of the NetBill protocol, taken from business domain, against some desirable properties. The obtained results show the effectiveness of our model checking approach when the system scales up. [ABSTRACT FROM AUTHOR]

The competency to compose web services from available services is one of the most crucial problems in the paradigm of service-oriented computing. Conventional software engineering approaches and even standard languages compose web services as workflow models that control the business logic required to coordinate data over participating services. Such models would not apply to the design of multi-agent based web services, which offer high-level abstractions that support autonomy, business-level compliance, and flexible dynamic changes. In this article, we model interactions among multi-agent based web services by commitment modalities in the form of contractual obligations and devote multi-agent commitment protocols to regulate such interactions and engineer services composition. We develop and fully implement an automatic verifier by enriching the MCMAS model checker with certain symbolic algorithms to verify the correctness of protocols, given properties expressed in a temporal commitment logic, suitably extended with actions. We analyze the time and space complexity of the verifier. Finally, we present the experimental results of two case studies, adopted to check the verifier's efficiency and scalability. [ABSTRACT FROM AUTHOR]

Highlights: [•] We present an extension of interpreted systems including probabilities and communication channels. [•] We introduce a new logic merging probabilities, knowledge, and social commitments. [•] We advocate a reduction-based technique to model check the logic and prove its soundness. [•] We implement the approach using the PRISM model checker. [Copyright &y& Elsevier]

Highlights: [•] We formalize the question of competing or cooperating for communities of agent-based services. [•] We use the game-theoretic best response technique to analyze competitive/cooperative behaviors of autonomous services within communities. [•] We analyze the computational complexity of the proposed decision mechanism and prove its efficiency. [•] We confirm the theoretical results through extensive simulation using real dataset of services on the web. [ABSTRACT FROM AUTHOR]

Highlights: [•] We define a new set of uncertainty measures for negotiation dialogue games. [•] We analyze the complexity of argumentation selection mechanism. [•] We formalize and analyze the uncertainty index of playing the right move. [•] We formalize and analyze the uncertainty of the move to be accepted by the addressee. [Copyright &y& Elsevier]

Abstract: Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. However, systems have also quantitative and uncertain (i.e., probabilistic) properties such as degree of reliability and reachability, which still need further attention from the model checking perspective. In this paper, we analyze such properties and present a new method for probabilistic model checking of epistemic multi-agent systems specified by a new probabilistic–epistemic logic PCTLK. We model multi-agent systems as distributed knowledge bases using probabilistic interpreted systems and define transformations from those interpreted systems into discrete-time Markov chains and from PCTLK formulae to PCTL formulae, an existing extension of CTL with probabilities. By so doing, we are able to convert the PCTLK model checking problem into the PCTL one. Thus, we make use of PRISM, the model checker of PCTL without adding new computation cost. A concrete case study has been implemented to show the applicability of the proposed technique along with performance analysis and comparison with MCK, an epistemic–probabilistic model checker, and MCMAS, a model checker for multi-agent systems, in terms of execution time and state space scalability. [Copyright &y& Elsevier]

Abstract: In agent and (web) service computing, collaboration takes place when distributed entities have limited knowledge and capabilities, so they cannot perform required tasks without interacting and helping each other. For instance, web services, which are loosely-coupled business applications, are called to cooperate in distributed settings for the sake of efficiency. In this context, agents that abstract and act on behalf of web services could act in cooperative groups that gather a number of agents sharing some common goals. Enabling those agent-based web services to decide about their strategies in terms of joining and acting within groups, inviting other agents to join, and leaving a group to act alone is an open issue that we address in this work. In this paper, we propose a framework where agent-based web services select strategies that maximize their outcomes. These strategies could be categorized into cooperative strategies involving other agents and strategies that highlight the single operative attitude. Although cooperation seems to bring better utility to cooperative agents, we highlight that web services in some environments obtain better outcome while they act individually (i.e., outside the group). This means that the cost of cooperation (in some particular cases) might negatively influence the outcome and obtained utility. As solution, we propose in this paper (1) an agent-based model that formalizes web services decision making where different parameters are considered; and (2) a game-theoretic framework that analyzes the web services strategies allowing them to maximize their acting performance where non-zero-sum games are being used. The paper presents theoretical results, which are also confirmed through extensive simulations. [Copyright &y& Elsevier]

Abstract: This paper addresses the issue of verifying if composite Web services design meets some desirable properties in terms of deadlock freedom, safety (something bad never happens), and reachability (something good will eventually happen). Composite Web services are modeled based on a separation of concerns between business and control aspects of Web services. This separation is achieved through the design of an operational behavior, which defines the composition functioning according to the Web services’ business logic, and a control behavior, which identifies the valid sequences of actions that the operational behavior should follow. These two behaviors are formally defined using automata-based techniques. The proposed approach is model checking-based where the operational behavior is the model to be checked against properties defined in the control behavior. The paper proves that the proposed technique allows checking the soundness and completeness of the design model with respect to the operational and control behaviors. Moreover, automatic translation procedures from the design models to the NuSMV model checker’s code and a verification tool are reported in the paper. [Copyright &y& Elsevier]

Abstract: Although several approaches have been proposed to specify multi-agent commitment-based protocols that capture flexible and rich interactions among autonomous and heterogeneous agents, very few of them synthesize their formal specification and automatic verification in an integrated framework. In this paper, we present a new logic-based language to specify commitment-based protocols, which is derived from ACTL∗c , a logic extending CTL∗ with modalities to represent and reason about social commitments and their actions. We present a reduction technique that formally transforms the problem of model checking ACTL∗c to the problem of model checking GCTL∗ (an extension of CTL∗ with action formulae). We prove that the reduction technique is sound and we fully implement it on top of the CWB-NC model checker to automatically verify the NetBill protocol, a motivated and specified example in the proposed specification language. We also apply the proposed technique to check the compliance of another protocol: the Contract Net protocol with given properties and report and discuss the obtained results. We finally develop a new symbolic algorithm to perform model checking dedicated to the proposed logic. [Copyright &y& Elsevier]

Abstract: Maintaining sound reputation requires robust control and investigation. In this paper, we analyze a reputation mechanism that objectively maintains accurate reputation evaluation of selfish agent-based web services. In the proposed framework, web services are ranked using their reputation as a result of provided feedback reflecting consumers’ satisfaction. However, selfish web services may alter their public reputation level by managing to get fake feedback. We investigate the payoffs of different scenarios by focusing on the issues that discourage web services to act maliciously. We also analyze the details of the proposed mechanism by discussing simulation and empirical results that fully depict the system parameters and show the feasibility of the proposed approach. [Copyright &y& Elsevier]

Abstract: We refine CTLC, a temporal logic of social commitments that extends CTL to allow reasoning about commitments agents create when communicating and their fulfillment. We present axioms of commitments and their fulfillment and provide the associated BDD-based model checking algorithms. We also analyze the time complexity of CTLC model checking in explicit models (i.e., Kripke-like structures) and its space complexity for concurrent programs, which provide compact representations. We prove that although CTLC extends CTL, their model checking algorithms still have the same time complexity for explicit models, which is P-complete with regard to the size of the model and length of the formula, and the same complexity for concurrent programs, which is PSPACE-complete with regard to the size of the components of these programs. We fully implemented the proposed algorithms on top of MCMAS, a model checker for the verification of multi-agent systems, and provide in this paper simulation results of an industrial case study. [Copyright &y& Elsevier]

Abstract: In open multi-agent systems, agents engage in interactions to share and exchange information. Due to the fact that these agents are self-interested, they may jeopardize mutual trust by not performing actions as they are expected to do. To this end, different models of trust have been proposed to assess the credibility of peers in the environment. These frameworks fail to consider and analyze the multiple factors impacting the trust. In this paper, we overcome this limit by proposing a comprehensive trust framework as a multi-factor model, which applies a number of measurements to evaluate the trust of interacting agents. First, this framework considers direct interactions among agents, and this part of the framework is called online trust estimation. Furthermore, after a variable interval of time, the actual performance of the evaluated agent is compared against the information provided by some other agents (consulting agents). This comparison in the off-line process leads to both adjusting the credibility of the contributing agents in trust evaluation and improving the system trust evaluation by minimizing the estimation error. What specifically distinguishes this work from the previous proposals in the same domain is its novelty in after-interaction investigation and performance analysis that prove the applicability of the proposed model in distributed multi-agent systems. In this paper, the agent structure and interaction mechanism of the proposed framework are described. A theoretical analysis of trust assessment and the system implementation along with simulations are also discussed. Finally, a comparison of our trust framework with other well-known frameworks from the literature is provided. [Copyright &y& Elsevier]

The purpose of this paper is to propose a formal description and implementation of a negotiation protocol between autonomous agents using persuasive argumentation. This protocol is designed to be simple and computationally efficient. The computational efficiency is achieved by specifying the protocol as a set of simple logical rules that software agents can easily combine. These latter are specified as a set of computational dialogue games about which agents can reason. The protocol converges by checking the termination conditions. The paper discusses the formal properties of the protocol and addresses, as proof of concept, the implementation issues using an agent-oriented platform equipped with logical programming mechanisms. [ABSTRACT FROM AUTHOR]

Abstract: This paper presents an agent-based framework for modeling and deploying usiness-to-usiness () applications, where autonomous agents act on behalf of the individual components that form these applications. This framework consists of three levels identified by strategic, application, and resource, with focus in this paper on the first two levels. The strategic level is about the common vision that independent businesses define as part of their decision of partnership. The application level is about the business processes that get virtually combined as result of this common vision. As conflicts are bound to arise among the independent applications/agents, the framework uses a formal model based on computational argumentation theory through a persuasion protocol to detect and resolve these conflicts. In this protocol, agents reason about partial information using partial arguments, partial attack, and partial acceptability. Agents can then jointly find arguments that support a new solution for their conflicts, which is not known by any of them individually. Termination, soundness, and completeness properties of this protocol are provided. Distributed and centralized coordination strategies are also supported in this framework, which is illustrated with an online-purchasing example. [ABSTRACT FROM AUTHOR]

Abstract: Model checking is a formal technique used to verify communication protocols against given properties. In this paper, we propose a new model checking algorithm aims at verifying systems designed as a set of autonomous interacting agents. These software agents are equipped with knowledge and beliefs and interact with each other according to protocols governed by a set of logical rules. We present a tableauased version of this algorithm and provide the soundness, completeness, termination and complexity results. A case study about an agent-based negotiation protocol and its implementation are also described. [Copyright &y& Elsevier]

• We propose a new probabilistic verification approach for agent-based systems. • We consider the interaction between group commitments and knowledge. • We transform model checking our extended commitment logic to model checking PCTL. • We prove the soundness and completeness of the approach and analyze its complexity. • We use PRISM to implement and evaluate our technique on two concrete case studies. 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 ( PCTL kc + ). In the proposed approach, model checking PCTL kc + is reduced to model checking the probabilistic branching-time logic PCTL. This is achieved by transforming PCTL kc + model to a Markov Decision Process (MDP), and reducing PCTL kc + 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. [ABSTRACT FROM AUTHOR]

• We introduce a novel trust model of IoT services considering dynamic environments. • We define a subjective, objective, collusion resistant and bootstrapped trust model. • We use the log score and error estimation to assess the model's prediction accuracy. • We use the ROC curves to measure the accuracy of the bootstrapping trust mechanism. • We employ real dataset to show the performance and efficiency of the proposed model. The paper addresses the problem of trust management of cloud, fog and IoT services in dynamically changing environments. The continuous dynamic environment is one of the challenges that trustworthy services management in the cloud, fog and IoT settings faces. Services in such an environmental context have difficulty securing an acceptable quality of service (QoS). This article proposes a trust management framework that establishes service trust by considering the direct trust from the truster (subjective trust), aggregating referrals about the service in a collusion-resistant manner (objective trust), and bootstrapping new services. We introduce a subjective trust model based on the formalism of dependency networks to dynamically predict the provided QoS in response to context environment changes. The proposed approach leverages the dependency relations that exist among the QoS metrics and environmental context variables. The novelty at the subjective trust level lies in considering the dynamic cyclic dependency relations that enhances the prediction accuracy. However, subjective trust based on direct interactions could be insufficient to make the trust estimate credible. Hence, on top of the subjective layer, we propose an objective trust management model resilient to collusion attacks by leveraging the power of mass collaboration among referees. Finally, we propose a bootstrapping mechanism that is resilient to the white-washing attacks by observing the behaviours of newcomer services with no trust resources using the concept of social adoption to estimate their initial trust values. Experiments conducted on real-life and synthetic datasets demonstrate the effectiveness of our approach compared with state-of-the-art approaches. We used the statistical log score to assess the model's prediction accuracy and employed the estimation error of the objective trust as indicated by referees relative to the one calculated by the multi-round simulation. The ROC (Receiver Operating Characteristic) curves are finally used to measure the accuracy of the classifier used in the proposed trust bootstrapping mechanism in providing accurate initial trust values. The main findings of the paper are around the new trust model of cloud, fog and IoT services considering their dynamically changing environments. The first finding is that the prediction of the provided QoS shows better results when it is dynamic and responds to context environment changes by leveraging the dynamic dependency network linking the QoS metrics and context variables of the environment. The second finding is that the objective trust performs better when it is resilient to collusion attacks by leveraging the power of mass collaboration among referees. The third finding is that the bootstrapping mechanism that observes the behaviours of new comer services with no trust resources using the concept of social adoption to estimate their initial trust values excels by being resilient to white watching attacks. [ABSTRACT FROM AUTHOR]

Testing embedded systems software has become a costly activity as these systems become more complex to fulfill rising needs. Testing processes should be both effective and affordable. An ideal testing process should begin with validated requirements and begin as early as possible so that requirements defects can be fixed before they propagate and become more difficult to address. Furthermore, the testing process should facilitate test procedures creation and automate their execution. We propose a novel methodology for testing functional requirements. The methodology activities include standard notations, such as UCM for modeling scenarios derived from requirements, TDL for describing test cases and TTCN-3 for executing test procedures; other test scripting languages can also be used with our methodology. Furthermore, the automation of the methodology generates test artifacts through model transformation. The main goals of this test methodology are to leverage requirements represented as scenarios, to replace the natural language test case descriptions with test scenarios in TDL, and to generate executable test procedures. Demonstration of the feasibility of the proposed approach is based on a public case study. An empirical evaluation of our approach is given using a case study from the avionics domain. [ABSTRACT FROM AUTHOR]

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. • The paper presents a comprehensive survey on transformers for deep learning tasks. • The paper conducts a thorough analysis on highly effective models in five domains. • The paper classifies the models based on respective tasks using a proposed taxonomy. • The characteristics of the surveyed models are deeply explored and analyzed. • Future directions and challenges for transformer-based models are deciphered. [ABSTRACT FROM AUTHOR]

Despite the widespread usage of the evaluation mediums for online services by the clients, there is a requirement for a trust evaluation tool that provides the clients with the degree of trustworthiness of the service providers. Such a tool can provide increased familiarity with unknown third party entities, e.g. service providers, especially when those entities neither project completely trustworthy nor totally untrustworthy behaviour. Indeed, developing some metrics for trust evaluation under uncertainty can come handy, e.g., for customers interested in evaluating the trustworthiness of an unknown service provider throughout queries to other customers of unknown reliability. In this research, we propose an evaluation metric to estimate the degree of trustworthiness of an unknown agent, say aD, through the information acquired through a group of agents who have interacted with agent aD. This group of agents is assumed to have an unknown degree of reliability. In order to tackle the uncertainty associated with the trust of these set of unknown agents, we suggest to use possibility distributions. Later, we introduce a new certainty metric to measure the degree of agreement in the information reported by the group of agents in A on agent aD. Fusion rules are then used to measure an estimation of the agent aD's degree of trustworthiness. To the best of our knowledge, this is the first work that estimates trust, out of empirical data, subject to some uncertainty, in a discrete multi-valued trust domain. Finally, numerical experiments are presented to validate the proposed tools and metrics. [ABSTRACT FROM AUTHOR]

With increasing adoption of cloud services in the e-market, collaboration between stakeholders is easier than ever. Consumer stakeholders demand data from various sources to analyze trends and improve customer services. Data-as-a-service enables data integration to serve the demands of data consumers. However, the data must be of good quality and trustful for accurate analysis and effective decision making. In addition, a data custodian or provider must conform to privacy policies to avoid potential penalties for privacy breaches. To address these challenges, we propose a twofold solution: 1) we present the first information entropy-based trust computation algorithm, IEB_Trust, that allows a semitrusted arbitrator to detect the covert behavior of a dishonest data provider and chooses the qualified providers for a data mashup and 2) we incorporate the Vickrey–Clarke–Groves (VCG) auction mechanism for the valuation of data providers’ attributes into the data mashup process. Experiments on real-life data demonstrate the robustness of our approach in restricting dishonest providers from participation in the data mashup and improving the efficiency in comparison to provenance-based approaches. Furthermore, we derive the monetary shares for the chosen providers from their information utility and trust scores over the differentially private release of the integrated dataset under their joint privacy requirements. [ABSTRACT FROM AUTHOR]

• We propose a formal approach to model, verify and test avionics systems. • We use intelligent agents to model the components of the landing gear system. • We introduce extended interpreted systems to reason about interactions and actions. • We introduce a testing methodology that follows a test-driven development approach. • We use MCMAS+ to generate traces for test suites achieving new coverage criteria. The paper contributes by introducing a novel, formal and operational approach that addresses the open challenging issues of modeling, verifying, and testing intelligent critical avionics systems. We advance the state-of-the-art by unifying the three challenges and considering the intelligence, autonomy, and accountability of the components as first citizen concepts. The proposed methodology is effectively applied to a real, practical and complex case study of intelligent avionics systems, namely the landing gear system and uses multi-agent systems to model each main component in the system as an intelligent agent. We also introduce the formalism of extended interpreted systems that supports intelligence, autonomy, communication, input and output actions, predicate conditions and post-conditions. The paper adopts the computation tree logic of conditional commitments to model communication among autonomous agents and trace its progress. The symbolic model checker of this logic is used to run the verification of the system model, encoded in an extended input language, against coverage criteria and properties. Furthermore, we introduce a new testing methodology that: 1) Follows a test-driven development approach; 2) performs unit testing, component testing, and system testing in each increment; and 3) uses model checking to generate automatically counterexamples and witness traces interpreted into concrete test suites that achieve new coverage criteria. The experimental results showed the efficiency and scalability of the developed approach against a transformation-based technique. Finally, the computational complexity of the developed approach is analysed. [ABSTRACT FROM AUTHOR]

In recent past, sensors and wireless sensor networks have played a major role in the success of smart environments such as smart cities, smart homes, and smart transportation. The artificial intelligent methods, such as machine learning, brain-inspired computing and other advanced artificial intelligence techniques are successfully employed in various areas of robotics, knowledge discovery, big data and other ICT domains. This community and social role detection method called SocioRank* using email interaction data crawled from a graduate class of students. [Extracted from the article]

The infrastructureless and decentralized nature of Vehicular Ad Hoc Network (VANET) makes it quite vulnerable to different types of malicious attacks. Detecting such attacks has attracted several contributions in the past few years. Nonetheless, the applicability of the current detection mechanisms in the deployed vehicular networks is hindered by two main challenges imposed by the special characteristics of VANETs. The first challenge is related to the highly mobile nature of vehicles that complicates the processes of monitoring, buffering, and analyzing observations on these vehicles as they are continuously moving and changing their locations. The second challenge is concerned with the limited resources of the vehicles especially in terms of storage space that restricts the vehicles’ capacity of storing a huge amount of observations and applying complex detection mechanisms. To tackle these challenges, we propose a multi-decision intelligent detection model called CEAP that complies with the highly mobile nature of VANET with increased detection rate and minimal overhead. The basic idea is to launch cooperative monitoring between vehicles to build a training dataset that is analyzed by the Support Vector Machine (SVM) learning technique in online and incremental fashions to classify the smart vehicles either cooperative or malicious. To adapt the proposed model to the high mobility, we design it on top of the VANET QoS-OLSR protocol, which is a clustering protocol that maintains the stability of the clusters and prolongs the network’s lifetime by considering the mobility metrics of vehicles during clusters formation. To reduce the overhead of the proposed detection model and make it feasible for the resource-constrained nodes, we reduce the size of the training dataset by (1) restricting the data collection, storage, and analysis to concern only a set of specialized nodes (i.e., Multi-Point Relays) that are responsible for forwarding packets on behalf of their clusters; and (2) migrating only few tuples (i.e., support vectors) from one detection iteration to another. We propose as well a propagation algorithm that disseminates only the final decisions (instead of the whole dataset) among clusters with the aim of reducing the overhead of either exchanging results between each set of vehicles or repeating the detection steps for the already detected malicious vehicles. Simulation results show that our model is able to increase the accuracy of detections, enhance the attack detection rate, decrease the false positive rate, and improve the packet delivery ratio in the presence of high mobility compared to the classical SVM-based, Dempster–Shafer-based, and averaging-based detection techniques. [ABSTRACT FROM AUTHOR]