Béatrice Bérard

Olga Kouchnarenko

John Mullins

Mathieu Sassolas

Opacity for Linear Constraint Markov Chains

On a partially observed system, a secret ϕ is opaque if an observer cannot ascertain that its trace belongs to ϕ. We consider specifications given as Constraint Markov Chains (CMC), which are underspecified Markov chains where probabilities on edges are required to belong to some set. The nondeterminism is resolved by a scheduler, and opacity on this model is defined as a worst case measure over all implementations obtained by scheduling. This measures the information obtained by a passive observer when the system is controlled by the smartest scheduler in coalition with the observer. When restricting to the subclass of Linear CMC, we compute (or approximate) this measure and prove that refinement of a specification can only improve opacity.

Introduction

Context and motivation. When modeling complex systems, a top-down approach allows gradually specifying various system requirements, while preserving some behavioral properties, like safety, reachability, and liveness under some conditions.

Security requirements, which are not behavioral ones [START_REF] Clarkson | Hyperproperties[END_REF], may not fare well under refinement, unless tailored specially to do so, as in [START_REF] Alur | Preserving secrecy under refinement[END_REF]. Several known security properties such as noninference or anonymity can be encoded in the framework of opacity [START_REF] Mazaré | Decidability of opacity with non-atomic keys[END_REF][START_REF] Bryans | Opacity generalised to transition systems[END_REF][START_REF] Alur | Preserving secrecy under refinement[END_REF]. In this context, an external observer tries to discover whether a predicate (given as an ω-regular set) holds by partially observing the system through a projection of its actions.

A system is opaque if the attacker fails to discover this information. In the possibilistic setting, a violation of opacity captures the existence of at least one perfect leak.

In probabilistic models like Discrete Time Markov Chains (DTMCs), naturally random events such as faults or message transmission failure, can be taken into account. Opacity was extended in this setting [START_REF] Saboori | Current-state opacity formulations in probabilistic finite automata[END_REF][START_REF] Bérard | Quantifying opacity[END_REF][START_REF] Bérard | Probabilistic Opacity for Markov decision processes[END_REF] to provide various measures of what is disclosed by observation.

Consider for instance the two systems in Fig. 1(a)-(b), which are DTMCs with the addition of labels on states (indicated inside). We assume that the occurrence of b must be kept secret and that all labels except b are observable. In this case, the only runs disclosing the secret are those observed by ad ω , since every such run betrays the occurrence of b. The probability of disclosure is 1/4 in A 1 while it is 3/4 in A 2 , hence A 1 is more secure than A 2 . Our aim is to establish sufficient conditions on systems like A 1 and A 2 , that can be compared, for one of them to be more secure than the other.

In the process of system modeling, it is common practice to use underspecified models as first steps of specification. A first approach is to con- sider sub-stochastic models where transition probabilities need not sum up to 1. In this framework, the notions of satisfaction and simulation were extensively studied in [START_REF] Baier | Comparative branching-time semantics for Markov chains[END_REF]. The second approach is to introduce nondeterminism in the model to describe environment choices [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF][START_REF] Chatterjee | Model-checking omega-regular properties of interval Markov chains[END_REF][START_REF] Caillaud | Constraint Markov chains[END_REF][START_REF] Benedikt | LTL model checking of interval Markov chains[END_REF][START_REF] Bérard | Probabilistic Opacity for Markov decision processes[END_REF][START_REF] Delahaye | Consistency for parametric interval Markov chains[END_REF]. These models have also been studied in relation to the refinement process [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], with the particular case of Interval Markov Chains (IMCs) where the transitions are equipped with probability bounds in the form of intervals, as done in Fig. 1(c). For example, both systems of Fig. 1(a)-(b) could have been derived from the single underspecified system S of Fig. 1(c), with the same structure but imprecise probabilities. Unfortunately, while closure under conjunction is a nice feature for specification formalisms, IMCs do not have this property. This is shown in [START_REF] Caillaud | Constraint Markov chains[END_REF], where Constraint Markov Chains (CMCs), first introduced in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], are considered for the specification of finite state processes, and proved to provide a more robust model. In a CMC, the family of intervals associated with a state is replaced by a given (possibly infinite) set of distributions.

[ 1 8 , 8 9 ] [ 1 8 , 2 3 ] [ 1 9 , 1 3 ] [1, 1] [1, 1] [1, 1] [1, 1] [1, 1] (c) S
Scheduling is an effective way to obtain implementations of a CMC: at each step, a scheduler provides a distribution belonging to the given set, thus producing a (possibly infinite) DTMC on-the-fly. In the case of opacity, a scheduler represents a strategy of an agent inside the system, trying to disclose as much information as possible to a passive observer. Several works used schedulers to evaluate disclosure: [START_REF] Bérard | Probabilistic Opacity for Markov decision processes[END_REF] in the context of (fully specified) Markov Decision Processes and [START_REF] Bérard | Preserving opacity on interval Markov chains under simulation[END_REF] for IMCs.

Contributions. We extend the latter work, investigating opacity for CMCs. As before, disclosure is defined in the worst case scenario, as the supremum of the disclosure for all scheduled implementations. This measures the information obtained by a passive observer when the system is controlled by the smartest scheduler in coalition with the observer.

However, without an explicit description of the given probability sets, algorithmic questions cannot be solved on CMCs. Therefore, we consider here a subclass called Linear Constraint Markov Chains (LCMCs), where the set of distributions associated with a state is defined by linear inequalities. This class is closed under conjunction and contains IMCs.

We first show how to compute the disclosure for a subclass of LCMCs, where no transition can be completely blocked by the scheduler. In the general case, we give an overapproximation for bounded memory schedulers. We then establish monotonicity of the disclosure for LCMCs: refining an LCMC can only improve the opacity of all implementations obtained by scheduling.

Organization of the paper. After short preliminaries on probabilistic transition systems and opacity (Section 2), we recall in Section 3 the background on Constraint Markov Chains, with the associated refinement relations, and we define probabilistic disclosure in this contex. We show how to compute this measure for a restricted case of LCMCs in Section 4, with an approximation scheme for the general case. Finally, we prove monotonicity of opacity under refinement in Section 5.

Probabilistic transition systems and opacity

The set of natural numbers is denoted by N and the set of rational numbers by Q. The composition of relations R 2 and R 1 is defined by

R 2 • R 1 = {(x, z) | ∃y, (x, y) ∈ R 1 ∧ (y, z) ∈ R 2 }.
Given a finite alphabet Σ, we denote by Σ * (resp. Σ ω ) the set of finite (resp. infinite) words over Σ, with Σ ∞ = Σ * ∪ Σ ω and ε the empty word. We denote by |w| the length of word w in N ∪ {+∞} with the same notation |E| for the cardinality of a set E.

Given a countable set Z, a discrete distribution is a mapping µ :

Z → [0, 1] such that z∈Z µ(z) = 1. The support of µ is supp(µ) = {z ∈ Z | µ(z) > 0}.
The set of all discrete distributions on Z is denoted by Dist(Z). When dealing with a joint distribution µ on domain

Z 1 × Z 2 , we write µ(Y 1 , Y 2 ) = y 1 ∈Y 1 ,y 2 ∈Y 2 µ(y 1 , y 2 ) for Y 1 ⊆ Z 1 and Y 2 ⊆ Z 2 ,

Probabilistic Labelled Transition Systems and their languages

The secret to be protected from disclosure is described by a Deterministic Parity Automaton (DPA, see example in Fig. 2). Implementations are given by Probabilistic Transition Systems (PTSs). They are classical Discrete Time Markov Chains, with the addition of state labeling [START_REF] Baier | Comparative branching-time semantics for Markov chains[END_REF], restricting the processes of [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] with a countable set of states.

Definition 2.1 (Deterministic Parity Automaton).

A deterministic parity automaton (DPA) over finite alphabet Σ is a tuple A = (Q, q 0 , θ, F ), where Q is a finite set of states, q 0 ∈ Q is an initial state, θ : Q × Σ → Q is a transition function, and F is a mapping from Q to a finite set of colors {1, . . . , k}.

A run of A on a word w = a 1 a 2 • • • ∈ Σ ω is an infinite sequence ρ = q 0 q 1 • • • ∈ Q ω such that for all i ≥ 0, q i+1 = θ(q i , a i+1 ). For such a q0 q1 q2 a b Σ Fig. 2. A DPA for ϕ b = abΣ ω with F (q 0 ) = F (q 2 ) = 1 and F (q 2 ) = 2.
run ρ, we define Inf(ρ) as the set of states appearing infinitely often in the sequence. The run is accepting if min{F (q) | q ∈ Inf(ρ)} is even. In this case, the corresponding word is accepted by A and L(A) is the subset of Σ ω of words accepted by A. A subset K of Σ ω is ω-regular if there is an automaton A such that K = L(A).

Definition 2.2 (Probabilistic Transition Systems

). A probabilistic transition system (PTS) over alphabet Σ is a tuple A = (Q, q init , ∆, L)
where Q is a countable set of states, with q init ∈ Q the initial state, ∆ : Q → Dist(Q) is a mapping associating with any state q ∈ Q a distribution ∆(q) over Q, with finite support, and L : Q → Σ is the labeling function on states.

PTSs can be seen as Discrete Time Markov Chains where the states are equipped with labels in Σ. While our presentation uses an alphabet Σ of labels for simplicity, it is always possible as done in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Caillaud | Constraint Markov chains[END_REF] to consider the case where Σ = 2 A for a set A of atomic propositions.

A (finite or infinite) run of A starting from state q ∈ Q is a sequence of states ρ = q 0 q 1 q 2 . . . such that q 0 = q and for each i, 0 ≤ i < |ρ|, ∆(q i )(q i+1 ) > 0. When the run is finite ρ = q 0 q 1 . . . q n , we note q n = lst(ρ). The trace of ρ is the word tr(ρ) = L(q 0 )L(q 1 ) . . . ∈ Σ ∞ . We denote by Runs q (A) the set of infinite runs starting from q and we set Runs(A) = Runs q init (A), and Tr(A) = {tr(ρ) | ρ ∈ Runs(A)}, the set of traces of A. We also define FRuns q (A) the set of finite runs starting from q, and similarly FRuns(A) = FRuns q init (A) and FTr(A) = {tr(ρ) | ρ ∈ FRuns(A)}, the subset of Σ * of finite traces of A.

Recall [START_REF] Billingsley | Probability and Measure[END_REF] that a probability measure P A can be defined on Runs(A): measurable sets are generated by cones, where the cone C ρ associated with a finite run ρ = q 0 q 1 . . . q n is the subset of infinite runs in Runs(A) having ρ as prefix. The probability of C ρ is P A (C ρ ) = n-1 i=0 ∆(q i )(q i+1 ). The cone of a word w ∈ Σ * is defined by C w = ρ∈tr -1 (w) C ρ .

Probabilistic Opacity

The original definition of opacity was given in [START_REF] Bryans | Opacity generalised to transition systems[END_REF] for (non probabilistic) transition systems, w.r.t. some observation function O and some predicate ϕ (the secret) on the runs of the system.

For an ω-regular set ϕ ⊆ Σ ω , a run ρ of a PTS A satisfies ϕ if its trace belongs to ϕ. We consider an observation function defined as a morphism

O : Σ ∞ → Σ ∞
o , based on a mapping π : Σ → Σ o ∪ {ε} for a finite alphabet Σ o . For instance, if Σ = 2 A for a set A of atomic propositions, we can define a subset A o of observable propositions. Then, by setting

A u = A \ A o , Σ o = 2 Ao , π can be defined by π(σ) = ε for σ ∈ 2 Au and π(σ) = σ ∩ A o otherwise.
The set ϕ is opaque with respect to A and O if each time a word satisfies ϕ, another word with the same observation does not. More precisely, the set of words violating this condition is defined by

V(A, O, ϕ) = (Tr(A) ∩ ϕ) \ (O -1 (O(Tr(A) \ ϕ))) and ϕ is opaque if V(A, O, ϕ) = ∅.
This set is used in [START_REF] Bérard | Quantifying opacity[END_REF][START_REF] Saboori | Current-state opacity formulations in probabilistic finite automata[END_REF] to define various notions of probabilistic opacity. For instance, in [START_REF] Saboori | Current-state opacity formulations in probabilistic finite automata[END_REF], one of the measures corresponds to the particular case where ϕ is the set of finite traces of runs reaching a fixed set of secret states. The boolean property is extended by defining the probability of this set, which is measurable since ϕ is ω-regular: For instance, recall systems A 1 and A 2 of Fig. 1. The secret predicate in this case is the set ϕ b = abΣ ω , accepted by the DPA in Fig. 2, and the observation function is the projection π onto {a, c, d} ω . This predicate is not opaque since the run abd ω discloses the occurrence of b. This is measured by the disclosure: 3 4 . Remark that disclosure only measures probabilities of the observer being sure that the run is in the secret. For example, one can model anonymity of an agent α initiating some protocol by defining ϕ α as the set of all runs initiated by α. Anonymity of α is then equivalent to opacity of ϕ α . In the case where anonymity is not guaranteed, disclosure provides a measure of the threat. In the case where anonymity holds, this measure will be 0 and does not give any insight on the "strength" of anonymity. Other notions measuring this strength were proposed in [START_REF] Chaum | The dining cryptographers problem: unconditional sender and recipient untraceability[END_REF][START_REF] Bhargava | Probabilistic Anonymity[END_REF] and quantitative opacity for partial disclosure of the secret have also been defined in [START_REF] Bérard | Quantifying opacity[END_REF], although they are not linear hence do not fare well under standard optimization techniques.

Disc(A 1 , π, ϕ b ) = P A 1 (abd ω ) = 1 4 and Disc(A 2 , π, ϕ b ) = P A 2 (abd ω ) =
For two PTSs A 1 and A 2 over the same alphabet Σ, predicate ϕ and observation function O, we say that A 1 is more opaque than

A 2 if Disc(A 1 , O, ϕ) ≤ Disc(A 2 , O, ϕ).
3 Constraint Markov Chains, Opacity and Refinement

Constraint Markov Chains and Opacity

Constraint Markov chains (CMCs) were first introduced in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] as a specification formalism and further studied in [START_REF] Caillaud | Constraint Markov chains[END_REF]. They generalize Interval Markov Chains (IMCs), that were also investigated in [START_REF] Chatterjee | Model-checking omega-regular properties of interval Markov chains[END_REF][START_REF] Benedikt | LTL model checking of interval Markov chains[END_REF][START_REF] Bérard | Preserving opacity on interval Markov chains under simulation[END_REF] and extended with parameters in [START_REF] Delahaye | Consistency for parametric interval Markov chains[END_REF] with a focus on the consistency problem, i.e., the problem of existence of an implementation satisfying a given specification.

Definition 3.1 (Constraint Markov Chains). A Constraint Markov

Chain (CMC) over alphabet Σ is a tuple S = (S, s init , T, λ) where S is a finite set of states, with s init ∈ S the initial state, T : S → 2 Dist(S) associates with any state s ∈ S a set T (s) of distributions over S, and λ : S → 2 Σ is the labeling function.

The class of CMCs is very general and benefits from nice closure properties as shown in [START_REF] Caillaud | Constraint Markov chains[END_REF]. However, without an explicit description of the sets T (s) for s ∈ S, algorithmic questions cannot be solved. For our purpose, we simply consider the subclass of Linear CMCs, where each set T (s) is defined by a conjunction of linear inequalities and the label λ(s) is a singleton. In this case, with a slight abuse of notation, we note λ(s) = a instead of λ(s) = {a}, as done in Fig. 1(c). By construction, Linear CMCs are closed under conjunction.

More precisely, a linear constraint over S is of the form s∈S α s x s β, with all α s and β in Q, ∈ {<, ≤, =, ≥, >}, and each x s is a variable for state s. A linear probability set on S is a subset of Dist(S) where the distributions µ = (µ(s)) s∈S are the solutions of a system of linear constraints over S. Remark that the conditions for µ to be a distribution are also described by linear constraints: s∈S x s = 1 and, for all s, 0 ≤ x s ≤ 1; these constraints are implicit in the sequel. Thus a linear probability set is a linear set in R |S| in the usual sense. It is also a convex polytope. We denote by L(S) the set of linear probability sets on S. For IMCs, each set T (s) is defined by a family (I(s, s )) s ∈S of intervals in [0, 1] and contains all distributions µ such that for each s ∈ S, µ(s ) ∈ I(s, s ). This can be expressed as a system of linear inequalities by introducing the lower and upper bounds of the intervals. Note that any PTS can be seen as an IMC (hence as an LCMC), where each interval is reduced to a point. For convenience, we keep the interval notation when applicable.

For example, consider the LCMC of Fig. 3, representing a simple system. For graphical depiction, an edge from s to s is labeled by the variable for x s in the system of linear constraints defining T (s); as usual, absence of edge (s, s ) means x s = 0 is a constraint of T (s). The aim of this system is to achieve Success, but there can be errors (which may be recovered) and failures (which cannot). The probabilities underlying the behavior of the system are not fixed, although a certain number of constraints are known. For example, the probability of a recoverable error is at least twice the one of an unrecoverable one, as expressed by the equation x 2 ≥ 2x 3 , and when trying to recover from an error, there is a probability of success exceeding the probability of definite failure by 1 4 .

Idle q0

Error q2

Recover q4

Success q1

Failure

q3 x1 x2 x3 1 y2 y1 y3 1 1 x 2 ≥ 2x 3 x 2 + x 3 ≤ 1 2 y 1 > y 3 + 1 4
Fig. 3. An LCMC which is not a conjunction of IMCs.

Note that it is not an IMC. Indeed, assume that the constraints on T (q 0 ) can be expressed by intervals. Any values for x 1 , x 2 , and x 3 that satisfy the linear constraints should be in the intervals. In particular, it is the case for the three tuples of values for (x 1 , x 2 , x 3 ): (1, 0, 0), and ( 12 , 1 2 , 0),

( 1 2 , 1 3 , 1 6
). So it must be the case that [ 1 2 , 1] ⊆ I(q 0 , q 1 ), [0, 1 2 ] ⊆ I(q 0 , q 2 ), and [0, 1 6 ] ⊆ I(q 0 , q 3 ). Hence the distribution defined by x 1 = 5 6 , x 2 = 0, x 3 = 1 6 is within the bounds of the intervals, although it does not satisfy the constraint x 2 ≥ 2x 3 , which is a contradiction.

In addition, it is neither the result of conjunction of several IMCs, as those only yield constraints where coefficients are positive, hence constraint x 2 ≥ 2x 3 (which is actually x 2 -2x 3 ≥ 0) cannot be expressed.

Several semantics can be given to CMCs with respect to the set of PTSs they specify. The simplest one corresponds to first choosing for each state s a distribution belonging to T (s), thus producing a PTS (the implementation), with the same structure as the CMC (the specification). This was done for IMCs in [START_REF] Chatterjee | Model-checking omega-regular properties of interval Markov chains[END_REF][START_REF] Benedikt | LTL model checking of interval Markov chains[END_REF] and called the Uncertain Markov Chain semantics. A richer semantics consists in introducing a scheduler, choosing the distribution at each step to obtain an implementation, as in a Markov Decision Process (MDP). This was also defined in [START_REF] Chatterjee | Model-checking omega-regular properties of interval Markov chains[END_REF] for IMCs and called IMDP for Interval Markov Decision Process. Finally, the most general semantics corresponds to the satisfaction relation from [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF][START_REF] Caillaud | Constraint Markov chains[END_REF], restricted in [START_REF] Caillaud | Constraint Markov chains[END_REF] to finite state processes. This relation can be obtained from the refinement defined below in Section 3.2.

We consider here the MDP semantics. A run of S starting from a state s is a sequence s

µ 1 -→ s 1 µ 2
-→ . . . where s i ∈ S and each µ i is a distribution over S such that ∀s ∈ S, µ i ∈ T (s i-1 ). As before, we denote by Runs s (S) the set of runs starting from s, we set Runs(S) = Runs s init (S), FRuns(S) is the set of finite runs of S starting from s init , and for a run ρ = s

µ 1 -→ s 1 µ 2 -→ . . . s n-1 µn -→ s n in FRuns(S) we define lst(ρ) = s n .
To associate a probability measure with the runs, it is necessary to resolve the non determinism by a scheduler that chooses a distribution at each step. More precisely: Definition 3.3 (Scheduler). A scheduler A for a CMC specification S = (S, s init , T, λ), is a mapping A : FRuns(S) → Dist(S) such that for each run ρ with s = lst(ρ), A(ρ) ∈ T (s).

We denote by Sched(S) the set of schedulers for S. Like for Markov Decision Processes, scheduling S with A produces a PTS denoted by S(A), where states are finite runs of S and the labelings must be consistent: S(A) = Q, q init , ∆, L with Q ⊆ FRuns(S), the initial state is q init = s init , the run containing only the initial state of S, and for ρ ∈ Q,

L(ρ) ∈ λ(lst(ρ)) and ∆(ρ)(ρ ) = A(ρ)(s ) for ρ = ρ A(ρ)
---→ s . We note:

sat(S) = {S(A) | A ∈ Sched(S)}.
Note that the Uncertain Markov Chains semantics corresponds to the particular case of memoryless schedulers.

We now lift the notion of disclosure to the set of scheduled implementations of a specification S by:

Disc(S, O, ϕ) = sup A∈Sched(S)
Disc(S(A), O, ϕ).

This measure differs from the similar one in [START_REF] Bérard | Probabilistic Opacity for Markov decision processes[END_REF] for Markov Decision Processes. The notion presented here is finer since the set of runs measured by the disclosure depends on the scheduled implementation. In [START_REF] Bérard | Probabilistic Opacity for Markov decision processes[END_REF], the set of runs of the disclosure is defined on the (unscheduled) MDP, and its probability is optimized afterwards. This would not be well-defined in CMCs, since two scheduled implementations can have different sets of edges with non-null probability, as explained in Section 4.

Refinement

The notion of strong refinement between probabilistic specifications was introduced in [9] through simulation. A weaker refinement was also proposed in [START_REF] Caillaud | Constraint Markov chains[END_REF]. These notions are adapted to our setting in Definitions 3.4 and 3.5 below.

Definition 3.4 (Strong refinement relation).

For two CMC specifications S 1 = (S 1 , s (1)

λ 1 (s 1 ) ⊆ λ 2 (s 2 ), (2)
there exists a function δ : S 1 → Dist(S 2 ) such that for all µ ∈ T 1 (s 1 )

s 1 ∈S 1 µ(s 1 ) • δ(s 1 ) ∈ T 2 (s 2 ), (3) s 1 Rs 2 whenever δ(s 1 )(s 2 ) > 0.
For weak refinement, the mapping δ depends on the chosen distribution µ (as well as on s 1 and s 2 ) instead of being uniform: (2) for each µ ∈ T 1 (s 1 ) there exists a function δ :

Definition 3.5 (Weak refinement relation). For two CMC specifi- cations S 1 = (S 1 , s 1,init , T 1 , λ 1 ) and S 2 = (S 2 , s 2,init , T 2 , λ 2 ) over alpha- bet Σ, S 1 weakly refines S 2 , written S 1 w S 2 , if there exists a relation R ⊆ S 1 × S 2 such that s 1,init R s 2,init and if s 1 Rs 2 then: (1) λ 1 (s 1 ) ⊆ λ 2 (s 2 ), a q0 S1 : b q1 b q2 [0, 1] [ 1 3 , 2 3 ] [ 1 4 , 1 3 ] [1, 1] [1, 1] a r0 S2 : b r1 [0, 1] [0, 1] [1, 1]
S 1 → Dist(S 2 ) such that s 1 ∈S 1 µ(s 1 ) • δ(s 1 ) ∈ T 2 (s 2 ), (3)
s 1 Rs 2 whenever δ(s 1 )(s 2 ) > 0.

Fig. 4 illustrates the strong refinement relation R of S 2 by S 1 . For Condition (2) above, we may uniformly use the function: δ 0 (q i )(r j ) = 1 if (q i , r j ) ∈ R and 0 otherwise, represented with dashed lines in Fig. 4.

Note that there is no weak refinement relation of S 1 by S 2 . Indeed, let µ ∈ T 2 (r 0 ) defined by µ(r 0 ) = 4 5 and µ(r 1 ) = 1 5 . Given any function δ : S 2 → Dist(S 1 ) as in Definition 3.5, it must be the case that δ(r 0 )(q 1 ) = 0 since labels do not match. However, µ(r 1 ) • δ(r 1 )(q 1 ) ≤ µ(r 1 ) = 1 5 / ∈ [ 1 3 , 2 3 ]. So µ(r 1 )•δ(r 1 ) is not a distribution in T 1 (q 0 ), which violates Condition [START_REF] Alur | Preserving secrecy under refinement[END_REF].

When a PTS refines a specification, both notions coincide and correspond to the satisfaction relation, which defines the most general semantics of CMCs (from [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF]): A PTS A = (Q, q init , ∆, L) implements a CMC S = (S, s init , T, λ), written A S for the associated relation ⊆ Q × P , if A refines S, where A is seen as a CMC with point distributions. Specification S is said consistent if it admits at least one implementation.

Refinement also applies to two PTSs, and since each probability set reduces to a single distribution, Condition (2) becomes ( 2): For all s 2 ∈ S 2 ,

s 1 ∈S 1 ∆ 1 (s 1 )(s 1 ) • δ(s 1 )(s 2 ) = ∆ 2 (s 2 )(s 2 ).
It is proved in [START_REF] Caillaud | Constraint Markov chains[END_REF] that S 1 s S 2 implies S 1 w S 2 , which in turn implies that for any PTS A, if A S 1 then A S 2 , all implications being strict.

Finally, it can be seen that scheduling a CMC specification is a particular case of implementation but not every implementation can be mapped to a scheduler: Proposition 3.6. Let S be a CMC specification. For each scheduler A of S, S(A) S.

Proof. The relation R ⊆ Q × S is defined by R = {(ρ, s) | lst(ρ) = s}.
We prove that the relation R is a refinement relation by defining δ (ρ,s) over Q × S as follows:

δ (ρ,s) (ρ , s ) = A(ρ)(s ) if ρ = ρ A(ρ) ---→ s , 0 otherwise. ( 1
)
The first condition results from the definition of the labeling and conditions 2 and 3 come from the fact that the joint distribution δ (ρ,s) is diagonal in this case.

(

) (a) δ(ρ , S) = A(ρ)(s ) = ∆(ρ)(ρ ) with ρ = ρ A(ρ) ---→ s for all ρ ∈ Q. (b) δ(Q, s ) = A(ρ)(s ) ∈ T (s)(s ) with s = lst(ρ) for all s ∈ S. 2
(3) ρ Rs whenever δ(ρ , s ) > 0 since s = lst(ρ ) by definition of R.

Indeed, for any scheduler A, S(A) is a kind of unfolding of S, which restricts the structure of S(A): at each step, the scheduler chooses a valid distribution among successor states. Hence not every implementation can be mapped to a scheduler. Said otherwise, not all implementations can be put in relation with S through a satisfaction relation where the joint distributions δ are diagonal.

For example, consider the specification S 0 of Fig. 5(a). There is a single possible scheduler for this specification: the one that picks in q 0 probability 1 2 to go to either q 1 or q 2 (A 1 in Fig. 5(b)). However, the PTS A 2 of Fig. 5(c) is also an implementation of this specification (A 2 |= S 0 ) where r 2 is split between q 1 and q 2 . The corresponding matrix is

δ(q 0 , r 0 ) =   r 0 r 1 r 2 r 3 q 0 1 0 0 0 q 1 0 1 3 1 6 0 q 2 0 0 1 6 1 3  

Motivating example

Consider a simple access control database mechanism to a medical database (inspired from [START_REF] Biondi | Maximizing entropy over Markov processes[END_REF]) as illustrated in Fig. 6(a). In S 2 , a user is first requested to input a username (a). If the user name is not on the list of Fig. 5. A specification with an implementation that is not the result of scheduling.

a q0 b q1 b q2 [ 1 2 , 1] [ 1 2 , 1] [1, 1] [1, 1] (a)
authorized medical staff (d), the request is rejected (e) and otherwise, the user is requested to input a password (b). If the password is correct, access to the database records is provided (c) and is refused (e), otherwise. The transition probabilities take in accountdepend many factors e.g. the number of legitimate users of the database, the robustness of their respective passwords, or the attacker's knowledge. S 1 depicted in Fig. 6(b) refines the password verification process. If the password is correct, it is accepted. Otherwise, a lookup of a black list of common password is performed. If the password is in the list, access is refused, considering it is a malicious attacker and the user is allowed to try again, otherwise. The refinement removes the modalities by restricting intervals (as explained below) and splits the state q 1 onto r 1 and r 2 in S 1 . In order to express security requirements that any implementation of these specifications should assume, consider the observation function O defined as

O(a) = a, O(c) = c, O(d) = d, O(e) = e et O(b) = ε.
It reflects the fact that the password input by the user should be kept secret. This could be realized by mean of some cryptographic infrastructure later on along the refinement process but it is not useful to specify this any further here.

It is well known that this kind of mechanism is not robust enough to provide an adequate protection against covert channels allowing an attacker to access any private information from patient medical record whose access should be strictly limited to medical professionals, the legitimate users of the database. As an example, imagine an observer who could discriminate between abc ω , the execution where a legitimate user is accepted at the first password try and any execution in abb + c ω where he

a q0 S2 : b q1 c q3 d q2 e q4 [0.2, 1] [0.2, 1] [1, 1] [0, 1] [0, 1] [0, 1] [1, 1] [1, 1] (a) S2 a r0 S1 : b r2 b r1 c r4 d r3 e r5 [0.2, 0.4] [0.2, 1] [1, 1] [0.1, 1] [0.1, 1] [0.1, 1] [0.1, 1] [1, 1] [1, 1] (b) S1
Fig. 6. An access control mechanism to a medical database S 2 and its refinement S 1 .

is only accepted after several tries. This could serve as a channel between this user and an attacker on behalf of whom he is acting for in order to leak any private information of any patient record. Requesting as best opacity as possible of the predicate ϕ = abc ω , for all implementations of the specification tears down the possibility of such information flow. Let us have a look at the opacity of ϕ. First note that Disc(S 2 , O, ϕ) > 0: since the interval labeling the loop on q 1 contains 0, there is a distribution µ ∈ T 2 (q 1 ) such that µ(q 1 ) = 0. This loop may or may not be scheduled by an attacker and is later called a modal edge for this reason. Hence any implementation S 2 (A) of S 2 blocking the loop on q 1 but not the edge (q 1 , q 2 ) discloses ϕ. Indeed, in this case T r(S 2 (A)) = abc ω + abe ω + ade ω , L \ ϕ = abe ω + ade ω , O(ϕ) = ac ω and O(L \ ϕ) = ae ω + ade ω proving that O(ϕ) ⊆ O(L \ ϕ). Note also that as there is no modal edge in S 1 , for any scheduler A, ∆(r 1 )(r 2 ), ∆(r 2 )(r 1 ) > 0 where ∆ is the S 1 (A) transition function. Hence, T r(S 1 (A) = abc ω + ab(bb) * c ω + a(bb) + e ω + ade ω , and O(L \ ϕ) = ac ω + ae ω + ade ω , proving that ϕ is opaque for the infinitely many implementations S 1 (A) of S 1 that is, Disc(S 1 , O, ϕ) = 0.

In Section 4 we give an algorithm to compute the exact disclosure of a specification without modal edges (such as S 1 ) and a scheme to approximate the general case (like for S 2 ). Finally note that Disc(S 1 , O, ϕ) < Disc(S 2 , O, ϕ). In Section 5 we prove that amazingly, since in general information flow properties are not preserved under refinement, when S 1 refines S 2 , it is always the case that Disc(S 1 , O, ϕ) ≤ Disc(S 2 , O, ϕ), for any secret ϕ and observation function O.

Modal edges

When the probability of an edge can be equal to 0, the corresponding action can be completely blocked by a scheduler. From a modeling point of view, modal edges add a lot of flexibility for refinement. This however means that the range of potential implementations is larger and so it will be harder to obtain meaningful properties. Therefore such edges are desirable in an early modeling phase but less so in the latest refinements.

As in [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF], we call these edges modal edges, and CMCs that contain such edges are called modal CMCs. In the context of opacity, removing an edge drastically changes the disclosure, since it can remove ambiguities. For example, consider the modal IMC S m of Fig. 7(a), where a and b are observed and the secret is the presence of c. An implementation of S m that blocks the direct edge from a to b (Fig. 7(c)) has a disclosure of 1, since the secret is guaranteed to be part of the only possible run. On the other hand, in the non-modal version of the IMC (Fig. 7(b)), such implementations are banned and only implementations that retain a small probability to avoid c are allowed. In these implementations, the disclosure is 0, since every run is observed as ab ω and it is possible that c did not occur.

The detection of modal edges is the first step toward computation of the disclosure.

Proposition 4.2. The set of modal edges can be computed in time polynomial in the number of edges.

Proof. The procedure for each edge (s, s ) is as follows. Assume T (s) is defined by the conjunction k i=1 C i where each C i is a linear constraint. The edge (s, s ) is modal if and only if x s = 0∧ k i=1 C i admits a solution. This can be checked in polynomial time [START_REF] Roos | Theory and Algorithms for Linear Optimization. An Interior Point Approach[END_REF].

Computation in non-modal LCMCs

In the case of non-modal LCMCs, the disclosure can be computed: Theorem 4.3. Computing the value of disclosure for an LCMC S without modal edges can be done in 2EXPTIME.

Proof. The proof relies on constructing an (exponentially larger) MDP on which an optimization problem is solved. In the spirit of [START_REF] Sen | Model-checking Markov chains in the presence of uncertainties[END_REF], the construction of the MDP relies on basic feasible solutions (BFSs), otherwise called corner points.

Starting from a DPA A ϕ for ϕ, a DPA A V for V(A K , O, ϕ) can be built, with size exponential in the size of S and A ϕ (and with a number k of colors polynomial in the size of A and A ϕ ). This construction relies on intersections and complementations of DPA, with a determinization step that brings the exponential blowup [START_REF] Piterman | From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata[END_REF]. Synchronizing the DPA A V with the original LCMC yields an LCMC S V . Finding the optimal scheduler for S V to accept yields the optimal value of Disc(A K , O, ϕ). This optimization is done by translating S V into an MDP M V as follows.

For each state s of S V , we compute the set of the BFS of the polytope defined by T (s). Then we build the corresponding state in the MDP M V by adding a transition (i.e. a probability distribution) per BFS. As a property of BFSs, any distribution in T (s) in S V can be expressed as a barycentric combination of BFSs. Hence a scheduler on M V corresponds exactly to a scheduler on S V . As a result maximizing the probability of V(A K , O, ϕ) in M V is exactly the same as computing said optimum in S V . This yields a memoryless scheduler, which in turn can be translated into a finite memory scheduler in S.

Note that this construction annihilates the difference between strict and large inequalities. This is of no consequence on the computation of the value of the disclosure. Indeed, if the optimal value is reached on a facet of the polytope defined through a strict inequality, one can build a sequence of ever closer schedulers converging in the limit to the optimal value. In the case where the strict constraint is of the form x s > 0, i.e. that the edge should disappear in the limit, this actually does not introduce a modal edge in the sense that the set

V(A K , O, ϕ) is not changed.
The number of BFSs of a system of rank r in dimension n is bounded by n r (the number of subsets of cardinality r in a set of n elements), hence for each state there is an exponential number of BFSs to consider. As a result the overall complexity of the procedure is in 2EXPTIME.

An example of the transformation described in the above proof is illustrated for state q 0 of the LCMC in Fig. 3. The BFSs are depicted in Fig. 8: all possible distributions are points in the red triangle with corners µ 1 , µ 2 , and µ 3 being the three BFSs. Note that these distributions only consider values for x 1 , x 2 , x 3 , since all other values are null. The transformation of the LCMC (for state q 0 ) into an MDP is illustrated in Fig. 9.

• • • µ 1 µ 2 µ 3 x1 x2 x3 1 2 1 1 2 1 6 µ1 = (1, 0, 0) µ2 = ( 1 2 , 1 2 , 0) µ3 = ( 1 2 , 1 3 , 1 6 )
Fig. 8. Basic Feasible Solutions for state q 0 .

Towards the general case

When a scheduler is faced with the choice to include or exclude a modal edge, it can produce several versions of PTSs, say A 1 and A 2 , with

Tr(A 1 ) = Tr(A 2 ), hence V(A 1 , O, ϕ) = V(A 2 , O, ϕ).
In addition, these choices may be history dependent, as in the example of Fig. 10, with ϕ = aΣ ω and only letters c and d being observed. Intuitively, a way for the scheduler to always disclose the presence of an initial a is to always follow an a by the same letter, say a c. However, this choice must be made after the first letter has been seen. Moreover, leaving the possibility of a run ad • • • to occur means that run ac • • • does not disclose ϕ. As a result, the scheduler should also take into account ϕ and the observation function before committing to a choice with respect to modal edges. So far, the general case of modal LCMCs remains open. However, we now propose an approximation scheme using finite memory schedulers.

In the case of modal LCMCs, disclosure can be approximated by computing only what can be disclosed by an adversary with bounded memory. Increasing the allotted memory provides a better approximation of the disclosure, although there is no guarantee that the disclosure can be achieved with finite memory. A finite memory adversary can be defined as follows: Scheduling S with A produces a PTS S(A) where the set of states is [n]×S, the initial state is (i init , s init ), for (i, s) ∈ [n]×S, L(i, s) ∈ λ(s) and θ(i, s)(i , s ) = γ(i, s)(s ) for i = θ(i, s). We denote by Sched n (S) the set of n-memory schedulers for S, with sat n

(S) = {S(A) | A ∈ Sched n (S)} and Disc n (S, O, ϕ) = sup A∈Schedn(S) Disc(S(A), O, ϕ).
Memoryless schedulers are those in Sched 1 (S) and the set of finite memory schedulers is n Sched n (S) [START_REF] Baier | Principles of Model Checking (Representation and Mind Series)[END_REF]. The computation of the disclosure of an LCMC S under bounded memory adversaries relies on:

the computations of the set of modal edges of S (Proposition 4.2); the value of disclosure for LCMCs without modal edges (Theorem 4.3); the unwinding of S with respect to a memory bound and the removal of modal edges (described below).

The unwinding construction. Given S = (S, s init , T, λ) and a finite tran-

sition system A n,θ = ([n], i init , θ), we construct the LCMC A n,θ × S = ([n] × S, (i init , s init ), T , λ) s.t. -μ ∈ T (i, s) iff ∃µ ∈ T (s) such that for i ∈ [n], μ(i , s ) = µ(s ) if i = θ(i, s) 0 otherwise -λ(i, s) = λ(s)
The unwinding of S by an n-state automaton A produces an LCMC S A formed with n copies of S (one for each state of A), communicating with each other according to the mode transition function of A. Memoryless schedulers on S A then correspond to n-memory schedulers on S. We note Sched A n,θ (S) the set of schedulers for S of the form A = (A n,θ , γ) for γ : [n] × S → Dist(S) where for s ∈ S and for all i ∈ [n], γ(i, s) ∈ T (s). Hence, any implementation of sat n (S) can be obtained by a memoryless scheduler on some S A . Remark that there is only a finite number of such automata. This construction entails:

Lemma 4.5. For any LCMC S,

sat 1 (A n,θ × S) = {S(A) | A = (A n,θ , γ) for some γ}.
The modal edge removing construction. Given S = (S, s init , T, λ), an LCMC, let M(S) be the set of modal edges of S. For a subset ξ ⊆ M(S), we define S \ ξ as the modal edge free LCMC obtained from S by removing edges in ξ and "unmodalizing" modal edges of S not in ξ: this means that if (s, s ) ∈ ξ, we add the constraint x s = 0 to T (s) and if (s, s ) / ∈ ξ, we add the constraint x s > 0 to T (s). Note that removing an arbitrary subset ξ of M(S) may result in an inconsistent specification. These will be ignored by our algorithm (recall that consistency checks are polynomial for LCMCs [START_REF] Caillaud | Constraint Markov chains[END_REF]).

The algorithm. Algorithm 1 enumerates all possible finite transition systems with n states and unwinds S over them. For each such unwinding, the algorithm explores the set of memoryless schedulers. This exploration is done by first selecting the set of modal edges to remove and for each set, compute the maximal disclosure using the procedure of Theorem 4.3. Since this procedure may use arbitrary schedulers, the output of the algorithm is an overapproximation of Disc n (S, O, ϕ), the disclosure of S restricted to n-memory schedulers. On the other hand, it is an underapproximation of the actual disclosure.

Correctness. The partial correctness of Algorithm 1 relies on Lemma 4.5 above as well as the following observation, indicating that the choice of some set of modal edges to remove exactly corresponds to the scheduler choice: Lemma 4.6. For any LCMC S and for any memoryless scheduler A = (A, γ) of S, there exists a maximal subset ξ of M(S) such that for any (s, s ) ∈ M(S), γ(1, s)(s ) = 0 iff (s, s ) ∈ ξ.

Proof. Since the scheduler is memoryless, the choice of scheduling a modal edge to 0 must be uniformly taken along any run, hence this edge never appears in the PTS scheduled by A. This is equivalent to remove this edge from S so the set ξ is the collection of all such edges. For the first inequality, let A = (A, γ) be an n-memory scheduler for S and let S A be the corresponding unwinding. This unwinding is computed in the loop of Algorithm 1 at line 3. By Lemma 4.5 the n-memory schedulers on S are exactly the memoryless schedulers on S A . Hence the choice function γ is memoryless on A × S. Therefore Lemma 4.6 provides a set ξ of modal edges to be removed, such that S A and S A \ξ coincide when scheduled by γ. The removal of this set ξ is performed in the inner loop at line 6. Hence the disclosure of S(A) is less than or equal to Disc(S A \ ξ, O, ϕ) computed at line 8 (equality is not ensured since the computation of Theorem 4.3 does not restrict memory). This value is itself smaller than the output of the algorithm, hence Disc n (S, O, ϕ) ≤ Disc(n, S, O, ϕ).

The second inequality results from the fact that all values computed by Algorithm 1 are of the form Disc(S A \ ξ, O, ϕ). Since the maximum is obtained on a subset of schedulers, Disc(n, S, O, ϕ) ≤ Disc(S, O, ϕ) holds.

This algorithm makes 2 O(n) calls to the 2EXPTIME procedure of Theorem 4.3. Thus the complexity of Algorithm 1 remains in 2EXPTIME as long as n is polynomial in the size of S.

Monotonicity of disclosure

This section is devoted to the proof of the following result, establishing monotonicity with respect to weak refinement for the disclosure over scheduled implementations: Theorem 5.1. Let S 1 and S 2 be LCMC specifications such that S 1 w S 2 . Then Disc(S 1 , O, ϕ) ≤ Disc(S 2 , O, ϕ).

Since scheduling is a restrictive way to derive implementations from a specification, it is not the case in general that sat(S 1 ) ⊆ sat(S 2 ): although any scheduling S 1 (A 1 ) of S 1 with A 1 is an implementation of S 2 , this implementation may not be a scheduling.

Instead, the proof builds a scheduler A 2 for S 2 , producing an implementation S 2 (A 2 ) that is refined by S 1 (A 1 ) (Theorem 5.2, illustrated in Fig. 11). Then, this refinement is shown to ensure that the probabilities of (cones of) finite words coincide (Propositions 5.3 and 5.4). The disclosure set being a measurable event, coincidence of probabilities on cones ensures coincidence of probabilities for the disclosure.

Notations. Given two specifications S 1 and S 2 such that S 1 weakly refines S 2 through relation R, we define the relation ∼ on FRuns(S 1 ) × FRuns(S 2 ) by: ρ 1 ∼ ρ 2 if |ρ 1 | = |ρ 2 | and at any intermediate step i, the corresponding states satisfy s 1,i R s 2,i .

For ρ 2 ∈ FRuns(S 2 ), we set sim(ρ 2 ) = {ρ 1 ∈ FRuns(S 1 ) | ρ 1 ∼ ρ 2 }. We now define a measure µ ρ 2 over sim(ρ 2 ) by µ ρ 2 (ρ 1 ) =

P A 1 (ρ 1 ) P A 1 (sim(ρ 2 ))
(where the probability of finite run ρ is abusively written instead of the probability of its cone C ρ ).

We first show how to build a scheduler A 2 for S 2 such that S 1 (A 1 ) refines S 2 (A 2 ). Recall from Section 3.2 that for PTSs, weak and strong re-

S 2 S 1 S 1 (A 1 ) S 2 (A 2 ) R sat 1 R • sat 1 R sat 2 Fig.
1 = S 1 (A 1 ) = (Q 1 , q init,1 , ∆ 1 , L 1
). Then we show that there exists A 2 ∈ Sched(S 2 ) and a refinement relation R such that R • sat 1 = sat 2 • R where sat 2 is the satisfaction relation related to A 2 . Let ρ 2 ∈ FRuns(S 2 ) with lst(ρ 2 ) = s 2 . Then, for any ρ 1 ∈ sim(ρ 2 ), A 1 (ρ 1 ) ∈ T 1 (lst(ρ 1 )) and lst(ρ 1 )R s 2 . Since S 1 weakly refines S 2 , there exists δ ρ 1 : S 1 → Dist(S 2 ) such that s 1 ∈S 1 A 1 (ρ 1 )(s 1 )δ ρ 1 (s 1 ) ∈ T 2 (s 2 ).

We define A 2 on FRuns(S 2 ) by:

A 2 (ρ 2 ) = ρ 1 ∈sim(ρ 2 ) µ ρ 2 (ρ 1 ) s 1 ∈S 1 A 1 (ρ 1 )(s 1 ) • δ ρ 1 (s 1 ).
From the definition of µ ρ 2 and the convexity of T 2 (s 2 ), we can conclude that A 2 (ρ 2 ) also belongs to

T 2 (s 2 ), hence A 2 is a scheduler of S 2 . Writing now A 2 = S 2 (A 2 ) = (Q 2 , q init,2 , ∆ 2 , L 2
), the relation R can be defined as ∼ (relating runs that are similar "step by step", as defined above). To see that the conditions are satisfied, let ρ 1 and ρ 2 be runs in Q 1 and Q 2 respectively. Then the mapping δ :

Q 1 → Dist(Q 2 ) is obtained by: δ (ρ 1 )(ρ 2 ) = µ ρ 2 (ρ 1 )δ ρ 1 (lst(ρ 1 ))(lst(ρ 2 )) if ρ 1 ∼ ρ 2 , 0 otherwise.
Since A 1 and A 2 are PTSs, we just need to show that Equation (3.2)

holds. Writing ρ 2 = ρ 2 A 2 (ρ 2 )
----→ s 2 , we have:

∆ 2 (ρ 2 )(ρ 2 ) = A 2 (ρ 2 )(s 2 ) = ρ 1 ∈sim(ρ 2 ) µ ρ 2 (ρ 1 ) s 1 ∈S 1 A 1 (ρ 1 )(s 1 ) • δ ρ 1 (s 1 )(s 2 ) = ρ 1 ∈sim(ρ 2 ) s 1 ∈S 1 A 1 (ρ 1 )(s 1 ) • δ (ρ 1 A(ρ 1 ) ---→ s 1 )(ρ 2 ) = ρ 1 ∈Q 1 A 1 (ρ 1 )(s 1 ) • δ (ρ 1 )(ρ 2 ) by defining ρ 1 = ρ 1 A 1 (ρ 1 )
----→ s 1 for each ρ 1 and remarking that δ = 0 if its arguments are not similar runs. Hence:

∆ 2 (ρ 2 )(ρ 2 ) = ρ 1 ∈Q 1 ∆ 1 (ρ 1 )(ρ 1 ) • δ (ρ 1 )(ρ 2 ).
Now we show that refinement between two PTSs is sufficient to compare their disclosure. Namely, we show that the probabilities of cones of words are equal in both systems. Note that although this property is well known to hold for paths, it needs to be lifted to words in order to compare disclosure.

We start by considering the sets of traces globally; although it is folklore that refinement implies trace inclusion, we provide a proof for completeness sake.

Proposition 5.3. Let A 1 and A 2 be PTSs such that A 1 refines A 2 . Then T r(A 1 ) = T r(A 2 ).

Proof. We prove the proposition by induction on a strengthened statement. Namely, we claim that for every finite run in A 1 there exists a similar run in A 2 . Since an infinite run is the limit of the sequence of its finite prefixes, this claim is sufficient to prove the proposition. Assume by induction that the proposition holds for every word of length n. Let w ∈ FTr(A 1 ) of length n+1. We write w = w 0 a for some a ∈ Σ. Consider a run of A 1 that produces w. It is of the form ρ 0 s 1 where λ(s 1 ) = a; let s 1 = lst(ρ 0 ). Let ρ 0 be a run in A 2 , similar to ρ 0 , and s 2 = lst(ρ 0 ). By definition of refinement, there exists a function δ such that for any state

s 2 of A 2 , ∆ 2 (s 2 )(s 2 ) = σ 1 ∈S 1 ∆ 1 (s 1 )(σ 1 ) • δ(σ 1 )(s 2 ).
Moreover, whenever δ(σ 1 )(s 2 ) > 0, λ(s 1 ) = λ(s 2 ). Since δ(s 1 ) is a distribution over S 2 , δ(s 1 )(s 2 ) > 0 for at least one state s 2 . Hence ρ 0 s 2 is similar to ρ, which shows in particular that w ∈ FTr(A 2 ).

We additionally show that probabilities coincide: Proposition 5.4. Let A 1 and A 2 be PTSs such that A 1 refines A 2 . Then for all w ∈ Σ * , P A 1 (C w ) = P A 2 (C w ).

Since a given word may be produced by several paths, their probabilities should be considered altogether. Hence the proof of the above proposition is not immediate; it is quite technical and can be found in Appendix A.

Existing properties about refinement for PTSs can be retrieved as consequences of the above result. They were for example obtained as a particular case of sub-stochastic refinement in [START_REF] Baier | Comparative branching-time semantics for Markov chains[END_REF]. Although not necessary to prove the main theorem, these results illustrate how constraining refinement between PTSs is.

Recall that a probabilistic bisimulation [START_REF] Jonsson | Specification and refinement of probabilistic processes[END_REF] is a bisimulation that preserves transition probabilities, i.e., a bisimulation relation R on states such that for any equivalence class R of R, and any two related states sRs , ∆(s)(R) = ∆(s )(R).

Corollary 5.5 ([8]). Let A 1 and A 2 be PTSs such that A 1 refines A 2 . Then there exists a probabilistic bisimulation over the union of both PTSs.

Corollary 5.6 ([8]

). Let A 1 and A 2 be PTSs such that A 1 refines A 2 . Then A 2 also refines A 1 .

We are now ready to prove Theorem 5.1:

Proof. Let A 1 ∈ sat(S 1 ). By Theorem 5.2 there exists A 2 ∈ sat(S 2 ) that is refined by A 1 . By Proposition 5.4, P A 1 (C w ) = P A 2 (C w ) for every word w ∈ FTr(A 1 ). Hence, for any ω-regular (hence measurable) language L, one has P A 1 (L) = P A 2 (L). It is in particular the case for V(A 1 , O, ϕ) = V(A 2 , O, ϕ). Therefore, Disc(A 1 , O, ϕ) = Disc(A 2 , O, ϕ). Consequently, the theorem holds.

The result above can now be combined with compositional results on refinement obtained in [START_REF] Caillaud | Constraint Markov chains[END_REF]. In particular, since the conjunction of two CMC specifications is the greatest lower bound with respect to weak refinement, and LCMCs are closed under conjunction, we have: Proposition 5.7. Let S 1 and S 2 be LCMC specifications. Then Disc(S 1 ∧ S 2 ) ≤ min(Disc(S 1 ), Disc(S 2 )). This work investigates how refinement between probabilistic models impacts the security, modeled as opacity, showing that disclosure is monotonic with respect to refinement when implementations are produced by an adversary through scheduling. We provide 2EXPTIME procedures to compute (1) the worst-case disclosure for a subclass of LCMCs and (2) lower bounds on disclosure for all LCMCs when restricted to polynomial size memory schedulers (in the size of the LCMC).

Directions for future work include computing exact disclosure for LCMCs with modal edges for example by bounding the size of schedulers required to reach the supremal value. We also plan to extend our results to larger sub-classes of CMCs or Parametric IMCs from [START_REF] Caillaud | Constraint Markov chains[END_REF][START_REF] Delahaye | Consistency for parametric interval Markov chains[END_REF]. In particular, a question that was left aside is the parallel composition of LCMC, which generates polynomial and possibly non-convex constraints on distributions. Studying the effect of disclosure with respect to this operation would be an interesting (but difficult) task. ∆ 1 (s 1 )(s 1 ) • ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s 1 P A 1 (C ρ 0 ) P A 1 (sim(ρ 0 ))

• P A 2 (C w 0 )

By induction hypothesis, P A 2 (C w 0 ) = P A 1 (C w 0 ) hence:

P A 2 (C w ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ))
∆ 1 (s 1 )(s 1 ) • ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s 1 P A 1 (C ρ 0 ) P A 1 (sim(ρ 0 ))

• P A 1 (C w 0 ) and since P A 1 (sim(ρ 0 )) = P A 1 (C w 0 ):

P A 2 (C w ) =

Fig. 1 .

 1 Fig. 1. Probabilistic systems A 1 or A 2 implementing underspecified system S.

  and we use as shorthands µ(y 1 , Y 2 ) = µ({y 1 }, Y 2 ) and µ(Y 1 , y 2 ) = µ(Y 1 , {y 2 }).

Definition 2 . 3 (

 23 Probabilistic Disclosure). Let A be a PTS, O an observation function and ϕ an ω-regular predicate. The probabilistic disclosure of ϕ in A for O is Disc(A, O, ϕ) = P A (V(A, O, ϕ)).

Definition 3 . 2 (

 32 Linear CMC). A Linear CMC (or shortly LCMC) is a CMC S = (S, s init , T, λ) where for each s ∈ S, T (s) ∈ L(S) and |λ(s)| = 1.

1 1 1 Fig. 4 .

 114 Fig. 4. A refinement of S 2 by S 1 .

  A2, an implementation (not a scheduling) of S0

Definition 4 . 1 (

 41 Modal edge). An edge (s, s ) in CMC S is modal if there exists a scheduler A such that ∆(ρ)(ρA(ρ)---→ s ) = 0 for any run ρ of S(A) with lst(ρ) = s. A disclosing implementation of Sm (but not of Snm). A non-disclosing implementation of Snm (and Sm), ε > 0.

Fig. 7 .

 7 Fig. 7. The influence of modal transitions on disclosure.

Fig. 9 .

 9 Fig. 9. Transforming an LCMC into an MDP using BFSs.

Fig. 10 .

 10 Fig.10. IMC where the choice on modal edge requires history.

Definition 4 .

 4 4 (n-memory scheduler). Let [n] denote the set {1, 2, . . . , n}. An n-memory scheduler A for an LCMC specification S = (S, s init , T, λ), is a tuple A = ([n], i init , θ, γ) where [n] is the set of modes, i init is the starting mode, θ : [n] × S → [n] is a mode transition function and γ : [n] × S → Dist(S), is the choice function with γ(i, s) ∈ T (s) for all i ∈ [n] and all s ∈ S.

ALGORITHM 1 : 2 5 8 compute 3 9 13 return

 128313 Overapproximating Discn(S, O, ϕ) Input: n ∈ N, S, O and ϕ Output: Disc(n, S, O, ϕ) such that Discn(S, O, ϕ) ≤ Disc(n, S, O, ϕ) ≤ Disc(S, O, ϕ) 1 Disc(n, S, O, ϕ) = 0; 2 foreach θ : [n] × S → [n] do 3 construct A n,θ × S; 4 compute the set M(A n,θ × S); // By the procedure described in the proof of Prop. 4.foreach ξ ∈ 2 M(A n,θ ,S) do 6 construct (A n,θ × S) \ ξ; 7 if (A n,θ × S) \ ξ is consistent then Disc((A n,θ × S) \ ξ, O, ϕ);// By the procedure described in the proof of Thm. 4.Disc(n, S, O, ϕ) = max{Disc(n, S, O, ϕ), Disc((A n,θ × S) \ ξ, O, ϕ)}; Disc(n, S, O, ϕ);

Theorem 4 . 7 (

 47 Correctness of Algorithm 1). Given a an LCMC S, an observation O and a secret ϕ for S, the disclosure of ϕ in S for O by a polynomial size adversary (in the size of S) can be over-approximated in 2EXPTIME.Proof. We prove that the output of Algorithm 1:Disc(n, S, O, ϕ) = maxθ max ξ Disc(A n,θ × S \ ξ, O, ϕ) satisfies the post-condition Disc n (S, O, ϕ) ≤ Disc(n, S, O, ϕ) ≤ Disc(S, O, ϕ).

s 1 2 P 1 P A 1 (P A 2 (C ρ 0 ) = s 1

 121121 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ))s 2 ∈S 2 ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s A 2 (C ρ 0 ) • ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 P A 2 (C ρ 0 ) • ∆ 1 (s 1 )(s ) ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 µ ρ 0 (ρ 0 ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) • ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 P A 2 (C ρ 0 )µ ρ 0 (ρ 0 ) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 • ρ 0 ∈FRuns(A 1 ) ρ 0 ∼ρ 0 lst(ρ 0 )=s 1 P A 2 (C ρ 0 ) P A 1 (C ρ 0 ) P A 1 (sim(ρ 0 )) = s 1 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s C ρ 0 ) P A 1 (sim(ρ 0 ))ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 ∈S 1 s 1 ∈S 1 λ(s 1 )=λ(lst(ρ))

s 1 ∈S 1 s 1 1 P A 1 (C ρ 0 ) = s 1 1 P A 1 (C ρ 0 ) • s 1

 11111111 ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) • ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s ∈S 1 ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 lst(ρ 0 )=s ∈S 1 λ(s 1 )=λ(lst(ρ)) ∆ 1 (s 1 )(s 1 ) = ρ 0 ∈FRuns(A 1 ) tr(ρ 0 )=w 0 P A 1 (C ρ 0 )∆ 1 (lst(ρ 0 ))(lst(ρ)) = P A 1 (C w )

  11. Result of Theorem 5.2. Relation R•sat 1 always exists but might not be a scheduling. finement coincide and are thus simply called refinement in the remainder of this section. Theorem 5.2. Let S 1 and S 2 be LCMC specifications such that S 1 weakly refines S 2 . Then for any A 1 ∈ Sched(S 1 ) there exists A 2 ∈ Sched(S 2 ) such that S 1 (A 1 ) refines S 2 (A 2 ).

Proof. Let S 1 = (S 1 , s init,1 , T 1 , λ 1 ) and S 2 = (S 2 , s init,2 , T 2 , λ 2 ) be LCMCs such that S 1 refines S 2 with R. Let sat 1 be the satisfaction relation related to A 1 and A

Partially supported by a grant from Coopération France-Québec, Service Coopération et Action Culturelle 2012/26/SCAC (French Government), the NSERC Discovery Individual grant No. 13321 (Government of Canada), the FQRNT Team grant No. 167440 (Quebec's Government) and the CFQCU France-Quebec Cooperative grant No. 167671 (Quebec's Government). This research has been partially done while this author was visiting the LIP6, Université Pierre & Marie Curie.

A Proof of Proposition 5.4 Assume by induction that the proposition holds for every word of length n. Let w ∈ FTr(A 1 ) = FTr(A 2 ) (recall Proposition 5.3) of length n + 1 with w = w 0 a for some a ∈ Σ. A run ρ of A 2 that produces w can be assumed to be of the form ρ = ρ 0 s 2 with tr(ρ 0 ) = w 0 and λ(s 2 ) = a.

where s 2 = lst(ρ 0 ) and hence:

tr(ρ )=w

we get:

tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s 2

ρ 0 ∈FRuns(A 2 ) tr(ρ 0 )=w 0 , lst(ρ 0 )=s 2 ,lst(ρ )=s 2


Adrien Barbaresi
email: adrien.barbaresi@oeaw.ac.at

Collection, Description, and Visualization of the German Reddit Corpus

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

Introduction

One of the main issues when dealing with web corpora, be it general-purpose corpora or specific ones, consists in the discovery of relevant web documents for linguistic studies. There are for example few projects dealing with computer-mediated communication in German, and it is quite rare to find readymade resources. The DeRiK project for instance features ongoing work with the purpose to build a reference corpus dedicated to computer-mediated communication [START_REF] Beißwenger | DeRiK: A German reference corpus of computer-mediated communication[END_REF]. Previous work towards the constitution of a German blog corpus under CC license implied a significant effort [START_REF] Barbaresi | For a fistful of blogs: Discovery and comparative benchmarking of republishable German content[END_REF].

In this respect, it has been particularly surprising to hear from the release of a complete dataset of comments published on Reddit, a major social network. This article describes the steps taken in order to get a first glimpse of German data in the corpus as well as to describe what makes CMC-data in general and Reddit data in particular so different.

One hope is that the Reddit corpus can be used to find relevant examples of previously undocumented language uses for lexicography and dictionary building projects, e.g. the DWDS lexicography project [START_REF] Geyken | The DWDS corpus: A reference corpus for the German language of the 20th century[END_REF], and/or to test linguistic annotation chains for robustness.

2 Description of the dataset

Reddit

Reddit is a social bookmarking and microblogging platform owned by the American mass media company Condé Nast. It ranks at first place worldwide in the news category according to the site metrics aggregator Alexa1 , which makes it a typical Internet phenomenon. The short description of the website according to Alexa is as follows: "Usergenerated news links. Votes promote stories to the front page." Indeed, the entries are organized into areas of interest called "reddits" or "subreddits", which are curated by the users ("redditors") themselves. Since the moderation processes are mature, and since the channels (or subreddits) have to be hand-picked, they ensure a certain stability. From a linguistic point of view, one may say that users account for the linguistic homogeneity if not relevance of their channel.

There is an API for Reddit, allowing automated retrieval of comments. However, search depth is limited: it is often not possible to go back in time further than the 500th oldest post, which severely restricts the number of links one may crawl [START_REF] Barbaresi | Crawling microblogging services to gather language-classified URLs. Workflow and case study[END_REF]. Continuous crawling is then necessary in order to gather all the possible comments on all the subreddits.

Original release

The work described in the article directly follows from the recent release of the "Reddit comment corpus": Reddit user Stuck In The Matrix (Jason Baumgartner) made the dataset publicly available on the platform archive.org 2 at the beginning of July 2015. In its original release statement on Reddit, Baumgartner claims to have gathered every publicly available Reddit comment, which amounts to 1.65 billion JSON objects.3 350,000 comments out of 1.65 billion were unavailable due to Reddit API issues.

While its compiler chose to name it a "corpus", the whole could rather be called a dataset. In fact, apart from ensuring the most complete collection process possible, no specific steps were taken to allow for a control of the contents in the sense of the linguistic tradition [START_REF] Barbaresi | Ad hoc and general-purpose corpus construction from web sources[END_REF].

Filtering steps

I use a two-tiered filter in order to deliver a hopefully well-balanced performance between speed and accuracy. The combined strategy proved efficient in preliminary tests as well as in previous studies [START_REF] Lui | Accurate Language Identification of Twitter Messages[END_REF]. The first filter consists in a dictionary-based approach taking benefit from spell-checking algorithms. It discriminates between comments using thresholds expressed as a percentage of tokens which do not pass the spell check. The second filter is a full-fledged language detection software, which outputs the most probable language according to its model.

First, spell checking algorithms benefit from years of optimization concerning both speed and accuracy. The library used, enchant, allows the use of a variety of spell-checking backends, like aspell, hunspell or ispell, with one or several locales. 4 English being the most prominent language on Reddit, each token is tested for errors in both English and German. A comment which induces a relatively high amount of errors for English (more than 30%) but a relatively low one for German (less than 70%) is considered to be interesting enough to proceed to the second step. In other studies [START_REF] Barbaresi | Crawling microblogging services to gather language-classified URLs. Workflow and case study[END_REF], I have used a threshold of 0.5; while I did not witness significant changes on Reddit data, I still chose a more defensive setting in order to ensure corpus relevance.

Second, a language identification tool is used to maximize the precision of the language recognition. langid.py [START_REF] Lui | langid.py: An Off-the-shelf Language Identification Tool[END_REF]) is open-source5 , it incorporates a model which has been pre-trained on a variety of web documents (Clue Web and Wikipedia inter alia). It has already been used to classify social media text on a large scale [START_REF] Baldwin | How noisy social media text, how diffrnt social media sources[END_REF] and it is fast enough to be able to classify data from the order of magnitude of the Reddit comments.

The filtering described here is reproducible and can be attempted using other parameters, instructions and code to do so are available. 63 Analysis of the corpus

Linguistic features

The corpus has been tokenized by WASTE [START_REF] Jurish | Word and Sentence Tokenization with Hidden Markov Models[END_REF] and lemmatized by MOOT (Jurish, 2003). It contains a total of 97,505 comments, 89,681 sentences, 566,362 tokens, and 3,352,472 characters. It is clear that Reddit is almost exclusively an English-speaking platform, however there are eminent German channels and due to the sheer size of the original dataset one could have expected a larger corpus. Maybe the precision of the filters could be lowered in favor of a better recall.

The mean token and sentence length (respectively 5.92 characters and 6.32 tokens) are in line with the expectations concerning computermediated communication, and it clearly anchors the corpus on this side of the spectrum. The relatively large vocabulary size in terms of types with 64,314 different forms (27% of which are hapax legomena) calls for further analyses. Qualitatively speaking, the ironic tone Reddit is known for could also prove to be interesting. The breakdown into different part-of-speech tags shown in table 1 gives insights on the actual contents. The proportion of a number of tags from the STTS tagset is in line with other general or CMCcorpora [START_REF] Barbaresi | Finding Viable Seed URLs for Web Corpora: A Scouting Approach and Comparative Study of Available Sources[END_REF], however the number of tokens tagged as proper nouns (NE) is particularly high (14.4%), which exemplifies the perplexity of the tool itself, for example because the redditors refer to trending and possibly short-lived notions and celebrities, or because of a high proportion of short, elliptic comments which fail to provide enough morpho-syntactic context. The relatively high but acceptable proportion of foreign words on token level (4%) both confirms this hypothesis and validates the language classification performed during corpus building. Thanks to the special training of the tokenizer on CMC-data, the smileys can be expected to be treated as whole tokens, which makes a focused analysis possible. The major part of frequent smileys listed in table 2 is commonly used, although there are idioms such as "=)" which may be more frequent on this platform. Emojis do not seem to be frequently used in German comments.

POS-tag

Smiley Frequency

Sociolinguistic factors

Information about the subreddit of each comment is part of the JSON metadata, which makes the extraction of subreddits straightforward. As can be seen in table 3, the most frequent ones include channels where expression in German is expected (de, rocketbeans, kreiswichs) and other where German is not necessarily spoken but could be appropriate (germany, Austria). Other channels, which are known to be among the most popular ones but whose link to German is not clear, may include enough quotes or occasional discussions (e.g. AskReddit) to explain their presence among the most frequent ones.

The nicknames are also part of the metadata returned by the API and as such they can be considered to be reliable information. A total of 51,155 different nicknames can be found throughout the German subset. 5,343 are marked as deleted, i.e. not active at the time of download.

The most frequent author names in The Reddit comments are not geotagged. Thus, a proxy has to be found in order to get a glance at their socio-geographical distribution. To do so, place names are extracted and projected on a map, which allows for a better description of the collected data. First, the German version of the Wiktionary, a user-curated dictionary launched by the Wikimedia foundation, is used in order to get lexical information about common nouns, which allows for a fine-grained discriminating analysis.

Second, geographical information about the places names has been compiled from the Geonames database7 , which is e.g. used by the Openstreetmap project8 , and whose Creative Commons Attribution license will allow for a release of research data in the near future. All databases for current European countries have been retrieved and preprocessed certain place types have been selected. In fact, toponym resolution often relies on namedentity recognition and artificial intelligence (Leidner and Lieberman, 2011), but knowledge-based methods using fine-grained data have already been used with encouraging results [START_REF] Hu | Improving Wikipedia-Based Place Name Disambiguation in Short Texts Using Structured Data from Dbpedia[END_REF].

The tokenized corpus has been filtered as described above and matched with the database. This operation includes finite-state automatons at two distinct stages: first to discover potential multiword place names, and second to select the most probable coordinates in the case of homonyms, based on type, relative distance, and population.

Results

The maps in figure 1 have been generated by the design environment TileMill9 and customized using the stylesheet language CartoCSS. Both maps were created using the same data, on the left the scale is smaller, while on the right place names for frequent entries have been added.

The linguistic corpora at the basis of the maps are a construct, and so are the maps themselves: although they seem immediately interpretable, the quality of data, the specialization of the processing tools, and quality assessment all have a major impact on the outcome.

The place names seem to be quite evenly distributed in the German language area relatively to the most populated cities and thus the expectations. There are a few interesting exceptions: Berlin is usually more precisely named (e.g. "Berlin-Kreuzberg" instead of just "Berlin"), which gives the capital the shape of a constellation on the map.

A clustering phase could be necessary in order to be able to compare it to the other main cities.

All in all, cities the western part of Germany seems to be more frequently mentioned, particularly when they are home to a well-known soccer team (such as Mönchengladbach). In Austria, Vienna clearly outweighs the rest of the country, which could be explained by a higher international visibility as well as a higher density of early-adopters of Reddit.

Conclusion

In this article, I have shown how a corpus focusing on German can be built using the publicly available Reddit comment dataset. In order to get a first impression of the corpus, I collected quantitative information and offered a visualization of structured data, more precisely place names which have to be extracted from the comments since they are not geotagged.

The structural properties of the corpus are in line with the expectations concerning CMC [START_REF] Barbaresi | For a fistful of blogs: Discovery and comparative benchmarking of republishable German content[END_REF]: short sentences, a relatively high number of different lemmata, and a whole vocabulary of smileys. The different nicknames involved seem to be rather evenly distributed, so are the different place names mentioned in the comments, which is good news in terms of diversity.

Since the license restrictions concerning the dataset are unclear, the corpus is only available upon request. Nonetheless, the German subset can be reconstructed and updated from scratch using code released under open source license. 10

Table 1 :

 1 Most frequent POS-tags and relative frequency on token level, without spaces and punctuation

		Frequency
	NN	17.6%
	NE	14.4%
	ADV	8.6%
	VVFIN	6.8%
	PPER	5.9%
	ADJD	4.7%
	ART	4.3%
	VAFIN	4.1%
	XY	3.8%
	ADJA	3.5%

Table 2 :

 2 Most frequent smileys and their frequency

			Smiley Frequency
	:)	3207	:-(	39
	;)	1667	-.-	33
	:(	590	:'(	31
	:-)	299	:))	29
	ˆˆ242	:]	25
	;-)	238	=(	19
	:/	179	:|	18
	=)	96

Table 3 :

 3 table4show Most frequent channels (subreddits) in the corpus that although there is a slight trend towards typical German nouns or syllables, they are not the majority. The crowd seems to be relatively evenly distributed, there is no single nickname outweighing all the others. That said, it can be common practice to change nicknames regularly, which also accounts for the relatively high number of deleted accounts found.

	Channel	Frequency
	de	14018
	AskReddit	8163
	rocketbeans	4899
	funny	3272
	kreiswichs	2848
	pics	2813
	soccer	2571
	Austria	1684
	WTF	1592
	leagueoflegends	1569
	reddit.com	1379
	todayilearned	1224
	germany	1137
	gaming	1133
	videos	1124
	Nickname	Frequency
	Wumselito	262
	Aschebescher	238
	Clit Commander	221
	oldandgreat	210
	GuantanaMo	200
	fLekkZ	187
	Obraka	180
	tin dog	155
	4-jan	151
	Omnilatent	141
	Table 4: Most frequent nicknames in the corpus
	and their frequency
	4 Visualization of extracted place names
	4.1 Method

http://www.alexa.com/topsites/category/Top/News

https://archive.org/details/2015 reddit comments corpus

https://www.reddit.com/r/datasets/comments/3bxlg7/ i have every publicly available reddit comment/

http://www.abisource.com/projects/enchant/

https://github.com/saffsd/langid.py

https://github.com/adbar/german-reddit

http://www.geonames.org

https://www.openstreetmap.org

https://www.mapbox.com/tilemill/


Ayman Hallal

Steve Bouhier

Simon Le Méhauté

François Bondu

Keywords: Feedback, Phase noise, millimeter wave generation, Cavity resonators

Towards an optical synthesis of low phase noise continuous millimeter waves in a compact and an all-fiber system, we present the all-electrical locking of the optical frequency of a distributed feedback laser (DFB) diode at 1549 nm tunable over 2 nm, on a fibered Fabry-Perot (FP) cavity. We demonstrate a 6 MHz servo bandwidth and a frequency noise suppression down to 3.10 -1 Hz/√Hz at 80 kHz carrier offset frequency in the error signal. Furthermore, we use a Brillouin fiber laser in order to refine the stabilized laser linewidth and we then demonstrate a frequency noise suppression down to 4 Hz/√Hz at 1 MHz offset frequency, limited by the phase noise floor of the measurement instrument.

I. INTRODUCTION

Tunable continuous millimeter electrical wave sources are the basis of a wide array of applications from the rovibrational spectroscopy of molecules [START_REF] Mouret | Versatile sub-THz spectrometer for trace gas analysis[END_REF] to radar applications [START_REF] Garenaux | Recent Breakthroughs in RF Photonics for Radar Systems[END_REF]. The generation of such sources by a beat note of two optical carriers enables a wide tunability over hundreds of GHz frequencies [START_REF] Alouini | Dual Tunable Wavelength Er :Yb : Glass Laser for Terahertz Beat Frequency Generation[END_REF][START_REF] Wake | Optical generation of millimeter wave signals for fiber-radio systems using a dual-mode DFB semiconductor laser[END_REF].

For a compact, low cost, versatile and all-fiber system design, we choose two similar commercial DFB diode lasers to produce the beat note rather than solid state and extended cavity lasers, at the expense of a larger linewidth. Furthermore, laser diodes provide reliability and wavelength tuning without mode jump. We use the temperature of the laser chips in order to tune each laser wavelength and obtain the desired beat note frequency on a scale of hundreds of GHz. We also change the laser current to bring each laser optical carrier to resonance of a single Fabry-Perot cavity. We then have a beat note frequency equal to a multiple of the cavity free spectral range. The frequency noise of the beat note is then not sensitive at first order to the common mode cavity length fluctuations.

We report as a first step towards a millimeter wave source, the optical frequency stabilization of a tunable DFB laser on a fibered FP cavity in an all fiber system. We present in the second section of this paper the concept of the optical frequency stabilization by the using of a PDH (Pound Drever Hall) technique [START_REF] Drever | Laser phase and frequency stabilization using an optical resonator[END_REF] with fast and slow servo loop paths. In the third section, we show experimental measurement results of the frequency noise suppression by the servo loop and by the additional Brillouin fiber laser. We show also the phase amplitude coupling into the FP cavity and we discuss its effect on the relative intensity noise (RIN).

II. EXPERIMENTAL SETUP

The DFB diode laser (EBLANA) has a 112 kHz linewidth and a 150 Hz/√Hz frequency noise floor extending over 100 MHz. Because of this wide frequency noise floor of the laser, we have created at first a LT spice model [START_REF]Design Simulation and Device Models[END_REF], in order to determine a unity gain frequency such that the root mean square values of both error and correction signals do not saturate. A high unity gain frequency will increase the frequency noise suppression band. The high unity gain frequency is limited to 6 MHz extra loop delay in this configuration; for that we have worked to decrease the open loop delay by shortening the servo loop path to a minimum, and we allowed for a larger frequency correction bandwidth by using two different actuators. Furthermore, the LTspice model allowed us to optimize the design of the correction electronics and to select for each function the fastest operational amplifiers.

In the Fig. 1, we show the scheme of the DFB laser diode stabilization on the fibered FP cavity with a 1 MHz linewidth and a 1 GHz free spectral range. The DFB laser is operated at 1549 nm at 25°C, and generates a 4.3 mW optical power at 192 Towards optical fiber synthesis of millimeter waves mA injection current by a low noise driver (VESCENT).

To generate the error signal, we used a PDH technique. The optical carrier is phase modulated at a 26 MHz modulation frequency f m . The phase modulated wave was injected in the cavity through a 50/50 coupler used as a dual polarization fibered circulator. A frequency-filtered optical signal is transmitted through the cavity. The reflected optical signal is detected by a trans-impedance photodiode with a 110 MHz bandwidth. The output voltage is mixed with a phase shifted modulation signal at f m in order to give the error signal. This error signal enters in an electronic control circuit with proportional and integrator function filters in order to provide a stable servo loop. This circuit was designed to maximize the unity gain frequency and minimize the error signal. The correction signal was divided over two different actuators, a fast (1) and slow (2) correction paths. First, an electro-optical phase modulator (EO-2) with a 150 MHz bandwidth and a 3.2 V Vπ was used to adjust the phase of the laser; the optical beam instantaneous frequency correction is proportional to the time derivative of the applied voltage. The fast loop had a 6 MHz bandwidth. This phase modulator was not able to correct the low frequency components of the instantaneous frequency fluctuations; for that we used a second actuator by introducing a bias on the driver current with a 127 MHz/mA coefficient; the optical frequency and the injection current are proportional by the Henry factor in a semiconductors [START_REF] Henry | Theory of the linewidth of semiconductor lasers[END_REF]. The slow path also avoids the saturation of the fast correction signal by reducing its magnitude over a 350 kHz bandwidth.

We have also developed a Brillouin fiber laser cavity [START_REF] Mihélic | Ultrahigh resolution spectral analysis based on a Brillouin fiber laser[END_REF] at the output of the FP cavity in order to reduce the stabilized DFB laser linewidth. We use a 100 m highly nonlinear fiber as a medium gain. The output of the Brillouin fiber laser is detuned by 9.6 GHz frequency.

III. EXPERIMENTAL RESULTS

In Fig. 2, we show the linear spectral density of the frequency noise of our DFB diode laser before and after locking, as well as downstream of the Brillouin fiber laser. The frequency noise of the free running laser (curve A) was measured in an autoheterodyne setup [START_REF] Schimpe | Characterization of frequency response of 1.5 µm InGaAsP DFB laser diode and InGaAs PIN photodiode by heterodyne measurement technique[END_REF]. It comprises in the first arm an acousto-optic modulator at 80 MHz and in the other arm a 𝐿 = 700 m length standard fiber. The curve B represents the measure of the error signal calibrated by the transfer function of the measurement chain, it displays a frequency noise suppression down to 3.10 -1 Hz/√Hz at 80 kHz carrier offset frequency. We calculate a 100 kHz root mean square excursion frequency value in the error signal. We also measure the frequency noise of the 9.6 GHz beat note between the stabilized laser in the cavity transmission used as a pump and the Brillouin laser output (curve C). We observe a degradation of the frequency noise in the cavity transmission below the 200 kHz offset frequency with respect to the error signal. We consider that this is due to an amplitude-phase coupling into the FP cavity originated from the optical power noise. Finally, in the curve D we show the auto-heterodyne measurement of the Brillouin output pumped by the stabilized laser. We have frequency noise suppression down to 4.10 -1 Hz/√Hz at 100 kHz offset frequency: this corresponds to a phase noise at -108 dBc/Hz of the optical carrier. Above 100 kHz offset frequency the auto-heterodyne measurement is limited by the phase noise floor of the electrical spectrum analyzer (dashed line). Fig. 3 shows the linear spectral density of the relative intensity noise (RIN) in 1/√Hz. In the locked mode (curve A), the relative intensity noise in the cavity transmission is degraded with respect to the free running laser (curve B). We consider that is a phase-amplitude (PM-AM) coupling into the FP cavity; we calculate it with the following procedure: we generate a time-domain envelope data whose frequency noise spectral density is the measured one; we then filter the instantaneous frequency by a low pass filter at a cut-off frequency 𝑓 𝑐 where 𝑓 𝑐 is the cavity half linewidth, to obtain 𝜈 𝑓 (𝑡); then we apply a nonlinear transformation 0.5 𝜈 𝑓 2 (𝑡)/𝑓 𝑐 2 , followed by a low pass filter. We then estimate the linear spectral density of the amplitude fluctuations (curve C) in good agreement with the measured one.

IV. CONCLUSION

We present in this paper a stabilization of the optical frequency of a DFB laser diode at 1549 nm tunable over 2 nm on a fibered Fabry-Perot cavity in an all fiber system. The PDH technique with a two-path servo loop has enabled us to achieve a unity gain frequency up to 6 MHz. A frequency noise suppression down to 3.10 -1 Hz/√Hz at 100 Hz offset frequency in the error signal has also been demonstrated and we noticed a relative intensity noise degradation to 2.10 -5 1/√Hz at 100 Hz in the cavity transmission. We have also used a Brillouin fiber laser in order to refine the stabilized laser linewidth and obtain frequency noise suppression down to 4.10 -1 Hz/√Hz at 100 kHz offset frequency.

We could improve the unity gain frequency by shorter or integrated fibered components. In a further step, the stability of the cavity would be improved by the stabilization of its free spectral range on a radio frequency synthesizer. Polarization beam splitters (PBS-1 and PBS-2) in the assembly (Fig. 1) will allow the future generation of a beat note between two DFB lasers.

Fig. 1 .

 1 Fig. 1. Scheme of the all fiber system (DFB laser diode, cavity) with a two path electronic servo loop. EO: electro-optic modulator; PBS: polarizing beam splitter.

Fig. 2 .

 2 Fig. 2. Frequency noise linear spectral densities of the free running DFB laser (curves A) and locked represented by the error signal (curve B) and in the cavity transmission (curve C). Frequency noise of the Brillouin fiber laser pumped by the stabilized DFB laser (curve D). The frequency noise floor of the electrical spectrum analyzer is in dashed line.

Fig. 3 .

 3 Fig. 3. Relative intensity noise linear spectral densities of the free running DFB laser (curve B), locked (curve A) and calculated from the PM-AM (Phase-Amplitude) coupling into the cavity (curve C).