A Logical Framework for Trust-Related Emotions Electronic Communications of the EASST Volume 22 (2009) Proceedings of the Third International Workshop on Formal Methods for Interactive Systems (FMIS 2009) A Logical Framework for Trust-Related Emotions Jean-François Bonnefon, Dominique Longin and Manh-Hung Nguyen 15 pages Guest Editors: Michael Harrison, Mieke Massink Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST A Logical Framework for Trust-Related Emotions Jean-François Bonnefon1, Dominique Longin2 and Manh-Hung Nguyen3 1 bonnefon@univ-tlse2.fr University of Toulouse, CNRS, CLLE, France 2 Dominique.Longin@irit.fr University of Toulouse, CNRS, IRIT, France 3 Manh-Hung.Nguyen@irit.fr University of Toulouse, UPS, IRIT, France Abstract: Emotion and trust are two important concerns for the elaboration of inter- action systems that would be closer and more attractive to their users, in particular by endowing machines with the ability to predict, understand, and process emotions and trust. This paper attempts to construct a common logical framework for the rep- resentation of emotion and trust. This logical framework combines a logic of belief and choice, a logic of time, and a dynamic logic. Using this common framework, we identify formal relations between trust and emotions, for which we also provide behavioral validation. Keywords: Modal logic, emotions, trust, distrust 1 Introduction The rapidly growing field of affective computing aims at developing interaction systems that are closer and more attractive to their users, in particular by endowing machines with the ability to predict, understand, and process emotions (on the one hand), and trust (on the other hand). In this article, we introduce a unified logical approach to represent the cognitive structure of some emotions, of trust/distrust, and their relations at a formal level. We formalize the concepts of emotions as well as trust/distrust based on cognitive models proposed by cognitive psychologists. Regarding emotions, we draw on cognitive theories (for more detail, see [SSJ01]) which assume that emotions are closely tied to changes in beliefs and desires. We capitalize on psychological models that allow to recognize and distinguish emotions based on their decomposition in cognitive factors particularly the cognitive structure of emotion of Ortony et al. [OCC88], the cognitive patterns of emotion of Lazarus [Laz91] and the belief- desire theory of emotion (BDTE) [Rei09, Dre95]. Similarly, we attempt to adhere closely to cognitive definition of trust [CF01] and distrust [CFL08]. Although there are tight conceptual connections between emotion and trust [Lah01], and al- though there ware some separated formalization of the concepts of trust as the works of Herzig et al. [HLH+08], and the concepts of emotions such as the works of Adam et al. [AHL09] and Steunebrink et al. [SDM07b, SDM07a], there is not yet a common logic to represent them both. Our work aims at filling that gap by formally representing trust and emotions in a common logic; 1 / 15 Volume 22 (2009) mailto:bonnefon@univ-tlse2.fr mailto:Dominique.Longin@irit.fr mailto:Manh-Hung.Nguyen@irit.fr A Logical Framework for Trust-Related Emotions this common logic will enable us to lay bare the formal relations between trust and emotion. The logic we offer is a combination of the logic of beliefs and choices as the one of Herzig and Longin [HL04] (a refinement from Cohen and Levesque [CL90]), the logic of time (introduced by Arthur Prior [Pri57]), and dynamic logic introduced by Fischer and Ladner [FL79] and Harel et al. [HKT00]. This paper is organized as follows: Part 2 introduces the logical framework. Part 3 formalizes the cognitive structure of some emotions, Part 4 formalizes the cognitive structure of trust and distrust. Part 5 shows some formal relations in the effect of trust/distrust on the emotions, and provides behavioral validation for these relations. 2 Logical Framework Syntax. The syntactic primitives of our logic are as follows: a nonempty finite set of agents AGT = {i1, i2, . . . , in}, a nonempty finite set of atomic events EVT = {e1, e2, . . . , ep}, and a nonempty set of atomic propositions ATM = {p1, p2, . . .}. The variables i, j, k. . . denote agents. The expression i1:e1 ∈ AGT × EVT denotes an event e1 intentionally caused by agent i1 and e1 is thus called an “action”. The variables α , β . . . denote such actions. The language of our logic is defined by the following BNF : ϕ :=p | i:α -happens | ¬ϕ | ϕ ∨ ϕ | Xϕ | X−1ϕ | Gϕ | Beli ϕ | Choicei ϕ | GrdI ϕ where p ranges over ATM, i:α ranges over AGT × EVT , i:α -happens ranges over ATM for each i:α ∈ AGT ×EVT , and I ⊆ AGT . The classical boolean connectives ∧ (conjunction), → (material implication), ↔ (material equivalence), > (tautology) and ⊥ (contradiction) are defined from ¬ (negation) and ∨ (disjunction). i:α -happens reads “agent i is just about to perform the action α ”; Xϕ reads “ϕ will be true next instant”; X−1ϕ reads “ϕ was true at the previous instant”; Gϕ reads “henceforth, ϕ is true”; Beli ϕ reads “agent i believes that ϕ is true”; Choicei ϕ reads “agent i prefers that ϕ be true”; GrdI ϕ reads “ϕ is publicly grounded between the agents in group I” (It is nothing else than a standard common belief operator). We define the following abbreviations: i:α -done def = X−1i:α -happens (Defi:α -done) Happensi:α ϕ def = i:α -happens ∧Xϕ (DefHappensi:α ) Afteri:α ϕ def = i:α -happens → Xϕ (DefAfteri:α ) Donei:α ϕ def = i:α -done ∧X−1ϕ (DefDonei:α ) Proc. FMIS 2009 2 / 15 ECEASST Fϕ def = ¬G¬ϕ (DefF) Goali ϕ def = Choicei FBeli ϕ (DefGoali ) Intendi α def = Choicei Fi:α -happens (DefIntendi ) Capableiα def = ¬Afteri:α⊥ (DefCapablei ) Possibleiϕ def = ¬Beli ¬ϕ (DefPossiblei ) Awarenessiϕ def = X−1¬Beli ϕ ∧Beli ϕ (DefAwarenessi ) i:α -done reads “agent i has done action α ”; Happensi:α ϕ reads “agent i is doing action α and ϕ will be true next instant”; Afteri:α ϕ reads “ϕ is true after any execution of α by i”; Donei:α ϕ reads “agent i has done action α and ϕ was true at previous instant”; Fϕ reads “ϕ will be true in some future instants”; Goali ϕ reads “agent i has the goal (chosen preference) that ϕ be true”; Intendi α reads “agent i intends to do α ”; Capableiα reads “agent i is capable to do α ”; Possibleiϕ reads “agent i believes that it is possible ϕ ”; Awarenessiϕ reads “agent i has just experienced that ϕ is true”. Semantics. For temporal operators, we use a semantics based on linear time described by a sequence (or story) of time points. (This semantics is very close to CTL* [CES86]) A frame F is a 4-tuples 〈H, B, C , G 〉 where: H is a set of stories that are represented as sequences of time points, where each time point is identified by an integer z ∈ Z, a time point z in a story h is called a situation < h, z >; B is the set of all Bi such that Bi(h, z) denotes the set of stories believed as being possible by the agent i in the situation < h, z >; C is the set of all Ci such that Ci(h, z) denotes the set of stories chosen by the agent i in the situation < h, z >; G is the set of all GI such that GI (h, z) denotes the set of stories which are publicly grounded in the group I of agents, in the situation < h, z >. All the accessibility relations Bi are serial1, transitive2 and euclidean3. This semantic is com- pletely standard in epistemic logic (see [Hin62, GG06]) All the accessibility relations GI are serial, transitive and euclidean (This is similar to the operator group grounding introduced by Gaudou et al. [GHL06]). All the accessibility Ci are serial. Moreover, we impose for every z ∈ Z that: if h′ ∈ Bi(h, z) then Ci(h, z) = Ci(h′, z). It means that if an agent believes that the world h’ is possible from the world h, then the set of his/her preference worlds from h and h’ are the same. In other terms, the worlds an agent prefers and the ones that agent believes that s/he prefers are the same (briefly, the agent is conscious about his/her preferences, and s/he prefers what s/he believes that s/he prefers). A model M is a couple 〈F , V 〉 where F is a frame and V is a function associating each atomic proposition p with the set V (p) of couple (h, z) where p is true. Truth conditions are 1 for every w1 ∈ M , there is w2 such that w1Biw2 2 if w1Biw2 and w2Biw3, then w1Biw3 3 if w1Biw2 and w1Biw3, then w2Biw3 3 / 15 Volume 22 (2009) A Logical Framework for Trust-Related Emotions defined as follows: M , h, z |= p iff (h, z) ∈ V (p) M , h, z |= Xϕ iff M , h, z + 1 |= ϕ M , h, z |= X−1ϕ iff M , h, z − 1 |= ϕ M , h, z |= Gϕ iff M , h, z′ |= ϕ for every z′ ≥ z M , h, z |= Beli ϕ iff M , h′, z |= ϕ for every (h′, z) ∈ Bi(h, z) M , h, z |= Choicei ϕ iff M , h′, z |= ϕ for every (h′, z) ∈ Ci(h, z) M , h, z |= GrdI ϕ iff M , h′, z |= ϕ for every (h′, z) ∈ GI (h, z) Other truth conditions are defined as usual. Axiomatics. Due to our linear time semantics, the temporal operators satisfy the following principles: i:α -happens ↔Xi:α -done (1) Xϕ ↔¬X¬ϕ (2) ϕ ↔XX−1ϕ (3) ϕ ↔X−1Xϕ (4) Gϕ ↔ϕ ∧XGϕ (5) G(ϕ → Xϕ) →(ϕ → Gϕ) (6) Beli and Choicei operators are defined in a normal modal logic plus (D) axioms. Thus, if � represents a Beli operator or Choicei operator: ϕ �ϕ (RN�) �(ϕ → ψ) →(�ϕ → �ψ) (K�) �ϕ →¬�¬ϕ (D�) For example, axiom D� applied to operator Beli is DBeli , which is described as: Beli ϕ → ¬Beli ¬ϕ . (RN�) means that all theorems are believed (respectively: chosen) by every agent i; (K�) means that beliefs (respectively: choices) are closed under material implication for every agent i; (D�) means that beliefs (respectively: choices) of every agent i are rational: they cannot be contradictory. The Beli operators satisfy the following principles of introspection: Beli ϕ ↔Beli Beli ϕ (4Beli ) ¬Beli ϕ ↔Beli ¬Beli ϕ (5Beli ) that means that agent i is conscious of its beliefs and of its disbeliefs. The following principle follows from the semantical constraint between belief accessibility relation and choice accessibility relation, and from axiom (D�) for Beli : Proc. FMIS 2009 4 / 15 ECEASST Choicei ϕ ↔Beli Choicei ϕ (4BC) ¬Choicei ϕ ↔Beli ¬Choicei ϕ (5BC) that means that agent i is conscious of its choices and of its dischoices. The sound and complete axiomatization of GrdI operator is defined as the one of common belief operator (also called mutual belief), which is closed to the operator described in Walton and Krabbe [WK95], also introduced by Gaudou et al. [GHL06]: ϕ GrdI ϕ (RNGrdI ) GrdI (ϕ → ψ) →(GrdI ϕ → GrdI ψ) (KGrdI ) GrdI ϕ →¬GrdI¬ϕ (DGrdI ) GrdI ϕ →GrdIGrdI ϕ (4GrdI ) ¬GrdI ϕ →GrdI¬GrdI ϕ (5GrdI ) Axiom (RNGrdI ) means that every tautology is public ground. Axiom (KGrdI ) means that if ϕ is publicly grounded in I and that ϕ implies ψ then ψ is also publicly grounded in I. Ax- iom (DGrdI ) means that the set of grounded informations is consistent: it can not be the case that both ϕ and ¬ϕ are simultaneously grounded. The positive introspection axiom (4GrdI ) and neg- ative introspection axiom (5GrdI ) account for the public character of GrdI . From these collective awareness results: if ϕ has (resp. has not) been grounded then it is established that ϕ has (resp. has not) been grounded. Linear time semantics entail the following principles: Gϕ →Afteri:α ϕ (7) Happensi:α ϕ →After j:β ϕ (8) Afteri:α ϕ ↔¬Happensi:α¬ϕ (9) Axiom (7) describe the relationship between time and action: if henceforth ϕ is true then after every action α of every agent i, ϕ will be true. (Note that the converse is not valid: it is possible that ϕ be true after every action α of every agent i performed in a situation < h, z >, and that ϕ be false at time z′ > z.) As time is linear, actions are deterministic on a given history. Thus, axiom (8) reads: if agent i is just about to perform α after what ϕ will be true, then after every performance of every action β by every agent j, ϕ will be true. In other words, if action α leads to a time point where ϕ is true, then every action performed by every agent leads to this time point. Finally, axiom (9) means that Afteri:α and Happensi:α operators are dual operators. This property is fair with respect to dynamic logic [HKT00]. 3 Formalization of the cognitive structure of emotion In this section, we present the formalization of emotions, based on their cognitive structure as proposed by Ortony et al. [OCC88], Frijda [Fri86] as well as those of Reisenzei [Rei09] and Scherer et al. [Sch01]. 5 / 15 Volume 22 (2009) A Logical Framework for Trust-Related Emotions Joy/Distress. The cognitive structure of Joy consists of two main factors: (i) a proposition ϕ is desirable for agent i, and (ii) agent i just experienced that ϕ is the case. To formalize the first factor, we consider that agent i desiring ϕ means that i wants ϕ to be the case. So we formalize desire as a goal (chosen preference). Therefore, the first factor is potentially formalized as Goali ϕ , the second factor may be formalized as Beli ϕ . However, we assume that emotion is triggered at the moment when all its factors are fulfilled, and that its intensity then decreases with time [dS01, Fri86]. Accordingly, we include a time factor into most emotional formulas. Thus, the first factor of Joy in particular means that agent i now recalls that at the previous instant, s/he desired ϕ , until experiencing that ϕ was in fact true: Beli X−1Goali ϕ . It means that in order to be joyful, agent i must keep in mind his desire in the previous instant. Hereafter, we add this analysis for almost emotional formulas. The second factor means that agent i has just experienced that ϕ is true and did not previously know it: Awarenessiϕ . The same analysis applies to Distress, except that in the first factor of Distress, ϕ is unde- sirable for agent i, which we assume to mean that agent i desired ¬ϕ : Beli X−1Goali ¬ϕ . We accordingly formalize the concept of Joy and Distress: Definition 1 (Joy/Distress) Joyi ϕ def =Beli X −1Goali ϕ ∧Awarenessiϕ Distressi ϕ def =Beli X −1Goali ¬ϕ ∧Awarenessiϕ To illustrate the definition of Joy, we can say that an individual is joyful when he has just realized that he won the lottery (Awarenessman(win lottery)) with the trivial assumption that he had been desiring to win the lottery (Belman X−1Goalman (win lottery)). In contrast, to illus- trate the definition of Distress, we can say that an individual feels distress when she learns she has lost her job (Awarenesswoman(lost job)) assuming that she had the goal not to lose her job (Belwoman X−1Goalwoman ¬(lost job)). Hope/Fear. The cognitive structure of Hope consists of two factors: (i) a proposition ϕ is desirable for agent i, and (ii) agent i believes that ϕ may be true in the future. To formalize the first factor, we consider that ϕ is not true at the moment when i hopes for it: Goali ϕ . We interpret the second factor, as meaning that among all of possible future worlds, agent i believes that there is at least one world in which ϕ will be the case. In other terms, agent i does not believe that ϕ will be false in all of possible future worlds: PossibleiFϕ . If i believes that ϕ can never be the case in all of possible future worlds, then i has no ground for hope. The same analysis applies to Fear, except that ϕ is now undesirable for agent i: Goali ¬ϕ . We accordingly formalize the concept of Hope and Fear: Definition 2 (Hope/Fear) Hopei ϕ def =Goali ϕ ∧PossibleiFϕ Feari ϕ def =Goali ¬ϕ ∧PossibleiFϕ Proc. FMIS 2009 6 / 15 ECEASST For example, a debutante is hopeful about being asked to dance, for she thinks it is possi- ble (PossiblegirlF(being asked to dance)) and this is what she wants (Goalgirl (being asked to dance)). In contrast, an employee fears to be fired when he does not wish to be fired (Goalemployee ¬( f ired)) but believes it is a possibility PossibleemployeeF(to be fired)). Satisfaction/Disappointment. The cognitive structure of Satisfaction consists of three factors: (i) agent i desired a proposition ϕ , (ii) agent i used to believe that ϕ might be true in the near future, and (iii) agent i now experiences that ϕ is really the case. The first two factors mean that now, agent keeps in mind that at the previous instant, s/he desired ϕ and believed that ϕ could be true in the future (Beli X−1(Goali ϕ ∧PossibleiFϕ)) (cf. the analysis of the second factor of Hope). The last factor means that i now experiences that ϕ is true, but did not know it the previous instant (Awarenessiϕ ). The difference in the case of Disappointment is agent recalls that, in the previous instant, s/he desired ¬ϕ instead of ϕ , and s/he believed that ¬ϕ was possibly true in the future (Beli X−1(Goali ¬ϕ ∧PossibleiF¬ϕ)). We formalize Satisfaction and Disappointment as Definition 3 (Satisfaction/Disappointment) Satisfactioni ϕ def =Beli X −1(Goali ϕ ∧PossibleiFϕ)∧Awarenessiϕ Disappointmenti ϕ def =Beli X −1(Goali ¬ϕ ∧PossibleiF¬ϕ)∧Awarenessiϕ For example, when the debutante realizes that she is indeed asked to dance (Awarenessgirl (asked to dance)) she is satisfied. Were she not to be asked to dance (Awarenessgirl (not asked to dance)), she would feel disappointed. We can point out the relations between Satisfaction, Disappointment and Hope: Satisfactioni ϕ ↔Beli X−1Hopei ϕ ∧Awarenessiϕ (10) Disappointmenti ϕ ↔Beli X −1Hopei ¬ϕ ∧Awarenessiϕ (11) The relation between Satisfaction and Joy can be formalized as Proposition 1: if we feel satisfaction about something, then we will also feel joy about it. Proposition 1 (Satisfaction implies Joy) Satisfactioni ϕ →Joyi ϕ Fear-confirmed/Relief. The cognitive structure of Fear-confirmed consists of three factors: (i) a proposition ϕ was undesirable for agent i, (ii) agent i believed that ϕ might be true in the near future, and (iii) agent i now experiences that ϕ is really true. We use the same analysis as for Satisfaction, except agent recalls that in the previous instant, ¬ϕ was desirable for agent i (Beli X−1Goali ¬ϕ ). The difference in the case of Relief is agent recalls that, in the previous instant, s/he desired ϕ (Beli X−1Goali ϕ ), and believed that ¬ϕ might be true in the near future (Beli X−1(Goali ϕ ∧ PossibleiF¬ϕ)). We formalize Fear-confirmed and Relief as: 7 / 15 Volume 22 (2009) A Logical Framework for Trust-Related Emotions Definition 4 (Fear-confirmed/Relief) FearConfirmedi ϕ def =Beli X −1(Goali ¬ϕ ∧PossibleiFϕ)∧Awarenessiϕ Reliefi ϕ def =Beli X −1(Goali ϕ ∧PossibleiF¬ϕ)∧Awarenessiϕ For example, the employee’s fear of being fired is confirmed when he learns that he is indeed about to be fired (Awarenessemployee( f ired)) which he had been afraid of (Belemployee X−1(Goalemployee ¬( f ired) ∧ PossibleemployeeF( f ired))). In contrast, were he to learn that he is not going to be fired (Awarenessemployee(not fired)), he would feel relief. We can also point out the relations between Fear-confirmed, Relief and Fear: FearConfirmedi ϕ ↔Beli X−1Feari ϕ ∧Awarenessiϕ (12) Reliefi ϕ ↔Beli X−1Feari ¬ϕ ∧Awarenessiϕ (13) The relation between Fear-confirmed and Distress is stated in Proposition 2: if our fears about something are confirmed, then we feel distressed. Proposition 2 (Fear-confirmed implies Distress) FearConfirmedi ϕ → Distressi ϕ 4 Formalization of Trust We now present the formalization of trust and distrust based on the cognitive definition of Castel- franchi and colleagues [CF01, CFL08]. Trust. We formalize the concept of trust based on Castelfranchi and Falcone’s definition [CF01] of trust in action which says that agent i trusts agent j to ensure ϕ by performing action α if and only if agent i desires to achieve ϕ (Goali ϕ ), and agent i expects that: (i) ϕ can be achieved by doing action α (Beli After j:α ϕ ); (ii) agent j is able to perform action α (Beli Capable jα ); and (iii) agent j has the intention to do such an action (Beli Intend j α ). However, these three factors are only necessary conditions, but not sufficient ones. For ex- ample, imagine that a robber wants to steal something located on the second floor of a mansion. There is a nurse on the first floor. The robber desires that the nurse stays where she is, because it makes his robbery possible. He also believes that it is possible that the nurse will stay where she is, and that it is actually her intention. Thus, the three conditions are satisfied, but we are reluc- tant nonetheless to say that the robber trusts the nurse to stay where she is in order to allow for his stealing, because there is no agreement between the nurse (trustee) and the robber (trustor). So here we need to add another condition for trust: an agreement between trustor and trustee that the trustee will perform such an action (GrdItrustee : α -happens), where I = {trustor,trustee}. We accordingly formalize the concept of trust as: Proc. FMIS 2009 8 / 15 ECEASST Definition 5 (Trust) Trusti, j(α, ϕ) def =Goali ϕ ∧Beli After j:α ϕ ∧Beli Capable jα∧ Beli Intend j α ∧Grd{i, j} j:α -happens For example, a boss trusts his secretary to prepare a report in order to present it at a company meeting because the boss desires the report (Goalboss (report)), and in his opinion, the report can be possibly ready after the secretary prepares it (Belboss A f tersecretary:prepare(report)), the secretary has the ability and intention to prepare the report (Belboss Capablesecretary(prepare)∧ Belboss Intendsecretary (prepare))). It is clear that in the relation between the boss and his secre- tary, there is an agreement that the secretary will prepare the report in time (Grdboss,secretarysecretary : prepare-happens). Distrust. We also adopt the definition of distrust given by Castelfranchi et al. [CFL08] which says that agent i distrusts agent j to ensure ϕ by performing action α if and only if agent i desires to achieve ϕ (Goali ϕ ), and agent i believes that at least one of these conditions is fulfilled: (i) agent j is not in the capacity to do action α : Beli ¬After j:α ϕ , or (ii) agent j is able to do α but he has not intention to do α : PossibleiAfter j:α ϕ ∧Beli ¬Intend j α . We accordingly formalize this concept as: Definition 6 (Distrust) DisTrusti, j(α, ϕ) def = Goali ϕ ∧(Beli ¬After j:α ϕ∨ (PossibleiAfter j:α ϕ ∧Beli ¬Intend j α)) For example, in spite of desiring the report (Goalboss (report)), the boss does not trust a new employee to prepare it because he believes the new employee is unable to perform that task(Belboss ¬Afteremployee:prepare(report)). From this definition, we can decompose the concept of distrust based only on the ability of trustee: Definition 7 (Distrust based on ability) C-DisTrusti, j(α, ϕ) def =Goali ϕ ∧Beli ¬After j:α ϕ 5 Trust-Related Emotions 5.1 Formal Relations Trust and Hope. Trust and Hope have an important relation because they both feature a pos- itive expectation [CF01]. When i trusts j, i has a positive expectation about j’s power and performance. Hope also implies some positive expectation. The greater the expectations, the deeper the trust; and, conversely, the deeper the disappointment when expectations are unreal- ized [Bry07]. We formalize the former relation as Proposition 3, the latter as Proposition 5. 9 / 15 Volume 22 (2009) A Logical Framework for Trust-Related Emotions Proposition 3 (Trust implies Hope) Trusti, j(α, ϕ) →Hopeiϕ This means that when we trust someone about an action that will bring some results, we are hopeful that the results will be obtained. For example, in a commercial transaction, when the buyer trusts his seller to send him a product after payment (Trustbuyer,seller(send, receipt)), he will be hopeful that he will receive the product (Hopebuyer receive product). This proposition will be proved by applying Lemma 1: if we believe that ϕ is true after every execution of action α , and that someone is able to do α , then we believe that there is at least a future world in which ϕ is true. Lemma 1 Beli After j:α ϕ ∧Beli Capable jα →PossibleiFϕ Once we trust someone to do an action to bring us something, we hope for the positive result of the action. In case of success, we feel satisfaction (formalized as Proposition 4). Conversely, in case of failure, we feel disappointment (formalized as Proposition 5). Proposition 4 (Successful Trust implies Satisfaction) Beli Done j:α Trusti, j(α, ϕ)∧Awarenessiϕ →Satisfactioniϕ This means that when we believe that what we trusted has now occurred, we are satisfied about it. For example, when the boss trusted his secretary to prepare the report (Donesecretary: prepareTrustboss,secretary(prepare, having report)), and on the morning of the day after, he has received the report (Belboss having report), then he is satisfied (Satisfactionbosshaving report). This proposition has a corollary which is deduced from Proposition 1 and 4: When we experience that what we trusted has really occurred, we will also feel joy about it. Corollary 1 Beli Done j:α Trusti, j(α, ϕ)∧Awarenessiϕ →Joyiϕ Proposition 5 (Unsuccessful Trust implies Disappointment) Beli Done j:α Trusti, j(α, ϕ)∧Awarenessi¬ϕ →Disappointmenti¬ϕ This means that we feel disappointed if what we trusted does not in fact occur. For example, a businessman trusted his partner to arrive on time to negotiate a contract. The businessman feels disappointed if the partner has not yet arrived at the scheduled time. DisTrust and Fear. Distrust features a negative expectation, involving fear of the other [LW00, AACS08]. We state the relation between Distrust based on ability and Fear as Proposition 6. Proc. FMIS 2009 10 / 15 ECEASST Proposition 6 (DisTrust implies Fear) C-DisTrusti, j(α, ϕ) →Feari¬ϕ This means that if we distrust someone to do an action to bring us something then we fear that our desire might not be fulfilled. For example, the boss might distrust his assistant with the preparation of a report he needs, and more specifically distrusts him to finish the report by the next morning (DisTrustboss,assistant ( f inish, report)). Therefore, he is fearful that he might miss the report the next morning (Fearboss¬report). This proposition will be proved by applying Lemma 2: if we believe that someone is unable to do an action to bring about something, then we believe that there is at least a future world without the expected result of this action. Lemma 2 Beli ¬After j:α ϕ →PossibleiF¬ϕ Once we distrust someone to do an action to bring about something, we experience fear. If the results are indeed negative, we feel fear-confirmed (formalized as Proposition 7). If, however the action is in fact successfully performed, we feel relief (formalized as Proposition 8). Proposition 7 (Confirmation of DisTrust implies Fear-confirmed) Beli Done j:α C-DisTrusti, j(α, ϕ)∧Awarenessi¬ϕ →FearConfirmedi¬ϕ If the boss realizes that his assistant really did not finish the report (Belboss ¬report), he feels fear-confirmed (FearConfirmedboss¬report). Combining the two Propositions 2 and 7, we arrive at a corollary: when we experience that what we distrusted has now happened, we feel distressed about it. Corollary 2 Beli Done j:α C-DisTrusti, j(α, ϕ)∧Awarenessi¬ϕ →Distressi¬ϕ Proposition 8 (Non-confirmation of DisTrust implies Relief) Beli Done j:α C-DisTrusti, j(α, ϕ)∧Awarenessiϕ →Reliefiϕ If the boss discovers that his assistant did in fact finish the report (Belboss report), he feels relieved (Reliefbossreport). 5.2 Behavioral validation Although the propositions that we proved in the previous section are intuitively plausible, some of them have not yet received behavioral validation from the field of experimental psychology. We decided to collect empirical data concerning three propositions in this article, related to the emotions that follow trust when it is confirmed (Proposition 4), and when it is unconfirmed (Proposition 5); and the emotions that follow distrust, when it is unconfirmed (Proposition 8) 4. 4 We could not test Proposition 7 for a linguistic reason: Neither in French nor in Vietnamese (the two languages used in our experiment) could we find an everyday term equivalent to ‘fear confirmed’. 11 / 15 Volume 22 (2009) A Logical Framework for Trust-Related Emotions Satisfaction Relief Disappointment Trust Distrust Trust Distrust Trust Distrust Success 4.9 (1.5) 4.6 (1.6) 2.8 (1.9) 3.6 (1.9) 1.1 (0.6) 1.3 (0.8) Failure 1.1 (0.5) 1.4 (1.0) 1.3 (1.0) 1.3 (0.9) 4.6 (1.7) 3.2 (1.4) Table 1: Mean and standard deviations of affective ratings, as a function of Trust and Outcome. Following the analysis in (Section 4) which argues that trust is the conjunction of the intention, the capacity, and the agreement of trustee, the presence of Agreement is intentionally fixed for the future test. We therefore operationalize Trust as the conjunction of Intention and Capacity, and Distrust as the three remaining cases. Participants to the survey read 8 different stories, fol- lowing a 2×2×2 within-subject design. The variables manipulated in the stories were Intention (Yes/No), Capacity (Yes/No), and Outcome (Success/Failure). As an example, here is the story corresponding to Intention = Yes, Capacity = Yes, and Outcome = Success. Mr. Boss is the marketing director of a big company. He needs an important financial report before a meeting tomorrow morning, but he has no time to write it because of other priorities. He asks Mr. Support to prepare it and put it on his desk before tomorrow morning. • Mr. Boss believes that Mr. Support has the intention to prepare the report in time. • Mr. Boss believes that Mr. Support is able to prepare the report in time. The morning after, Mr. Boss finds the report on his desk when he arrives. In your opinion, what does he feel? In the condition Intention = No, “Mr. Boss believes that Mr. Support has the intention to prepare the report in time” was replaced with “Mr. Boss believes that Mr. Support has no intention to prepare the report in time.” In the condition Capacity = No, “Mr. Boss believes that Mr. Support is able to prepare the report in time” was replaced with “Mr. Boss believes that Mr. Support is unable to prepare the report in time.” Finally, in the condition Outcome = Failure, “Mr. Boss finds the report on his desk when he arrives” was replaced with “Mr. Boss does not find the report on his desk when he arrives.” After reading each story, participants rated the extent to which the main character would feel each of 7 emotions, which included our target emotions, satisfaction, disappointment, and relief; but also some emotions that we included for exploratory purposes, such as anger or thankfulness. Ratings used a 6-point scale anchored at Not at all and Totally. A total of 100 participants took part in an online survey. The survey was offered in two languages, French (30% of the final sample) and Vietnamese (70%). Language was entered as a control variable in all statistical analyses, but added only a small overall main effect on participants’ responses, and will not be discussed any further. Descriptive statistics are displayed in Table 1. Participants’ responses were analyzed by means of a repeated-measure analysis of variance, aimed at detecting statistically reliable effects of Trust and Outcome on our emotions of interest. Satisfaction. Unsurprisingly, the analysis of variance detected a huge effect of Outcome, F(1, 98) = 597, p < .001, accounting for most of the observed variance, η 2p = .86. In other terms, Proc. FMIS 2009 12 / 15 ECEASST Satisfaction is almost perfectly predicted by Outcome alone. The analysis, however, also detects a comparatively small interaction effect Outcome × Trust, F(1, 98) = 8.8, p < .01, η 2p = .08, reflecting the fact that success is even more pleasant in case of trust. Table 1 shows that the biggest score of Satisfaction is in the case of Trust follows a Success: M = 4.9, SD < 1.5. The data are in line with what was expected from Proposition 4. Relief. The analysis detected main effects of Trust, F(1, 98) = 19.1, p < .001, η 2p = .23; and Outcome, F(1, 98) = 127, p < .001, η 2p = .80. However, these main effects were qualified by an interaction effect Trust × Outcome, F(1, 98) = 12.3, p < .001, η 2p = .31. Table 1 shows that the score of Relief is especially high in the case of Success is obtained despite of Distrust: M = 3.6, SD < 1.9. This interaction reflects our expectation (Proposition 8). Disappointment. The analysis detected main effects of Trust, F(1, 98) = 28.4, p < .001, η 2 p = .16; and Outcome, F(1, 98) = 389, p < .001, η 2 p = .56. However, these main effects were qualified by an interaction effect Trust × Outcome, F(1, 98) = 44.7, p < .001, η 2p = .11. Table 1 shows that the score of Disappointment is especially high in the case of Failure is obtained despite of Trust: M = 4.6, SD < 1.7. This interaction reflects our expectation (Proposition 5). 6 Conclusion This paper introduced a logical framework that can represent the cognitive structure of emotions, trust, and the formal relations between them. In other terms, it enables to represent the effect of trust (and distrust) on emotions. Furthermore, this logical framework respects the instantaneity of emotions that previous logics of emotions did not fulfill. Finally, the formal relations between emotion and trust laid bare by the logical framework were subjected to a behavioral validation following the methods of experimental psychology. The success of this behavioral validation gives strong support to our approach, which is shown to capture lay users’ intuitions about trust- related emotion. Although we have added time factor into almost emotional formulas, which enables to elim- inate rightly emotion when the relevant event has passed a long time, but it have not yet helped us to represent the nature of continuous intensity of emotions. Additionally, this paper has formalized only the effect of trust/distrust on emotions but not yet the effect of emotions on trust/distrust. These current limitations are also the potential perspective for our future research. Acknowledgements: This work has been supported by the Agence Nationale de la Recherche (ANR), contract No. ANR-08-CORD-005-1, and by a doctoral scholarship awarded by the Uni- versity of Toulouse, contract No. 26977-2007. Bibliography [AACS08] P. Aghion, Y. Algan, P. Cahuc, A. Shleifer. Regulation and Distrust. SUS.DIV– CEPR–PSEConference of Models of Cultural Dynamics and Diversity, 2008. 13 / 15 Volume 22 (2009) A Logical Framework for Trust-Related Emotions [AHL09] C. Adam, A. Herzig, D. Longin. A logical formalization of the OCC theory of emo- tions. Synthese 168(2):201–248, 2009. [Bry07] H. J. Bryce. Formalizing Civic Engagement: NGOs and the Concepts of Trust, Struc- ture, and Order in the Public Policy Process. Workshop on Building Trust Through Civic Engagement and for the International Political Science Association, Section on Governance, conference on Government Crisis in Comparative Perspective, Seoul, Korea, 2007. [CES86] E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatic verification of finite-state con- current systems using temporal logic specifications. ACM Transactions on Program- ming Languages and Systems 8(2):244–263, 1986. [CF01] C. Castelfranchi, R. Falcone. Social Trust: A Cognitive Approach. In Castelfranchi and Tan (eds.), Trust and Deception in Virtual Societies. Pp. 55–90. Kluwer Aca- demic Publishers, Dordrecht, 2001. [CFL08] C. Castelfranchi, R. Falcone, E. Lorini. A non-reductionist Approach to Trust. In Goldbeck (ed.), Computing with Social Trust. Pp. 45–72. Springer, Berlin, 2008. [CL90] P. R. Cohen, H. J. Levesque. Intention is choice with commitment. Artificial Intelli- gence 42:213–261, 1990. [Dre95] F. Dretske. Naturalizing the mind. MIT Press, Cambridge, 1995. [FL79] M. Fischer, R. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2):194–211, 1979. [Fri86] N. H. Frijda. The Emotions: Studies in Emotion & Social Interaction. Edition de la Maison des Sciences de l’Homme. Cambridge University Press, Paris, 1986. [GG06] P. Gochet, P. Gribomont. Epistemic Logic. In Gabbay and Woods (eds.), Twenti- eth Century Modalities. Handbook of the History of Logic 7, pp. 99–195. Elsevier, amsterdam edition, 2006. [GHL06] B. Gaudou, A. Herzig, D. Longin. A Logical Framework for Grounding-based Dia- logue Analysis. In Hoek et al. (eds.), International Workshop on Logic and Commu- nication in Multi-Agent Systems (LCMAS), Edinburgh, Scotland, UK, 01/08/2005. Electronic Notes in Theoretical Computer Science (ENTCS) 157(4), pp. 117–137. Elsevier, http://www.elsevier.com/, 2006. [Hin62] J. Hintikka. Knowledge and Belief: An Introduction to the Logic of the Two Notions. Cornell University Press, Ithaca, 1962. [HKT00] D. Harel, D. Kozen, J. Tiuryn. Dynamic Logic. MIT Press, 2000. [HL04] A. Herzig, D. Longin. C&L intention revisited. In Proceedings of Int. Conf. of knowl- edge representation and reasoning KR’04. Pp. 527–535. Morgan Kaufmann, 2004. Proc. FMIS 2009 14 / 15 ECEASST [HLH+08] A. Herzig, E. Lorini, J. F. Hübner, J. Ben-Naim, O. Boissier, C. Castelfranchi, R. De- molombe, D. Longin, L. Perrussel, L. Vercouter. Prolegomena for a logic of trust and reputation. In Proceedings of 3rd International Workshop on Normative Multiagent Systems (NorMAS). Luxembourg, July 2008. [Lah01] B. Lahno. On the Emotional Character of Trust. Journal of Ethical Theory and Moral Practice 4:171–189, 2001. [Laz91] R. S. Lazarus. Emotion & Adaptation. Oxford University Press, 1991. [LW00] R. Lewicki, C. Wiethoff. Trust, Trust Development, and Trust Repair. In Deutsch and Coleman (eds.), The Handbook of Conflict Resolution: Theory and Practice. Pp. 86–107. Jossey-Bass, San Francisco, CA, 2000. [OCC88] A. Ortony, G. L. Clore, A. Collins. The Congnitive Structure of Emotions. The Cam- bridge University Press, 1988. [Pri57] A. N. Prior. Time and Modality. Clarendon Press, Oxford, 1957. [Rei09] R. Reisenzein. Emotions as metarepresentational states of mind: Naturalizing the belief-desire theory of emotion. Cognitive Systems Research 10(1):6–20, 2009. [Sch01] K. R. Scherer. Appraisal Processes in Emotion : Theory, Methods, Research. Chap- ter Appraisal Considered as a Process of Multilevel Sequential Checking, pp. 92– 120. Oxford University Press, New York, 2001. [SDM07a] B. R. Steunebrink, M. Dastani, J.-J. C. Meyer. A Logic of Emotions for Intelligent Agents. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelli- gence, July 22-26, 2007, Vancouver, British Columbia, Canada. Pp. 142–147. AAAI Press, 2007. [SDM07b] B. R. Steunebrink, M. Dastani, J.-J. C. Meyer. Towards a Quantitative Model of Emotions for Intelligent Agents. In Reichardt and Levi (eds.), Proceedings of the 2nd Workshop on Emotion and Computing - Current Research and Future Impact. Osnabrück, Germany, 2007. [dS01] R. de Sousa. The Rationality of Emotion. MIT Press, 6 edition, 2001. [SSJ01] K. R. Scherer, A. Schorr, T. Johnstone. Appraisal Processes in Emotion: Theory, methode, Research. Series in Affective Science. Oxford university Press, 2001. [WK95] D. N. Walton, E. C. Krabbe. Commitment in Dialogue: Basic Concepts of Interper- sonal Reasoning. State University of New-York Press, NY, 1995. 15 / 15 Volume 22 (2009) Introduction Logical Framework Formalization of the cognitive structure of emotion Formalization of Trust Trust-Related Emotions Formal Relations Behavioral validation Conclusion