Search

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]

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]

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]

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

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