Search

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]

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. [ABSTRACT FROM AUTHOR]

Interaction among autonomous agents in Multi-Agent Systems (MASs) is a key aspect for agents to coordinate with one another. Social approaches, as opposed to the mental approaches, have recently received a considerable attention in the area of agent communication. They exploit observable social commitments to develop a verifiable formal semantics through which communication protocols can be specified. Developing and implementing algorithmic model checking for social commitments have been recently addressed. However, model checking social commitments in the presence of uncertainty is yet to be investigated. In this paper, we propose a model checking technique for verifying social commitments in uncertain settings. Social commitments are specified in a modal logical language called Probabilistic Computation Tree Logic of Commitments (PCTLC). The modal logic PCTLC extends PCTL, the probabilistic extension of CTL, with modalities for commitments and their fulfillments. The proposed verification method is a reduction-based model checking technique to the model checking of PCTL. The technique is based upon a set of reduction rules that translate PCTLC formulae to PCTL formulae to take benefit of existing model checkers such as PRISM. Proofs that confirm the soundness of the reduction technique are presented. We also present rules that transform our new version of interpreted systems into models of Markov Decision Processes (MDPs) to be suitable for the PRISM tool. We implemented our approach on top of the PRISM model checker and verified some given properties for the Oblivious Transfer Protocol from the cryptography domain. Our simulation demonstrates the effectiveness of our approach in verifying and model checking social commitments in the presence of uncertainty. We believe that the proposed formal verification technique will advance the literature of social commitments in such a way that not only representing social commitments in uncertain settings is doable, but also verifying them in such settings becomes achievable. [ABSTRACT FROM AUTHOR]

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]

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: 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]

• 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]