Bollig Benedikt
email: bollig@lsv.fr

Lsv

One-Counter Automata with Counter Observability

Keywords: 1998 ACM Subject Classification F.1.1 Models of Computation One-counter automata, inclusion checking, observability, visibly onecounter automata, strong automata

In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are e ectively determinizable and closed under all boolean operations. Moreover, it turns out that they are expressively equivalent to strong automata, in which transitions are guarded by MSO formulas over the natural numbers with successor.

Introduction

One-counter automata (OCAs) are a fundamental model of infinite-state systems. Their expressive power resides between finite automata and pushdown automata. Unlike finite automata, however, OCAs are not robust: They lack closure under complementation and have an undecidable universality, equivalence, and inclusion problem [START_REF] Greibach | An infinite hierarchy of context-free languages[END_REF][START_REF] Ibarra | Restricted one-counter machines with undecidable universe problems[END_REF]. Several directions to overcome this drawback have been taken. One may underapproximate the above decision problems in terms of bisimilarity [START_REF] Ar | Decidability of bisimilarity for one-counter processes[END_REF] or overapproximate the system behavior by a finite-state abstraction, e.g., in terms of the downward closure or preserving the Parikh image [START_REF] Parikh | On context-free languages[END_REF][START_REF] Van Leeuwen | E ective constructions in well-partially-ordered free monoids[END_REF].

In this paper, we consider a new and simple way of obtaining a robust model of onecounter systems. Whenever the automaton produces a letter from a finite alphabet , it will also output the current counter value along with it (transitions that manipulate the counter are not concerned). Hence, its language is henceforth a subset of ( ◊ N) ú . For obvious reasons, we call this variant OCAs with counter observability. We will show that, under the observability semantics, OCAs form a robust automata model: They are closed under all boolean operations. Moreover, their universality and inclusion problem are in PSPACE and, as a simple reduction from universality for finite automata shows, PSPACE-complete.

These results may come as a surprise given that universality for OCAs is undecidable and introducing counter observability seems like an extension of OCAs. But, actually, the problem becomes quite di erent. The fact that a priori hidden details from a run (in terms of the counter values) are revealed makes the model more robust and the decision problems easier. Note that this is also what happens in input-driven/visibly pushdown automata [START_REF] Alur | Adding nesting structure to words[END_REF][START_REF] Mehlhorn | Pebbling mountain ranges and its application of DCFL-recognition[END_REF] XX:2

One-Counter Automata with Counter Observability

or their restriction of visibly OCAs [START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF][START_REF] Srba | Visibly pushdown automata: From language equivalence to simulation and bisimulation[END_REF]. They all recognize languages over a finite alphabet and the stack/counter operation can be deduced from the letter that is read. Interestingly, our proofs establish a link between the observability semantics and visibly OCAs. This link is not immediate and relies on a couple of technical lemmas. However, it somehow explains the robustness of OCAs under the observability semantics.

It is worth noting that revealing details from a system configuration does not always help, quite the contrary: Though timed automata and counter automata are closely related [START_REF] Haase | Relating reachability problems in timed and counter automata[END_REF], the universality problem of timed automata is decidable only if time stamps are excluded from the semantics [START_REF] Alur | A theory of timed automata[END_REF].

Note that it is not only for the pure fact that we obtain a robust model that we consider counter observability. Counter values usually have a meaning, such as energy level, value of a variable, or number of items yet to be produced (cf. Example 2). In those contexts, it is natural to include them in the semantics, just like including time stamps in timed automata.

Apart from the connection with visibly OCAs, another model closely related to ours is that of strong automata [START_REF] Czyba | Finite automata over infinite alphabets: Two models with transitions for local change[END_REF]. Strong automata operate on infinite alphabets and were introduced as an extension of symbolic automata [START_REF] Bès | An application of the Feferman-Vaught theorem to automata and logics for words over an infinite alphabet[END_REF][START_REF] Veanes | Minimization of symbolic automata[END_REF]. Essentially, a transition of a strong automaton is labeled with a formula from monadic second-order (MSO) logic over some infinite structure, say (N, +1). In fact, the formula has two free first-order variables so that it defines a binary relation over N. This relation is interpreted as a constraint between successive letters from the infinite alphabet. We will show that OCAs with the observability semantics and strong automata over (N, +1) (extended by a component for the finite alphabet ) are expressively equivalent. This underpins a certain naturalness of the observability semantics. Note that the universality and the inclusion problem have been shown decidable for strong automata over (N, +1) [START_REF] Czyba | Finite automata over infinite alphabets: Two models with transitions for local change[END_REF]. However, strong automata do not allow us to derive any elementary complexity upper bounds. In fact, our model can be seen as an operational counterpart of strong automata over (N, +1).

The outline of the paper is as follows. Section 2 defines OCAs and their di erent semantics. Section 3 relates the observability semantics with visibly OCAs and shows that, under the new semantics, OCAs are closed under boolean operations and have a PSPACE-complete universality and inclusion problem. In Section 4, we show expressive equivalence of strong automata and OCAs with counter observability. We conclude in Section 5. Omitted proofs or proof details can be found in the full version of this paper, which is available at the following link: https://arxiv.org/abs/1602.05940

One-Counter Automata with Counter Observability

For n oe N = {0, 1, 2, . . .}, we set [n] := {1, . . . , n} and [n] 0 := {0, 1, . . . , n}. Given an alphabet , the set of finite words over , including the empty word Á, is denoted by ú .

One-Counter Automata and Their Semantics

We consider ordinary one-counter automata over some nonempty finite alphabet . In addition to a finite-state control and transitions that produce a letter from , they have a counter that can be incremented, decremented, or tested for values up to some threshold m oe N (as defined in [START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF]). Accordingly, the set of counter operations is Op = {ˆ, ´}, where ˆstands for "increment the counter by one" and ´for "decrement the counter by one". A transition is of the form (q, k, ‡, q Õ ) where q, q Õ are states, k oe [m] 0 is a counter test, and ‡ oe fi Op. It leads from q to q Õ , while ‡ either produces a letter from or modifies the B. Bollig XX:3 counter. However, the transition can only be taken if the current counter value x oe N satisfies k = min{x, m}. That is, counter values can be checked against any number strictly below m or for being at least m. In particular, if m = 1, then we deal with the classical definition of one-counter automata, which only allows for zero and non-zero tests.

q 0 q 1 q 2 q 3 ≥1 | req ˆ≥1 | prod =0 | prod
I Definition 1 (OCA, cf. [START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF]). A one-counter automaton (or simply OCA) is a tuple A = (Q, , ÿ, F, m, ) where Q is a finite set of states, is a nonempty finite alphabet (disjoint from Op), ÿ oe Q is the initial state, F ™ Q is the set of final states, m oe N is the threshold, and

™ Q ◊ [m]
0 ◊ ( fi Op) ◊ Q is the transition relation. We also say that A is an m-OCA. Its size is defined as

|Q| + | | + m + | |.
An OCA A = (Q, , ÿ, F, m, ) can have several di erent semantics: L oca (A) ™ ú is the classical semantics when A is seen as an ordinary OCA. L vis (A) ™ ( fi Op) ú is the visibly semantics where, in addition to the letters from , all counter movements are made apparent.

L

obs (A) ™ ( ◊ N) ú is the semantics with counter observability where the current counter value is output each time a -transition is taken.

We define all three semantics in one go. Let Conf A := Q ◊ N be the set of configurations of A. In a configuration (q, x), q is the current state and x is the current counter value. The initial configuration is (ÿ, 0), and a configuration (q, x) is final if q oe F .

We determine a global transition relation =∆ A ™ Conf A ◊ (( ◊ N) fi Op) ◊ Conf A . For two configurations (q, x), (q Õ , x Õ ) oe Conf A and • oe ( ◊ N) fi Op, we have (q, x)

• =∆ A (q Õ , x Õ ) if one of the following holds:

• = ˆand x Õ = x + 1 and (q, min{x, m}, ˆ, q Õ ) oe , or • = ´and x Õ = x ≠ 1 and (q, min{x, m}, ´, q Õ ) oe , or

x Õ = x and there is a oe such that • = (a, x) and (q, min{x, m}, a, q Õ ) oe . A partial run of A is a sequence fl = (q 0 , x 0 )

•1 =∆ A (q 1 , x 1 ) •2 =∆ A . . . •n =∆ A (q n , x n ), with n Ø 0. If, in addition, (q 0 , x 0 )
is the initial configuration, then we say that fl is a run. We call fl accepting if its last configuration (q n , x n ) is final. Now, the semantics of A that we consider depends on what we would like to extract from trace(fl

) := • 1 . . . • n oe (( ◊ N) fi Op) ú .
We let (given (a, x) oe ◊ N): oca((a, x)) = a and oca(ˆ) = oca(´) = Á vis((a, x)) = a and vis(ˆ) = ˆand vis(´) = óbs((a,

x)) = (a, x) and obs(ˆ) = obs(´) = Á Moreover, we extend each such mapping ÷ oe {oca, vis, obs} to For readability, counter tests 0 and 1 are written as =0 and Ø1, respectively. A transition without counter test stands for two distinct transitions, one for =0 and one for Ø1 (i.e., the counter value may actually be arbitrary). When looking at the semantics L obs (A), i.e., with counter observability, we can think of (req, n) signalizing that the production of n Ø 1 items is required (where n is the current counter value). Moreover, prod indicates that an item has been produced so that, along a run, the counter value represents the number of items yet to be produced. It is thus natural to include it in the semantics. Concretely, we have the following:

• 1 . . . • n oe (( ◊ N) fi Op) ú letting ÷(• 1 . . . • n ) := ÷(• 1 ) • . . . • ÷(• n ). Note that, hereby u • Á = Á • u = u
L oca (A) = {req prod n | n Ø 1} L vis (A) = {ˆnreq (´prod) n | n Ø 1} L obs (A) = {(req, n)(prod, n ≠ 1)(prod, n ≠ 2) . . . (prod, 0) | n Ø 1} Apparently, L vis (A)
and L obs (A) are the only meaningful semantics in the context described above.

I Remark. Visibly OCAs [START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF][START_REF] Srba | Visibly pushdown automata: From language equivalence to simulation and bisimulation[END_REF] usually allow for general input alphabets , which are partitioned into = inc ‡ dec ‡ nop so that every " oe is associated with a unique counter operation (or "no counter operation" if " oe nop ). In fact, we consider here (wrt. the visibly semantics) a particular case where = fi Op with inc = {ˆ}, dec = {´}, and nop = .

Standard Results for OCAs

Let us recall some well-known results for classical OCAs and visibly OCAs. For ÷ oe {oca, vis, obs}, the nonemptiness problem for OCAs wrt. the ÷-semantics is defined as follows: Given an OCA A, do we have L ÷ (A) " = ÿ ? Of course, this reduces to a reachability problem that is independent of the actual choice of the semantics: ([25]). The nonemptiness problem for OCAs is NL-complete, wrt. any of the three semantics.

I Theorem 3
However, the universality (and, therefore, inclusion) problem for classical OCAs is undecidable: ([12, 14]). The following problem is undecidable: Given an OCA A with alphabet , do we have L oca (A) = ú ? In this paper, we show that universality and inclusion are decidable when considering counter observability. To do so, we make use of the theory of the visibly semantics. Concretely, we exploit determinizability as well as closure under complementation and intersection. In fact, the following definition of determinism only makes sense for the visibly semantics, but we will see later that a subclass of deterministic OCAs gives a natural notion of determinism for the observability semantics as well.

I Theorem 4
I Definition 5 (deterministic OCA). An OCA A = (Q, , ÿ, F, m, ) is called deterministic (dOCA or m-dOCA) if, for all (q, k, ‡) oe Q ◊ [m] 0 ◊ ( fi Op)
, there is exactly one q Õ oe Q such that (q, k, ‡, q Õ ) oe . In that case, represents a (total) function " : Q◊ [m] 0 ◊( fiOp) ae Q so that we rather consider A to be the tuple (Q, , ÿ, F, m, ").

A powerset construction like for finite automata can be used to determinize OCAs wrt. the visibly semantics [START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF]. That construction also preserves the two other semantics. However, Definition 5 only guarantees uniqueness of runs for words from ( fi Op) ú . That is, for complementation, we have to restrict to the visibly semantics (cf. Lemma 7 below).

B. Bollig

XX:5

counter value

a 1 a 2 x 1 x 2 ι p 1 p 2 p ′ 2 p 3 p 4 p 5 p 6 p 7 p 8 2 |= ϕ p2,p ′ 2 1 |= ψ p7,p8 ∧ ψ q7,q8 a 1 a 2 x 1 x 2 ι q 1 q 2 q 3 q 4 q 5 q 6 q 7 q 8 a 1 a 2 x 1 x 2
. . . ι p 1 p 2 p 3 p 4 p 5 p 6 p 7 q 1 q 2 q 3 q 4 q 5 q 6 q 7 ↘ ↗ Figure 2 Decompositions of two runs on (a1, 3)(a2, 1), and corresponding runs in normal form I Lemma 6 (cf. [START_REF] Bárány | Regularity problems for visibly pushdown languages[END_REF]). Let A be an m-OCA. There is an m-dOCA A det of exponential size such that L ÷ (A det ) = L ÷ (A) for all ÷ oe {oca, vis, obs}. A (visibly) dOCA can be easily complemented wrt. the set of well-formed words WF := {w oe ( fi Op) ú | no prefix of w contains more ´'s than ˆ's}. In fact, for all OCAs A with alphabet , we have L vis (A) ™ WF .

I Lemma 7. Let A = (Q, , ÿ, F, m, ") be a dOCA and define Ā as the dOCA (Q, , ÿ, Q \ F, m, "). Then, L vis ( Ā) = WF \ L vis (A).
Finally, visibility of counter operations allows us to simulate two OCAs in sync by a straightforward product construction: I Lemma 8 (cf. [START_REF] Alur | Adding nesting structure to words[END_REF]). Let A 1 be an m 1 -OCA and A 2 be an m 2 -OCA over the same alphabet. There is a max{m

1 , m 2 }-OCA A 1 ◊ A 2 of polynomial size such that L vis (A 1 ◊ A 2 ) = L vis (A 1 ) fl L vis (A 2 ). Moreover, if A 1 and A 2 are deterministic, then so is A 1 ◊ A 2 .

Determinizing and Complementing OCAs

In this section, we will show that, under the observability semantics, OCAs are e ectively closed under all boolean operations. The main ingredient of the proof is a determinization procedure, which we first describe informally. Let A = (Q, , ÿ, F, m, ) be the OCA to be determinized (wrt. the observability semantics). Moreover, let w = (a

1 , x 1 ) . . . (a n , x n ) oe ( ◊ N) ú .
Every run fl of A such that obs(trace(fl)) = w has to have reached the counter value x

1 by the time it reads the first letter a 1 . In particular, it has to perform at least x 1 counter increments. In other words, we can identify x 1 transitions that lift the counter value from 0 to 1, from 1 to 2, and, finally, from x 1 ≠ 1 to x 1 , respectively, and that are separated by partial runs that "oscillate" around the current counter value but, at the end, return to their original level. Similarly, before reading the second letter a 2 , A will perform |x 2 ≠ x 1 |-many identical counter operations to reach x 2 , again separated by some oscillation phases, and so on. This is illustrated on the left hand side of Figure 2 for two runs on the word (a 1 , 3)(a 2 , 1). We will transform A into another automaton that decomposes a run into oscillations and increment/decrement/letter transitions, but, in fact, abstracts away oscillations. Thus, the automaton starts in an increasing mode and goes straight to the value x 1 . Once it reads letter a 1 , it may go into an increasing or decreasing mode, and so on. Observe that a run fl F S T T C S 2 0 1 6

XX:6

One-Counter Automata with Counter Observability of this new automaton is in a sort of normal form as illustrated on the right hand side of Figure 2. The crux is that vis(trace(fl)) is a unique encoding of w: Of course, it determines the counter values output when a letter is read; and it is unique, since it continues incrementing (decrementing, respectively) until a letter is read. This normalization and encoding finally allows us to apply known results on visibly one-counter automata for determinization and complementation.

There is a little issue here, since the possibility of performing an oscillation leading from p 2 to p Õ 2 (cf. left hand side of Figure 2) depends on the current counter value. However, it was shown in [START_REF] Göller | On the computational complexity of verifying one-counter processes[END_REF] that the set of counter values allowing for such a shortcut can be described as a boolean combination of arithmetic progressions that can be computed in polynomial time. We will, therefore, work with an extended version of OCAs that includes arithmetic-progression tests (but is no more expressive, as we show afterwards).

The outline of this section is as follows: We present extended OCAs in Section 3.1 and the link between the observability and the visibly semantics in Section 3.2. In Section 3.3, we solve the universality and inclusion problem for OCAs wrt. the observability semantics.

Extended One-Counter Automata

While OCAs can only test a counter value up to some threshold, extended OCAs have access to boolean combinations of modulo constraints. The set Guards mod is given by the grammar Before we introduce extended OCAs, we will state a lemma saying that the "possibility" of a shortcut in terms of an oscillation (see above) is definable in Guards mod . Let A = (Q, , ÿ, F, m, ) be an OCA and p, q oe Q. By X A p,q , we denote the set of natural numbers x oe N such that (p, x) ( =∆ A fi =∆ A ) ú (q, x), i.e., there is a partial run from (p, x) to (q, x) that performs only counter operations. Moreover, we define Y A p,q to be the set of natural numbers x oe N such that (p, x) ( =∆ A fi =∆ A ) ú (q, x Õ ) for some x Õ oe N. Note that

Ï ::= c + dN | ¬Ï | Ï • Ï | Ï ' Ï
X A p,q ™ Y A p,q .
The following result is due to [11, Lemmas 6-9]: I Lemma 9 ([11]). Let A = (Q, , ÿ, F, m, ) be an OCA and p, q oe Q. We can compute, in polynomial time, guards Ï p,q ,  p,q oe Guards mod such that [[Ï p,q ]] = X A p,q and [[ p,q ]] = Y A p,q . In particular, the constants in Ï p,q and  p,q are all polynomially bounded. I Definition 10 (extended OCA). An extended OCA (eOCA) is a tuple A = (Q, , ÿ, f, ) where Q, , ÿ are like in an OCA, f : Q ae Guards mod is the acceptance condition, and is the transition relation:

a finite subset of Q ◊ Guards mod ◊ ( fi Op) ◊ Q

Runs and the languages L

÷ (A), with ÷ oe {oca, vis, obs}, of an eOCA A = (Q, , ÿ, f, ) are defined very similarly to OCAs. In fact, there are only two (slight) changes:

The definition of =∆

A ™ Conf A ◊ (( ◊ N) fi Op) ◊ Conf A is
now as follows: For (q, x), (q Õ , x Õ ) oe Conf A and • oe ( ◊ N) fi Op, we have (q, x)

• =∆ A (q Õ , x Õ ) if there is Ï oe Guards mod such that x |= Ï and one of the following holds:

• = ˆand x Õ = x + 1 and (q, Ï, ˆ, q Õ ) oe , or • = ´and x Õ = x ≠ 1 and (q, Ï, ´, q Õ ) oe , or x Õ = x and there is a oe such that • = (a, x) and (q, Ï, a, q Õ ) oe .

B. Bollig XX:7

2. A run is now accepting if its last configuration (q, x) is such that x |= f (q). Apart from these modifications, the languages L oca (A), L vis (A), and L obs (A) are defined in exactly the same way as for OCAs.

From OCAs with Counter Observability to Visibly OCAs

To establish a link between the observability and the visibly semantics, we will encode a word w = (a Obviously, there is a small dOCA whose visibly semantics is Enc . It will be needed later for complementation of OCAs wrt. the observability semantics. I Lemma 11. There is a 0-dOCA B enc with only four states such that L vis (B enc ) = Enc . The idea is that B enc enters an "increasing" or "decreasing" mode as soon as it performs ˆor, respectively, ´. Such a mode can only be quit by reading a letter from or entering a sink state. This avoids forbidden reversals between ˆand ´. Finally, it is easy to ensure that any nonempty accepted word ends in a letter from .

In fact, there is a tight link between the visibly and the observability semantics of OCAs provided the visibly semantics contains only valid encodings: I Lemma 12. Let A be an OCA with alphabet such that L vis (A) ™ Enc . Then, we have L vis (A) = enc(L obs (A)) and, equivalently, L obs (A) = enc ≠1 (L vis (A)). Lemmas 8 and 12 imply the following closure property, which will later be exploited to solve the inclusion problem: Lemma 8). The next lemma constitutes the main ingredient of the determinization procedure. It will eventually allow us to rely on OCAs whose visibly semantics consists only of valid encodings. I Lemma 14. Let A be an OCA. We can compute, in polynomial time, an eOCA A ext such that L obs (A ext ) = L obs (A) and, for all w oe L obs (A ext ), we have enc(w) oe L vis (A ext ). Proof. Suppose A = (Q, , ÿ, F, m, ) is the given OCA. We first translate a simple "threshold constraint" into an arithmetic expression that can be used as a guard in the eOCA A ext : Let fi m = m + 1N, and fi k = k + 0N for all k oe {0, . . . , m ≠ 1}. We define A ext = (Q, , ÿ, f, Õ ) as follows: Essentially, A ext simulates A so that it has the same state space. However, when A allows for a shortcut (oscillation) from state p to state q (which will be checked in terms of Ï p,q from Lemma 9) and there is a transition (q, k, ‡, q Õ ) of A, then A ext may perform ‡ and go directly from p to q Õ , provided fi k is satisfied as well. Formally, the transition relation is given as for some q oe F (cf. Lemma 9). That is, for all p oe Q, we let f (p) = x qoeF Â p,q . J To transform an eOCA back into an ordinary OCA while determinizing it and preserving its observability semantics, we will need a dOCA that takes care of the modulo constraints: I Lemma 15. Let ™ Guards mod be a nonempty finite set. Set m := max{c | c + dN is an atomic subformula of some Ï oe } + 2. There are a dOCA B = (Q, , ÿ, Q, m , ") of exponential size and ⁄ : Q ae 2 such that, for all (q, x) oe Conf B and all runs of B ending in (q, x), we have ⁄(q) = {Ï oe | x |= Ï}.

I Proposition 13. Let A 1 and A 2 be OCAs over such that L vis (A 1 ) ™ Enc and L vis (A 2 ) ™ Enc . Then, L obs (A 1 ◊ A 2 ) = L obs (A 1 ) fl L obs (A 2 ) (where A 1 ◊ A 2 is due to
Õ = {(p, Ï p,q • fi k , ‡, q Õ ) | p oe Q and (q, k, ‡, q Õ ) oe } .

F S T T C S

Proof. We sketch the idea. For every arithmetic-progression formula c + dN that occurs in (for simplicity, let us assume d Ø 1), we introduce a state component {0, 1, . . . , c} ◊ {0, 1, . . . , d ≠ 1}. Increasing the counter, we increment the first component until c and then count modulo d in the second. We proceed similarly when decreasing the counter. The current state (x, y) oe [c] 0 ◊ [d ≠ 1] 0 will then tell us whether c + dN holds, namely i x = c and y = 0. Finally, the mapping ⁄ evaluates a formula based on the outcome for its atomic subformulas. Note that B can be computed in exponential time. Its size is exponential in the number of arithmetic-progression formulas that occur in . J

We will now apply Lemma 15 to transform an eOCA into a dOCA (cf. also Lemma 6).

I Lemma 16. Let A be an eOCA. We can compute, in exponential time, a dOCA A Õ (deterministic according to Definition 5) such that L ÷ (A Õ ) = L ÷ (A) for all ÷ oe {oca, vis, obs}. Proof. Suppose A = (Q, , ÿ, f, ) is the given eOCA. Let ™ Guards mod be the set of formulas that occur in or f , and let B = ( Q, , ÿ, Q, m , ") be the dOCA along with the function ⁄ according to Lemma 15.

We build the dOCA A Õ = (Q Õ , , ÿ Õ , F Õ , m , " Õ ) as follows. Essentially, we perform a simple powerset construction for A. Moreover, to eliminate modulo guards, we run B in parallel. Thus, the set of states is Q Õ = 2 Q ◊ Q, with initial state ÿ Õ = ({ÿ}, ÿ) and set of final states

F Õ = {(P, q) oe Q Õ | f (p) oe ⁄(q)
for some p oe P }. Finally, the transition function is given by " Õ ((P, q), k, ‡) = (P Õ , "(q, k, ‡)) where

P Õ = ) p Õ | (p, Ï, ‡, p Õ ) oe fl (P ◊ ⁄(q) ◊{ ‡}◊Q) * . J
There is a "nondeterministic version" of Lemma 16, which does not perform a powerset construction but rather computes a nondeterministic OCA. The latter is then still of exponential size, but only wrt. to the number of arithmetic-progression formulas in A.

With Theorem 3, it follows that nonemptiness for eOCAs can be solved in PSPACE. We do not know if this upper bound is tight.

Let A be a dOCA with alphabet and let w oe ( ◊ N) ú . By fl A (w), we denote the unique run of A such that vis(trace(fl A (w))) = enc(w).

By the following observation, which follows directly from Lemma 12, it is justified to call any dOCA A with L vis (A) ™ Enc deterministic wrt. the observability semantics: I Lemma 17. Let A be a dOCA such that L vis (A) ™ Enc . For every word w oe ( ◊ N) ú , we have w oe L obs (A) i fl A (w) is accepting. Altogether, we obtain that OCAs are determinizable wrt. the observability semantics.

I Theorem 18 (determinizability). Let A be an OCA over . We can compute, in exponential time, an m-dOCA A Õ (with m only polynomial) such that L obs (A Õ ) = L obs (A) and L vis (A Õ ) ™ Enc .

B. Bollig XX:9

Proof. Let A be the given OCA. We apply Lemmas 14 and 16 to obtain a dOCA Â A of exponential size such that L obs ( Â A) = L obs (A) and, for all w oe L obs ( Â A), we have enc(w) oe Lemmas 8 and 11) and obtain L obs (A Õ ) = L obs (A) and L vis (A Õ ) ™ Enc . J

L vis ( Â A). We set A Õ = Â A ◊ B enc (cf.
We conclude that OCAs are complementable wrt. the observability semantics:

I Theorem 19 (complementability). Let A be an OCA with alphabet . We can compute, in exponential time, a dOCA

Ā such that L obs ( Ā) = ( ◊ N) ú \ L obs (A). Proof. We first transform A into the dOCA A Õ =  A ◊ B enc according to (the proof of) Theorem 18. Suppose  A = (Q, , ÿ, F, m, "). Then, we set Ā = (Q, , ÿ, Q \ F, m, ") ◊ B enc .
Note that Ā is indeed a dOCA and that L vis ( Ā) ™ Enc . For w oe ( ◊ N) ú , we have:

w oe L obs ( Ā)
Lem. 17

≈∆ fl Ā(w) is accepting (ú)
≈∆ fl A Õ (w) is not accepting Lem. 17

≈∆ w " oe L obs (A Õ ) Equivalence (ú) holds as fl Ā(w) and fl A Õ (w) have the same projection to the Q-component. J Determinization and complementation of extended OCAs are a priori more expensive: Lemmas 9 and 14 only apply to OCAs so that one has to go through Lemma 16 first.

Universality and Inclusion Problem wrt. Observability Semantics

We are now ready to solve the universality and the inclusion problem for OCAs wrt. the observability semantics. The universality problem is defined as follows: Given an OCA A over some alphabet , do we have L obs (A) = ( ◊ N) ú ? The inclusion problem asks whether, given OCAs A Proof. To solve the universality problem for a given OCA A = (Q, , ÿ, F, m, ) in (nondeterministic) polynomial space, we apply the construction from Theorem 19 (and, in particular, Theorem 18) on the fly to obtain a dOCA Ā such that L obs ( Ā) = ( ◊ N) ú \ L obs (A). That is, we have to keep in memory a state of the form (P, q, r), where P ™ Q, q is the modulo-counting component (Lemma 15), and r is a state of B enc (Lemma 11). In addition, we will maintain a component for the current counter value. In fact, the latter can be supposed to be polynomially bounded (cf. [START_REF] Chistikov | Shortest paths in one-counter systems[END_REF] for a tight upper bound) in the size of Ā. The size of Ā is exponential in the size of A, and so the required information can be stored in polynomial space. To compute a successor state of (P, q, r), we first guess an operation ‡ oe fi Op. We then compute (P Õ , q Õ ) according to the proof of Lemma 16 and update r to r Õ according to the type of ‡. Note that this takes polynomial time only, since the function ⁄ as required in Lemma 15 can be computed on the fly. Finally, the algorithm outputs "non-universal" when we find a final state of Ā.

For the inclusion problem, we rely on Proposition 13 and perform the determinization procedure on-the-fly for both of the given OCAs.

For the lower bound, we will restrict to the universality problem, since it is a special case of the inclusion problem. We reduce from the universality problem for ordinary finite automata, which is known to be PSPACE-complete [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF]. If we suppose that is part of the input, then there is a straightforward reduction, which essentially takes the (ordinary) finite F S T T C S 2 0 1 6 XX:10 One-Counter Automata with Counter Observability automaton and adds self-looping increment/decrement transitions to each state. Assuming | | = 1, the reduction is as follows. Let A be a finite automaton over some finite alphabet = {a 0 , . . . , a n≠1 }. We construct an OCA A Õ over the singleton alphabet such that

L(A) = ú i L(A Õ ) = ( ◊ N) ú .
The idea is to represent letter a i by (counter) value i. To obtain A Õ , an a i -transition in A is replaced with a gadget that nondeterministically outputs i or any other natural number strictly greater than n ≠ 1. J

Relation with Strong Automata

In this section, we show that OCAs with counter observability are expressively equivalent to strong automata over (N, +1) [START_REF] Czyba | Finite automata over infinite alphabets: Two models with transitions for local change[END_REF]. As the latter are descriptive in spirit, OCAs can thus be seen as their operational counterpart.

Let us first give a short account of monadic second-order (MSO) logic over (N, +1) (see [START_REF] Thomas | Languages, automata and logic[END_REF] for more details). We have infinite supplies of first-order variables, ranging over N, and second-order variables, ranging over subsets of N. The atomic formulas are true, x Õ = x + 1, x Õ = x, and x oe X where x and x Õ are first-order variables and X is a second-order variable. Those formulas have the expected meaning. Further, MSO logic includes all boolean combinations, first-order quantification ÷x , and second-order quantification ÷X (with an MSO formula). The latter requires that there is a (possibly infinite) subset of N satisfying . As abbreviations, we may also employ x Õ = x ≠ 1 and formulas of the form x Õ oe (x + c + dN), where c, d oe N. This does not change the expressive power of MSO logic.

In the following, we assume that x and x Õ are two distinguished first-order variables. We write (x, x Õ ) to indicate that the free variables of are among x and x Õ . If (x, x Õ ) is evaluated to true when x is interpreted as x oe N and x Õ is interpreted as x Õ oe N, then we write (x, x Õ ) |= . In fact, a transition of a strong automaton is labeled with a formula (x, x Õ ) and can only be executed if (x, x Õ ) |= where x and x Õ are the natural numbers read at the previous and the current position, respectively. Thus, two successive natural numbers in a word can be related explicitly in terms of an MSO formula.

I Definition 21 ([9]). A strong automaton is a tuple S = (Q, , ÿ, F, ) where Q is the finite set of states, is a nonempty finite alphabet, ÿ oe Q is the initial state, and F ™ Q is the set of final states. Further, is a finite set of transitions, which are of the form (q, , a, q Õ ) where q, q Õ oe Q are the source and the target state, a oe , and (x, x Õ ) is an MSO formula.

Similarly to an OCA, S induces a relation =∆ S ™ Conf S ◊ ( ◊ N) ◊ Conf S , where Conf S = Q ◊ N. For (q, x), (q Õ , x Õ ) oe Conf S and (a, y) oe ◊ N, we have (q, x) (a,y)

===∆ S (q Õ , x Õ ) if y = x Õ and there is an MSO formula (x, x Õ ) such that (q, , a, q Õ ) oe and (x, x Õ ) |= .

A run of S on w = (a

1 , x 1 ) . . . (a n , x n ) oe ( ◊ N) ú is a sequence fl = (q 0 , x 0 ) (a1,x1) = ==== ∆ S (q 1 , x 1 ) (a2,x2) = ==== ∆ S . . . (an,xn)
= ==== ∆ S (q n , x n ) such that q 0 = ÿ and x 0 = 0. It is accepting if q n oe F . The language L(S) ™ ( ◊ N) ú of S is defined as the set of words w oe ( ◊ N) ú such that there is an accepting run of S on w. I Example 22. We refer to the OCA A from Example 2. Figure 3 depicts a strong automaton

S such that L(S) = L obs (A) = {(req, n)(prod, n ≠ 1)(prod, n ≠ 2) . . . (prod, 0) | n Ø 1}.
In fact, we can transform any OCA into an equivalent strong automaton preserving the observability semantics, and vice versa: Proof. "=∆": Using the following observation, we can directly transform an OCA into a strong automaton: For all states q and q Õ of the given OCA A, there is an MSO formula q,q Õ (x, x Õ ) such that, for all x, x Õ oe N, we have (x, x Õ ) |= q,q Õ i (q, x)

I Theorem 23. Let L ™ ( ◊ N) ú . There is an OCA A such that L obs (A) = L i there is a strong automaton S such that L(S) = L. B. Bollig XX:11 q 0 q 1 q 2 x ′ ≥ 1 | req x ′ = x -1 | prod x ′ = x -1 ∧ x ′ = 0 | prod
! =∆ A fi =∆ A " ú (q Õ , x Õ
). The existence of q,q Õ can be shown using a two-way automaton over infinite words [START_REF] Pécuchet | Automates boustrophédon et mots infinis[END_REF], which simulates A and can be translated into an MSO formula [START_REF] Pécuchet | Automates boustrophédon et mots infinis[END_REF][START_REF] Thomas | Languages, automata and logic[END_REF].

More precisely, given q, q Õ , we build a two-way automaton T q,q Õ over the alphabet 2 {$,$ Õ } . The idea is that word positions represent counter values (the first position marking 0, the second 1, and so on), and $ and $ Õ represent x and x Õ , respectively. Thus, we are only interested in words in which $ and $ Õ each occur exactly once. Clearly, this is a regular property. At the beginning, T q,q Õ goes to the position carrying $. It then simulates A starting in q, and it accepts if it is on the position carrying $ Õ and in state q Õ . The simulation itself is straightforward: Counter increments and decrements of an OCA are simulated by going one step to the left or to the right, respectively, and a zero test simply checks whether the automaton is at the first position of the word. Note that T q,q Õ checks for the markers $ and $ Õ only at the beginning and at the end of an execution, but not during the actual simulation

of A. Let w = z 0 z 1 z 2 . . . oe ! 2 {$,$ Õ } "
Ê and x, x Õ oe N be unique positions such that $ oe z x and $ Õ oe z

x Õ . Then, w is accepted by T q,q Õ i (q, x) ( =∆ A fi =∆ A ) ú (q Õ , x Õ ). It is well known that two-way word automata are expressively equivalent to one-way automata (cf. [START_REF] Pécuchet | Automates boustrophédon et mots infinis[END_REF]). Therefore, by Büchi's theorem, the word language accepted by T q,q Õ can be translated into a corresponding MSO formula without free variables but with subformulas of the form "position y carries $" and "position y carries $ Õ " [START_REF] Thomas | Languages, automata and logic[END_REF]. We replace the latter two by y = x and y = x Õ , respectively, and finally obtain q,q Õ as required.

"≈=": We will transform a strong automaton S into an equivalent OCA with super transitions.

A super transition can perform counter operations of the form + or ≠ where  oe Guards mod . Operation + allows the counter value to be increased by n oe N provided n |= Â. Similarly, ≠ allows the counter value to be decreased by n if n |= Â.

I Definition 24 (OCA with super transitions). An OCA with super transitions is a tuple A = (Q, , ÿ, F, ) where Q, , ÿ, F are like in an OCA and is the finite transition relation.

A transition is of the form (q, Ï, op, a, Ï Õ , q Õ ) where q, q Õ oe Q are the source and the target state, Ï, Ï Õ oe Guards mod are guards checking the original and the modified counter value, respectively, a oe is the output letter, and op is of the form + or ≠ where  oe Guards mod . We define a global transition relation =∆ A ™ Conf A ◊ ( ◊ N) ◊ Conf A where, as usual, Conf A = Q ◊ N. For (q, x), (q Õ , x Õ ) oe Conf A and (a, y) oe ◊ N, we have (q, x) (a,y)

===∆ A (q Õ , x Õ ) if y = x Õ and there are Ï, Ï Õ , Â oe Guards mod such that x |= Ï, x Õ |= Ï Õ , and one of the following holds:

x AE x Õ and (q, Ï, +Â, a, Ï Õ , q Õ ) oe and x Õ ≠ x |= Â, or

x Ø x Õ and (q, Ï, ≠Â, a, Ï Õ , q Õ ) oe and x ≠ x Õ |= Â. This concludes the correctness proof of A. Finally, recall that one can easily transform A into an OCA whose observability semantics coincides with L(A). J

Conclusion

The observability semantics opens several directions for follow-up work. We may carry it over to other classes of infinite-state systems such as Petri nets. Are there infinite-state restrictions of Petri nets other than 1-VASS whose observability semantics is robust? A direct application of our results is that the language L ™ ( ◊ N) ú of an OCA with observability semantics/strong automaton is learnable (in the sense of Angluin [START_REF] Angluin | Learning regular sets from queries and counterexamples[END_REF]) in terms of a visibly one-counter automaton for enc(L) [START_REF] Neider | Learning visibly one-counter automata in polynomial time[END_REF]. It would be worthwhile to transfer results on visibly one-counter/pushdown automata that concern Myhill-Nerode congruences or minimization [START_REF] Alur | Congruences for visibly pushdown languages[END_REF][START_REF] Chervet | Minimizing variants of visibly pushdown automata[END_REF].

Another interesting question is to which extent we can relax the requirement that the counter value be output with every letter a oe . It may indeed be possible to deal with a bounded number of -transitions between any two counter outputs. Note that there have been relaxations of the visibility condition in pushdown automata, albeit preserving closure under boolean operations [START_REF] Nowotka | Height-deterministic pushdown automata[END_REF].

Figure 1 A

 1 Figure 1 A one-counter automaton with threshold m = 1

FI Example 2 .

 2 for any word u. Finally, we let L ÷ (A) = {÷(trace(fl)) | fl is an accepting run of A}. Consider the 1-OCA A from Figure 1 over = {req, prod}.

  where c, d oe N. We call c + dN an arithmetic-progression formula and assume that c and d are encoded in unary. For x oe N (a counter value), we define x |= c + dN if x = c + d • i for some i oe N. Thus, we may use true as an abbreviation for 0 + 1N. The other formulas are interpreted as expected. Moreover, given Ï oe Guards mod , we set [[Ï]] := {x oe N | x |= Ï}.

1 and A 2 ,

 2 we have L obs (A 1 ) ™ L obs (A 2 ). I Theorem 20. The universality problem and the inclusion problem for OCAs wrt. the observability semantics are PSPACE-complete. In both cases, PSPACE-hardness already holds when | | = 1.

Figure 3 A

 3 Figure 3 A strong automaton over (N, +1)

F S T T C S 2 0 1 6 XXFigure 4

 64 Figure 4 Finite automaton for L + (c1, d1, c2, d2)

  The mapping enc is extended to sets L ™ ( ◊ N) ú by enc(L) = {enc(w) | w oe L}. Let Enc := enc(( ◊ N) ú ) denote the set of valid encodings. Note that enc is a bijection between ( ◊ N) ú and Enc , and that Enc is the set of well-formed words of the form u

	1 , x 1 )(a 2 , x 2 ) . . . (a n , x n ) oe ( ◊ N) ú as a word enc(w) oe ( fi Op) ú as follows: a 1 sign(x 2 ≠ x 1 ) |x2≠x1| a 2 . . . sign(x n ≠ x n≠1 ) |xn≠xn≠1| a n enc(w) := ˆx1 where, for an integer z oe Z, we let sign(z) = ˆif z Ø 0, and sign(z) = ´if z < 0. For example, enc(Á) = Á and enc((a, 5)(b, 2)(c, 4)) = ˆ5a ´3b ˆ2c. 1 a 1 u 2 a 2 . . . u n a n where a i oe and
	u

i oe {ˆ} ú fi {´} ú for all i oe {1, . . . , n}.

2 0 1 6 XX:8 One-Counter Automata with Counter Observability Moreover

  , a configuration (p, x) is "final" in A ext if the current counter value x satisfies Â

	p,q

Acknowledgments

The author is grateful to C. Aiswarya, Stefan Göller, Christoph Haase, and Arnaud Sangnier for numerous helpful discussions and pointers to the literature.

F S T T C S

2 0 1 6 XX:14 One-Counter Automata with Counter Observability

With this, the language L(A) ™ ( ◊ N) ú is defined in the expected way, like for strong automata.

It is easily seen that A can be translated into an eOCA A Õ such that L obs (A Õ ) = L(A): For every  oe Guards mod , the set {⇤ n | n oe [[Â]]} is a regular language over the unary alphabet {⇤}. Thus, counter operations of the form + or ≠ can be simulated by a finite-state gadget. Essentially, we take a finite automaton for {⇤ n | n oe [[Â]]} and replace ⇤ by ˆor, respectively, ´. It will thus be enough to translate a strong automaton into an OCA with super transitions.

Next, we demonstrate why super transitions are indeed useful to emulate an MSO formula (x, x Õ ). Using Büchi's theorem (cf. [START_REF] Thomas | Languages, automata and logic[END_REF]), we can transform into finite automata B + and B ≠ recognizing the following regular languages over the alphabet {⇤, $ 1 , $ 2 }:

x, y oe N such that (x + y, x) |= } Similarly to $ and $ Õ in the other proof direction, the positions of $ 1 and $ 2 in a word from L(B + ) fi L(B ≠ ) encode an interpretation of the free variables x and, respectively, x Õ that makes true. Note that L(B + ) can be written as a finite union of sets

This is achieved by determinizing B + and splitting it into components as illustrated in Figure 4 (cf. also [START_REF] To | Unary finite automata vs. arithmetic progressions[END_REF] for a polynomial transformation). Similarly, L(B ≠ ) is the finite union of sets of the form

and

. We now turn to the actual translation of a strong automaton S = (Q, , ÿ, F, ) into an OCA with super transitions A = (Q, , ÿ, F, Õ ) such that L(A) = L(S). Note that the only change is in the transition relation: For all (q, , a, q Õ ) oe and (c

), a, true, q Õ ). Moreover, for all (q, , a, q Õ ) oe and

). This concludes the construction of A.

To prove L(A) = L(S), it is enough to show that, for all configurations (q, x), (q Õ , x Õ ) oe Conf A and all a oe , the following are equivalent:

(1) (q, x)

B. Bollig

XX:13

Suppose (1) holds. There is an MSO formula such that (q, , a, q Õ ) oe and (x, x Õ ) |= . We distinguish two (not necessarily disjoint) cases:

), a, true, q Õ ) oe Õ , (2) holds as well. Now, suppose x Ø x Õ . Then, by (x, x Õ ) |= , we have a,c 1 +d 1 N, q Õ ) oe Õ . We conclude that (2) holds.

Towards the other direction, suppose that (2) is true. Again, we will distinguish two (not necessarily disjoint) cases: Suppose x AE x Õ and suppose there is

There is an MSO formula such that (q, , a, q Õ ) oe and (c

). Thus, (x, x Õ ) |= . We deduce that (1) holds.

Assume x Ø x Õ and suppose there is a transition (q, true, ≠(c 2 +d 2 N), a, c

. There is such that (q, , a, q Õ ) oe and (c

). This implies (x, x Õ ) |= . Thus, (1) holds.


Abdel Nasser Tigrine

Zohra Bellahsene

Konstantin Todorov

Light-Weight Cross-Lingual Ontology Matching with LYAM++

Keywords: Ontology Matching, Background Knowledge, Cross-lingualisme 1

During the last decade, several automatic ontology matching systems were developed to address the problem of ontology heterogeneity. Aligning cross-lingual ontologies is among the current challenging issues in the field of ontology matching. The majority of the existing approaches rely on machine translation to deal with this problem. However, inherent problems of machine translation are imprecision and ambiguity. In this paper, we propose a novel approach to the cross-lingual ontology matching task, relying on the large multilingual semantic network BabelNet as a source of background knowledge to assist the matching process. We have designed and tested a novel orchestration of the components of the matching workflow. Our approach is implemented under the form of a prototype named LYAM++ (Yet Another Matcher-Light)a fully automatic cross-lingual ontology matching system that does not rely on machine translation. We report the results of our experiments that show that LYAM++ outperforms considerably the best techniques in the state-of-the-art according to the obtained results on the MultiFarm datasets of the Ontology Alignment Evaluation Initiative 2014.

Introduction

Ontologies have become key elements in a variety of knowledge-based applications. However, they are continuously confronted with the problem of heterogeneity -syntactic, terminological, conceptual or semantic. Ontology matching techniques propose solutions to the heterogeneity problem by automatically discovering correspondences between the elements of two different ontologies and thus enabling interoperability [START_REF] Euzenat | Ontology matching[END_REF][START_REF] Ngo | YAM++ : A multi-strategy based approach for ontology matching task[END_REF].

In spite of the considerable progress that has been made in the field of ontology matching recently, many questions still remain open and many challenges to face -a complete overview can be found in [START_REF] Shvaiko | Ontology matching: state of the art and future challenges[END_REF]. The current work addresses the challenge of using explicit reference knowledge in order to make up for the missing background knowledge in the matching process. We apply this solution to a particular ontology matching problem -aligning cross-lingual ontologies, i.e., ontologies that are defined in different natural languages. Indeed, considering multilingual and cross-lingual information is becoming more and more important, in view particularly of the growing number of contentcreating non-English users and the clear demand of cross-language interoperability leading to the need of bringing multilingual semantic information and knowledge together in an explicit manner. In the context of the web of data, it is important to propose procedures for linking vocabularies across natural languages. Ontology matching techniques are also largely applied for data linking, or instance matching, where the problem of multilingualism appears even more often. Cross-lingual data and ontology matching is therefore a crucial task in order to foster the creation of a global information network, instead of a set of linguistically isolated data islands. However, as observed by Spohr et al. [START_REF] Spohr | A machine learning approach to multilingual and cross-lingual ontology matching[END_REF], most of the ontology alignment algorithms assume that the ontologies to be aligned are defined in a single natural language.

The methods that have been proposed to deal with cross-lingual ontology matching most commonly rely on automatic translation of labels to a single target language [START_REF] Faria | The agreementmakerlight ontology matching system[END_REF]. However, machine translation tolerates low precision levels and there is often a lack of exact one-to-one correspondence between the terms in different natural languages. Other approaches apply machine learning techniques [START_REF] Spohr | A machine learning approach to multilingual and cross-lingual ontology matching[END_REF] that usually require large training corpora that are rarely available in an ontology matching scenario.

We present LYAM++ (Yet Another Matcher -Light), a fully automatic crosslingual ontology matching system making use of background knowledge to assist the matching process and to recreate the missing semantic context. Since we focus on the cross-lingual ontology matching problem, we rely on the multilingual semantic network BabelNet 1 , which has the advantages of being openly available, large and general-purpose. Note that an alignment system is composed by a number of components, comprising usually a terminological matcher and a structural matcher, as well as certain filtering and verification modules [START_REF] Ngo | Opening the black box of ontology matching[END_REF]. The background knowledge provided by BabelNet is used in our approach within two of these components. In the first place, it is applied to evaluate the terminological similarities between the names of the ontological elements by reconstituting in a semantically coherent manner the label of a source entity in the language of the target ontology. In the second place, BabelNet is called upon within the structural matching component of the matching procedure. Note that the explicit background knowledge helps to reduce significantly the complexity of the similarity computation algorithms (wherefrom the word "light" in the name of our tool). Another original feature of our approach is the choice of orchestration of the components of the alignment workflow. Our experiments on the MultiFarm 2 benchmark data show that (1) our method outperforms the best cross-lingual matching approaches in the current state-of-the-art and (2) the novel workflow orchestration provides better results compared to the one that is commonly used by the established alignment systems.

In the following section, we focus on the technical aspects of our approach (Section 2). The experiments that have been conducted and their results are discussed afterwards (Section 3), followed by an overview of related approaches (Section 4) and a conclusion (Section 5).

Overview of the Approach

LYAM++ is a matching system specialized in dealing with cross-lingual ontology heterogeneity. LYAM++ makes use of several matching modules of YAM++ (an established and highly-performant tool [START_REF] Ngo | YAM++ : A multi-strategy based approach for ontology matching task[END_REF], also developed by our research group), adding a reference knowledge component that aims to (1) provide the missing semantic context in the matching process and (2) lighten the alignment pipeline used in the original system. Particularly, LYAM++ makes use of the natural language processing module from YAM++ as well as several similarities measures. Indeed, one of our working hypotheses is that background knowledge, when used appropriately, can help to reduce the effort of matcher selection and tuning and can considerably shorten the chain of similarity measures that is commonly applied within the alignment processing workflow [START_REF] Ngo | Opening the black box of ontology matching[END_REF].

The workflow of LYAM++ is shown in Fig. 1. Let S and T be two input ontologies. Our goal is to align the former (source) to the latter (target). Additionally, we assume that S is given in a natural language l S and T -in a language l T . We have chosen BabelNet as a source of background knowledge and our processing pipeline uses two matchers: a multilingual terminological matcher (the main matcher), making use of only two similarity measures, and a structural matcher. In addition, we apply a mapping verification and selection filter.

A Novel Orchestration of the Workflow Components

In the following sections, we will describe each of the components mentioned above in details. Here, we draw the reader's attention to the first original contribution of our approach, which lies in the choice of orchestration of these components (Fig. 1). Note that most of the alignment tools perform terminological and structural matching before mapping selection and verification [START_REF] Ngo | Opening the black box of ontology matching[END_REF]. We reversed this order in an attempt to ensure that we "feed" only good quality mappings to the structural matcher. In that, LYAM++ filters the discovered correspondences right after producing the initial terminological alignment. The viability of this decision is supported experimentally in Section 3.

Preprocessing

As every ontology matching system, LYAM++ transforms the source and the target ontologies before applying the alignment procedure. The first preprocessing step performed by LYAM++ consists in splitting the elements of each ontology into three groups: labels of classes, labels of object properties and labels of data object properties, since these groups of elements are to be aligned separately. The labels of ontological elements are seen as strings of characters. In order to improve the result of comparing two strings, we apply a standard set of preprocessing procedures: normalization of characters and spaces, removing diacritics or accents, deleting numbers, punctuations and stop words, tokenization and lemmatization.

Background Knowledge: BabelNet

As stated above, our system makes use of multilingual background knowledge and our choice has fallen on BabelNet for several reasons. BabelNet is a multilingual semantic network and ontology that has been built by merging different encyclopedic and linguistic resources, such as the English and the multilingual WordNet, Wikipedia, the linked database Wikidata, and the multilingual dictionaries Wiktionary and OmegaWiki. The integration of these resources has been conducted automatically. BabelNet is openly available, large in scale and general-purpose resource, covering 271 languages. For these reasons, it appears to be an appropriate choice of background knowledge for cross-lingual ontology matching, although potentially our system is not restricted to this particular choice and could make use of any other multilingual reference knowledge base.

Terminological Similarity Measures

The main matching component of an alignment system (see following subsection) produces an intermediate alignment based on terminological similarities between the labels by calling on a string-based similarity measure. The ontology matching literature is rich in definitions of measures computing the degree of similarity between two labels. An exhaustive overview can be found in [START_REF] Ngo | Extended tversky similarity for resolving terminological heterogeneities across ontologies[END_REF]. Our system makes use of only two similarity measures -a simple token similarity and a compound label similarity. The former is applied for measuring similarities between single-token strings while the latter is suited for labels composed of several tokens (like for example "Conference Dinner", "ConferenceDinner", "Conference-Dinner"). We will denote by s and t -two labels (strings of characters) to be compared, by s i and t j -tokens belonging to s and t, respectively, and by |s| -the number of tokens in s.

Single-token Similarity Measures. An ontology matching system designer can choose among a large set of single-token similarity measures. Our choice has fallen on the Jaccard coefficient, which is based on the simple idea of estimating the relative overlap of two sets of objects. In our case, two tokens are seen as two strings of characters, s i and t j and the Jaccard coefficient is given as

sim(s i , t j ) = |si∩tj | |si∪tj |
, where the numerator represents the number of common symbols of the two strings and the denominator -the total number of symbols. Note that we have carried out experiments with edit-distance based measures, such as Levenshtein, but we retained the Jaccard coefficient because it showed to perform best in our experiments.

Similarity Measures for Compound Labels. This group of measures is based on first splitting the labels into the tokens that compose them, then applying a simple token similarity function (such as Levenshtein or Jaccard, denoted by sim in the following) internally before evaluating the overall label similarity. Our choice has fallen on three of the most common measures of this type.

(1) The SoftTFIDF measure is defined as a modification of the well-known cosine measure by using the TF/IDF weights [START_REF] Cohen | A comparison of string distance metrics for name-matching tasks[END_REF]. We refer the reader to [START_REF] Ngo | Extended tversky similarity for resolving terminological heterogeneities across ontologies[END_REF] for a formal definition. The TF/IDF weighting scheme is used to measure the relevance of a term with respect to a document and within a given corpus. In an ontology matching scenario, given a label composed by several tokens and an ontology composed of several labels, this scheme is applied by considering a token as a term, a label -as a document and the collection of labels in an ontology -as a corpus.

(2) The Monge-Elkan measure is defined as follows:

M ongeElkan(s, t) = 1 |s| |s| i=1 |t| max i=1 sim(s i , t j )
(3) The Extended Jaccard measure, as its name suggests, is based on the Jaccard similarity [START_REF] Ngo | Extended tversky similarity for resolving terminological heterogeneities across ontologies[END_REF] given as follows:

ExtJaccard(s, t) = | C | | C | + | U niqueT oken(s) | + | U niqueT oken(t) | ,
where token(s) is a function returning the set of tokens composing a string s, C = {(s i , t j )|s i ∈ token(s) ∧ t j ∈ token(t) : sim(s i , t j ) > θ} and U niqueT oken(s) = {s i |s i ∈ token(s) ∧ t j ∈ token(t) ∧ (s i , t j ) / ∈ C}.

Main Multilingual Terminological Matching Using BabelNet

The main matcher is responsible for producing an initial terminological (i.e., based on the labels of the ontology elements) alignment that will be further on improved by the filtering modules and the structural matcher. This matcher uses in its algorithm the tools described in the previous subsections (BabelNet and two similarity measures). The multilingual matching is performed in two steps:

(1) the labels of the source ontology are transformed into the language of the target ontology by using BabelNet and then (2) a monolingual label similarity computation is performed. In this process, two similarity measures are useda simple similarity measure applied on single-token strings (in step 1) and a similarity function applied on compound labels composed by multiple tokens (in step 2). Our main contribution within this matching module lies in (1) a procedure for transforming the source labels into the language of the target ontology by using BebelNet and (2) a method for the semantic expansion of the transformed labels aiming to improve the final similarity values.

Transforming the Source Labels into the Target Language. In order to overpass the cross-lingual barrier, the tokens of the elements of T are transformed and enhanced by the help of BabelNet. At first, every token of a given label s in S is enriched by related terms and synonyms from BabelNet in the language l T , which makes these terms comparable to the tokens of the labels in T . A simple similarity evaluation by the help of the Jaccard coefficient selects the term in each set of related terms corresponding to a given token from s that has the highest score with respect to every token in each label of T . This helps to re-constitute the label s in the language l T . This procedure is presented in Algorithm 1. Finally, the labels in each group of S and T , seen as sets of tokens in the same language (l T ), are compared to one another by using one of the measures described above (Soft TFIDF, Extended Jaccard or Monge-Elkan).

Example. We accompany the algorithm by an example given in Fig. 2. We look at the source label s={"chair of program committee"} given in English and the target label t={"président du comité de programme"}, given in French. After tokenization of s, the function getSources() is called for each of its tokens. This function queries BabelNet and returns a set of terms in the target language (French) related to the token it takes in its argument. In our example, we have -getSources("chair", "EN", "FR")={Chair acrobatics, maître de cérémonie, président, Fixation des rails aux traverses, professeur, fauteuil, Chaise élec trique, plomb, chaise} -getSources("program", "EN", "FR")={Animatrix, logiciel, mission, plan, Programme électoral, programme, programmer} -getSources("committee","EN", "FR")={comité, Committee (comics)}.

The resulting tokens are compared to the tokens of t pairwise by using the Jaccard measure, denoted by sim in the algorithm and in the figure. In order to Algorithm 1 Transforming a label from its source language into a target language by using BabelNet.

Input: s, t: two labels si ∈ s, tj ∈ t: two tokens lS : language of s , lT : language of t sim(si, tj) : a basic token similarity measure (e.g., Jaccard, Levensthein, or other) Output: BabelLabel: the transformed label of s in the language lT , as an outcome of BabelNet 1: for each si ∈ s do 2:

babelsource ← getSources(si, lS, lT ) 3:

for each tj ∈ t do 4:

for each b ∈ babelsource do 5:

score ← sim(b, tj) 6:

if score > maxScore then 7:

maxScore ← score 8:

source ← b 9:

end if 10:

end for 11:

add(BabelLabel, source) 12:

end for 13: end for constitute the French version of the source label s, denoted by s "F R" , we replace each source token by the token returned by getSources that has scored best with respect to the target tokens (in bold in the example above). As a result, the transformed version of the source label takes the form s "F R" = {"président", "programme", "comité"}. The final similarity score between s and t is an outcome of a compound label similarity function, like for example, the SoftTFIDF, computed for the labels s "F R" and t, that are now both in the same language (French, in our example).

Semantically Enhancing the Transformed Source Label Terms. In the case when the final similarity value produced by the softTFIDF measure for a given pair of labels is not satisfactory (i.e., is under a given threshold), Alg. 1 is called again by each of the tokens of the source label in its transformed form (an outcome of Alg.1), this time taking as an argument the token and two times the language l T in order to enhance semantically the input information by looking for more related terms in BabelNet that might be better matching candidates. This process can be called upon as many times as desired, but in order to avoid complexity problems, we have limited the number of these iterations to two.

Example. Let us take a look at the source token s i = "bid", and let l S = "EN " and l T = "F R", where "EN" stands for English and "FR" -for French. In this case, getSources(s i , l S , l T ) = {Prixbid, souhaiter, offre, commande, offrir, Bid-TV, inviter, implorer, appeler}. However, the right term for "bid" is "proposition" and it is not on the list. This results in flawed values of the final similarity Fig. 2: Applying Alg. 1 -a transformation of a source label into the language of a target label by using BabelNet. An example with the token "chair". between the source label, of which "bid" is part and any target label. To make up for that, since the terms in BabelNet are linked, we can map from the term "offre" to the term "proposition" by applying getSources("offre", l T , l T ).

Unlike most matching systems, which translate the labels of source and target ontology into English, LYAM++ transforms the labels of S from the language of S into the language of T . Note again that only one similarity measure is used on label level and one -on token level, which makes LYAM++ a light-weight ontology matching system.

Mapping Verification and Mapping Selection

The mapping verification step aims to remove correspondences that are less likely to be satisfiable based on the information present in the ontologies. This component filters out the trustworthy pairs of aligned concepts by looking at the similarity values produced for their parents and their children in the ontology hierarchies.

In an ontology matching system, mapping selection is an important task used as a filter to select high quality mapping candidates before producing the final alignment. This module transforms the initial 1 to many alignment (a source element possibly corresponding to multiple target elements) to a 1:1 alignment (a source element corresponds to exactly one target element) based on the principle of iteratively retaining the pairs of concepts with maximal value of similarity.

Structural Matching with BabelNet

Structural methods exploit the relations between entities, relying often on the hierarchical structure of the ontologies defined by the subsumption relation.

The basic idea is that if two entities are similar, their "relatives" could also be in one way or another similar. Two entities are considered similar if either of the following heuristics is true: (i) their direct super-entities (or all super-entities) are similar, (ii) all their sisters, who are the entities with the same super entity directly with the entities in question are similar, (iii) all of their sub-entities are similar, (iv) their descendants are similar, (v) all their leaves are similar.

In order to cope with the cross-lingual character of the input ontologies in the process of structural matching, we call upon BabelNet again. Note that the structural information is language independent, but a similarity measure is needed to verify the heuristics given above, and this similarity measure is most commonly language dependent, since it is based on similarity of strings. Our cross-lingual structural matching procedure is presented in Algorithm 2. Similarly to Algorithm 1, we query BabelNet to construct language transformations of the labels of the source ontology. Before computing similarity between the transformed source labels and the labels of the target ontology we check their structural information using the M atchExist() function. The function GetStructure() returns all structural information of an entity such as its super-entities and sub-entities. M atchExist() returns true if any structural informations of the two entities are similar. It reduces the number comparisons between entities and thus optimizes considerably the matching process.

Algorithm 2 Structural matching with BabelNet

Input: e1, e2: two entities s: label of e1, t: label of e2 si ∈ s, tj ∈ t: tow tokens -lS : language of s , lT : language of t Output: BabelLabel: outcome of BabelNet We have evaluated LYAM++ on data coming from the ontology alignment evaluation initiative (OAEI)3 of year 2014 and particularly Multifarm-a benchmark designed for evaluating cross-lingual ontology matching systems. Multifarm data consist of a set of 7 ontologies originally coming from the Conference benchmark of OAEI, translated into 8 languages. Two evaluation tasks are defined: task 1 consists in matching two different ontologies given in different languages, while task 2 aims to align different language versions of one single ontology.

We used the Alignment API4 in order to compute precision, recall, and Fmeasures. We use BabelNet 3.0 API to query online BabelNet.

We have performed experiments on both tasks by using several MultiFarm datasets (the ontologies CMT, conference, confOf, iasted and sigkdd). We have conducted three experiments. In the first one, we compare LYAM++ to Agreement Maker Light (AML) [START_REF] Faria | The agreementmakerlight ontology matching system[END_REF] on both tasks and all pairs of languages. The choice of AML is motivated by the fact that, according to the reports of the OAEI 2014, this system performs best on the Multifarm track. In the second experiment, we evaluate the standard orchestration of the ontology matching workflow and the novel orchestration proposed in this paper. Finally, the third experiment compares the resuts obtained by each of the three similarity measures introduced in the previous section (TF/IDF, Extended Jaccard and Monge-Elkan) and shows that the performance of LYAM++ does not depend on the choice of measure, but is due to the use of background knowledge and the novel orchestration of the matching workflow.

Comparing LYAM++ to AML

The mapping threshold determines the value of the similarity function, above with a pair of labels can be considered as a potential mapping. It can also be seen as a confidence value of the produced alignment -the higher the mapping threshold, the more conservative we are in filtering out mappings and therefore the more confident we are in the final result. The F-measure depends strongly on this value and therefore, commonly, ontology matching results are presented in the form of an F-measure curve as a function of the mapping threshold.

Within this experiment, the SoftTFIDF similarity measure has been used to produce the initial terminological similarities. The Jaccard coefficient has been applied for the source label reconstitution in the target language (the measure sim within Alg. 1).

Table 1 shows the average F-measures over all threshold values per language pair for tasks 1 and 2. As it can be seen, LYAM++ outperforms AML systematically for all pairs of languages on both tasks, even for more difficult to handle languages like Russian. The high average F-measure values over all threshold values provide evidence of the stability of LYAM++ in terms of confidence value. Fig. 3: Average F-measures over all language pairs per threshold value and task.

Figure 3 shows the average F-measures over all language-pairs per threshold value and task. On task 1, both systems have similar and stable behavior for threshold values lower than 0.8. When this value is surpassed, however, one can see a clear advantage of LYAM++, which remains on more or less the same F-measure level, while the performance of AML drastically decreases reaching almost a 0 F-measure for a threshold values close to 1.

On task 2, the divergence in the performance of the two systems is observed at a much lower value-0.4-of the mapping threshold. For threshold values greater than 0.4, the values of the F-measure for AML start to decrease while LYAM++ remains stable until the threshold value reaches 0.8.

We explain the good results of our system by the appropriate use of a specific background knowledge source (BabelNet), particularly suited for cross-lingual ontology matching, as well as by the novel composition of the matching modules (see results of the experiment in the following subsection). We underline the fact that LYAM++ remains stable and outperforms AML for even high threshold values (close to or equaling 1), which demonstrates the capacity of the system to produce quality cross-lingual alignments with a very high level of confidence. Fig. 4: Average F-measures over all language-pairs per threshold value of task 2 for the novel and the standard orchestrations.

Comparing the Standard and the Novel Orchestrations

This experiment aims to demonstrate the advantage of the novel orchestration of the components within the matching workflow as compared to the standard one. Again, the two similarity measures that are used are SoftTFIDF for the intermediate terminological alignment and Jaccard for the label reconstitution (Alg. 1). Following the same presentation pattern as the one in the subsection above, Table 2 shows the average F-measures over all threshold values per language pair, while Figure 4 shows the average F-measures over all language-pairs per threshold value. We have presented the results on task 2 only for reasons of space limitation. Similar results were obtained on task 1.

As we can see, the novel orchestration largely outperforms the classical one. This is due to the fact that the mappings resulting from the mapping selection module have high precision and these mappings are passed to the structural matcher, responsible for the final alignment.

Impact of the Choice of Similarity Measure

This experiment evaluates the impact of the choice of a similarity measure for comparing compound labels on the quality of the alignment produced with LYAM++. Fig. 5 shows the average F-measures over all language-pairs per threshold value again for task 2. It can be seen that the F-measures obtained by the three evaluated similarity measures are not significantly different and are all of good quality. This comes to show that our system is robust to the choice of similarity measure, its high performance being mainly due to the novel orchestration and the use of suitable background knowledge in the alignment process.

Related work

The current section introduces related approaches to ontology matching with regard to two aspects: (1) the use of background knowledge and (2) handling cross-lingual heterogeneity.

Ontology Matching Using Background Knowledge

Using background knowledge (BK) for enhancing ontology matching is an idea that has been realized in several matching approaches in the literature. Sabou et al. [START_REF] Sabou | Exploring the semantic web as background knowledge for ontology matching[END_REF] motivate the use of BK by the observation that two ontologies are always inherently different in terms of intention. Background knowledge comes to bridge the inherent semantic gap between them. We provide an overview of some of the relevant groups of techniques, categorized in terms of the type of background knowledge that is used, following the introduction found in [START_REF] Shvaiko | Ontology matching: state of the art and future challenges[END_REF].

Reusing existing mappings. Stored mappings can be used to discover new ones. Several approaches [START_REF] Do | COMA -A system for flexible combination of schema matching approaches[END_REF][START_REF] Groß | GOMMA results for OAEI 2012[END_REF][START_REF] Saha | Schema covering: a step towards enabling reuse in information integration[END_REF] follow this paradigm by reusing existing mappings to efficiently match two ontologies. The weak point of this group of approaches is the fact that they depend heavily on the quality of the re-used mappings, therefore on the performance of the ontology matching techniques that have been used to produce the initial mappings.

Using domain specific corpus. A corpus can be seen as a collection of elements (e.g., relation and attribute names) and their data types, relationships between elements, sample data instances, and other knowledge that can be used to discover mappings between entities [START_REF] Madhavan | Corpusbased schema matching[END_REF][START_REF] Madhavan | Corpus-based schema matching[END_REF]. Since a corpus is specific to a domain, it can only be used in specific matching cases. For example, a corpus in the field of anatomy can only be used for matching anatomy ontologies.

Using domain specific ontologies. Domain specific ontologies are often seen as quality sources of background knowledge. In [START_REF] Aleksovski | Matching unstructured vocabularies using a background ontology[END_REF][START_REF] Aleksovski | Exploiting the structure of background knowledge used in ontology matching[END_REF], the alignment process takes place in two steps: anchoring and driving relations. Anchoring consists in matching the concepts of the source and target ontologies to the concepts of the reference knowledge using standard ontology matching techniques. In this step, each concept from the source and the target ontologies is mapped, or anchored, to a concept from the reference ontology. Driving relations is the process of finding relations between source and target concepts by checking if their corresponding anchored concepts are related.

Using the semantic web. This group of approaches is based on harvesting the semantic web in order to discover and explore multiple heterogeneous on-line knowledge sources [START_REF] Sabou | Exploring the semantic web as background knowledge for ontology matching[END_REF]. The originality of the proposal is the use of the web in order to discover (by crawling) automatically appropriate BK sources (instead of using a single fixed source). Thus, the question of the availability and the coverage of the BK is addressed. This is particularly useful when the needed background knowledge is spread among different available sources.

Discussion. Due to the nature of the background knowledge that is used in our system, it is difficult to situate our approach in one of these families. Indeed, BabelNet can be seen as a corpus of existing mappings, since the terms are related semantically, but it can be also seen as an ontology. In contrast to the cited approaches, in our case the BK is used to enrich the semantic information contained in the source ontology in order to make it more "compatible" and easer to compare to the target ontology.

Cross-Lingual Ontology Matching

Gracia et al. [START_REF] Gracia | Challenges to the multilingual web of data[END_REF] present a global vision of a multilingual semantic web together with several challenges to the multilingual semantic web community. According to the authors, multilingualism has to be seen as an extension of the semantic web-a group of techniques which will be added to the existing semantic technologies in order to resolve linguistic heterogeneity where it appears. The semantic web is seen as language-independent, because semantic information is given in formal languages. The main gap is, therefore, between language specific needs of users and the language-independent semantic content. The authors prognosticate that monolingual non-English linked data will increase in years creating "islands" of unconnected monolingual linked data. The challenge is to connect these islands by interconnecting the language-specific information. The authors outline the development of systems for establishing relations between ontology terms or semantic data with labels and instances in different languages as a main direction of future research. We proceed to discuss different crosslingual approaches grouped in four main categories depending on the underlying technique.

Machine translation (MT). The majority of approaches rely on MT techniques. Fu et al. [START_REF] Fu | Cross-lingual ontology mapping-an investigation of the impact of machine translation[END_REF] follow a standard paradigm of using monolingual matching techniques enhanced with an MT module. As a result of an analysis of the effect of the quality of the MT, the authors propose a noise-minimization method to reduce the flaw in the performance introduced by the translation. Trojahn et al. [START_REF] Santos | An api for multi-lingual ontology matching[END_REF] have implemented an API for multilingual OM applying two strategies: a direct matching by a direct translation of one ontology to the other prior to the matching process and indirect matching, based on a composition of alignments. The latter approach is originally proposed by Jung et al. [START_REF] Jung | Indirect alignment between multilingual ontologies: A case study of korean and swedish ontologies[END_REF] and it is based on first establishing manual alignment between cross-lingual ontologies and then using these alignments in order to infer new ones. Paulheim et al. [START_REF] Paulheim | Wesee-match results for oaei 2013[END_REF] apply web-search-based techniques for computing concept similarities by using MT for cross-lingual ontologies. Several well-established ontology matching systems propose to take cross-lingual ontologies as input by using machine translation in the alignment process, two of them being YAM++ [START_REF] Ngo | YAM++ : A multi-strategy based approach for ontology matching task[END_REF] and AML [START_REF] Faria | The agreementmakerlight ontology matching system[END_REF].

Machine learning (ML). Spohr et al. [START_REF] Spohr | A machine learning approach to multilingual and cross-lingual ontology matching[END_REF] present an approach applying ML techniques. They use a small amount of manually produced cross-lingual alignments in order to learn a matching function for two cross-lingual ontologies. The paper introduces a clear distinction between a multilingual ontology (that which contains annotations given in different languages) and cross-lingual ontologies (two or more monolingual ontologies given in different natural languages).

Use of background knowledge. On the edge of the OM approaches that use background knowledge, Rinser et al. [START_REF] Rinser | Cross-lingual entity matching and infobox alignment in wikipedia[END_REF] propose a method for entity matching by using the info-boxes of Wikipedia. Entities given in different languages are aligned by the help of the explicit relations between Wikipedia pages in different languages. The matching relies mainly on the values of each property, since the actual labels are in different languages (e.g., "population" and "Einwohner" have approximately the same values (3,4M) in the info-boxes of the English and the German Wikipedia pages of Berlin). A very important and useful contribution of this paper is an analysis of the structure of the Wikipedia interlanguage links. Todorov et al. [23] [24] propose an ontology alignment framework based on background knowledge (the multilingual YAGO ontology) and fuzzy sets and logics to deal with imprecision in the cross-lingual matching process.

Natural language processing (NLP). Outside of the context of ontology matching, in the NLP field, research has been carried on the topic of measuring semantic distance between cross-lingual terms or concept labels. Mohammad et al. [START_REF] Mohammad | Cross-lingual distributional profiles of concepts for measuring semantic distance[END_REF] and Eger et al. [START_REF] Eger | Computing semantic similarity from bilingual dictionaries[END_REF] propose measures of semantic distance between cross-lingual concept labels based on the use of bilingual lexicons. Explicit Semantic Analysis (ESA) applied with Wikipedia has been proposed as a framework for measuring cross-lingual semantic relatedness of terms, first in a paper by Gabrilovich et al. [START_REF] Gabrilovich | Computing semantic relatedness using wikipedia-based esa[END_REF] and then in an extended proposal by Hassan et al. [START_REF] Hassan | Cross-lingual semantic relatedness using encyclopedic knowledge[END_REF]. It is suggested to rely on the multiple language versions of Wikipedia in order to measure semantic relatedness between terms. The authors use an ESA framework in order to model a concept as a vector in a space defined by a set of "encyclopedic concepts" in which the concept appears.

Discussion. The methods that have been proposed to deal with multilingualism in ontology matching, with few exceptions, rely on automatic translation of labels to a single target language. As noted in the introduction, MT tolerates low precision levels and often external sources are needed in order to achieve good performance. An inherent problem of translation as such is that there is often a lack of exact one-to-one correspondence between the terms across natural languages. Our approach is therefore closer in spirit to the approaches comping the NLP domain, the main idea being to use a bilingual reference vocabulary in order to link related terms across languages.

Conclusion

The moment to pay attention to cross-lingual ontology matching appears to be appropriate for several reasons. On the one hand, an important factor is the historical moment of the development of the Web community. As mentioned at the start, although originally predominantly English-speaking the Web, and consequently the Semantic Web, has the tendency of comprising more and more non-English active users, i.e., users that both consume and create Web content in languages other than English. In the current state of affairs there is only little above 30 percent of English Internet users 5 and the number of other language speaking users is constantly growing. In order to fully unlock the potential of the Web of Data project, the web community needs to be provided tools for the automatic integration of web knowledge-vocabularies and data-given in different natural languages.

In this paper, we have addressed this problem by proposing a novel crossontology matching approach implemented in the system LYAM++. In order to make up for the disadvantages of the currently existing cross-lingual matching systems, we do not rely on machine translation, but make use of background knowledge in the form of a large multilingual lexical network (BabelNet). In addition, we have proposed a novel orchestration of the matching components that form the ontology matching processing pipeline. We have shown experimentally by using data from the Multifarm benchmark, that our matching technique outperforms the best systems in the current state-of-the-art and that the novel workflow orchestration provides better results than the standard one.

In the future, we plan to explore the use of different kinds of background knowledge and the impact of this choice on the matching task. We will also apply our technique to the monolingual matching problem by exploiting the rich semantic information contained in a background knowledge source.

Fig. 1 :

 1 Fig. 1: The processing pipeline of LYAM++.

  FR-PT FR-NL ES-FR ES-RU ES-PT ES-NL EN-PT EN-RU EN-FR LYAM++ 0measures over all threshold values per language pair for task 2. (a) Task 1 (b) Task 2

Fig. 5 :

 5 Fig. 5: Comparing the similarities measures.

Table 1 :

 1 Comparing LYAM++ to AML

	Lang.	FR-RU FR-PT FR-NL ES-FR ES-RU ES-PT ES-NL EN-PT EN-RU EN-FR
	pair
	LYAM++ 0.54	0.58	0.62	0.60	0.60	0.60 0.63	0.67	0.53	0.59
	AML	0.48	0.51	0.47	0.53	0.47	0.51 0.52	0.53	0.51	0.49
	Average F-measures over all threshold values per language pair for task 1.

Table 2 :

 2 Comparing the standard and the novel orchestrations Langauge pair FR-RU FR-PT FR-NL ES-FR ES-RU ES-PT ES-NL EN-PT EN-RU EN-FR

	Novel	0.58	0.72	0.67	0.77	0.64	0.70 0.68	0.74	0.59	0.85
	Standard 0.50	0.58	0.60	0.39	0.54	0.57 0.58	0.50	0.32	0.39
	Average F-measures over all threshold values per language pair for task 2.

http://oaei.ontologymatching.org/

http://alignapi.gforge.inria.fr/

http://www.internetworldstats.com/

Acknowledgment

This work has been partially supported by the French National Research Agency (ANR) within the DOREMUS Project, under grant number ANR-14-CE24-0020 and the Ministry of Higher Education and Research of Algeria.


Abdel Nasser Tigrine

Zohra Bellahsene

Konstantin Todorov

Lyam++

LYAM++ Results for OAEI 2015

Presentation of the System

In spite of the considerable advance that has been made in the field of ontology matching recently, many questions remain open [START_REF] Shvaiko | Ontology matching: state of the art and future challenges[END_REF]. The current work addresses the challenge of using background knowledge with a focus on aligning cross-lingual ontologies, i.e., ontologies defined in different natural languages [START_REF] Spohr | A machine learning approach to multilingual and cross-lingual ontology matching[END_REF].

Indeed, considering multilingual and cross-lingual information is becoming more and more important, in view particularly of the growing number of web content-creating non-English users and the clear demand of cross-language interoperability. In the context of the web of data, it is important to propose procedures for linking vocabularies across natural languages, in order to foster the creation of a veritable global information network.

The use of different natural languages in the concepts and relations labeling process is becoming an important source of ontology heterogeneity. The methods that have been proposed to deal with it most commonly rely on automatic translation of labels to a single target language [START_REF] Faria | The agreementmakerlight ontology matching system[END_REF] or apply machine learning techniques [START_REF] Spohr | A machine learning approach to multilingual and cross-lingual ontology matching[END_REF]. However, machine translation tolerates low precision levels and machine learning methods require large training corpus that is rarely available in an ontology matching scenario. An inherent problem of translation is that there is often a lack of exact one-to-one correspondence between the terms in different natural languages.

State, Purpose, General Statement

We present LYAM++ (Yet Another Matcher -Light) [START_REF] Tigrine | Light-weight cross-lingual ontology matching with LYAM++[END_REF], a fully automatic cross-lingual ontology matching system that does not rely on machine translation. Instead, we make use of the openly available general-purpose multilingual semantic network BabelNet1 in order to recreate the missing semantic context in the matching process. Another original feature of our approach is the choice of orchestration of the matching workflow. Our experiments on the MultiFarm2 benchmark data show that (1) our method outperforms the best approaches in the current state-of-the-art and (2) the novel workflow orchestration provides better results compared to the classical one. We refer the reader to the results reported in [START_REF] Tigrine | Light-weight cross-lingual ontology matching with LYAM++[END_REF].

Specific Techniques Used

The workflow of LYAM++ is given in Fig. 1. We take as an input a source ontology S, given in a natural language l S and a target ontology T , given in a language l T . The overall process consists of four main components: a terminological multilingual matcher, a mapping selection module and, finally, a structural matcher. One of the original contributions of this work is the choice of orchestration of these components. Indeed, the places of the mapping selection module and the structural matcher are reversed in the existing OM tools [START_REF] Ngo | Opening the black box of ontology matching[END_REF]. However, we wanted to ensure that we feed only good quality mappings to the structural matcher, therefore we decided to filter the discovered correspondences right after producing the initial alignment. This decision is supported experimentally in the following section.

The multilingual terminological matching module, the second contribution described in this paper, acts on the one hand as a preprocessing component and, on the other hand -as a light-weight terminological matcher between crosslingual labels. We start by splitting the elements of each ontology in three groups: labels of classes, labels of object properties and labels of data object properties (in colors blue, black and red in the figure), since these groups of elements are to be aligned separately. A standard preprocessing procedure is applied on these sets of labels, comprising character normalization, stop-words filtering, tokenization and lemmatization. The tokens of the elements of T are then aligned to BabelNet. At first, every token of a given label s in S is enriched by related terms and synonyms from BabelNet and all of these terms are represented in the language l T , which makes these terms comparable to the tokens of the labels in T . A simple similarity evaluation by the help of the Jaccard coefficient selects the term in each set of related terms corresponding to a given token from s that has the highest score with respect to every token in each label of T . This helps to restitute the label s in the language l T . Finally, the labels in each group of S and T , seen as sets of tokens, are compared by using the Soft TFIDF similarity measure [START_REF] Cohen | A comparison of string distance metrics for name-matching tasks[END_REF], which produces an intermediate terminological alignment.

The three remaining components are standard OM modules [START_REF] Ngo | Opening the black box of ontology matching[END_REF], although ordered in a new manner. The Mapping selection is a module that transforms the initial 1 to many mapping to a 1:1 mapping based on the principle of iteratively retaining the pairs of concepts with maximal value of similarity. Finally, the structural matcher component filters the trustworthy pairs of aligned concepts by looking at the similarity values produced for their parents and their children in the ontology hierarchies.

Links to the System and to the Set of Provided Alignments

The system is not yet available online because it depends heavily on the use of BabelNet, which is under a non-free licence. We are working on implementing a sharable version of LYAM++ making use of different open access background knowledge sources, such as YAGO.

The alignments produced by LYAM++ for this year's Multifarm track can be found under the following link: http://www.lirmm.fr/benellefi/Lyam++.rar

Results

We have evaluated our approach on data coming from the ontology alignment evaluation initiative (OAEI) 3 and particularly Multifarm-a benchmark designed for evaluating cross-lingual ontology matching systems. Multifarm data consist of a set of 7 ontologies originally coming from the Conference benchmark of OAEI, translated into 8 languages. Two evaluation tasks are defined: task 1 consists in matching two different ontologies given in different languages, while task 2 aims to align different language versions of one single ontology.

We have performed experiments on both tasks by using the pairs of languages given in the summary of our results in Table 1.

In another experiment, we have evaluated the results obtained by using our novel orchestration of matching components, as compared to the standard orchestration. The figures in Table 2 show that the workflow proposed in this paper acts in favor of achieving better results as compared to the standard method.

Table 3 presents the results obtained by LYAM++ on this year's Multifarm evaluation campaign. What we see is the average F-measure value for all Table 1: Results of LYAM++ on the Multifarm datesets. language-pairs without any threshold on the confidence measure. The value in the parenthesis corresponds to the average F-measure value for the generated alignments only (the pairs of languages that the system handles). Note that at this stage, LYAM++ is not able to generate alignments for all language-pairs because of query constraints related to the use of BabelNet, which is under non-free license. The table compares LYAM++ to the top 3 systems this year (LYAM++ excluded). We see that with respect to the languages that our system can handle, it scores second, little behind AML, on task 1 and first on task 2.

Possible Improvements of the System

Currently, we are working on enhancing the system in order to make it applicable to the general ontology matching problem and not only to the cross-lingual one. We have generated first results on the Conference benchmark without any modification in the settings and our results are promising. For the majority of the datasets (ontology pairs) our system achieves a F-score almost as good as the F-score of AML, the best performing system on that track.

We consider that a key feature for the improvement of our system is the appropriate choice of background knowledge. In order to improve the results achieved on the Conference track, we plan to use monolingual general purpose background knowledge (for example, the english subgraphs of YAGO or DBPedia) instead of BabelNet.

We intend to use domain specific background knowledge in order to solve alignment problems in specific areas of knowledge. More precisely, we plan to participate on the Anatomy track by testing different kinds of domain specific background knowledge, such as UMLS or other.

Conclusion

We presented an efficient approach for aligning cross-lingual ontologies by using the multilingual lexical database BabelNet. Subjects of ongoing and future work are (1) testing and evaluating different sources of external knowledge, (2) applying the approach to a larger set of languages, (3) adaptation of the approach to the monolingual case and studying the use of background knowledge in a monolingual ontology matching scenario.

Fig. 1 :

 1 Fig. 1: The processing pipeline of LYAM++.

  FR-PT FR-NL ES-FR ES-RU ES-PT ES-NL EN-PT EN-RU EN-FR LYAM++ 0measures over all threshold values per language pair for task 1.

  FR-PT FR-NL ES-FR ES-RU ES-PT ES-NL EN-PT EN-RU EN-FR LYAM++ 0measures over all threshold values per language pair for task 2.

Table 2 :

 2 Comparing the standard and the novel orchestrations

	Langauge	FR-RU FR-PT FR-NL ES-FR ES-RU ES-PT ES-NL EN-PT EN-RU EN-FR
	pair
	Novel	0.58	0.72	0.67 0.77 0.64 0.70 0.68	0.74	0.59	0.85
	Standard 0.50	0.58	0.60 0.39 0.54 0.57 0.58	0.50	0.32	0.39
	Average F-measures over all threshold values per language pair for task 2.

Table 3 :

 3 Results of LYAM++ for Multifarm 2015.

		Task1	Task2
	LYAM++	0.14(0.49) 0.19(0.66)
	AML	0.51(0.51) 0.64(0.64)
	LogMap	0.41(0.41) 0.45(0.45)
	CLONA	0.39(0.39) 0.58(0.58)

http://babelnet.org/

http://web.informatik.uni-mannheim.de/multifarm/

http://oaei.ontologymatching.org/