Formalizing Group and Propagated Trust in Multi-Agent Systems

1 Introduction

Trust is a crucial basis for the development of effective Multi-Agent System (MAS) applications. It has been extensively addressed in many research contexts (e.g., peerto-peer networks and grid computing). These researches are mainly placed under two major streams: trust computational models and logical trust formalization. The former measures the value of trust to compute the strength level in which an agent trusts other agents in order to establish future interactions [Wahab et al., 2018; Sardana et al., 2018; Nayak et al., 2019]. In this stream, trust was first formalized as a measurable concept in [Marsh, 1994]. Following this work, a number of trust models have been put forward and several proposals investigated trust propagation [Jamali and Ester, 2010; Chakraborty and Karform, 2012]. On the other hand, the latter deals with how one agent in the system can trust that another agent behaves and will perform an action in a certain way [Singh, 2011; Primiero and Raimondi, 2014; Primiero, 2016; Liu and Lorini, 2017; Drawel et al., 2020].

Trust is a complex concept that is hard to be precisely defined. Different meanings of trust have been given in various domains. In the context of MASs, [Castelfranchi and Falcone, 1998] defined trust as mental attitudes of the truster who believes that the trustee is capable to act and achieve a given goal. From logical point of view, modal logics have been used to reason about cognitive aspects of trust by many researchers. For instance, in [Herzig et al., 2012], the authors proposed a logical framework for the concept of trust where trust is basically expressed as a combination of different modalities based on the logic of action and time [Harel et al., 2000] and the BDI logic [Cohen and Levesque, 1990]. In [Liu and Lorini, 2017], the authors presented a new dynamic logic called DL-BET for reasoning about the interaction between belief, evidence and trust. Huang et al. [Huang et al., 2019] considered the setting of stochastic multi-agent systems, where an automated verification framework for quantifying and reasoning about cognitive trust is proposed. Moreover, some proposals have abstracted from the cognitive stance and presented trust as a direct modality. In [Drawel et al., 2020], a new branching temporal logic of preconditional trust, which extends the Computation Tree Logic (CTL) is introduced along with its model checking technique. [Singh, 2011] provided a formal semantics for trust with various logical postulates used to reason about trust from an architectural perspective. However, most of these approaches focus solely on individual trust that defines trust as a relationship that only involves two agents and is not propagated to other agents.

In this paper, we are interested in trust that goes beyond individuals where one individual agent trusts another agent, toward a group trust where a group of agents trusts a particular agent. We aim to capture the concepts of everyone trust and distributed trust toward a particular agent. Everyone trust is when all the members of the group agree on trusting another agent. Distributed trust is when the trust is distributed among the members of the group. We are also interested in trust that can propagate through the MAS from one agent to another. We are considering these two concepts from the logical perspective, in particular formalization, model checking and satisfiability problems.

A branching temporal logic extending CTL has been introduced to reason about trust and time in MASs [Drawel et al., 2017; Drawel et al., 2020]. This logic, called TCTL provides an interesting framework to reason about individual trust. However, we will show in this paper that this logic cannot be extended to accommodate group and propagated trust because of its limited expressive power. The logic fails to appropriately represent nested trust formulae. We will present a branching time temporal logic named BT that refines TCTL while being expressive enough to go beyond individual trust and include operators that express the concepts of everyone trust, distributed trust and propagated trust. Moreover, we will analyze the model checking and satisfiability problems of this logic using a sound reduction technique.

The paper is organized as follows. We first present the syntax and semantics of TCTL and discuss its limitation in Section 2. In Section 3, we introduce the Branching Trust Logic

(BT). The model checking and satisfiability problems of BT are addressed using a transformation procedure in Section 4. The complexity of these problems is analyzed in Section 5. In Section 6, we present the experimental results. We end by concluding the paper in Section 7.

2 Trust Computational Temporal Logic

2.1 Preliminaries

The semantics of TCTL formulae is interpreted using a model generated from the extended Interpreted System formalism introduced in [Drawel et al., 2017]. This formalism includes the notion of agents' vector ν to account for the interaction that occurs during the execution of MAS. That is, for all states s, s′ ∈ S and i, j ∈ Agt, a vector of size n is associated with each local state li ∈ Li of the n agents. The vector ν is used to define the trust accessibility relation ∼i,j. The idea is, the relation ∼i,j relates the states that are considered to be trustful from the vision of agent i with regard to agent j. Specifically, this is obtained by comparing the element ν i (j) in the local state li at the global state s (denoted by li(s)(ν i (j))) with ν i (j) in the local state li at the global state s′ (denoted by li(s′ )(ν i (j))). Thus, the trust accessibility of agent i toward agent j does exist between two global states 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.

Definition 1 (Model of TCTL). A model of trust is a tuple Mt = (S, I,R, {∼i,j |(i, j) ∈ Agt2 }, V )

where: S is a non-empty set of reachable global states for the system; I ⊆ S is a set of initial global states for the system; R ⊆ S × S is the transition relation; ∼i,j ⊆ S × S is the direct trust accessibility relation for each truster-trustee pair of agents (i, j) ∈ Agt2 defined by ∼i,j iff: (1) li(s)(ν i (j)) = li(s′ )(ν i (j)) and (2) s′ is reachable from s using transitions from the transition relation R; V : S → 2AP is a labeling function, where AP is a set of propositional variables.

Definition 2 (Syntax of TCTL). The syntax of TCTL is defined recursively as follows:

The CTL fragment formulae are defined as usual (see [Emerson, 1990]). The formula T(i, j, ϕ) called trust formula is read as "agent i trusts agent j to bring about ϕ".

Definition 3 (Semantics of TCTL). Given the model Mt, the satisfaction of a TCTL formula ϕ in a global state s, denoted as (Mt, s) |= ϕ, is recursively defined. The semantics of the CTL fragment is as usual [Emerson, 1990]. The semantics of the operator T is as follows:

The state formula T(i, j, ϕ) is satisfied in the model Mt at s iff ϕ does not hold in s and all the trust accessible states s′ that are different from the current state satisfy the content ϕ.

2.2 Discussion

Although TCTL has been presented with interesting reasoning postulates [Drawel et al., 2017; Drawel et al., 2020], a deep analysis of this logic reveals a major paradox resulted from the underlying assumption that complies with the first postulate in [Singh, 2011] stating that "when the content holds, the trust in this content is completed and is, therefore, no longer active". Indeed, enforcing the condition ¬ϕ to be satisfied in the current state s for the trust to take place yields the following paradoxical postulate:

which means if i trusts j about ϕ, then i trusts this agent that the first trust does not hold. The proof is straightforward since all accessible states satisfy ¬T(i, j, ϕ) because of the satisfaction of ϕ and the current state satisfies T (i, j, ϕ).

Therefore, this logic is not suitable to reason about trust properties that need nested trust formulae to hold. We present then a refined logic that does not have this postulate, so it can express nested formulae needed for propagated trust, everyone trust and distributed trust. In this logic, tautologies are trusted, but this is less important in practical scenarios.

3 Branching Trust Logic (BT)

Definition 4 (Syntax of BT). Let G ⊆ Agt be a group of agents and ρ a propositional variable from the set APb. The syntax of BT is defined recursively as follows:

The formula T represents trust and three notions of group and propagated trust: ET , DT , and PT . The formula ET refers to "Everyone trusts" and means that everyone in the group G trusts agent j to bring about ϕ. Technically, "Everyone trusts" can be seen as the conjunction of the individual trust of each agent in the group. Moreover, DT denotes "Distributed trust". That is, a group has its trust distributed among its member agents. Propagated trust PT indicates that a new trust relationship can be derived from preexisting agent's trust. BT formulae are evaluated over an extended Interpreted System Mb = (Sb, Ib, Rb, {∼i,j |(i, j) ∈ Agt2 }, Vb), which is the same as Mt.

The semantics of group and propagated trust is defined using new accessibility relations derived from the trust accessibility relation as follows.

Definition 5 (Group/Propagation Accessibility Relations). The group and propagation accessibility relations are:

- ∼EG,j = ⋃i∈G ∼i,j, i.e., the union of the trust accessibility relations between every agent of the group G and the agent j.

- ∼DG,j = ⋂i∈G ∼i,j , i.e., is the intersection of the trust accessibility relations between every agent in the group G and the agent j.

Definition 6 (Satisfaction). Given the model Mb, the semantics of trust and group trust operators is recursively defined as follows:

The following reasoning postulates hold in BT:

1. T(i, j1, T(j1, j2, ϕ)) ⇒PT (i, j2, ϕ)
2. PT (i, j1, T(j1, j2, ϕ)) ⇒PT (i, j2, ϕ)
3. T(i, j1, PT (j1, j2, ϕ)) ⇒PT (i, j2, ϕ)
4. PT (i, j1, PT (j1, j2, ϕ)) ⇒PT (i, j2, ϕ)
5. T(i1, j, ϕ) ∧ T(i2, j, ϕ⇒ψ) ⇒DT ({i1, i2}, j, ψ)
6. ∨ i∈G T (i, j, ϕ) ⇒ DT (G, j, ϕ)

The first four postulates capture the trust propagation among agents in one step (1st postulate) or many steps. The 5th and 6th postulates capture the properties of the distributed trust among the group members. The 7th postulate shows the everyone trust property.

4 Transformation Procedure

To address the model checking and satisfiability problems of BT, we introduce a transformation procedure [El-Menshawy et al., 2010] that allows us to leverage the model checking and satisfiability procedures of CTL [Emerson, 1990; Emerson and Halpern, 1985]. A transformation from TCTL model checking to CTL model checking has been attempted in [Drawel et al., 2018]. However, this approach does not capture the alignments between source and target models, which results in unsound transformations. Technically, the transformation algorithms for both the model and formulae overlook some critical cases. More precisely, the technique provided for the model consists of adding transitions to represent the accessibility relations, and so, it does not distinguish between original transitions in the original TCTL model and the transitions added in the CTL model. It turns out that some formulae with temporal operators EX and U become true in the transformed CTL model while they are false in the original TCTL model. Our procedure avoids these problems by capturing accessibility relations through distinguishable states and transitions using atomic propositions added in the transformed CTL formulae.

4.1 FromBTModel to CTLModel

In this section, we start by recalling the definition of the CTL model needed for the transformation algorithm.

Definition 7 (Model of CTL). A CTL formula is interpreted over a Kripke structure Mc = (Sc,Rc, Ic, Vc), where: Sc is a non-empty set of states for the system; Rc ⊆ Sc ×Sc is the transition relation; Ic ⊆ Sc is a set of possible initial global states for the system; and Vc : Sc → 2APc is a labeling function that maps each state to the set of CTL propositional variables APc holding in it.

Having presented the CTL model, the next step is to establish our transformation procedure. Given a BT model Mb = (Sb,Rb, Ib, {∼i,j |(i, j) ∈ Agt2 }, Vb), Algorithm 1 shows how this model, taken as input, is transformed into a CTL model Mc = (Sc,Rc, Ic, Vc) as output. Initially, the output model Mc has the same set of system states, initial states, transitions and valuation function as Mb (i.e., Sc = Sb; Ic = Ib; Rc = Rb; and Vc = Vb). Thus, at the beginning, the states of Mc are labeled with the same propositional variables as the states in Mb. We define a new set of fresh propositional variables Prop for the CTL logic needed to represent the trust accessibility relations to capture the semantics of trust operators. Moreover, we define a new atomic proposition χ for CTL that will be used to preserve the actual temporal transition relation by distinguishing the added states and transitions from the original ones in Mb. The set APc is then defined as the set APb augmented with χ and the propositional variables αij , αEj , αDj , and αPj for the individual, group, and propagated trust accessibility relations for all the agents i, j and groups G. The algorithm proceeds to transform the trust accessibility relations for all the agents. First, it checks if there is an accessibility relation between each pair of distinct states s and s′ . Based on the type of all the possible accessibility relations, it assigns a specific propositional variable to the set Prop. A new state s′′ is added to the set of system states Sc along with new transitions from s to s′′ and from s′′ to s′ in Rc. Further, the new state s′′ is labeled with χ and the atomic propositions in the set Prop in order to distinguish the states that are accessible from any other next state that satisfies the trust formulae without having accessibility to the current state. However, to avoid adding many states for different accessibility relations between the same two states, the algorithm checks if s′′ is already added for another accessibility relation. If s′′ already exists, the algorithm will only add the atomic propositions Prop to mark the accessible state for any other interacting agents. Finally, the algorithm returns the transformed model Mc after iterating over all the transitions.

Proposition 1 (Boundedness of Model Transformation). Let Mc be the model obtained from Mb using Algorithm 1 and |Mc| and |Mb| be the size of Mc and Mb respectively. |Mc| < 3|Mb|

Proof. Let |Ab| be the number of accessibility relations in Mb, i.e., |Ab| = |{∼i,j |(i, j) ∈ Agt2 }|. We have: |Mc| = |Sc| + |Rc| and |Mb| = |Sb| + |Rb| + |Ab|. In the worst case, each pair of distinct states (s, s′ ) ∈ Rb is connected by exactly one accessibility relation. Since each accessibility relation is translated into one state and two transitions in Mc, we obtain: |Mc| = |Sb| + |Rb| + 3|Ab|. In the general case, more than one accessible state might exist between each pair of states. Since the other accessibility relations benefit from Algorithm 1 Transform Mb = (Sb,Rb, Ib,∼i,j |(i, j) ∈ Agt2 }, Vb) into Mc = (Sc, Ic, Rc, Vc)

1: Sc := Sb; Ic := Ib; Rc := Rb; Vc := Vb; 2: for each (s, s′ ) ∈ S2 b s.t. s′ ̸= s and all i, j,G do 3: Prop := ∅; 4: if s ∼i,j s′ then Prop := Prop ∪ {αij }; 5: if s ∼EG,j s′ then Prop := Prop ∪ {αEj }; 6: if s ∼DG,j s′ then Prop := Prop ∪ {αDj }; 7: if s ∼Pi,j s′ then Prop := Prop ∪ {αPj } ; 8: if ∃s′′ s.t. (s, s′′ ), (s′′ , s′ ) ∈ Rc and χ ∈ Vc(s′′ ) then 9: Vc(s′′ ) := Vc(s′′ ) ∪ Prop; 10: else 11: Sc := Sc ∪ {s′′ }; Rc := Rc ∪ {(s, s′′ ), (s′′ , s′ )}; 12: Vc(s′′ ) := {χ} ∪ Prop; 13: end if 14: end for 15: returnMc;

the already added states and transitions, we obtain: |Mc| ≤ |Sb| + |Rb| + 3|Ab|. The result then follows.

4.2 FromBT Formulae to CTL Formulae

Algorithm 2 illustrates the formulae transformation function defined over the structure of the original BT formula. The function is recursive with the propositional variables of APb being the base case (APb ⊂ APc). For the temporal operators, we need to make sure that the transformation does not affect the CTL semantics. That is, since a new state and new transitions are added to the corresponding model Mc, we have to make sure that the path through which a formula is satisfied in the original model Mb is still satisfied in the corresponding path of the translated model Mc. Indeed, this is the main reason behind the conjunction of ¬χ for the temporal operators. This allows us to exclude the additional state and transitions when we consider the satisfaction of the formulae. For instance, the formula EXϕ is transformed into a CTL formula stating that there exist a path in the next state where the transformation of ϕ and the negation of the atomic proposition χ (added to represent the temporal transition) is true in this state. For the trust, group trust, and propagated trust modalities, each formula is transformed inductively into CTL according to the defined semantics as follows: along each path, if the next state on that path satisfies the corresponding atomic proposition (from the set Prop), then the next state of the added state also satisfies the transformation of the trust content ϕ. The state that satisfies the fresh propositional variable is the added state to capture the corresponding accessibility, which explains the double use of AX.

Proposition 2 (Boundedness of Formula Transformation). Let ϕ be a BT formula and f the transformation function defined in Algorithm 2. There exists a constant k such that |f(ϕ)| < k|ϕ|, where |ϕ| is the length of ϕ.

Proof. The proof is by induction on the structure of the formula.

• The result holds for the base case (atomic propositions).

Algorithm 2 Transform BT formula ϕ into CTL formula f (ϕ)

1: f(ρ) = ρ if ρ ∈ APb; 2: f(¬ϕ) = ¬f(ϕ); 3: f(ϕ∨ψ) = f(ϕ) ∨ f(ψ); 4: f(EXϕ) = EX(f(ϕ) ∧¬χ); 5: f(E(ϕ ∪ ψ)) = E((f(ϕ) ∧¬χ) ∪ (f(ψ) ∧¬χ)) ; 6: f(EGϕ) = EG(f(ϕ) ∧¬χ); 7: f(T(i, j, ϕ)) = AX(αij →AXf(ϕ)); 8: fET (G, j, ϕ) = AX(αEj →AXf(ϕ)); 9: fDT (G, j, ϕ) = AX(αDj →AXf(ϕ)); 10: fPT (i, j, ϕ) = AX(αPj →AXf(ϕ));

• For the formula φ = ¬ϕ, we have |f(φ)| = |f(ϕ)| + 1. Therefore, by assumption that the proposition holds for the formula ϕ, ∃k1 such that |f(φ)| < k1|ϕ| + 1. Since |ϕ| <|φ|, and |φ| > 1, we get |f(φ)| < (k1 + 1)|φ|, so the proposition.
• For the formula φ = EXϕ, we have |f(φ)| = |f(ϕ)| + 4. Therefore, by assumption that the proposition holds for the formula ϕ, ∃k1 such that |f(φ)| < k1|ϕ| + 4. Since |ϕ| <|φ|, and |φ| > 1, we get |f(φ)| < (k1 + 4)|φ|, so the proposition. The proof for EGϕ is similar.
• For the formula φ = E(ϕ ∪ ψ), we have |f(φ)| = |f(ϕ)|+|f(ψ)|+7. Thus. by assumption that the proposition holds for the formulae ϕ and ψ, ∃k1, k2 such that |f(φ)| < k1|ϕ|+k2|ψ|+7. Because |ϕ| <|φ|, |ψ| <|φ|, and |φ| > 1, we obtain |f(φ)| < (k1 + k2 + 7)|φ|. The proof for ϕ ∨ ψ is similar (k = k1 + k2 + 1).
• For the formula φ = T (i, j, ϕ), we have f(T (i, j, ϕ)) = AX(αij → AXf(ϕ)). Thus, |f(φ)| =|f(ϕ)| + 4, and by assumption that the proposition holds for the formula ϕ, ∃k1 such that |f(φ)| < k1|ϕ|+4. Since |ϕ| <|φ|, and |φ| > 1, we get |f(φ)| < (k1+4)|φ|, so the proposition. The proof is similar for the group and propagated trust formulae ET , DT , and PT .

Model Checking

Given a BT model Mb representing a MAS and a BT formula ϕ describing the property that the model Mb has to satisfy, the problem of model checking BT is the problem of verifying whether or not Mb |= ϕ. The introduced transformation procedure provides a solution to this problem, by simply calling the model checking procedures of CTL as stated by the following theorem.

Theorem 1 (BT Model Checking). Let Mb and ϕ be respectively a BT model and formula and let f (Mb) and f (ϕ) be the CTL model and formula obtained via Algorithms 1 and 2. We have (Mb, s) |= ϕ iff (f(Mb), s) |= f(ϕ).

Proof. We prove this theorem by induction on the structure of the formula ϕ.

• For the propositional variables from the set APb, the result is straightforward (notice that APb ⊂ APc). The result is also direct for the negation and disjunction cases.

• For the formula φ = EXϕ, we have (Mb, s) |= EXϕ iff there exists an immediate successor to s where ϕ holds. Consequently, from the definition of f(Mb) and f(ϕ), we obtain (Mb, s) |= EXϕ iff (Mc, s) |= EX(f(ϕ) ∧ ¬χ). That is, we are excluding the new added path as this path will never be considered because next state (the added state) has χ and we are forcing ¬χ.
• For the formula φ = E(ϕ ∪ ψ), and from the definition of f, (f(ϕ) ∧ ¬χ) ∪ (f(ψ) ∧ ¬χ) captures the semantics of Until in CTL which states the existence of a path starting in the current state that satisfies (ϕ ∧ ¬χ) until reaching a state in which (ψ ∧ ¬χ) holds, where only original temporal transitions are considered.
• The trust formula: T(i, j, ϕ). AX(αij → AXf(ϕ)) captures the semantics of the trust formula where all accessible states (those satisfying αij inMc) should satisfy ϕ. The proof is similar for the group and propagated trust formulae.

Satisfiability

Given a BT formula ϕ, the satisfiability of BT is the problem of deciding if there exists a model Mb such that Mb |= ϕ. As for model checking problem, the transformation procedure provides also a solution for the BT satisfiability problem.

Theorem 2 (BT Satisfiability). Let ϕ be a BT formula and f(ϕ) the CTL formula obtained via Algorithm 2. We have ϕ is satisfiable iff f(ϕ) is satisfiable.

Proof. The right implication is direct from Theorem 1 because if there is a model Mb satisfying ϕ, then f(Mb) that satisfies f(ϕ) does exist. For the left implication, we can prove by induction on the structure of the formula that if there is a model Mc that satisfies f(ϕ), we can always find a model M ′c that satisfies the same formula where states satisfying fresh propositional variables from APc \ APb do not satisfy any other non-fresh propositional variable from APb. From M ′c we can construct a model Mb s.t. f(Mb) = M ′c

5 Complexity Analysis

In this section, we will first analyze the time complexity of model checking BT with regard to the size of the explicit model Mb and length of the formula to be checked. Since we are using symbolic model checking of CTL, we will also analyze the space complexity of model checking BT for concurrent programs [Kupferman et al., 2000] with respect to the size of the components of these programs and length of the formula. The complexity of the BT satisfiability problem will end this section.

As our approach is transformation-based, we start by analyzing the time complexity of transforming the BT model and formula with respect to explicit models, where all states and transitions are enumerated. Specifically, we prove that these two transformations are linear with respect to both the input BT model and the formula. The linear complexity of these two transformations entails the P-completeness of the BT model checking problem in explicit models. Given that, we proceed to analyze the space complexity of the BT model checking problem and prove its PSPACE-completeness with respect to concurrent programs where the model has the form of a synchronized product of agent programs. Indeed, our motivation behind considering the complexity of our model checking procedure for concurrent programs that provide compact representations of the systems to be checked is that in practice, existing model checking tools (e.g., MCMAS and NuSMV) do not support explicit representations where states and transitions are listed explicitly (as Kripke-like structures). In fact, only local states and transitions of each component are represented. Therefore, the actual system can still be represented by combining local states and transitions to build reachable states.

5.1 Model Checking Time Complexity

In this subsection, we will prove that model checking BT in explicit models is P-complete, so it can be done in a polynomial running time with respect to the size of the model and length of the formula.

Theorem 3 (Explicit BT Model Checking: Upper Bound). The BT model checking problem can be solved in time O(|Mb| × |ϕ|).

Proof. BT can be reduced to CTL, and it is known from [Clarke et al., 1999] that CTL model checking can be done in a linear time with respect to the size of the CTL model and formula, i.e., O(|f(Mb)| × |f(ϕ)|). From Proposition 1, |f(Mb)| < 3|Mb|, i.e., the size of f(Mb) is linear with the size of Mb. Moreover, from Proposition 2, the length of f(ϕ) is linear with the length of ϕ. Indeed, Algorithm 2 takes the BT formula ϕ as input and writes in a recursion manner the corresponding CTL formula according to the structure of ϕ. The time complexity of transforming the BT formula is linear with respect to the length of the input formula ϕ. This follows from the fact that (1) the length of the recursion is bounded by the size of the input formula ϕ, and (2) the size of f(ϕ) is bounded by the size of ϕ, so the theorem.

Theorem 4 (Explicit BT Model Checking: Completeness). The problem of BT model checking is P-complete.

Proof. Membership (i.e., upper bound) in P follows from Theorem 3. Hardness (i.e., lower bound) in P is a result of the polynomial reduction from model checking CTL proved to be P-complete [Schnoebelen, 2002].

5.2 Model Checking Space Complexity

In this subsection, we will prove that the complexity of BT model checking for concurrent programs is PSPACEcomplete. This result means that there is an algorithm solving the problem in polynomial space in the size of the components constituting concurrent programs and the length of the formula being model checked.

Theorem 5 (Polynomial Reduction of BT Model Checking: Upper Bound). Let ⊑psr denote the polynomial-space reduction. The problem of model checking BT can be reduced into the problem of model checking CTL in a polynomial space, i.e., MC(BT) ⊑psr MC(CTL).

Proof. The transformation of the BT model and BT formula into the corresponding CTL model and formula could be computed by a deterministic Turing Machine (TM) in space O(log n) where n is the size of the input BT model, and polynomial space w.r.t. the length of the BT formula. For the model, TM reads in the input tape a model of BT and produces in the output tape, one-by-one, the same states including the initial ones and the same valuations. Then, for the transitions (s, s′ ) in the input model, it writes one-by-one, the transitions in the set Rc. It also reads the accessibility relations ∼i,j between two given states in the input model oneby-one and for each one, it adds an intermediate state to the set Sc labeled with two fresh propositional variables: 1) αij that depends on the accessibility relation, and 2) χ, along with two transitions if such a state does not already exist; otherwise, only the propositional variable αij is added. The group and propagated accessibility relations are done in the same way. All these writing operations are clearly logarithmic in space because this transformation is done on-the-fly, step-bystep. Moreover, we showed in Proposition 2 that any BT formula is transformable into a CTL formula whose length is linearly bounded by the length of the input formula. All these recursive transformations are clearly polynomial space in the length of the input formula, so the theorem.

Theorem 6 (BT Model Checking for Concurrent Programs: Completeness). The space complexity of the BT model checking for concurrent programs is PSPACEcomplete with respect to the size of the components of these programs and the length of the formula.

Proof. Since model checking CTL is PSPACE-complete for concurrent programs [Schnoebelen, 2002], the lower bound of model checking BT is PSPACE as well. In fact, BT subsumes CTL as it integrates the CTL modalities and the trust modalities. The upper bound in PSPACE follows from Theorem 5, so the result.

5.3 Satisfiability Complexity

Theorem 7 (BT Satisfiability: Completeness). The BT satisfiability problem is EXPTIME-complete.

Proof. Membership. Using the result of Theorem 2, we can imagine an EXPTIME algorithm that solves the BT satisfiability problem as follows: 1) Transform the input BT formula ϕ to the CTL formula f(ϕ) using Algorithm 2. As mentioned in the proof of Theorem 3, this can be done in a linear time; 2) Call the algorithm to solve the satisfiability of f (ϕ) which can be done in EXPTIME [Emerson and Halpern, 1985]. Hardness. The hardness follows from the fact that BT subsumes CTL proven to be EXPTIME-complete [Emerson and Halpern, 1985].

6 Implementation and Experimental Results

To support the modeling and verification of BT logic for MASs, we implemented the transformation procedure and developed a tool that automatically: (i) transforms a given BT model and formulae to a valid CTL model and formulae; (ii) interacts with the NuSMV model checker in order to perform the verification process. For testing, we used the well-known ordering protocol that regulates the interaction between seller and buyer agents introduced in [Desai et al., 2005]. Our motivation is to formalize the protocol requirements using BT model Mb and by expressing a set of properties in BT logic in order to assess the scalability of our technique. We expressed a set of group and propagated trust properties. For example, the formula EF ET (Group, Seller,EF DeliverGoods), checks whether or not there exists a possibility that every member in the group trusts the seller for delivering the requested goods. We measured the transformation times of the models and formulae along with the verification time in seconds and memory usage in megabyte when running on a machine Intel(R) Core(TM) i7-6700 CPU - 3.40GHZ with 16 GB memory. We run our experiments with a number of agents ranging from 3 to 66. We considered different numbers of agents to achieve different levels of scalability that makes the problem complex enough to observe significant results. The verification results in Table1 reveal that the number of reachable states reflecting the size of the model increases exponentially with the number of agents, while the space increase is only polynomial. This confirms the PSPACE complexity result. Moreover, the execution time (i.e., the transformation time of both the models and formulae, and the time of the verification process) shows a clear polynomial increase up to 33 agents. After 33, the increase rate is much higher but still polynomial with the number of states, which is inline with the fact that PSPACE=APTIME.

7 Conclusion

The main contributions of the paper are: (1) a new logical language that allows us to express individual, group and propagated trust; (2) a sound transformation procedure that provides a solution of the model checking and satisfiability problems of the logic, along with their complexity analysis. The procedure has been fully implemented and the experiments conducted on a large case study reaching 2.38419e15 states confirmed the theoretical results. For future work, we plan to tackle the run-time verification to investigate the dynamic changes of agents' behavior and their impact on group trust.