Andreas Teucke

Marco Voigt

Christoph Weidenbach

On the Expressivity and Applicability of Model Representation Formalisms

A number of first-order calculi employ an explicit model representation formalism in support of non-redundant inferences and for detecting satisfiability. Many of these formalisms can represent infinite Herbrand models. The first-order fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism used in the approximation refinement calculus (AR). Our first result is a finite model property for MSLH clause sets. Therefore, MSLH clause sets cannot represent models of clause sets with inherently infinite models. Through a translation to tree automata, we further show that this limitation also applies to the linear fragments of implicit generalizations, which is the formalism used in the model-evolution calculus (ME), to atoms with disequality constraints, the formalisms used in the non-redundant clause learning calculus (NRCL), and to atoms with membership constraints, a formalism used for example in decision procedures for algebraic data types. Although these formalisms cannot represent models of clause sets with inherently infinite models, through an additional approximation step they can. This is our second main result. For clause sets including the definition of an equivalence relation with the help of an additional, novel approximation, called reflexive relation splitting, the approximation refinement calculus can automatically show satisfiability through the MSLH clause set formalism.

Introduction

Proving satisfiability of a first-order clause set is more difficult than proving unsatisfiability, in general. Still, for many applications the detection of failing refutations by establishing a counter model is more than desirable. In the past, several methods, calculi and systems have been presented that can detect satisfiability of a clause set, in particular, if there is a finite model that is not too large. The approaches can be separated into the following classes:

(1) the model building is integrated into a first-order calculus or a decision procedure for some fragment, directly operating on the first-order clause set, complete for unsatisfiability, e.g., [START_REF] Caferra | Automated Model Building[END_REF][START_REF] Baumgartner | Lemma learning in the model evolution calculus[END_REF][START_REF] Piskac | Deciding effectively propositional logic using DPLL and substitution sets[END_REF][START_REF] Suter | Decision procedures for algebraic data types with abstractions[END_REF][START_REF] Alagi | NRCL -A model building approach to the Bernays-Schönfinkel fragment[END_REF][START_REF] Maria | On first-order model-based reasoning[END_REF][START_REF] Bonacina | Semantically-guided goal-sensitive reasoning: Model representation[END_REF],

(2) the model building is integrated into a first-order calculus that operates on the first-order clause set modulo an approximation, complete for unsatisfiability, e.g., [START_REF] Korovin | Inst-gen -A modular approach to instantiation-based automated reasoning[END_REF][START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF][START_REF] Cesar | Towards an abstractionrefinement framework for reasoning with large theories[END_REF], (3) the model building aims at finding finite models without being complete for unsatisfiability, e.g., [START_REF] Slaney | FINDER: finite domain enumerator -system description[END_REF][START_REF] Mccune | Mace4 reference manual and guide[END_REF][START_REF] Claessen | New techniques that improve mace-style finite model finding[END_REF], (4) the model building aims at finding finite and infinite models without being complete for unsatisfiability, e.g., [START_REF] Peltier | Constructing infinite models represented by tree automata[END_REF],

where superposition [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] does not belong to any of the above classes, because the model building is implicit and reached by a finite saturation of the clause set modulo inferences and the elimination of redundant clauses.

The approaches in classes ( 1) and ( 2) select inferences with respect to the explicit (partial) model by identifying a false clause (instance). Therefore, the representation of models needs to be effective, e.g., falsity of a clause (instance) with respect to the model needs to be (efficiently) decidable.

For superposition it is undecidable whether a clause is false with respect to a saturated clause set, in general. This can be seen by a reduction through the Post Correspondence Problem (PCP) [START_REF] Post | A variant of a recursively unsolvable problem[END_REF]. The clause set consisting of R( , ) and clauses R(x, y) → R(t i [x], s i [y]) where the t i , s i are terms built over the monadic functions g, h and variables x, y, respectively, is saturated with strictly maximal atoms R(t i [x], s i [y]) and encodes the words (w 1 , . . . , w n ), (v 1 , . . . , v n ) generated by a PCP over letters g, h. That means words are represented by nestings of monadic functions. The PCP has a solution iff a ground atom R(g(t), g(t)) or R(h(t), h(t)) is a consequence of the above clause set. This corresponds to testing whether one of the clauses R(g(x), g(x)) or R(h(x), h(x)) has a false instance with respect to the implicit model of the saturated PCP clause set.

Reasoning with respect to a (partial) model assumption has advantages. The superposition completeness proof shows that an inference with a clause that is false in the current partial model is not redundant [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF]. This has meanwhile also been shown for the CDCL [START_REF] Weidenbach | Automated reasoning building blocks[END_REF] and the NRCL [START_REF] Alagi | NRCL -A model building approach to the Bernays-Schönfinkel fragment[END_REF] calculus. The non-redundant inference property might also hold for other calculi of classes (1) and [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF]. It requires exhaustive model generation and eager conflict detection.

Our first contribution is showing that the model representation used in [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF], monadic shallow linear Horn clauses (MSLH) has the finite model property, Section 3. This means that if a finite MSLH clause set has a model, it also has a finite model. Hence, MSLH clause sets cannot be used directly to represent models of clause sets with inherently infinite models. A further consequence is that any calculus in class [START_REF] Alagi | NRCL -A model building approach to the Bernays-Schönfinkel fragment[END_REF], where the model representation can be represented by an MSLH clause set, cannot terminate on satisfiable clause sets with inherently infinite models. A more detailed discussion of this aspect is contained in Section 4.

The fact that MSLH clause sets have the finite model property does not mean that the approximation refinement (AR) calculus presented in [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF] cannot be used for finding infinite models of clause sets with inherently infinite models. The reason is that the MSLH model representation in [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF] does not directly relate to a model of the original clause set, but via an approximation. For the approximation it is shown in a constructive way that it preserves satisfiability. This is done modulo the minimal Herbrand model of a saturated MSLH clause set. Such Herbrand models become infinite as soon as there are non-constant function symbols. So the question is whether AR can actually terminate on clause sets with inherently infinite models. In Section 5, we show that this is the case for certain classes of such clause sets relying on reflexivity of a binary (equivalence) relation. The technique we propose is an additional approximation called reflexive relation splitting. A similar relationship between a clause set and its approximation was already observed in [START_REF] Peltier | Constructing infinite models represented by tree automata[END_REF] where an approximation of a first-order clause set into a class of tree automata is used in order to find finite and infinite models.

Our results concerning the MSLH fragment and the reflexive relation splitting modulo the AR calculus can be demonstrated by the following example. Consider the following three clauses defining a reflexive binary relation R (see [START_REF] Caferra | Automated Model Building[END_REF], page 55 for further discussion of this example).

{R(x, x), R(g(x), g(y)) → R(x, y), ¬R(g(x), c)} This set has only infinite models. No resolution inference between R(x, x) and ¬R(g(x), c) is possible. Following the AR approach [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF], the MSLH clause set

{T (f R (x, y)), T (f R (g(x), g(y))) → T (f R (x, y)), ¬T (f R (g(x), c
))} is generated. We write unit clauses as single literals, and non-unit clauses as implications. The relation R is translated into a binary function f R over a monadic predicate T . The approximation is the replacement of R(x, x) by T (f R (x, y)), where now the connection between the non-linear occurrences of x is lost. As a consequence, a refutation containing a resolution step between T (f R (x, y)) and ¬T (f R (g(x), c)) with substitution {x → g(v), y → c} is possible, which cannot be lifted to the original clause set because g(v) and c are not unifiable. The refinement then excludes this particular instance by generating R(g(x), g(x)), however, after approximating this clause, the empty clause can be derived again. This time the derivation also uses the second clause, where the substitution instance of the refutation contains one further nesting of g. The approximation refinement approach does not terminate on this example.

If in the approximation the inference between T (f R (x, x)) and ¬T (f R (g(x), c)) can be blocked, saturation will terminate without finding a contradiction. As said, in the original clause set this inference is not possible, because of the nonlinear occurrence of x. Now the idea is to split the relation R into its reflexive and irreflexive part, denoted by the two predicates R ref and R irr . The original clause set is satisfiable if and only if the following clause set is satisfiable {R ref (x, x), R irr (g(x), g(y)) → R irr (x, y), ¬R irr (g(x), c)}, details are explained in Section 5. After approximation it becomes

{T (f R ref (x, y)) * , T (f Rirr (g(x), g(y))) + → T (f Rirr (x, y)), ¬T (f Rirr (g(x), c)) * } ( †)
where * highlights maximal and + selected literals of the ordered resolution calculus used to decide MSLH clauses [START_REF] Teucke | First-order logic theorem proving and model building via approximation and instantiation[END_REF][START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF]. There are no possible inferences generating further clauses, i.e. the set is already saturated.

The infinite minimal Herbrand model is

I = {T (f R ref (g i (c), g j (c))) | i, j ≥ 0}
which is also a model for the clause set before approximation [START_REF] Teucke | First-order logic theorem proving and model building via approximation and instantiation[END_REF][START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF] by simply undoing the shift of R irr , R ref to the function level: I = {R ref (g i (c), g j (c))) | i, j ≥ 0}. Nestings of functions in the Herbrand model representing relations, e.g., f R ref , can be prevented by adding further MSLH clauses. We omit these here for simplicity. This model can then be translated, see the proof of Lemma 9, into the Herbrand model I = {R(g i (c), g i (c))) | i ≥ 0} of the original clause set.

In Section 3, we prove a finite model property for saturated, satisfiable MSLH clause sets. For the example, see ( †), the thus constructed model has the domain A := {a c , a (1) , a (2) , a (3) , b (1) , b (2) , b (3) }. The predicate T is interpreted with the set {b (1) , b (2) , b (3) }. For the constant c we use the distinguished element a c . The interpretation of the function f R ref is given in the following function table :  a c , a c -→ b (1) a (i) , a (i) -→ b (j) for every i and some j = i b (i) , b (i) -→ b (j) for every i and some j = i c, d -→ a (j) for any c, d ∈ A with c = d and some j chosen such that for any i, if c or d is equal to a (i) or b (i) , then j = i For the function f Rirr we get a similar function table in which every pair c, d is mapped to some a (j) , where j is chosen such that c, d = a (j) . Finally, the interpretation of the function g is given by g(a c ) = a (1) , g(a (i) ) = a (j) and g(b (i) ) = a (j) for every i and some j = i.

The paper is now organized as follows: after fixing some notions and notations, Section 2, the finite model property of MSLH clause sets is shown in Section 3. Consequences of this result for other model representation formalisms are discussed in Section 4. In Section 5 reflexive relation splitting is introduced and its application to AR investigated. The present paper ends with a discussion on the obtained results and future research directions, Section 6. Due to space limitations, not all proof details could be included. The interested reader will find the full details in the extended preprint [START_REF] Teucke | On the expressivity and applicability of model representation formalisms[END_REF].

Preliminaries

We consider a standard first-order language without equality where letters v, w, x, y, z denote variables, f, g, h functions, a, b, c constants, s, t terms, and Greek letters σ, τ, ρ are used for substitutions. S, P, Q, R denote predicates, A, B atoms, E, K, L literals, C, D clauses, N clause sets and V sets of variables. The notation [¬]A denotes A or its negation. The signature Σ = (F, P) consists of two disjoint, non-empty, in general infinite sets of function and predicate symbols F and P, respectively. The set of all terms over the variables in V is T (F, V). If there are no variables, then terms, literals and clauses are called ground, respectively. A substitution σ is denoted by pairs {x → t}. A substitution σ is a grounding substitution for a term, atom, literal, clause if the application of σ yields a ground term, ground atom, ground literal, ground clause, respectively.

The set of free variables of an atom A (term t, literal L, clause C) is denoted by vars(A) (vars(t), vars(L), vars(C)). A predicate with exactly one argument is called monadic. A term is complex if it is not a variable and shallow if it is a constant, a variable, or of the form f (x 1 , . . . , x n ). A term, atom is called linear if there are no duplicate variable occurrences.

A clause is a multiset of literals which we write as an implication Γ → ∆ where the atoms in the multiset ∆ (the succedent) denote the positive literals and the atoms in the multiset Γ (the antecedent) the negative literals. Alternatively, we write a clause also as a disjunction of its literals. We write for the empty clause. We abbreviate disjoint set union with sequencing, for example, we write

Γ, Γ → ∆, L instead of Γ ∪ Γ → ∆ ∪ {L}. A clause Γ → ∆ is called an MSLH clause, if (i)
∆ contains at most one atom, i.e., the clause is Horn, (ii) all occurring predicates are monadic, (iii) the argument of any monadic atom in ∆ is shallow and linear. The first-order fragment consisting of finite MSLH clause sets we call MSLH.

An atom ordering ≺ is an irreflexive, well-founded, total ordering on ground atoms. It is lifted to literals by defining A ≺ ¬A ≺ B for any atoms A, B with A ≺ B. It is lifted to clauses by its multiset extension. The ordering is lifted from the ground level through ground instantiation: for two different atoms A, B containing variables, A ≺ B if Aσ ≺ Bσ for all grounding substitutions σ and the atoms are incomparable otherwise. A literal L is maximal

(strictly maximal ) in a clause C ∨ L if there is no literal K ∈ C with L ≺ K (L K).
The clause ordering is compatible with the atom ordering; if the maximal atom in C is greater than the maximal atom in D then D ≺ C. We use ≺ simultaneously to denote an atom ordering and its multiset, literal, and clause extensions. For a ground clause set N and clause C, the set

N ≺C = {D ∈ N | D ≺ C} denotes the clauses of N smaller than C.
As usual, we interpret atoms, clauses, and clause sets with respect to structures A, also called interpretations, consisting of a nonempty universe A and interpretations c A , f A , and P A of all occurring constants, functions, and predicates. We often use a special kind of interpretations, called Herbrand interpretations, whose universe is the set of all ground terms. A Herbrand interpretation I is represented by a -possibly infinite -set of ground atoms. A ground atom A is true in I if A ∈ I and false, otherwise. I is said to satisfy a ground clause

C = Γ → ∆, denoted by I C, if ∆ ∩ I = ∅ or Γ ⊆ I. A non-ground clause C is satisfied by I if I Cσ for every grounding substitution σ. An interpretation I is called a model of N , I N , if I C for every C ∈ N . A Herbrand model I of N is considered minimal (with respect to set inclusion) if there is no model I with I ⊂ I and I N . A set of clauses N is satisfiable,
if there exists a model that satisfies N . Otherwise, the set is unsatisfiable.

The superpositon calculus [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] restricted to first-order logic without equality results in the ordered resolution calculus together with the superposition redundancy criterion and partial model operator, see below. For ordered resolution, a selection function is assumed that may select negative literals in clauses. Then (C ∨ D)σ is an ordered resolution inference between a clause C ∨ A and a clause D ∨ ¬B, if (i) σ is the mgu between A and B, (ii) Aσ is strictly maximal in (C ∨ A)σ and nothing is selected in C ∨ A, (iii) ¬Bσ is maximal in (D ∨ ¬B)σ or selected. The clause (C ∨ A)σ is an ordered factoring inference on a clause

C ∨ A ∨ A , if (i) σ is the mgu between A and A , (ii) Aσ is maximal in (C ∨ A)σ and nothing is selected in C ∨ A ∨ A . Selection is stable under instantiation, i.e., if ¬A is selected in ¬A ∨ C it is also selected in (¬A ∨ C)σ,
N C := D≺C δ D δ D :=        {P (t 1 , . . . , t n )} if D = D ∨ P (t 1 , . . . , t n ), P (t 1 , . . . , t n ) strictly maxi- mal in D,

MSLH Model Properties

By definition, Herbrand models for MSLH clause sets with non-constant function symbols have an infinite domain. In what follows we show how to construct non-Herbrand models with finite domains for satisfiable finite MSLH clause sets. The constructed model is a finite representation of the minimal Herbrand model.

Consider a satisfiable finite MSLH clause set N . It is known that N can be finitely saturated using superposition (ordered resolution) with an appropriate ordering and selection strategy such that the following property holds for the obtained saturated clause set N * [START_REF] Weidenbach | Towards an automatic analysis of security protocols in first-order logic[END_REF]. Every clause C in N * that is productive in the sense of the superposition model operator has the form C = P 1 (x 1 ), . . . , P n (x n ) → S(f (y 1 , . . . , y m )) where {x 1 , . . . , x n } ⊆ {y 1 , . . . , y m }, f (y 1 , . . . , y m ) is linear, and S(f (y 1 , . . . , y m )) is strictly maximal in C. Such a saturation can, e.g., be obtained by choosing for ≺ a Knuth-Bendix-Ordering (KBO) with weight one for all function symbols, variables, and a selection strategy that selects a negative literal P i (t i ) in any clause P 1 (t 1 ), . . . , P n (t n ) → S(f (y 1 , . . . , y m )) if t i is not a variable, if t i is a variable that does not occur in f (y 1 , . . . , y m ), or if t i is a variable in a clause P 1 (x), . . . , P n (x) → S(x) [START_REF] Weidenbach | Towards an automatic analysis of security protocols in first-order logic[END_REF][START_REF] Teucke | Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints[END_REF].

Proposition 1 (Entailed by Lemma 4 from [START_REF] Weidenbach | Towards an automatic analysis of security protocols in first-order logic[END_REF]). Consider a satisfiable finite MSLH clause set N . There is a finite MSLH clause set N * such that N ⊆ N * and N |= N * and there is a (minimal) Herbrand model H |= N * such that for every ground atom A of the form S f (s 1 , . . . , s m ) we have H |= A only if there is some clause C in N * and a variable assignment β with the following properties (notice that for m = 0 f degenerates to a constant symbol):

(a) C has the form P 1 (x 1 ), . . . , P n (x n ) → S f (y 1 , . . . , y m ) where {x 1 , . . . , x n } ⊆ {y 1 , . . . , y m }, the y 1 , . . . , y m are pairwise distinct, and m, n ≥ 0; (b) we have β(y i ) = s i for every i, 1 ≤ i ≤ m; and (c) we have H, β |= P j (x j ) for every j, 1 ≤ j ≤ n.

Since N * is satisfiable and all its clauses are Horn, it possesses a unique minimal Herbrand model H (cf. [START_REF] Ebbinghaus | Mathematical Logic[END_REF], Chapter XI, Theorem 3.8). The property described in Proposition 1 provides the key to construct a finite model for N and N * from H. The following example is intended to illustrate the ideas underlying the construction in a simplified form.

Example 2. Consider the following set of MSLH clauses with constants a and b:

N := {P (a), Q(b), ¬P (z) ∨ ¬Q(z) ∨ ¬R(z), ¬P (u) ∨ ¬P (u ) ∨ P (f (u, u )), ¬Q(v) ∨ ¬Q(v ) ∨ Q(f (v, v )), ¬P (x) ∨ R(f (x, y)), ¬P (y) ∨ R(f (x, y)), ¬Q(x) ∨ R(f (x, y)), ¬Q(y) ∨ R(f (x, y))} .
The set N is satisfied by the minimal Herbrand interpretation H with P H := a, f (a, a), f a, f (a, a) , f f (a, a), a , f f (a, a), f (a, a) , . . . ,

Q H := b, f (b, b), f b, f (b, b) , f f (b, b), b , f f (b, b), f (b, b) , . . . , R H := f (s, t) s ∈ P H or t ∈ Q H .
The interpretation H, together with N * := N , satisfies the conditions of Proposition 1: for every term f (s, t) that belongs to R H we have that one of the clauses ¬P

(x) ∨ R(f (x, y)) or ¬P (y) ∨ R(f (x, y)) or ¬Q(x) ∨ R(f (x, y)) or ¬Q(y)∨R(f (x, y)) enforces H |= R(f (s, t)) because of H |= P (s) or H |= P (t) or H |= Q(s) or H |= Q(t), respectively. Similarly, the presence of any term f (. . .) in P H or Q H is enforced by one of the clauses ¬P (u) ∨ ¬P (u ) ∨ P (f (u, u )) or ¬Q(v) ∨ ¬Q(v ) ∨ Q(f (v, v )).
These requirements towards the minimality of H provide us with a certain knowledge about distinct terms f (s, t) and f (s , t ). Suppose the terms s and s are indistinguishable with respect to their membership in P H , Q H , R H . Further suppose that the same holds for the terms t and t . Then, f (s, t) and f (s , t ) are also indistinguishable with respect to their belonging to P H , Q H , and R H , because the arguments s, t and s , t trigger the same productive clauses. A formal statement of this property is given in Lemma 3.

Based on this observation, we use H as a blueprint for a finite model A, which is depicted in Figure 1 Next, we describe formally how to construct a finite model for the given satisfiable and finite MSLH clause set N . Let N * and H be the objects described in Proposition 1. Lemma 3. For every non-constant function symbol f in N of arity m and all tuples s 1 , . . . , s m , t 1 , . . . , t m ∈ H m for which s i ∼ t i holds for every i we have f (s 1 , . . . , s m ) ∼ f (t 1 , . . . , t m ).

P \ R Q \ R P ∩ R Q ∩ R R \ (P ∪ Q)
Proof. By Definition of H, H |= S f (s 1 , . . . , s m ) entails that there is a clause C of the form ¬P 1 (x 1 ) ∨ . . . ∨ ¬P n (x n ) ∨ S f (y 1 , . . . , y m ) in N * and a variable assignment β that satisfy Properties (a) to (c) from Proposition 1. Let γ be a variable assignment for which we have γ(y i ) := t i for every i. Notice that such a γ with γ(y 1 ), . . . , γ(y m ) = t 1 , . . . , t m always exists because the y 1 , . . . , y m are pairwise distinct. Since we assume s i ∼ t i for every i and because of {x 1 , . . . , x n } ⊆ {y 1 , . . . , y m }, Conditions (b) and (c) of Proposition 1 stipulate for every j that β(x j ) ∈ P H j and, hence, we also have γ(x j ) ∈ P H j . Since H is a model of N * , we have H, γ |= C. This together with H, γ |= P j (x j ), for every j, entails H, γ |= S(f (y 1 , . . . , y m )). Put differently, we have H |= S f (t 1 , . . . , t m ) .

Consequently, for every S we observe that H |= S f (s 1 , . . . , s m ) entails H |= S f (t 1 , . . . , t m ) . The converse direction can be shown by a symmetric argument.

We now construct the finite structure A. The universe of A shall be A := Using Lemma 4, it is easy to show that N is satisfied by the finite structure A (see [START_REF] Teucke | On the expressivity and applicability of model representation formalisms[END_REF] for details).

[s] ∼ | s ∈ H ,
Theorem 6 (Finite Model Property for MSLH). Every satisfiable finite MSLH clause set N has a finite model whose domain contains at most 2 p elements, where p is the number of predicates occurring in N .

For a number of fragments enjoying the finite model property, such as the Bernays-Schoenfinkel fragment, the size of minimal models also depends on the number of constants. Ground unit clauses are sufficient to force the growth of models. Ground unit clauses such as the unit clause T (f (a, b, c)) are not admitted in MSLH. But they can be encoded. For the example, the unit clauses S 1 (a), S 2 (b), S 3 (c) together with the clause ¬S 1 (x) ∨ ¬S 2 (y) ∨ ¬S 3 (z) ∨ T (f (x, y, z)) entail the ground unit clause T (f (a, b, c)). Forcing the growth of models via ground unit clauses requires the introduction of additional predicates in MSLH.

Model Representation Formalisms

Many known explicit first-order model representation formalisms are built on sequences of literals, often enhanced with constraints, eventually representing Herbrand models, e.g., [START_REF] Baumgartner | Lemma learning in the model evolution calculus[END_REF][START_REF] Piskac | Deciding effectively propositional logic using DPLL and substitution sets[END_REF][START_REF] Maria | On first-order model-based reasoning[END_REF][START_REF] Alagi | NRCL -A model building approach to the Bernays-Schönfinkel fragment[END_REF][START_REF] Bonacina | Semantically-guided goal-sensitive reasoning: Model representation[END_REF], so called constraints atomic representations (CARMs) [START_REF] Caferra | Automated Model Building[END_REF]. A thorough discussion of all known CARM model representation formalisms is beyond the scope of this paper. We concentrate on three basic building blocks of known model representation formalisms: atoms with disequality constraints [START_REF] Caferra | Automated Model Building[END_REF][START_REF] Comon | Disunification: A survey[END_REF] (ADCs), implicit generalizations [START_REF] Fermüller | Model representation over finite and infinite signatures[END_REF] (IGs) and atoms with membership constraints [START_REF] Caferra | Automated Model Building[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF] (AMCs). They form the basis for a number of concrete model representation formalisms that actually appear in the above mentioned calculi. For this section we consider a fixed, finite signature Σ = (F, P), e.g., the function and predicate symbols occurring in some finite clause set N . The results in this section for all three model representations will be the same: if terms, literals are linear, the models represented by the respective approaches have the finite model property. We will prove this as follows: (i) we provide an effective linear time translation of atoms with disequality constraints to implicit generalizations; (ii) we provide a linear time translation of implicit generalizations to intersections of tree automata [START_REF] Comon | Tree automata techniques and applications[END_REF] or complements thereof; (iii) we represent an atom with membership constraints by a tree automaton. Then, because tree automata are closed under intersection and complement, potentially causing an exponential blow up in size [START_REF] Comon | Tree automata techniques and applications[END_REF], the atoms generated by ADCs and IGs can also be represented by the accepted language of a single tree automaton. The accepted language of a tree automaton can be represented by a finite MSLH clause set, e.g., see [START_REF] Jacquemard | Unification in extensions of shallow equational theories[END_REF]. Thus, by Theorem 6, linear ADCs, linear IGs, and linear AMCs have all the finite model property, i.e., they cannot represent models for clause sets with inherently infinite models.

A linear ADC [START_REF] Caferra | Automated Model Building[END_REF][START_REF] Comon | Disunification: A survey[END_REF] has the form (A :

x 1 = t 1 , . . . , x n = t n )
where the x i are all different and occur in A, the x i do not occur in any t j , the variables of the t j do not occur in A and A as well as all t j are linear. The ground atoms generated by such an ADC are all ground atoms Aσ such that there is no δ with x i σ = t i δ for some i. A linear IG [START_REF] Fermüller | Model representation over finite and infinite signatures[END_REF] is an expression A/{B 1 , . . . , B n } where A and the B i are linear atoms. Every ground instance of A that is not an instance of any B i is generated by the IG A/{B 1 , . . . , B n }. The ground atoms generated by an ADC are exactly the ground atoms generated by the respective linear IG A/{A{x 1 → t 1 }, . . . , A{x n → t n }}.

A tree automaton [START_REF] Brainerd | The minimalization of tree automata[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF] consists of a finite set Q of states, a finite set O of operators, a subset of accepting states Q A ⊆ Q, and a finite set of rules f (q 1 . . . , q n ) → q where q, q i ∈ Q, f ∈ O. The accepted language of a tree automaton is inductively defined by f (t 1 , . . . , t n ) ∈ q A if there is a rule f (q 1 . . . , q n ) → q and t i ∈ q A i for all i. The overall accepted language is then {q

A | q ∈ Q A }.
For example, the ground instances of the linear atom R(x, g(a, y)) over signature Σ = ({g, a, b}, {R}) is the accepted language of the tree automaton O = {R, g, a, b} with rules a → q 1 , b → q 1 , g(q 1 , q 1 ) → q 1 , hence state q 1 accepts all ground terms, a → q 2 , g(q 2 , q 1 ) → q 3 , and R(q 1 , q 3 ) → q 4 where q 4 is the only accepting state recognizing all ground instances of R(x, g(a, y)).

If ta is a function mapping linear atoms to a tree automata accepting the respective ground instances, then the ground atoms generated by an IG A/{B 1 , . . . , B n } are accepted by the tree automaton ta(A) ∩ ¬ ta(B 1 ) ∩ . . . ∩ ¬ ta(B n ). Recall that tree automata are closed under intersection (∩) and complement (¬), however the above tree automaton may be exponentially larger in size compared to the size of ta(A) and the ta(B i ).

A linear atom with membership constraint A : x ∈ S is the pair of a linear atom A and a constraint x ∈ S where x occurs in A and S is represented by a tree automaton. It generates all ground instances Aσ where xσ is accepted by the tree automaton representing S. There is a function ta(A : x ∈ S) that computes in linear time a tree automaton accepting exactly the generated ground instances of A : x ∈ S. Basically, the state(s) representing the instances of x in A in ta(A) have to be replaced by the accepting states of the tree automaton representing S.

Finally, tree automata can be straight forwardly represented via MSLH clause sets. For example, the tree automaton representing the ground instances of R(x, g(a, y)) shown before, can be translated into the MSLH clause set → Q 1 (a);

→ Q 1 (b); Q 1 (x), Q 1 (y) → Q 1 (g(x, y)); → Q 2 (a); Q 2 (x), Q 1 (y) → Q 3 (g(x, y)); and Q 1 (x), Q 3 (y) → Q f (f R (x, y))
. This, together with Theorem 6, eventually proves the following theorem. Theorem 7. Linear disequality constraints (ADCs), linear implicit generalizations (IGs) and linear atoms with membership constraints (AMCs) have the finite model property.

This result can be easily generalized to any "Boolean combination" of linear ADCs, IGs, and AMCs, because tree automata are closed under Boolean operations. Our restriction on linearity does not imply that non-linear ADCs, IGs, and AMCs do not have the finite model property. This is an open problem. For example, the non-linear IG R(x, x)/{R(g(x), g(x))} over signature Σ = ({g, h, a}, {R}) generates the infinite Herbrand model {R(a, a)} ∪ {R(h(x), h(x))σ | σ grounding}. However, it also has a finite model over the domain A := {a, b} of two elements where a is interpreted by a, g maps constantly to b, h maps constantly to a, and R is the relation {(a, a)}.

Non-linear MSH clause sets do not have the finite model property, because they are as expressive as full first-order logic.

Model Finding by Approximation Refinement

The AR calculus as it is used here works as follows [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF]. Starting from a clause set N it is approximated into a MSLH clause set N by the following steps: (i) all non monadic relation literals are turned into function terms below of a new monadic predicate T , (ii) all non-linear variable occurrences in positive literals are linearized, (iii) all nested function terms in positive literals are abstracted through the introduction of further monadic predicates, (iv) non Horn clauses are split into Horn clauses after removing variable dependencies between positive literals. Then if N is satisfiable, so is N . If N is unsatisfiable, the AR calculus tries to lift the proof to N . This may fail, in particular, because of the variable linearizations. In this case the respective clauses are instantiated and again approximated in order to get rid of the particular proof in N and the AR calculus continues. If the proofs out of N are generated in a fair way, the AR calculus is complete [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF]. The Horn splitting can be omitted but then a decision procedure for MSL clause sets is needed [START_REF] Teucke | Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints[END_REF].

The approximation refinement approach [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF] cannot show satisfiability of the simple clause set with the two unit clauses R(x, x), ¬R(y, g(y)). The approximated clause set consisting of the three clauses T (f R (x, y)), ¬S(z) ∨ ¬T (f R (y, z)), S(g(y)) immediately yields a refutation. The problem is that R(x, x) cannot be refined in such a way that all instances of the conflict clause ¬R(y, g(y)) are excluded. The refinement loop instead ends up enumerating all R(g i (x), g i (x)) but R(g i+1 (y), g i+2 (y)) will always remain as a conflict clause.

The non-termination can be resolved, if the resolution inference in the abstracted clause set can be blocked. Our suggestion in case of reflexive relations is reflexive relation splitting, i.e., we split a reflexive relation into its reflexive part R ref and irreflexive part R irr . For the example, this yields R ref (x, x), ¬R irr (y, g(y)) and after approximation T (f R ref (x, y)), ¬S(z) ∨ ¬T (f Rirr (y, z)), S(g(y)). Now the approximation is saturated. The operation preserves satisfiability because the two R literals could not be resolved anyway.

In general, for each predicate R with a reflexivity axiom, all occurrences of atoms R(s, t) are replaced with R ref (s, t) and/or R irr (s, t). If s and t are not unifiable, R(s, t) is replaced with R irr (s, t). If there is an mgu σ of s and t, R(s, t) is replaced with both R ref (sσ, tσ) and R irr (s, t). More precisely, any clause

C ∨[¬]R(s, t) is replaced by two clauses: C ∨[¬]R irr (s, t) and Cσ ∨[¬]R ref (sσ, tσ).
The process is repeated until all atom occurrences with R have been replaced. In the final result, any clause that contains an atom of the form R irr (s, s) can be deleted.

More formally, the following transition system replaces a reflexive R by the two new predicates. Notice that the above lemma holds independently of the fact whether there is a reflexivity clause in N or not. Such a clause would, of course, also be transformed by ⇒ RRS .

Irreflexive N {[¬]R(s, t) ∨ C} ⇒ RRS N {[¬]R irr (s, t) ∨ C}
Let us take a look at an example that is a little bit more involved. Consider an equivalence relation R with the respective axiom clauses.

→ R(x, x) R(x, y) → R(y, x) R(x, y), R(y, z) → R(x, z) Applying ⇒ RRS exhaustively results in the clause set → R ref (x, x) R irr (x, y) → R irr (y, x) R ref (x, x) → R ref (x, x) R irr (x, y), R irr (y, z) → R irr (x, z) R irr (x, y), R irr (y, x) → R ref (x, x) R irr (x, y), R ref (y, y) → R irr (x, y) R ref (x, x), R irr (x, z) → R irr (x, z) R ref (x, x), R ref (x, x) → R ref (x, x).
After removing redundant clauses, we are conveniently left with just

→ R ref (x, x) R irr (x, y) → R irr (y, x) R irr (x, y), R irr (y, z) → R irr (x, z)
which are no longer trivialized by the linear approximation T (f R (x, y)) of the reflexivity axiom generated by the AR calculus. See also the example in the introduction, Section 1, for another application of reflexive relation splitting.

The rule Reflexive replaces a clause by two clauses and can, therefore, cause an exponential blow up in the number of generated clauses. However, this is only the case for a clause with several occurrences R(s i , t i ) such that the respective term pairs are all simultaneously unifiable. This situation can be detected and then reflexive relation splitting may not be efficiently applicable. However, the above example on the equivalence relation R shows that in the case of variable chains as they occur in the transitivity axiom, all of the eventually generated clauses become redundant, except one: R irr (x, y), R irr (y, z) → R irr (x, z). We have integrated reflexive relation splitting into Spass-AR [START_REF] Teucke | Ordered resolution with straight dismatching constraints[END_REF][START_REF] Teucke | An Approximation and Refinement Approach to First-Order Automated Reasoning[END_REF] and have run it on the overall TPTP [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0[END_REF]. There is no example in TPTP v.7.2.0 showing the exponential blow up and the set of problems solved by Spass-AR with reflexive relation splitting is strictly larger than without.

Nevertheless, reflexive relation splitting is, of course, not sufficient to transform all problems with inherently infinite models based on a (ir)reflexive relation into clause sets that can eventually be decided by AR via MSLH clause sets. Consider a strict partial ordering without endpoints: R(x, x) → → R(x, g(x)) R(x, y), R(y, z) → R(x, z).

Reflexive relation splitting yields R ref (x, x) → → R irr (x, g(x)) R irr (x, y), R irr (y, z) → R irr (x, z) R irr (x, y), R irr (y, x) → R ref (x, x) but after approximation, the abstraction refinement does not terminate on the example. The reason is the approximation of the clause R irr (x, g(x)) into the two clauses S(g(x)) and S(y) → T (f Rirr (x, y)) where the property is lost that in any ground instance of R irr (x, g(x)) the first argument has one occurrence of g less than the second. This was resolved in [START_REF] Peltier | Constructing infinite models represented by tree automata[END_REF] by the use of tuple tree automata.

Discussion

We have shown that the MSLH clause fragment has the finite model property and can therefore not represent models of clause sets with inherently infinite models. This applies to the model representation building blocks atoms with disequality constraints, implicit generalizations, and atoms with membership constraints as well, if atoms and terms are linear. For non-linear terms, our finite model property proof breaks, and, in fact, the example from the introduction shows already that non-linear atoms can represent models for clause sets with inherently infinite models.

Unsatisfiability of monadic shallow Horn clause sets is undecidable. One occurrence of a clause Γ → S(f (x, x)) suffices to this end. This can be seen by a respective monadic reformulation of the PCP encoding from the introduction. On the other hand, models represented by ground instances of finite sets of (linear or non-linear) atoms are also restricted in expressivity, because they cannot express any recursive structure. For example, MSLH clause sets and extensions thereof have been successfully used for the analysis of security protocols [START_REF] Weidenbach | Towards an automatic analysis of security protocols in first-order logic[END_REF][START_REF] Blanchet | Automatic proof of strong secrecy for security protocols[END_REF] where (counter-) models cannot be expressed by ground instances of finite sets of atoms. In summary, and not surprisingly, there is currently no unique superior model representation formalism.

If models are eventually constructed through the reversal of an approximation, the used representation may have the finite model property and can still show satisfiability of clause sets with inherently infinite models. We obtained this result via reflexive relation splitting. This insight is already a consequence of [START_REF] Peltier | Constructing infinite models represented by tree automata[END_REF]. There, an approximation into a theory of tuple tree automata is described and it is even complete with respect to models generated out of these automata. We can currently not provide such a completeness result although this would be highly desirable. On the other hand, our techniques are embedded into a refutationally complete procedure, whereas the approach in [START_REF] Peltier | Constructing infinite models represented by tree automata[END_REF] can only show satisfiability.

  for any substitution σ. A clause C is redundant with respect to a clause set N , if for all ground instances Cσ there are ground instancesD 1 σ 1 , . . . , D n σ n , {D 1 , . . . , D n } ⊆ N , D i σ i ≺ Cσ for all i, such that D 1 σ 1 , . . . , D n σ n |= Cσ, i.e., Cσ is implied by smaller ground instances from clauses in N . A clause set N is called saturated if all clauses generated by ordered resolution or ordered factoring from clauses in N are either redundant or contained in N . Given a ground clause set N and an ordering ≺ we can construct a (partial) Herbrand model N I for N by the superposition (partial) model operator inductively as follows:

  no literal selected in D and N D |= D ∅ otherwise N I := C∈N δ C Clauses C with δ C = ∅ are called productive. For a non-ground clause set N we define N I := ({Cσ | C ∈ N, σ grounding for C}) I . The main completeness result of superposition is: for a clause set N let N * be its (possibly infinite) saturation, then either ∈ N * and N is unsatisfiable, or N * I |= N [2]. Basically, inferences of the superposition calculus are restricted to maximal, or selected negative literals. If all non-redundant inferences of a clause set are performed, i.e., the clause set is saturated, then the superposition model operator generates an overall model for the clause set.

  . The domain of A shall be A := {a, b, c, d, e}, and we set a A := a and b A := b. The predicate symbols are interpreted by P A := {a, c}, Q A := {b, d}, R A := {c, d, e}. Moreover, we define f A (a, a) := c f A (a, c) := c f A (c, a) := c f A (c, c) := c f A (b, b) := d f A (b, d) := d f A (d, b) := d f A (d, d) := d. For all other inputs, f A shall yield e as output. Every domain element in A represents one equivalence class of the terms in H's Herbrand domain with respect to membership in the sets P H , Q H , and R H . The domain element a represents the class [a] := {a} of terms that belong to P H and to no other set. Similarly, b represents [b] := {b} of terms that belong to Q H and to no other set. The element c represents the class of all terms belonging to P H ∩ R H , i.e. to the class containing f (a, a), f (a, f (a, a)) and so on. The class of terms belonging to Q H ∩ R H is represented by d. Finally, e corresponds to the class of all terms that are member of R H but of none of the other predicates, e.g. f (a, b), f (a, f (b, a)).

  a: a terms yielding b: b terms yielding c: f (a, a), f (f (a, a), a), f (a, f (a, a)), . . . terms yielding d: f (b, b), f (b, f (b, b)), f (f (b, b), b), . . . terms yielding e: f (a, b), f (b, a), f (a, f (a, b)), . . .

Fig. 1 .

 1 Fig. 1. Illustration of the model A of N from Example 2.

  above claim and still ensure that I |= N . It then follows that I |= N , I |= N 1 , . . . , I |= rrs(N ). Symmetrically, let I be a Herbrand model of rrs(N ). Since rrs(N ) does not contain the predicate R, we can reshape I so that the above claim is applicable and I is still a model of rrs(N ). Then, we get I |= rrs(N ), . . . , I |= N .

  Let Π denote the set of all predicates occurring in N , and recall that Π contains only unary predicate symbols. Let ∼ be the equivalence relation on H such that s ∼ t holds if and only if we have for every P ∈ Π that H |= P (s) if and only if H |= P (t).

Then, we have H |= N * and H |= N . Let H be the domain of H, i.e. H is the set of all ground terms over the vocabulary underlying N . We aim at constructing a finite model A |= N starting from H.

  where [s] ∼ denotes the (unique) equivalence class with respect to ∼ which contains the term s. For every function symbol f (including constants) we setf A [s 1 ] ∼ , . . . , [s m ] ∼ := f (s 1 , . . . ,s m ) ∼ for all ground terms s 1 , . . . , s m . Finally, we define each predicate P under A by P A := [s] ∼ | H |= P (s) . Let γ be any variable assignment over A's domain. Let β be some variable assignment over H's domain defined such that for every x we have γ(x) = β(x) ∼ . By definition of H, such a β must exist. Then, for every term t in N and every predicate P we have A, γ |= P (t) if and only if H, β |= P (t). (Sketch). We proceed by case distinction regarding the structure of the term t. If t = x is a variable, then we have A, γ |= P (x) if and only if γ(x) = β(x) ∼ ∈ P A if and only if β(x) ∈ P H if and only if H, β |= P (x). If t = c is a constant, then we have A, γ |= P (c) if and only if c A = [c] ∼ ∈ P A if and only if c ∈ P H if and only if H, β |= P (c). Suppose t = f (s 1 , . . . , s m ) for some function f of arity m ≥ 1 and terms s 1 , . . . , s m . Let t 1 , . . . , t m be ground terms such that A(γ)(s i ) = [t i ] ∼ . Such terms exist by definition of H. Then, A, γ |= P f (s 1 , . . . , s m ) if and onlyif f A [t 1 ] ∼ , . . . , [t m ] ∼ = f (t 1 , . . . , t m ) ∼ ∈ P A ifand only if H |= P f (t 1 , . . . , t m ) . A straightforward induction on the structure of the terms s i yields t i ∼ H(β)(s i ) for every i (see[START_REF] Teucke | On the expressivity and applicability of model representation formalisms[END_REF] for details), where H(β)(s i ) denotes the value of the term s i under H and β. Then, byLemma 3, we have H |= P f (t 1 , . . . , t m ) if and only if H |= P f H(β)(s 1 ), . . . , H(β)(s m ) if and only if H, β |= P f (s 1 , . . . , s m ) . For the special case of ground terms, there is a simpler form of Lemma 4: Corollary 5. For every ground term t and every predicate symbol P we have A |= P (t) if and only if H |= P (t).

	Lemma 4. Proof

Acknowledgments: This work was funded by DFG grant 389792660 as part of TRR 248. We thank our reviewers for their valuable comments.

Proof (Sketch). Termination is easy to prove. Each application of the rules Irreflexive or Reflexive reduces the multiset of the numbers of R-occurrences in all clauses, and no new occurrences of R are ever introduced when Delete is applied. Each application of the rule Delete reduces the number of occurrences of R irr . Combining these two properties into a well-founded multi-set-based ordering completes the proof of termination. For local confluence, the non-obvious case is a clause [¬]R(s, t) ∨ [¬]R(s , t ) ∨ C where R(s, t) and R(s , t ) share variables, and without loss of generality, s and t are unifiable by the mgu σ. Applying first the reflexive transformation to the first literal yields the two clauses

Now the interesting case is where s , t are unifiable but s σ and t σ are not. Then we get with the mgu τ of s , t :

. This is also exactly the result we get when starting with a translation of [¬]R(s , t ): if s σ, t σ are not unifiable, then sτ, tτ are not unifiable as well. For otherwise, sτ τ , tτ τ for unifier τ is an instance of sσ, tσ, so s σ, t σ must be unifiable as well, a contradiction to the above assumption. All other cases are similar to this case. By Newman's Lemma, termination plus local confluence implies confluence.

Given any finite clause set N , we write rrs(N ) to address the normal form of N after exhaustively applying ⇒ RRS . Notice that any clause D ∈ rrs(N ) is an instance of a clause in N with respect to the renaming of R ref , R irr with R. Moreover, we use rrs(C) as shorthand for rrs({C}) for any clause C. Lemma 9 (Reflexive Relation Splitting). Let N be a finite clause set that does not contain the predicates R ref and R irr . N is satisfiable if and only if rrs(N ) is satisfiable.

Proof (Sketch). Consider the derivation N ⇒ RRS N 1 ⇒ RRS . . . ⇒ RRS rrs(N ) where we assume that the rule Delete is applied with priority whenever it is applicable. By confluence of ⇒ RRS , this is not a restriction.

We use an auxiliary result that is not hard to prove (see [START_REF] Teucke | On the expressivity and applicability of model representation formalisms[END_REF] for details):


Olivier Faury

Arnaud Serry

Ronan Kerbiriou

Yann Alix

Analysis of Murmansk as a gateway for the Arctic production

Keywords: Port System, Tanker, Bulk, Murmansk, Hub, Arctic

The Western Russian Arctic seabed, due to the huge quantity of oil and gas, is subject to numerous investment and drill like in the Yamal peninsula with the port of Sabetta. Extreme climate conditions and remoteness impact negatively the cost of transportation of raw materials and so the use of ice or polar class vessels due to the ice.

In order to give to Murmansk, the role of transshipment Hub for oil and gas coming from Arctic fields, investment have been made to update existing infrastructure and implement new one.

However, if we are aware of the origin of the cargo, the destination is more complex to define.

The aim of this article is to analyze, the way Murmansk is integrated in the global maritime network.

To do so, we use the Automatic Identification System (AIS) to visualize the different typology of vessel. Even if Murmansk is originally a port mainly dedicated to coal exportation, the coming investment increased the amount of crude oil handled, hence we decided to focus on tankers, container and dry bulk vessels. In order to stress the impact of NSR development on Murmansk, we looked at its input and output evolution since 2010. This evolution is analysed in comparison with the price of commodities.

In conclusion, the future competitiveness of the Murmansk port complex is discussed, considering other comparable investment forecasted on deep-water greenports like Arkhangelsk as well Kirkenes, both promoted as future strategic gateway to Western Russia, Scandinavia and Eastern Europe markets thanks mainly to efficient projected railways & roads networks.

Introduction

In recent years, the Russian government has invested in port infrastructures and more precisely in Arctic port, a region with numerous oil and gas currently exploited. The part of the project receiving most of the investment and attention, Murmansk is one of the examples that represents the renewed interest for these ports.

Within the Russia toward the north, Murmansk appears as being at its inner center. The recolonization of the north as mentioned by [START_REF] Kinossian | Re-colonising the Arctic: The preparation of spatial planning policy in Murmansk Oblast[END_REF] is the corner stone of the NSR development.

Few things to know about Murmansk is that it is one of the few deep-water ports with an icefree access all year long. Besides, it is connected thanks to a railway to the rest of the Russian railway network. Murmansk is also the largest city in terms of population in the Arctic.

Looking at implemented projects, we could quote the implantation of a free trade zone (Murmansk transport Hub) supposed to handle dry bulk such as coal, liquid bulk and container. Until now, Murmansk is mainly known for, handling coal, being the home port of the northern fleet.

The harsh sailing conditions in the Arctic impose the use of specific vessel able to sail in ice infested waters. However, it may not be relevant to use these ships within warm waters for maneuverability reasons and also because they are smaller than vessels usually used to ship raw materials. Besides, the remoteness of the oil and gas fields increases the cost of transporting crude oil from these fields.

All these parameters posit Murmansk as a potential regional Hub. Yet, if Murmansk is clearly connected to the other Russian ports of the Arctic, the question is which ports located overseas and out of the Arctic Ocean are connected to Murmansk.

The aim of this article is to shed a light on the evolution of Murmansk as a potential hub and to determine the number of dry and liquid bulk calls. The general idea of this article is that because it is complicated to get the amount of cargo transported from the Russian authorities, we will focus on the number of times each type of vessel calls in Murmansk for origin or destination.

The new Russian strategy has been implemented in 2010, so we are going to look at its evolution and impact on Murmansk between 2011 and 2017.

To do so, after a short literature review on this subject, we shall explain the way we extract and manipulate data. The third section deals with the result for dry and liquid bulk. Section four provides prospective approach of the area and the way Murmansk may change. Finally, after a discussion, we propose concluding remarks.

Literature review

The development is grounded on the development of ports for mainly safety and economic purposes [START_REF] Ragner | Northern Sea Route Cargo Flows and Infrastructure -Present state and Future potential[END_REF][START_REF] Kitigawa | The Northern Sea Route -The Shortest Sea Route linking East Asia and Europe[END_REF][START_REF] Gunnarsson | The Future of Arctic Marine Operations and Shipping Logistics[END_REF]. The ice melting and the oil gas reserves in the western part of the Russian shore [START_REF] Grigoriev | Oil and gas: Russian arctic offshore[END_REF], explain the numerous academics and professional analysis of this area. Besides, the Arctic region is highly sensitive to Russian development with a production representing 20% of Russia GDP and 22% of its export [START_REF] Scherbanin | Transport and transport infrastructure in 2030: Some predictive estimates[END_REF]. [START_REF] Monios | Port system evolution-the emergence of second-tier hubs[END_REF] conceptualized the idea of second-tier hub based on three examples. If their explanation relies on the port handling containers, they defined a second-tier as a hybrid managing goods coming from other but with also including cargo coming from its own hinterland. Looking at this definition, it appears that Murmansk seems to fit to this definition. The coal exported comes from its hinterland and the oil and gas have for origin arctic ports situated along the Western Arctic Russian shore.

As explained by Monios et al (2018), a second-tier hub has to manage transshipment and be connected to its hinterland. Regarding the hinterland connection, we could quote [START_REF] Scherbanin | Transport and transport infrastructure in 2030: Some predictive estimates[END_REF] who explained that one of the objectives of the Russian transport strategy is to develop the loading capacity of the railroad to ports such as Murmansk by two. Besides, [START_REF] Scherbanin | Transport and transport infrastructure in 2030: Some predictive estimates[END_REF] presents Murmansk as a hub.

Related to the link with the hinterland, [START_REF] Smirnova | Creation of development zones in the Arctic: methodology and practice[END_REF] pointed the importance of Murmansk Transport Hub, defined it as an "anchor project" and one of the main Artic projects, for the Russian Federation. [START_REF] Pavlenko | Development of Transport and Logistics Infrastructure in Russian Arctic[END_REF] demonstrated the importance of Murmansk within the Russian strategy with a planned capacity of 91 million tons by 2030 far above the 39.2 and 37.5 Million tons of, respectively, Sabetta and Arkhangelsk. [START_REF] Pahl | Arctic Port Development[END_REF] highlighted that Murmansk is the biggest port within the Arctic and also shed a light on its ice-free position. The development of the NSR is dependent on the development of Murmansk. [START_REF] Pahl | Arctic Port Development[END_REF], [START_REF] Bennett | North by Northeast: toward an Asian-Arctic region[END_REF] and [START_REF] Scherbanin | Transport and transport infrastructure in 2030: Some predictive estimates[END_REF] clearly pointed the importance of resources extraction, raw materials and cargo shipping for the NSR. In fact, the raw materials such as oil and gas are the pillar of the Arctic economic development and the building and upgrading of proper infrastructures in order to render safer and more profitable navigation within the Arctic [START_REF] Gunnarsson | The Future of Arctic Marine Operations and Shipping Logistics[END_REF].

In order to manage the extraction of Arctic resources, [START_REF] Gunnarsson | The Future of Arctic Marine Operations and Shipping Logistics[END_REF] considered the development of Arctic ports infrastructures as one of the main elements to take into consideration when dealing with the marine transportation system.

The ice and geographical constraints impose the use of an ice class vessel [START_REF] Fedi | The impact of the Polar Code on risk mitigation in Arctic Waters: a 'Toolbox' for underwriters?[END_REF]. The presence of ice does not facilitate port access on a year basis and limits the number of vessels able to call in these ports. Thus, the use of "shuttle vessel" would be necessary as stated by [START_REF] Gunnarsson | The Future of Arctic Marine Operations and Shipping Logistics[END_REF]. He also explains that the implantation of a HUB in the west and the east boarder of the NSR would be necessary and considered that the location of Murmansk is valuable [START_REF] Gunnarsson | The Future of Arctic Marine Operations and Shipping Logistics[END_REF] Yet as pointed out by [START_REF] Gunnarsson | The Future of Arctic Marine Operations and Shipping Logistics[END_REF], crude oil transshipments also supposed to play a major role within the port activity.

Our analysis focuses on the evolution of Murmansk seaport connection with the rest of the world in function of the typology of vessel between 2011 and 2017. The objective is to demonstrate that Murmansk is clearly a gateway for dry and liquid bulk and that the fishing activity appears as a one of the main levers for growth of the port.

Methodology

This work is based on a database constructed using the IHS maritime database (https://maritime.ihs.com/) and with collected data from AISHub, a data sharing service which provides access to real time ship positions for vessel tracking systems.

The AIS is a tracking system used on ships to provide information on surrounding traffic situation and supplements marine radar as a collision avoidance device. AIS devices are obligatory on all large vessels according to the IMO SOLAS Convention (SOLAS Convention, 2004). AIS presents advantages for maritime transportation actors: improvements in safety, progresses in fleet management and navigation. The data acquired from AIS systems also constitute a new means of information for the maritime community, or the wider public (See Above all, broadcasting AIS data in real-time makes a tangible contribution to the scientific community [START_REF] Serry | Automatic Identification System (AIS) as a Tool to Study Maritime Traffic: the Case of the Baltic Sea, Marine Navigation[END_REF]. This data is first used for work mainly based on security or coastal areas. Furthermore, the literature is fragmented between different approaches and subjects like international maritime law, physics, signal processing, geopolitics and many others. The use of AIS data provides the opportunity to study vessel behaviour due to meteorological circumstances or highly refined vessel movement and improved emissions estimation [START_REF] Perez | Automatic Identification Systems (AIS) Data Use in Marine Vessel Emission Estimation[END_REF]. A potential application of archived AIS data is also to extract trip duration statistics for a population of ships [START_REF] Mitchell | Waterway Performance Monitoring via Automatic Identification System (AIS) Data[END_REF].

AIS data improves a network of stations covering more and more areas, providing new possibilities to the mapping of transport activity. "Thanks to the availability of AIS data, it is possible to identify, quantify and map navigation lanes of vessels" [START_REF] Le Guyader | Exploitation de données AIS (Automatic Identification System) pour la cartographie du transport maritime[END_REF]. The automatic character of transmitting vessel positioning signals and its generalisation provide an opportunity to track and analyse the vessels' itineraries. Once this source of information has been properly checked through matching it with external data with regard to vessels and ports, it opens the way to reasoning on a global scale as well as on the scale of port approaches, in real-time as well as long term.

The method, founded on a spatial analysis within a geographical information system (GIS) combined with a database server, makes it possible to reconstruct each vessel's trajectory in such a way as to identify the navigation lanes then to match the daily traffic in its temporal and quantitative dimensions. It is then possible to analyse the maritime networks.

As AIS data can be free of charge, it may raise preoccupations with a confidentiality [START_REF] Serry | Le Système d'Identification Automatique (AIS) : du Big Data maritime aux potentialités géoéconomiques[END_REF]. Using of AIS signals request a number of methodological and technical issues, some related to the duration of observation which must be long enough to account for seasonal trends, others related to the geographic scope, which must be comprehensive if you want to account for the economic gap between different regions of the globe. All this requires the accumulation of large masses of data. There is also the question of the intrinsic quality of the data transmitted by the AIS signals.

As AIS data is "Big Data", it requires specific techniques for data handling and processing which has limited its use. We create a platform (CIRMAR) to develop capacity and methods for better use of this massive source of maritime data. It has to receive, decode, clean, store and analyse AIS messages. During a first phase, AIS messages are received: each message contains position reports from ships, base stations reports... Second, the messages are decoded, made ready to be checked and messages with errors are ignored. As seen in figure 1, the decoded AIS data are human-readable tables containing several parameters such as the date and time when the signal was issued, the identification of the AIS message, the identification number of the AIS transmitter... We also need to clean the data which will be used in our analysis and to create statistics or maps, for instance, removal of duplicated signals or wrong MMSI signals. The data cleaning is necessary to remove erroneous signals and duplicates. In reality, several problems appear during the treatment. At first, speaking about data treatment, the two major obstacles to produce information for geo-economic issues are the amount of data to process and the quality of data and particularly static data. Even if they are of small size (39 characters for example) the number of AIS messages received, led to the formation of large amounts of data. Regarding data quality, most of the problems relate to information that are manually integrated in the system (port of destination, navigation status, draught of the ship and estimated time of arrival). So, dynamic data (positioning and road) are more reliable than the static ones, therefore, it is interesting to match AIS data with some external databases on ships or on ports (Lévêque, 2016). The next step is to store AIS messages in the database.

In this study, due to the lack of coverage of AISHub in the Arctic area, we mainly used data from IHS Maritime for years 2011 and 2017. As shown in Figure 2, container ships are not calling in Murmansk. So we decided to focus on bulk flows from and to Murmansk.

At least, from a general point of view, as Murmansk is traditionally considered as the beginning of the NSR [START_REF] Selin | Economic development of the Russian Arctic space by upgrading transport and logistics sector[END_REF], and because it is the largest transportation hub in the Russian Arctic, we decided to have a special focus on ship departing from Murmansk.

Results

As highlighted by the Figure 2, the main type of vessel calling in Murmansk are fishing vessels in 2011 and 2017. Fishing vessels, tankers, bulk carrier, general cargo and tug represent representing 80% of calling within Murmansk. Besides, in 2017, the number of calls increased by 34.3 % compared to 2011, reaching 3,758 called. The first results also clearly show that container flows are missing in Murmansk. Even if fishing vessels represent the highest evolution in term of number of calls between 2011 and 2017, we assumed to concentrate on tanker, bulk carrier. We made this choice based on the Murmansk's importance for the development of the Russian economy. One of the main growth levers is the exportation of raw materials coming from the Arctic mines and oil and gas fields. Due to its geographical position, Murmansk is the main gateway.

If the number of calls of bulk and tankers vessels increase between 2011 and 2017, their share within the exportation decrease from 39.6% till 36.7% in 2011 and 2017 respectively. Despite the increase of 271 tankers, general cargo and bulk vessels, the additional 835 fishing vessels decrease the global share of commercial vessels.

Regarding tankers, in 2017, Murmansk is still the first with 1,414 calls but Varandey is the second one due to the existing shuttle tanker for the transshipment of additional crude oil coming from the joint venture with Basneft. The second port is Rotterdam with 98 calls. The next non-Arctic and non-Russia port is Antwerp with 35 calls and Hamburg who was the second port in 2011 comes after with 17 calls. In 2011, most of the flows were concentrated between the North-Range and for some of them on the American shore of the Mexican gulf (Figure 2).

Tankers flows

Figure 3a and 3b demonstrate the position of Murmansk as the main port in term of crude oil management in the Arctic. The Figure 3a and 3b shed a light on the evolution of the connection of Murmansk via the flow of liquid bulk. In 2011, Murmansk main destination is the European Northern range, the rest of the connection being disseminate all around the globe. In 2017, if the Northern range is still present, new point appeared such as in, the Baltic sea, the Bosporus strait. From a Russian perspective, the Arctic Russian ports of Arkhangelsk, Sabetta and Varandey appear. The reason for the emergence of Russia has to be found in the exploitation of oil fields and the implementation of shuttle tankers. In 2017, the situation is quite different and flows were more concentrated compared to 2011 (Table 2a and2b). 1% of ports connected to Murmansk represent 60% of calling. out of these 8 ports are part of the North-range (Rotterdam, Le Havre, Antwerp, Wilhelmshaven), the rest being Russian port such as Arkhangelsk, Vorota Arktiki Oil Terminal, and Varandey for the crude oil and Sabetta for the LNG. The high level of connection of the Russian ports can be explained by the Russian strategy to posit Murmansk as a Gateway for the export of raw materials. The management of crude oil is paramount for the Russian economy. In addition, Murmansk as a deep-water ports and ice free all year long provide the benefits to be close to the zone of production and to be able to manage Very Large Crude Carrier or Aframax with no ice-class. Gulf and the Baltic sea. In 2017, the north-range and the Mexican gulf and the Baltic sea were still highly connected to Murmansk but some new area appears or enhanced their level of connection such as Gibraltar Strait, Aegean Sea, Malacca Strait and the African West-coast.

Prospective 5.1. Energy analysis

Murmansk connect the Russian port of the Russian Arctic shore with the rest of the world by playing the role of gateway for the Arctic production (figure 5). Figure 5 stressed the importance of Murmansk as a regional hub for the Arctic ports mostly dedicated to the exportation of crude oil and LNG as explained above with the figure 3b. Figure 5 also shows the use of shuttle doomed to deliver crude oil extracted and shipped in Varandey. Murmansk in 2017 was also used as a transshipment hub for the LNG produce in Sabetta.

Based on British Petroleum report (2018), most of energy resources comes from oil and gas industry and may represent 60% of the total energy consumed. One explanation is based on the development of India and China. As an example, China aims to increase its consumption of LNG in the coming years. This objective may be one reason explaining the growth of 3% in LNG consumption.

If we consider the current volume of energy consumed worldwide with the forecasted economic growth of the most energy-intensive economies (China, USA, Russia, India, European Union, etc.), the emblematic threshold of 15 000 Mt of equivalent oil could be exceeded before 2030 (SEFACIL Foundation, 2018). That perspective also includes the fact that 2017 has seen a growth of 2.2% of the world total of energy, a best ever since 2013 to be injected into a ten-year growth which stands at 1.7% (BP Energy, 2018). It should also be reminded that China is, for the 17th consecutive year, the country with the highest growth in energy consumption with 3.1% in 2017 making China as the most interesting destination market in the short and medium term. It appears obvious in the light of the projection of the future Chinese energy mix defended by Beijing whose plans to convert the most polluted heavy-industries fueled with dirty coals to ever cleaner energy (natural gas and electricity). A remarkable increase of 15% in its natural gas consumption has already been recorded for the sole year of 2017, which weighs for one third of the net worldwide growth (96 Bcm).

As mentioned, Beijing is currently leading the most ambitious energy conversion ever experienced with millions of private homes which have to be equipped for natural gas. In stake is the purification of the air, especially in the largest cities located in the northwestern part of the country. From a purely geographical and strategic point of view, Chinese LNG Port & industrial infrastructure investments are carried out everywhere on the coastal fringe and not only focused on the northwestern areas. Two important facts to be bear in mind: a twentieth LNG terminal has been confirmed in 2018 whereas the opening of the LNG infrastructure market to the private sector should stimulate healthy competition with public historical actors.

For instance, the ENN Group terminal in Zhoushan, Zheijang province (capacity of 3 Mt per year) is expected to reach 10 Mt with nearly 1.5 billion investments [START_REF] Xin | First privately run LNG port opens[END_REF]. Those perspectives are built on Chinese projected imports of LNG to be continued to grow at an amazing pace. A spectacular increase of 47.3% has been tracked between 2016 and 2017 to reach a total of 39.1 Mt and the first 6 months of 2018 looks as even more promising with another 50% increase in volumes! On the European perspective, still the dominant market destination for Russian natural energy resources, the trend is towards a slowdown in net consumption of petroleum products despite an increase in 2017. Europe "only" accounts for 15% of the world's crude oil consumption. With an increase of 5.5% in 2017 the Russian natural gas looks quite much more attractive for European market, both fed by pipelines and LNG shipped by specialized ships and stored and transformed on industrial complex such as Zeebrugge in Belgium, Montoir in France and various Spanish terminals. Those ports are in fierce competition to impose as Western European port gateway as well as international hub for LNG ship-to-LNG ship transshipment activities.

And a final word to include the fact that the full relevance of an energy strategic prospective depends on the genuineness of relevant data on potential oil and gas reserves in the Arctic areas.

In 2008, the US Geological Survey estimated that "only" 10% of the oil reserves and 29% of the gas reserves could be found in the Arctic which represent 90 billion barrels of oil and 47,261 Bcm of natural gas. These real volumes, how huge they may be, weight about "only" three years of the current world oil consumption and no more than seven years for natural gas [START_REF] Lasserre | La géopolitique de l'Arctique : sous le signe de la coopération[END_REF]. For Russia alone, the largest country of the World, the Arctic territories cover 15% of the total national territory and account nowadays for 20% of the GNP with just over one million inhabitants [START_REF] Zarudnitskiy | National interest of the Russian Federation in the Arctic. Significance of the Arctic for Russia[END_REF]. Noteworthy, according to Zarudnitskiy and Chvarkov "up to 90% of recoverable hydrocarbons of the entire Russian continental shelf are deposited and up to 80% of Russia's explored gas reserves are produced here" [START_REF] Zarudnitskiy | National interest of the Russian Federation in the Arctic. Significance of the Arctic for Russia[END_REF].

Incidentally, the same glitches apply to mining potential, with the endless equation to be found between the ever more complex Arctic exploitation surcharges and remuneration by an increasingly volatile global market. This will not prevent the launching of huge extraction projects and therefore the development of maritime segments from the Russian Arctic. With respect to import inputs, real traffic opportunities are based on the provision of all the "supply stuff" needed for the development and production of future mining sites. Heavy lift for machinery, ro-ro flows for rolling stock, containerized manufactured products: a whole range of Arctic flows will probably continue to grow in the coming years, activating ports' infrastructures nearby mining extraction sites. Consequently, on the exportation output, some new ports intensities will emerge like the ones at the Taimyr-Norislsk zone with the development of specialized infrastructure in Dudinka and Dikson for the massive export of nickel and coal in particular. In a longer-term perspective, Yacoutie's proven reserves of raw materials (energy, of course, but also mineral resources with, for example, interesting high value-added deposits such as diamonds) could support the development of new infrastructure in addition to those already active. However, these perspective in Yacoutie ties to a very different climatic temporality, keeping in mind the complexity of organizing an integrated supply chain including reliable shipping services.

Murmansk positioning

Due to its geographical position, Murmansk has an open access all along the year providing the possibility for non-ice class ships to call. Besides, if the other Russian ports have a limited draft, it is not the case of Murmansk who can handle AFRAmax or even bigger vessels with a result to improve its potential connectivity.

Regarding transshipment, Murmansk attract crude oil flows coming from Novy, Prirazlomnoye platform and the Varandey terminal which represent almost the whole crude oil exported from the Arctic fields and the production of mineral leaving Dudinka.

As part of the numerous projects planned, the MTH and the connection of the Lavna coal terminal financed by SUEK group, via the 46 km railway (Staalesen, 2018a) shall provide 9 million tons of dry bulk dedicated to the exportation by 2019. When complete, the new project capacity shall reach 25 million tons per year reinforcing the link of Murmansk with its hinterland.

The coal terminal is not the only one included within the MTH. Facility for the exportation of 6 million tons is also planned (Staalesen, 2018a).

Yet as specified Monios et al (2018), the position of second-tier hub is not static and can be challenged by other ports and Murmansk is not an exception. The Kola bay port is facing the competition of two other ports, Kirkenes and Arkhangelsk (Figure 6).

Smaller than Murmansk but with the same advantages (ice free all year long and deep-water port) Kirkenes has already managed transshipment of crude oil coming from Varandey oil terminal. Yet, aware of its quite small hinterland, for the moment, compared with Murmansk the Norwegian and Finnish government agreed to connect Kirkenes to the Arctic Corridor Railway (ACR). This r-project provide a railway connection between Kirkenes and Rovaniemi in Finland. This railroad is the first step of a much larger project doomed to connect Rovaniemi to Berlin via Helsinki which is part of the Barents Euro-Arctic Transport Network connecting Northern Europe, Scandinavia, the Baltic and the Russian railway network. If the ACR would provide finished goods for exportation, it shall offer the possibility for Kirkenes to export raw materials coming from the Kevitsa, Sakatti and probably the Sokli mine thanks to its 500 km for an estimated investment between 2.5 and 3 Billion Euros (Eilertsen, 2018a). We could add the timber from the Finnish forest. Arkhangelsk is already a serious challenger for Murmansk despite an ice blanket covering its access involving the use of an icebreaker. If the MTH is considered as a main project, so is the Arkhangelsk Transport Hub (ATH).

The dredging of the port till 14.5 m port 55 km away from port city of Arkhangelsk will occur between 2023 and 2028 [START_REF] Nilsen | New mega-port in Arkhangelsk with Chinese investments[END_REF] and the upgrade of the Belkomur railway financed by the Chinese group, Polytechnology shall provide the possibility for Arkhangelsk to increase its flows through connection to the Kusbass coal mine and container handling. According to [START_REF] Bambulyak | Oil transport from the Russian part of the Barents Region[END_REF], the update of this 1,161 km railway, with 715 km newly built, should cost around 4.8 billion USD and supply 22 million tons of cargo per year to Arkhangelsk [START_REF] Khomiakova | Arctic Shipping Development Prospect Evaluation: Nuclear Icebreaker Fleet in the Northern Sea Route[END_REF][START_REF] Nilsen | The new railway line connecting the South-Urals with the White Sea is an important step closer to realization as the Komi Republic and Perm Territory sign implementation agreement[END_REF]. More than an opportunity, this railroad appears to be a prerequisite for Arkhangelsk port development [START_REF] Chernov | Phantoms of Russian infrastructure in[END_REF] in order to reach the 30 million tons of output per year. [START_REF] Kokin | The port of Arkhangelsk is Russia's northern gateway to the Arctic[END_REF] shed a light on the investment of coming from Poly Group dedicated to the dredge of the port till -14.5 m and appears as a strategic point for the future Ice Silk Road in western Russia.

To conclude on this prospective part, Murmansk's position as a regional hub may change in the coming years with the upgrade of ports such as Arkhangelsk and the building of others like Sabetta. However, Murmansk must maintain a leading position due to its ability to be ice-free all year round and to manage a larger vessel without dredging its berth.

Conclusion

This analysis made it possible to draw a picture of the Murmansk connection level in 2011 and 2017 based on dry and liquid bulk flows. We may think that this analysis could be complemented by additional work also based on AIS data such as the calculation of shipping time between Arctic ports or the efficiency of ports in handling operations.

The article analyzed how Murmansk's connection with the rest of the world evolved between 2011 and 2017 and demonstrated the importance of this port in Russian strategy. Most of the flows from Murmansk are definitely raw materials coming from an area representing 20% of the national GDP.

Despite these assumptions, our analysis highlighted four main points. Firstly, fishing activity is growing over the years with an 89% increase between 2011 and 2017. This evolution demonstrates the importance the fishing industry can have in the future of Murmansk.

Secondly, liquid bulk flow are quite concentrated and balanced when looking the main destination and origin. This result points out the position of Murmansk as a Regional Hub for transportation of crude oil and LNG coming from the Arctic fields.

Thirdly, the bulk is a product coming from the Murmansk hinterland with very different origin and destination very different from those of liquid bulk.

Finally, the position of Murmansk as a regional hub is challenged by two others ports, Arkhangelsk and Kirkenes. If both do not provide the same level of services as Murmansk, they have some arguments that has already made the difference in the past and may continue in the future.

Fig

Figure 1 :

 1 Figure 1: Nature of AIS data Source: Adapted from Le Guyader, Brosset, Gourmelon, (2011).

Figure 2 :

 2 Figure 2: Calls to Murmansk by Vessel type Source: Authors (2019)

Figure 3a :

 3a Figure 3a: Connection of Murmansk in 2011 -Liquid Bulk flows. Source: Authors (2019) based on IHS

Figure 4a :

 4a Figure 4a: Connection of Murmansk in 2011-Dry bulk flows. Source: Authors (2019) based on IHS

Figure 5 :

 5 Figure 5: Murmansk connection with Arctic ports Source : Faury et al (2019)

Figure 6 :

 6 Figure 6: Prospective vision of the Arctic Range Source: Alix (2018)

Table 1a :

 1a Number of calls for tankers with as origin (80% of the total calls) in 2011

Table 1b :

 1b Number of calls for tankers from Murmansk (80% of the total calls) in 2011 3% of ports represented 60% of Murmansk tankers calling (Table1a and 1b). Exception for Dudinka and Pevek in the eastern shore of Russian Artic zone, no one are Russian. European ports represented the lion share of the flows (5 out of 11) with Rotterdam and Antwerp as, respectively, first and second, ports in number of calls. With the port of new-York, and Corpus Christi in Texas, the USA was connected to Murmansk.

	Source: Authors (2019)
	In 2011,

  Besides, when looking at the number of calls in both directions, they are quite balanced with only a difference of 30 calls between these 8 ports. The difference being explained by Antwerp, Le Havre and Wilhelmshaven.

			Port	To Murmansk
			Rotterdam	25
	Table 2a: Number of calls for tankers	Antwerp Table 2b: Number of calls for tankers from 11
	vessel with as origin (80% of the total	Amsterdam Murmansk (80% of the total calls) in 2017
	Port calls) in 2017 Rotterdam Port Antwerp Varandey New York & New Jersey Rotterdam Fawley Corpus Christi Amsterdam Singapore Ijmuiden Archangel Antwerp Le Havre Sabetta Vorota Arktiki Oil Terminal Pointe-a-Pierre Dudinka Gladstone Pevek Fawley Sullom Voe Mamonal Freeport (Bahamas) Immingham Mongstad Kalundborg Asnaesvaerkets Havn Pevek Galveston Gothenburg Naantali Brofjorden Hamburg St Petersburg Port Said	From Murmansk From Murmansk 34 87 11 58 5 5 5 4 4 29 28 19 18 17 11 3 10 3 8 3 7 3 6 3 6 2 6 2 2 2 6 4 4 2 2	Montreal New York & New Jersey Port Ijmuiden Varandey Fawley Rotterdam Dudinka Pevek Sullom Voe Mongstad Corpus Christi Archangel Vorota Arktiki Oil Terminal Sabetta Antwerp Wilhelmshaven Amderma Le Havre Hamburg Immingham Immingham Skagen Skagen Sydney (Australia) Asnaesvaerkets Havn Sines Hamburg Galveston Botlek Gdansk Kalundborg St Petersburg Botlek Melbourne Liverpool (United Kingdom) Le Havre London	To Murmansk 87 55 31 16 12 10
			Scapa Flow Milford Haven
			Slagen Fawley
			Tallinn Kalundborg
			Wilhelmshaven Pevek
			Algeciras Mongstad
			Vlissingen
			Amsterdam
			Bilbao
			Cork
			Suez
			Gladstone
			Novorossiysk
			Gothenburg
			Piraeus
			Finnart
			Townsville
		Source: Authors (2019)

4.2. Dry-bulk flows

This section focuses on the connection of Murmansk with other ports when dealing with dry bulk carrier whether Murmansk is the destination or the origin. Figure

4a

and 4b point out the importance relation linking Murmansk to the North-range, the American coast of the Mexican

Table 3a :

 3a Number of calls for bulk vessel with as origin (80% of the total calls) in 2011

Table 3b :

 3b Number of calls for bulk vessel from Murmansk (80% of the total calls) in 2011Table3aand 3b stress the ports representing the origin of 80% of vessels calling in Murmansk and the destination of 80% of bulk vessel coming from Murmansk and the numerous varieties of port trading with Murmansk. Furthermore, they point out the existing imbalance of flows. If the main destination is exactly the same as the main origin in the case of tankers, it is clearly not the same for bulk vessels. Besides, the number of time ports receiving vessels coming from Murmansk are not the same number as the number of times vessel coming from these ports call in Murmansk. Table 4a and 4b stressed the strong imbalance between the flows coming in and leaving Murmansk in 2017. Firstly, 80% of calls in vessel calling in Murmansk come from 37 ports and while 80 % of bulk carriers leaving Murmansk are calling in 28 ports. 11 ports that are part of the main destination are not in the main list of the main origin and among them Jorf Lasfar and Singapore respectively the first and eighth destination and 18 new ports appear within the list of main origin. Besides, Sabetta is the only Russian in this list the next being Dudinka with one origin.

			Port	From Murmansk
	Port	Destination Murmansk	Hunterston	12
	Hamburg	19	Immingham	10
	Rotterdam	12	Dunkirk	8
	Immingham	10	Klaipeda	8
	Terneuzen	10	Hamburg	6
	Amsterdam	9	Terneuzen	6
	Antwerp	8	Grenland Harbour	6
	Shannon Foynes Port	7	Jorf Lasfar	6
	Hull	6	Nordenham	5
	Liverpool (United Kingdom)	5	Las Palmas	5
	Botlek	5	Singapore	5
	Newcastle upon Tyne	5	Amsterdam	4
	Hunterston	3	Antwerp	4
	Dunkirk	3	Liverpool (United Kingdom)	4
	Grenland Harbour	3	Hadera	4
	Ijmuiden	3	Donges	4
	Santa Cruz de Tenerife	3	Puerto Cabello	4
	Ghent	3	Botlek	3
	Wilhelmshaven	3	Newcastle upon Tyne	3
	Nordenham	2	Gibraltar	3
	Leith	2	La Coruna	2
	Ashdod	2	Plaquemines	2
	Esbjerg	2
			Port Nador	2
	Teesport	2
			Santander	2
			Suez Canal	2
		Source: Authors (2019)

Table 4a :

 4a Number of calls for bulk vessel with as origin (80% of the total calls) in 2017

	Table 4b: Number of calls for bulk vessel
	from Murmansk (80% of the total calls) in
	2017
	Source: Authors (2019)

IAME 2019 Conference, June 25 th -28 th , Athens, Greece


Jojomon Joseph
email: joseph.jojomon@mitis.be

Rabia Nacereddine

Michel Delanaye

Andres Giraldo

Mehdi Rouabah

Juergen J Brandner

Advanced CFD methodology to investigate heat exchanger performance and experimental validation of a reduced model for a micro-CHP application

Keywords: Micro channel, CFD methodology, Reduced model, Wire-net perturbators, S-shaped perturbators, High-temperature heat exchangers

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

The objective of this paper is to predict compact heat exchanger performance for a miniaturized Combined Heat and Power (CHP) system by a detailed modelling of complex micro channels (with wire-net and S-shaped perturbators) using a new methodology to assess the entire heat exchanger characteristics based on reduced order modelling. Localized turbulence can enhance the heat exchanger performance. Besides, this will also increase the pressure losses too. Shifting the Reynolds critical to smaller Reynolds number by using perturbators will control the pressure losses and enhance the thermal efficiency to a considerable extent. In this paper, we consider the microchannel performance of two different types of perturbators, Wire-net [START_REF] Delanaye | Development of a recuperated flameless combustor for an inverted Bryton cycle microturbine used in residential micro-CHP[END_REF][START_REF] Joseph | Advanced CFD methodology to analyze hightemperature wire net compact heat exchangers for a micro-CHP application[END_REF] and the S-shaped. The wire-net heat exchanger (Figure 1 (a, b, c)) is assembled as a stack of counter-flow passages with optimized thickness separated by thin foils. A metallic wire mesh is inserted in the flow passages (Figure 1 (b)) to provide the required stiffness and enhance the microchannel efficiency (localized turbulence). The S-shaped heat exchanger model consists of S-shaped protrusions (Figure 2 (a)) along the counter-flow passages with an integrated collector (Figure 2

(b)).

There is an optimum mass flow where the thermal efficiency reaches its maximum (See Figure 1 (d)). However, a substantial decrease in efficiency at higher mass flow rates has been encountered [START_REF] Joseph | Advanced CFD methodology to analyze hightemperature wire net compact heat exchangers for a micro-CHP application[END_REF]. The steepness of this efficiency curve pattern is stronger for the wire net design compared to the S-shaped protrusions. However, for the wirenet (at higher Reynolds numbers) the pressure loss is also relatively high together with a lower thermal efficiency as compared with Sshape perturbators. These performance characteristics were utilised to reduce the size and cost of the heat exchanger. A detailed investigation of the S-shaped perturbators showed that the overall heat transfer coefficient is directly correlated with the Turbulent Reynolds stress term, uv. This is induced by the strong recirculation zones induced by the S-shaped structures. The turbulence production term, uv•Du/DY is higher for a particular S-shape arrangement. The increased wire net pressure loss could not enhance the thermal efficiency like the S-shaped perturbators. Linearly arranged Sshaped perturbators with an optimum spacing found to be the best among all other variants (See Figure 2 (a)).

A parametric study was conducted on various heat exchanger parameters to optimize it for the micro-CHP system. The Reynolds number based on the inlet hydraulic diameter is between 30-300 (for micro-channels), 500-30000 (for secondary collectors) and even higher for primary collectors. Microchannel porosity (78-82%) can enhance localized turbulence at smaller Reynolds numbers. Since the Knudsen number is low, thermal creep or rarefaction effects are negligible. Besides, a detailed investigation of the wire net flow physics is made using a higher order Reynolds Stress turbulence model to obtain the full velocity gradient tensor. This could investigate the effect of anisotropic flow physics in the isotropic wire net micro channels. Lambda 2 criteria was implemented to investigate the flow mixing of the centrally convected non-disturbed mass flow. Furthermore, the analysis of the turbulence production terms provided a deeper insight into flow attachment and detachment near the wire net intersections. The CFD methodology (which comprises Conjugate Heat Transfer and Reduced order modelling, See Figure 3) mentioned in this paper is to reduce the computational grid size to a considerable extent and predict the collector performance with reasonable accuracy. The reduced model consists of collectors and micro channels, modelled through a porous medium approximation [START_REF] Yizhou | CFD simulation of a research reactor[END_REF]. The porous medium model [START_REF] Nield | Convection in Porous Media[END_REF][START_REF] Nicolas | High temperature and pressure reactive flows through porous media[END_REF], based on the Darcy-Forchheimer law, is modified (Constant Integration Method) to account for the high-temperature evolution in the heat exchanger. The modified equation takes into account the high-temperature variation inside the micro channels along with the localized turbulence effects [START_REF] Bernard | Turbulent Flow: Analysis, Measurement & Prediction[END_REF]. The resulting microchannel characteristics (pressure drop, temperature drop etc.) from a series of 3D-CFD Conjugate Heat Transfer analysis is used to calculate the inertial and viscous coefficients using the Constant Integration method. These characteristics have been implemented and numerically verified. The best-revised methodology allows obtaining pressure drop with less than three per cent error with respect to the full 3D-CFD Conjugate Heat Transfer modelling for Brayton and Inverted Brayton micro-CHP cycle (See Figure 4). An experimental validation showed that the reduced model predicts the overall heat exchanger performance with a reasonably good accuracy (See Figure 5).

Figure 1 .

 1 Figure 1. Wire net brazed heat exchanger (a), Arrangement (b), Numerical Conjugate Heat Transfer domain (c), Thermal efficiency curve for various mass flows (D).

Figure 2 .Figure 3 .Figure 4 .Figure 5 .

 2345 Figure 2. S-shaped protrusions, microchannel design