A Logic for Reasoning about Counterfactual Emotions

1 Introduction

A major objective of AI is to develop interactive cognitive systems that are more attractive and closer to the users and that can be considered as believable interlocutors. In this perspective, a challenge for AI is to build artificial agents which are capable: to reason about emotions, to predict and understand human emotions, and to process emotions in reasoning and during their interaction with a human user. With the aim of creating a new generation of emotional interaction systems, the study of affective phenomena has become a "hot" topic in AI where the domain of Affective Computing [Picard, 1997] has emerged in the last few years.

Recently, some researchers have been interested in developing logical frameworks for the formal specification of emotions (see [Lorini and Castelfranchi, 2007; Meyer, 2006; Steunebrink et al., 2007; El-Nasr et al., 2000] for instance). Their main concern is to exploit logical methods in order to provide a rigorous specification of how emotions should be implemented in an artificial agent. The design of agent-based systems where agents are capable to reason about and to dis-

Franc¸ois Schwarzentruber

IRIT, Toulouse, France schwarze@irit.fr

play some kind of emotions can indeed benefit from the accuracy of logical methods.

Although the application of logical methods to the formal specification of emotions has been quite successful, there is still much work to be done in the field of computational and logical modeling of 'counterfactual emotions'. In line with psychological theories of 'counterfactual emotions', we use this term to denote those emotions such as regret which arise during 'counterfactual thinking', that is, when "[...] reality is compared to an imagined view of what might have been." [Kahneman and Miller, 1986, p. 136]. In other terms, counterfactual emotions are based on an agent's alteration of a factual situation and in the agent's imagination of an alternative situation that could have realized if something different was done [Roese et al., 2005].

The aim of our work is to advance the state of the art on computational modeling of emotions by providing a logic which supports reasoning about this kind of emotions. Our major concern here is to find a fair trade off between expressivity and complexity of the formalism. We want a logic which is sufficiently expressive to capture the fundamental constituents of counterfactual emotions and, at the same time, with good mathematical properties in terms of decidability and complexity. To this aim, we exploit a well-known logic called STIT [Belnap et al., 2001; Horty, 2001]. STIT logic has been proposed in the domain of formal philosophy in the nineties and, more recently, it has been imported into the field of theoretical computer science where its formal relationships with other logics for multi-agent systems have been studied (see [Broersen et al., 2006] for instance). It is a very suitable formalism to reason about counterfactual choices of agents and of groups of agents. Unfortunately, the version of STIT with agents and groups proposed in [Horty, 2001] has been recently proved to be undecidable [Herzig and Schwarzentruber, 2008]. In this work we study a decidable fragment of this logic which is sufficiently expressive for our purpose of formalizing counterfactual emotions.

The paper is organized as follows. In Section 2 we introduce a fragment of the version of STIT with agents and groups proposed in [Horty, 2001]. Differently from Horty's logic, we prove that this fragment is decidable. Section 3 is devoted to characterize in our STIT fragment counterfactual statements of the form "group J (or agent i) could have prevented χ to be true". These are indeed fundamental constituents of counterfactual emotions. In Section 4 we provide an extension of our STIT fragment with knowledge operators. This is a necessary step in order to capture the subjective dimension of the affective phenomena we intend to analyze. The last part of the paper (Section 5) is devoted to the formalization of two kinds of counterfactual emotions: regret and rejoicing.

2 A decidable fragment of STIT

STIT (the logic of "Seeing to it that") is a modal logic framework dealing with what agents and groups of agents do and can do. More precisely, STIT supports reasoning about the effects of actions of agents and groups, and about the capabilities of agents and groups to ensure certain outcomes. In [Belnap et al., 2001] the language of STIT without groups is studied: a complete axiomatization of STIT without groups is provided and the logic is proved to be decidable. The extension of STIT with groups has been proposed in [Horty, 2001]. Unfortunately, in [Herzig and Schwarzentruber, 2008] it has been proved to be undecidable.

We here introduce a decidable fragment of STIT with agents and groups called dfSTIT which is sufficiently expressive to formalize counterfactual emotions.

2.1 Syntax

Let n be a strictly positive integer. Let ATM be a countable set of atomic propositions and let AGT = {1, . . . , n} be a countable set of agents. The language LSTIT of the logic STIT with agents and groups proposed by Horty [Horty, 2001] is defined by the following BNF:

where p ranges over ATM and J over 2AGT . 〈J〉ϕ is an abbreviation of ¬[J]¬ϕ. Operators of type [J] are used to describe the effects of the action that has been chosen by J. If J is a singleton we refer to J as an agent, whereas if J has more than one element we refer to J as a group. We call joint actions the actions chosen by groups. If J has more than one element the construction [J]ϕ means "group J sees to it that ϕ no matter what the other agents in AGT \ J do". If J is a singleton {i} the construction [{i}]ϕ means "agent i sees to it that ϕ no matter what the other agents in AGT \ {i} do". For notational convenience, we write [i] instead of [{i}]. [∅]ϕ can be shorten to "ϕ is necessarily true". The dual expression 〈∅〉ϕ means "ϕ is possibly true". Note that the operators 〈∅〉 and [J] can be combined in order to express what agents and groups can do: 〈∅〉[J]ϕ means "J can see to it that ϕ whatever the other agents in AGT \ J do".

The STIT fragment we are interested in here is called dfSTIT and is defined by the following BNF:

ϕ ::= χ | ψ | ϕ ∧ ϕ | ¬ϕ | 〈∅〉ψ (see-to-it and "can" formulas) where p ranges over ATM and J over 2AGT \ {∅}.

2.2 Models

Here we give two semantics of STIT. It is proved in [Herzig and Schwarzentruber, 2008] that these two semantics are equivalent. The first one corresponds to the original semantics of STIT with agents and groups given in [Horty, 2001]. The other one is based on the product logic S5n [Gabbay et al., 2003] and is used in the proof of decidability of the satisfiability problem of a dfSTIT -formula (Theorem 1). Let us give first the original semantics of STIT.

Definition 1. A STIT-model is a tuple

M = (W, {RJ }J⊆AGT, V ) where:

• W is a non-empty set of possible worlds or states;
• For all J ⊆ AGT, RJ is an equivalence relation over W such that:
• RJ ⊆ R∅;
• RJ = ⋂j∈J R{j};
• for all w ∈ W, for all (wj)j∈AGT ∈ R∅(w)n , ⋂j∈AGT R{j}(wj) ̸= ∅;
• RAGT = idW.
• V is a valuation function, that is, V : W → 2ATM .

As in the previous Constraint 3, it is convenient to view relations on W as functions from W to 2W , that is, for every J ∈ 2AGT , RJ(w) = {v ∈W | wRJv}. RJ represents the actual action chosen by J: if wRJv then v is an outcome of the action chosen by J at w. We recall that R∅ is the relation over all possible outcomes: if w is the current world and wR∅v then v is a possible outcome at w. Thus, Constraint 1 on STIT models just means that all outcomes brought about by J are possible outcomes. Constraint 2 just says that the set of outcomes brought about by J at a given world w is equal to the pointwise intersection of the sets of outcomes brought about by the agents in J at w. Constraint 3 expresses a socalled assumption of independence of agents: if w1, . . . ,wn are possible outcomes at w then the intersection of the set of outcomes that agent 1 brings about at w1, and the set of outcomes that agent 2 brings about at w2,..., and the set of outcomes that agent n brings about at wn is not empty. More intuitively, this means that agents can never be deprived of choices due to the choices made by other agents. Constraint 4 expresses an assumption of determinism: the set of outcomes brought about by all agents is a singleton.

Truth conditions for atomic formulas and the boolean operators are entirely standard. For every J ∈ 2AGT , the truth condition of the modal operator [J] is:

M, w |= [J]ϕ iff M, v |= ϕ for all v ∈ W such that wRJv. The alternative semantics of STIT is based on the product logic S5n . It is defined as follows:

Definition 2. A product STIT-model is a tupleM= (W, V ) where:

• W = W1 × · · · ×Wn where Wi are non-empty sets of worlds or states;
• V is a valuation function, that is, V : W → 2ATM .

The truth conditions for the modal operators [J] in product STIT-models are:

A formula ϕ is STIT-valid (noted |=STIT ϕ) iff ϕ is true in every world of every STIT-model (or product STIT-model).

2.3 Decidability

Our fragment dfSTIT of STIT with agents and groups has interesting computational properties. In particular:

Theorem 1. The problem of satisfiability of dfSTIT is NPcomplete.

This is implied by the following fact:

Theorem 2. If a dfSTIT -formula is satisfiable, then it is in a polynomial sized model.

Sketch of proof. The main idea of the proof is a selection-ofpoints argument as in [Ladner, 1977]. The entire proof is given in [Lorini and Schwarzentruber, 2009].

3 Counterfactual statements in STIT

The following counterfactual statement is a fundamental constituent of an analysis of counterfactual emotions:

(*) group J (or agent i) could have prevented a certain state of affairs χ to be true now.

Our STIT fragment enables a formal translation of it. We denote this translation by CHPJχ, defined as follows:

The expression ¬[AGT \ J]χ just means that: the complement of J with respect to AGT (i.e. AGT \ J) does not see to it that χ (no matter what the agents in J have chosen to do). This is the same thing as saying that: given what the agents in AGT \ J have chosen, there exists an alternative joint action of the agents in J such that, if the agents in J did choose this action, χ would be false now. Thus, χ and ¬[AGT \ J]χ together correctly translate the previous counterfactual statement (*).

EXAMPLE. Imagine a typical coordination scenario with two agents AGT = {1, 2}. Agents 1 and 2 have to take care of a plant. Each agent has only two actions available: water the plant (water) or do nothing (skip). If either both agents water the plant or both agents do nothing, the plant will die (dead). In the former case the plant will die since it does not tolerate too much water. In the latter case it will die since it lacks water. If one agent waters the plant and the other does nothing, the plant will survive (¬dead). The scenario is represented in the STITmodel in Fig. 1. For instance both at world w2 and w4, formulas CHP1dead and CHP2dead are true: each agent could have prevented the plant to be dead. Indeed, at world w2, dead and ¬[2]dead are true: given what agent 2 has chosen (i.e. water), there exists an alternative action of agent 1 (i.e. skip) such that, if 1 did choose this action, dead would be false now. At world w4, dead and ¬[2]dead are also true: given what agent 2 has chosen (i.e. skip), there exists an alternative action of agent 1 (i.e. water) such that, if 1 did choose this action, dead would be false now. The case for agent 2 is completely symmetrical.

The following are some interesting properties of the operator CHPJ. If J1 ⊆ J2 then:

• |=STIT CHPJ1 χ → CHPJ2 χ (2)

Proof. We give the proof of Validity 2 as an example. Let M be a STIT-model and w ∈ W such that M, w |= CHPJ1 χ. We have M, w |= χ and M, w |= ¬[AGT \ J1]χ. As RAGT\J1 ⊆ RAGT\J2 , it implies thatM,w |= ¬[AGT \ J2]χ. That is why we have M, w |= CHPJ2 χ.

According to Validity 1 J1 could have prevented χ1 or χ2 to be true if and only if, J1 could have prevented χ1 or could have prevented χ2. Validity 2 expresses a monotonicity property: if J1 is a subset of J2 and J1 could have prevented χ then, J2 could have prevented χ as well. Finally Validity 3 shows how the operator CHPJ behaves over conjunction: if J1 could have prevented χ1 and χ2 then, J1 could have prevented χ1 and could have prevented χ2 separately.

REMARK. It is worth noting that counterfactual statements of the form "group J (or agent i) could have prevented χ to be true", which are expressible in STIT, are not expressible in other well-known logics of multi-agent interaction such as Alternating-time temporal logic (ATL) [Alur and Henzinger, 2002] and Coalition Logic (CL) [Pauly, 2002]. This is due to the fact that STIT is more expressive than ATL and CL (this is formally proved in [Broersen et al., 2006]) so that there are STIT formulas such as [J]χ and ¬[J]χ that cannot be translated into ATL and CL.

4 A STIT extension with knowledge

This section presents an extension of the fragment dfSTIT of STIT logic presented in section 2 with standard operators for knowledge of the form Ki, where Kiϕ means "agent i knows that ϕ is true". This is a necessary step for the formalization of regret and relief that will be presented in section 5.

The language LdfKSTIT of logic dfKSTIT is defined by the following BNF:

where p ranges over ATM, i ranges over AGT and J over 2AGT \ {∅}.

Definition 3. A KSTIT-model is a tuple

M = (W, {RJ }J⊆AGT, {Ei}i∈AGT, V ) where:

• (W, {RJ}J⊆AGT, V ) is a STIT-model;
• For all i ∈ AGT, Ei is an equivalence relation.

Truth conditions for atomic formulas and the boolean operators are again entirely standard. Truth conditions for the STIT operators [J] are given in section 2. Truth conditions for knowledge operators are defined in the standard way:

That is, agent i knows that ϕ at world w in model M if and only if ϕ is true at all worlds that are indistinguishable for agent i at world w.

A formula ϕ is KSTIT-valid (noted |=KSTIT ϕ) iff ϕ is true in every world of every KSTIT-model.

Theorem 3. The satisfiability problem of dfKSTIT is NP-complete if card(AGT) = 1 and PSPACE-complete if card(AGT) ≥ 2.

Sketch of proof. If card(AGT) = 1, we can notice that there are only three operators: [∅], [{1}], and K1. Nevertheless, the operator [{1}] can be removed because we force RAGT = idW in our models. As no K1-operator can appear after a [∅]-operator, we can prove by a selected points argument (in [Ladner, 1977], it is done for S5) that if a dfKSTIT -formula is KSTIT-satisfiable, then it is in a polynomial sized model.

If card(AGT) ≥ 2, we can create a tableau method to see if a dfKSTIT -formula ϕ is KSTIT-satisfiable. The idea consists in using a classical tableau algorithm for the knowledge part considering the STIT-subformulas as propositions (see tableau method for S5n in [Halpern and Moses, 1992]). At each step, we take care of STIT-subformulas by choosing non-deterministically a polynomial sized STIT-model. We can prove correctness and soundness of this tableau method. This algorithm runs using a polynomial space memory so the satisfiability problem of dfKSTIT is NPSPACE. As NPSPACE = PSPACE (Savitch's theorem [Papadimitriou, 1994]), it is PSPACE. It is PSPACE-hard because the logic S5n is embedded into dfKSTIT .

5 Regret and rejoicing: a formalization

In order to provide a logical characterization of counterfactual emotions such as regret, we need to introduce a concept of agent's preference. Modal operators for desires and goals have been widely studied (see e.g. [Cohen and Levesque, 1990; Meyer et al., 1999]). The disadvantage of such approaches is that they complicate the underlying logical framework. An alternative, which we adopt in this paper is to label states with atoms that capture the "goodness" of these states for an agent. Our approach supposes a binary relation of preference between worlds.

Let us introduce a special atom goodi for every agent i ∈ AGT. These atoms are used to specify those worlds which are positive for an agent.

We say that χ is good for agent i if and only if χ is true in all good states. Formally:

Now, we are in a position to define the concept of desirable state of affairs. We say that χ is desirable for agent i if and only if, i knows that χ is something good for him:

As the following valid formulas highlight, every operator DESi satisfies the principle K of normal modal logic, and the properties of positive and negative introspection: χ is (resp. is not) desirable for i if and only if i knows this.

We have now all necessary and sufficient ingredients to define the cognitive structure of regret and to specify its counterfactual dimension. Such a dimension has been widely studied in the psychological literature on regret (see [Kahneman and Miller, 1986; Kahneman, 1995] for instance). Our aim here is to capture it formally. We say that an agent i regrets for χ if and only if ¬χ is desirable for i and i knows that it could have prevented χ to be true now. Formally:

The following example is given in order to better clarify this definition.

EXAMPLE. Consider the popular two-person hand game "Rock-paper-scissors" (Roshambo). Each of the two players AGT = {1, 2} has three available actions: play rock, play paper, play scissors. The goal of each player is to select an action which defeats that of the opponent. Combinations of actions are resolved as follows: rock wins against scissors, paper wins against rock; scissors wins against paper. If both players choose the same action, they both lose. The scenario is represented in the STIT model in Fig. 2. It is supposed winning is something good for each agent and each agent has the desire to win the game: GOOD11Win, GOOD22Win, DES11Win and DES22Win are true at worlds w1-w9. Suppose world w1 is the actual world in which 1 plays rock and 2 plays paper. In this world 1 loses the game (¬1Win), and 1 knows that (by playing scissors) it could have prevented ¬1Win to be true (i.e. K1CHP1¬1Win is true at w1). It follows that at w1 player 1 regrets for having lost the game, that is, REGRET1¬1Win is true at w1.

As the following validity highlights, regret implies the frustration of an agent's desire:

More precisely, if agent i regrets for χ then, i knows that χ holds and ¬χ is something desirable for i (in this sense i feels frustrated for not having achieved ¬χ). Moreover, regret satisfies the properties of positive and negative introspection:

As emphasized by some psychological theories of counterfactual emotions (see [Zeelenberg et al., 1996] for instance), the positive counterpart of regret is rejoicing: while regret has a negative valence (i.e. it is associated with the frustration of an agent's desire), rejoicing has a positive valence (i.e. it is associated with the satisfaction of an agent's desire). According to these theories, a person experiences regret when believing that the foregone outcome would have been better if she did a different action, whilst she rejoices when believing that the foregone outcome would have been worse if she did a different action. More precisely, an agent i rejoices for χ if and only if, χ is desirable for i and, i knows that it could have prevented χ to be true now by doing a different action:

EXAMPLE. Consider again the game "Rock-paper-scissors" represented by the STIT-model in Fig. 2. Suppose world w2 is the actual world in which player 1 plays rock and player 2 plays scissors. In this world player 1 is the winner (1Win) and it knows that (by playing paper or scissors) it could have prevented 1Win to be true (i.e. K1CHP11Win is true at w2). Since DES11Win holds at w2, it follows that at w2 player 1 rejoices for having won the game, that is, REJOICE11Win is true at w2.

The following validity highlights that rejoicing implies desire satisfaction:

More precisely, if agent i rejoices for χ then, i knows that χ and χ is something desirable for i (in this sense i feels satisfied for having achieved χ). As regret, rejoicing satisfies the properties of positive and negative introspection:

That is, agent i rejoices (resp. does not rejoice) for χ if and only if it knows this.

6 Related works

As emphasized in the introduction, there are other researchers who have exploited logical methods in order to build formal models of emotions and affective agents.

In [Meyer, 2006; Steunebrink et al., 2007] a logical approach to emotions based on the modal logical framework KARO [Meyer et al., 1999] is proposed. KARO is a framework based on a blend of dynamic logic with epistemic logic, enriched with modal operators for motivational attitudes such as desires and goals. In Meyer et al.'s approach each instance of emotion is represented with a special predicate, or fluent, in the jargon of reasoning about action and change, to indicate that these predicates change over time. For every fluent a set of effects of the corresponding emotion on the agent's planning strategies and decision processes are specified, as well as the preconditions for triggering the emotion. Although Meyer et al. provide a very detailed formal analysis of emotions, they do not take into account counterfactual emotions. This is also due to some intrinsic limitations of the KARO framework in expressing counterfactual reasoning and statements of the form "agent i could have prevented χ to be true" which are fundamental constituents of this kind of emotions. Indeed, standard dynamic logic on the top of which KARO is built, is not suited to express such statements. In contrast to that, our STIT-based approach overcomes this limitation.

In [El-Nasr et al., 2000] a formal approach to emotions based on fuzzy logic is proposed. The main contribution of this work is a quantification of emotional intensity based on appraisal variables like desirability of an event and its likelihood. For example, following [Ortony et al., 1988], in FLAME the variables affecting the intensity of hope with respect to the occurrence of a certain event are the degree to which the expected event is desirable, and the likelihood of the event. However, in FLAME only basic emotions like joy, sadness, fear and hope are considered and there is no formal analysis of counterfactual emotions as the ones analyzed in our work. Indeed, the formal language exploited in [El-Nasr et al., 2000] is not sufficiently expressive to model counterfactual reasoning about agents' choices and actions.

7 Conclusion

Directions for our future research are manifold. An analysis of intensity of regret and rejoicing was beyond the objectives of the present work. However, we intend to investigate this issue in the future in order to complement our qualitative analysis of affective phenomena with a quantitative analysis. Moreover, we have focused in this paper on the logical characterization of two counterfactual emotions: regret and rejoicing. We intend to extend our analysis in the future by studying the counterfactual dimension of "moral" emotions such as guilt and shame. Several psychologists (see [Lazarus, 1991] for instance) have stressed that guilt involves the conviction of having injured someone or of having violated some norm or imperative, and the belief that this could have been avoided.

It has been proved in [Herzig and Schwarzentruber, 2008] that the logic STIT with agents and groups proposed by Horty [Horty, 2001] is not only undecidable but also not axiomatizable, i.e. there is no axiomatization Ax such that that for every formula ϕ in LSTIT, ⊢Ax ϕ if and only if |=STIT ϕ. In this work, we have dealt with the first problem by presenting a decidable fragment of Horty's logic which is sufficiently expressive for our purpose of formalizing counterfactual emotions. It is still an open question whether we can find a finite and complete axiomatization for our fragment dfSTIT of STIT with agents and groups. Our future work will also be devoted to solve this problem in order to come up with a complete and decidable fragment of STIT with agents and groups.

Acknowledgments

This research is supported by the project CECIL 'Complex Emotions in Communication, Interaction and Language' financed by the French 'Agence Nationale de la Recherche'.