Several formal trust frameworks have been introduced in the area of Multi-Agent Systems (MASs). However, the problem of model checking trust logics is still a challenging research topic that has not been sufficiently investigated yet. In this paper, we address this challenge by proposing a formal and fully automatic model checking technique for a temporal logic of trust. From the logical perspective, the starting point of our proposal is TCTL, a Computation Tree Logic of preconditional Trust that has been recently proposed. We extend this logic by introducing a new modality for conditional trust and describe the logical relationship between preconditional and conditional trust. From the formal verification perspective, we develop transformation-based algorithms fully implemented in a Java toolkit that automatically interacts with the NuSMV model checker. Our verification approach automatically transforms the problem of model checking TCTL into the problem of model checking CTL. We also develop a model checking algorithm for the conditional trust. We provide proofs of the soundness and completeness of our transformation algorithms. Finally, experiments conducted on a standard industrial case study of auto-insurance claim processing demonstrate the efficiency and scalability of our approach in verifying TCTL and conditional trust formulae.
Trust is regarded as being one of the key aspects behind the success and growth of applications based on Multi-Agent Systems (MASs). It has been the focus of many research projects, both theoretical and practical, in the recent years, particularly in domains where open multi-agent technologies are applied (e.g., Internet-based markets, information retrieval, etc.). The importance of trust in such domains arises mainly because it provides a social control that regulates the relationships and interactions among agents. However, despite the growing number of various multi-agent applications, they still encounter many challenges in the verification of agents' behaviors. The existence of many autonomous entities in such systems makes this verification difficult due to the increase in their complexity and heterogeneity. The main challenge that faces MASs is how to ensure the reliability of the trust relationships in the presence of misbehaving entities. Such entities not only create an exception for other agents, but also may obstruct their proper work [26]. The fact that such systems usually operate in open and uncertain environments makes reasoning about trust and checking the existence of untrusted computations highly desired.
Many formalisms and approaches that facilitate the specifications of trust in MASs can be found in the literature. However, few approaches addressed trust from a high level abstraction viewpoint [12,13,37]. Modal logic approaches provide powerful mechanisms that can be effectively used for trust reasoning. Such approaches yield a formal semantics to reason about trust properties in various applications such as security protocols, information sources, and e-markets. For instance, in [10,23,31], the authors proposed several logical frameworks for the concept of trust. Trust in such logics is mostly expressed as a combination of different modalities based on the logic of action and time [22] and the BDI logic [8]. In [28], a modal logic for reasoning about the interaction between belief, evidence and trust is presented. Other approaches are interested in analyzing trust in information sources [3,10,11,27]. Moreover, some proposals have addressed trust in the context of computer security [21,31]. Most of these approaches focus on the cognitive side of trust (i.e., trusted agents are capable of exhibiting beliefs, desires, and intentions properties). Hence, the trust is considered as a belief of an agent (the truster) involving ability and willingness of the trustee to perform some actions for the truster. Although these approaches are highly appropriate to reason about trust, their verification faces a fundamental limitation due to their reliance on the internal structure of the interacting agents. In fact, the distributed and open nature of MASs makes the capability of handling and verifying the trust interaction issues of such approaches arduous. That is, it is very difficult for one agent to completely trust others by making assumptions about their internal states.
As in [12,13,37], in this paper, we are considering a cognitive-independent view of trust where trust ingredients are seen from a non-epistemic angle. Trust in our work is defined from a high-level abstraction perspective without having to depend on individual agents' internal states. We represent trust as a direct relation from one agent, the truster, toward another agent, the trustee, where such a relation presupposes specific preconditions with respect to a particular content. Specifically, the truster considers the trustee as a trustworthy agent with regard to a specific content when the behavior of the trustee with respect to this content is as the truster expects, where this expectation is shared by the two participants. For example, the buyer trusts that the seller will deliver the ordered items upon the buyer's payment, where the payment consists the precondition and the order delivery is the expectation commonly shared. From the modeling and specification perspectives, we are considering the Trust Computation Tree Logic (TCTL) [13], an extension of the CTL logic [19]. Equipped with reasoning postulates, TCTL does not only provide a formal basis for reasoning about trust states with preconditions, but it can also be seen as a formal modeling of the social trust interactions among agents.
As mentioned earlier, the fact that agents are autonomous and have to interact with each other within unreliable social environments entails that deciding whether to trust another agent (for instance to perform some actions) or not is a challenging task. For instance, agents may not be able to comply with their obligations (e.g., an agent may not send the agreed payment for goods received). This raises the need for developing efficient methodologies to handle their present and future behaviors in order to ensure the fulfillment of the system requirements. Currently, the technique of model checking [6,7] has attracted several contributions with a significant industrial implication. Although these contributions addressed a number of multi-agent aspects such as social commitments [4,14] and knowledge [30,41], model checking trust in multi-agent settings has not been sufficiently investigated yet. From this view, we aim in this work to contribute in the modeling and verification of trust systems. To do so, we show how trust is formally defined and present a formal and fully automatic model checking technique to verify trust properties. We consider two types of trust, analyze the relationship between them and develop transformation-based model checking techniques for verifying the properties that an agent requires to be achieved by the trusted agent. The two types are preconditional, where trust requires first the satisfaction of the precondition, and conditional, where trust is expressed with antecedents and consequences. The following example shows a typical situation in the context of electronic commerce where trust is a highly desired property.
Example 1. Let us consider the buyers-sellers relationships. The seller has to trust the buyer that the payment for the ordered goods will be sent, and the buyer has to trust the seller to ship the goods. For instance, the buyer requests to purchase one or more items from the seller (i.e., the trust relationship is established between the two parties). Once the former selects an item, the seller trusts that buyer with regard to the payment in order for the request to take place. When the requested items are paid, the seller confirms the order and starts the delivery process. Finally, the requested items are shipped and the buyer is notified.
Obviously, on-line interactions are characterized by uncertainty and, moreover, the anonymity of the interaction partners. Thus, there is no guarantee that this process will be surely satisfied in concrete applications. Therefore, the need for a logical language that can provide a certain level of abstraction with the ability to express the trust properties explicitly and a verification procedure to verify the trust interactions are of great significance. Figure 1 illustrates the overall approach of model checking TCTL, which consists of three different but integrated phases. In the first phase, we recall the logic TCTL and its formal model defined using the formalism of vector-based interpreted systems [13]. In the second phase, we introduce our formal verification technique based on transforming the problem of model checking TCTL into the problem of model checking CTL. In the third phase, we implement our transformation technique in a Java toolkit that automatically interacts with the NuSMV model checker and report the verification results using a case study. Moreover, the paper also introduces conditional trust which is not expressed in TCTL, analyzes the logical relationship between preconditional and conditional trust and exploits this relationship to design a new algorithm to verify properties with conditional trust.
TCTL model represented as a Vector-based Interpreted System TCTL formula 𝝋
Transformed CTL model represented as a Kripke Structure 𝒇(𝑴)
Transformed CTL formula The present article is organized as follows. We discuss the related work in Section 2. In Section 3, we recall the syntax and semantics of the TCTL logic framework, and introduce the conditional trust along with its syntax, semantics, and logical relationship with preconditional trust. We present our formal transformation algorithms to model check TCTL and conditional trust in Section 4 along with the soundness and completeness proofs. In Section 5, we present the case study and experimental results obtained using the tool that implements our transformation algorithms. We conclude and identify future research directions in Section 6.
While the number of proposals on trust modeling is significant, they differ, however, in the topics they addressed and the systems they implemented. In this paper, we are primarily concerned with the issues of reasoning about and verifying trust in the context of MASs using the model checking approach, which has not been deeply investigated yet for trust systems. Various approaches on trust modeling have developed modal logics that capture the important elements of the cognitive theory of trust as proposed in [5]. In these approaches, trust is considered as a mental attitude based on a specific set of goals and expressed in terms of certain beliefs. In this respect, Herzig et al. [23] proposed a formal logical framework to formally reason about occurrent and dispositional trust in a multi-agent environment. The authors defined a logic that combines temporal, dynamic, belief and choice logics. Moreover, the proposed logic is extended with operators to allow reasoning about reputation in the scope of collective beliefs. In another work [24], Herzig and his colleagues simplified the previous logic presented in [23] by considering a very simple kind of actions based on the concepts of propositional assignment. That is, the truth values of a propositional variable is assigned to either true or false by the corresponding agents' actions. The new logic provides a simple framework, and it is expressive enough to account for the cognitive theory of trust. In [28], Liu and Lorini presented a new dynamic logic called DL-BET for reasoning about the interaction between belief, evidence and trust. The authors introduced three modal operators where each of these concepts are respectively represented. In this logic, the trust operator semantics is interpreted using neighborhood semantics [32], which maps each world into a set of subsets of worlds. The authors provided a complete axiomatization for both the static component of the proposed logic and its dynamic extension. Other approaches have focused on trust in information sources. In this line, an early work presented BIT, a modal logic that extends the traditional doxastic logic with modalities for representing belief, information acquisition, and trust [27]. In the BIT formalism, the trust operator is interpreted using neighborhood semantics [32]. The logic is provided with a rigorous semantics to precisely characterize 1) the relationships among beliefs and information acquisition, and 2) how different trust properties are represented by considering various axioms of the logic. In a related work, Demolombe and Lorini [11,31] have focused on analyzing trust in various features of information sources. That is, a certain agent is trusting another agent if the former believes that the information transmitted to them is reliable. In particular, in [31], the authors formalized some security properties and their relationships with trust such as integrity, availability and privacy by proposing a modal operator of obligation. Fuchs and colleagues [21] also addressed trust in the context of computer security. More recent proposals have made the link between trust and argument-based frameworks [3,34,39]. However, the above mentioned models are not suitable for verification mechanisms using model checking techniques because of their reliance on the internal structure of the interacting agents. Practically, the fact that MASs are deployed in open environments means that these agents are managed by different providers using different types of platforms. Thus, it is very difficult for one agent to completely trust others or to make assumptions about their internal states. Moreover, model checking neighborhood semantics-based modal logics is yet to be solved [17,33].
The closest approach to our work is the one presented by Singh in [37] where the social perspective of trust has been put forward. Specifically, the author provided a formal semantics for trust with various logical constraints used to reason about trust from an architectural point of view. This logical model combines temporal modalities of linear temporal logic (LTL) [35], modality C for commitments [36] and modality T for trust. Yet, unlike our approach that is based on interpreted systems structure with a grounded semantics, Singh's logic is interpreted using neighborhood semantics [32] whose model checking is still an open problem [17].
From the model checking point of view, some authors adopt a direct method, which can be performed by either developing a proper model checker from scratch or by extending existing tools with new algorithms for the needed temporal modalities. For instance, in our previous work [13], we proposed a new logic-based framework for specifying and model checking preconditional trust in MASs. We introduced TCTL, a branching temporal logic of preconditional trust interpreted in a new vector-based version of interpreted systems that captures the trust relationship between the interacting parties. Reasoning postulates and new symbolic model checking algorithms are presented to formally specify and automatically verify the system under consideration against some desirable properties expressed in TCTL. Thus, a new model checker extending MCMAS, called MCMAS-T, dedicated to TCTL, along with its new input language VISPL (Vectorextended ISPL) have been created. However, TCTL is restricted to preconditional trust and does not support conditional trust, and the symbolic model checking algorithms, although efficient with flat models, showed limited efficiency when the verified models are not flat (i.e., include non-self loops). In this paper, in addition to the introduction of conditional trust, we investigate a different verification mechanism that does not suffer from the non-flat-models limitation. This has been achieved thanks to the high efficiency of CTL model checking to which the model checking of TCTL and conditional trust is transformed.
Another relevant work is presented by Aldini in [2], where a formal framework to evaluate the effectiveness and robustness of trust-based models in order to detect and then isolate different kinds of attacks has been introduced. Indeed, the author integrates trust modeling with distributed systems. In this work, the system properties are expressed using a trust temporal logic (TTL) which combines CTL [19] and its action-based extension (ACTL) [9]. Moreover, the trust system model is based on an instance of both labeled transition systems and Kripke structures. The verification of temporal logic properties expressed in TTL has been performed through a mapping to an existing model checking technique. However, the model mapping between the two logics has not been specified and TTL can only specify a single agent model, and it is not adapted to autonomous MASs. El-Qurna et al. presented a model checking framework to verify service trust behaviors model against regular and non-regular properties [18]. The authors introduced an algorithm to generate a configuration graph of a deterministic pushdown automata (PDA), where the trust behaviors are captured through the observations sequences related to certain interactions between the services and users. The trust behavior properties are specified using Fixed point Logic with Chop (FLC). From the model checking prospective, a symbolic FLC model checking algorithm is applied in order to verify service trust behaviors with respect to trust properties. However, this approach lacks formal semantics for trust because trust formulae are inferred from the context free grammar of trust pattern languages. Moreover, the approach is not designed to formalize and verify trust in the context of MASs.
On the other hand, model checking trust can also be achieved by indirect techniques, also called transformation-based methods. The idea is to apply certain reduction rules in order to transform the problem at hand to an existing model checking problem. In fact, transformation has been acknowledged as an alternative mechanism for verifying various MASs aspects. The main advantage of this technique is that it enables the designers of MASs applications to get benefit from powerful and already tested model checkers. This technique has been applied for model checking commitments [15], knowledge [29], and the interaction between knowledge and commitments [1,38]. To the best of our knowledge, our work is the first attempt that introduces and implements a full transformation technique for verifying trust specifications in MASs.
3 Trust and Temporal Logic -TCTL
In [13], we introduced TCTL, a temporal logic of trust that extends the Computation Tree Logic (CTL) [19] to enable reasoning about trust and time. The syntax and semantics of TCTL are as follows:
The syntax of TCTL is defined recursively as follows:
where ρ ∈ AP is an atomic proposition from the set of atomic propositions AP, E is the existential quantifier over paths, the formula EXϕ stands for "ϕ holds in the next state in at least one path"; EGϕ stands for "there exists a path in which ϕ holds globally", and the formula E(ϕ ∪ ψ) holds at the current state if there is some future moment for which ψ holds and ϕ holds at all moments until that future moment. EFϕ is the abbreviation of E(true ∪ ϕ). A, the universal quantifier over paths, can be defined in terms of the above as usual: AXϕ = ¬EX¬ϕ; AGϕ = ¬EF¬ϕ; and A(ϕ ∪ ψ) = ¬(E(¬ψ ∪ (¬ϕ ∧ ¬ψ)) ∨ EG¬ψ). The modality T p (i, j, ψ, ϕ) stands for "Preconditional Trust" and is read as "the truster i trusts the trustee j to bring about ϕ given that the precondition ψ holds". That is, we have the trust over the content given that the precondition is satisfied.
TCTL formula is interpreted over vector-based interpreted system formalism. [12] extended the original interpreted systems introduced by [20] to explicitly capture the trust relationship that is established between agents engaged in an interaction. The vector-based interpreted system is composed of:
agents in which each agent i ∈ Agt is described by:
-A non-empty set of local states L i , which represents the complete information that the agent can access at a particular time;
-A set of local actions Act i to model the temporal evolution of the system;
-A vector ν of size n , i.e., ν i 1×n , where n is the number of agents in the system at a given time, is associated with each local state l i ∈ L i . ( ν(i), ν( j), ..., ν(k) are the components of the vector ν i at local state l i (s)). The vector ν will be used later to define the trust accessibility relation (Definition 2). Indeed, the vector ν i represents the vision of agent i with regard to the trust of other agents.
-A local protocol ρ i : L i → 2 Act i assigning a list of enabled actions that may be performed by agent i in a given local state L i ;
-A local evolution function τ i is defined as: τ i = L i × Act i → L i , which determines the transitions for an individual agent i between local states;
• A set of global states s ∈ S that represent a snapshot of all agents in the system at a given time. A global state s is a tuple s = (l 1 . . . l n ). The notation L i (s) is used to represent the local state of agent i in the global state s;
• I ⊆ S is a set of initial global states for the system;
• The global evolution function of the system is defined as follows: τ : G × ACT −→ G, where ACT = Act 1 × . . . × Act n and each component a ∈ ACT is called a joint action, which is a tuple of actions;
• As in [20], a special agent e is used to model the environment in which the agents operate. e is modeled using a set of local states L e , a set of actions Act e , a protocol P e , and an evolution function τ e .
A model of trust generated from vector-based interpreted systems is a tuple M t = (S t , R t , I t , { i→ j |(i, j) ∈ Agt 2 },V t ), where:
• S t is a non-empty set of reachable global states for the system;
• R t ⊆ S t × S t is the transition relation;
• I t ⊆ S t is a set of initial global states for the system;
• i→ j ⊆ S t × S t is the direct trust accessibility relation for each truster-trustee pair of agents (i, j) ∈ Agt 2 defined by i→ j iff:
l i (s t )(ν i ( j)) = l i (s t )(ν i ( j)); s t is reachable from s t using transitions from the transition relation R t ;
• V t : S t → 2 AP t is a labeling function, where AP t is a set of atomic propositions.
As in [13], the intuition behind the relation i→ j is, for agent i to gain trust in agent j, the former identifies the states that are compatible with their trust vision with regard to the latter, i.e., where agent i is expecting that agent j is trustful. Specifically, this is obtained by comparing the element ν i ( j) in the local state l i at the global state s t (denoted by l i (s t )(ν i ( j))) with ν i ( j) in the local state l i at the global state s t (denoted by l i (s t )(ν i ( j))). Thus, the trust accessibility of agent i towards agent j (i.e., i→ j ) does exist only if the element value that we have for agent j in the vector of the local states of agent i for both global states is the same, i.e., l i (s t )(ν i ( j)) = l i (s t )(ν i ( j)). Finally, infinite sequences of states linked by transitions define paths. If π is a path, then π(i) is the (i + 1)th state in π.
Given the model M t , the satisfaction for a TCTL formula ϕ in a global state s t , denoted as (M t , s t ) |= ϕ, is recursively defined as follows: Excluding the trust modality, the semantics of TCTL state formulae is defined as usual (semantics of CTL, since the main component of TCTL is CTL). The state formula T p (i, j, ψ, ϕ) is satisfied in the model M t at s t iff (1) there exists a state s t such that s t = s t and s t i→ j s t , and (2) all the trust accessible states s t that are different from the current state s t satisfy the content of trust ϕ.
In [37], Singh propounds that trust must be conditional, meaning that trust should be expressed using antecedents and consequents. For example, a customer may trust a merchant as follows: "if I pay, then I trust the merchant will deliver the goods" [37]. Such a statement expresses the customer's expectation and the effect of this expectation on their future plans. Our preconditional trust modality that assumes the prior satisfaction of the precondition is different from conditional trust. Expressing conditional trust requires an extension of TCTL, and to distinguish the two languages, the extended one is called TCTL'. However, there is a logical relationship between preconditional and conditional trust. In fact, as our main objective in the paper is the verification of temporal trust, we will show how this logical relationship will be exploited to inaugurate a model checking procedure for conditional trust (see Section 4.3). The idea we aim to convey is that it is possible to decide if a given state, and thus a given model, satisfies a conditional trust formula by calling the model checking of TCTL. To show this, let us first introduce the syntax and semantics of conditional trust. From the syntax perspective, T c (i, j, ψ, ϕ) is read as "agent i trusts agent j about the consequent ϕ when the antecedent ψ holds". It is worth noticing that in the case of precondition trust, for the trust to take place between the interacting agents i and j, the condition ψ ∧ ¬ϕ must be satisfied in the current state s t to ensure that the precondition ψ holds before the trust content ϕ is brought about, while conditional trust requires the existence of at least one accessible state satisfying the antecedent ψ. This condition captures the intuition that the satisfaction of the antecedent is possible in some future. The semantics of T c (i, j, ψ, ϕ) is as follows: −(M t , s t ) |= T c (i, j, ψ, ϕ) iff s t |= ¬ϕ and ∃s t = s t such that s t i→ j s t and s t |= ψ, and ∀s t = s t such that s t i→ j s t and (M t , s t ) |= ψ, we have (M t , s t ) |= ϕ.
The non satisfaction of the consequent ϕ complies with the first postulate in [37] stating that when the consequent holds, the trust in this consequent is "completed and is, therefore, no longer active". The following proposition shows the logical link between conditional and preconditional trust:
The proof of this proposition is direct from the semantics and omitted for the reason of limited space. Furthermore, it is worth mentioning that conditional trust T c (i, j, ψ, φ ) is conceptually and semantically different from trust about conditions, which can be represented by T c (i, j, , ψ → φ ). An example of the former is "if the customer i pays the merchant j, then i trusts j will deliver the goods", while for the latter the example is: "the customer i trusts the merchant j about the fact that, if i pays, then j will deliver the goods" .
In this section, we first introduce a transformation-based approach to address the problem of model checking TCTL. In a nutshell, given a model M t representing a trust based MAS and a TCTL formula ϕ that describes the property that the model M t has to satisfy, the problem of model checking TCTL can be defined as verifying whether or not ϕ holds in M t , which is formally denoted by M t |= ϕ. In particular, we apply specific reduction rules to formally transform the problem of model checking TCTL into the problem of model checking CTL [19]. This provides a way to perform our implementation on NuSMV. Technically, our transformation method encompasses two stages. First, we apply a set of formal rules to transform vector-based transition systems into Kripke structures. Then, we transform TCTL formulae to CTL ones based on certain rules developed specifically for this purpose. Such a transformation is performed by developing two formal methods that provide accurate alignments between source and target models, and at the same time preserve TCTL semantics without losing the validity of the original model properties. This transformation is then extended to check conditional trust.
In this section, we start by recalling the definition of the CTL model needed for the transformation algorithm.
A CTL formula is interpreted over a Kripke Structure M c = (S c , R c , I c ,V c ), where:
• S c is a non-empty set of states for the system;
• R c ⊆ S c × S c is the transition relation;
• I c ⊆ S c is a set of possible initial global states for the system;
• V c : S c → 2 AP c is a labeling function that maps each state to the set of propositional variables AP c that hold in it.
Having presented the CTL model, the next step is to establish our transformation technique. Given a TCTL model
The algorithm takes as input a model M t (line 1) and outputs the transformed model M c (line 2). First, the corresponding model M c has the same set of system states and initial states (i.e., S c = S t ; I c = I t ). Thereafter, the algorithm initializes the set R c , and then the set V c (s) to be equal to the set V t (s) (i.e., at the beginning, states are labeled with the same atomic propositions). We define a new set of atomic propositions needed to represent the trust accessibility relation to capture the semantics of trust as follows X = {α i α j |(i, j) ∈ Agt 2 }. Thus, the set AP c is as follows: AP c = X ∪AP t . Moreover, the algorithm proceeds to transform transition and trust accessibility relations to constitute the transition relations in R c based on two conditions. The first condition checks if the states s t and s t have a transition relation in R t , then this relation becomes a transition relation in R c (lines 8 & 9). For the second condition, the algorithm iterates using for all . . . do to go through each truster-trustee pair of agents and checks if the current state s t has an accessible state s t using the accessibility relation i→ j and this state is different from the state itself, then the algorithm: (1) adds a new transition from the corresponding s c to the corresponding s c in R c if such a transition is not already in R c , and (2) a new atomic proposition is added into the label of s c for the interacting agents i and j in order to mark the accessible state (lines 12 & 13). Finally, the algorithm returns the transformed model M c after iterating over all the transitions. (1) if (s c , s c ) / ∈ R c then R c := R c ∪ {(s c , s c )} where s c = s t and s c = s t ;
13:
(2) V c (s c ) := V c (s c ) ∪ {α i α j } where s c = s t ;
14:
end for 16: end for 17: return M c ;
This section presents our method to formally transform any TCTL formula ϕ to a CTL formula f (ϕ) using a recursive transformation function f . The details of this method are illustrated in Algorithm 2. The transformation of the CTL fragment of TCTL is straightforward (lines 1-6). For the trust modality (line 7), the trust formula is transformed inductively into CTL according to the defined semantics as follows: the transformation of the formula ψ ∧¬ϕ should hold in the current state, there exists a path where next state satisfies the added atomic proposition α i α j , which captures the existence of an accessible state, and along all paths, the next states that satisfy the atomic proposition α i α j also satisfy the transformation of the trust content ϕ. The states s 1 , s 2 and s 4 are accessible from s 0 , while s 3 is not. Furthermore, the trust formula (T p (i, j, ψ, ϕ)) holds in s 0 (i.e., (M t , s 0 ) |= T p (i, j, ψ, ϕ)). According together to provide a trusted service which facilitates efficient claim settlement. The process starts when the policyholder phones the call center Europ Assist to notify a new claim. Thereafter, Europ Assist registers the information and assigns an appropriate garage to provide the repair service to the policyholder. It then notifies the insurance company AGFIL which checks whether the policy is valid or not, and it confirms the claim coverage. AGFIL then sends the claim details to Lee Consulting Services (Lee CS) which is responsible for managing the operation of this service. Lee CS normally appoints an assessor to conduct a physical inspection of damaged vehicle and checks vehicle repair estimates with the garage. When repairs are completed, the garage will issue an invoice to Lee CS which will check the invoice against the original estimate. Lee CS sends all invoices to AGFIL, which in turn finalizes the payment processes.
In the above scenario, the participating parties have to ensure that the trust relationships are established on one another to perform their task accordingly. Such relationships are formalized using our model of trust M t = (S t , R t , I t , { i→ j |(i. j) ∈ Agt2 },V t ). To verify the correctness of the AGFIL scenario at design time, we used the safety (something bad will never happen) and liveness (something good will eventually occur) properties expressed using our TCTL' logic. Such important properties have been widely investigated in different context; for instance, by [13,16,25]. Formally, the safety property ϕ 1 expresses the negation of the bad situation where the insurance company validates the policyholder claim, but the latter never establishes their trust towards the garage with regard to the vehicle repair. The liveness property ϕ 2 states that in all paths globally, it is always the case that if the policy holder reports an accident and their claim is valid, then eventually in all future computation paths, their trust towards the insurance company with regard to the claim payment will take place.
We also checked a liveness property, given by ϕ 3 , expressed as a conditional trust. The formula expresses the existence of a computation path where the repairer trusts AGFIL to pay for the repairs once AGFIL accepts the proposed estimate from the garage. ϕ 3 = EG(T c (Repairer, AGFIL, agreeEstimate, f ul f illRepairPayment)).
We have fully implemented the presented model checking algorithms in a Java toolkit1 that interacts automatically with the NuSMV model checker. We have verified the three properties in a parametric way in different models having different numbers of agents ranging from 6 to 30 2 . The results will be presented and discussed in the next section.
We encoded our model M t by considering the participating agents, the set of their local states and actions, the local protocol, the local evolution function, and the initial states for each agent. We also considered the accessibility relations between agents by encoding the vector variables, which give a particular agent the possibility to establish the trust towards other agents. We used the VISPL input language of the MCMAS T model checker introduced in [13]. Thereafter, we used our transformation tool to transform the VISPL model and formulae into the SMV model in order to be able to start the verification process using NuSMV. The experiments are conducted on AMD FX-8350 -8 Cores -4GHZ per core with 32 GB memory. To test the scalability of our algorithms, we report five experiments in Table 1, where we consider the number of agents (Agents#), the number of reachable states (States#), the transformation times of both models and formulae in milliseconds, and the average total time calculated based on the transformation and verification times. The experiments revealed that all the tested formulae are satisfied in our models. As shown in the table, the number of reachable states reflects the fact that the state space increases exponentially when the number of agent increases. Yet, it is clear that the transformation times of both the models and formulae increase only logarithmically with regard to the number of states. It is also worth noticing that the average total time increases polynomially with respect to the number of states.
to the semantics, we obtain (M t , s 0 ) |= ψ ∧ ¬ϕ , and there exists a state s such that s = s and s i→ j s , and all the trust accessible states s such that s = s satisfy ϕ (i.e., (M t , s 1 ) |= ϕ), (M t , s 2 ) |= ϕ, and (M t , s 4 ) |= ϕ)). Using the proposed transformation technique, the model M t is transformed into the CTL model M c of the right side (part b) as follows: the transition and accessibility relations in M t are transformed into transition relations in M c , and the atomic propositions α i α j are added to represent the accessibility relations. Moreover, each state formula in TCTL is transformed into a CTL formula using the transformation function f . Thus, the formulae T p (i, j, ψ, ϕ) and ψ ∧ ¬ϕ are transformed into f (T p (i, j, ψ, ϕ) and f (ψ) ∧ f (¬ϕ) in state s 0 , and for every path, the next state that satisfies the added atomic proposition (i.e., s 1 , s 2 , and s 4 ) also satisfies the transformation of the trust content ϕ.
Theorem 1 (Soundness and Completeness of the Transformation). Let M t and ϕ be respectively a TCTL model and formula and let M C and f (ϕ) be the corresponding model and formula in CTL. We have
where s c is the corresponding state of s t in M c .
Proof. We prove this theorem by induction on the structure of the formula ϕ. All the formulae are straightforward, except the trust formula: T p (i, j, ψ, ϕ). The first and second parts: ( f (ψ) ∧ f (¬ϕ)) capture the first condition of the semantics where the current state should satisfy ψ ∧ ¬ϕ. The third part (EX(α i α j )) captures the second condition, i.e., the existence of an state different from the current state since α i α j holds only in such accessible states (line 13 of Algorithm 1). Finally, the fourth part (AX(α i α j → f (ϕ))) captures the last condition in the semantics of the trust formula where all accessible states (those satisfying α i α j in M c ) should satisfy ϕ.
A similar approach to model checking TCTL can be used to model check conditional trust by transforming the conditional trust formula of TCTL' to a CTL formula as follows:
In this section, we introduce an alternative solution that uses the developed model checking algorithm of TCTL. The algorithm of model checking conditional trust (Algorithm 3) capitalizes on the equivalence shown in Proposition 1 (line 3). If T p (i, j, , ψ → ϕ) ∧ ¬T p (i, j, , ¬ψ) does not hold, then a transformation will be needed. Such a transformation works in all cases, but to be more efficient, the algorithm uses it only if the direct condition on line 3 fails. The transformation, which also exploits Proposition 1, introduces two fresh atomic propositions: µ and κ. µ holds in the current state (line 4) and in every state where ψ holds (line 7). Thus, if ¬T p (i, j, , ¬µ) holds (condition 1), then there is an accessible state different from the current state where ψ holds. κ does not hold in the current state, but holds in every state where ψ → ϕ holds. Consequently, if T p (i, j, ¬ϕ, κ) holds (condition 2), then ¬ϕ holds and all accessible states different from the current state satisfy ψ → ϕ. The algorithm returns true if the two conditions 1 and 2 hold (line 9), false otherwise (line 10). The following theorem is direct from the semantics of conditional trust and Proposition 1.
Theorem 2 (Soundness and Completeness of Algorithm 3). Algorithm 3 returns true iff (M t , s t ) |= T c (i, j, ψ, ϕ).
Algorithm 3: Model Check T c (i, j, ψ, ϕ) 1: Input: M t , s t , i, j, ψ, ϕ 2: Output: true if (M t , s t ) |= T c (i, j, ψ, ϕ); false otherwise 3: if (M t , s t ) |= T p (i, j, , ψ → ϕ) ∧ ¬T p (i, j, , ¬ψ) then return true; 4: V t (s t ) := V t (s t ) ∪ {µ}; 5: for all s t = s t 6:
j, , µ) then return true; 10: return false; 5 Experimental Results
To explain our approach, we use a standard industrial case study [40] that outlines the process by which auto insurance claims are handled by an insurance company, AGFIL. There are multiple parties involved in the AGFIL cooperation process: AGFIL, Policyholder, Europ Assist, Lee Consulting Services, Garage, and Assessor. The participating parties work