Henri Hansen
email: henri.hansen@tut.fi

Marta Kwiatkowska
email: marta.kwiatkowska@cs.ox.ac.uk

Hongyang Qu
email: hongyang.qu@cs.ox.ac.uk

Partial order reduction for model checking Markov decision processes under unconditional fairness

Keywords: Probabilistic model checking, partial order reduction, Markov decision processes, unconditional fairness

Fairness assumptions are needed to verify liveness properties of concurrent systems. In this paper we explore the so-called unconditional fairness in Markov decision processes (MDPs), which is a prerequisite for quantitative assumeguarantee reasoning. Unconditional fairness refers to executions where all processes are guaranteed to participate. We prove that realisability of unconditional fairness coincides with the absence of partial deadlocks, i.e., end components where a process suffers from starvation. We propose a weak variant of the stubborn set method to reduce MDPs, while preserving the realisability of unconditional fairness and maximal probabilities of reaching bottom end components under fair schedulers.

I. INTRODUCTION

Probabilistic model checking refers to a range of automated and systematic techniques for verification of systems exhibiting probabilistic behaviours. It has received much attention in the last two decades and has been applied to various problems, from communication protocols to biological systems. With continuous improvement of the technique, the size of systems that can be handled by probabilistic model checkers has increased. Nevertheless, the larger systems exceed the capacity of available tools. Recently, compositional verification has been introduced for probabilistic model checkers [1], [START_REF] Forejt | Quantitative multi-objective verification for probabilistic systems[END_REF]. In compositional verification, a system is verified by analysing modules of the system individually. Due to the probabilistic and concurrent characteristics of the problem, fairness conditions in general, and unconditional fairness in particular, are required for the verification of probabilistic liveness properties [START_REF] Forejt | Quantitative multi-objective verification for probabilistic systems[END_REF].

In this paper, we present and implement an approach to establish probabilistic properties under unconditional fairness. In our approach, we incorporate partial order reduction to tackle the so called state space explosion problem. Partial order reduction has been studied intensively for non-probabilistic system, such as [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF], [START_REF] Godefroid | Using partial orders to improve automatic verification methods[END_REF], [START_REF] Peled | All from one, one for all: on model checking using representatives[END_REF], [START_REF] Mcmillan | A technique of state space search based on unfolding[END_REF]. For probabilistic systems, only the ample set approach has been investigated [START_REF] Baier | Partial order reduction for probabilistic systems[END_REF], [START_REF] Baier | Partial order reduction for probabilistic branching time[END_REF], [START_REF] D'argenio | Partial order reduction on concurrent probabilistic programs[END_REF], [START_REF] Baier | Quantitative analysis under fairness constraints[END_REF] so far as ample sets are comparably easier to compute than stubborn sets, in spite of the better reduction from the latter. [START_REF] Größer | Partial order reduction for markov decision processes: A survey[END_REF] gave a survey on these methods. Our paper is the first to combine the stubborn set approach and probabilistic model checking. In addition, we adopt the weak stubborn set method, instead of the well-known (strong) stubborn set, to obtain more compact reduced models. Weak stubborn sets are often regarded as impractical, but Hansen and Wang have recently described an efficient and accessible method [START_REF] Hansen | Compositional analysis for weak stubborn sets[END_REF]. It is worth noting that our approach can also be applied to probabilistic verification without fairness constraints. Another contribution of this paper is the realisability check for unconditional fairness, which can be performed efficiently on the nonprobabilistic version of the original model. This is very useful for examining the compatibility of the components in a parallel composition.

This paper is structured as follows. Section II presents the background knowledge about LTSs, MDPs and unconditional fairness (UF). In Section III, we discuss our approach for checking realisability of UF in MDPs, which can be reduced to the realisability of UF in LTSs. In Section IV, we use the weak stubborn sets to generate a reduced model and to compute the maximum/minimum probability of reaching a set of target states under unconditional fairness. The model checking algorithm for computing the max/min probability is explained in Section V. We briefly discuss some implementation choices and present experimental results in Section VI. We conclude the paper in Section VII.

II. PRELIMINARIES

A. MDPs and LTSs

MDP An MDP is a tuple M = (S, Σ, Steps, s) where Steps associates a probability distribution function µ to each enabled action a at s. For convenience, we assume ⊥ simply assigns the value zero to all states.

• S is a finite set of states, • s ∈ S is the initial state, • Σ is a finite set of actions, • Steps : (S × Σ) → Dist(S)
There are two steps to determine a successor state of s. First, an action is chosen non-deterministically from the set of enabled actions. Next, the probability of moving to state s is decided by µ, i.e., µ(s ). We assume there are no terminating states in MDPs.

An action a is said to be deterministic if for all states Steps(s, a) is either ⊥ or the Dirac-distribution, i.e., it assigns the probability 1 to some state. If an action is not deterministic, we say that it is probabilistic.

A path in an MDP is a non-empty sequence of the form

s 0 a1 ----→ s 1 a2 ----→ s 2 . . .
where for all i ≥ 0, s i ∈ S, and there is some µ i+1 such that µ i+1 = Steps(s i , a i+1 ) and µ i+1 (s i+1 ) > 0. We use ω(i) to denote the ith state in the path ω, ω f in to denote a finite path, last(ω f in ) to denote the last state in ω f in , and P ath f in s (P ath s ) to denote the set of all finite (infinite) paths starting in state s. Moreover, the ith action in ω is represented by step(ω, i), and the i-length prefix of ω is denoted ω i .

The sequence of actions that occur in ω is denoted by Σ(ω). An execution of M, from s to s n , is denoted s

a1•••an ----→ s n ,
and means that there is some path ω such that Σ(ω) = a 1 • • • a n and last(ω) = s n .

The probability measure of a finite path, denoted p(ω), is defined as the product n i=1 µ i (ω(i)). In addition, we define the probability of executions as

• p(s a -→ s ) = Steps(s, a)(s ), • p(s a1•••an ----→ s ) = s * ∈S p(s a1•••an-1 ------→ s * )Steps(s * , a n )(s ).
To resolve the non-deterministic choices when we execute an MDP, we employ an adversary to select an action based on the history of choices made so far.

Adversary An adversary A of an MDP M is a function mapping every finite path ω f in onto an element A(ω f in ) of the set en(last(ω f in )). We use Adv M to denote the set of all possible adversaries of the MDP and, for any adversary A, we use P ath A s denote the subset of P ath s defined as

{ω | ω(0) = s ∧ ∀i.ω(i) A(ωi) ----→ ω(i + 1)}
We say that the paths in P ath A s are controlled by A. End component An end component (EC) of M is a pair (R, A) such that R ⊆ S, A : R → 2 Σ and:

• ∅ = A(s) ⊆ en(s) for every s ∈ R, • For each a ∈ A(s) and s ∈ R, {s | Steps(s, a)(s ) > 0} ⊆ R, • R is strongly connected in the transition-state graph of M.
A bottom EC is an end component with the condition A(s) = en(s) for all states s ∈ R. Unless stated otherwise, we assume an EC to be maximal, i.e., that there is no end component (R , A ) such that R ⊂ R .

Parallel composition Let M i = (S i , Σ i , Steps i , s i ) be MDPs. Then the parallel composition M 1 ||M 2 is the MDP (S, Σ, Steps, s), where:

• S = S 1 × S 2 , • Σ = Σ 1 ∪ Σ 2 , • s = (s 1 , s 2 ), • Steps((s 1 , s 2 ), a) = µ 1 × µ 2 iff -a ∈ Σ 1 ∩ Σ 2 , Steps 1 (s 1 , a) = µ 1 and Steps 1 (s 2 , a) = µ 2 , or -a ∈ Σ 1 \Σ 2 , Steps 1 (s 1 , a) = µ 1 , and µ 2 = η s2 , or -a ∈ Σ 2 \Σ 1 , Steps 2 (s 2 , a) = µ 2 and µ 1 = η s1
where µ 1 × µ 2 is the product of distributions µ 1 and µ 2 , and

η si ∈ Dist(S i ) is the Dirac-distribution on s i ∈ S i .
For a state s of the parallel composition of n components, we write s(i) for the state of the ith component and en

i (s) = {a ∈ Σ i | s(i) a -→ i }.
LTSs are a special type of MDPs 1 , where each distribution is a Dirac-distribution. To distinguish LTSs from the full class of MDPs, we write L = (S, Σ, ∆, s) for an LTS. An end component in LTSs is also called a strongly connected component (SCC).

B. Computing maximum reachability probabilities

Verification of MDPs usually requires properties to be specified in temporal logics, e.g., PCTL [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF], [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF] and LTL [START_REF] Pnueli | The temporal logic of programs[END_REF]. Reachability probabilities are one of the key properties central to probabilistic verification. In this paper, we focus on maximum reachability probabilities of reaching a set of target states F ⊆ S from s, over all possible adversaries:

p max s (F) = sup A∈Adv M p A s (F) p A s (F) = Prob A s ({ω ∈ Path A s | ∃i . ω(i) ∈ F}).
Our technique can be extended to minimum reachability probabilities in a straightforward manner.

Usually, p max s (F) can be computed by value iteration or linear programing. We use value iteration with partial order reduction, as we dynamically prune transitions to speed up the state space exploration and probability computation. In value iteration, a vector is used to store the current estimation of the probability of states. Iteratively, the vector is updated by the multiplication of itself and the probabilistic transition relation, which is represented as a matrix. Let p max,k s be the probability of state s in the kth iteration. Initially, i.e., k = 0, the states in F have probability one in the vector, and other states have probability zero. For k > 0, p max,k s is defined as follows:

p max,k s := 1 if s ∈ F max µ∈Steps(s) s ∈S µ(s ) • p max,k-1 s if s ∈ S\F.
Eventually, p max,k s is guaranteed to converge to p max s (F). In practice, precomputation, such as P rob0A [START_REF] Bianco | Model checking of probabilistic and nondeterministic systems[END_REF] and P rob1E [START_REF] Alfaro | Formal verification of probabilistic systems[END_REF], is performed before value iteration starts in order to identify states that have either probability one or zero. These states are excluded from value iteration to save time and space. However, precomputation cannot be applied before the state space is generated by partial order reduction. Therefore, we omit it in this paper. We also write p max s , instead of p max s (F) for simplicity. In [START_REF] Ciesinski | Reduction techniques for model checking Markov decision processes[END_REF], [START_REF] Kwiatkowska | Incremental quantitative verification for Markov decision processes[END_REF], an MDP is decomposed into SCCs first and value iteration is carried out in each SCC in the reversed topological order, rather than in the whole model directly. Experimental results in both papers show that computation time can be dramatically reduced in this way.

C. Unconditional fairness

Unconditional fairness is crucial in probabilistic assumeguarantee reasoning [START_REF] Forejt | Quantitative multi-objective verification for probabilistic systems[END_REF], as it guarantees that the intermediate adversary computed during reasoning is not partial.

Unconditional fairness Given an MDP

M = (S, Σ, Steps, s) composed of n components M 1 , . . . , M n , i.e., M = M 1
. . . M n , an infinite path π is unconditionally fair, denoted π |= f air, if for each component M i there exists an action a ∈ Σ i that occurs infinitely often in the path. An adversary A is unconditionally fair, or fair for short, if for every state s ∈ S, every infinite path starting at s controlled by A is unconditionally fair.

Realisability Unconditional fairness is realisable in an MDP M if there exists some fair adversary for M.

A state is visited by an adversary if the state is reached from the initial state in an execution controlled by the adversary.

Generalised fair adversary When unconditional fairness is not realisable in an MDP M , an adversary A is generalised fair (or fair for short) if for every state s ∈ M that is visited by A, all infinite paths starting at s are fair.

If there does not exist any fair adversary, then the maximum probabilities are restricted to generalised fair adversaries.

To compute the maximum probabilities for an MDP under unconditional fairness, we need to reduce the model, i.e., leave out the parts where fairness is not realisable. Basically, states that cannot be visited by any fair adversary should be removed, as suggested in [START_REF] Baier | Quantitative analysis under fairness constraints[END_REF], so that we only perform value iteration over the remaining states. We address this issue in Section V. Example Figure 1 shows an MDP with four components. Actions x, y and z are synchronised, and the others are local. Unconditional fairness is not realisable in this model because, in any global state containing s 1 , no actions in M 2 and M 4 can be executed. The maximum probability of reaching the target state s 2 , marked by a double circle in the figure, is 0.8 if we do not consider fairness, while it becomes 0.7 under unconditional fairness.

III. CHECKING REALISABILITY

In the rest of the paper, let L = (S, Σ, ∆, s) be composed of n components L 1 , . . . , L n , i.e., L = L 1 . . . L n , and M = M 1 . . . M n . Let Reach(s) ⊆ S be the set of states that can be reached from state s.

Partial deadlock

The process L i is partially deadlocked in state s ∈ S if for each s ∈ Reach(s) and each a ∈ Σ i we have s a -→. A partial deadlock of L i is a bottom SCC of L such that L i is partially deadlocked in all the states of the SCC.

Theorem 3.1: Unconditional fairness is realisable in L iff, for all L i , there does not exist a partial deadlock in L.

Proof: "⇒". Suppose there exists a partial deadlock Ω for L i . Consequently, L i is partially deadlocked in any state s ∈ Ω. Then there does not exist an infinite path π starting at s such that action a appears infinitely often in π for some a ∈ Σ i . This is in contradiction with the definition of unconditional fairness.

"⇐". Suppose unconditional fairness is not realisable in L. Thus we can find a state s ∈ S where it holds that, for all infinite paths starting at s, there is some i such that no a ∈ Σ i occurs infinitely often. In particular, this holds for all infinite paths that lead from s to some bottom SCC C, and visit all the states of C in that SCC infinitely often. Therefore, no a ∈ Σ i is enabled in any state of C, and C is a deadlock for L i .

In [10, Theorem 1], Baier et. al showed that a strong/weak fairness constraint is realisable if and only if, for every state s in an MDP M, there exists a path with nonzero probability leading to a fair maximal end component (FMEC). Since unconditional fairness can be formulated as a strong fairness constraint, this result still holds. An FMEC in our case is a maximum end component that contains at least one action for each M i . Let L M = (S M , Σ M , ∆ M , s M ) be an LTS obtained by converting probabilistic choice in an MDP M = (S, Σ, Steps, s) into non-deterministic choices as follows:

• S M = S, • s M = s, • For any s ∈ S and any a ∈ Σ, a s ∈ Σ M and
(s, a s , s ) ∈ ∆ M iff Steps(s, a)(s ) > 0. Synchronisation of actions in the resulting LTS-parallel composition is somewhat involved; all the actions resulting from actions with the same labels are synchronised, i.e., multi-way synchronisation, which does not affect partial order reduction [START_REF] Hansen | Compositional analysis for weak stubborn sets[END_REF].

Theorem 3.2: Unconditional fairness is realisable in an MDP M iff, for all L Mi , there does not exist a partial deadlock in L M .

The proof is similar to that of Theorem 3.1, and hence omitted here.

T -reduction Let L = (S, Σ, ∆, s) be an LTS, and let T : S → 2 Σ be some function. Then the T -reduction of L is the LTS (S T , Σ, ∆ T , s), where S T and ∆ T are minimal sets such that:

• s ∈ S T ; • if s ∈ S T , (s, a, s ) ∈ ∆ and a ∈ T (s), then s ∈ S T
and (s, a, s ) ∈ ∆ T .

We also use the subscript s a -→ T when talking about the reduced LTS.

Stubborn set Let (S, Σ, ∆, s) be an LTS, and let T : S → 2 Σ . we say that the function T is a stubborn set generator if, for all s ∈ S, T (s) satisfies the following properties:

D0 T (s) ∩ en(s) = ∅ iff en(s) = ∅, D1 For all a ∈ T (s) and b 1 , . . . , b n ∈ Σ\T (s), and s ∈ S, if s b1•••bna -----→ s then s ab1•••bn -----→ s , D2 Either en(s) = ∅, or there exists a ∈ T (s) such that, for all b 1 , . . . , b n ∈ Σ \ T (s), s b1•••bna -----→ s .
An action a ∈ T (s) with this property is called a key action.

The stubborn set defined above is sometimes referred to as a weak stubborn set, in contrast to the (strong) stubborn set. The difference is in the condition D2, which for strong stubborn sets is replaced by a condition that requires that all enabled actions of T (s) are key actions. If we reduce an LTS with a (weak or strong) stubborn set generator, it is known that the reduced LTS contains exactly the deadlocks of the original LTS [START_REF] Valmari | Stubborn set methods for process algebras[END_REF]. A case where D0-D2 are not enough to preserve partial deadlocks can also be found in Figure 1. In the state (s 0 , r 0 , w 1 , v 0 ), the set {τ 2 } is a legitimate stubborn set, but when M 1 is in state s 1 , M 2 and M 4 are partially deadlocked. What is more, in the resulting reduced LTS, there is an "extra" partial deadlock induced, as the reduced LTS would stay in that state for ever, and all other processes would be "partially deadlocked".

The phenomenon is a manifestation of the so-called ignoring problem [START_REF] Valmari | A stubborn attack on state explosion[END_REF], [START_REF] Evangelista | Solving the ignoring problem for partial order reduction[END_REF], whereby a cycle of actions is considered completed, with some transition enabled on the way and never explored. When looking for global deadlocks, this is not a problem. However, the stubborn set conditions do not guarantee that we find all partial deadlocks, and thus the problem needs to be addressed.

To solve the problem, an additional constraint must be imposed on stubborn sets. This is the safety condition [START_REF] Valmari | The state explosion problem[END_REF]:

S For every state s in S T and every b ∈ en(s), there exists some a 1 , . . . , a n such that s = s 0

a1 -→ s 1 a2 -→ • • • an --→ s n ,
T = (L 1 || • • • ||L n ) T contains a partial deadlock if and only if L = (L 1 || • • • ||L n ) does.
Proof: The "if"-part follows from Lemma 3.3. Let C be a bottom SCC of L T that is a partial deadlock for L j in L T . For proof by contradiction, assume there is no partial deadlock for L j in L. Let s 0 ∈ C and b ∈ Σ j such that s 0 a1•••anb -----→ is minimal among states of C. An obvious contradiction comes if for some i, a i ∈ T (s 0 ), as taking minimal such i would give s 0 ai -→ T s 0 and there would be a path of length n -1 to a state where b is enabled.

Therefore, assume that each a i / ∈ T (s 0 ). S guarantees a path of key actions

x 1 , x 2 , • • • , x m such that s 0 x1•••xm
-----→ T s 0 and a 1 ∈ T (s 0 ). D1 guarantees, with a simple induction over m, that either one a i is in a stubborn set in one of the states on the path, contradicting minimality that was previously assumed, or that minimality is contradicted by the state s * such that s 0 a1 -→ T s * .

IV. PRESERVING MAX PROBABILITIES UNDER UNCONDITIONAL FAIRNESS

A. Preserving terminal states

Probabilistic stubborn set Let M = (S, Σ, Steps, s) be an MDP. We say that the function T : S → 2 Σ is a probabilistic stubborn set generator if it satisfies the following properties: To preserve safety properties and partial deadlocks for MDPs, we need to tackle the ignoring problem in end components. There are various ways of doing this in the context of partial order reduction for MDPs. Such conditions are often referred to as cycle conditions. Two variants in the literature [START_REF] Baier | Partial order reduction for probabilistic systems[END_REF], [START_REF] Baier | Partial order reduction for probabilistic branching time[END_REF] ----→ s n = s 0 there exists a state s i which is fully expanded, i.e., T (s) = en(s). Of the two, A3b is clearly stronger, but also easier to implement, which is why most practical implementations adopt it. However, we do not actually need such powerful conditions if we are concerned only with reachability and other safety properties. Instead, we use the S condition as it stands.

D0 T (s) ∩ en(s) = ∅ if and only if en(s) = ∅. D1 For every a ∈ T (s) and b 1 , . . . , b n / ∈ T (s), s b1•••bna -----→ s implies p(s b1•••bna -----→ s ) = p(s ab1•••bn -----→ s ). D2 If T (s) = ∅,
It is a well-known problem for maximal probabilities, first identified in [START_REF] Baier | Partial order reduction for probabilistic systems[END_REF], [START_REF] D'argenio | Partial order reduction on concurrent probabilistic programs[END_REF], that the usual non-probabilistic rules do not guarantee the preservation of maximal probabilities. This is true with rules D0-D2 and S. The most common fix for this probabilistic branching problem is to impose a rule:

A5 If s b1•••bnc -----→ such that b 1 , . . . , b n , c / ∈ T (s)
, and c is probabilistic, then |T (s) ∩ en(s)| = 1. Note that, for ample sets, in which we assume T (s) ⊆ en(s), this rule seems to be different than for stubborn sets. The difference, however, is only superficial. Rule D1 disallows actions outside the stubborn set to enable disabled actions within the stubborn set. The intricacies of the stubborn set method do allow, however, a more careful analysis of the condition. Rule A5 is hard to implement, as mentioned in [START_REF] Baier | Partial order reduction for probabilistic systems[END_REF], which is why a number of heuristics have been proposed for it. For instance, in [START_REF] Baier | Partial order reduction for probabilistic systems[END_REF], a stronger version is given, which requires that T (s) ∩ en(s) is a singleton unless it contains all the enabled actions.

We propose to replace A5 with another rule that is stronger in the context of stubborn sets, in the sense that, with the support of D1, this rule implies A5. This rule is significantly weaker than the simplistic rule of always requiring singleton sets, and should allow for more reduction. PB If |T (s) ∩ en(s)| = 1, then T (s) contains all probabilistic actions in the model. -----→, c be probalistic and b 1 , . . . , b n deterministic. PB implies that c ∈ T (s). D1 guarantees that either c is enabled at s, or at least one b i ∈ T (s). In both cases, then, A5 is satisfied. The exact relationship of PB and A5 is unknown to us. On the face of it, PB does seem stronger, because it requires that disabled probabilistic actions are inside the set, but definite evidence is lacking at this time.

Theorem 4.2: If T (s) satisfies D0-D2, S and PB, then the maximum probability of reaching each bottom EC is preserved through T -reduction.

Proof: Let C be a bottom EC in the original MDP M. Let us denote by p max s0 (C) the maximum probability of ending in C from s 0 in M, and by q max s0 (C) the maximum probability in the reduced MDP M T . If s 0 ∈ C, then naturally p max s0 (C) = q max s0 (C). This also holds if p max s0 (C) = 0, i.e., C is not reachable from s 0 . We assume this is not the case.

It is known that the maximum probability of reaching C can be realised by a memoryless adversary. Let A be such an adversary, and A(s 0 ) the only action chosen by A for s 0 . We prove that there exists a memoryless adversary A T in M T such that p A s0 (C) = q A T s0 (C), where p A s0 (C) and q A T s0 (C) are the probability of reaching C under A and A T respectively.

If A(s 0 ) ∈ T (s 0 ), then A T (s 0 ) = A(s 0 ), and nothing else is needed. Otherwise, to show that p A s0 (C) = q A T s0 (C), we show that we can choose b) PB guarantees that, if T (s 0 )∩en(s 0 ) is not a singleton (which means that A(s 0 ) is not probabilistic), then in any sequence s 0 a1•••an ----→ s n that starts with A(s 0 ), either the first probabilistic action or some action before it is in T (s 0 ). Let k be the index of such an action. D1 and the fact that a i is deterministic for i < k guarantee that:

A T (s 0 ) = b such that p max s0 (C) = s 0 µ(s 0 ) • p max
1) s 0 a1•••a k-1 ------→ s k-1 is
a deterministic sequence for some state s k-1 , and 2) for each s 0 such that Steps(s 0 , a k )(s 0 ) > 0, we have s 0

a1•••a k-1 ------→ s k-1 for some state s k-1 , and
Steps(s k-1 , a k )(s k ) = Steps(s 0 , a k )(s 0 ).
Again, this holds for all the sequences such that A(s i ) = a i+1 , so we have that p max s0 (C) =

s 0 µ(s 0 )p max s 0 (C).
When case b) happens, one action from the sequence leading to the SCC is executed. On the other hand, the a) case cannot happen indefinitely: S guarantees that, because a 1 ∈ en(s), there is a sequence of key actions that lead to a state where a 1 is in the stubborn set, and in the a) case, there is only a single key action, so either a 1 is eventually in the stubborn set or the b) case materialises. Theorem 4.2 does not consider the maximum probabilities under unconditional fairness. We have to prune actions that can lead to a partial deadlock in order to do so. The following theorem guarantees that the maximum probability under unconditional fairness in a reduced MDP is the same as in the original MDP.

Theorem 4.3: If T (s) satisfies D0-D2, S and PB, then the maximum probability of reaching a bottom FMEC under unconditional fairness is preserved through T -reduction.

Proof: Note that a bottom FMEC is a bottom SCC that has no partial deadlock, or an FMEC from which only partially deadlocking bottom SCCs can be reached.

In the first case, we only need to consider states where we can reach a number of bottom SCCs, some of which are FMECs. Otherwise Theorem 4.2 suffices. Let s ∈ S T and let A F be the fair adversary that maximises the probability. A F will never assign an action that leads to a state from which the maximal probability of reaching a fair bottom SCC is less than one.

Using a construction similar to the one in the proof of Theorem 4.2, we can prove that either there is some action b ∈ T (s) such that A F might as well assign b, or that there is some sequence of key actions that lead to the execution of A F (s), and hence the maximum probability of reaching the FMEC is the same.

V. MODEL CHECKING ALGORITHM

A. Generating basic stubborn sets

The concept of independence of actions is central in most partial order reduction methods. It is important also for the practical implementation of stubborn sets.

Traditionally, independence means that, when two actions are enabled at the same state, they commute in the sense that both actions can always be taken and the result is independent of the order in which they are executed. We shall refer to such independence as strong independence.

Strong Independence Let M = (S, Σ, Steps, s) be an MDP and a, b ∈ Σ. We say that a and b are strongly independent iff, for all states s ∈ S such that a ∈ en(s) and b ∈ en(s), we have:

• for all s 1 ∈ S, s a -→ s 1 ⇒ b ∈ en(s 1 ), • for all s 1 ∈ S, s b - → s 1 ⇒ a ∈ en(s 1 ), • for all s ∈ S it is true that p(s ab -→ s ) = p(s ba -→ s ).
If a and b are not strongly independent, they are strongly dependent.

A careful examination of the rules for stubborn sets, however, reveals that D1 is not entirely symmetric. Commutativity of an inside action with some sequence of outside actions is required only if executing a sequence of outside actions, followed by an inside action, is possible to begin with. In fact, D1 in no way rules out the possibility of a becoming disabled by a sequence of b-actions. What is more, D2 requires only that we have at least one action that cannot be disabled by outside sequences.

The so-called weak independence is designed to capture this asymmetry. We require commutativity only if a can be executed after b. The relation does allow for b and a to disable one another.

Weak Independence Let M = (S, Σ, Steps, s) be an MDP and a, b ∈ Σ. We say that a is weakly independent of b iff, for all states s ∈ S such that s ba -→, it holds that a ∈ en(s) and:

• for all s 1 ∈ S, s a -→ s 1 ⇒ b ∈ en(s 1 ), • for all s 1 ∈ S, s b - → s 1 ⇒ a ∈ en(s 1 ), • for all s ∈ S, it is true that p(s ab -→ s ) = p(s ba -→ s ).
If a is not weakly independent of b, we say that a is weakly dependent with b.

We emphasise the difference: the requirement that a and b commute is the same as in strong independence, but it is "triggered" only if a can be executed after b. In fact, if we know that b completely disables a, then a is weakly independent of b.

The concept of causes and causality is also helpful in designing a practical method for calculating stubborn sets. D1 implies that, if a is a disabled inside action, then no sequence of outside actions may enable a. Verifying this can be computationally expensive, and, what is more, a simple binary relation for actions may not fully capture all the intricacies of action sequences enabling one another.

We introduce the following notational convention for 3ary relations: if Q is a 3-ary relation, we write in the following (a, c, -) ∈ Q if there exists some b such that (a, c, b) ∈ Q. We define the causality relation as follows. The intuition of this definition is as follows. For a disabled action a, there is some set of causes that need to be "triggered" before a can happen. This is some subset of C. Intuitively, C can be thought of as a set of guards or conditions that must be met in order for actions to become enabled. For example, in Petri nets, "actions" would be the structural transitions and "causes" would be the places that are empty. Now, if a is disabled in the current state, but enabled after some sequence of actions, then all the causes of a must be triggered by some action.

Causality relation

Note that the definition is conditioned on s, i.e., it is dynamic. The set of causes can of course be static; the only dynamic feature is when a cause is "active" (e.g., a true guard) and when it is "inactive" (e.g.., a false guard). In a parallel composition, for instance, the "inactive" causes can simply be the components where the corresponding action is disabled, and "active" causes are those where it is enabled. The action becomes enabled when all causes are active.

Example In Figure 1, actions a and b are strongly dependent of each other, as one disables the other. Similarly, y and z, as well as y and c are strongly dependent. Action c is weakly dependent of y, but not the other way around, because the first condition in the definition of weak independence is violated, i.e., (s 2 , r 1 , w 0 , v 0 ) c -→ (s 2 , r 1 , w 1 , v 0 ) ⇒ y ∈ en(s 2 , r 1 , w 1 , v 0 ). For the same reason, z is weakly dependent of y. Actions a and b are the causes of x, y and z (through component M 1 ); x is a cause of z, and y is a cause of x (through component M 2 ).

Strong and weak dependency and causality are relations on top of which we shall build what we call a dependency graph. The role of this graph is to capture the information in the relations so that we can calculate stubborn sets.

Dependency graph Let M = (S, Σ, Steps, s) be an MDP and s ∈ S be a state. A dependency graph for s is a tuple (E, D, C, ; S , ; W , ; C ) such that (E ∪ D ∪ C, ; S ∪ ; W ∪ ; C ) is a directed graph satisfying the following conditions:

• E = en(s), In the above definition, E is the set of enabled actions, D the set of disabled actions, and C the set of "inactive" causes for the actions in D. The relation ; C links the disabled actions with their causes and causes to actions that can activate them.

• C = ∅ ∨ D = ∅, • D = Σ \ en(s), • ; S ⊆ E × Σ, • ; W ⊆ E × Σ, • ; C ⊆ (D × C) ∪ (C × Σ), • ∀a ∈ D : ∃c ∈ C : a ; C c. • for each v ∈ E

Stubborn set for dependency graph

A set V ⊆ Σ ∪ C is a stubborn set for G if 1) Either E = ∅ or V ∩ E = ∅, 2) If V ∩ E = ∅, then there exists a v ∈ V ∩ E, such that: {u | v ; S u} ⊆ V , 3) For each v ∈ V ∩ E, it holds that either {u | v ; S u} ⊆ V , or {u | v ; W u} ⊆ V , 4) For each v ∈ V ∩ C, it holds that {u | v ; C u} ⊆ V , 5) For each v ∈ V ∩ D we have {u | v ; C u} ∩ V = ∅.
We call these conditions the closure properties of the stubborn set. The first requirement is natural; V must contain some enabled action if there are any. The second requirement is there to make sure some key action is in the set. The third one requires that for each enabled action in V , either the weakly or the strongly dependent actions are in V . The fourth requirement says that if a cause is in V , then every action that can activate that cause must be in V ; and the last one that, if a disabled action is in V , at least one of its causes must also be in V . From the definition of causality, it follows that for at least one i ∈ {1, . . . , n}, b i ∈ V , which leads to contradiction. D2 follows from the fact that there is some a k ∈ V ∩ en(s) such that {u | a k ; S u} ⊆ V .

Relations for (weak or strong) dependency, and causality, can be safely approximated in a number of ways. In a parallel composition, a common heuristic is to consider all the actions inside a given component dependent on one another, but such relations will not benefit from weak dependency. One possibility is to analyse each component, as in [START_REF] Hansen | Compositional analysis for weak stubborn sets[END_REF], so that every component is searched for manifestations of dependency and causality. The causality is implemented so that, for every action a and every i such that a ∈ Σ i , there is a "cause" c i a , and (a, c i a , b) is in the causality relation if b enables a in some state of the ith component.

For shared variable models with, e.g., guarded commands, the effects of actions on guards need to be assessed. A common heuristic is to consider all write accesses as dependencies, but, again, a more nuanced approach is needed to make use of weak dependency.

Once the dependency and causality relations are known, and we know which causes are relevant at the current state, we can generate a dependency graph.

Example In the initial state (s 0 , r 0 , w 0 , v 0 ) in Figure 1, the dependency graph G = (E, D, C, ; S , ; W , ; C ) is as follows: spent on computing these relations was compensated by the much smaller models after reduction.

VII. CONCLUSION

In this paper, we first proved that realisability of unconditional fairness in MDPs can be carried out on their non-probabilistic abstractions to enable fast check. Then we proved the maximum probability of reaching some bottom EC under unconditional fairness is preserved by the weak stubborn set T -reduction. We also presented data structures and the model checking algorithm for computing such probability through T -reduction.

There are several possible future directions. The first is to extend our approach to allow arbitrary target states, rather than just bottom FMECs. Secondly, we would like to optimise our initial implementation to improve the overapproximations of computing dependency relation and conduct more case studies to explore the potential of weak stubborn sets. Computing the maximum probability under strong/weak fairness constraints via partial order reduction has been discussed in [START_REF] Baier | Quantitative analysis under fairness constraints[END_REF]. It would be very interesting to compare our approach with theirs.

  ∪ {⊥} is the probabilistic transition function. The probabilistic transition function Steps maps each state s ∈ S and action a ∈ Σ to an element of Dist(S) ∪ {⊥}. For each state s ∈ S, Steps defines a set of enabled actions en(s): en(s) = {a ∈ Σ | Steps(s, a) = ⊥}. We usually write s a -→ to denote a ∈ en(s).

Figure 1 .

 1 Figure 1. An MDP with four components M 1 , M 2 , M 3 and M 4

  all a i are key actions, and b ∈ T (s n ). Lemma 3.3 ([3],[START_REF] Valmari | The state explosion problem[END_REF]): Let T be a stubborn set generator for L such that T satisfies D0 -D2 and S. Then, for every bottom SCC C ⊆ S, C ∩ S T = ∅.Theorem 3.4: If the stubborn set generator T satisfies D0 -D2 and S, then the reduced LTS L

  then there exists at least one a ∈ T (s) such that for all b 1 , . . . , b n / ∈ T (s), s b1•••bn ----→ s implies s a -→. Such an action is called a key action. Reduced MDP Let M = (S, Σ, Steps, s) be an MDP and T be a stubborn set generator for M. We define the Treduced MDP, denoted M T = (S T , Σ, Steps T , s), as the minimal MDP that satisfies: if s ∈ S T , a ∈ T (s), then {s | Steps(s, a)(s ) > 0} ⊆ S T and Steps T (s, a) = Steps(s, a).

  include: A3a If (R, A) is an EC of M T and a ∈ s∈R en(s) then a ∈ s∈R T (s); A3b On each cycle s 0 a1•••an

Lemma 4 . 1 :

 41 If T (s) satisfies D0-D2 and PB, then it satisfies A5. Proof: Let |T (s) ∩ en(s)| = 1 and s b1•••bnc

s 0 (

 0 C), where µ = Steps(s 0 , b). S then guarantees that the execution can always make progress. a) If A(s 0 ) is probabilistic, then T (s 0 ) ∩ en(s 0 ) is a singleton (PB). In this case, any sequence s 0 a1•••an ----→ s n that does not contain b can be extended by b, and does not have any other actions from T (s 0 ) (D1), and p(s 0 ba1•••an-----→ s n ) = p(s 0 a1•••anb -----→ s n ).In particular, this holds for sequences where a i+1 = A(s i ), and thus if s n ∈ C, then, because C is a bottom EC and also s n ∈ C, we obtain p max s0 (

  Let C be a finite set of causes at a state s. A causality relation at s is a 3-ary relation Q ⊆ Σ×C ×Σ, such that for every a / ∈ en(s), and b 1 , . . . , b n = a with s b1•••bna-----→, it holds that for every c such that (a, c, -) ∈ Q we have (a, c, b i ) ∈ Q for at least one i ∈ {1, . . . , n}.

  and u ∈ Σ, either v ; S u or v and u are strongly independent; • for each v ∈ E and u ∈ Σ, either v ; W u or v and u are weakly independent; • there exists a causality relation Q such that for a ∈ D, c ∈ C, and b ∈ Σ, (a, c, b) ∈ Q if and only if a ; C c ; C b.

Theorem 5 . 1 :

 51 If V is a stubborn set of a dependency graph G at s, then V ∩ Σ is a stubborn set at s. Proof: D0 follows from the first condition in the definition of stubborn set for G. For D1, let a ∈ V ∩ Σ and let b 1 , . . . , b n ∈ Σ \ V , and s ∈ S be a state such that s b1•••bna -----→ s . There are two possibilities. (1) If a ∈ en(s), then we can readily infer commutativity by induction from (weak or strong) independence. (2) If a ∈ Σ \ en(s), then let Q be the causality relation required by definition.

•

  E = {a, b, c}, • D = {x, y, z, τ 1 , τ 2 }, • C = {τ 1 1 , τ 3 2 , x 1 , y 1 , y 2 , z 1 , z 2 }, • ; S = {(a, b), (b, a), (c, y)}, • ; W = {(c, y)}, • ; C = {(τ 1 , τ 1 1 ), (τ 2 , τ32 ), (x, x 1 ), (y, y 1 ), (y, y 2 ), (z, z 1 ), (z, z 2 ), (x 1 , a), (x 1 , b), (τ 1 1 , a), (τ 3 2 , c), (y 1 , a), (y 1 , b), (y 2 , x), (z 1 , a), (z 1 , b), (z 2 , x)}. The stubborn set for G is {a, b}, where both a and b are the key actions.

Table I EXPERIMENTAL

 I RESULTS ON ZEROCONF.

	Parameters	No reduction	With reduction
	(K)	States	Time (s)	States	Time (s)
	2	13474	103.819	461	2.479
	4	57960	1940.343	747	2.805
	6	125697 *	timeout	1033	3.582
	8	163229 *	timeout	1319	4.181
	10	176316 *	timeout	1605	4.929

* Computed using PRISM BDD engine

Strictly speaking, LTSs allow non-deterministic actions, which does not affect our proof in next section. Due to the page limit, we do not provide the full definition of an LTS.

In this case study, the number of states under unconditional fairness is the same as that without fairness in both the original and reduced models, as the states in all partial deadlocks are explored.

ACKNOWLEDGEMENTS

The first author was supported by the TEKES postdoctoral grant of 2010. The second and third authors are partly supported by EC FP 7 project CONNECT (IST 231167) and ERC Advanced Grant VERIWARE.

end if

Delete(b)

12:

end if 13: end for as follows. We have a candidate stubborn set Stub, initially the set of all actions. Det is the set of deterministic actions in the model, and P rob = Σ \ Det is the set of probabilistic actions of the model. The set U is a set of required actions. Usually this is empty, and has no effect on the generation of the stubborn set. Sometimes, to satisfy the S-condition, we must require that certain actions will be guaranteed in the stubborn set.

We try each enabled action a in turn. If {a} is a legitimate stubborn set, we return that. This is done using a predicate Single(a), which checks the following conditions: That these conditions are sufficient results from the following: (a) makes sure that a is strongly independent with all other enabled actions, and (b) makes sure that, if b is an action that a is dependent with, b has a cause that cannot be satisfied without executing either a or some action that a is dependent with. One such action would need to be executed first, but this cannot happen without a, and thus {a} is stubborn.

If either of these conditions fail, then we attempt to remove a deterministic a. (If a is not deterministic, we do not attempt to remove it as this could violate PB.) We start with the current candidate set by the recursive procedure Delete(a). The procedure makes sure that the closure properties of stubborn sets are satisfied. It works as follows: after deleting an action (or condition) a from the set, we have possible violations of the closure properties. The deletion of a may cause a violation for any b such that b ; a. (We write b ; a whenever b ; X a for some X ∈ {S, W, C}) We check for such a violation, and if it happens, we also delete b.

If the removal of a would result in a void set, i.e., empty or without key actions, a set violating PB, or not containing the set U , the removal is cancelled. In such a case, the sets Stub, Keys, and W eak must be returned to what they were before the deletion of a. Otherwise we go with the new values.

Naturally we can optimize Delete, and stop the procedure if a probabilistic action or a member of U is deleted without the need to complete the run. Other optimizations include stopping the procedure when a member of U would be deleted. Once we are done, we return the enabled actions of the stubborn set, along with the key actions.

To show that this results in a stubborn set for the graph, we present the following reasoning. Delete(a) removes a from the candidate set. The closure properties may be violated for b if b ; a. Firstly, if b ∈ C, then b needs to be removed, as we know that b has no ; W -neighbours. Secondly, if b ∈ en(s), we have to check that either all its weak neighbours are in the set or it is a key action. If neither is true, b needs to be deleted, otherwise its closure properties are intact. Thirdly, if b ∈ Σ \ en(s), and all its causes have been removed, it must be removed as well. If not, its closure properties are still intact. Later we only need to check the existence of key actions and that PB is not violated.

B. Combining partial order reduction with probability computation

To check reachability properties, partial order reduction is usually implemented in depth-first search (DFS). In this section, we give a complete DFS algorithm for exploring reduced state space under unconditional fairness and computing maximum probability on-the-fly by SCC-based value iteration [START_REF] Ciesinski | Reduction techniques for model checking Markov decision processes[END_REF], [START_REF] Kwiatkowska | Incremental quantitative verification for Markov decision processes[END_REF]. Our algorithm is based on the Tarjan's algorithm [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF], which is an efficient algorithm for identifying SCCs using DFS. Algorithm 3 combines partial order reduction with an optimised version of the Tarjan's algorithm proposed in [START_REF] Nuutila | On finding the strongly connected components in a directed graph[END_REF], as well as on-the-fly reduction. for all s with µ(s ) > 0 do if a ∈ Keys then s.sat := s.sat ∪ s .sat else P U SH(stack , s) end if 45: end if In Algorithm 3, stack is the stack for the depth-first search. T OP returns the element on top of stack, P OP and P U SH are the usual stack operations. Before the first call to the recursive function por tarjan, stack contains only the initial state s and the global variable index is set to one. The attribute p of a state s is the probability in s, and pdl indicates if no FMEC can be reached from s. The process of action a is interrupted once we find it can lead to a partial deadlock with non-zero probability. Then a is removed from the set R, which initially represents the whole weak stubborn set. The role of s.sat is to make sure the condition S for partial order reduction is satisfied: it denotes all the actions that have been executed after a path of key actions. When the actions of a stubborn set have been explored, if there are still "unsatisfied" actions left, we need to generate a new stubborn set such that they are included.

Identifying a partial deadlock can be done in two steps. (1) Identifying a bottom EC can be done by checking if there exists an action in the EC leading to states outside the EC. Note that an action that is not chosen by any fair adversaries cannot be counted as an action leaving the EC. (2) To check partial deadlock in a bottom EC, each state s in the EC is associated with a vector, one entry per process. If a process has an enabled action in s, then the corresponding entry is set to true. We perform an entry-wise disjunction operation on the vectors in the bottom EC. A partial deadlock is found if and only if an entry remains f alse after the disjunction operation.

VI. IMPLEMENTATION AND EXPERIMENTS

We implemented a prototype for the partial order reduction algorithm (Algorithm 3) in the probabilistic model checker PRISM [START_REF] Hinton | PRISM: A tool for automatic verification of probabilistic systems[END_REF]. The strong and weak independence relations are defined on the global state space, which we try to avoid to generate. Therefore, we compute overapproximations of these relations using the local state space of each component. In PRISM, each component has a set of local variables, which can be read in the guard of actions in other components. Therefore, it might be impossible to compute accurate local state spaces individually. Instead, we compute an over-approximation again, which contains the actual local state space, and may also include nonreachable local states. The over-approximated local state space is generated by removing all conjuncts containing nonlocal variables from the actions' guard, assuming each guard is specified in conjunction normal form.

The performance of our reduction technique can be demonstrated by a case study of the Zeroconf network configuration protocol [START_REF] Kwiatkowska | Performance analysis of probabilistic timed automata using digital clocks[END_REF]. Table I shows the number of states 2 and running time under unconditional fairness, with and without reduction respectively. These results clearly show the advantage of partial order reduction, even under the over-approximation of dependency relations. The time


Christyves Chevallier
email: christyves.chevallier@supelec.fr

Nicolas Fressengeas

Frédéric Genty

Joel Jacquet

Mid-infrared sub-wavelength grating mirror design: tolerance and influence of technological constraints

Keywords: numbers: 42.25.Fx, 42.79.Dj, 42.79.Fm, 42.82.Bq, 42.55.Sa, 78.20.Bh Sub-wavelength grating mirror, mirror design, tolerant design, VCSEL

published or not. The documents may come

Introduction

VCSEL emitting in the mid-infrared (λ > 2.2 µm) are of high interest for their use as stable and tunable sources for spectroscopic measurements. In this wavelength range, AlGaInAsSb appears as the best material system for mid-infrared VCSEL fabrication. However the wavelength emission of devices made from this material system is currently limited close to λ = 2.6 µm essentially due to the very thick (> 11 µm) distributed Bragg mirror (DBR) necessary to achieve 99.5 % reflectivity [START_REF] Cerutti | GaSb-based VCSELs emitting in the mid-infrared wavelength range (2-3 µm) grown by MBE[END_REF][START_REF] Bachmann | Single-mode electrically pumped GaSb-based VCSELs emitting continuous-wave at 2.4 and 2.6 µm[END_REF] which impairs the VCSEL properties. Sub-wavelength grating mirrors (SGM) with a low index sublayer [START_REF] Mateus | Ultrabroadband mirror using low-index cladded subwavelength grating[END_REF] can advantageously replace this DBR by exhibiting high reflectivity with a low thickness. SGM have already been successfully used as VCSEL top mirror [START_REF] Huang | A surface-emitting laser incorporating a highindex-contrast subwavelength grating[END_REF] providing a 100 nm large stopband with a 99.9 % reflectivity near 850 nm. A tolerance study has also been performed on this type of mirror which is made of an AlGaAs grating above an air gap as low index sublayer [START_REF] Zhou | Large fabrication tolerance for vcsels using high-contrast grating[END_REF]. The most critical parameter from a fabrication point of view is the etching of the 100 nm wide grooves. However, it has been shown that the grating parameters are very tolerant with ± 30 % on this etch length and ± 10 % on the grating period. These high tolerance values, compared to the 1 % tolerance of DBR, is another very good advantage for VCSEL fabrication [START_REF] Zhou | Large fabrication tolerance for vcsels using high-contrast grating[END_REF]. Moreover, such mirrors present a polarization sensitivity which should improve the quality of the laser emitted beam. In a previous work, SiO 2 /Si-based mid-infrared sub-wavelength grating mirrors (SGM) have been modelled and optimized for VCSEL application [START_REF] Chevallier | Optimized sub-wavelength grating mirror design for mid-infrared wavelength range[END_REF]. These first simulations have shown that such SGM mirrors, centered at λ 0 = 2.3 µm, can present high enough optical properties for successful VCSEL integration if an adequate design is carefully chosen.

In a first part of this work, a study of the impact of the technological constraints on the 2.3 µm centered mirror performances is presented through the comparison of two different designs. Then, the robustness with respect to fabrication errors is evaluated thanks to a tolerance computation of the different geometrical parameters of the design.

Design

The mirror structure is composed by a sub-wavelength grating mirror on top of a silica sublayer as shown on Figure 1. A quarter-wavelength SiO 2 /Si pair inserted below the grating is used to achieve the VCSEL mirror reflectivity necessary for laser operation [START_REF] Chevallier | Optimized sub-wavelength grating mirror design for mid-infrared wavelength range[END_REF]. Then, the optical properties for a TM-polarized VCSEL have been defined. To ensure the polarization selectivity, the TM reflectivity was chosen to have a minimum value of 99.9 % together with the widest possible bandwidth while the TE one was kept below 90 %. These requirements allow to define a quality factor Q as follow :

Q = ∆λ λ 0 1 N λ 2 λ=λ 1 R T M (λ)g(λ) (1)
The quality factor Q mainly represents the normalized bandwidth of the mirror. The bandwidth ∆λ normalized by λ 0 is defined by the range of wavelengths λ around λ 0 where the TM reflectivity R T M is higher than 99.9 % and the TE reflectivity R T E is lower than 90 %. The centering of the mirror is then taken into account by performing a gaussian weighted average of the R T M values on the N points of the bandwidth ∆λ = |λ 2 -λ 1 |.

A global optimization algorithm [7] was then used to increase the SGM performances. The quality factor Q, specifically defined for this application, is thus automatically maximized by adjusting the different SGM characteristic dimensions. However, such a problem presents many local maxima and the use of a global algorithm is mandatory. For each evaluation of the quality factor Q, reflectivity spectra were numerically computed by rigorous coupled-wave analysis (RCWA) [START_REF] Moharam | Stable implementation of the rigorous coupled-wave analysis for surface-relief gratings: enhanced transmittance matrix approach[END_REF][START_REF] Rathgen | mrcwa 20080820[END_REF] with constant optical index values of n Si = 3.48, n SiO2 = 1.47 and n GaSb = 3.9. Moreover, the use of an optimization algorithm allows the designer to define boundaries for the mirror geometrical dimensions. Thus, the technological constraints were also taken into account by the way of depth and length limitations. These constraints limit the filled length L f , the empty length L e of the grating and its aspect ratio AR, defined as the grating thickness T g to the etched length L e ratio (Figure 1). These limitations can be easily adjusted by the manufacturers according to the etching process used and the machine specifications.

Influence of the technological constraints on the mirror performances

SGM structures require a vertical etching profile with squared pattern to reach the 99.9 % high reflectivity. In order to obtain an experimental square grating profile close to the theoretical one presented on Figure 1, the first optimization was done by keeping the filled length L f and etched length L e of the grating larger than 500 nm and the aspect ratio AR smaller than 1.1 as constraints values. This means that the optimization retains only the designs with wide grooves since a shallow pattern is easier to etch than a deep one. Compared to data already published in the literature, these constraints are relatively severe for the optimization algorithm since the best Si/SiO 2 SGMs with bandwidths as large as 350 nm were defined with narrower patterns of less than 260 nm and a large AR of more than 2.6 [START_REF] Mateus | Ultrabroadband mirror using low-index cladded subwavelength grating[END_REF]. Even if a simple SGM structure could exhibit 99.9 % reflectivity under these technological constraints, the quarter wavelength layers have been added to increase the bandwidth of the mirror [START_REF] Chevallier | Optimized sub-wavelength grating mirror design for mid-infrared wavelength range[END_REF].

The optimization of such a mirror shows a design [START_REF] Chevallier | Optimized sub-wavelength grating mirror design for mid-infrared wavelength range[END_REF] with a grating thickness T g of 715 nm, a SiO 2 sublayer (T L ) of 17 nm, a filled length L f of 629 nm and an empty length L e of 675 nm (Table 1). The spectral reflection of this SGM is presented in [START_REF] Chevallier | Optimized sub-wavelength grating mirror design for mid-infrared wavelength range[END_REF] : it exhibits a ∆λ = 152 nm large stop-band for TM mode with a polarization selectivity ensured by a maximum reflectivity value of 80 % for TE mode. This structure exhibits all the optical characteristics required for integration in a VCSEL structure and should limit pitfalls during the manufacturing process with large etched areas of more than 500 nm and an aspect ratio of AR = 1.06.

This mirror exhibits very interesting optical properties for VCSEL integration. However, it appears that technological constraints dramatically impact on these properties since the normalized bandwidth obtained in this case is ∆λ/λ 0 = 6.6 % while it can be 17 % without constraints [START_REF] Mateus | Ultrabroadband mirror using low-index cladded subwavelength grating[END_REF]. For a better understanding and quantification of this impact, a new design was developed. For this new design, the optimization was performed under slightly more severe technological constraints which lowered the limitations of the optimization algorithm. The minimum lengths L e and L f were kept above 400 nm and the aspect ratio AR smaller than 1.25. These constraints lead to a 721 nm thick grating with a filled length L f of 479 nm and an empty length L e of 591 nm. The SiO 2 sublayer has a thickness of 499 nm (Table 2). Moreover, due to these lower constraints, the reflector exhibits better performances with a ∆λ = 270 nm bandwidth (Figure 2). Nevertheless, with smaller steps for the grating and narrower and deeper grooves (AR = 1.22), this design requires a better control of the etching process.

To conclude this part, the quality of the mirror increases significantly with the reduction of the technological limitations where AR = T g /L e is a key factor. However, the grating pattern could be manufactured with a certain inaccuracy resulting in new design limitations. Nevertheless, this new form of technological constraint, related to the reliability of the fabrication process, is less critical in the case of a robust design.

Robustness of the mirrors

The robustness of a design is evaluated by performing tolerance computations on the different dimensions of the structure.

The tolerance of one parameter is defined by the variation range of this parameter for which the bandwidth of the mirror verifies the condition ∆λ > 0 nm. This means that the design keeps R T M > 99.9 % and R T E < 90 % at λ 0 . It is important to note that for the computation of one tolerance value, L e for instance, the quality of the mirror is measured by varying it while the other parameters (L f , T g and T L ) are kept at their optimal values. Since the different geometrical dimensions of the grating are not decorrelated, if one parameter is inaccurately achieved during the fabrication process, for instance the grating thickness T g , the computed tolerances of the other parameters, in the example L e , L f and T L , are not valid any more. To simplify the problem in 2D, only two parameters L e and L f , which variation ranges are defined by ∆L e = L max e -L min e and ∆L f = L max f -L min f respectively, will be considered at the following. In the worst case, if one parameter is at its extremum value, L e = L max e for instance, a small variation of the other parameter L f would also decrease the quality of the mirror. Thus, the variation range of L f would tend to 0 when L e tends to its extremum value.

By making the hypothesis that the decrease of the variation range is linear, the four extrema L min e , L max e , L min f and L max f define the vertices of a quadrilateral in the (L e , L f ) plan. The area within the quadrilateral represents the set of pairs (L e , L f ) which define VCSEL-quality mirrors. A similar approach can be made to define an hyper-polyhedron in dimension 4 with the parameters L e , L f , T g and T L .

The computation of the tolerances of the first design shows very large variation range of 288 nm for L e , 146 nm for L f and 66 nm for T g (Table 1) which renders the grating very robust with respect to the fabrication imperfections. Moreover, as shown in Figure 3 which represents the variation range of L f versus L e , the optimal value found by the optimization algorithm is well centered within the quadrilateral delimited by the extrema (675, 685), (841, 629), (675, 539), (553, 629) (dashed lines). The computation of the variation range of the grating period Λ = L e + L f and the fill factor F F = L f /Λ results in (L e , L f ) pairs which are not included within the quadrilateral. The hatchings correspond to the silica thickness range where the TE polarization condition is not respected. For lower thicknesses (T L < 100 nm), better gratings can be found but they exhibit smaller tolerance values as low as 12 nm for the filled length L f . Thus, the tolerance area in the (L e , L f ) plan is extended to a polygon, the grey area in Figure 3, which is larger than the region defined by dashed line, validating the worst case hypothesis made previously.

The grating thickness is the most sensitive parameter for this design but thanks to the presence of the SiO 2 sublayer, a selective etching method can be used which would increase the control of the etched depth. The silica sublayer of 17 nm exhibits the largest tolerance and can vary from 0 nm up to 502 nm. As discussed in [START_REF] Chevallier | Optimized sub-wavelength grating mirror design for mid-infrared wavelength range[END_REF], the suppression of this layer can result in a more performant design. This is perfectly shown on Figure 4 where the normalized bandwidth ∆λ/λ 0 is plotted versus the silica sublayer thickness T L . This figure indicates that the thinner is T L , the larger the bandwidth becomes. Thus the interest of this sublayer is mainly to provide the possibility of using a selective etching method and must be very thin.

For the second design, computations indicate smaller variation range of 76 nm for L e , 38 nm for L f and 42 nm for T g (Table 2) which impose to have a better control of the fabrication process. Moreover, the optimum value of T L is more sensitive with a variation range of only 48 nm. This length is limited by the apparition of high TE reflectivity of more than 90 % within the bandwidth for thicknesses T L < 495 nm (Figure 5) which is forbidden by our hypothesis. Besides these smaller tolerance values, the optimum design found is not centered within the tolerance area. As shown in Figure 6, the optimum point is very close to the boundary of the area in the (L e , L f ) plan which imposes even smaller precision of less than 4 nm for the fabrication process. A solution to avoid this requirement is to choose another point in the grey area of the Figure 6 which would be more centered but would result in a less performant mirror.

It is also interesting to note that a smaller value of T L of 18 nm lead to a better mirror with a bandwidth as large as 300 nm (Figure 5). This design has not been found by our optimization algorithm since it has smaller tolerance values as low as 12 nm for L f . Such a design represents a narrow maximum for the quality function Q and thanks to the use of probability in the optimization algorithm, designs with large tolerance values are statistically promoted.

Conclusion

In this work, two different SGM designs based on Si/SiO 2 materials and centered at 2.3 µm are described. These mirrors with total thicknesses lower than 2 µm are well adapted for a VCSEL integration. The design of the SGM mirror can easily be adapted to the technological constraints of the manufacturers by adjusting the limitations defined for the automated optimization process. Indeed, the comparison between different technological constraints shows that a better accuracy of the etching process results in an increase of the quality of the mirror with a 118 nm larger bandwidth. However, this quality increase is also linked to a less robust mirror with respect to fabrication imperfections on the different dimensions. The choice of the design in regard to the manufacturing process can be made by taking into account not only the limitations on the pattern resolution but also the precision required to keep a efficient mirror. This work can also be adapted to a large range of materials, such as semi-conductors, structures and wavelengths to meet the optical requirements of numerous applications.

  (a) Reflection spectra of TM (solid blue) and TE (dashed red) mode. (b) Zoom on the high reflectivity values of the reflector above 99 %.

Figure 2 .

 2 Figure 2. Reflectivity of the SGM optimized under constraints (L e and L f > 400 nm and AR < 1.25) exhibiting a 270 nm large bandwidth for a 99.9 % TM reflectivity.

Figure 3 .

 3 Figure 3. Tolerance of the filled length L f versus etched length L e for the first design. The point (675, 629) at the center represents the optimum value found by the optimization.The quadrilateral (dashed line) defines, in a linear approximation, the area of (L e , L f ) pairs which correspond to VCSEL-quality designs. The computations of the period Λ and the fill factor F F define 4 points which extend the quadrilateral to a polyhedron (grey area). The worst case hypothesis is thus confirmed by a larger area of tolerance.

Figure 4 .

 4 Figure 4. Evolution of the normalized bandwidth ∆λ/λ 0 versus the silica thickness T L . The arrow shows the optimum design (T L = 17 nm). The silica thickness T L can be as large as 100 nm without decreasing excessively the quality of the mirror by keeping a 115 nm large bandwitdh.

Figure 5 .

 5 Figure 5. Evolution of the normalized bandwidth ∆λ/λ 0 versus the silica thickness T L for the second design. The arrow shows the optimum design (T L = 499 nm). The hatchings correspond to the silica thickness range where the TE polarization condition is not respected. For lower thicknesses (T L < 100 nm), better gratings can be found but they exhibit smaller tolerance values as low as 12 nm for the filled length L f .

Figure 6 .

 6 Figure 6. Tolerance of the filled length L f versus etched length L e for the second design. The optimum design (591, 479) is very closed to the boundary of the tolerance area defined by the polyhedron (grey area). This design requires a better etching precision with less than 5 nm of error allowed.

Table 1 .

 1 Dimensions and tolerances of the mirror optimized under large technological constraints (L f and L e > 500 nm and AR < 1.1).Optimum Tolerance for R T M > 99.9 % and R T E < 90 %

	L e	675 nm	553 nm < L e < 841 nm
	L f	629 nm	539 nm < L f < 685 nm
	Λ = L e + L f	1304 nm 1109 nm < Λ < 1429 nm
	F F = L f /Λ	48.23 %	42.14 %< F F <51.64 %
	T g	715 nm	678 nm < T g < 744 nm
	T L	17 nm	0 nm < T L < 502 nm
	∆λ	152 nm
	∆λ/λ 0	6.6 %

Table 2 .

 2 Dimensions and tolerances of the mirror optimized under technological constraints chosen as L f and L e > 400 nm and AR < 1.25.

	L e	591 nm	519 nm < L e < 595 nm
	L f	479 nm	443 nm < L f < 481 nm
	Λ = L e + L f 1070 nm	1015 nm < Λ < 1075 nm
	F F = L f /Λ 44.77 %	40.07 % < F F <52.07 %
	T g	721 nm	717 nm < T g < 759 nm
	T L	499 nm	495 nm < T L < 543 nm
	∆λ 270 nm
	∆λ/λ 0 11.6 %

Optimum Tolerance for R T M > 99.9 % and R T E < 90 %

Acknowledgments

The authors thank ANR for financial support in the framework of Marsupilami project (ANR-09-BLAN-0166-03) and IES and LAAS (France), partners of LMOPS/Supélec in this project.

This work was also partly funded by the InterCell grant (http://intercell.metz.supelec.fr) by INRIA and Région Lorraine (CPER2007).


Paolo Masci
email: paolo.masci@eecs.qmul.ac.uk

Nicola Nostro
email: nicola.nostro@isti.cnr.it

Felicita Di Giandomenico
email: felicita.digiandomenico@isti.cnr.it

On enabling dependability assurance in heterogeneous networks through automated model-based analysis

We present the specification of a basic library of dependability mechanisms that can be used within automated approaches for synthesising dependable Connectors in heterogeneous networks. The library builds on classical dependability patterns, such as majority voting and retry, and uses the concept of overlay networks for triggering the synthesis of specific dependability mechanisms in the Connector from high-level specifications. We translated such dependability mechanisms into SAN models with the aim to evaluate, through model-based analysis, which dependability mechanisms should be embedded in the synthesised Connector for ensuring a given dependability level between networked systems willing to be connected. A case study is also presented to show the application of selected library mechanisms. This work is carried out in the context of Connect, a European FET project which is investigating the possibility of enabling long-lasting inter-operation among networked systems by synthesising mediating Connectors at run-time.

Introduction and background

Interoperability in future networks will be characterised by seamless and continuous communication among heterogeneous networked systems. Over time, networked systems may change mode of operation, e.g., because of hardware/software updates or new application contexts. As a consequence, network infrastructures ought to provide appropriate means for supporting interoperability among evolving networked systems.

In the European FET project Connect [START_REF]Connect: Emergent connectors for Eternal Software Intensive Networked Systems[END_REF], interoperability issues of evolving networks are tackled by synthesising dependable Connectors at run-time. To do this, the network infrastructure defined in Connect embeds five logical units, denominated enablers, that seamlessly collaborate for ensuring continuous and long-lasting inter-operation among networked systems. In Connect, the discovery enabler discovers the functionality of networked systems and applications and retrieves information on the interfaces they use for inter-operating with others. The learning enabler completes such a knowledge on the interaction behaviour of networked systems by applying learning algorithms, and produces a model of this behaviour in the form of a labelled transition system (LTS). The synthesis enabler dynamically synthesises a software mediator using code generation techniques (from the independent LTS models of each system) that will connect and coordinate the interoperability between heterogeneous systems. In order to fulfil dependability requirements, synthesis triggers the dependability enabler, which is in charge of analysing the Connector's design before the Connector gets deployed and put in operation. If needed, the dependability enabler drives the synthesis enabler towards possible Connector's enhancement. The monitoring enabler continuously monitors the deployed Connectors during their execution for updating the other enablers with run-time data.

In this work, we focus on the dependability enabler, which performs a modelbased analysis for assessing the dependability level of the synthesised Connectors. Specifically, we point our attention on a dependability enabler's module, denominated enhancer. Such a module is responsible for guiding the synthesis process towards enhancements of a Connector's design whenever the analysis reveals inadequate dependability levels. In brief, this module is in charge of selecting a combination of dependability mechanisms suitable for enhancing the synthesised Connector so that it complies with given requirements. Then, the synthesis enabler embeds the selected dependability mechanisms in the Connector's design and proceeds with its implementation and deployment. The architecture of the dependability enabler and the functionalities of the enhancer have been presented in [START_REF] Masci | Towards automated dependability analysis of dynamically connected systems[END_REF]. The contribution of this paper consists in the definition of a basic library of dependability mechanisms for the enhancer. The library builds on classical dependability patterns (see [START_REF]EU project ReSIST: Resilience for Survivability in IST[END_REF] for a survey), and uses the concept of overlay networks for triggering the synthesis of specific dependability mechanisms in the synthesised Connector from high-level specifications. How these dependability mechanisms can then be embedded in the synthesised connectors pertains to the synthesis enabler and is not addressed in this paper.

The paper is organised as follows. In Section 2, the stochastic activity networks [START_REF] Movaghar | Performability modelling with stochastic activity networks[END_REF] (SAN) formalism, a widely used formalism for model-based dependability analysis of complex systems, is briefly illustrated in order to allow the reader to understand the formal specification of the developed dependability mechanisms. In Section 3, we explain the ideas underpinning the library of dependability mechanisms, and we present the specification of such a library with the SAN formalism. In Section 4, we trial our ideas by applying the library to a case study based on a demonstrative scenario based on that presented in [START_REF]Deliverable D5.2 -Dependability Assurance[END_REF]. In Section 5, we report on related work and conclude the paper.

The SAN Formalism

Stochastic Activity Networks [START_REF] Movaghar | Performability modelling with stochastic activity networks[END_REF][START_REF] Movaghar | Stochastic activity networks: a new definition and some properties[END_REF][START_REF] Sanders | Stochastic activity networks: formal definitions and concepts[END_REF] are an extension of the Petri Nets (PN) formalism [START_REF] Adam | Kommunikation mit Automaten[END_REF][START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF]. SANs are directed graphs with four disjoint sets of nodes: places, input gates, output gates, and activities.

Activities replace and extend the transitions of the PN formalism. Each SAN activity may be either instantaneous or timed. Timed activities represent actions with a duration affecting the performance of the modelled system, e.g., message transmission time. The duration of each timed activity is expressed via a time distribution function. Any instantaneous or timed activity may have mutually exclusive outcomes, called cases, chosen probabilistically according to the case distribution of the activity. Cases can be used to model probabilistic behaviours. An activity completes when its (possibly instantaneous) execution terminates.

As in PNs, the state of a SAN is defined by its marking, i.e., a function that, at each step of the net's evolution, maps the places to non-negative integers (called the number of tokens of the place). SANs enable the user to specify any desired enabling condition and firing rule for each activity. This is accomplished by associating an enabling predicate and an input function to each input gate, and an output function to each output gate. The enabling predicate is a Boolean function of the marking of the gate's input places. The input and output functions compute the next marking of the input and output places. If these predicates and functions are not specified for some activity, the standard PN rules are assumed. The evolution of a SAN, starting from a given marking µ, may be described as follows:

1. the instantaneous activities enabled in µ complete in some unspecified order; 2. if no instantaneous activities are enabled in µ, the enabled (timed) activities become active; 3. the completion times of each active (timed) activity are computed stochastically, according to the respective time distributions; the activity with the earliest completion time is selected for completion; 4. when an activity (timed or not) completes, one of its cases is selected according to the case distribution, and the next marking µ ′ is computed by evaluating the input and output functions; 5. if an activity that was active in µ is no longer enabled in µ ′ , it is removed from the set of active activities.

Graphically, places are drawn as circles, input gates as left-pointing triangles, output gates as right-pointing triangles, instantaneous activities as narrow vertical bars, and timed activities as thick vertical bars. Cases are drawn as small circles on the right side of activities.

Library of dependability mechanisms

Overlay networks are virtual networks built on top of existing network substrates: nodes in overlay networks represent logical hosts involved in interactions, and links in overlay networks correspond to paths in the network substrate that are traversed by messages during inter-operations. To date, overlay networks have been used for exploiting peculiar characteristics of network substrates at the application level; for instance, Andersen et al [START_REF] Andersen | Resilient overlay networks[END_REF] exploit highly redundant networks substrates for defining resilient communication systems as overlay networks (a survey on the use of overlay networks for defining new applications can be found in [START_REF] Kurian | A survey on the design, applications, and enhancements of application-layer overlay networks[END_REF]).

Thanks to the infrastructure provided by Connect, here we can use the concept of overlay networks in an alternative way, i.e., rather than using overlay networks for exploiting the characteristics of the network substrate, we use them for defining the characteristics of the network substrate that should be synthesised. The basic idea is to view Connectors as overlay networks, and to exploit their structure for triggering the generation of specific dependability mechanisms in the network substrate during the synthesis process.

In the following, we describe the models we defined for triggering the generation of typical dependability mechanisms suitable to contrast two typical classes of failure modes that may happen during interactions: timing failures, in which networked systems send messages at time instants that do not match an agreed schedule, and value failures, in which networked systems send messages containing incorrect information items. For the purpose of this paper, we consider timing failures of type omission, i.e., late messages are always discarded, and value failures that cause a networked system to respond within the correct time interval but with an incorrect value. Each model is specified with the SAN formalism. The models are developed according to three basic rules that allow to simplify the automated procedure for embedding the mechanism in the specification of the synthesised Connector: (i) each model has an initial place, s0, whose tokens enable the first activity of the model; (ii) each model has a final place, s1, which contains tokens whenever the last activity of the model completes; (iii) the overall number of tokens in s1 is always less or equal to the number of tokens in s0. With the above rules, the behaviour of the model can be seen as an enhanced activity, and can be directly used to replace any activity that moves tokens between two places in the specification of the Connector (the basic semantics of an activity is always preserved).

Retry Mechanism

The retry mechanism consists in re-sending messages that get corrupted or lost during communications, e.g., due to transient failures of communication links. This mechanism is widely adopted in communication protocols, such as TCP/IP [START_REF] Braden | RFC 1122: Requirements for Internet hosts -communication layers[END_REF] for enabling reliable communication over unreliable channels. A typical implementation of the retry mechanism uses time-outs and acknowledgements: after transmitting a message, the sender waits for a message of the receiver that acknowledges successful communication. If the acknowledgement is not received within a certain time interval, the sender assumes that the communication was not successful, and re-transmits the message.

The synthesis of a retry mechanism can be triggered with the stochastic activity network shown in Figure 1. On the sender side, the mechanism creates a message re-transmission policy for re-sending the message at most N times; on the receiver side, the mechanism creates a policy for avoiding duplicated reception of messages and for sending acknowledgements. In the model, all places initially contain zero tokens, except p0, which contains N tokens, where N is a model parameter representing the maximum number of re-transmissions. Activity send is enabled when the conjunction of the following conditions is true: p0 and s0 contain at least one token, and ackReceived contains zero tokens. When activity send completes with success (case 0, with probability pr0), a token is removed from s0 and p0, and the marking of p1 is incremented by one. Activity receive is enabled when p1 contains at least one token and messageReceived contains zero tokens. When activity receive completes, a token is moved to s1, and the marking of p2 and messageReceived is incremented by one. A token in p2 enables activity sendAck, whose aim is to enable the receiving host notify the sender that the message has been successfully received. The sender stops re-transmitting the message as soon as it gets an acknowledgement that the message has been successfully received, or after N attempts.

Probing Mechanism

The probing mechanism exploits redundant paths and periodic keep-alive messages for enabling reliable communication in face of path failures. The basic idea is to continuously collect statistics on the characteristics of the communication channels, and to select the best channel on the basis of such statistics. This mechanism has been used for defining communication services with guaranteed delivery and performance levels, e.g., see Akamai's SureRoute [START_REF]Akamai sureroute for failover and performance[END_REF] and reliable multi-cast protocols for peer-to-peer networks [START_REF] Zeng | Path-diversity p2p overlay retransmission for reliable ip-multicast[END_REF].

The synthesis of a probing mechanism that uses two redundant communication channels can be triggered with the stochastic activity network shown in Figure 2. The mechanism instruments the sender with a periodic channel probing functionality suitable to feed a monitoring system that collects statistics about the reliability level of the communication channels.

In the model, place mode is a state variable that indicates the mode of operation of the mechanism, which can be either probing mode (mode contains zero tokens), i.e., the mechanism tests the characteristics of the communication channels through keep-alive messages, or normal mode (mode contains one token), i.e., Fig. 2. Probing mechanism the mechanism selects the best estimated channel for relaying messages. Initially, all places contain zero tokens, except ready, which contains one token.

When in normal mode, activity select is enabled when s0 contains at least one token, and ready contains one token. When select completes, one token is removed from s0 and ready, and send0 gets enabled if monitor0 has more tokens than monitor1 (send1 gets enabled in the other case). If send0 completes with success (case 0), then a token is added to s1 and ready. Similarly, when send1 completes with success, a token is moved to s1 and ready.

When in probing mode, the model behave as follows: send0 and send1 have both the same rate R0 (while their case probabilities depend on the characteristics of the channels, which may vary over time). Activity select is enabled when ready contains one token; when select completes, ready contains zero tokens and activities send0 and send1 get enabled (by moving one token in both p0 and p1). When send0 completes with success (case 0), a token is added to monitor0. Similarly, when send1 completes, a token is added to monitor1. A token is moved to ready when both send0 and send1 complete.

Majority Voting Mechanism

Majority voting is a fault-tolerant mechanism that relies on a decentralised voting system for checking the consistency of data. Voters are software systems that constantly check each other's results, and has been widely used for developing resilient systems in the presence of faulty components. In a network, voting systems can be used to compare message replicas transmitted over different channels, see, for instance, the protocol proposed in [START_REF] Zhou | Efficient multipath communication for time-critical applications in underwater acoustic sensor networks[END_REF] for time-critical applications in acoustic sensor networks.

The synthesis of a majority voting mechanism that uses three redundant communication channels can be triggered with the stochastic activity network shown in Figure 3. The mechanism replicates the message sent by the transmitting host over three channels. In this case, the mechanism is able to tolerate one faulty channel.

In the model, all places initially contain zero tokens. Activity multipathRouter gets enabled when s0 contains a token. When such an activity completes, Fig. 3. Majority voting mechanism the token is removed from s0, and three send activities (send0, send1, send2) get enabled by moving tokens into places p0, p1, and p2. The number of tokens moved in such places encode the actual informative content of the message. When a send activity completes with success, the activity preserves the number of tokens (i.e., all tokens are moved forward into the next place). Activity voter gets enabled when the all sends complete (such activities will eventually change the marking of p3, p4, and p5). When activity voter completes, a token is moved into s1 and all tokens in other places are removed.

Error Correction Mechanism

Error correction deals with the detection of errors and re-construction of the original, error-free data. A widely used approach for enabling hosts to automatically detect and correct errors in received messages is forward error correction (FEC). The mechanism requires the sender host to transmit a small amount of additional data along with the message. The mechanism has been used, for instance, in [START_REF] Subramanian | Overqos: offering internet qos using overlays[END_REF] for defining an overlay-based architecture for enhancing the quality of service of best-effort services over the Internet.

The synthesis of an error correction mechanism that uses two redundant communication channels can be triggered with the stochastic activity network shown in Figure 4. One channel is used to send the original message, and the other channel is used to send the error correction (EC) code. The receiver is instrumented with a filtering mechanism that checks and corrects messages.

Initially, all places contain zero tokens. When a token is moved into s0, activity fec gets enabled. When such an activity completes, a token is removed from s0, and activities sendMsg and sendEC get enabled by moving tokens into p0 and p1. The number of tokens moved in such places encode the actual informative content of the message. When sendMsg completes with success, all tokens in place p0 are moved into p2. Similarly, when sendEC completes, all tokens of p1 are moved into p3. Activity filter gets enabled when places p2 and p3 contain

Security Mechanism

A typical way to enforce protection on a host is to decouple the host from the rest of the network. A host can, for instance, be protected from receiving unwanted traffic by creating a ring that selectively filters the incoming traffic. Similarly, the identity of a host can be protected by anonymising the host's messages through a set of intermediary hosts, denominated proxies. This mechanism has been used, for instance, in [START_REF] Keromytis | Sos: Secure overlay services[END_REF] and [START_REF] David | Mayday: Distributed Filtering for Internet Services[END_REF] for protecting hosts from denial-of-service attacks.

The synthesis of a security mechanism over a network with two intermediary hosts can be triggered with the stochastic activity network shown in Figure 5. The mechanism creates an anonymiser service that selects a channel with a certain probability, and forwards the message on such a channel. In the model, Fig. 5. Security mechanism all places initially contain zero tokens. When a token is moved into s0, activity Anonymiser gets enabled. When such an activity completes, a token is moved from s0 either to p0 (with probability pr0), or to p1 (with probability pr1), and either send0 or send1 gets enabled. When a send activity completes, a token is moved in s1.

Case study

In this section, we show how the developed library can be used within an automated model-based dependability analysis with the aim to enhance a synthesised Connector. We consider a demonstrative scenario described in [START_REF]Deliverable D5.2 -Dependability Assurance[END_REF], where two kinds of heterogeneous devices need to communicate in a reliable and timely manner. For clarity of exposition, in order to fit the purpose of this paper and also make it self-contained, in the following we report a concise and slightly reworded description of the scenario reported in [START_REF]Deliverable D5.2 -Dependability Assurance[END_REF], and an informal specification of the protocols used by the two kinds of heterogeneous devices, and of the synthesised Connector. Readers interested in the complete original specification are re-directed to [START_REF]Deliverable D5.2 -Dependability Assurance[END_REF].

Specification

The scenario considers an emergency situation in which policemen need to exchange information with security guards. Each policeman can exchange confidential data with other policemen with a secured file sharing protocol. Security guards, on the other hand, exchange information by using another protocol, denominated emergency call. The two protocols have the same aim (i.e., enable information exchange) but a mediating Connector is needed in order to enable inter-operation, because they use different message types and different message sequences.

Secured File Sharing. This is a basic peer-to-peer protocol for enabling file sharing. The peer that initiates the communication, denominated coordinator, sends a multicast message (selectArea) to a selected group of peers. When a peer receives a selectArea message, the peer replies to the coordinator with a areaSelected message. Upon receiving the areaSelected message, the coordinator sends a data file to the peers (uploadData message) that, in turn, automatically reply with an uploadSuccess message if the data has been successfully received.

Emergency Call. This is a peer-to-peer protocol for sending data files from a control centre to groups of devices. Each group of devices is coordinated by a leader. The protocols is initiated by the control centre, which sends an eReq message to a group of devices located in a selected area of interest. The group leader is in charge of replying to the control centre with an eResp. Whenever the control centre receives the eResp from a group leader, an emergencyAlert message is sent to all devices. Each device automatically notifies the control center with an eACK message whenever it successfully receives the data.

Mediating Connector. A mediating Connector suitable for enabling interoperation from devices using the secured file sharing protocol to devices using the emergency call protocol performs the following translations: selectArea messages are translated into eReq messages directed to the leaders of selected group of devices; eResp messages are translated into areaSelected messages; uploadData messages are translated into multicast emergencyAlert messages; eACK messages are collected by the Connector and then translated into a single uploadSuccess message. A timeout is used to avoid infinite wait in the case of failure of eACK messages. The SAN models corresponding to the specifications are shown in Figure 6. The Connector uses two different channels to communicate with the two different kinds of devices. Any send and receive action performed by the Connector is represented by a timed activity. Each activity has two case probabilities: case 0 is associated to the correct behaviour; case 1 is associated to incorrect behaviour. Since the purpose of this case study is not to show new results on a real-world protocol, but to exemplify the utility of the developed library, here we assume that timed activities are all exponentially distributed and with the same rate. The model of the Connected system, which is shown in Figure 7, is obtained by composing the models through place sharing. In the Connected system, there is a shared place for each pair of activities that represent send/receive actions: send activities add tokens in the shared place, while receive activities remove tokens from the shared place and use the marking of the shared place as enabling condition.

SAN Models

Analysis

The analysis is performed through Möbius [START_REF] Daly | Möbius: An extensible tool for performance and dependability modeling[END_REF], and consists in a measure of latency and a measure of coverage. Latency is measured from when the control centre sends the initial request selectArea to when it receives uploadSuccess. Coverage is given by the percentage of responses the control centre receives back within a certain time T .

The analysis we describe can be automated with the approach reported in [START_REF] Masci | Towards automated dependability analysis of dynamically connected systems[END_REF]. In order to simplify the exposition, here we consider only failures between the Connector and the guards' devices (which execute the Emergency Call protocol), and we use the probing mechanism to contrast timing failures, and the majority voting mechanism to contrast value failure. Both mechanisms are introduced on the communication channel between the Connector and the guards' devices (which follow the Emergency Call protocol).

Latency. The first analysis aims to assess the trend of latency for different values of timeout, assuming three different values of timing failure probability between the Connector and the guards. Figure 8(a), shows the value of latency (on the y axis) for the Connected system without dependability mechanisms (the timeout value is reported on the x axis). Figure 8(b), shows the same analysis performed on the model enhanced with the probing mechanism. We can notice that, with the considered system parameters, the mechanism is able to reduce latency only in two out of three situations. When the timing failure probability is 0.5 the latency has very similar values for both models; in fact, in such a case the failure probability has a too high value and the probing mechanism is a too light means to contrast its effects.

Coverage. The second analysis is performed for three different probabilities of value failures between the Connector and the guards. Figures 9(a) and 9(b) show the analysis results for the basic model and for the model enhanced with the majority voting mechanism. In this case, the mechanism is able to improve coverage in all considered cases. We can notice that, for the probability values considered, the coverage provided by the enhanced model is approximately double compared to basic one.

Related work and conclusions

Automated dependability analysis, pursued through transformation-based verification and validation environments, has been the subject of several studies in the last decade. Automatic/automated methods from system specification languages to modelling languages amenable to perform dependability analysis has been recognised as an important support for improving the quality of systems. Moreover, it favours the application of verification and validation techniques at industry level, where these methods have difficulties to be applied on a routine basis, primarily due to the high level of expertise required to deal with mathematical modelling and analysis techniques. Development of an integrated environment to support the early phases of system design, where design tools based on the UML (Unified Modeling Language) are augmented with transformation-based validation and analysis techniques, is presented in [START_REF] Bondavalli | Dependability analysis in the early phases of uml-based system design[END_REF], among several other works. A Modeling framework allowing the generation of dependability-oriented analytical models from AADL (Architecture Analysis and Design Language) models is described in [START_REF] Rugina | A system dependability modeling framework using aadl and gspns[END_REF]. Tools have also been developed, supporting the definition of model-based transformations. To provide some examples, the Viatra tool [START_REF] Csertan | Viatra -visual automated transformations for formal verification and validation of uml models[END_REF] automatically checks consistency, completeness, and dependability requirements of systems designed using the Unified Modeling Language. The Genet tool [START_REF] Carmona | Genet: A tool for the synthesis and mining of petri nets[END_REF] allows the derivation of a general Petri net from a state-based representation of a system. The ADAPT Tool supports model transformations from AADL Architectural Models to Stochastic Petri Nets [START_REF] Rugina | The adapt tool: From aadl architectural models to stochastic petri nets through model transformation[END_REF]. However, from the point of view of enhancing the model-transformation environment with template models of basic fault tolerance mechanisms to allow automated assessment of enhanced, fault tolerant designs, it appears a rather novel research direction. Although studies exist dealing with libraries of fault tolerance mechanisms (e.g. [START_REF]EU project ReSIST: Resilience for Survivability in IST[END_REF]) to assist the design of dependable systems, to the best of the authors' knowledge the attempt to provide template models of dependability mechanisms, to be incorporated in a wider system dependability model to assess their efficacy at system design time, is a new contribution of this paper.

In this paper, five dependability mechanisms have been specified in terms of SAN models, covering basic means to cope with timing and value failures of communication channels in heterogeneous networked systems. They are first encapsulated in the dependability model of the Connector set-up to allow interoperability among networked systems, and managed by the dependability evaluator enabler to analyse their appropriateness to satisfy dependability properties required by the networked systems. Upon positive assessment, they are employed to build advanced Connectors design. A case study has been also included, inspired by current research activity ongoing in the context of the EU Connect project, to show the practical application of selected dependability mechanisms in presence of failure scenarios.

The work described is a first step in the development of enhanced automated dependability analysis as a support for the synthesis of dependable Connectors. After the definition of the individual dependability mechanisms, all the implications related with their systematic usage to replace basic elements of the Connector dependability model (showing unsatisfactory from the dependability or performance point of view), have to be rigorously considered and solved. Of course, also investigations on further dependability mechanisms suitable to the addressed context would be interesting to carry-on. Indeed, these are among the directions we are exploring as future work.

Fig. 1 .

 1 Fig. 1. Retry mechanism

Fig. 4 .

 4 Fig. 4. Error correction mechanism

Fig. 6 .

 6 Fig. 6. SAN Models

Fig. 7 .

 7 Fig. 7. SAN model of the Connected system

Fig. 8 .Fig. 9 .

 89 Fig. 8. Latency assessment in case of timing failure

Acknowledgements

This work is partially supported by the EU FP7 Project Connect (FP7-231167).