Emiliano Lorini
email: emiliano.lorini@irit.fr

A dynamic logic of knowledge, graded beliefs and graded goals and its application to emotion modelling

The paper introduces a logic which allows to represent different kinds of mental states of an agent such as knowledge, graded belief, and graded goal, and the notion of epistemic action (as the action of learning that a certain fact ϕ is true.) The logic is applied to the formalization of expectation-based emotions such as hope, fear, disappointment and relief, and of their intensity.

Introduction

In this paper, I will present a logic called DL-KGBG (Dynamic Logic of Knowledge, Graded Beliefs and Goals) which allows: [START_REF] Adam | A logical formalization of the OCC theory of emotions[END_REF] to express that a given epistemic action is going to occur; [START_REF] Alchourrón | On the logic of theory change: partial meet contraction and revision functions[END_REF] to describe the effects of an epistemic action on an agent's mental state; [START_REF] Aucher | A combined system for update logic and belief revision[END_REF] to represent different kinds of mental attitudes including knowledge, graded beliefs (i.e., believing with a certain strength that a given proposition is true) and graded goals (i.e., wishing with a certain strength a given proposition to be true.) An epistemic action is nothing but the mental action (or process) of learning that a given proposition is true, of changing the agent's beliefs in the light of a new incoming evidence. I here follow the tradition of Dynamic Epistemic Logic (DEL) [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF] in modelling epistemic actions as basic operations of model transformation in the semantics.

In the second part of the paper, the logic DL-KGBG will be applied to the formalization of expectation-based emotions such as hope, fear, disappointment and relief. It will be shown that this logic allows to represent the notion of emotion intensity (e.g., how much an agent feels happy or sad, disappointed or relieved, etc.), which is ignored by most of current logical models of emotions [START_REF] Meyer | Reasoning about emotional agents[END_REF][START_REF] Adam | A logical formalization of the OCC theory of emotions[END_REF][START_REF] Lorini | A logic for reasoning about counterfactual emotions[END_REF]. 1 Following previous works on the cognitive theory of expectations [START_REF] Castelfranchi | Cognitive anatomy and functions of expectations[END_REF][START_REF] Miceli | The mind and the future: the (negative) power of expectations[END_REF], an expectation-based emotion is here conceived as an emotion that an agent experiences when having an expectation about a certain fact ϕ, that is when: [START_REF] Adam | A logical formalization of the OCC theory of emotions[END_REF] believing that ϕ is true with a certain strength, but envisaging the possibility that ϕ could be false, and (2) either, having the goal that ϕ is true (positive expectation) or, having the goal that ϕ is false (negative expectation).

The rest of the paper is organized as follows. Section 2 will be devoted to present the logic DL-KGBG. A complete axiomatization as well as a decidability result for this logic will be given in Section 3. In Section 4, the logic DL-KGBG will be applied to the formalization of expectation-based emotions and of their intensity.

A dynamic logic of knowledge, graded beliefs and graded goals

This section presents the syntax and the semantics of the logic DL-KGBG, as well as a complete axiomatization and a decidability result for this logic.

Syntax

Assume a countable set of atomic propositions Prop = {p, q, . . .} and a finite set of natural numbers Num = {x ∈ N : 0 ≤ x ≤ max} with max ∈ N. The language L of DL-KGBG is defined by the following grammar in Backus-Naur Form (BNF):

Act : α * ϕ Atm : χ p | after |α | exc h | des h Fml : ϕ χ | ¬ϕ | ϕ ∧ ϕ | [K]ϕ | [α]ϕ
where p ranges over Prop, h ranges over Num, α ranges over Act, and ranges over the set of epistemic action sequences Act * . The other Boolean constructions , ⊥, ∨, → and ↔ are defined from p, ¬ and ∧ in the standard way. I define the set of objective facts Obj as the set of all Boolean combinations of atomic propositions. An epistemic action * ϕ in Act is the mental action (or process) of learning that ϕ is true. As I will show in Section 2.2, technically this amounts to an operation of beliefs' conditionalization in Spohn's sense [START_REF] Spohn | Ordinal conditional functions: a dynamic theory of epistemic states[END_REF]. Act * is the set of epistemic action sequences. An epistemic action sequence is of the form α 1 ; . . . ; α n where ";" stands for concatenation. I note nil the empty sequence of epistemic actions.

Atm contains special constructions of different types which are used to represent both the objective world as well as the mental state of an agent. The formula after |α is a special atom that is read "after the sequence of epistemic actions , the epistemic action α will occur". The atomic formula after nil|α specifies the actual epistemic action that is going to occur next. Therefore, I define:

occ α def = after nil|α
where occ α has to be read "the epistemic action α is going to occur".

The special atoms exc h are used to identify the degree of plausibility of a given world for the agent. Starting from [START_REF] Grove | Two modellings for theory change[END_REF], ranking among possible worlds have been extensively used in belief revision theory. I here use the notion of plausibility first introduced by Spohn [START_REF] Spohn | Ordinal conditional functions: a dynamic theory of epistemic states[END_REF]. Following Spohn's theory, the worlds that are assigned the smallest numbers are the most plausible, according to the beliefs of the individual. That is, the number h assigned to a given world rather captures the degree of exceptionality of this world, where the exceptionality degree of a world is nothing but the opposite of its plausibility degree (i.e., the exceptionality degree of a world decreases when its plausibility degree increases.) Therefore, formula exc h can be read alternatively as "the current world has a degree of exceptionality h" or "the current world has a degree of plausibility maxh". The special atoms des h are used to identify the degree of desirability (or the degree of goodness) of a given world for the agent. Contrary to plausibility, the worlds that are assigned the biggest numbers are the most desirable for the agent. The degree of undesirability (or degree of a badness) of a given world is the opposite of its desirability degree. Therefore, formula des h can be read alternatively as "the current world has a degree of desirability h" or "the current world has a degree of undesirability maxh".

The formula [α]ϕ has to be read "after the occurrence of epistemic action α, ϕ will be true", while [K]ϕ has to be read "the agent knows that ϕ is true". This concept of knowledge is the standard S5-notion, partition-based and fully introspective, that is commonly used both in computer science [START_REF] Fagin | Reasoning about Knowledge[END_REF] and economics [START_REF] Aumann | Interactive epistemology I: Knowledge[END_REF]. As I will show in the next Section 2.2, the operator [K] captures a form of 'absolutely unrevisable belief', that is, a form of belief which is stable under belief revision with any new evidence. A similar property for the notion of knowledge has been advanced by the so-called defeasibility (or stability) theory of knowledge [START_REF] Klein | A proposed definition of propositional knowledge[END_REF][START_REF] Stalnaker | On logics of knowledge and belief[END_REF][START_REF] Rott | Stability, strength and sensitivity: converting belief into knowledge[END_REF]. According to this theory, a given piece of information ϕ is part of the agent's knowledge only if the agent's justification to believe that ϕ is true is sufficiently strong that it is not capable of being defeated by evidence that the agent does not possess. As pointed out by [START_REF] Baltag | A qualitative theory of dynamic interactive belief revision[END_REF], two different interpretations of the term 'evidence' have been given in the context of this theory, each giving a different interpretation of what knowledge is. The first one defines knowledge as a form of belief which is stable under belief revision with 'any piece of true information', while the second one gives a stronger definition of knowledge as a form of belief which is stable under belief revision with 'any piece of information'. The concept formalized by the operator [K] captures this latter form of knowledge in a stronger sense.

Semantics

Definition 1 (Model). DL-KGBG-models are tuples M = W, ∼, κ exc , κ des , P, V where:

-W is a nonempty set of possible worlds or states; -∼ is an equivalence relation between worlds in W; -κ exc : W -→ Num and κ des : W -→ Num are functions from the set of possible worlds into the finite set of natural numbers Num; -P : W × Act * -→ Act is a partial function called protocol, mapping worlds and action sequences to actions; -V : W -→ 2 Prop is a valuation function.

As usual, p ∈ V(w) means that proposition p is true at world w. The equivalence relation ∼, which is used to interpret the epistemic operator [K], can be viewed as a function from W to 2 W . Therefore, we can write ∼(w) = {v ∈ W : w ∼ v}. The set ∼(w) is the agent's information state at world w: the set of worlds that the agent considers possible at world w or, the set of worlds that the agent cannot distinguish from world w. As ∼ is an equivalence relation, if w ∼ v then the agent has the same information state at w and v (i.e., the agent has the same knowledge at w and v.)

The function κ exc represents a plausibility grading of the possible worlds and is used to interpret the atomic formulas exc h . κ exc (w) = h means that, according to the agent the world w has a degree of exceptionality h or, alternatively, according to the agent the world w has a degree of plausibility maxh. (Remember that the degree of plausibility of a world is the opposite of its exceptionality degree.) The function κ exc allows to model the notion of belief: among the worlds the agent cannot distinguish from a given world w (i.e., the agent's information state at w), there are worlds that the agent considers more plausible than others. For example, suppose that ∼(w) = {w, v, u}, κ exc (w) = 2, κ exc (u) = 1 and κ exc (v) = 0. This means that at world w the agent cannot distinguish the three worlds w, v and u, that is, {w, v, u} is the set of worlds that the agent considers possible at world w. Moreover, according to the agent, the world v is strictly more plausible than the world u and the world u is strictly more plausible than the world w (as max -0 > max -1 > max -2.)

The function κ des is used to interpret the atomic formulas des h . κ des (w) = h means that, according to the agent the world w has a degree of goodness (or desirability) h or, alternatively, according to the agent the world w has a degree of badness (or undesirability) maxh. (Remember that the degree of undesirability of a world is the opposite of its desirability degree.)

Finally, the protocol function P is used to interpret the atomic formulas after |α . A similar notion of protocol has been studied by [START_REF] Van Benthem | Merging frameworks for interaction[END_REF]. For every world w ∈ W, P(w, ) = α means that, at world w, the epistemic action α will occur after the sequence of epistemic actions . For example, imagine that the agent wakes up in the morning. Then P(w, * 8pm; * rain) = * earthquake means that, at world w, after learning in sequence that 'it is 8 p.m.' (by looking at the alarm) and that 'it is raining outside' (by opening the window), the agent (will switch on the radio) and will learn that 'during the night an earthquake of magnitude 5 has occurred'. P(w, nil) = α means that, at world w, the epistemic action α will occur next. P is supposed to be a partial function as I want to allow states in which no action occurs.

DL-KGBG-models are supposed to satisfy the following additional normality constraint for the plausibility grading.

(NORM κ exc ) for every w ∈ W, there is v such that w ∼ v and κ exc (v) = 0. Definition 2 (Truth conditions). Given a DL-KGBG-model M, a world w and a formula ϕ, M, w | = ϕ means that ϕ is true at world w in M. The rules defining the truth conditions of formulas are:

-M, w | = p iff p ∈ V(w) -M, w | = after |α iff P(w, ) is defined and P(w, ) = α -M, w | = exc h iff κ exc (w) = h -M, w | = des h iff κ des (w) = h -M, w | = ¬ϕ iff not M, w | = ϕ -M, w | = ϕ ∧ ψ iff M, w | = ϕ and M, w | = ψ -M, w | = [K]ϕ iff M, v | = ϕ for all v with w ∼ v -M, w | = [ * ϕ]ψ iff M * ϕ , w | = ψ
where the updated model M * ϕ is defined according to the Definition 9 below.

Following [START_REF] Spohn | Ordinal conditional functions: a dynamic theory of epistemic states[END_REF], I extend the exceptionality degree of a possible world to a plausibility/exceptionality degree of a formula viewed as a set of worlds.

Definition 3 (Exceptionality degree of a formula). The exceptionality degree of a formula ϕ at world w, noted κ w exc (ϕ), is defined as follows:

κ w exc (ϕ) def = min{κ exc (v) : M, v | = ϕ and w ∼ v}.
As expected, the plausibility degree of a formula ϕ, noted κ w plaus (ϕ), is defined as maxκ w exc (ϕ). I do a similar manipulation for the desirability degree of a formula. Definition 4 (Desirability degree of a formula). The desirability degree of a formula ϕ at world w, noted κ w des (ϕ), is defined as follows:

κ w des (ϕ) def = min{κ des (v) : M, v | = ϕ and w ∼ v}.
As expected, the undesirability degree of a formula ϕ, noted κ w undes (ϕ), is defined as max -κ w des (ϕ). Again following [START_REF] Spohn | Ordinal conditional functions: a dynamic theory of epistemic states[END_REF], I define the concept of belief as a formula which is true in all worlds that are maximally plausible (or minimally exceptional).

Definition 5 (Belief). At world w the agent believes that ϕ is true if and only if, for every v such that w

∼ v, if κ exc (v) = 0 then M, v | = ϕ.
The following concept of graded belief is taken from [START_REF] Laverny | From knowledge-based programs to graded belief-based programs, part II: off-line reasoning[END_REF]. I say that at world w the agent believes that ϕ with strength at least h if and only if, all possible worlds in which ϕ is false are exceptional at least degree h (or all possible worlds in which ϕ is false are plausible at most degree maxh.) Definition 6 (Graded belief). At world w the agent believes that ϕ with strength at least h if and only if, κ w exc (¬ϕ) ≥ h. I define the following concept of strong (or certain) belief: an agent has the strong belief that ϕ if and only if either he knows that ϕ is true (i.e., he has an unrevisable belief that ϕ is true) or he believes that ϕ is true with maximal strength max.

Definition 7 (Strong belief). At world w the agent strongly believes that ϕ (or at w the agent is certain that ϕ is true) if and only if, M, v | = ϕ for all v with w ∼ v or κ w exc (¬ϕ) = max.

The following concept of graded goal is the motivational counterpart of the notion of graded belief. This concept has not been studied before in the logical literature. I say that at world w the agent wants (or wishes) ϕ to be true with strength at least h if and only if, all possible worlds in which ϕ is true are desirable at least degree h (or all possible worlds in which ϕ is true are undesirable at most degree maxh.) This implies that, all possible worlds which are desirable at most degree h -1 satisfy ¬ϕ (or all possible worlds which are undesirable at least degree max -(h -1) satisfy ¬ϕ.)

Definition 8 (Graded goal). At world w the agent wants/wishes ϕ to be true with strength at least h (or the agent has the goal that ϕ with strength at least h) if and only if, κ w des (ϕ) ≥ h. The reason why the definition of graded goal is not symmetric to the definition of graded belief is that these two concepts satisfy different logical properties. As I will show below in Section 2.3, Definition 6 and Definition 8 allow to capture interesting differences between graded belief and graded goal, especially on the way they distribute over conjunction and over disjunction. As the following proposition highlights, the concepts of belief, graded belief, strong belief and graded goal semantically defined in Definitions 5-8 are all syntactically expressible in the logic DL-KGBG. Proposition 1. For every DL-KGBG-model M and world w:

( K (des l ∧ ϕ) ∧ k∈Num:k<l [K](des k → ¬ϕ))
In the light of Proposition 1, I provide the following four syntactic abbreviations:

Belϕ def = [K](exc 0 → ϕ) Bel ≥h ϕ def = l∈Num:l≥h ( K (exc l ∧ ¬ϕ) ∧ k∈Num:k<l [K](exc k → ϕ)) SBelϕ def = k∈Num:k<max [K](exc k → ϕ) Goal ≥h ϕ def = l∈Num:l≥h ( K (des l ∧ ϕ) ∧ k∈Num:k<l [K](des k → ¬ϕ))
where Belϕ, Bel ≥h ϕ, SBelϕ and Goal ≥h ϕ respectively mean: "the agent believes that ϕ", "the agent believes that ϕ with strength at least h",2 "the agent strongly believes that ϕ" and "the agent wants/wishes ϕ to be true with strength at least h".

Definition 9 (Model update). Given a DL-KGBG-model M = W, ∼, κ exc , κ des , P, V , M * ϕ is the model such that:

W * ϕ = W ∼ * ϕ = ∼ for all w, κ * ϕ exc (w) =        κ exc (w) -κ w exc (ϕ) if M, w | = ϕ Cut max (κ exc (w) + ∆) if M, w | = ¬ϕ for all w, κ * ϕ des (w) = κ des (w)
for all w, P * ϕ (w, )

=        α if P(w, * ϕ; ) = α undefined if P(w, * ϕ; ) is undefined V * ϕ = V where ∆ ∈ Num \ {0} and Cut max (x) =        x if 0 ≤ x ≤ max max if x > max
An epistemic action * ϕ makes the protocol P to advance one step forward (see the definition of P * ϕ .) That is, if α will occur after the sequence of events * ϕ; then, after the occurrence of the epistemic action * ϕ, it is the case that α will occur after the sequence of events . As epistemic actions only affect the agent's beliefs and do not affect the objective world, the valuation function V is not altered by them (see the definition of V * ϕ .) Moreover, the epistemic action * ϕ modifies the plausibility ordering (see the definition of κ * ϕ exc ) but does not modify the agent's information state (see the definition of ∼ * ϕ ) nor the desirability ordering (see the definition of κ * ϕ des .) In particular, the epistemic action of learning that ϕ is true induces a kind of belief conditionalization in Spohn's sense [START_REF] Spohn | Ordinal conditional functions: a dynamic theory of epistemic states[END_REF]. The plausibility ranking over possible worlds is updated as follows.

-For every world w in which ϕ is true, the degree of exceptionality of w decreases from κ exc (w) to κ exc (w) -κ w exc (ϕ), which is the same thing as saying that, degree of plausibility of w increases from max -κ exc (w) to max -(κ exc (w) -κ w exc (ϕ)). (Note that, by Definition 3, we have κ exc (w) -κ w exc (ϕ) ≤ κ exc (w).) -For every world w in which ϕ is false, the degree of exceptionality of w increases from κ exc (w) to Cut max (κ exc (w) + ∆), which is the same thing as saying that, degree of plausibility of w decreases from max -κ exc (w) to max -Cut max (κ exc (w) + ∆).

Cut max is a minor technical device, taken from [START_REF] Aucher | A combined system for update logic and belief revision[END_REF], which ensures that the new plausibility assignment fits into the finite set of natural numbers Num. The parameter ∆ is a conservativeness index which captures the agent's disposition to radically change his beliefs in the light of a new evidence. More precisely, the higher is the index ∆, and the higher is the agent's disposition to decrease the plausibility degree of those worlds in which the learnt fact ϕ is false. (When ∆ = max, the agent is minimally conservative.) I assume that ∆ is different from 0 in order to ensure that, after learning that p is true, the agent will believe p. That is, from ∆ ∈ Num \ {0} it follows that [ * p]Bel p is valid for every proposition p ∈ Prop. Note that the operation * ϕ preserves the constraints on DL-KGBG-models: if M is a DL-KGBG-model then M * ϕ is a DL-KGBG-model too.

In the sequel I write | = DL-KGBG ϕ to mean that ϕ is valid in DL-KGBG (ϕ is true in all DL-KGBG-models.)

Some properties of mental attitudes

The following are some interesting examples of validity. For every h, k ∈ Num we have:

| = DL-KGBG Bel ≥h ϕ → Bel ≥k ϕ if h ≥ k (1)
| = DL-KGBG Goal ≥h ϕ → Goal ≥k ϕ if h ≥ k (2)
| = DL-KGBG [K]ϕ → ¬Bel ≥h ϕ (3) | = DL-KGBG SBelϕ ↔ ([K]ϕ ∨ Bel ≥max ϕ) (4) | = DL-KGBG ¬(Belϕ ∧ Bel¬ϕ) (5) | = DL-KGBG [ * ϕ]Belϕ if ϕ ∈ Obj (6) | = DL-KGBG [K]ϕ → [ * ψ][K]ϕ if ϕ ∈ Obj (7) | = DL-KGBG (Bel ≥h ϕ ∧ Bel ≥k ψ) → Bel ≥min{h,k} (ϕ ∧ ψ) (8)
| = DL-KGBG (Goal ≥h ϕ ∧ Goal ≥k ψ) → (Goal ≥max{h,k} (ϕ ∧ ψ) ∨ [K](¬ϕ ∨ ¬ψ)) (9)
| = DL-KGBG (Bel ≥h ϕ ∧ Bel ≥k ψ) → (Bel ≥max{h,k} (ϕ ∨ ψ) ∨ [K](ϕ ∨ ψ)) (10)
| = DL-KGBG (Goal ≥h ϕ ∧ Goal ≥k ψ) → Goal ≥min{h,k} (ϕ ∨ ψ) (11)
According to the validity (1), if the agent believes that ϕ with strength at least h and h ≥ k, then he believes that ϕ is true with strength at least k. Validity (2) is the corresponding property for graded goals. The validity (3) highlights that knowledge and graded belief are distinct concepts. According to the validity (4), the agent has the strong belief that ϕ (i.e., the agent is certain that ϕ) if and only if, either he knows that ϕ is true (i.e., he has an unrevisable belief that ϕ is true) or he believes that ϕ with maximal strength max.

According to the validity (5) (which follows from the normality constraint NORM κ exc given in Section 2.2), an agent cannot have inconsistent beliefs.

The validity (6) highlights a basic property of belief revision in the sense of AGM theory [START_REF] Alchourrón | On the logic of theory change: partial meet contraction and revision functions[END_REF]: if ϕ is an objective fact then, after learning that ϕ is true, the agent believes that ϕ is true. The validity (7) highlights a basic property of knowledge as unrevisable belief (see Section 2.1 for a discussion): if ϕ is an objective fact and the agent knows that ϕ is true then, after learning a new fact ψ, he will continue to know that ϕ is true. In this sense, knowledge is stable under belief revision. According to the validity (8), if the agent believes that ϕ with strength at least h and believes that ψ with strength at least k, then the strength of the belief that ϕ ∧ ψ is at least min{h, k}. According to the validity [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF], if the agent believes that ϕ with strength h and believes that ψ with strength k, then either he believes ϕ ∨ ψ with strength at least max{h, k} or he knows that ϕ ∨ ψ. (Remember that knowledge and graded belief are distinct concepts.)

The validities ( 9) and ( 11) are corresponding principles for goals. According to the validity ( 9), if the agent wishes ϕ to be true with strength at least h and wishes ψ to be true with strength at least k, then either he wishes ϕ ∧ ψ to be true with strength at least max{h, k} or he knows that ϕ and ψ are inconsistent facts. According to the validity [START_REF] Fagin | Reasoning about Knowledge[END_REF], if the agent wishes ϕ to be true with strength at least h and wishes ψ to be true with strength at least k, then he wishes ϕ ∨ ψ to be true with strength at least min{h, k}.

The interesting aspect is that graded goals distribute over conjunction and over disjunction in the opposite way as graded beliefs. Consider for instance the validity [START_REF] Van Ditmarsch | Prolegomena to dynamic logic for belief revision[END_REF] and compare it to the validity [START_REF] Castelfranchi | Cognitive anatomy and functions of expectations[END_REF]. The joint occurrence of two events ϕ and ψ is less plausible than the occurrence of a single event. This is the reason why in the right side of the validity [START_REF] Castelfranchi | Cognitive anatomy and functions of expectations[END_REF] we have the min. On the contrary, the joint occurrence of two desired events ϕ and ψ is more desirable than the occurrence of a single event. This is the reason why in the right side of the validity [START_REF] Van Ditmarsch | Prolegomena to dynamic logic for belief revision[END_REF] we have the max. For example, suppose Peter wishes to go to the cinema in the evening with strength at least h (i.e., Goal ≥h goToCinema) and, at the same time, he wishes to spend the evening with his girlfriend with strength at least k (i.e., Goal ≥k stayWithGirlfriend.) Then, according to the validity [START_REF] Van Ditmarsch | Prolegomena to dynamic logic for belief revision[END_REF], either Peter wishes to to go the cinema with his girlfriend with strength at least max{h, k} (i.e., Goal ≥max{h,k} (goToCinema ∧ stayWithGirlfriend)) or Peter knows that going to the cinema with his girlfriend is impossible (i.e., [K](¬goToCinema ∨ ¬stayWithGirlfriend)), perhaps because he knows that his girlfriend has the flu and cannot go out.

Exact strength of belief and exact strength of goal

The operators of type Bel ≥h and Goal ≥h introduced above enable to specify a concept of graded belief of the form "the agent believes that ϕ with strength h" in which the exact strength of the agent's belief is specified. I assume that "the agent believes that ϕ exactly with strength h", noted Bel h ϕ if and only if, the agent believes that ϕ with strength at least h and it is not the case that the agent believes that ϕ with strength at least h+1. Formally, for every h < max, I define:

Bel h ϕ def = Bel ≥h ϕ ∧ ¬Bel ≥h+1 ϕ
In order to have a uniform notation, I will use Bel ≥max ϕ and Bel max ϕ as interchangeable expressions. I do a similar manipulation for goals. For every h < max, I define:

Goal h ϕ def = Goal ≥h ϕ ∧ ¬Goal ≥h+1 ϕ
where Goal h ϕ has to be read "the agent wants/wishes ϕ to be true exactly with strength h". As for beliefs, I will use Goal ≥max ϕ and Goal max ϕ as interchangeable expressions.

Decidability and axiomatization

Let L-KGBG be the fragment of the logic DL-KGBG without dynamic operators, that is, let the language of L-KGBG be the set of formulas defined by the following BNF:

Act : α * ϕ Atm : χ p | after |α | exc h | des h Fml : ϕ χ | ¬ϕ | ϕ ∧ ϕ | [K]ϕ
where p ranges over Atm, h ranges over Num, α ranges over Act, and ranges over Act * .

Proposition 2. The following formulas are DL-KGBG valid for every h, k ∈ Num, α ∈ Act, ∈ Act * .

after |α → ¬after |β if α β h∈Num exc h h∈Num des h K exc 0 exc h → ¬exc k if h k des h → ¬des k if h k Proposition 3.
The following equivalences are DL-KGBG valid for every p ∈ Atm,

h ∈ Num, α ∈ Act, ∈ Act * . (R.1) [ * ϕ]p ↔ p (R.2) [ * ϕ]after |α ↔ after * ϕ; |α (R.3) [ * ϕ]exc h ↔ ((ϕ ∧ k,l:k-l=h (exc k ∧ Bel l ¬ϕ)) ∨ (¬ϕ ∧ k:Cut max (k+∆)=h exc k )) (R.4) [ * ϕ]des h ↔ des h (R.5) [ * ϕ]¬ψ ↔ ¬[ * ϕ]ψ (R.6) [ * ϕ](ψ 1 ∧ ψ 2 ) ↔ ([ * ϕ]ψ 1 ∧ [ * ϕ]ψ 2 ) (R.7) [ * ϕ][K]ψ ↔ [K][ * ϕ]ψ
The equivalences of Proposition 3 provide a complete set of reduction axioms for DL-KGBG. Call red the mapping on DL-KGBG formulas which iteratively applies the above equivalences from the left to the right, starting from one of the innermost modal operators. red pushes the dynamic operators inside the formula, and finally eliminates them when facing an atomic formula. Proposition 4. Let ϕ be a formula in the language of DL-KGBG. Then

red(ϕ) has no dynamic operators

[α] 2. red(ϕ) ↔ ϕ is DL-KGBG valid 3. red(ϕ) is DL-KGBG valid iff red(ϕ) is L-KGBG valid.
Sketch of Proof. The first item is clear. The second item is proved using Proposition 3 and the rule of replacement of equivalents. The last item follows from the second item and the fact that DL-KGBG is a conservative extension of L-KGBG.

Theorem 1. Satisfiability in DL-KGBG is decidable.

Sketch of Proof. We first show that the logic L-KGBG is decidable. Note that the problem of satisfiability in L-KGBG is reducible to the problem of global logical consequence in S5, where the set of global axioms Γ is the set of all formulas of Proposition 2. That is, we have

| = L-KGBG ϕ if and only if Γ | = S5 ϕ. We can show that Γ | = S5 ϕ if and only if Γ ϕ | = S5 ϕ, where Γ ϕ = Γ \ { after |α → ¬after |β : after |α SUB(ϕ)
or after |β SUB(ϕ) } and SUB(ϕ) is the set of all subformulas of ϕ. In other words, Γ ϕ is the subset of Γ containing only formulas of the type after |α → ¬after |β which are ϕ-relevant. Observe that every Γ ϕ is finite. It is well-known that the problem of global logical consequence in S5 with a finite number of global axioms is reducible to the problem of satisfiability in S5. The problem of satisfiability checking in S5 is decidable [START_REF] Fagin | Reasoning about Knowledge[END_REF][START_REF] Blackburn | Modal Logic[END_REF]. It follows that the problem of satisfiability checking in the logic L-KGBG is decidable too. red provides an effective procedure for reducing a DL-KGBG formula ϕ into an equivalent L-KGBG formula red(ϕ). As L-KGBG is decidable, DL-KGBG is decidable too.

Formalization of expectation-based emotions and their intensity

The modal operators of graded belief and graded goal defined above are used here to provide a logical analysis of expectation-based emotions and their intensities.

Hope and fear

According to some psychological models [START_REF] Reisenzein | Emotions as metarepresentational states of mind: naturalizing the beliefdesire theory of emotion[END_REF][START_REF] Lazarus | Emotion and adaptation[END_REF][START_REF] Ortony | The cognitive structure of emotions[END_REF] and computational models [START_REF] Gratch | A domain independent framework for modeling emotion[END_REF] of emotions, the intensity of hope with respect to a given event is a monotonically increasing function of: the degree to which the event is desirable and the likelihood of the event. That is, the higher is the desirability of the event ϕ, and the higher is the intensity of the agent's hope that this event will occur; the higher is the likelihood of the event ϕ, and the higher is the intensity of the agent's hope that this event will occur. Analogously, the intensity of fear with respect to a given event is a monotonically increasing function of: the degree to which the event is undesirable and the likelihood of the event. There are several possible merging functions which satisfy these properties. For example, I could define the merging function merge as an average function, according to which the intensity of hope about a certain event ϕ is the average of the strength of the belief that ϕ will occur and the strength of the goal that ϕ will occur. That is, for every h, k ∈ Num representing respectively the strength of the belief and the strength of the goal, I could define merge(h,k) as h+k 2 . Another possibility is to define merge as a product function h × k (also used in [START_REF] Gratch | A domain independent framework for modeling emotion[END_REF]), according to which the intensity of hope about a certain event ϕ is the product of the strength of the belief that ϕ will occur and the strength of the goal that ϕ will occur. Here I do not choose a specific merging function, as this would require a serious experimental validation and would much depend on the domain of application in which the formal model has to be used.

Let me now define the notions of hope and fear with their corresponding intensities. An agent is experiencing a hope with with intensity i about ϕ if and only if there are h, k ∈ Num such that such that h < max, h is the strength to which the agent believes that ϕ is true, k is the strength to which the agent wishes ϕ to be true and merge(h,k) = i:

Hope i ϕ def = h,k∈Num:h<max and merge(h,k)=i (Bel h ϕ ∧ Goal k ϕ)
The notion of fear can be defined in a similar way, after assuming that if an agent wishes ϕ to be true, then the situation in which ϕ is false is undesirable for him. 3 An agent is experiencing a fear with with intensity i about ϕ if and only if there are h, k ∈ Num such that h < max, h is the strength to which the agent believes that ϕ is true, k is the strength to which the agent wishes ϕ to be false and merge(h,k) = i:

Fear i ϕ def = h,k∈Num:h<max and merge(h,k)=i (Bel h ϕ ∧ Goal k ¬ϕ)
In the preceding definitions of hope and fear, the strength of the belief is supposed to be less than max in order to distinguish hope and fear, which imply some form of uncertainty, from happiness and sadness (or unhappiness) which are based on certainty. In order to experience hope (resp. fear) about ϕ, the agent should have a minimal degree of uncertainty that ϕ might be false. Indeed, we have that:

| = DL-KGBG Hope i ϕ → ¬SBelϕ (12)
| = DL-KGBG Fear i ϕ → ¬SBelϕ (13)
This means that if an agent hopes (resp. fears) ϕ to be true, then he is not certain that ϕ (i.e., the agent does not have the strong belief that ϕ.) For example, if I hope that my paper will be accepted at the next LORI III workshop, then it means that I am not certain that my paper will be accepted. The preceding two validities are consistent with Spinoza's quote "Fear cannot be without hope nor hope without fear". Indeed, if an agent hopes that ϕ will be true then, according to the validity [START_REF] Gratch | A domain independent framework for modeling emotion[END_REF], he envisages the possibility that ϕ will be false. Therefore, he experiences some fear that ϕ will be false. Conversely, if an agent fears that ϕ will be true then, according to the validity (13), he envisages the possibility that ϕ will be false. Therefore, he experiences some hope that ϕ will be false.

Remark 1. It has to be noted that hope and fear, and more generally expectations, are not necessarily about a future state of affairs, but they can also be about a present state of affairs or a past state of affairs. For example, I might say 'I hope that you feel better now!' or 'I fear that you did not enjoy the party yesterday night!'.

On the contrary, to feel happy (resp. sad) about ϕ, the agent should be certain that ϕ is true. For example, if I am happy that my paper has been accepted at the LORI III workshop, then it means that I am certain that my paper has been accepted. More precisely, an agent is experiencing happiness with intensity h about ϕ if and only if, the agent strong believes (is certain) that ϕ is true and h is the strength to which the agent wishes ϕ to be true:

Happiness h ϕ def = SBelϕ ∧ Goal h ϕ
Moreover, an agent is experiencing sadness with intensity h about ϕ if and only if, the agent strongly believes (is certain) that ϕ is true and h is the strength to which the agent wishes ϕ to be false:

Sadness h ϕ def = SBelϕ ∧ Goal h ¬ϕ
The following validities highlight some relationships between hope and fear, and happiness and sadness. Suppose ∆ = max and ϕ ∈ Obj, then:

| = DL-KGBG Hope i ϕ → [ * ϕ] k∈Num Happiness k ϕ (14)
| = DL-KGBG Fear i ϕ → [ * ϕ] k∈Num Sadness k ϕ (15)
This means that, if the agent is minimally conservative and hopes ϕ to be true then, after learning that ϕ, his sadness will transform into happiness about ϕ (with a certain strength.) On the contrary, if he is minimally conservative and fears ϕ to be true then, after learning that ϕ, his fear will transform into sadness about ϕ (with a certain strength.) As the following two validities highlight, if the agent is minimally conservative and learns that ϕ is false, then his hope about ϕ will transform into sadness about ¬ϕ and his fear about ϕ will transform into happiness about ¬ϕ. That is, suppose ∆ = max and ϕ ∈ Obj, then:

| = DL-KGBG Hope i ϕ → [ * ¬ϕ]

Disappointment and relief

An interesting class of expectation-based emotions are those based on the invalidation of either a positive or a negative expectation. In agreement with Ortony et al.'s psychological model [START_REF] Ortony | The cognitive structure of emotions[END_REF], I distinguish two types of these emotions: disappointment and relief. Disappointment is the emotion due to the invalidation of an agent's hope, while relief is the emotion due to the invalidation of an agent's fear. On the one hand, the higher is the intensity of the invalidated hope that ϕ is true, and the higher is the intensity of the agent's disappointment. On the other hand, the higher is the intensity of the invalidated fear that ϕ is true, and the higher is the intensity of the agent's relief. More precisely, an agent is going to experience a disappointment with intensity i about ϕ if and only if the agent hopes ϕ to be true with intensity i and the agent is going to learn that ϕ if false:

Disappointment i ϕ def = Hope i ϕ ∧ occ * ¬ϕ
Moreover, an agent is going to experience a relief with intensity i about ϕ if and only if the agent fears ϕ to be true with intensity i and the agent is going to learn that ϕ if false:

Relief i ϕ def = Fear i ϕ ∧ occ * ¬ϕ
It has to be noted that disappointment and relief always imply some form of surprise, where surprise is defined as the invalidation of an agent's belief (see also [START_REF] Lorini | The cognitive structure of surprise: looking for basic principles[END_REF]):

Surprise h ϕ def = Bel h ϕ ∧ occ * ¬ϕ
where Surprise h ϕ has to be read the agent feels surprised about ϕ with intensity h.

Conclusion

The analysis of expectation-based emotions presented in Section 4 is obviously very simplistic, as it misses a lot of important psychological aspects. For example, the fact that mental states on which emotions such as hope, fear, disappointment and relief are based are usually joined with bodily activation and components, and these components shape the whole subjective state of the agent and determine his behavior. I have only focused on the cognitive structure of emotions, without considering the felt aspect of emotions. This is of course a limitation of the model presented in this paper, as the intensity of emotion also depends on the presence of these somatic components (e.g., the intensity of fear is amplified by the fact that, when experiencing this emotion I feel my stomach contracted, my throat dry, etc.) However, an analysis of the cognitive structure of emotions (i.e., identifying the mental states which determine a given type of emotion), as the one presented above, is a necessary step for having an adequate understanding of affective phenomena. I postpone to future work an analysis of the relationships between emotion and action (i.e., how an emotion with a given intensity determines the agent's future reactions), and of the relationships between cognitive structure and somatic aspects of emotions (i.e., how somatic components affect emotion intensity.)

Theorem 2 .

 2 The validities of DL-KGBG are completely axiomatized by some axiomatization of S5 for the epistemic operator [K] the schemas of Proposition 2 the reduction axioms of Proposition 3 the inference rule ϕ↔ψ [α]ϕ↔[α]ψ

k∈Num Sadness k ¬ϕ ( 16 )

 16 | = DL-KGBG Fear i ϕ → [ * ¬ϕ]

  1. at w the agent believes that ϕ is true if and only if M, w | = [K](exc 0 → ϕ) 2. at w the agent believes that ϕ is true with strength at least h if and only if M, w | = l∈Num:l≥h ( K (exc l ∧ ¬ϕ) ∧ k∈Num:k<l [K](exc k → ϕ)) 3. at w the agent strongly believes that ϕ is true (or the agent is certain that ϕ is true) if and only if M, w | = k∈Num:k<max [K](exc k → ϕ) 4. at w the agent wants ϕ to be true with strength at least h if and only if M, w | = l∈Num:l≥h

The only exception is[START_REF] Steunebrink | A formal model of emotions: integrating qualitative and quantitative aspects[END_REF]. However, different from the approach presented here, Meyer and coll. do not study the cognitive variables determining intensities (e.g., the strength of an agent's beliefs and the importance of his goals) but instead propose a function describing how the intensity of an emotion decreases over time.

Similar operators for graded belief are studied in[15,

3, 9].

If an agent wishes ϕ to be true, then in the situation in which ϕ is false he will be frustrated. This is the reason why the latter situation is undesirable for the agent.


Sacha Hodencq

Fabrice Forest

Théo Carrano

Benoit Delinchant

Wurtz Frederic

Théo Carrano -Benoit

Delinchant -Frédéric Wurtz

User experience inquiry to specify COFFEE: a Collaborative Open Framework For Energy Engineering

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In the current context of climate change, the transition to energy systems combining the three pillars of sufficiency, efficiency and consistency [START_REF] Samadi | Sufficiency in energy scenario studies: Taking the potential benefits of lifestyle changes into account[END_REF] represents a major challenge for the scientific research. The electricity field can face this challenge with energy modelling, in order to understand and size new sustainable energy systems, taking into account cross-sectoral interactions. While the study of sustainable energy systems is essential, this major challenge of the energy transition invites scientists to open up and pool their research. Collaborative platforms incorporating open energy modelling principles can be the place for this shift.

In this article, we introduce COFFEE (Collaborative Open Framework For Energy Engineering), a collaborative open platform that aims at making research works accessible to peers as well as public authorities, design offices and citizen collectives. We first present the interests of open energy modelling and the characteristics of collaborative platforms, before introducing the concept of COFFEE. Finally, we present the associated main conclusions of a user experience inquiry that was carried out to design the platform, in the form of 12 recommendations.

Collaborative platforms for open energy modelling

Interests of open energy modelling

Institutions such as the European Union [START_REF] Glinos | Open Science[END_REF] and the UNESCO [START_REF]Joint Appeal for Open Science[END_REF] are increasingly asking for transparency and open science practices. Yet, historical and current mainstream approaches in energy modelling are proprietary solutions and lack transparency [START_REF] Pfenninger | Opening the black box of energy modelling: Strategies and lessons learned[END_REF]. Rather than being subjected to coming binding jurisdictions, researchers could embrace open energy modelling that comes with many interests. Here, we refer to "open" as models, code, and data that can be freely accessed, used, modified, and shared by anyone for any purpose [START_REF]Open Definition 2.1 -Open Definition -Defining[END_REF].

First, openness and transparency facilitate peer reviewing and models comparison in the scientific community, as well as the identification of biases, errors or even fraud [START_REF] Morrison | Energy system modeling: Public transparency, scientific reproducibility, and open development[END_REF]. It also improves collaboration and reduces parallel efforts in the research field, but also with other stakeholders such as public authorities through a share of both methods and quantitative work [START_REF] Pfenninger | The importance of open data and software: Is energy research lagging behind?[END_REF]. When it comes to designing sustainable energy systems in a variety of contexts, opensource enables to easily add and discuss specific features [START_REF] Oberle | Are open access models able to assess today's energy scenarios?[END_REF]. Open energy modelling tools meet high standards [START_REF] Groissböck | Are open source energy system optimization tools mature enough for serious use?[END_REF]: they are highly maintainable as well as continuously Sacha Hodencq -Fabrice Forest -Théo Carrano -Benoit Delinchant -Frédéric Wurtz Univ. Grenoble Alpes, CNRS, Grenoble INP, G2Elab 38000 Grenoble, France E-mail: sacha.hodencq@g2elab.grenoble-inp.fr improved [START_REF] Hilpert | The Open Energy Modelling Framework (oemof) -A new approach to facilitate open science in energy system modelling[END_REF], and their source code remains available over time with respect to proprietary software.

Openness also lowers barriers for adoption relative to conventional proprietary solutions [START_REF] Bazilian | Open source software and crowdsourcing for energy analysis[END_REF], and improves comprehensibility [START_REF] Cao | Raising awareness in model-based energy scenario studies-a transparency checklist[END_REF]. Since the outcomes of energy systems studies can shape energy policies and affect the public, opening up these studies can enable the affected stakeholders to participate in the decision-making process [START_REF] Weinand | Reviewing energy system modelling of decentralized energy autonomy[END_REF], which has been identified as a key for the success of energy transition projects [START_REF] Roth | Holistic framework for land settlement development project sustainability assessment: Comparison of El Hierro Island hydro wind project and Sivens dam project[END_REF]. Furthermore, transparency provides reliability to scientific arguments in public debate of energy transition and enable public engagement [START_REF] Barnes | Publish your computer code: it is good enough[END_REF] that can lead to virtuous behaviours. Finally open collaborations favours user-centred innovation with faster development cycles, increased interoperability and cost savings [START_REF]Software Defined Vertical Industries: Transformation through Open Source[END_REF].

The main interests of open energy modelling by audience are presented in Table 1.

Including human actors in the design process

The previously mentioned interests of open energy modelling reflect the importance of taking human actors into account to improve design processes, in addition to technical considerations alone. I.e., going from a positivist epistemology to a constructivist one, where knowledge and especially models, depend on the objective and context of the modeller [START_REF] Bodner | Constructivism: A theory of knowledge[END_REF].

In addition to making energy modelling accessible in legal, financial and technical terms with free and licensed open workflows, these workflows should also be accessible in terms of understanding for the human actors. This includes user-friendliness features such as intelligibility and debatability of knowledge, graphical user interfaces, and abstraction levels close to the stakeholders' understanding when developing energy models [START_REF] Hodencq | OMEGAlpes, an Open-Source Optimisation Model Generation Tool to Support Energy Stakeholders at District Scale[END_REF]. Such features can answer particular issues in the field, such as the lack of permanence of methods and tools following their developer departure from a research team.

More generally, this accessibility need can be answered with online collaborative platforms.

Characteristics of online collaborative platforms in the energy field

Online collaborative platforms enable scattered researchers to cooperate and share research objects as well and ideas and experiences. Collaborative platforms are usually online services ranging from extensive virtual research environments (VREs) that include various features to facilitate sharing and collaboration (accessing data, software, and processing resources), down to single specific tools that enable researchers to work together on specific aspects of research [START_REF] Foster | Open Science Training Handbook[END_REF].

In the energy field, online collaborative platforms can address the issues of transparency and replicability [START_REF] Pfenninger | Opening the black box of energy modelling: Strategies and lessons learned[END_REF], by making open energy modelling principles the norm and facilitating transfers of knowledge. [START_REF] Hodencq | Open and Reproducible Use Cases for Energy (ORUCE) methodology in systems design and operation: a dwelling photovoltaic selfconsumption example[END_REF]. A runtime environment will allow direct use of the tools [START_REF] Boettiger | An introduction to Docker for reproducible research[END_REF]. Finally, synchronous or asynchronous socialisation means such as forums, if used by a sufficiently large community, can connect communities of energy model developers and users, and thus capture and disseminate both explicit and tacit knowledge [START_REF] Nonaka | A Dynamic Theory of Organizational Knowledge Creation[END_REF]. Such platforms enable community building, transparency and legitimacy of studies and participation. Community of actors can then form between these platforms, such as openmod [START_REF] Morrison | An Open Energy System Modeling Community[END_REF]. Notebooks that can be directly understood, adapted and used online [START_REF] Jupyter | Binder 2.0 -Reproducible, interactive, sharable environments for science at scale[END_REF]. Thus, a use case can be used as an intermediary object to explore energy scenarios with an intermediate level of complexity for the workflow and results. It is also a gateway to collaborate and exchange with professionals, tackling information asymmetry.

COFFEE implementation

While the implementation of a first version of COFFEE platform is underway, previous work presented the use case of a dwelling photovoltaic self-consumption [START_REF] Hodencq | Open and Reproducible Use Cases for Energy (ORUCE) methodology in systems design and operation: a dwelling photovoltaic selfconsumption example[END_REF] that can be translated in the functions of COFFEE.

The library would include this dwelling PV selfconsumption use case with a directly usable notebook (available in the Supplementary Materials section). The notebook presents the sources and management of the load profile, PV profile and greenhouse gas data, the main assumptions and methods for the energy modelling with the use of the Mixed Integer Linear Programming modelling tool, OMEGAlpes [START_REF] Hodencq | OMEGAlpes, an Open-Source Optimisation Model Generation Tool to Support Energy Stakeholders at District Scale[END_REF], as well as the results and interpretation. A user can also directly find the open data and open access article in the associated sections. The use case and the tools such as OMEGAlpes will be presented in summary forms based on the Open Energy Platform fact sheets and on interdisciplinary research work from the Eco-SESA program 1 . The introduction of forms, presenting a clear, understandable and available representation of the models, can significantly improve transparency [START_REF] Hülk | Transparency, reproducibility, and quality of energy system analyses -A process to improve scientific work[END_REF]. Moreover, developers can add their own use case, tools or data sets through these forms to contribute. Derived teaching materials are also accessible, such as an introduction to open energy modelling taught to architecture students. Finally, the model developers and users can exchange asynchronously on the online forum about the use case with its specific functions, or general issues about selfconsumption.

CAUTIC inquiry: method and results

A study was led to qualify the relevance of the COFFEE platform concept for the stakeholders, and to contribute to the research on collaborative open platforms in the energy field. In other words, the aim was to ensure future COFFEE platform instances would be usable, used and useful, going beyond the authors common sense. An inquiry was carried out using the CAUTIC method [START_REF] Forest | Paradoxical User Acceptance of Ambient Intelligent Systems[END_REF]. CAUTIC is a user experience qualitative method that is used to explore criteria for the meaning of use. These criteria are divided in 4 categories:

1. Banalisation (how does it work?): assesses the possibility for the user to assimilate the innovation into his customary technical know-how 2. Hybridisation (what does it do?): assesses the possibility for the user to associate the innovation with his existing practices.

3. Active identity (who is it for?): evaluates the possibility for the user to appropriate the innovation to his private and professional identity.

4. Integration in the social environment (how does it fit in?): evaluates the possibility for the user to adapt the innovation to his private or professional environment.

The method first consisted in the formalisation of the use value for the COFFEE concept and presentation of usage scenarios, before carrying out 15 interviews (in addition to two test interviews) with energy stakeholders including:

-researchers (4 interviews),

-public authorities (3 interviews) and design offices (3 interviews), -citizen collectives (5 interviews).

While the sample group is not as representative as it is in quantitative surveys, the twenty hours of interviews with representative user profiles enable to identify and to characterise the decisive factors for COFFEE adoption but not to quantify their weight in the expected success.

After the interviews analysis, the results consist in the identification of the attractors of use and the conditions for the use of COFFEE. Based on this, recommendations for improvements. The overall assessment of the inquiry reveals very few barriers to the adoption of the COFFEE platform. The points of tension are more related to conditions of use and not to barriers. Researchers are the most likely to use COFFEE, while members of collectives are the ones who have the most conditions of use. In general, the aggregation function of COFFEE makes sense but raises the question of potential duplication with existing systems. The library of case studies is a relevant approach but encouraging the user input is a real issue. Animation is an interesting perspective to develop collaborations. Finally, the question of the economic model of COFFEE is not to be underestimated, as users need visibility in order to engage in a contributory logic. This also raises the question of the human resources that would need to be made available to run the network and manage the data on the platform.

Twelve thematic recommendations have been built at the end of the analysis, based on the matching between the users' expectations and conditions to use:

1. Improve communication on the integrator role of COFFEE: adopt a partnership approach with the actors who are already carrying out initiatives, proposing new resources only to create added value to what already exists (e.g., through openness), and offer guidance features in the complex ecosystem of energy modelling for the access to resources to be inclusive.

Position COFFEE in an open science dynamic for energy transition stakeholders:

positioning the platform as providing existing scientific knowledge and highlighting the reciprocity of the research carried out in the field, thus sharing the operational benefits for the territories. An interesting trail could be to identify future challenges and locks arising in the field in the short and long term.

Strengthen COFFEE's perspectives in terms of its economic model: reassure on the minimum means of perpetuation of the platform, and on the open model of research results

, so that the user has sufficient confidence to contribute.

Unlocking the stock of individual resources:

prospecting to uncover a pool of both formal and informal scientific resources for collaboration, and encourage sharing by raising awareness on open science practices.

5.

Organising data: offering a standard formalisation framework to ease inputs and to make resources identifiable and usable, according to various criteria such as peer rating, Technology Readiness Level, level of difficulty, etc…

Propose verification and certification of data provided:

positioning as a trusted network through its neutrality, to guide and make energy studies reliable.

7. Facilitate the COFFEE network: promotion of new contents and facilitation of thematic workshops, thus bridging the gap between communities on operational issues and concretising the transfer of research.

8. Clarify the positioning between proven vs. innovative solutions: positioning the platform according to the solutions level of maturity. It can be key for the implication of actors such as design offices, in accordance with their open or closed model strategy.

9. Support the development of the skills of novices in the groups, with entry-level resources. Also, offer collaborative skills building for professionals.

10. Supporting the relationship between the conurbations and small local communities: while urbanised conurbations usually already benefit from an expert network linked to the research field, small local communities could benefit from the platform to access resources for new projects or citizen actions.

11. Balancing socio-economic resources and technological solutions: solutions related to socioeconomic issues are tough to find for stakeholders and often more relevant than technological solutions. An interdisciplinary link with social, economic and legal research, as well as feedbacks on financial and organisational models should be welcome on the platform.

12. Implement a search engine and/or human resources: given the high quantity of resource and the variety of level of expertise, either a dedicated search engine and/or human resource could help in the indexation and mediation.

These results and recommendations will be used for the implementation of a first version of COFFEE instance to be as relevant as possible for stakeholders. The order in which the recommendations are presented corresponds to the order of priority given for this first implementation in the Grenoble Electrical Engineering laboratory (G2Elab). The Table 2 presents the details of occurrences by profile for each recommendation: that is to say the volume of occurrences of an expression of need or improvement to COFFEE by respondents.

Discussion and perspectives

First, a distinction should be made between the COFFEE platform concept on the one hand, which is fed by literature, authors work and the inquiry results, and implementations of COFFEE platform on the other hand.

The first implementation of COFFEE platform will obviously not cover all the recommendation from the CAUTIC inquiry but rather be used as a first operational version of the COFFEE concept and a showcase for open energy modelling use cases. The order of priority of recommendations for this implementation was made according to our objectives and resources. Even if most improvements are expected from citizen collectives, public authorities and design offices, the recommendations aimed at improving the user experience of the researchers' profile was first prioritized. It is of strategical importance for the development roadmap of an open science platform to ease the inputs coming from scientists. The next step will be to consider the expectations of the citizen collectives, public authorities and design offices. So the recommendations feed the G2Elab's strategy to design COFFEE.

For other use of the COFFEE concept, other priorities could be given to the recommendations depending on the context. If the analysis of the inquiry and the recommendations represent first results, further validations need to be addressed. Methodologies exist [START_REF] Cao | Raising awareness in model-based energy scenario studies-a transparency checklist[END_REF] and have been applied to quantify the transparency, reproducibility and quality of open science approaches: self-assessment is indeed essential in this field. The durability of the platform implementations is also an important matter since it is related to the users confidence in the solution. This will be addressed on the long run, with community development around the platform. An additional challenge is the effort of digital sufficiency in the development and use of online platforms [START_REF] Colaço | Digital Sufficiency as a Principle for Energy Transition Policies[END_REF], to ensure that the progress made in energy transition projects is not wasted. Finally, short-term perspectives include the development of forms for the use cases and tools, and the implementation of a first version of COFFEE. Such a platform will enable to experience actual user feedbacks, and to develop collaborative design, methods and models with users from the various audiences. Including the user from the early steps of the design phase makes it possible to take into account his habits, with systems that are adapted, adopted and not too complex. It can also foster virtuous energy behaviours and be a source of innovation.

Conclusions

This article presents the interests of online collaborative platforms in the energy field, with a focus on open energy modelling practices. It introduces COFFEE, a concept of energy modelling platform that aims at making studies and associated resources accessible for stakeholders. A qualitative user-experience inquiry was carried out to qualify the user experience of the platform, and the analysis results and recommendations are presented. Beyond the single implementation of a platform in the G2Elab; the COFFEE concept and associated inquiry results are intended to be used for the dissemination of open energy modelling platforms.

Figure 1

 1 Figure 1 presents essential concepts for the dissemination of an online collaborative platform in the field of open energy modelling. Documented and versioned open source tools form a basis, where tutorials will allow to quickly grasp the functionality and uses of the models [4]. Documented examples including the context and workflow of the use case from raw data to open access results improve knowledge capitalisation through context understanding[START_REF] Hodencq | Open and Reproducible Use Cases for Energy (ORUCE) methodology in systems design and operation: a dwelling photovoltaic selfconsumption example[END_REF]. A runtime environment will allow direct use of the tools[START_REF] Boettiger | An introduction to Docker for reproducible research[END_REF]. Finally, synchronous or asynchronous socialisation means such as forums, if used by a sufficiently large community, can connect communities of energy model developers and users, and thus capture and disseminate both explicit and tacit knowledge[START_REF] Nonaka | A Dynamic Theory of Organizational Knowledge Creation[END_REF]. Such platforms enable community building, transparency and legitimacy of studies and participation. Community of actors can then form between these platforms, such as openmod[START_REF] Morrison | An Open Energy System Modeling Community[END_REF].

Fig. 1

 1 Fig. 1 Basic concepts for the dissemination of online collaborative platforms. Source: Author

Fig. 2

 2 Fig. 2 COFFEE main functions. Source: Author

Table 1

 1 Main interests of open energy modelling by audience

	Researchers	Public authorities and design offices	Citizen collectives
	Reducing parallel efforts
	Useful, accessible and	Tools for the study of energy projects
	sustainable models with	with low barriers for adoption
	specific features	Education, awareness and
	Peer review, identifying	involvement, that can lead to
	and reducing biases,	virtuous behavioural responses
	errors
	Improved collaboration between science and	Equipping and
	policy makers.	accompanying
	Transfer, valorisation, innovation	citizens
	Scientific credibility in the public debate, comprehensibility of
		energy studies
	Linking science and society

Table 2

 2 Occurrences of recommendations by audience

	Recommenda-tions	Research (4)	Public authorities and design offices (6)	Citizen collectives (5)	Tot. (15)
	1. Integrator	2	3	4	9
	2. Positioning	2	4	2	8
	3. Economic model	-	5	1	6
	4. Unlocking	3	1	-	4
	5. Organising data	2	4	3	9
	6. Verification	1	5	1	7
	7. Facilitation	3	5	5	13
	8. Innovative?	-	2	2	4
	9. Support	-	2	3	5
	10. Local communities	1	4	2	7
	11. Balancing	2	3	5	10
	12. Human resource	2	1	5	8

Table 2

 2 can help regarding the representativeness of recommendations in the targeted audiences. Regarding these results, biases exist given the low number of participants and the way it gives a weight to each recommendation. The role of a user centric method such as CAUTIC is to reveal the expectations of the user profiles to the designer but the user needs are not the design strategy. Regardless the weight of the recommendations, it shows what the designer has to improve depending on the targeted profile.

Acknowledgements The authors would like to thank the INNOVACS

Supplementary materials

To access the notebook discussed in section 3.2: https://gricad-gitlab.univ-grenoblealpes.fr/omegalpes/omegalpes_examples/-/blob/846814ba1c42309642f1032c188d2bbb94ca2435/not ebooks/article_2021_BS_ORUCE.ipynb


G Parent

R Penin

J P Lecointe

J F Brudny

T Belgrand

Analysis of the Magnetic Flux Distribution in a New Shifted Non Segmented Grain Oriented AC Motor Magnetic Circuit

Keywords: AC machine efficiency, finite element methods (FEMs), grain oriented electrical steel, magnetic cores

This paper deals with a new AC electric motor magnetic circuit structure made of shifted non-segmented grain oriented steel laminations. The aim of the paper is to understand with a finite element approach the local distribution of the magnetic flux density inside shifted laminations as well as in the air-gaps between them. It is shown that the air-gap flux distribution is not trivial at all and very difficult to appreciate.

I. INTRODUCTION

U SUALLY, most of the low and medium power AC electric rotating machine magnetic circuits are made of Non Oriented (NO) steel. Grain Oriented (GO) steel laminations, as for them, are used in transformer cores.

Nevertheless, recently, a new AC stator magnetic circuit, based on the stacking of shifted non-segmented GO sheets, has been developed [START_REF] Brudny | Magnetic core and use of magnetic core for electrical machines[END_REF] [START_REF]Magnetic core and use of magnetic core for electrical machines[END_REF]. Previous works showed that such a structure allows decreasing iron losses in the machine compared with stators made of NO sheets of same thickness [START_REF] Lopez | Grain oriented steel assembly characterization for the development of high efficiency ac rotating electrical machines[END_REF]. This method has been applied to a 11 kW induction machine in order to make it more environment-friendly [START_REF] Boughanmi | Life cycle assessment of a three-phase electrical machine in continuous operation[END_REF]. Indeed, its efficiency has been increased of 3% at full load compared with the same machine built with NO sheets magnetic circuit [START_REF] Lopez | Grain oriented steel assembly characterization for the development of high efficiency ac rotating electrical machines[END_REF]. The emitted noise has also been reduced [START_REF] Demian | Ac magnetic circuits using nonsegmented shifted grain oriented electrical steel sheets: Impact on induction machine magnetic noise[END_REF]. Hence, this kind of GO steel magnetic circuit may be included in a higher IE class. Moreover, in a certain way, this structure presents some similarities with transformer core corner joints [START_REF] Hihat | Equivalent permeability of step-lap joints of transformer cores: Computational and experimental considerations[END_REF].

In such configurations, the b magnetic flux density in the magnetic circuit of the machine has to pass from one lamination to another in order to satisfy the principle of energy minimization. Hence, b flows both in the planes of the magnetic sheets and in a direction perpendicular to those planes. That 3D distribution is really particular and specific and so required to be studied. In this paper, the authors show that the path thus taken by b is not trivial at all. Moreover, due to the very small thickness of the air-gaps between laminations, measuring b experimentally is quite a difficult task. Hence, using numerical methods, such as the Finite Element (FE) method, is the most appropriate approach for the understanding of this kind of phenomena.

In the first part of this paper, the studied device is presented and the authors show with a FE simulation how the magnetic flux distribution on the latter is complex. Moreover, FE results are strengthned with experimental results. The second part consists in several FE results showing which parameters influence the magnetic flux density distribution in the struture. The last part, as for it, is a results discussion in which the authors explain the reasons of the 3D flux distribution.

II. STUDIED SETUP -PARTICULARITIES OF THE MAGNETIC FLUX DENSITY DISTRIBUTION

A. Non-segmented shifted GO steel sheets stack

The studied structure is an annular yoke made of GO laminations whose Rolling Directions (RDs) are shifted from each other by a constant angle (Fig. 1). An unidirectional excitation is provided by a winding regularly laid out around the yoke and supplied by a sinusoidal current. This structure seems very simple to analyze at first glance. Nevertheless, contrary to a classical NO steel sheet stack in which the magnetic flux density is homogeneous and identical in every single sheet, the latter, in this particular stack, follow rather the lamination whose RD is the most adapted to its circulation -minimizating the magnetic energy -and, depending on the reluctance of the air-gaps, crosses the latters [START_REF] Pfutzner | Concept for more correct iron loss measurements considering path length dynamics[END_REF].

Hence, studying this annular structure excited with an uniform pulsating magnetic field is an important step for the understanding of the phenomena occuring in GO magnetic circuit of AC machines excited with a rotating magnetic field. The paper relates about a structure made of GO steel sheets of 0.35 mm thickness and the study is limited to the case = 90 .

B. Finite Element model

In order to analyze the magnetic flux distribution in the studied structure, a FE simulation of a stack of annular GO steel sheets such as the one presented in Fig. 1 is performed using the code GETDP [START_REF] Dular | A general environment for the treatment of discrete problems and its application to the finite element method[END_REF]. The internal radius, the external radius and the thickness of each sheet are 100 mm, 81.5 mm and 0.35 mm respectively. Moreover, the model takes into account both the insulation and the interlaminar thicknesses by including a 5 µm air-gap between each lamination.

With such a ratio between the sheets and the air-gaps thickness, it is obvious that modeling a stack made of hundreds of laminations, like in a real stator, is not an option. Indeed, such cases would lead to extremely high computation time problems, or even unsolvable problems. Hence, in order to get accurate results with descent computation times, the model is made of a number of sheets chosen as follows : at a given angle, only three times the number of sheets necessary to cover a full permutation are modelled. As an example, for = 90 , a full permutation is covered by two sheets, so six sheets are modeled and the fields are analyzed in the two ones situated in the middle of the stack in order to avoid the influence of the borders on the flux distribution. Note that for = 90 it is also possible to take advantages of symetries and so only model two sheets.

The anisotropy of the GO sheets is defined by three directions : the Rolling Direction (RD), the Transverse Direction (TD) and the Normal Direction (ND). The first two directions are included into the plane of the sheets, while the third one is normal to that plane (Fig. 4). Hence, the relation between the magnetic flux density and the magnetic field can be expressed as follows:

0 @ b RD b T D b ND 1 A = 0 @ µ RD 0 0 0 µ T D 0 0 0 µ ND 1 A • 0 @ h RD h T D h ND 1 A (1)
In (1), each magnetic permeability µ RD , µ T D and µ ND is a function of the magnetic field so that saturation is taken into account (Fig. 2). The first magnetization b(h) curves related to the RD and the TD are determined by standardised Epstein frame test. On the other hand, the curve related to the ND is obtained by use of a specific test bench [START_REF] Hihat | Experimental and numerical characterization of magnetically anisotropic laminations in the direction normal to their surface[END_REF] and the values are conform to those found in the literature [START_REF] Pfutzner | Threedimensional flux distributions in transformer cores as a function of package design[END_REF]. Relation (1) allows taking into account the magnetic characteristics only in the main directions. This is a simple method to get hints about the field behaviour, but appropriate enough for this study. Furthermore, very few other approaches are available. Moreover, a more realistic model would mean integrate the behaviour of domain walls in the material [START_REF] Ebrahimi | Correlation between normal flux transfer from lamination to lamination during the magnetization process with static domain structures in grain oriented[END_REF] which is something not available at present time. Finally, in order to get results as valid as possible, every simulations are performed with both scalar and vector magnetic potentials formulations [START_REF] Bossavit | Whitney forms: a class of finite elements for threedimensional computations in electromagnetism[END_REF].

C. Results

The results of the FE simulation of the studied stack in the case of = 90 are presented in Fig. 3 and in Fig. 4. The latter shows the air gap magnetic flux distribution in the case of lamination 2 (whose RD is RD2) is on top of lamination 1.

As expected, b is concentrated in the sheets that are best adapted to its circulation (Fig. 3). Nevertheless, it is noticeable that the flux distribution in the air-gap is not homogeneous. Indeed, in Fig. 4, three zones can be highlighted. The first one shows a flux concentration toward the external border of the structure. Actually, this zone represents the area where the magnetic flux density passes through the air gap, leaving the RD of a lamination to reach the RD of another lamination. That phenomenon was expected. On the other hand, the fact that this zone is concentrated toward the external border of the structure is noticeable. This phenomenon is quite easy to explain actually. Indeed, once the magnetic flux follow the RD of a lamination, it tends to follow it as long as possible before crossing the air-gap. Thus, the best place for the flux to cross pass from one sheet to another is situated at 45 , ie It is also interesting to underline that the flux density in the air-gap presents, spatially, a sinusoidal waveform. Fig. 5 presents this distribution along 360 close to the two borders (zones 1 and 2) and in the middle (zone 3) of the structure.

D. Experimental validation

Since the flux density distribution is different than expected, an experiment on a real stack excited as stated in section II-A has been performed. The frequency of the excitation is set at 50 Hz and the global value of the b magnetic flux density is 0.7 T. Nine wounded sensors (three turns of 4 mm denoted 1 to 9 in Fig. 6) have been placed in three zones: three of them in the RD of a lamination whereas the last six ones are seperated into two groups of three at 45 on both sides of the RD. They make it possible to measure the magnetic flux density close to the borders and in the middle of the lamination. Table I shows that the three sensors noted 7, 8 and 9 positioned along the RD measure low flux amplitudes, which is in accordance with the results of the FE simulation (Fig. 4). Moreover, the voltages measured by sensors 1 and 3 are higher than sensor 2. The same comment can be made about sensors 4 and 6 compared with sensor 5. It can be pointed out that, despite the fact that sensors 1, 2, 3 and 4, 5, 6 are located symmetrically with RD, differences concerning the amplitudes occur. Those differences come from the sensors themselves. Indeed, they are manually wounded and then stuck between the sheets. Hence, their shapes may not exactly be the same at first and also may have been modified during the sheets clamping process. The results are prefectly in accordance with the FE simultation results when it comes to phases. Indeed, the signals measured by sensors 1 and 3 are phase-opposited as well as the signals measured by sensors 4 and 6.

III. PARAMETERS INFLUENCING THE FLUX DENSITY

DISTRIBUTION

Several parameters have been modified in order to understand their impact on the magnetic flux density distribution in

A. Impact of the internal radius

The internal radius of the rings has been reduced, the external radius being unchanged. That influences the distribution of b in the sheets and in the air gap, as shown in Fig. 7. The zone 1 has moved from the external border to be closer from the central hole. The zone 2, where the flux is almost null is still present. The zone 3 is really more reduced. It shows that the central hole has a major rule for the flux distribution : as the hole size is reduced, the zone 3 is not so important. Nevertheless, the values of the magnetic flux density are, of course, impacted. Indeed, the thinner the air-gap is, the less reluctant it is and so the flux present in the laminations can cross it more easily when it has to turn toward the RD.

C. Impact of the saturation

The FE simulation results presented in previous sections involved a stack magnetization level in the linear part of the constitutive law [START_REF] Brudny | Magnetic core and use of magnetic core for electrical machines[END_REF]. Taking into account a higher magnetization level of the stack, ie more saturated sheets, doesn't change the double path of the flux density observed in Fig. 4. Indeed, each one of the three zones previously highlighted is present in unsaturated as well as saturated cases. The saturation of the laminations on the flux density distribution in the air-gap is presented in Fig. 8. Instead of being purely sinusoidal, the waveforms are classically deformed by the saturation.

Fig. 1 .

 1 Fig. 1. Yoke composed of shifted laminations

Fig. 2 .

 2 Fig. 2. b(h) curves in RD, TD and ND

Fig. 3 .Fig. 4 .

 34 Fig. 3. Distribution of b in stacked laminations

Fig. 5 .

 5 Fig. 5. Distribution of b in the air-gap

Fig. 6 .

 6 Fig. 6. Position of the 9 sensors between 2 sheets the structure.

Fig. 7 .

 7 Fig. 7. Distribution of b in the air gap with a reduced central hole

Fig. 8 .

 8 Fig. 8. Distribution of b in the air-gap IV. RESULTS AND DISCUSSION The section III has shown what the influent parameters are. Let us analyse the two zones, keeping in mind that the flux "tries" to follow the RD as longest as possible. Concerning the first zone, the flux tends, as it has been sensed in section II, to be in the RD. Then, it goes down or up through the air gap to the RD of the adjacent sheet. That explains well the distribution of b in the air gap between the RD of two nearby sheets, as shown in Fig. 9 with the dotted blue path. This figure , where the ring has a small internal radius allows understanding the flux distribution. The central hole acts as a buttress for the flux, which can not continue into the RD. As a consequence, although passing through the TD of the same sheet, it passes the air gap for being in the RD of the next sheet. When the internal radius is close to the external

Fig. 9 .

 9 Fig. 9. Scheme of the flux path with a small central hole

Fig. 10 .

 10 Fig. 10. Scheme of the flux path with a large central hole laminations. Moreover, these conclusions can be very usefull in order to calculate the losses in such structures as well as they allow finding explanations on how the Maxwell forces and the magnetostriction forces occur between the sheets and in the magnetic circuit respectively.

TABLE I

 I

				EXPERIMENTAL VALUES
	Sensor	1	2	3	4	5	6	7	8	9
	Sensor
	Voltage 34.2 31.2	124 41.3 15.5 79.6 92.8 19.8	68
	(µV)
	B (mT) 18.1 16.5	66.1 21.9 82.3 42.3 49.2 10.5 36.1
	Phase
	lag ( ) Ref -172.7 -179.1 -176 -5.3 0.1 -10.4 -169.1 -73.8

, from the RDs. But due to the annular shape of the sheets, the flux meets the border of the laters before 45 , leading to a concentration on the external border.The second and third zones are more unexpected. Indeed, in the zone 2 close to the central hole, there is a concentration of flux density similar to the first zone, but with an opposed direction. This internal border is rather unusual. Finaly, there is almost no flux in the zone

ACKNOWLEDGMENT This work is supported by MEDEE program supervised by the French national technological research cluster on electrical machine efficiency increase. This program, including ThyssenKrupp Electrical Steel, is sponsored by the region Nord Pas-de-Calais (France), the French ministry and the European founds (FEDER).