Hans Van Ditmarsch

Ji Ruan
email: j.ruan@csc.liv.ac.uk

Model Checking Logic Puzzles

Keywords: communications multi-agent, vérification des modèles, logique dynamique épistémique, annonce publique agent communication, model checking, dynamic epistemic logic, public announcement

Dans les puzzles épistémiques les annonces d'ignorance, ou des séquences de tels annonces, souvent résultent en connaissances. Nous présentons le puzzle 'Quelle Somme ?', et le modèlisent dans la logique des annonces publiques -un langage logique avec des opérateurs dynamiques et épistémiques. La solution du puzzle est controlée avec la programme de vérification DEMO.

Introduction

The following riddle (transcribed in our terminology) appeared in Math Horizons in 2004, as 'Problem 182' in a regular problem section of the journal, edited by A. Liu [START_REF] Liu | Problem section: Problem 182[END_REF].

Each of agents Anne, Bill, and Cath has a positive integer on its forehead. They can only see the foreheads of others. One of the numbers is the sum of the other two. All the previous is common knowledge. The agents now successively make the truthful announcements: i. Anne: "I do not know my number. "

ii. Bill: "I do not know my number. "

iii. Cath: "I do not know my number. " iv. Anne: "I know my number. It is 50. "

What are the other numbers?

You know your own number if and only if you know which of the three numbers is the sum. This 'What is the sum?', from now on 'What Sum', riddle combines features from wisemen or Muddy Children puzzles [START_REF] Moses | Cheating husbands and other stories: a case study in knowledge, action, and communication[END_REF] with features from the Sum and Product riddle [START_REF]formulation of the sumand-product problem)[END_REF][START_REF] Mccarthy | Formalization of two puzzles involving knowledge[END_REF]. A common feature in such riddles is that we are given a multi-agent interpreted system, and that successive announcements of ignorance finally result in its opposite, typically factual knowledge. In a global state of an interpreted system [START_REF] Fagin | Reasoning about Knowledge[END_REF] each agent or processor has a local state, and there is common knowledge that each agent only knows its local state, and what the extent is of the domain. If the domain consists of the full cartesian product of the sets of local state values, it is common knowledge that agents are ignorant about others' local states. In that case an ignorance announcement has no informative value. For ignorance statements to be informative, the domain should be more restrictive than the full cartesian product; and this is the case in all such riddles. As in Muddy Children, we do not take the 'real' state of the agent (the number on its forehead) as its local state, but instead the information seen on the foreheads of others (the other numbers). This change of perspective is, clearly, inessential. 'Sum and Product' 2 is also about numbers, and even about sums of numbers, and the announcements are similar. But the structure of the background knowledge is very different (which will become clearer after introducing the logic to describe both riddles).

Other epistemic riddles involve cryptography and the verification of information security protocols ('Russian Cards', see [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]), or involve communication protocols with private signals involving diffusion of information in a distributed environment ('100 prisoners and a lightbulb', see [START_REF] Wu | 100 prisoners and a lightbulb[END_REF]).

The understanding of such riddles is facilitated by the availability of suitable specification languages. For 'What Sum' we propose the logic of public announcements, wherein succinct descriptions in the logical language are combined with convenient relational structures on which to interpret them. We also benefit from the availability of verification tools, to aid interpreting such descriptions on such structures. In our case we have used DEMO, an epistemic model checker developed by Van Eijck (see homepages.cwi.nl/ ~jve/demo/ and [START_REF] Van Eijck | Dynamic epistemic modelling[END_REF]). Some adjustments are required (we need a finite version of the model) to make this model checking work. This results in possibly in- 2 A says to S and P : I have chosen two integers x, y such that 1 < x < y and x + y ≤ 100. In a moment, I will inform S only of s = x+y, and P only of p = xy. These announcements remain private. You are required to determine the pair (x, y).

He acts as said. The following conversation now takes place: i. P says: "I do not know it. "

ii. S says: "I knew you didn't. "

iii. P says: "I now know it. " iv. S says: "I now also know it. "

Determine the pair (x, y). [3, translated] teresting versions of the riddle.

Even though such riddles are often pivotal to the development and spreading of a specialisation area-who doesn't know about the 'Muddy Children' puzzle?-the detailed and rockbottom analysis of their highly proceduralised features is not necessarily considered a serious enough pursuit to increase our understanding of multiagent system dynamics. May our original analysis of 'What Sum' be seen as a worthy contribution.

Section 2 provides an introduction into public announcement logic, and in Section 3 we analyse 'What Sum' in this logic. Section 4 'preprocesses' the riddle for model checking and discusses some versions of the riddle. In Section 5 we introduce DEMO, and in Section 6 we specify and verify a finite version of the riddle in that model checker.

Public Announcement Logic

Public announcement logic is a dynamic epistemic logic and is an extension of standard multi-agent epistemic logic. Intuitive explanations of the epistemic part of the semantics can be found in [START_REF] Fagin | Reasoning about Knowledge[END_REF][START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. We give a concise overview of, in that order, the language, the structures on which the language is interpreted, and the semantics.

Given are a finite set of agents N and a finite or countably infinite set of atoms P . The language of public announcement logic is inductively defined as For the semantics, assuming an epistemic model M = S, ∼, V :

ϕ ::= p | ¬ϕ | (ϕ ∧ ψ) | K n ϕ | C B ϕ | [ϕ]
M, s | = p iff s ∈ V p M, s | = ¬ϕ iff M, s | = ϕ M, s | = ϕ ∧ ψ iff M, s | = ϕ and M, s | = ψ M, s | = K n ϕ iff for all t ∈ S : s ∼ n t implies M, t | = ϕ M, s | = C B ϕ iff for all t ∈ S : s ∼ B t implies M, t | = ϕ M, s | = [ϕ]ψ iff M, s | = ϕ implies M|ϕ, s | = ψ where model M|ϕ = S ′ , ∼ ′ , V ′ is de- fined as S ′ = {s ′ ∈ S | M, s ′ | = ϕ} ∼ ′ n = ∼ n ∩ (S ′ × S ′ ) V ′ p = V p ∩ S ′
The dynamic modal operator [ϕ] is interpreted as an epistemic state transformer. Announcements are assumed to be truthful, and this is commonly known by all agents. Therefore, the model M|ϕ is the model M restricted to all the states where ϕ is true, including access between states.

The dual of

[ϕ] is ϕ : M, s | = ϕ ψ iff M, s | = ϕ and M|ϕ, s | = ψ. Formula ϕ is valid on model M, notation M | = ϕ,
iff for all states s in the domain of M: M, s | = ϕ. Formula ϕ is valid, notation | = ϕ, iff for all models M: M | = ϕ.

A proof system for this logic is presented, and shown to be complete, in [START_REF] Baltag | The logic of public announcements, common knowledge, and private suspicions[END_REF], with precursors-namely for public announcement logic without common knowledgein [START_REF] Plaza | Logics of public communications[END_REF][START_REF] Gerbrandy | Bisimulations on Planet Kripke[END_REF]. A concise completeness proof is given in [START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. The logic is decidable both with and without common knowledge [START_REF] Plaza | Logics of public communications[END_REF][START_REF] Baltag | The logic of public announcements, common knowledge, and private suspicions[END_REF]. Results on the complexity of both logics can be found in [START_REF] Lutz | Complexity and succinctness of public announcement logic[END_REF]. The original [START_REF] Plaza | Logics of public communications[END_REF] also contains a version of the semantics (no completeness results) with 'knowvalue'-operators that can be said to formalise infinitary conjunctions (or disjunctions), including announcements of such formulas with corresponding restriction of the domain to those states where the formula is true. To analyse 'What Sum' we need to refer to that extension (that we prefer to leave informal for the sake of the exposition).

In public announcement logic, not all formulas remain true after their announcement, in other words, [ϕ]ϕ is not a principle of the logic. Some formulas involving epistemic operators become false after being announced! For a simple example, consider that Bill were to tell Anne (truthfully) at the initial setting of the riddle: "Your number is 50 but you don't know that." Interpreting 'but' as a conjunction, this is formalised as 50 a ∧ ¬K a 50 a . After the announcement, Anne knows that her number is 50: K a 50 a . Therefore the announced formula, that was true before the announcement, has become false after the announcement. In the somewhat different setting that formulas of form p ∧ ¬K n p cannot be consistently known this phenomenon is called the Moore-paradox [START_REF] Moore | A reply to my critics[END_REF][START_REF] Hintikka | Knowledge and Belief[END_REF]. In the underlying dynamic setting it has been described as an unsuccessful update [START_REF] Gerbrandy | Bisimulations on Planet Kripke[END_REF][START_REF] Van Ditmarsch | Dynamic Epistemic Logic[END_REF]. Similarly, ignorance statements in 'What Sum' such as Anne saying that she does not know her number, may in due time lead to Anne knowing her number, the opposite of her ignorance.

Formalisation of 'What Sum'

The set of agents {a, b, c} represent Anne, Bill and Cath, respectively. Atomic propositions i n represent that agent n has natural number i on its forehead. Therefore the set of atoms is {i n | i ∈ N + and n ∈ {a, b, c}}.

If Anne sees (knows) that Bill has 20 on his forehead and Cath 30, we describe this as K a (20 b ∧ 30 c ). If an upper bound max for all numbers were specified in the riddle, the number of states would be finite and "knowing the others' numbers" would be described as y,z≤max K a (y b ∧ z c ). For model checking it is relevant to point out that this expression is equiva-

lent to y,z≤max (y b ∧ z c ) → K a (y b ∧ z c ),
given that different Bill/Cath number pairs are mutually exclusive, and using standard validities for the logic. The latter form is 'cheaper' to model check than the for-mer, because the truth of the boolean condition in the conjuncts of the latter can be determined in a given state, whereas an epistemic statement requires checks in that agent's entire equivalence class.

For 'What Sum', Anne seeing the numbers of Bill and Cath is therefore described as the infinitary y,z∈N + K a (y b ∧ z c ), and Anne saying: "I don't know my number" is similarly described as

¬ x∈N + K a x a (or x∈N + (x a → ¬K a x a )
). Infinitary descriptions are, unlike infinitely large models, not permitted in this (propositional) logic. Our model checking results will be for a finite version of the riddle.

The epistemic model T = S, ∼, V is defined as follows, assuming positive natural numbers x, y, z.

S ≡ {(x, y, z) | x = y+z or y = x+z or z = x+y} (x, y, z) ∼ a (x ′ , y ′ , z ′ ) iff y = y ′ and z = z ′ (x, y, z) ∼ b (x ′ , y ′ , z ′ ) iff x = x ′ and z = z ′ (x, y, z) ∼ c (x ′ , y ′ , z ′ ) iff x = x ′ and y = y ′ (x, y, z) ∈ V xa (x, y, z) ∈ V yb (x, y, z) ∈ V zc
The fine-structure of the epistemic model T is not apparent from its formal definition. A relevant question is what the background knowledge is that is available to the agents, i.e., what the abc-classes in the model are (an abc-class, or {a, b, c} equivalence class, of a state s in the model consists of all states t such that s ∼ {a,b,c} t, where ∼ {a,b,c} = (∼ a ∪ ∼ b ∪ ∼ c ) * , as above). Such a computation was performed by Panti [START_REF] Panti | Solution of a number theoretic problem involving knowledge[END_REF] for 'Sum and Product' (see footnote 2), which revealed three classes: either (in two of the three classes) the solution of the problem is already common knowledge in the initial state, or the agents commonly know that the sum of the numbers is at least 7. This means that in 'Sum and Product' not very much is commonly known. In contrast, a model T for 'What Sum' has a very different structure, with many more common knowledge classes. It is therefore quite informative to know what they are, and we will describe them in detail.

An abc-class in T can be visualised as an infinite binary tree. The depth of the tree reflects the following order on number triples in the domain of T : (x, y, z) > (u, v, w) iff (x > u and y = v and z = w) or (x = u and y > v and z = w) or (x = u and y = v and z > w). If (x, y, z) > (u, v, w) according to this definition, (x, y, z) is a child of (u, v, w) in that tree. Every node except the root has one predecessor and two successors, as in Figure 1. The root of each tree has label (2x, x, x) or (x, 2x, x) or (x, x, 2x). Differently said, given three natural numbers such that one is the sum of the other two, replace that sum by the difference of the other two; one of those other two has now become the sum; if you repeat the procedure, you always end up with two equal numbers and their sum. An agent who sees two equal numbers, immediately infers that its own number must be their sum (twice the number that is seen), because otherwise it would have to be their difference 0 which is not a positive natural number. It will be obvious that: the structure truly is a forest (a set of trees), because each node only has a single parent; all nodes except roots are triples of three different numbers; and all trees are infinite. All abc-trees are isomorphic modulo (i) a multiplication factor for the numbers occurring in the arguments of the node labels, and modulo (ii) a permutation of arguments and a cor-responding swap of agents, i.e., swap of arc labels. For example, the numbers occurring in the tree with root (6, 3, 3) are thrice the corresponding numbers in the tree with root (2, 1, 1); the tree with root (2, 1, 1) is like the tree for root (1, 2, 1) by applying permutation (213) to arguments and (alphabetically ordered) agent labels alike. The left side of Figure 3 shows the trees with roots (2, 1, 1), (1, 2, 1), and

(1, 1, 2). For simplicity, we write 211 instead of (2, 1, 1), etc. In the left tree, for Bill (2, 1, 1) is indistinguishable from (2, 3, 1) wherein his number is the sum of the other two instead of their difference; for Anne triple (2, 3, 1) is indistinguishable from (4, 3, 1), etc.

Processing Announcements The result of an announcement (whether described infinitary or not) is the restriction of the model to all states where the announcement is true. We can also apply this to the ignorance announcements of agents in 'What Sum'. Consider an abc-tree T in T . Let n be an arbitrary agent. Either the root of T is a singleton n-class, or all its nclasses consist of two elements: a twoelement class represents the agent's uncertainty about its own number. An ignorance announcement by agent n in this riddle corresponds to removal of all singleton nclasses from the model T . This means that some of the model's trees are split into two subtrees (with both children of the original root now roots of infinite trees).

An ignorance announcement may have very different effects on abc-classes that are the same modulo agent permutations. For example, given abc-classes in T with roots 121, 112, and 211, the effect of Anne saying that she does not know her number only results in elimination of 211, as only the first abc-class contains an a-singleton.

Given 211, Anne knows that she has number 2 (as 0 is excluded). But triple 112 she cannot distinguish from 312, and 121 not from 321. Thus one proceeds with all three announcements. See also Figure 2.

Solving the riddle

We have now sufficient background to solve the riddle. We apply the successive ignorance announcements to the three classes with roots (2, 1, 1), (1, 2, 1), and (1, 1, 2), determine the triples wherein Anne knows the numbers, and from those, wherein Anne's number divides 50. See Figure 3 The original riddle could have more restrictive: in the quoted version [START_REF] Liu | Problem section: Problem 182[END_REF] it is not required to determine who holds which other number, but as we have seen this can also be determined. It also occurred to us that the original riddle could have been posed differently (and we tend to think, far more elegantly) as follows: Consulting Figure 3, it will be obvious that the answer should be: '5, 2, and 3'.

Each

Towards Model Checking

To be able to use a model checker we need a finite approximation of the model. Suppose we use an upper bound max for the numbers. Let T max be the corresponding epistemic model. An abc-tree is now cut at the depth where nodes (x, y, z) occur such that the sum of two of the arguments x, y, z exceeds max. This finite approximation may not seem a big deal but it makes the problem completely different: abc-classes will not just have roots wherein the agent may know his number (because the other numbers are equal) but will also have leaves wherein the agent may know his number (because the sum of the other two numbers exceeds max).

In other words, we have far more singleton equivalence classes. Let max = 10. Node (2, 5, 7) in the abc-class with root (2, 1, 1) has only a b-child (2, 9, 7) and a c-parent (2, 5, 3), and not an a-child, as 5 + 7 = 12 > max. So Anne immediately knows that her number is 2. All roots (2x, x, x) with 3x > max form singleton abc-classes in T max , for the same reason.

In such models it is no longer the case that all equivalence classes are isomorphic modulo a multiplication factor and swapping of agent labels. For a given upper bound max we still have that, if x > y, the abc-class T with root (2x, x, x) is a prefix (in a partially ordered sense) of the abcclass T ′ with root (2y, y, y), which implies that T ⊆ T ′ (modulo a factor y x for numbers occurring in T ). For different upper bounds max, max ′ we have that (literally)

T max ⊆ T max ′ iff max ≤ max ′ .
Under these circumstances it is less clear what constitutes an exhaustive search of 'all possibilities that remain after an announcement'. Fortunately, we are now talking about formal announcements in the language of public announcement logic. The following non-trivial result is essential. Let T, T ′ be different epistemic mod-els T for 'What Sum' (i.e., for different upper bounds max) or, modulo a multiplication factor, different abc-classes in a given T model.

If T ⊆ T ′ and ϕ is a sequence of ignorance announcements executable in both T and

T ′ , then T | ϕ ⊆ T ′ | ϕ.
The proof is simple, and by induction on the number of such announcements. Consider a next ignorance announcement ψ being made, by agent n. As said, it removes singleton equivalence classes for that agent. If T ⊆ T ′ it may be that some singleton n-classes in T were twostate n-classes in T ′ . These will therefore be omitted when executing the announcement of ψ in T , whereas they would have been preserved when executing the same announcement in T ′ . There are no other differences in execution: all nclasses that were singleton in both T and T ′ will be omitted anyway as a result of the ψ-announcement. Therefore, we still have that T |ψ ⊆ T ′ |ψ.

This may seem obvious. But it is far from that: for arbitrary M ′ ⊆ M and arbitrary ϕ we do not have that M ′ |ϕ ⊆ M|ϕ. Let us give a counterexample. Given agents a, b and state variables p, q (in 10 p is true and q is false) consider the (two-state) model M ′ = 11|a|10, which is a restriction of the (three state) model M = 11|a|10|b|01. Consider ϕ = K b q∨K b ¬q, for 'Bill knows whether q.' Then M ′ |ϕ = M ′ , whereas M|ϕ is the singleton model consisting of state 11 wherein a and b have common knowledge of p and q. Therefore M ′ ⊆ M but M ′ |ϕ ⊆ M|ϕ.

Apart from having an upper bound we discuss one other, less essential, change: suppose we start counting from 0 instead of 1. In that case each abc-equivalence class with root (2x, x, x) is extended with one more node: the new root (0, x, x) is indistinguishable from (2x, x, x) for Anne. An agent who sees a 0, infers that his number must be the other number that (s)he sees. If there is a 0, two of the three agents see that. Therefore, the root has just one child (2x, x, x); if the triple is (0, x, x) Bill and Cath know that their number is x. 3 The abc-class with root 011 from the epistemic model T 10 0 (upper bound 10, lower bound 0) is displayed on the left in Fig- ure 4. The result of the three ignorance announcements is displayed on the right. We can now investigate different versions of the problem. The model checker is then helpful because some versions are hard to verify with pencil and paper, or mere mental computation. For example, we considered the version: If 0 ≤ x, y, z ≤ max, for which values of max does Anne always know the numbers after the three announcements? This range is 8 ≤ max ≤ 13 (so, for 7 not all three announcements can be made truthfully, and for 14 it may be that Anne does not know her number) and this includes max = 10. Figure 4 shows that from abc-class with root 011 the triples 211 and 213 remain. In both cases Anne knows her number. Similar computations show that from the abcclasses with root 101 and 110 no triples remain. In other words, the announcements could not all three have been made (truthfully) if the number triple occurs in either of those two classes. Using the properties of inclusion for different abc-classes, we have now ruled out all classes of type x0x and xx0 and only have to check other classes of type 0xx. From class 022, the triples 242 and 246 remain after the three announcements (and the ones with root 033 and beyond are empty again). Therefore, whatever the numbers, Anne now 3 Suppose there is no upper bound but 0 is still allowedevery audience being presented with this riddle for positive integers contains at least one person asking if 0 is allowed. This is an interesting variation. Anne will still learn her own number if it is 50 from the three ignorance announcements, but the reader ('problem solver') can now no longer deduce Bill's and Cath's number in that case: these can now also be 25 and 25. The reader should be able to determine this easily by contemplating Figure 3. From the models resulting from the three ignorance announcements, only one now looks different. Which one? knows her number. But the problem solver cannot determine what that number is (it may be 1, or it may be 2) and also cannot determine what the other numbers are, not even if it is also known what Anne's number is (if it is 1, the other numbers may be 2 and 1, or 2 and 3; and similarly if it is 2).

Model Checker DEMO

Epistemic model checkers with dynamic facilities have been developed to verify properties of interpreted systems, knowledge-based protocols, and various other multi-agent systems. Examples are MCK [START_REF] Gammie | MCK: Model checking the logic of knowledge[END_REF], MCMAS [START_REF] Raimondi | Verification of multiagent systems via ordered binary decision diagrams: An algorithm and its implementation[END_REF], and recent work by Su [START_REF] Su | Model checking temporal logics of knowledge in distributed systems[END_REF]. All those model checkers use the interpreted systems architecture, and exploration of the search space is based on ordered binary decision diagrams. Their dynamics are expressed in temporal or temporal epistemic (linear and/or branching time) logics.

A different model checker, not based on a temporal epistemic architecture, is DEMO. It has been developed by Van Eijck [START_REF] Van Eijck | Dynamic epistemic modelling[END_REF]. DEMO is short for Dynamic Epistemic MOdelling. It allows modelling epistemic updates, graphical display of Kripke structures involved, and formula evaluation in epistemic states. This general purpose model checker has also many other facilities. DEMO is written in the functional programming language Haskell.

The model checker DEMO implements the dynamic epistemic logic of [START_REF] Baltag | The logic of public announcements, common knowledge, and private suspicions[END_REF]. In this 'action model logic' the global state of a multi-agent system is represented by an epistemic model. But more epistemic actions are allowed than just public announcements, and each epistemic action is represented by an action model. Just like an epistemic model, an action model is also based on a multi-agent Kripke frame, but instead of carrying a valuation it has a precondition function that assigns a precondition to each point in the action model. A point in the action model domain stands for an atomic action.

The epistemic state change in the system is via a general operation called the update product: this is a way to produce a single structure (the next epistemic model) from two given structures (the current epistemic model and the current action model). We do not give details, as we restrict our attention to very simple action models, namely those corresponding to public announcements. Such action models have a singleton domain, and the precondition of that point is the announced formula. The next epistemic model is produced from the current epistemic model and the singleton action model for the announcement by the model restriction introduced in Section 2.

The recursive definition of formulas in DEMO includes (we omitted the clause for updates)

Form = Top | Prop Prop | Neg Form | Conj [Form] | Disj [Form] | K Agent Form | CK
[Agent] Form . Formula Top stands for ⊤, Prop Prop for atomic propositional letters (the first occurrence of Prop means that the datatype is 'propositional atom', whereas the second occurrence of Prop is the placeholder for an actual proposition letter, such as P 3), Neg for negation, Conj [Form] stands for the conjunction of a list of formulas of type Form, similarly for Disj, K Agent stands for the individual knowledge operator for agent Agent, and CK [Agent] for the common knowledge operator for the group of agents listed in

[Agent].
The pointed and singleton action model for a public announcement is created by a function public with a precondition (the announced formula) as argument. The update operation is specified as upd :: EpistM -> PoAM -> EpistM ; here EpistM is an epistemic state and PoAM is a pointed action model, and the update generates a new epistemic state. If the input epistemic state EpistM corresponds to some (M, s), then in case of the truthful public announcement of ϕ the resulting EpistM has the form (M|ϕ, s). We can also update with a list of pointed action models: upds :: EpistM -> [PoAM] -> EpistM .

Complexity Each model restriction M|ϕ requires determining the set {s ∈ D(M) | M, s | = ϕ}. Given a model M, a state s, and a formula ϕ, checking whether M, s | = ϕ can be solved in time O(|M| × |ϕ|), where |M| is the size of the model as measured in the size of its domain plus the number of pairs in its accessibility relations, and where |ϕ| is the length of the formula ϕ. This result has been established by the well-known labelling method [START_REF] Halpern | Model checking vs. theorem proving: a manifesto[END_REF][START_REF] Fagin | Reasoning about Knowledge[END_REF]. This method is based on dividing ϕ into subformulas. One then orders all these subformulas, of which there are at most |ϕ|, by increasing length. For each subformula, all states are labelled with either the formula or its negation, according to the valuation of the model and based on the results of previous steps. This is a bottomup approach, in the sense that the labelling starts from the smallest subformulas. So it ensures that each subformula is checked only once in each state.

In DEMO (v1.02) the algorithm to check whether M, s | = ϕ does not employ this bottom-up approach. Instead, it uses a top-down approach, starting with the formula ϕ and recursively checking its largest subformulas. For example, to check whether M, s | = K a ψ, the algorithm checks whether M, s ′ | = ψ for all s ′ such that s ∼ a s ′ , and then recursively checks the subformulas of ψ. This algorithm is O(|M| |ϕ| ), since each subformula may need to be checked |M| times, and there are at most |ϕ| subformulas of ϕ. So, theoretically, DEMO's algorithm is quite expensive.

In practice it is less expensive, because the Haskell language and its compiler and interpreter support a cache mechanism: after evaluating a function, it caches some results in memory for reuse (see e.g. [START_REF] Nethercote | The cache behaviour of large lazy functional programs on stock hardware[END_REF]). Since it is hard to predict what results will be cached and for how long, we cannot give an estimate how much the cache mechanism influences the computational results for DEMO. See also [START_REF] Van Ditmarsch | Sum and product in dynamic epistemic logic[END_REF]. Computational results for the experiments in the next section are given in footnote 5.

'What Sum' in DEMO

The DEMO program SUMXYZ.hs, displayed in Figure 5, implements the 'What Sum' problem for upper bound max = 10. 4The list triples = triplesx ++ triplesy ++ triplesz (this is a union (++) of three lists) corresponds to the set of possible triples (x, y, z) for the given bound 10-note that in Haskell we are required to define such sets as lists. The next part of the program constructs the domain based on that list: this merely means that each member of the list must be associated with a state name.

that state number 67 corresponds to triple (6, 8, 2). Given (43,[p10, q8, r2]) we now find (a,43,67) in acc.

Anne's announcement that she does not know her number is represented as the action model aagxnot constructed from the announcement formula fagxnot by the function public. The last corresponds to ¬x a ∨ ¬K a x a , which is equivalent to x a → ¬K a x a . Therefore, the whole expression corresponds to 0≤x≤10 x a → ¬K a x a . This is the computationally cheaper version also formalised as ¬ 0≤x≤10 K a x a , see Section 3.

The final line in the program asks to display the results of the three ignorance announcements. Its output is States are sequentially renumbered starting from 0 after each update. The four remaining triples 211, 132, 134, and 213 are clearly shown, see also Figure 4. Anne always knows her number, as her partition on the set of four states is the identity (and so does Bill, but not Cath). 5 5 We did experiments in a PC configured as Windows XP, AMD CPU 1.8Ghz, with 1G RAM. We use the Glasgow Haskell Compiler Interactive (GHCi) version 6.4.1, enabling the option ":set +s" to display information after evaluating each expression, including the elapsed time and number of bytes allocated. The results for time and space consumption of the crucial upds msnp [aagxnot,aagynot,aagznot] are as follows: for upb=10, time: 1.59 seconds, and space: 29,075,432 bytes; to give an impression of how this scales up: for upb=20, time: 30.31 seconds, and space: 334,474,032 bytes; for upb=30, time: 193.20 seconds, and space: 1,706,593,672 bytes.

We hope that this rather summary overview of DEMO nevertheless reveals its enormous versatility as a model checker. E.g., to check which states remain when a different upper bound is chosen, one merely has to replace the line upb = 10 in the program by that other upper bound. In general, the enormous advantage of this model checker is that it allows for a separate specification of the initial model and the subsequent dynamic features, as in the original riddle (and, typically, as in the specification of the dynamics of a multiagent system to be formally modelled).

Conclusions

We presented an original analysis of an epistemic riddle, and formalised a finite version of the riddle with the use of public announcement logic and epistemic model checking. Crucial in the analysis was to model the riddle as an interpreted system, and to focus on the description of the background knowledge, i.e., abc-equivalence classes of the epistemic model. We introduced the model checker DEMO and the specification of the riddle in DEMO.

We think that detailed analysis of logic puzzles contributes to the understanding of logical tools and formalisms, and how to apply them to model multiagent system dynamics. In particular, the specification of security protocols in DEMO is, we think, promising. In our experiences with specifying such protocols, DEMO compares favourably to other state-of-theart model checkers MCK and MCMASof course we would not dare to suggest that DEMO is 'better': when specifying a problem in which public announcements are essential, it is not surprising that a tool specially developed for such dynamics functions well.

Future development of DEMO may involve (Jan van Eijck, personal communi-cation) facilities to model not merely information change, such as incoming new information, but also factual change. This would expand the use of this tool to model planning protocols, security protocols that include key exchange, etc. We are much looking forward to that development.

Figure 1 :

 1 Figure 1: Modulo agent symmetry, all parts of the model T branch as here. Arcs connecting nodes are labelled with the agent who cannot distinguish those nodes.

Figure 2 :

 2 Figure 2: The results of three ignorance announcements on the abc-class with root (2, 1, 1).

Figure 3 :

 3 Figure 3: On the left, abc-classes of the model T with root 211, 121, and 112. Any other abc-class is isomorphic to one of these, modulo a multiplication factor. The results of the (combined) three ignorance announcements on those abc-classes are on the right. The triples in bold are those where Anne knows her number.

Figure 4 :

 4 Figure 4: The abc-class with root 011 in model T 10 0 , and the result of three ignorance announcements. The horizontal order of branches has no meaning. Symbol A represents 10.

  [p2,q1,r1])(1,[p1,q3,r2]) (2,[p1,q3,r4])(3,[p2,q1,r3]) (a,[[0],[1],[2],[3]]) (b,[[0],[1],[2],[3]]) (c,[[0,3],[1,2]])

  Anne has the number 50.' For C B ϕ, read 'group of agents B commonly know formula ϕ'. For example, we have that C abc (20 b → K a 20 b ): it is common knowledge to Anne, Bill, and Cath, that if Bill's number is 20, Anne knows that (because she can see Bill's number on his forehead)-instead of {a, b, c} we often write abc. For [ϕ]ψ, read 'after public announcement of ϕ, formula ψ (is true)'. For example, after Anne announces "(I know my number. It is 50.)" it is common knowledge that Bill's number is 20. This is formalised as [K a 50 a ]C abc 20 b .

	-
	bility ∼ : N → P(S × S), where each ∼(n) is an equivalence relation, and a val-uation V : P → P(S). For s ∈ S, (M, s) is an epistemic state (also known as a pointed Kripke model). For ∼ (n) we write ∼ n , and for V (p) we write V p . Ac-cessibility ∼ can be seen as a set of equiv-alence relations ∼ n , and V as a set of val-uations V p . Given two states s, s ′ in the domain, s ∼ n s ′ means that s is indistin-guishable from s ′ for agent n on the basis
	of its information. For example, at the be-
	ginning of the riddle, triples (2, 14, 16) and (30, 14, 16) are indistinguishable for Anne
	but not for Bill nor for Cath. Therefore, as-
	suming a domain of natural number triples,
	we have that (2, 14, 16) ∼ a (30, 14, 16). The group accessibility relation ∼ B is the
	transitive and reflexive closure of the union
	of all accessibility relations for the individ-uals in B: ∼ B ≡ ( n∈B ∼ n ) * . This re-lation is used to interpret common knowl-
	edge for group B. Instead of '∼ B equiv-
	alence class' (∼ n equivalence class) we write B-class (n-class).

ψ where p ∈ P , n ∈ N, and B ⊆ N are arbitrary. Other propositional and epistemic operators are introduced by abbreviation. For K n ϕ, read 'agent n knows formula ϕ'. For example, if Anne knows that her number is 50, we can write K a 50 a , where a stands for Anne and some set of atomic propositions is assumed that contains 50 a to represent '

The basic structure is the epistemic model. This is a Kripke structure, or model, wherein all accessibility relations are equivalence relations. An epistemic model M = S, ∼, V consists of a domain S of (factual) states (or 'worlds'), accessi

  In other words, the unique abctree in the entire model T where Anne knows that she has 50 after the three ignorance announcements, is the one with root[START_REF] Mccarthy | Formalization of two puzzles involving knowledge[END_REF][START_REF] Van Eijck | Dynamic epistemic modelling[END_REF][START_REF] Mccarthy | Formalization of two puzzles involving knowledge[END_REF]. The solution to the riddle is therefore that Bill has 20 and Cath has 30. After the three announcements in the abc-class with root[START_REF] Mccarthy | Formalization of two puzzles involving knowledge[END_REF][START_REF] Van Eijck | Dynamic epistemic modelling[END_REF][START_REF] Mccarthy | Formalization of two puzzles involving knowledge[END_REF], the triple (50, 20, 30) remains wherein Anne knows that Bill has 20 and Cath 30.

	-note that in triple (8, 3, 5) Anne also knows her num-ber: the alternative (2, 3, 5) wherein her number is 2 has been eliminated by Cath's, last, ignorance announcement. The unique triple wherein Anne's number divides 50 is (5, 2, 3). 211 231 431 235 451 437 835 275 . . . . . . . . . . . . b c 213 413 473 . . . a c a b b c a b b c 121 321 123 341 325 143 541 347 385 725 743 . . . . . . . . . . . . . . . a c b c b a a c b a a c 112 132 312 134 532 314 b a c a c b b a c b b a 154 734 538 572 374 . . . . . . . . . . . . . . .	253 415 . . . 523 145 . . . 352 514 . . .	853 . . . a c 583 . . . b c c a 358 . . .	257 . . . 527 . . . 752 . . .	451 . . . 541 . . . 154 . . .	437 . . . b c 347 . . . a c 734 . . .	431 835 . . . 341 385 . . . 134 538 . . .	275 . . . 321 325 725 . . . b c b a 132 532 572 . . .	413 473 . . . b c 143 743 . . . a c 312 314 374 . . .	253 415 . . . 523 145 . . . 352 514 . . .	853 . . . a c 583 . . . b c 358 . . .	257 . . . 527 . . . 752 . . .

We acknowledge input from David Atkinson, Jan van Eijck, Wiebe van der Hoek, Barteld Kooi, and Rineke Verbrugge. We thank the anonymous MFI referees for their comments. Hans appreciates support from the NIAS (Netherlands Institute for Advanced Study in the Humanities and Social Sciences) project 'Games, Action, and Social Software' and the NWO (Netherlands Organisation for Scientific Research) Cognition Program for the Advanced Studies grant NWO 051-04-120.

The program is original but should be considered a version of the DEMO program for 'Sum and Product' in[START_REF] Van Ditmarsch | Sum and product in dynamic epistemic logic[END_REF].

State names must be consecutive numbers, counting from 0. The association is explicit in the list itriples that consists of pairs of which the first argument is a number (from the list [0..numtriples-1]) and the second argument is one of the triples (x, y, z) in the list triples. The initial model T 10 0 is then represented as three in the program. The expression (Pmod [0..numtriples-1] val acc [0..numtriples-1]) defines three as an epistemic model (Pmod), with domain [0..numtriples-1], valuation val, a set (list) of accessibility relations acc (and [0..numtriples-1] points-left unexplained here). In val we find for example (67,[p6, q8, r2]) which says


Hubert Olivier

Lavernhe-Taillard Karine

FALL Mame - Daro

Chang Xuyang

Savary Maxime

Sevestre Olivia
email: fsevestre@lmt.ens-cachan.fr

Multiscale approach for the modeling of chemo-magneto-thermomechanical couplings -reversible framework

Keywords: multiscale, multiphysics, coupled constitutive laws, sensors and actuators

We focus in this paper on a multiscale modeling approach of the materials' reversible behavior involving couplings of the chemo-magneto-thermo-mechanical type. It is shown that it is possible to take into account a large variety of these coupled environments by a unified approach using the springs of the scale change and the build of an appropriate Gibbs free energy function. The approach is well suited to situations where some fields can be considered homogeneous at a relevant scale and where free deformation can be defined.

Introduction

Our time is characterized by an increasingly intensive use of actuators in extremely large fields of applications, from the largest to the smallest scales. The miniaturization of these systems adds new design constraints and requires the development of materials with controlled properties and robust models. One of the solutions being considered is the use of material exhibiting at least one strong multiphysic coupling (one of the physic being mechanics). This includes magnetostrictive materials [1], classical (SMA) or magnetic shape memory alloys (MSMA) [START_REF] Lexcellent | Shape-Memory Alloys Handbook[END_REF], piezoelectric materials, multiferroic composite media, etc. One of the modeling challenges is to better describe the complex interactions observed experimentally (nonlinearity, non-monotony, irreversibly, dynamic and multiaxial effects etc ...), and to derive constitutive models with sufficient domains of validity for the considered applications. A multiscale model of a representative volume element (RVE) of such materials is proposed. It is relevant for multiaxial stress, thermal and magnetic loadings in a pseudoreversible framework (heat exchange can be considered for instance). The objective of the paper is to recall the main hypotheses and principles required to develop this modeling. The reader will be able to find some practical examples and applications of this modeling approach in the different references added all along the text.

Gibbs free energy at the magnetic domain family scale

In the following, g denotes a grain. It is supposed to be composed of several phases ! (typically austenite, martensite). ! denotes a variant meaning that a phase ! can develop different variants depending on its symmetry; ! denotes a magnetic domain family inside the variant ! and represents the lower scale. The scale organization is illustrated in Fig. 1, from the RVE to the domain scale, and corresponds to scales where some physical fields can be considered as homogeneous leading to some simplifications in the energy description. Indeed the selection of a phase, a variant or a domain family is based on the principle of minimum energy. A first step consists to build an energy function at the domain scale where anisotropic crystallographic phenomena are significant and some fields can be simplified.

Figure 1: Detail of scales involved in the modeling approach

The first principle given at the local scale (J/m 3 ) express that the total energy density composed of kinetic energy density and internal energy density can only change by the action of external work and heat power. The internal energy density at the domain scale is written as: ! ! . At constant velocity, kinetic energy is constant. There is a direct relationship between the variation of internal energy density and power sources:

!" ! = !ℎ ! + ! ! !! ! + ! ! : !! ! + ! ! . !! ! (1)
This expression is composed of: -!ℎ ! : chemical energy variation= bound energy variation from one phase to another; -! ! : !! ! : mechanical energy variation (mechanical power), function of deformation variation !! ! and local stress ! ! . -! ! !! ! = !! ! : heat quantity variation (thermal power), function of entropy variation !! ! (second law of thermodynamics) and local temperature ! ! ; this expression applies in a reversible framework. -! ! . !! ! : magnetic energy variation (magnetic power), function of induction variation !! ! and magnetic field ! ! .

The introduction of free (Helmholtz) energy ! ! = ! ! -! ! ! ! (Legendre transformation of heat quantity) allows the energy variation to be defined as function of temperature variation instead of entropy variation. The magnetic free enthalpy ! ! = ! ! -! ! . ! ! (Legendre transformation of magnetic quantity) allows the energy variation to be defined as function of magnetic field variation instead of induction variation. The Gibbs free energy (or free enthalpy) ! ! = ! ! -! ! : ! ! (Legendre transformation of mechanical quantity) allows finally the energy variation to be defined as function of stress variation instead of deformation variation. Variation of Gibbs free energy is given by:

!" ! = !ℎ ! -! ! !! ! -! ! : !! ! -! ! . !! ! (2)
Since a domain ! is a part of a variant inside a phase, variation of chemical energy is null leading to [START_REF] Mason | [END_REF]:

!" ! = -! ! !! ! -! ! : !! ! -! ! . !! ! (3)
Entropy density, strain and magnetic induction finally derive from the Gibbs free energy function following:

! ! = - !" ! !! ! ! ! = - !" ! !! ! ! ! = - !" ! !! ! (4)
A second order Taylor expansion of entropy leads to derive the classical expression [4]: where ! ! ! is the reference entropy at the reference temperature ! ! ! , ! ! is the mass density and ! ! ! the specific heat capacity. The chemical part of the Gibbs free energy is defined as:

! ! = ! ! ! -! ! ! ! ! 1 - ! ! ! ! ! + !" ! ! ! ! ! (5)
! ! ! = ℎ ! -! ! ! ! = ℎ ! -! ! ! ! ! -! ! ! ! ! ! ! -! ! ! + ! ! !" ! ! ! ! ! (6)
Small perturbation hypothesis allows the total deformation ! ! to be considered as a sum of different contributions, allowing some specific couplings between mechanics and another physic to be defined. In the case of the target materials, classical ! ! ! and thermal ! ! ! deformation are considered first. Free deformation ! ! ! associated with magnetostriction on the one hand and transformation deformation on the other hand is the third deformation source leading to:

! ! = ! ! ! + ! ! ! + ! ! ! = ! ! !! : ! ! + ! ! ! (! ! -! ! ! )1 + ! ! ! ( 7
)
! ! is the 4 th order local stiffness tensor, ! ! is the volumetric dilatation coefficient and 1 the second order identity tensor. At this step, it is interesting to observe that the free deformation can be considered as stress independent at the local scale, allowing a simple derivation of the mechanical part of Gibbs free energy. Complementary hypotheses can help to simplify the last term.

! ! ! = - ! ! ! ! : ! ! !! : ! ! - ! ! ! (! ! -! ! ! )!"(! ! ) - ! ! ! : !! ! ! ! ! (8)
The magnetic induction is resulting from the local magnetic field and local magnetization of the material ! ! following:

! ! = ! ! (! ! + ! ! ) (9)
where ! ! is the vacuum magnetic permeability. The magnetic contribution to the internal energy variation can be expressed as:

!" ! = ! ! ! ! . !! ! + ! ! ! ! . !! ! (10)
At the local scale (magnetic domain) the magnetization variations can be very high (much higher than magnetic field) so that the second term is often neglected [5] and the Helmholtz magnetic free energy is expressed as function of magnetization. A Taylor expansion is used (3 rd order development), taking into account the fact that the magnetic behavior is an odd function. The Helmholtz magnetic free energy is consequently an even function of magnetization [START_REF] Mason | [END_REF].

! ! ! = ! ! . ! ! ! . ! ! + ! ! ! ! : ! ! ! : ! ! ! ! + ! ! . ! ! ! ! : ! ! ! : ! ! ! ! . ! ! (11)
Using a second order ! ! ! , 4 th order ! ! ! and 6 th order ! ! ! tensors as material dependent whose expressions are strongly correlated to material symmetries. The associated expression of Gibbs magnetic free energy (after Legendre transformation) is given by:

! ! ! = ! ! . ! ! ! . ! ! + ! ! ! ! : ! ! ! : ! ! ! ! + ! ! . ! ! ! ! : ! ! ! : ! ! ! ! . ! ! -! ! ! ! . ! ! (12) The sum of ! ! ! , ! ! ! and ! ! !
gives the total Gibbs free energy of medium that must be minimum with respect to temperature, stress and magnetic field at the equilibrium.

Usual simplifications of Gibbs free energy

At this step, it is interesting to observe that the magnetization at the domain scale has a constant norm equal to the saturation magnetization ! ! [START_REF] Hubert | Magnetic domains[END_REF]. The magnetization vector can be defined using the direction cosines ! ! ! in the local frame (usually crystal frame) as:

! ! = ! ! ! ! ! . ! ! = ! ! (! ! ! . ! ! + ! ! ! . ! ! + ! ! ! . ! ! ) (13)
leading to the so-called dyadic expression of the second order orientation tensor !:

! ! ! ! = ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! = ! ! ! ! (14)
Using the cubic symmetry and the identity

! ! ! ! ! ! + ! ! ! ! ! ! + ! ! ! ! ! ! = 1
, the magnetic part of Gibbs free energy simplifies into [START_REF] Mason | [END_REF][START_REF] Hubert | Magnetic domains[END_REF]:

! ! ! = ! ! + ! ! (! ! ! ! ! ! ! ! ! ! ! + ! ! ! ! ! ! ! ! ! ! ! ! + ! ! ! ! ! ! ! ! ! ! ! ! ) + ! ! (! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ) -! ! ! ! . ! ! (15
) where ! ! , ! ! and ! ! are the so-called magnetocrystalline constants (defining the magnetocrystalline energy density) and the last term is usually called Zeemann energy density (if ! ! is considered homogeneous case of uniaxial anisotropy of axis ! (so that ! ! . ! = ! ! ! ! ! ), a quadratic magnetocrystalline energy is usually enough to express the magnetic part of Gibbs free energy:

! ! ! = ! ! (1 -! ! ! ! ! ! ) -! ! ! ! . ! ! ( 16
)
The magnetic part of Gibbs free energy is often used to express the magneto-elastic coupling energy term ! ! !" considered as linearly dependent to stress and as a quadratic function of magnetization, without excluding some complementary higher order terms [START_REF] Mason | [END_REF].

! ! !" = -! ! ! ! : ! ! : ! ! = - ! ! ! : !! ! ! ! ! = -! ! ! : ! ! ( 17
)
! ! is the piezomagnetic 4 th order tensor defined by 3 constants in the cubic crystallographic framework. Looking at equation ( 8), it is possible to identify ! ! ! ! : ! ! as the so-called magnetostriction 2 nd order tensor ! ! ! reducing to 2 independent constants in case of incompressible deformation [START_REF] Hubert | Magnetic domains[END_REF][START_REF] Du | Tremolet de Magnetostriction: theory and of magnetoelasticity[END_REF]:

! ! ! = ! ! ! !"" (! ! ! ! ! ! -! ! ) ! !!! ! ! ! ! ! ! ! !!! ! ! ! ! ! ! ! !!! ! ! ! ! ! ! ! !"" (! ! ! ! ! ! -! ! ) ! !!! ! ! ! ! ! ! ! !!! ! ! ! ! ! ! ! !!! ! ! ! ! ! ! ! !"" (! ! ! ! ! ! -! ! ) (18)
where ! !"" and ! !!! are the magnetostriction constants that correspond to the deformation of a perfect single crystal along <100> and <111> axis respectively at the magnetic saturation.

Simplifications can concern the loading itself and some homogeneity hypotheses that can be applied:

-homogeneous stress at the grain scale:

! ! = ! ! = ! ! -homogeneous temperature over the volume: ! ! = ! ! = ! ! = !
-homogeneous magnetic field at the grain scale: ! ! = ! ! = ! ! Only stress and magnetic field have usually to be localized (to be defined as function of loading at the upper scale).

Constitutive law, localization and homogenization procedures

Gibbs energy is defined at the domain scale, inside a variant, inside a phase, inside a grain, inside the representative volume element. A stochastic approach is relevant for a description "at equilibrium". The internal variables of the problem are the volume fraction of domain families denoted as ! ! and the orientation of the magnetization inside each domain family (giving the direction cosines ! ! ! ). The total number of internal variables strongly depends on the number of phases (n), variants (m) and number of domain families (p) inside each variant. Following [START_REF] Daniel | [END_REF] we use a probabilistic Boltzmann like function to calculate the volume fraction and implement an energy minimization for the determination of the magnetization direction. Equation (19) gives the simplest expression of volume fraction ! ! , where ! ! is an adjusting parameter.

! ! = !"#(!! ! ! ! ) !"#(!! ! ! ! ) ! ! ! (19)
This equation is complemented by the minimization operation reported in equation (20).

! ! ! = !"#(! ! ) (20)
This formulation is well suited for a single variant and monophasic ferromagnetic material [START_REF] Daniel | [END_REF][9][10][11][12][13] (ferromagnetic ferrite or austenite). A more complex formulation has been proposed recently. The new volume fraction is using up to three different parameters (! ! , ! ! , ! ! ) driving three different kinetics (domain, variant and phase kinetics).

! ! = !"#(!! ! ! ! ) ! ! !!"(!! ! ! ! ) ! ! ! !"#(!! ! ! ! ) ! !"#(!! ! ! ) ! ! !"#(!! ! ! ! ) !"#(!! ! ! ! ) ! (21)
Moreover the volume fraction of a variant ! and a phase ! are simply given by:

! ! = ! ! ! = !"#(!! ! ! ! ) ! ! It can be noticed that, for (! ! = ! ! = ! ! ), equation (19) is recovered.
Different materials can be considered: ferromagnetic materials without phase transformation (electric steels, iron, nickel -equation ( 19)), paramagnetic materials with phase transformation and a single variant (austenite/ferrite allotropic transformation -equation (23) [14]), or with multiple variants (SMA -equation ( 22) [15]), ferromagnetic materials with phase transformation and multivariants (MSMA -equation (21) [16]), or magneto-caloric materials where the phase transformation temperature coincides with the Curie temperature (equation (21) [START_REF] Bartok | A multiscale model of thermo-magneto-elastic phase transition in Mn-Fe-P-Si[END_REF]). Some localization rules are required to define the stress and magnetic fields at the grain scale (they are supposed homogeneous over the variants and magnetic domains) [START_REF] Daniel | [END_REF]. An Eshelby approach is applied for the determination of both fields. The stress at the grain scale ! ! is function of the macroscopic stress !, a stress concentration tensor ! ! , an accommodation stiffness tensor ! ! !"" and the contrast between macroscopic ! ! and microscopic ! ! ! free strain tensor:

! ! = ! ! : ! + ! ! !"" : (! ! -! ! ! ) (24)
This relation is complemented by classical averaging operations:

! =< ! ! > ! ! =< ! ! ! : ! ! ! > (25)
The magnetic field at the grain scale ! ! is function of the macroscopic magnetic field !, an average secant susceptibility ! = !/! and the contrast between macroscopic to microscopic magnetization:

! ! = ! + ! !!!! (! -! ! ) (26)
This relation is complemented by classical averaging operations:

! =< ! ! > ! =< ! ! > (27)

Conclusion

The principles of multiscale modeling with thermodynamic foundations were presented. The stochastic constitutive law is well adapted to the existence of fine microstructures for which it is possible to consider some fields as homogeneous. It is very well adapted to the description of many couplings involving a mechanical free deformation. The localization procedures from the RVE to the grain scale makes it possible to better account for demagnetizing fields and residual stresses effects [13]. Such a modeling requires physical parameters usually coming from literature and adjusting parameters identified using a differential scanning calorimetry measurement for the phase kinetic [16], a mechanical measurement for variant kinetic [15], and an anhysteretic magnetic measurement for the magnetic domain kinetic [START_REF] Daniel | [END_REF]. Validation is usually obtained from coupled experiments (involving the concomitant variation of several fields). This approach must usually be complemented by a numerical modeling, leading a minima to the resolution of the heat equation [START_REF] Depriester | [END_REF]. Indeed chemical enthalpy variation acts as a heat source in the heat equation, making each phase transformation problem a strongly coupled themomechanical situation. Another important issue is the introduction of irreversible phenomena associated with germination and effects.