Emiliano Lorini
email: lorini@irit.fr

Frédéric Moisan
email: moisan@irit.fr

Frédéric Moisan An

Équipe Lilac

An Epistemic Logic of Extensive Games

Keywords: epistemic logic, game theory, extensive form games, rationality, backward induction, Aumann's theorem

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

Introduction

The aim of this article is to propose a modal logic framework that allows to reason about epistemic games in extensive form. In this kind of games, players decide what to do according to some general principles of rationality while being uncertain about several aspects of the interaction such as other agents' choices, other agents' preferences, etc.

While epistemic games have been extensively studied in economics (in the so-called interactive epistemology area, see e.g. [START_REF] Aumann | Epistemic Conditions for Nash Equilibrium[END_REF][START_REF] Aumann | Interactive Epistemology I: Knowledge[END_REF]9,5,[START_REF] Brandenburger | Knowledge and Equilibrium in Games[END_REF]12]) and while there have been few modal logic analyses of epistemic games both in strategic form and in extensive form (see, e.g., [START_REF] Van Benthem | Rational dynamics and epistemic logic in games[END_REF][START_REF] Bruin | Explaining games: on the logic of game theoretic explanations[END_REF]9,[START_REF] Roy | Thinking before acting: intentions, logic, rational choice[END_REF][START_REF] Van Der | Modal Logic for Games and Information[END_REF][START_REF] Lorini | A modal logic of epistemic games[END_REF][START_REF] Van Benthem | Toward a Theory of Play: A Logical Perspective on Games and Interaction[END_REF]24,[START_REF] Baltag | Keep 'hoping' for rationality: a solution to the backward induction paradox[END_REF]), there exists no logic with a corresponding formal semantics for extensive form games which has been showed to be sufficiently general:

• to express in the object language solution concepts like backward induction,

• to derive syntactically the epistemic and rationality conditions on which such solution concepts are based.

While it is shown in [START_REF] Van Benthem | Toward a Theory of Play: A Logical Perspective on Games and Interaction[END_REF] and [24] that reasoning about actions only is sufficient to compute solution concepts like the backward induction, such game logics can not express the notion of substantive rationality as in Aumann's definition, which fully considers the temporal aspect of the concept of strategy. Indeed, unlike for strategic games where a strategy can be simply reduced to a set of actions (see [START_REF] Lorini | A modal logic of epistemic games[END_REF]), a strategy in an extensive form game expresses not only the sequence of actions that will occur next, but also the actions that would occur in every vertex of the game.In [START_REF] Bruin | Explaining games: on the logic of game theoretic explanations[END_REF] a logic which enables to reason about the epistemic aspects of extensive games is presented. This logic deals with several gametheoretic concepts like the concepts of knowledge, rationality and backward induction. Nevertheless, all these notions are atomic propositions of the logic managed by an ad hoc axiomatization. Moreover, the logical approach to extensive form games proposed in [START_REF] Bruin | Explaining games: on the logic of game theoretic explanations[END_REF] is purely syntactic: no model-theoretic analysis of extensive form games is proposed.

In this article, we try to fill this gap by proposing both a semantic and a syntactic analysis of extensive form games in modal logic. In particular, we introduce a multi-modal logic interpreted on a Kripke-style semantics which integrates the concepts of action, strategy, knowledge and preference and which allows to reason about the properties of extensive form games. In order to illustrate the expressive power of the logic, we define in its object language the well known concepts of rationality and backward induction, as they are defined according to economic theory. Based on these definitions, we then provide a syntactic proof of Aumann's theorem that states the following: "for any non degenerate game of perfect information, common knowledge of rationality implies the backward induction solution" [START_REF] Aumann | Backward Induction and Common Knowledge of Rationality[END_REF]. While there exist other logics that formalize similar theorems, none of these is expressive enough to provide syntactic proofs that would emphasize the various requirements assumed for the theorems. For example, while [START_REF] Baltag | Keep 'hoping' for rationality: a solution to the backward induction paradox[END_REF] presents a logic that can correctly define the statement of Aumann's theorem, no syntactic proof of it is provided, and its language does not allow to verify whether the theorem holds when the epistemic conditions are weakened. Indeed, if one realistically only considers common knowledge to be bounded to some finite level, then the maximal depth of the game represents an important variable to the proof of the theorem. By considering the temporal dimension of such extensive games, we demonstrate its relevance to the proof of some weaker version of the theorem.

Our intention, throughout this paper, is not to show that a syntactic derivation of Aumann's theorem is interesting in itself. Instead, we wish to demonstrate that this kind of analysis is useful to identify specific assumptions about the relationship between players' knowledge and the game structure that are needed in order to prove the theorem.

The rest of the article is organized as follows. Section 2 is devoted to presenting our logic of action, strategy, knowledge and preference with the definition of its language and its semantics. Then, in Section 3, we define the concept of rationality in the case of extensive form games and the backward induction concept, as they are defined by Robert Aumann. Section 4 provides a syntactic proof of Aumann's well-known theorem as well as a systematic analysis of the hypotheses that are needed to prove it. Finally, in section 5, we propose some possible revisions to our logic, which lead to a more realistic interpretation of Aumann's theorem. Related works on the logic of extensive games are discussed in Section 6.

The syntactic proof of Aumann's theorem is given in the Appendix at the end of the article.

A modal logic of actions, strategies, knowledge and preferences

We present in this section the modal logic ELEG (Epistemic Logic of Extensive Games) integrating the concepts of action, strategy, knowledge and preference. This logic supports reasoning about games in extensive form in which an agent might be uncertain about the current choices of the other agents.

Syntax

The syntactic primitives of the logic ELEG are the finite set of agents Agt, the set of atomic propositions Atm, a nonempty finite set of atomic action names Act = {α 1 , α 2 , . . . , α |Act| }, a non-empty finite set of n integers I = {0, . . . , n}.

The language L of the logic ELEG is given by the following BNF:

χ ::= p | α | turn i | end | k i ϕ ::= χ | ¬ϕ | ϕ ∨ ϕ | ϕ | AXϕ | [K i ]ϕ | Xϕ
where p ranges over Atm, i ranges over Agt, α ranges over Act, and k ranges over I. Formulas χ are called atomic formulas. The classical Boolean connectives ⊥, , ∧, → and ↔ are defined from ∨ and ¬ in the usual manner.

The formula α has to be read "the action α is performed", while turn i and k i are read respectively "it is agent i's turn to play", and "the current strategy will ensure a payoff k to agent i". Finally, end is meant to stand for "the current vertex of the game is an end vertex".

The operator is used to quantify over strategies of the current game. ϕ has to be read "ϕ holds for all strategies of the current extensive game". The operator AX is used to quantify over next vertices of the current extensive game. AXϕ has to be read "ϕ is true at every possible next vertex along the current strategy".

The formula [K i ]ϕ is read as usual "agent i knows that ϕ is true". X is the standard temporal operator of next. The formula Xϕ has to be read "ϕ will be true next".

Moreover, the following abbreviations are given:

♦ϕ def = ¬ ¬ϕ AX 0 ϕ def = ϕ EXϕ def = ¬AX¬ϕ AX n+1 ϕ def = AX(AX n ϕ) K i ϕ def = ¬[K i ]¬ϕ AX ≤n ϕ def = 0≤m≤n AX m ϕ α i def = α ∧ turn i EX n ϕ def = ¬AX n ¬ϕ X 0 ϕ def = ϕ EX ≤n ϕ def = ¬AX ≤n ¬ϕ X n+1 ϕ def = XX n ϕ
♦ϕ has to be read "ϕ holds for at least one strategy of the current extensive game", whereas EXϕ has to read "ϕ is true in at least one possible next vertex along the current strategy". K i ϕ has to be read "agent i thinks that ϕ is possible", whereas α i has to be read "agent i performs the action α". X n has to be read "ϕ will be true n steps from now". Operators AX n ϕ and AX ≤n ϕ respectively read "ϕ is true in every vertex that can be reached in exactly n step(s) from now, along the current strategy" and "ϕ is true in every vertex that can be reached within n step(s) from now, along the current strategy". Finally the corresponding dual operators EX n ϕ and EX ≤n ϕ can be interpreted as "ϕ is true in at least one vertex that can be reached in exactly n step(s) from now, along the current strategy" and "ϕ is true in at least one vertex that can be reached within n step(s) from now, along the current strategy".

As common in Propositional Dynamic Logic (PDL), we introduce an operator of sequential composition ";". We define the set Seq of action sequences as the smallest set such that: α ∈ Seq for any α ∈ Act, and if 1 , 2 ∈ Seq then 1 ; 2 ∈ Seq. Moreover, we consider Seq n ⊆ Seq to be the set of action sequences of length n. The fact that a given action sequence will occur and ϕ will be true afterwards can be defined in the object language by means of the following definition:

α 0 ; . . . ; α n ϕ def = 0≤l≤n X l α l ∧ X n ϕ We use [EK C ]ϕ as an abbreviation of i∈C [K i ]ϕ, i.e. every agent in C knows ϕ (if C = ∅ then [EK C ]ϕ is equivalent to ). Then we define by induction [EK k C ]ϕ for every natural number k ∈ N: [EK 0 C ]ϕ def = ϕ and for all k ≥ 1, [EK k C ]ϕ def = [EK C ]([EK k-1 C ]ϕ)
Similarly, we define for all natural numbers n ∈ N:

[CK 0 C ]ϕ def = ϕ and for all n ≥ 1, [CK n C ]ϕ def = 1≤k≤n [EK k C ]ϕ [CK n C
]ϕ expresses C's mutual knowledge that ϕ up to n iterations, i.e. everyone in C knows ϕ, everyone in C knows that everyone in C knows ϕ, and so on until level n.

Semantics

A strategic structure includes a set of vertices, a set of strategies, a successor function associating vertices and strategies to vertices, a turn-taking function assigning agents to vertices. The set of vertices includes end vertices.

Strategic structure A strategic structure is a tuple T = V , Q, S, next, EndV where:

• V is a non-empty set of vertices;

• Q is total function Q : V -→ Agt mapping vertices to agents;

• S is a nonempty set of strategies on V , and every strategy s ∈ S is a total function s : V -→ Act mapping vertices to actions;

• next is a partial function next : V × S -→ V mapping vertices and strategies to vertices such that:

C1 if s(w) = s (w) then next(w, s) = next(w, s );
• EndV ⊆ V is the set of end vertices such that:

C2 w ∈ EndV if and only if, next(w, s) is undefined for every s.

Q(w) = i means that at vertex w it is agent i's turn to play, and next(w, s) = w means that w is the next vertex of w with respect to the strategy s. We call index a pair (w, s) with w ∈ V and s ∈ S. We define H = V × S the set of all indices. Note that the particular concept of a strategy in Definition 2.2 considers every vertex of the game and is not restricted to a single player's moves as usually done in game theory. However, for every s ∈ S, a single player i's strategy s i can be defined as the restriction of s to the vertices in which it is agent i's turn to play.

According to the Constraint C1, two strategies selecting the same action at a given vertex lead to the same next vertex. According to the constraint C2, an end vertex is a vertex which does not have a next vertex.

Successor R is a relation on vertices such that:

for every w, v ∈ V , wRv if and only if there is s ∈ S such that next(w, s) = v.

wRv means that vertex v is a successor of vertex w.

An extensive game model is nothing but a strategic structure supplemented with accessibility relations for agents' knowledge over strategies, agents' preferences and a valuation of atomic propositions.

Extensive game model

An extensive game model is a tuple M = T, {E i | i ∈ Agt}, {P i | i ∈ Agt}, π where:
• T is a strategic structure;

• Every E i is an equivalence relation on S such that:

C3 if sE i s and Q(w) = i, then s(w) = s (w);
• every P i is a total function P i : H -→ I mapping every index to an integer such that:

C4 if next(w, s) = w , then P i (w, s) = k if and only if P i (w , s) = k;
C5 if w ∈ EndV and s(w) = s (w) then P i (w, s) = P i (w, s ).

• π : Atm -→ 2 H is a valuation function on indices.

sE i s means that agent i cannot distinguish the strategy s from the strategy s . P i (w, s) = k means that the strategy s played at the vertex w will ensure a payoff k to agent i.

Constraint C3 is the assumption that every agent knows his choice when it is his turn to play [START_REF] Aumann | Backward Induction and Common Knowledge of Rationality[END_REF]5]. Constraint C4 correctly expresses the fact that in an extensive form game, preferences are built over histories, where a history is nothing but a sequence of indices (w 0 , s), . . . , (w n , s), . . . such that next(w i , s) = w i+1 for every 0 ≤ i. According to the Constraint C5, two strategies selecting the same action at an end vertex lead to the same payoff for an agent. In other words, at an end vertex the payoff of an action is uniquely determined.

Example In order to illustrate the use of our logic ELEG to model extensive form games, let us consider a well known game in economics, namely the trust game [6]. The binary version of the trust game (BTG) involves two players, the truster and the trustee, playing sequentially in the following way: first the truster can choose between leaving the game and divide the amount of $2 equally with the trustee (i.e. $1 for each) or let the trustee play. In the latter case, the trustee can either divide the amount of $6 equally with the truster (i.e. $3 for each) or keep the whole amount for himself (i.e. $6 for himself and $0 for the truster). Consider a version of this game, whose graphical representation is depicted in Figure 1.

v w (1,1) (0,6) (3,3) C 1 D 1 C 2 D 2 Figure 1: Binary Trust Game (BTG)
In Figure 1, let us consider a player i 1 , as the truster who plays at vertex v, and a player i 2 , as the trustee who plays at vertex w. At each leaf of the tree, payoffs take the form (X, Y ), where player i 1 gets $X and player i 2 gets $Y . Moreover, actions named C x and D x respectably stand for "player i x cooperates" and "player i x defects" (with x being either 1 or 2).

Therefore, we suppose

Agt = {i 1 , i 2 }, Act = {C 1 , C 2 , D 1 , D 2 }, V = {v, w}, EndV = {w}, and S = {s 1 , s 2 , s 3 , s 4 };
Let us now represent the extensive game model corresponding to the binary trust game in ELEG:

• next(v, s 1 ) = w, next(v, s 2 ) = w; • Q(v) = i 1 , Q(w) = i 2 ; • E i 1 (s 1 ) = E i 1 (s 2 ) = {s 1 , s 2 }; E i 1 (s 3 ) = E i 1 (s 4 ) = {s 3 , s 4 }; E i 2 (s 1 ) = E i 2 (s 3 ) = {s 1 , s 3 }; E i 2 (s 2 ) = E i 2 (s 4 ) = {s 2 , s 4 }; • P i 1 (v, s 1 ) = P i 1 (w, s 1 ) = P i 1 (w, s 3 ) = 3, P i 2 (v, s 1 ) = P i 2 (w, s 1 ) = P i 2 (w, s 3 ) = 3, P i 1 (v, s 2 ) = P i 1 (w, s 2 ) = P i 1 (w, s 4 ) = 0, P i 1 (v, s 3 ) = P i 1 (v, s 4 ) = P i 2 (v, s 3 ) = P i 2 (v, s 4 ) = 1, P i 2 (v, s 2 ) = P i 2 (w, s 2 ) = P i 2 (w, s 4 ) = 6
This model represents the four possible strategies s 1 , s 2 , s 3 and s 4 of the BTG, each of which includes the same two vertices v and w where various actions occur:

• s 1 corresponds to strategy (C 1 , C 2 ); • s 2 corresponds to strategy (C 1 , D 2 ); • s 3 corresponds to strategy (D 1 , C 2 );
• s 4 corresponds to strategy (D 1 , D 2 ); Vertices v and w represent the nodes within the game where respectively player i 1 and player i 2 have to play. The epistemic relations E i 1 and E i 2 , as they are defined in this model, represent perfect uncertainty for each player over the strategies. One should note however that these epistemic relations are only examples and could possibly be defined differently without modifying the strategic structure of the game.

Truth conditions Truth of a formula in a model M at a given index (w, s) is defined as follows:

• M, w, s |= p iff (w, s) ∈ π(p); • M, w, s |= ¬ϕ iff M, w, s |= ϕ; • M, w, s |= ϕ ∨ ψ iff M, w, s |= ϕ or M, w, s |= ψ; • M, w, s |= α iff s(w) = α; • M, w, s |= turn i iff Q(w) = i; • M, w, s |= end iff w ∈ EndV ; • M, w, s |= k i iff P i (w, s) = k; • M, w, s |= Xϕ iff if next(w, s) is defined then M, next(w, s), s |= ϕ; • M, w, s |= ϕ iff M, w, s |= ϕ for all s ∈ S; • M, w, s |= AXϕ iff M, w , s |= ϕ for all w ∈ V such that wRw ; • M, w, s |= [K i ]ϕ iff M, w, s |= ϕ for all s such that sE i s .
A formula ϕ is true in an extensive game model M iff M, w, s |= ϕ for every vertex w in V and every strategy s in S. ϕ is ELEG-valid (noted |= ϕ) iff ϕ is true in all extensive game models. ϕ is ELEG-satisfiable iff ¬ϕ is not ELEG-valid.

All principles of classical propositional logic (CPL)

All S5 principles for (S5 ) All S5 principles for every

[K i ] (S5 [K i ] ) All K principles for X (K X ) All K principles for AX (K AX ) Xϕ ∨ X¬ϕ (Det X ) end ↔ X⊥ (EndVert) ϕ → [K i ]ϕ (PerfectInfo) AXϕ ↔ AX ϕ (Perm ,AX ) X ϕ ↔ AX ϕ (NxtVert) [K i ]AXϕ ↔ AX[K i ]ϕ (Perm [K i ],AX ) turn i → turn i (TurnStr) AXϕ → Xϕ (TimeVert) turn i → (α → [K i ]α) (Aware) k∈I k i (CompletePref) k i → ¬h i if k = h (SinglePref) α∈Act α (OneAct) α → ¬β if α = β (SingleAct) i∈Agt turn i (TurnTaking) turn i → ¬turn j if i = j (SingleTurn) ¬end → (k i ↔ Xk i ) (TimePref) (end ∧ α ∧ k i ) → (α → k i ) (EndAct) (α ∧ X ϕ) → (α → Xϕ) (StrAct)

Some validities

Table 1 provides an exhaustive list of ELEG validities that will be sufficient to provide in Section 4 a syntactic proof of Aumann's theorem.

Let us prove the validity Perm [K i ],AX as an example. Assume M, w, s |= [K i ]AXϕ for an arbitrary ELEG model M . This is equivalent to say that M, w, s |= AXϕ for all s such that sE i s which, in turn, is equivalent to say that M, w , s |= ϕ for all (w , s ) such that sE i s and wRw . The latter is equivalent to say that M, w , s |= [K i ]ϕ for all w such that wRw which, in turn, is equivalent to say that M, w, s |= AX[K i ]ϕ.

In the sequel, we will write ELEG ϕ to mean that ϕ can be derived by means of the list of principles given in Table 1. The study of a complete axiomatization of the logic ELEG is postponed to future work.

Backward induction and rationality

We here define two fundamental concepts in Aumann's epistemic analysis of extensive form games: the concept of backward induction and the concept of rationality.

As a matter of simplicity to later prove Aumann's Theorem, we only provide in this section simplified formal definitions that only apply to games of uniform depth. One should note however that more general definitions of both backward induction and rationality can easily be expressed in ELEG.

Backward induction

The notion of backward induction represents the process of reasoning backwards in time, starting from each end vertex of the game in order to determine a sequence of optimal actions. This method is generally used to compute the subgame perfect Nash equilibria in sequential games. The backward induction (BI) solution in a game of depth n (i.e. where at most n steps are necessary to reach an end vertex of the game) can be computed by iterating the process n times, as the BI solution at one state relies on the BI solution at every possible successive state. Therefore, the first step BI solution (n = 0) corresponds to the maximization of preferences for the last player to play at each possible end vertex of the game. The BI solution after n (n > 0) steps corresponds to the maximization of the current player's preferences, considering only those that satisfy the BI solution after n -1 steps at any possible next state.

The recursive formal definition in ELEG of the BI solution after n steps is as follows. For the case n = 0 we define:

BI 0 def = end ∧ i∈Agt,k∈I (turn i ∧ k i ∧ ( h∈I:h≤k h i ))
For every n > 0 we define:

BI n def = ¬end ∧ i∈Agt,k∈I (turn i ∧ k i ∧ AX(BI n-1 ∧ h∈I:h≤k h i ))
Therefore: M, w, s |= BI n if and only if the current strategy s, when starting from vertex w, corresponds to a backward induction solution that can be computed in n steps.

Epistemic rationality

The following ELEG definition characterizes a notion of rationality that is supposed in Aumann's epistemic analysis of extensive form games:

Rat end i def = (end ∧ turn i ) → k∈I (k i ∧ ( h∈I:h≤k h i ))
Rat end i means that an agent i is rational at an end vertex (i.e. at some end vertex of the game) if and only if i chooses an action that maximizes his individual payoff. Note that in this case, rationality does not rely on any epistemic component.

Rat ¬end i def = (¬end ∧ turn i ) → k∈I K i (k i ∧ AX( h∈I:h≤k K i h i ))
Rat ¬end i means that an agent i is rational at any intermediate vertex (any node that is not an end vertex of the game) if and only if i chooses an action in such a way that what he considers possible to happen afterwards is not strictly dominated by some alternative future he would consider, had he chosen any other action. In other words, as every possible next vertex corresponds to one of i's possible actions, i is rational if and only if each of these vertices is not strictly dominated, according to i's uncertainty, by the next actual vertex (corresponding to the actual action chosen by i).

Rat i def = Rat end i ∧ Rat ¬end i
Note that introspection on rationality is expressed by the following valid formula of ELEG (see the syntactic proof of Lemma A.1 in the Appendix for details):

Rat i ↔ [K i ]Rat i

A syntactic proof of Aumann's theorem

As already stated in the previous section, a fundamental assumption of Aumann's theorem is that the game is in "general position", i.e. every history of the game is associated to a unique preference value for every agent. This important notion can be defined in the logic ELEG in the following way:

GenPos n def = 0≤h≤n k∈I,i∈Agt, ∈Seq h AX ≤n ((k i ∧ end) → ( end ↔ k i ))
In our syntactic proof of Aumann's theorem we only consider game structures with uniform depth, that is, games whose end vertices have the same distance from a given vertex.

The following construction Depth n means that "the current game has a uniform depth of degree n from the current vertex". In other words, no matter what actions will be chosen in the future, an end vertex will be reached in exactly n steps. This concept is thus captured by the following ELEG formula:

Depth n def = ( X) n end
This assumption, which is not stated in Aumann's original theorem, is used here only to simplify the formal proof. One should note however that any extensive game can be represented by an extensive game with uniform depth (i.e. by adding additional non informative actions and preferences).

According to Aumann's theorem, the following constraints must be satisfied in order for the current strategy to be a backward induction solution:

• the game is finite;

• the game has a uniform depth of degree n from the current vertex;

• the game is in the general position;

• there is common knowledge up to level at least n that at every future vertex (up to depth n) all agents are rational.

Theorem 4.1 For every n, m ∈ N such that n ≤ m, we have:

ELEG ([CK m Agt ]AX ≤n ( i∈Agt Rat i ) ∧ Depth n ∧ GenPos n ) → BI n
Note that the proof of Theorem 4.1 only requires to prove the case where m = n (see Lemma A.2 for details).

The proof of theorem 4.1 in the Appendix indicates several points that need to be discussed. A strong assumption made in the theorem is about the type of rationality that is used. In fact, Aumann's theorem considers substantive rationality in the hypothesis, which means that in every vertex of the game, the players will be rational. Such a definition is criticizable because it requires players to be even rational in vertices that will never be reached given some expected strategy. According to Stalnaker [START_REF] Stalnaker | Belief revision in games: forward and backward induction1[END_REF] 1 , a more realistic concept of rationality should be considered only on the vertices that are actually reached. However, the latter definition does not guarantee the backward induction solution. Our proof of the theorem suggests that this definition of substantive rationality is indeed important to the derivation of the equilibrium solution. To be even more precise, the use of Axiom Perm [K i ],AX in the proof of Theorem 4.1 indicates that common knowledge of substantive rationality must be true not only now but in every future vertex. Obviously Axiom Perm [K i ],AX is very strong as it assumes that players know at the beginning of the game what they will do at any reachable state in the future where they have to play. This simply means that players can not learn anything through the game play. This important Axiom Perm [K i ],AX reflects the structure of the epistemic relation in our logic that only considers strategies (i.e. agents have the same uncertainty regarding strategies no matter which vertex they are in). In order to allow the players to act more realistically and learn as they advance through the game, one needs to consider vertices along with strategies in the epistemic relation. In this way, a player who finds out that a possible strategy is discarded by another's move at some vertex may then update his/her knowledge, allowing him/her to later act accordingly.

A more convenient characterization of knowledge

Following the previous analysis of the syntactic proof of Aumann's theorem, we propose to revise our logic by providing a more realistic interpretation of Aumann's theorem.

First, one can note from the syntactic proof in the Appendix that Aumann's theorem can be weakened through a reinterpretation of the epistemic operator. Indeed, every proof step from Theorem 4.1 using Axiom T for the S5 knowledge operator [K i ] can still be proved using KD45 principles for the belief modal operator. Such an observation implies that a simple notion of belief (which is not necessarily truthful) is sufficient to prove Aumann's theorem. The detailed proof of Theorem 4.1 in the Appendix shows that such a weakening of the epistemic operator is made possible mainly by Axiom Aware that requires agents to have introspection on their own performing action (see specific proofs of Lemmas A.1 and A.2 in the Appendix for details). In other words, agents always believe without a doubt what they'll actually perform.

Moreover, as already stated in the previous section, the epistemic operator still remains unrealistic as it restricts agents to only consider static uncertainty over strategies and therefore prevents them to learn through the game. Hence in order to be more realistic, we here interpret the epistemic modal operator by means of an equivalence epistemic relation E w i on strategies for every agent i ∈ Agt and vertex w ∈ W . In this case, agents' uncertainty over strategies can change through time.

Given this change on the epistemic relation, the truth condition of the knowledge operator then becomes:

• M, w, s |= [K i ]ϕ iff M,
w, s |= ϕ for all s such that sE w i s . Considering this new epistemic relation E w i , the previous constraint C3 has to be reformulated as follows:

C3 *
if sE w i s and Q(w) = i, then s(w) = s(w) Moreover, the following constraints need to be introduced in order to keep Axiom Perm [K i ],AX as in Table 1:

C6

if sE v i s and wRv then sE w i s

C7

if sE w i s and wRv then sE v i s According to constraint C6, agents will never forget their current uncertainty over strategies in every reachable vertex. In other words, C6 simply means that agents will always have a perfect recall of their past uncertainty throughout the game. According to constraint C7, agents are always aware of their future uncertainty over strategies in every reachable vertex. In other words, C7 means that agents will never be able to discard strategies and therefore learn as they advance through time.

Let us provide the axiom corresponding to constraint C6:

[K i ]AXϕ → AX[K i ]ϕ (Perm * [K i ],AX ) Note that Axiom Perm * [K i ],
AX is simply a weaker version of the initial Axiom Perm [K i ],AX from Table 1. It is clearly showed in the Appendix that constraint C6 along with its corresponding Axiom Perm * [K i ],AX are sufficient to the syntactic proof of Theorem 4.1. Such an observation simply implies that Aumann's theorem holds even though agents are learning through the game (i.e. constraint C7, which is not necessary, can be removed). However, this analysis also indicates that Aumann's theorem requires agents to have perfect recall through the game. In other words, for the theorem to be correct, players should never forget anything as they advance in time.

One should note that such a constraint remains very strong and therefore not so realistic. The complete removal of constraint C6 and its corresponding Axiom Perm * [K i ],AX in our logic would however require a reinterpretation of the hypothesis of Aumann's theorem in a way that would take into account the evolution of the players' uncertainty through time. We choose not to pursue the analysis here and leave it for future work.

We are not the first to provide a logical analysis of extensive games. Several logical systems have been proposed which support reasoning about this class of games. We here discuss some of these systems and compare them with our logic ELEG.

In [21], van Benthem analyzes extensive games using different modal languages such as propositional dynamic logic (PDL), PDL with converse, and a modal forcing language which allows to express what a player can bring about in a given extensive game, no matter what the other players do. Moreover, he also studies a variety of notions of game equivalence based on the notion of bisimulation. Although van Benthem shows how PDL extended with epistemic operators can represent extensive games with imperfect information, he does not consider the concept of rationality which is a fundamental element of Aumann's epistemic analysis of extensive games. It is worth noting that, differently from our logic ELEG, standard PDL would fail to define such a concept, because it can neither identify the current strategy that is going to be played nor express what will be true at every possible next vertex along the current strategy (which is done through the operator AX in ELEG). Moreover, our logic ELEG shows that defining strategies explicitly in the object language -as done in PDL -is not necessary to express interesting game-theoretic concepts such as rationality and backward induction.

Related to van Benthem's work is Ramanujan & Simon's work [17,16] who have recently proposed an elegant approach to extensive games based on dynamic logic. However, Ramanujan & Simon do not deal with epistemic aspects of extensive games, as their logic does not have operators for representing epistemic states of players. The game logic presented in [15] also lacks epistemic operators, therefore preventing a formalization of the concept of epistemic rationality and a logical analysis of Aumann's theorem. Bonanno's logical account of extensive games [8,7] has the same limitation. He proposes a variant of dynamic logic extended with temporal operators for (branching) future and (linear) past and shows how his logic can be used to characterize the solution concept of backward induction. 2 But, like Ramanujan & Simon's logic, Bonanno's logic does not have epistemic operators which are required to represent Aumann's notion of rationality and the statement of Aumann's theorem. The same remark also applies to some recent work [20], which presents a similar logical approach to extensive games without considering the epistemic aspects.

ATL-based approaches to extensive games presented in [START_REF] Walther | Alternating-time temporal logic with explicit strategies[END_REF] and [START_REF] Van Der | A logic for strategic reasoning[END_REF] come closer to our current approach. For instance, in [START_REF] Walther | Alternating-time temporal logic with explicit strategies[END_REF] a variant of ATL (Alternating-time temporal logic) with explicit strategies called ATEL (Alternating-time logic with explicit strategies) is proposed which allows to define solution concepts such as backward induction. The interesting aspect of ATEL, compared to ATL, is that one can explicitly reason about strategies in the object language. However, like Ramanujan & Simon and Bonanno, ATEL misses epistemic operators necessary to define Aumann's notion of rationality. Another important difference between ATEL and our logic ELEG is that in ATEL formulas are interpreted with respect to states, whereas in ELEG they are interpreted with respect to state/strategy pairs (in this sense, ELEG semantics is bidimensional). The latter is an advantage because, differently from ATEL, it is possible in ELEG to reason about what will be true at every possible next vertex along the current strategy. We have shown that this is fundamental for expressing in the object language Aumann's notion of rationality and the statement of Aumann's theorem.

In [START_REF] Vestergaard | The inductive and modal proof theory of Aumann's theorem on rationality[END_REF], the authors propose an alternative way of proving Aumann's theorem by using a purely proof-theoretic approach based on type theory. Differently from Vestergaard et al.'s approach, our approach based on modal logic has the advantage of combining a prooftheoretic analysis of extensive games -which is what we have done in Section 4 -with a model-theoretic semantics.

Conclusion

In this paper, we have introduced a logical framework that provides an alternative way of representing extensive form games as compared to their usual specification in economics.

We showed that our logic is sufficiently general for our purpose to reason about dynamic epistemic games, as illustrated by the well known concepts of rationality and backward induction. Although these concepts have been extensively studied in economics, very few logical analyses have been proposed up to now. While several related works discuss and present some logical approaches to epistemic reasoning in such extensive games, none of these define a logic expressive enough to represent syntactically both the epistemic concepts and the equilibrium solutions. By the formal syntactic proof of Aumann's theorem, we demonstrate that our logic is capable to fill this gap and provide further interesting information about them.

In addition to providing a complete axiomatization of our logic, we intend in future work to investigate some extensions of the logic ELEG. While the language of the logic presented here is restricted to reason about the future only, the current semantics can be extended to reason also about the past and every possible counterfactual situation. This represents another research direction that we also consider to study further.

Inductive case:

Let n ∈ N and let us prove that if the theorem is true for all k ≤ n, then it is true for n + 1.

Table 1 :

 1 Some validities of ELEG

4 .

 4 ELEG end ∧ turn i ∧ k i → [K i ]k i by 3, Axioms EndAct, PerfectInfo, and Aware, and Axiom K for [K i ]; 5. ELEG [K i ]Rat i → [K i ]Rat end i ∧ [K i ]Rat ¬end i by the definitions of Rat i and boolean principles; 6. ELEG [K i ]Rat end i → ((end ∧ turn i ) → [K i ] k∈I (k i ∧ ( h∈I:h≤k h i )) by 1, the definitions of Rat end i , Axiom PerfectInfo, and Axioms T and K for [K i ] (or Axioms D and K if [K i ] is KD45 modal operator), and Axiom 5 for ;7. ELEG [K i ]Rat end i → ((end ∧ turn i ) → k ∈I k i ∧ [K i ] k∈I (k i ∧ ( h∈I:h≤k h i ))by 6 and Axiom CompletePref;8. ELEG [K i ]Rat end i → ((end ∧ turn i ) → k∈I k i ∧ [K i ](k i ∧ ( h∈I:h≤k h i ))by 7 and 4, and Axiom SinglePref;9. ELEG [K i ]Rat end i → ((end ∧ turn i ) → k∈I k i ∧ ( h∈I:h≤k h i ) by 8, Axiom PerfectInfo, Axiom T for [K i ] (or Axiom D if [K i ] is KD45 modal operator),and Axiom 5 for ; 10. ELEG [K i ]Rat end i → Rat end i by 9 and the definition of Rat end i ; 11. ELEG [K i ]Rat ¬end i → (¬end ∧ turn i ) → [K i ] k∈I K i (k i ∧ AX( h∈I:h≤k K i h i )) by 2, the definitions of Rat ¬end i , Axiom PerfectInfo, and Axioms T and K for [K i ] (or Axioms D and K if [K i ] is KD45 modal operator), and Axiom 5 for ; 12. ELEG [K i ]Rat ¬end i → (¬end ∧ turn i ) → k∈I K i K i (k i ∧ AX( h∈I:h≤k K i h i )) by 11 and boolean principles; 13. ELEG [K i ]Rat ¬end i → (¬end ∧ turn i ) → k∈I K i (k i ∧ AX( h∈I:h≤k K i h i )) by 12 and Axiom 4 for [K i ]; 14. ELEG [K i ]Rat ¬end ELEG [K i ]Rat i → Rat i by 15 and the definition of Rat i ; 17. ELEG Rat i → Rat end ]((end ∧ turn i ) → k∈I (k i ∧ ( h∈I:h≤k h i )) by 19 and 1, Axiom PerfectInfo, and Axiom K for[K i ]; GenPos 0 ∧ k j ∧ BI 0 ) → (BI 0 → k j ) 1. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → i∈Agt,k ,k ∈I turn i ∧ k i ∧ BI 0 ∧ ♦(turn i ∧ k i ∧ BI 0 )by Axioms TurnTaking, TurnStr and CompletePref and Axiom T for ;2. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → i∈Agt,k ,k ∈I turn i ∧ k i ∧ ( h∈I:h≤k h i ) ∧ ♦(turn i ∧ k i ∧ ( h∈I:h≤k h i ))by 1 and the definition of BI 0 ;3. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → i∈Agt,k ,k ∈I turn i ∧ k i ∧ ♦(turn i ∧ k i ) ∧ ( h∈I:h≤k ,h≤k h i ))by 2, Axiom 5 for , and boolean principles;4. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → i∈Agt,k ,k ∈I turn i ∧ k i ∧ h∈I:h≤k ,h≤k h i ∧ ♦(turn i ∧ k i ∧ h∈I:h≤k ,h≤k h i )by 5, Axiom K and T for , and boolean principles;5. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → i∈Agt,k ,k ∈I:k ≤k ,k ≤k turn i ∧ k i ∧ BI 0 ∧ ♦(turn i ∧ k i ∧ BI 0 )by 7, Axiom SinglePref, and boolean principles;6. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → ( i∈Agt,k ,k ∈I:k =k turn i ∧ k i ∧ BI 0 ∧ ♦(turn i ∧ k i ∧ BI 0 )) → ⊥by 8, and boolean principles; 7. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → i∈Agt,k ∈I turn i ∧ k i ∧ BI 0 ∧ (BI 0 → k i ) by 9 and boolean principles; 8. ELEG (end ∧ GenPos 0 ∧ k j ∧ BI 0 ) → (BI 0 → k j ) by 10 and Lemma A.5;

	i by 13 and the definition of Rat ¬end → Rat ¬end i i 15. ELEG [K i ]Rat i → Rat end i ∧ Rat ¬end i by 5, 10, and 14; 16. 21. ELEG Rat end i → [K i ]Rat end i by 20 and the definition of Rat end i ; 22. Here, we prove:	;

i ∧ Rat ¬end i by the definition of Rat i ; 18. ELEG Rat end i → ((end ∧ turn i ) → k∈I (k i ∧ ( h∈I:h≤k h i )) by the definition of Rat end i ; 19. ELEG Rat end i → ((end ∧ turn i ) → k∈I [K i ](k i ∧ ( h∈I:h≤k h i )) by 18 and 4, Axiom PerfectInfo, and Axiom 4 for ; 20. ELEG Rat end i → [K i ELEG Rat ¬end i → ((¬end ∧ turn i ) → k∈I K i (k i ∧ AX( h∈I:h≤k K i h i ))) by the definition of Rat ¬end i ; Basic case (n = 0): ELEG (end ∧

See also[START_REF] Halpern | Substantive rationality and backward induction[END_REF] for a discussion.

Bonanno's logic has four kinds of operators for past and future describing:[START_REF] Aumann | Backward Induction and Common Knowledge of Rationality[END_REF] what is going to be the case at every future vertex of the game tree,[START_REF] Aumann | Interactive Epistemology I: Knowledge[END_REF] what has always been the case at every past vertex,[START_REF] Aumann | Epistemic Conditions for Nash Equilibrium[END_REF] what is going to be the case at every predicted future vertex of the game tree, and (4) what has always been the case at every past vertex at which today was predicted.

A Appendix

We first provide the proof of the following Lemmas that are necessary to later prove Theorem 4.1.

To make the proofs of Lemmas and Theorem 4.1 more readable, we use the following abbreviation:

A.1 Syntactic proof of lemma A.1

We prove the following:

A.2 Syntactic proof of lemma A.2

We prove the following:

Basic case (n = 0):

AllRat by the definition of [CK 1 Agt ];

ELEG [CK 1

Agt ]AllRat → i∈Agt [K i ]Rat i by 1 and the definitions of [EK 1 Agt ] and AllRat; General case (for n > 0):

ELEG [CK

Agt ];

Agt ]AX n AllRat by 1 and boolean principles;

and the definition of [CK n

Agt ];

A.3 Syntactic proof of lemma A.3

We prove the following:

A.4 Syntactic proof of lemma A.4

We prove the following:

by 1, Theorem ELEG AX n+1 ϕ → AXAX ≤n ϕ, and boolean principles;

3. ELEG GenPos n+1 → AXGenPos n by 2 and the definition of GenPos n ;

A.5 Syntactic proof of lemma A.5

We prove the following inductively:

Basic case n=0:

Here, we prove

by definition of GenPos 0 , Axiom OneAct, and Axiom T for ;

by 1 and boolean principles;

Inductive case:

Let n ∈ N and let us prove that if the theorem is true for all k ≤ n, then it is true for n + 1.

by Axiom TimePref, and Lemmas A.3 and A.4;

by 1 and 2, and Axiom OneAct;

by 3, and Axiom StrAct;

by 4, Axiom TimePref and the definition of Depth n+1 ;

by 5 and the definition of GenPos n+1 ;

by 6 and boolean principles;

by 7, and boolean principles;

by 8, and boolean principles;

A.6 Syntactic proof of lemma A.6

We prove the following:

by 9 and boolean principles;

11. ELEG Depth n+1 ∧ GenPos n+1 ∧ k j ∧ BI n+1 → (BI n+1 → k j ) by 10 and Lemma A.5;

A.7 Syntactic proof of theorem 4.1

We demonstrate Aumann's theorem, which states the following:

We therefore prove the following inductively:

Basic case n=0:

Here, we prove ELEG AllRat ∧ end ∧ GenPos 0 → BI 0 .

1. ELEG (AllRat ∧ end ∧ GenPos 0 ) → i∈Agt (turn i ∧ Rat end i ) by the definition of Rat i , and Axiom TurnTaking;

by 1, and the definition of Rat end i ;

3. ELEG (AllRat ∧ end ∧ GenPos 0 ) → BI 0 by 2 and the definition of BI 0 ;

Inductive case:

Let n ∈ N and let us prove that if the theorem is true for all k ≤ n, then it is true for n + 1.

Agt ]AX m AllRat ∧ Depth n ∧ GenPos n ) by 1, Lemmas A.3 and A.4, and Axiom Perm [

and A.4, and Axiom Perm

by 9, Lemma A.6, and Axioms TurnTaking, TimeVert, OneAct, and Aware;

ABSTRACT

The aim of this work is to propose a logical framework for representing interacting agents in the context of extensive form games. Because of the importance of the temporal dimension provided by such games, we create a modal epistemic logic that allows to quantify over both strategies and vertices within the game tree. The first part of the article is devoted to the logic itself with the definition of its language and its semantics. In order to illustrate the use of this logic, we define, in the following part, the concept of rationality in the case of extensive form games and the backward induction concept, as they are defined by Robert Aumann. Based on these definitions, we then provide a syntactic proof of Aumann's theorem that states the following: "for any non degenerate game of perfect information, common knowledge of rationality implies the backward induction solution". We finally propose an in-depth formal analysis of the hypotheses that are needed to prove such a theorem.


Zaidao Li

Nathalie Limodin

Amina Tandjaoui

Philippe Quaegebeur

Pierre Osmond

David Balloy

Influence of Sr, Fe and Mn content and casting process on the microstructures and mechanical properties of AlSi7Cu3 alloy

Keywords: casting aluminium alloys, microstructure, mechanical characterization, microanalysis, tomography

The effects of Strontium (Sr), Iron (Fe) and Manganese (Mn) additions, casting process (i.e., cooling rate) on the microstructures and mechanical properties of AlSi7Cu3 alloy were investigated. 2D and 3D metallographic and image analysis have been performed to measure the microstructural changes occurring at different Sr, Fe and Mn levels and casting process. The evolution of mechanical properties of the alloys has been monitored by Brinell and Vickers hardness measurement and tensile tests. Addition of Sr slightly refines the eutectic silicon particles but it also introduces more pores. The combined addition of Fe and Mn induces an increase of Fe-rich intermetallic compounds which include both α-Al15(Fe,Mn)3Si2 and β-Al5FeSi phase, while the volume fraction of porosity decreases with the Fe and Mn content increase. The secondary dendrite arm spacing slightly decreases with the addition of Sr, Fe and Mn alloying elements.

Introduction

Aluminum-silicon (Al-Si) system alloys are characterized by their excellent castability, high thermal conductivity and low thermal expansion coefficient [START_REF] Kaufman | Aluminum alloy castings: properties, processes, and applications[END_REF]. These characteristics make them excellent candidates for automotive and aerospace applications.

The microstructure of alloys can be influenced by several alloying elements and casting process parameters [START_REF] Seifeddine | The influence of Fe and Mn content and cooling rate on the microstructure and mechanical properties of A380-die casting alloys[END_REF]. As the alloy properties are strongly affected by the resulting microstructure, controlling and understanding the influence of microstructure is a key issue in many industries. The microstructure of Al-Si alloys is defined by the size, morphology and content of eutectic Si phase, intermetallic compounds, and pores. Understanding the complex relationship between the mechanical properties and the microstructure of the Al-Si alloy requires a reliable way to identify and quantify this microstructure.

Al-Si alloys are often used for the production of automotive parts such as cylinder heads. To manufacture such complex parts at a reduced cost, the Lost Foam Casting (LFC) process offers a promising alternative to the traditional gravity Die Casting (DC) method in permanent mold with sand cores. However, the LFC process tend to show lower mechanical properties than parts produced with conventional casting processes due to the low cooling rate [START_REF] Albonetti | Porosity and Intermetallic Formation in Lost Foam Casting of 356 Alloy: National Library of Canada= Bibliothèque nationale du Canada[END_REF], thus it is necessary to compare the microstructures and properties of DC and LFC alloy. In addition, the alloy composition of cylinder heads produced from secondary alloys may vary within a given composition tolerance for each element [START_REF] Mbuya | Effective Recycling of Cast Aluminium Alloys for Small Foundries[END_REF]. This composition tolerance introduces microstructural variations that need to be understood. The influence of different alloys elements addition on the microstructure and mechanical properties of the Al-Si alloy has been already studied by some researchers [START_REF] Seifeddine | The influence of Fe and Mn content and cooling rate on the microstructure and mechanical properties of A380-die casting alloys[END_REF][START_REF] Fabrizi | The influence of Sr, Mg and Cu addition on the microstructural properties of a secondary AlSi9Cu3 (Fe) die casting alloy[END_REF]. Strontium (Sr) is commonly added to Al-Si alloys to improve mechanical properties by reducing the size and changing the morphology of the eutectic Si particles [START_REF] Dahle | Eutectic modification and microstructure development in Al-Si Alloys[END_REF], while more dispersed and round pores will be introduced with the Sr addition [START_REF] Dinnis | The influence of strontium on porosity formation in Al-Si alloys[END_REF]. In recent years, more secondary (recycled) aluminium alloys are used to replace primary alloys due to their lower energy consumption and comparable properties with primary aluminium alloys [START_REF] Hurtalová | Effect of chemical composition of secondary Al-Si cast alloy on intermetallic phases[END_REF]. Iron (Fe) is one of the most undesirable impurities in recycled aluminium alloys due to the formation of brittle intermetallics, called plate-like β-Al5FeSi intermetallics, which have been shown to act as stress raisers and lead to crack initiation and are thus detrimental to in-service mechanical properties [START_REF] Yi | Effect of Fe-content on fatigue crack initiation and propagation in a cast aluminum-silicon alloy (A356-T6)[END_REF][START_REF] Ma | A study of tensile properties in Al-Si-Cu and Al-Si-Mg alloys: Effect of β-iron intermetallics and porosity[END_REF]. The surface fraction and size of Fe-intermetallics in Al-Si alloy is affected by the Fe level [START_REF] Tash | Effect of metallurgical parameters on the hardness and microstructural characterization of as-cast and heat-treated 356 and 319 aluminum alloys[END_REF] and cooling rate [START_REF] Narayanan | Crystallization behavior of iron-containing intermetallic compounds in 319 aluminum alloy[END_REF]. The addition of manganese (Mn) can change the morphology of iron intermetallics from the deleterious plate-like morphology of the β-Al5FeSi phase to the less harmful Chinese script morphology of the α-Al15(Fe,Mn)3Si2 phase, and the degree of transformation depends on the cooling rate [START_REF] Narayanan | Crystallization behavior of iron-containing intermetallic compounds in 319 aluminum alloy[END_REF]. Seifeddine et al. [START_REF] Seifeddine | The influence of cooling rate and manganese content on the β-Al5FeSi phase formation and mechanical properties of Al-Si-based alloys[END_REF] showed that Mn additions are not able to totally nullify the formation of β-Al5FeSi-needles onto α-Al15(Fe,Mn)3Si2-Chinese scripts at high cooling rates for a 2:1 Mn:Fe ratio in an Al-9w.%Si alloy. In addition, several researchers have also investigated the effect of Fe on the porosity formation in Al-Si cast alloys [START_REF] Moustafa | Effect of iron content on the formation of β-Al5FeSi and porosity in Al-Si eutectic alloys[END_REF][START_REF] Roy | Porosity formation in AI-9 Wt pct Si-3 Wt pct Cu alloy systems: Metallographic observations[END_REF][START_REF] Taylor | The role of iron in the formation of porosity in Al-Si-Cu-based casting alloys: Part I. Initial experimental observations[END_REF]. Moustafa [START_REF] Moustafa | Effect of iron content on the formation of β-Al 5 FeSi and porosity in Al-Si eutectic alloys[END_REF] reported that a high Fe content can promote the formation of pores because the precipitation of β-phase can prevent the liquid metal to fill the spaces between the branched platelets as β-phase can block the interdendritic liquid channels and thus hinder liquid flow and feeding during solidification. Dinnis et al. [START_REF] Dinnis | Iron-related porosity in Al-Si-(Cu) foundry alloys[END_REF] reported that the effect of Fe content on porosity depends apparently on both the Si and copper (Cu) content. Another study by Taylor et al. [START_REF] Taylor | The role of iron in the formation of porosity in Al-Si-Cu-based casting alloys: Part I. Initial experimental observations[END_REF] indicates that a minimum level of porosity exists at an intermediate Fe content.

However, most of this research has been based on two-dimensional (2D) analysis of the microstructure due to the complexity in generating or accurately representing their three-dimensional (3D) microstructure. In fact, the over-idealized 2D microstructure does not effectively allow understanding the relationship between the microstructure and mechanical behavior of the alloys, especially for the pores, which play a vital role in determining the mechanical behavior [START_REF] Dezecot | In situ 3D characterization of high temperature fatigue damage mechanisms in a cast aluminum alloy using synchrotron X-ray tomography[END_REF].Thus, a preliminary 3D characterization of the pores to study how they are affected by alloy elements and casting process would appear to be particularly important.

In the present investigation, a full metallographic 2D and 3D characterization of the microstructure through optical-and Scanning Electron Microscopy (SEM) and laboratory X-ray tomography was performed in order to study the influence of variation in Sr, Fe, and Mn content within the composition tolerance of the AlSi7Cu3 alloy and of the casting process, i.e. Die casting (DC) and Lost Foam Casting (LFC), on the microstructure. The relationship between microstructure and mechanical properties was also studied. In order to achieve this, two primary, i.e. with low Fe levels, DC AlSi7Cu3 alloys with a different Sr content were used to study the Sr effect on the microstructure and mechanical properties. At the same time, two secondary, i.e. with high Fe levels, DC AlSi7Cu3 alloys with different Mn:Fe ratios were used to clarify the role of Fe and Mn. Besides, the secondary alloy with a lower ratio of Mn to Fe, which is usually used to manufacture commercial cylinder heads, was produced by two different casting methods, i.e. DC vs LFC, in order to study the effect of these processes.

Experimental procedures

Alloys and casting procedure

For the two primary DC AlSi7Cu3 alloys with different Sr content (i.e. alloy A and B), the base alloys were supplied as commercial ingots of primary alloy. Sr addition was achieved by introducing different amounts of an Al-10 wt. % Sr master alloy to the molten base alloy. For the two DC AlSi7Cu3 alloys with different Mn:Fe ratios (i.e. alloy C and D), the base alloy was received as ingots of secondary alloy. Different amounts of Sr, Fe and Mn in the form of Al-10 wt. % Sr, Al-25%Fe and Al-25%Mn master alloys were added into the melt, the holding time was over 60 min in the electric resistance furnace to achieve homogeneous melts.

The ingots were cut into smaller pieces, dried, and melted in a silicon carbide crucible, using an electric resistance furnace (temperature deviation of ±5 °C). The melting temperature was held at 735 ± 5 °C. High purity dry argon was used as degasser; the degassing period was 12min with a flow of 2l/min. The melt was then poured into the mold at about 720 ℃.

After the casting, 30 cylindrical cast specimens with the 20 mm diameter and 200 mm length were obtained for each composition, and each specimen was examined with X-ray radiography in order to assess the specimen porosity level. Each specimen was classified with a range between 1 to 8 according to the ASTM E155 standard [START_REF] Standard | Standard Reference Radiographs for Inspection of Aluminum and Magnesium Castings[END_REF]. The compositions of the experimental alloys were measured using a mass spectrometer and the results are given in Table 1. Some specimens that have a chemical composition, given in Table 1, similar to DC alloy C were cut from industrially manufactured cylinder heads obtained by LFC process.

Microstructural and mechanical characterization

The specimens for the characterization of the microstructure and mechanical properties were extracted from the center of cylindrical parts.

Characterization technologies

The measurement of pores characteristics was performed with X-ray laboratory Computed Tomography (Lab-CT) at a 2.75×2.75×2.75 µm 3 voxel size. Thanks to the absorption contrast provided by Lab-CT, the pores can be easily distinguished from the matrix. X-ray microtomography was realized at the LML laboratory (Lille, France) within an Ultratom (RX Solution) Lab-CT system fitted with a Nanofocus tube at an acceleration voltage of 70 kV. The specimen was placed on a rotating stage in the tomography chamber between the X-ray source and a Flat panel detector of dimensions 1920×1496 voxels. A set of 4320 radiographs (scan) were taken while the sample was rotating over 360° along its vertical axis. With an acquisition time per image of 330 ms, one scan lasted about 2 hours. The average analyzed volume for each alloy was about 32 mm 3 .

3D characterization for the Si phase could not be achieved with Lab-CT as Al and Si have close atomic numbers hence similar X-ray attenuation. As for intermetallic compounds, their size in DC alloys is too small compared to the tomography resolution. However, optical microscopy at a pixel size of 0.7µm gives enough contrast between the intermetallic phase, eutectic silicon and Al matrix, thus 2D metallographic analysis was used to characterize the Si phase and intermetallic compounds. The 2D microstructure observations were done using a Nikon YM-EPI light microscope equipped with a Sony color video camera and a JEOL 7800 F LV SEM. The EDS analyses were performed using the equipped OXFORD System Aztec and an X-Max 80 mm 2 premium spectrometer Microanalysis System. The size and morphology of eutectic silicon phase and intermetallic compounds were estimated for each alloy on polished samples covering an average area of about 1.2 mm 2 large enough to be representative of the whole sample.

Image processing

2D and 3D images were processed and analyzed using ImageJ/Fiji and Avizo Fire softwares, respectively, using the following procedure: (i) median filtering was applied prior to segmentation in order to reduce the noise in the image, (ii) a simple grayscale thresholding technique was used to segment the different phases, i.e. hard inclusions in the 2D images and pores in the 3D images.

Quantitative analysis could then be realized to label the objects, i.e. to attribute each individual object a given label or color, and to measure several characteristics of the labelled objects. Objects that are small as compared to the resolution of the images, i.e. with a volume less than 9 voxels in 3D or with an area less than 9 pixels in 2D, were neglected and discarded from the analysis.

The main parameters used to characterize the morphology of intermetallics, Si particles and pores are Feret diameter and sphericity (F). Feret diameter is defined as the longest distance measured between two parallel tangents on each side of the 2D or 3D object of interest. Feret diameter was used to assess the size of either pores or hard inclusions as it could better reflect not only the size but also the shape of objects. Sphericity corresponds to the ratio between the particle area and the area of the circle with the same perimeter as the object in 2D [START_REF] Ruxanda | Graphite shape characterisation in cast iron-from visual estimation to fractal dimension[END_REF] or to the ratio between the object volume and the volume of a sphere with the same surface as the object in 3D.

In order to determine the average value of the Secondary Dendrite Arm Spacing (SDAS) in one sample, the size of SDAS was obtained as an average value of at least 10 measurements.

Mechanical testing

Hardness measurements were performed on the polished samples. Vickers hardness measurements were carried out using a load of 30 kg and a 15 second dwell time. Each measurement represents the average of at least twelve indentation readings taken from different areas of the specimen.

Tensile tests were conducted as per ISO 6892-1 [START_REF] Iso | Metallic materials-tensile testing-Part[END_REF] on dog-bone shaped round samples of 5 mm gauge diameter and 30 mm gauge length. For each alloy, three tensile tests were carried out on a computer controlled testing machine (Instron) at a constant cross head speed of 1 mm/min. All the tests were performed at ambient temperature (∼25 °C). A strain gauge extensometer (gauge length of 25 mm) was used to measure the 0.2% proof stress, ultimate tensile strength and the elongation up to fracture.

Results and discussion

3.1 Microstructure examination

Secondary Dendrite Arm Spacing (SDAS) analysis

The typical microstructures obtained from alloy C in the cross section of samples are shown in Figure 1; the micrographs (a) and (b) refer to the DC and LFC, respectively. Compared with the DC alloy, the LFC alloy shows a coarser microstructure, i.e. larger SDAS, platelet eutectic Si particles, needle-like iron-intermetallics; SDAS values are given in Table 2. The average size of SDAS increased from 18.4µm to 76.4µm when the cooling rate decreased from 30°C/s (DC) to 0.8°C/s (LFC) [START_REF] Albonetti | [END_REF].

Figure 1 Optical microstructures of Alloy C in (a) DC and (b) LFC

Although the size of the dendrites appears strongly affected by the cooling rate, the chemical composition of the alloy has also some effect on this structural characteristic.

In order to study the effect of Sr, Fe and Mn content on the size of the microstructure, SDAS measurements were performed on the four different alloys having the chemical composition shown in Table 1. The average SDAS values are listed in Table 2. Comparing alloy A and alloy B, the addition of Sr from 47ppm to 133ppm leads to a SDAS reduction of about 6.25%, besides the SDAS slightly decreased from 19.5 µm to 17.0 µm when the content of Fe and Mn increased from 0.14 wt. % and 0.01 wt. % to 0.8 wt. % and 0.51 wt. %, respectively (Table 2).

SDAS variation appears slightly connected to the initial chemical composition of the alloy, i.e. to the Sr, Fe and Mn content. Similar results from Sanna et al. [START_REF] Sanna | Multiscale characterisation of AlSi9Cu3 (Fe) die casting alloys after Cu, Mg, Zn and Sr addition[END_REF] and Fabrizi et al. [START_REF] Fabrizi | The influence of Sr, Mg and Cu addition on the microstructural properties of a secondary AlSi9Cu3 (Fe) die casting alloy[END_REF] confirmed that SDAS varies when the content of alloying elements such as Sr, Cu, Fe and Mg is changed in Al-Si-Cu based DC alloys for a fixed solidification time. The refining effect of alloying elements on SDAS may be attributable to the solute segregation limiting the effective diffusion length when the dendrites are first formed during the solidification [START_REF] Sivarupan | Alloy Composition and Dendrite Arm Spacing in Al-Si-Cu-Mg-Fe Alloys[END_REF]; a higher concentration of alloying elements will cause the precipitation of finer dendrites and vice versa.

Porosity characterization

To the authors' knowledge, no experimental results have been reported showing use of 3D characterization of pores to study the influence of chemical composition on microstructure of Al-Si alloy. Some researchers [START_REF] Dinnis | The influence of strontium on porosity formation in Al-Si alloys[END_REF][START_REF] Dinnis | Iron-related porosity in Al-Si-(Cu) foundry alloys[END_REF] have studied the influence of different elements on pore formation for Al-Si alloys. However, their measurements are based on 2D analysis which cannot accurately characterize the features of pore. In the present work, in order to quantitatively characterize the distribution and size of the pores in 3D, cylindrical specimens with 3 mm length and 4 mm diameter were extracted from the center of the cast cylindrical bars and scanned with X-ray tomography. This allowed determining the volume fraction and characteristics of pores. Figure 2 shows the 3D rendering of the pores in different alloys and for different casting process at a voxel size of 2.45 µm. The measured pores characteristics for the four different AlSi7Cu3 alloys are provided in Table 3. In alloys A and B, the number and the volume fraction of pores increased by more than twice (Table 3) with the Sr content increase from 47ppm to 133ppm (see Table 1). The distributions of pores as a function of Feret diameter in alloy A and B in Figure 3 show that increasing Sr content introduces more fine pores in the range of 10 to 50 µm but also more large microshrinkage cavities in the range of 50 to 300 µm. The addition of Sr changes the amount of porosity as already reported by several studies [START_REF] Dinnis | The influence of strontium on porosity formation in Al-Si alloys[END_REF][START_REF] Emadi | The effect of Na and Sr modification on surface tension and volumetric shrinkage of A356 alloy and their influence on porosity formation[END_REF][START_REF] Liu | Influence of oxides on porosity formation in Srtreated Al-Si casting alloys[END_REF] due to a complex interaction of different parameters. Liu et al. [START_REF] Liu | Influence of oxides on porosity formation in Srtreated Al-Si casting alloys[END_REF] explain the increased porosity level with the content of Sr by the formation of strontium oxides due to the high affinity of Sr for oxygen; these strontium oxides are frequently observed associated with microporosity in Sr-modified alloys. Emadi et al. [START_REF] Ruxanda | Graphite shape characterisation in cast iron-from visual estimation to fractal dimension[END_REF] reported that the addition of Sr can reduce the surface tension, an effect that can facilitate porosity formation and results in increased porosity. Argo and Gruzleski [START_REF] Argo | Porosity in modified aluminum alloy castings[END_REF] indicate that interdendritic feeding becomes more difficult in modified alloys as they have a longer mushy zone due to the depression of the eutectic temperature. Consequently, more pores may form over a longer period, which explains the larger microshrinkage cavities observed in alloy B.

Figure 3 Size distribution of pores in number (Nv) and in volume (%) for alloy A and B in Die casting

Prior to 3D characterization of pores in DC alloys, the presence of porosity was studied by X-ray radiography for DC alloys B, C and D; for each alloy, 30 specimens were analyzed. ASTM E155 standard gives the criteria to define the 'qualitative' amount of porosity allowable and defines 8 defect classes. Figure 4 shows the frequency distribution of shrinkage cavity level according to the standard ASTM E155. The maximum pore density is observed at alloy B which has the lowest Fe and Mn content among the four alloys. The result of 2D X-ray radiography characterization shows that the porosity level seems to decrease with an increase in the Fe and Mn content.

From the 3D characterization results, the volume fraction of pores decreased from 0.065% to 0.032% when the Fe and Mn content increased from 0.14% and 0.01% to 0.80% and 0.51% for the DC alloys B, C and D (Table 2). This confirmed the previous qualitative results of 2D characterization for pores, and it also proves that decreased porosity level results from an increase of Fe and Mn content in some extent. However, this result is in contradiction with some reports [START_REF] Moustafa | Effect of iron content on the formation of β-Al5FeSi and porosity in Al-Si eutectic alloys[END_REF][START_REF] Dash | Effect of key alloying elements on the feeding characteristics of aluminumsilicon casting alloys[END_REF] that claim iron-intermetallics help nucleate pores. Studies made by Taylor et al. [START_REF] Taylor | The role of iron in the formation of porosity in Al-Si-Cu-based casting alloys: Part I. Initial experimental observations[END_REF] and Dinnis et al. [START_REF] Dinnis | Iron-related porosity in Al-Si-(Cu) foundry alloys[END_REF] indicates that the existence of a critical Fe content for a minimum porosity formation in unmodified Al-Si-Cu alloy, and that different solidification paths resulting from different Fe levels lead to variations in microstructural permeability, i.e. interdendritic feedability, and hence in porosity formation. Besides in the study of Puncreobutr et al. [START_REF] Puncreobutr | Quantitative 3D Characterization of Solidification Structure and Defect Evolution in Al Alloys[END_REF], larger pores were observed to nucleate before the intermetallics during in-situ solidification of an A319 alloy at 0.36°C/s. Thus, maybe it is more interesting to study the influence of Fe content on the porosity formation through in-situ solidification experiment.

Figure 4 The frequency distribution of shrinkage cavity level according to the standard ASTM E155 for alloys B, C and D

In the present work, the decrease in porosity content could also be due to the increase of Mn content in alloys B, C and D. As reported by Dinnis et al. [START_REF] Dinnis | Porosity formation and eutectic growth in Al-Si-Cu-Mg alloys containing iron and manganese[END_REF], the addition of Mn also can reduce the amount of porosity, because Mn additions reduce the poisoning of Al-Si eutectic nucleation sites by Fe. This leads to the formation of a greater number of smaller Al-Si grains during solidification and in turn results in improved permeability and feeding, and hence a reduction in porosity. According to Dinnis et al. [START_REF] Dinnis | Porosity formation and eutectic growth in Al-Si-Cu-Mg alloys containing iron and manganese[END_REF], the addition of 0.5%Mn to a 1%Fe-containing Al-9%Si alloy can reduce porosity levels to those obtained in the same alloy with 0.6%Fe (i.e. the critical iron content for that composition). Moreover, as mentioned before, the decrease of Sr content from 130 ppm to 100 ppm also can contribute to the slight decrease of porosity fraction for alloy B, C and D. These may be the reasons why alloy D, which has higher Fe/Mn content and lower Sr content, has lower porosity level.

The effect of casting process (DC vs. LFC) on the porosity was also investigated. As shown in Figure 2, a decrease in cooling rate from 30°C/s (DC) to 0.8°C/s (LFC) increases both the total volume of porosity and the average pore size measured in alloy C (Table 3).

The distribution of pores as function of Feret diameter for DC and LFC is shown in Figure 5. DC alloy has more micropores within the range of 10 to 200 µm than LFC alloy. However LFC alloy has larger pores with a maximum Feret diameter up to 1535µm, and the largest pore represent approximately 45% of the total volume fraction of the pores population (see Figure 5). The significant difference in porosity content and size between DC and LFC alloys can be explained by the different cooling rate during solidification. At increasing solidification rates, hydrogen has less time to diffuse into the interdendritic spaces of the partially solidified metal [START_REF] Seifeddine | The influence of Fe and Mn content and cooling rate on the microstructure and mechanical properties of A380-die casting alloys[END_REF], resulting in more finely dispersed porosity. Furthermore, the higher temperature gradients present at higher solidification rates tend to limit the length of the mushy zone, making feeding easier and retarding porosity formation [START_REF] Emadi | Combating Al-Si porosity: the strontium/hydrogen myth[END_REF]. In addition, LFC casting method utilizes an evaporative pattern which may increase the entrapped gas content in the alloy and hence lead to increased porosity. The spherical gas porosity, which is observed in LFC alloy (Figure 2(e)), could be due to entrapment of gas bubbles in the casting [START_REF] Caceres | Casting defects and the tensile properties of an AlSiMg alloy[END_REF].

Figure 5 The distribution of pores as function of Feret diameter for DC and LFC alloys

Eutectic Si characterization

Mechanical properties of Al-Si alloys are known to be influenced by the size, shape and distribution of eutectic silicon present in the microstructure. Thus, Al-Si alloys are generally subjected to Si modification in order to improve mechanical properties. Si modification, which transforms the acicular silicon morphology to fibrous one resulting in a noticeable improvement in elongation and strength [START_REF] Hegde | Modification of eutectic silicon in Al-Si alloys[END_REF], can be achieved in three different ways: modification by addition of some elements (chemical modification) or with a rapid cooling rate (quench modification), globalization by high temperature annealing.

The effect of Sr content

The effect of Sr as a modifying agent on the microstructure of gravity die cast Al-Si alloys is widely reported in literature [START_REF] Dahle | Eutectic modification and microstructure development in Al-Si Alloys[END_REF][START_REF] Haque | Effects of strontium on the structure and properties of aluminium-silicon alloys[END_REF][START_REF] Kosa | Effects of strontium on the microstructure of Al-Si casting alloys[END_REF]. The addition of Sr promotes the formation of a fibrous silicon structure by retarding the growth rate of silicon [START_REF] Hegde | Modification of eutectic silicon in Al-Si alloys[END_REF]. The effect of Sr content on the modification of the eutectic Si particles was studied in alloys A and B. The micrographs of alloy A (Figure 6a) and alloy B (Figure 6b) in different magnification are compared in Figure 6: eutectic Si appears as the darkest phase. In both cases the effect of modification of eutectic Si is visible. However, significant differences in the extent of the modification between alloy A and B cannot be observed by naked eye from Figure 6 . Thus, quantitative metallographic characterization of eutectic Si particles was performed with image analysis in terms of sphericity. The distributions of eutectic Si particles morphology in Figure 8 show that more eutectic Si particles with sphericity above 0.4 were present in alloy B compared to alloy A; this means that the amount of plate-like morphology eutectic Si decreased with an increase in the content of Sr. As a result, the higher the Sr content, the more eutectic Si shows a fibrous and globular morphology in Srmodified alloy. Eutectic Si particles modification was shown to depend not only on the cooling rate, but also on the Sr content. Besides the effect due to cooling rate is stronger than that due to Sr addition at high cooling rate (SDAS=20µm).

Figure 6 Optical micrographs of alloy A (a) and alloy B (b) in Permanent mold casting; eutectic

Si is the dark phase

The effect of cooling rate

A typical eutectic microstructure of both DC and LFC AlSi7Cu3 alloy is shown in Figure 7 in the same magnification. From this figure, casting process appears to have a significant impact on eutectic modification for AlSi7Cu3 alloy. The DC alloy in Figure 6(a) clearly shows the fine fibrous morphology of the eutectic Si phase. In contrast, the LFC alloy in Figure 7(b) reveals the eutectic Si phase that appears as platelets.

Iron Intermetallic compounds

The effect of Fe, Mn content and casting process on the formation of the Fe-rich intermetallic compounds was studied in alloys B, C, and D. Manganese is often added in Al-Si alloy to alter the shape of iron intermetallics from sharp needle β-phase Al5FeSi to a more compact type α-phase Al15(Fe,Mn)3Si2 in order to reduce the embrittlement due to the needle morphology. Besides, the amount of α-phase and β-phase depends on Fe-Mn levels and on the cooling rate [START_REF] Seifeddine | The influence of Fe and Mn content and cooling rate on the microstructure and mechanical properties of A380-die casting alloys[END_REF][START_REF] Narayanan | Crystallization behavior of iron-containing intermetallic compounds in 319 aluminum alloy[END_REF].

The size and morphology, i.e. maximum length, surface area fraction, of iron-intermetallics are listed in Table 4. Small size α-phase is extremely difficult to distinguish from β-phase as their shape and gray level are similar in 2D optical images as well as in BSE images. Thus the iron-intermetallics mentioned in this part include both α-and β-phase. phases were measured by EDX (at%), and the results are provided in Table 5, which allowed identifying the α-phase (yellow arrow) with a script morphology (point 2 and 5) and β-phase (red arrow) with an acicular or plate-like morphology (point 1, 3 and 4) in Figure 9a-h. The distributions of ironintermetallics as functions of Feret diameter and sphericity for alloy B, C and D are presented in Figure 10a andb. As can be seen from Figure 10a, the peak which corresponds to an average size of ironintermetallics shifted with the Fe and Mn content changed, when the Fe and Mn content increased from 0.14% and 0.01% to 0.80% and 0.51%, the average size of iron-intermetallics increased from 5.6 µm to 15.8 µm. Figure 10b shows those iron-intermetallics with sphericity less than 0.3 increases with increasing content of Fe and Mn. It can be concluded that the amount of β-Al5FeSi phase in needle-like shape increases with the Fe content increases in the alloys.

As shown in Table 4, the maximum length and the surface fraction of the iron-intermetallics increased as the iron and manganese content increased. All alloys exhibit almost linear relationships: the higher the iron and manganese content, the higher the surface fraction of the iron-intermetallics. As seen from Figure 9c, g and h, alloy D, with the highest content of Fe and Mn, showed the largest surface fraction of iron-intermetallic compounds, which mainly consisted in the β-phase, with the needle-like morphology (Figure 9g), and in some α-phase (Figure 9h). Figure 9a andd showed that in alloy B, with the lowest content of Fe and Mn, only a few amount of small size β-Al5FeSi phase with its typical needle-like morphology was observed. A higher fraction of iron-intermetallic compounds was detected in alloy C, with intermediate Fe content and a Mn to Fe ratio of 0.26, as compared to alloy B. Besides the addition of Mn promotes the formation of script α-phase Al15(Fe,Mn)3Si2 (Figure 9b, e and f) [START_REF] Lu | Iron-rich intermetallic phases and their role in casting defect formation in hypoeutectic Al-Si alloys[END_REF]. Figure 9a, b andc show that the ratio of α and β phases increased as the Mn/Fe ratio increased from alloy B to alloy D. The influence of the cooling rate on distributions of iron-intermetallics as functions of Feret diameter and sphericity can be observed in Figure 10a andb. Optical micrographs show the β platelets (arrowed) in the microstructure of alloy C in both die (Figure 11a) and lost foam casting (Figure 11b). It should be noted that the variation in size of the Fe-intermetallics in both DC and LFC alloy may also exist due to their formation at different stages during solidification. For the LFC alloy C, large size intermetallics (i.e. Feret diameter larger than 50µm) with small sphericity represent most of the total volume fraction of the intermetallics phase (Figure 10). The maximum length of iron-intermetallic compounds increased from 56.3µm to 245.5µm when the cooling rate decreases from 30°C/s (DC) to 0.8°C/s (LFC), respectively (Table 4). The longer time available for growth of iron-intermetallic at lower cooling rate may explain the larger size of intermetallics. As reported by Ceschini et al. [START_REF] Ceschini | Microstructure, tensile and fatigue properties of the Al-10% Si-2% Cu alloy with different Fe and Mn content cast under controlled conditions[END_REF], the size of intermetallic compounds mainly depends on the solidification time (i.e., cooling rate). Moreover, as reported in Table 4, the surface area fraction of the iron-intermetallics also increased from 1.81% in DC alloy to 2.32% in LFC alloy.

Copper based phase

Cu-bearing particles were also detected in the studied alloys. As shown in Figure 9d, the Al2Cu phase connects with the iron intermetallics so that it can be reasonably assumed that the β-platelets act as nucleation sites for the copper phase particles [START_REF] Li | Effect of alloying elements on the segregation and dissolution of CuAl2 phase in Al-Si-Cu 319 alloys[END_REF].

In this work, the quantitative metallography analysis shows that alloying elements (such as Sr, Fe and Mn) have no effect of the amount and morphology of Al2Cu phase. However, the cooling rate resulting from different casting process can significantly affect the formation of Al2Cu phase. The distributions of Al2Cu as functions of Feret diameter and sphericity in DC and LFC for alloy C are reported in Figure 12a andb. The LFC alloy with the lower cooling rate presents larger Al2Cu particles, which correspond to most of the surface fraction (Figure 12a), this could also be attributed to the longer time available for growth of Al2Cu phase at lower cooling rate. Figure 12b shows that more Al2Cu phase with sphericity above 0.3 was present in DC alloy compared to LFC alloy. Thus, the morphology of Al2Cu phase becomes more round with an increase in the cooling rate; this can be explained by the fact that at increasing cooling rate, an increased nuclei number could affect the number, and thus, the size and morphology of the Al2Cu phase precipitates [START_REF] Labisz | Phases morphology and distribution of the Al-Si-Cu alloy[END_REF].

Mechanical properties

The mechanical properties, such as hardness, UTS, YS and elongation (%El) values obtained in the present study were analyzed with respect to the different microstructure involved, viz. SDAS, amount, size of eutectic Si, iron Intermetallic compounds, and porosity. The relationship between the microstructure and mechanical properties for the studied alloys will be discussed in the following sections.

Hardness test

The hardness trend observed in the different alloys shows an opposite behavior to SDAS value (Table 6) when comparing DC to LFC alloy C at an almost constant area fraction of iron intermetallic. The Vickers hardness of alloy C decreases from 80.8HV to 63.5HV when the SDAS increases from 18.4µm (DC) to 76.4µm (LFC); this result proves that the evolution of hardness also depends on the SDAS of alloys. In agreement with the results from Sanna et al. [START_REF] Sanna | Multiscale characterisation of AlSi9Cu3 (Fe) die casting alloys after Cu, Mg, Zn and Sr addition[END_REF], Sofyan et al. [START_REF] Sofyan | Grain refinement of AA333 aluminium cast alloy by Al-Ti granulated flux[END_REF] and Krupiński et al. [START_REF] Krupiński | Derivative thermo-analysis application to assess the cooling rate influence on the microstructure of Al-Si alloy cast[END_REF], the hardness decreases with an increase in the size of SDAS. To investigate the influence of Sr, Fe and Mn content on the variation in hardness, Vickers hardness measurements for each alloy are reported in Table 6. Sr addition from 47ppm (alloy A) to 130ppm (alloy B) has no obvious effect on the hardness. However, comparison of the alloys A, B and C shows that the hardness increases from 85.3HB (alloy B) to 95.1HB (alloy D) when the iron content increases from 0.1 wt. % to 0.8 wt. %. Besides the alloy D, where the Fe level was highest (0.8%), shows the highest hardness value. This hardness increase is in agreement with Ref. [START_REF] Tash | Effect of metallurgical parameters on the hardness and microstructural characterization of as-cast and heat-treated 356 and 319 aluminum alloys[END_REF][START_REF] Moustafa | Effect of iron content on the formation of β-Al 5 FeSi and porosity in Al-Si eutectic alloys[END_REF], where it is reported that the increase of Fe content increases the hardness of Al-Si alloys as the Fe-intermetallic surface fractions increase. The hardness strongly depends on the composition and fraction of phases in the material. According to Seifeddine et al. [START_REF] Seifeddine | The influence of cooling rate and manganese content on the β-Al 5 FeSi phase formation and mechanical properties of Al-Si-based alloys[END_REF], the hardness of intermetallic compounds obtained from nanoindentation measurements, i.e. β-Al5FeSi-needle (11.5 GPa) and α-Al15(Fe, Mn)3Si2-script phase (14.8 GPa), is larger than that of Al matrix (2.1 GPa). Thus, the almost linear hardness increase with the amount of hard phase reported in Table 6 can be expected for a given SDAS value.

Tensile test

The tensile properties (i.e., ultimate tensile strength, Young modulus, yield strength and elongation) at room temperature are shown in Table 7.

• The effect of Sr

By comparing alloy A with B, the Sr content increase from 47ppm to 130ppm has no obvious influence on the UTS and YS. Thus slightly different morphology of eutectic Si resulting from a different Sr content has a negligible effect on the mechanical properties. The slight decrease of plastic elongation may be due to the increased pore volume fraction [START_REF] Ma | A study of tensile properties in Al-Si-Cu and Al-Si-Mg alloys: Effect of β-iron intermetallics and porosity[END_REF]. In addition, the Young's modulus depends on the volume fraction of the alloy components (such as Al matrix and hard inclusions) [START_REF] Lasagni | Enhanced Young's Modulus of Al-Si Alloys and Reinforced Matrices by Cocontinuous Structures[END_REF] and has no obvious reason to vary with Sr. Besides, as shown in Table 7, the variation of Young's modulus with Sr is within the standard deviation.

• The effect of Fe and Mn

The effect of Fe content on the mechanical properties of the DC AlSi7Cu3 alloys is shown in Figure 13. A slight increase in the yield strength, a slight decrease in the UTS and a significant decrease in the elongation is observed when increasing the Fe-Mn content. The elongation to failure decreases due to the increased volume fraction of iron-intermetallics especially the needle-like β-phase [START_REF] Seifeddine | The influence of Fe and Mn content and cooling rate on the microstructure and mechanical properties of A380-die casting alloys[END_REF]. As mentioned previously, the Fe-containing intermetallics particles are more easily fractured under tensile load than the aluminium matrix or the fine silicon particles [START_REF] Taylor | The effect of iron in Al-Si casting alloys[END_REF]. As reported by Wang et al. [START_REF] Wang | Tensile properties of aluminum die-casting alloys[END_REF], the cracking of Fe-rich compounds tends to account for most of the damage when the Si particles are small. On the other hand, due to the very low pore volume fraction (i.e. 0.03% to 0.06%) in the DC alloys, the effect of pore on elongation is negligible compared to the effect of Fe-containing intermetallics. In addition, Fe can slightly increase the yield strength of Al-Si alloys as reported by Ji et al. [START_REF] Ji | Effect of iron on the microstructure and mechanical property of Al-Mg-Si-Mn and Al-Mg-Si diecast alloys[END_REF], and this is usually accompanied by an increase in hardness. The experimental results have confirmed that the amount of Fe-rich intermetallics significantly affect the mechanical properties of the Al-Si-Cu alloys.

Table 6 and Table 7 show that the Young's modulus increased from 71.2 GPa to 80.4 GPa when the surface fraction of iron-intermetallics increased from 0.22% to 2.48%, i.e. for the alloys B and D. This increase of Young modulus with Fe content is mainly due to the hardness and rigidity of ironintermetallics, which is higher than that of Al matrix [START_REF] Seifeddine | The influence of cooling rate and manganese content on the β-Al5FeSi phase formation and mechanical properties of Al-Si-based alloys[END_REF].

Figure 13 The effect of Fe content on the mechanical properties of the DC AlSi7Cu3 alloys (YS: yield strength; UTS: ultimate tensile strength; El: elongation).

• The effect of casting process

The mechanical properties also depend on the casting process. As shown in Table 7, the lower Young's modulus and yield strength of LFC alloy as compared to DC alloy can be explained by the pore volume fraction that is higher in LFC alloy than in DC alloy [START_REF] Mugica | Effect of porosity on the tensile properties of low ductility aluminum alloys[END_REF]. Besides, Seifeddine et al. [START_REF] Seifeddine | Prediction of mechanical properties of cast aluminium components at various iron contents[END_REF] reported that the dendrites are likely to get enriched with Si at a rapidly cooling rate; the higher Si induces a higher strength of the Al matrix in DC alloy.

The average ultimate tensile strength (UTS) has significantly decreased from 254MPa for DC alloy to 180 MPa for LFC alloy, this might be due to the lower SDAS in DC alloy [START_REF] Ceschini | Correlation between ultimate tensile strength and solidification microstructure for the sand cast A357 aluminium alloy[END_REF]. However, the plastic elongation of LFC alloy is severely reduced compared with DC alloy with a plastic elongation that decreased from 2.1% for the DC alloy to 0.15% for the LFC. The decreased elongation can be attributed to the more numerous and larger pores and coarser microstructures in terms of larger SDAS [START_REF] Li | Parameters controlling the performance of AA319-type alloys: Part I. Tensile properties[END_REF], platelike eutectic Si particles, iron-intermetallics in LFC alloy compared to DC alloy. These coarser flakes of eutectic Si particles (Figure 7) in LFC alloy promote brittleness. Hafiz et al. [START_REF] Hafiz | Mechanical properties of modified and nonmodified eutectic Al-Si alloys[END_REF] reported that the nucleated crack seems to propagate in a brittle manner in the large plate-like eutectic Si particles while Si particles having a fine fibrous morphology fracture in a ductile fashion. Besides, as reported by Ma et al. [START_REF] Ma | A study of tensile properties in Al-Si-Cu and Al-Si-Mg alloys: Effect of β-iron intermetallics and porosity[END_REF], the β-Al5FeSi platelet size is also essential to Al-Si alloy ductility and increasing β platelet size from 25 μm to 200 μm causes a significant decrease in elongation (from 14% to 1%). As shown in Table 4, the maximum length of iron-intermetallic increases from 56.3 µm in DC alloy to 245.5 µm in LFC alloy. In addition, the presence of pores facilitates fracture. Large pores, especially shrinkage pores, have an irregular 3D shape, which induces stress concentration, and they are usually responsible for crack initiation during loading [START_REF] Savelli | Pore characterization in a model cast aluminum alloy and its quantitative relation to fatigue life studied by synchrotron X-ray microtomography[END_REF] as reported by Wang et al. for an A319 LFC alloy [START_REF] Wang | Influence of pores on crack initiation in monotonic tensile and cyclic loadings in lost foam casting A319 alloy by using 3D in-situ analysis[END_REF]. The large shrinkage porosity found in LFC alloy (Figure 2e) may impose this detrimental effect on mechanical properties. Therefore, DC alloys with the refinement of microstructures (i.e. eutectic Si, ironintermetallics) and fewer defects tend to show higher tensile properties.

Conclusion

In the present study, five batches of AlSi7Cu3 alloy with different contents in alloying elements (Sr, Fe and Mn) were obtained by two different casting processes (DC and LFC). Microstructural and mechanical characterizations were performed to relate microstructural features resulting from different metallurgical parameters to mechanical properties. The following main conclusions could be drawn:

1. The size of the dendrites is strongly affected by the cooling rate. However, the chemical composition of the alloys has also some effect on the SDAS, which slightly decreases with the incremental addition of Sr, Fe and Mn. 2. A finer and more fibrous eutectic Si structure can be obtained with an increased Sr content with the drawback that the Sr addition can introduce more pores in the DC alloy. However, no change of the tensile properties with the Sr content increase from 47ppm to 130ppm was noticed. 3. The morphology and surface fraction of iron-intermetallic are influenced by the Fe and Mn content: the amount of Fe-intermetallics (α-Al15(Fe,Mn)3Si2 and β-Al5FeSi phase) increases with an increase in the Fe-Mn level while the ratio of α and β phases increased with the increase of Mn/Fe. In addition, a slight decrease of pore volume fraction is observed with an increase in the Fe and Mn content in some extent. 4. Iron has a detrimental effect on the UTS and above all on ductility in terms of the amount of β-Al5FeSi phase. However, Fe addition increases YS in the alloys studied, i.e. the presence of iron can harden the alloy to some extent. 5. Mechanical properties of AlSi7Cu3 alloy are highly influenced by casting process by the intermediate of the microstructure. The LFC AlSi7Cu3 alloy shows more casting defects (i.e. larger pores and microshrinkage cavities), a coarser microstructure (i.e. larger SDAS, plate-like eutectic Si particles, needle-like iron-intermetallics) than DC AlSi7Cu3 alloy. DC alloys showed higher UTS, YS and elongation than LFC alloy.

In order to understand the damage mechanisms associated to the different hard inclusions characteristics that result from different Sr, Fe, Mn content and casting process, ongoing studies examine the role of the different hard particles (i.e. eutectic Si, iron-intermetallics and Al2Cu phases) on the propagation of cracks by in-situ tensile tests observation.

Figure 2 3D

 2 Figure 2 3D rendering of pores for alloys (a) A, (b) B, (c) C and (d) D in DC, and (e) alloy C in LFC. (Dimension: Ø3.7mm×Height 3mm)

Figure 7

 7 Figure 7 Optical micrographs showing eutectic Si microstructure in (a) Permanent mold casting, (b) Lost Foam casting for alloy C The distributions of eutectic Si phase as function of the Feret diameter in DC and LFC alloy C are shown in Figure 8a. Due to the differences in the cooling rate between LFC and DC, the distributions of eutectic Si phase as function of the Feret diameter are quite different from each other. More small eutectic Si particles, i.e. with a size between 1 and 13 µm, are distributed in DC alloy compared to LFC alloy. On the other hand, more large eutectic Si particles, which correspond to most of the surface fraction, were revealed in LFC alloy; the largest Feret diameter of eutectic Si can reach up to 141µm in LFC compared to 32µm in DC.In addition, the distributions of sphericity in Figure8bshow that at low cooling rate (i.e. LFC alloy), the alloy C shows more Si particles with sphericity less than 0.3 than at high cooling rate (i.e. DC alloy). As shown in Figure6, most of the eutectic Si present in DC appears with a fibrous morphology when the Sr content is 120 ppm in alloy C. However, the addition of the same Sr level to

Figure 8

 8 Figure 8 Distributions of Feret diameter (a) and sphericity (b) of eutectic Si particles in alloy A, B, C and D

  Figure 9a-h shows SEM micrographs of AlSi7Cu3 alloys containing different Fe and Mn content, i.e. alloy B, C and D. The composition of the iron-intermetallic

Figure 9 Figure 10

 910 Figure 9 Backscattered electrons SEM micrographs showing the distribution of α-phase Al15 (Fe,Mn)3Si2 (yellow arrow) with a script morphology, β-phase Al5FeSi (red arrow) with a needle morphology and Al2Cu phase (blue arrow) in the (a) alloy B, (b) C and (c) D. Points of EDX microanalysis are labeled, and the results are available in Table 5.

Figure 11

 11 Figure 11 Optical micrographs showing iron-intermetallics in (a) Permanent mold casting, (b) Lost Foam Casting for alloy C

Figure 12

 12 Figure 12 Distributions of Al2Cu as functions of Feret diameter (a) and sphericity (b) in DC and LFC for alloy C

Table 1

 1 Chemical compositions of the experimental AlSi7Cu3 alloys (wt. %)

	Allo y	Castin g method	Al	Si	Fe	Mn	Mn/F e	Sr	Cu Mg	Ti	Pb	Zn
	A	DC	bal .	6.9 1	0.1 0	0.00 7	0.07	0.004 7	2.8 9	0.2 9	0.11	0.00 3	0.02 2
	B	DC	bal .	7.0 1	0.1 4	0.01 0	0.07	0.013 3	3.3 6	0.3 0	0.11	0.00 4	0.03 3
	C	DC LFC	bal . bal .	7.6 6 7.8 5	0.4 9 0.3 0	0.13 0 0.19 0	0.26 0.63	0.012 0 0.012 0	3.6 7 3.0 5	0.3 1 0.2 8	0.11 0.09 8	0.05 4 0.01 5	0.33 0.16
	D	DC	bal .	7.0 0	0.8 0	0.51 0	0.64	0.010 0	3.4 5	0.2 8	0.12 0.05 0.24

Table 2 SDAS in four different studied alloys SDAS

 2

	A	DC	20.8	2.4
	B	DC	19.5	2.4
	C	DC LFC	18.4 76.4	2.1 6.9
	D	DC	17.0	2.3

(µm) Alloy code Casting method Mean Standard deviation

Table 3 Porosity characteristics as a function of alloy composition and casting method. Feret diameter (µm)

 3

	Alloy	Casting method	Volume fraction %	Av.	Max.	Analysed volume (mm 3 )	Density (particles/mm 3 )
	A	DC	0.034	30	276	30.8	94
	B	DC	0.065	28	294	31.2	200
	C	DC LFC	0.045 0.940	27 64	279 1536	31.2 33.0	174 17
	D	DC	0.032	24	299	31.6	97

Table 4 The maximum length and surface area fraction of iron-intermetallics for the alloys B to D.

 4

						Dimension and quantity
	Sample code	Fe wt.%	Mn wt.%	Mn/Fe	Casting process	of iron-intermetallics maximum Surface area
						length (µm)	fraction(%)
	Alloy B	0.14	0.01	0.07	DC	23.2	0.22
	Alloy C	0.49 0.30	0.13 0.19	0.26 0.63	DC LFC	56.3 245.5	1.81 2.32
	Alloy D	0.80	0.51	0.64	DC	63.0	2.48

Table 5 EDX analysis of the intermetallic compounds in Figure 9

 5

	Alloy	Number	Al	Element content (at. %) Si Mn	Fe	Identified phase
	B	1	62.97	24.76	0.34	11.93	Al5FeSi
	C	2 3	71.12 52.59	12.40 32.49	3.51 2.56	12.97 12.36	Al15 (Fe,Mn)3Si2 Al5FeSi
	D	4 5	60.90 71.52	26.03 11.86	4.06 6.93	9.02 9.69	Al5FeSi Al15 (Fe,Mn)3Si2

Table 6 Vickers hardness, area fraction of iron-intermetallic and DAS measured from investigated alloys

 6

	Alloy	Casting process	Average Vickers hardness (HV/30)	Area fraction of iron-intermetallic (%)	Mean SDAS (µm)
	A	DC	73.7	0.16	20.8
	B	DC	74.9	0.22	19.5
	C	DC LFC	80.8 63.5	1.81 2.32	18.4 76.4
	D	DC	83.8	2.48	17.0

Table 7 Tensile properties of studied alloys

 7

	Alloy	Casting process	Young modulus [GPa]	Yield Strength [MPa]	Ultimate Tensile Strength [MPa]	Plastic Elongation [%]
	A	DC	75.2±4.5	81	256±3	3.8±0.3
	B	DC	71.2±3.8	83	258±4	3.2±0.5
	C	DC LFC	77.6±6.0 67.5±1.2	88 78	254±10 180±3	2.1±0.2 0.29±0.02
	D	DC	80.4±5.1	93	239±3	1.3±0.1

Acknowledgement

The authors wish to thank the ANR (Agence Nationale de la Recherche) MatetPro project INDiANA (ANR-12RMNP-0011) for funding the study on Al-Si alloys. The ISIS4D X-Ray CT platform (LML, France) is also acknowledged for microtomographic acquisition.