Serge Haddad
email: serge.haddad@lsv.ens-cachan.fr

Benjamin Monmege
email: benjamin.monmege@ulb.ac.be

Reachability in MDPs: Refining Convergence of Value Iteration

Markov Decision Processes (MDP) are a widely used model including both non-deterministic and probabilistic choices. Minimal and maximal probabilities to reach a target set of states, with respect to a policy resolving non-determinism, may be computed by several methods including value iteration. This algorithm, easy to implement and efficient in terms of space complexity, consists in iteratively finding the probabilities of paths of increasing length. However, it raises three issues: (1) defining a stopping criterion ensuring a bound on the approximation, (2) analyzing the rate of convergence, and (3) specifying an additional procedure to obtain the exact values once a sufficient number of iterations has been performed. The first two issues are still open and for the third one a "crude" upper bound on the number of iterations has been proposed. Based on a graph analysis and transformation of MDPs, we address these problems. First we introduce an interval iteration algorithm, for which the stopping criterion is straightforward. Then we exhibit convergence rate. Finally we significantly improve the bound on the number of iterations required to get the exact values.

Introduction

Markov Decision Processes (MDP) are a commonly used formalism for modelling systems that use both probabilistic and non-deterministic behaviors. These are generalizations of discrete-time Markov chains for which non-determinism is forbidden. MDPs have acquired an even greater gain of interest since the development of quantitative verification of systems, which in particular may take into account probabilistic aspects (see [START_REF] Baier | Principles of Model Checking[END_REF] for a deep study of model checking techniques, in particular for probabilistic systems). Automated verification techniques have been extensively studied to handle such probabilistic models, leading to various tools like the PRISM probabilistic model checker [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF]. Value iteration for reachability problems. In the tutorial paper [START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF], the authors cover some of the algorithms for the model-checking of MDPs and Markov chains. The first simple, yet intriguing, problem lies in the computation of minimum and maximum probabilities to reach a target set of states of an MDP. Exact polynomial time methods, like linear programming, exist to compute those probabilities, but they seem unable to scale on large systems. Nonetheless, they are based on the fact that these probabilities are indeed fixpoints of some operators. Usually, numerical approximate methods are rather used in practice, the most used one being value iteration. The algorithm consists in asymptotically reaching the previous fixpoints by iterating the operators. However, it raises three issues. Since the algorithm must terminates after a finite number of iterations one has to define a stopping criterion ensuring a bound on the difference between the computed and the exact values. From a theoretical point of view, establishing the rate of convergence with respect to the parameters of the MDP (number of states, smallest positive transition probability, etc.) helps to estimate the complexity of value iteration. Sometimes for further application the exact values and/or the optimal policy are required. This is generally done by performing an additional rounding procedure once a sufficient number of iterations has been performed. The first two issues are still open and for the third one a "crude" upper bound on the number of iterations has been proposed [START_REF] Chatterjee | Value iteration. In 25 Years of Model Checking[END_REF]Sec 3.5].

Our contributions. Generally the numerical computations of optimal reachability probabilities are preceded by a qualitative analysis that computes the sets of states for which this probability is 0 or 1 and performs an appropriate transformation of the MDP. We adopt here an alternative approach based on the maximal end component (MEC) decomposition of an MDP (that can be computed in polynomial time [START_REF] Alfaro | Formal Verification of Probabilistic Systems[END_REF]). We show that for an MDP featuring a particular MEC decomposition, some safety probability is null with an additional convergence rate with respect to the length of the run. Then we design a min-(respectively, max-) reduction that ensures this feature while preserving the minimal (respectively, maximal) reachability probabilities. In both cases, we establish that the reachability probabilities are unique fixed points of some operator.

So we iterate these operators starting from the maximal and the minimal possible vectors. These iterations naturally yield an interval iteration algorithm for which the stopping criterion is straightforward since, at any step, the two current vectors constitute a framing of the reachability probabilities. Similar computations of parallel under-and over-approximations have been used in [START_REF] Katoen | Safe on-the-fly steady-state detection for timebounded reachability[END_REF], in order to detect steady-state on-the-fly during the transient analysis of continuous-time Markov chains. In [START_REF] Kattenbelt | A game-based abstraction-refinement framework for Markov decision processes[END_REF], under-and over-approximations of reachability probabilities in MDPs are obtained by substituting to the MDP a stochastic game. Combining it with a CEGAR-based procedure leads to an iterative procedure with approximations converging to the exact values. However the speed of convergence is only studied from an experimental point of view. Afterwards, we provide probabilistic interpretations for the adjacent sequences of the interval iteration algorithm. Combining such an interpretation with the safety convergence rate of the reduced MDP allows us to exhibit a convergence rate for interval iteration algorithm. At last, exploiting this convergence rate, we significantly im-prove the bound on the number of iterations required to get the exact values by a rounding procedure. Related work. Interestingly, our approach has been realized in parallel of Brázdil et al [START_REF] Brázdil | Verification of Markov decision processes using learning algorithms[END_REF] that solves a different problem with similar ideas. There, authors use some machine learning algorithm, namely real-time dynamic programming, in order to avoid to apply the full operator at each step of the value iteration, but rather to partially apply it based on some statistical test. Using the same idea of lower and upper approximations, they prove that their algorithm almost surely converges towards the optimal probability, in case of MDPs without nontrivial end components. In the presence of non-trivial end components, rather than computing in advance a simplified equivalent MDP as we do, they rather compute the simplification on-the-fly. It allows them to also obtain results in the case where the MDP is not explicitly given. However, no analysis of the speed of convergence of their algorithm is provided, nor are given explicit stopping criteria enabling an exact computation of values. Outline. Section 2 introduces MDPs and the reachability/safety problems. It also includes MEC decomposition, dedicated MDP transformations and characterization of minimal and maximal reachability probabilities as unique fixed points of operators. Section 3 presents our main contributions: the interval iteration algorithm, the analysis of the convergence rate and a better bound for the number of iterations required for obtaining the exact values by rounding. Due to space constraints, a complete version, with full proofs, can be found in [START_REF] Haddad | Reachability in MDPs: Refining convergence of value iteration[END_REF].

Reachability problems for Markov decision processes

Problem specification

We mainly follow the notations of [START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF]. We denote by Dist(S) the set of distributions over a finite set S, i.e., every mapping p : S → [0, 1] from S to the set [0, 1] such that s∈S p(s) = 1. The support of a distribution p, denoted by Supp(p), is the subset of S defined by Supp(p) = {s ∈ S | p(s) > 0}.

A Markov Decision Process (MDP) is a tuple M = (S, α M , δ M ) where S is a finite set of states; α M = s∈S A(s) where every A(s) is a non empty finite set of actions with A(s) ∩ A(s ) = ∅ for all s = s ; and δ M : S × α M → Dist(S) is a partial probabilistic transition function defined for (s, a) if and only if a ∈ A(s).

The dynamic of the system is defined as follows. Given a current state s, an action a ∈ A(s) is chosen non deterministically. The next state is then randomly selected, using the corresponding distribution δ M (s, a), i.e., the probability that a transition to s occurs equals δ M (s, a)(s ). In a more suggestive way, one denotes δ M (s, a)(s ) by δ M (s |s, a) and s ∈S δ M (s |s, a) by δ M (S |s, a).

More formally, an infinite path through an MDP is a sequence π = s 0 a0 -→ s 1 a1 -→ • • • where s i ∈ S, a i ∈ A(s i ) and δ M (s i+1 |s i , a i ) > 0 for all i ∈ N: in the following, state s i is denoted by π(i). For every i ∈ N, π ↑i denotes the suffix of π starting in s i , i.e., π ↑i = s i ai

-→ s i+1 • • • . A finite path ρ = s 0 a0 -→ s 1 a1 -→ • • • an-1
---→ s n is a prefix of an infinite path ending in a state s n , denoted by last(ρ). We denote by Path M,s (respectively, FPath M,s ) the set of infinite paths (respectively, finite paths) starting in state s, whereas Path M (respectively, FPath M ) denotes the set of all infinite paths (respectively, finite paths).

To associate a probability space with an MDP, we need to eliminate the nondeterminism of the behaviour. This is done by introducing policies (also called schedulers or strategies). A policy of an MDP M = (S, α M , δ M ) is a function σ : FPath M → Dist(α M ) such that σ(ρ)(a) > 0 only if a ∈ A(last(ρ)). One denotes σ(ρ)(a) by σ(a|ρ). We denote by P ol M the set of all policies of M. A policy σ is deterministic when σ(ρ) is a Dirac distribution for every ρ ∈ FPath M (in that case, σ(ρ) denotes the action a ∈ A(last(ρ)) associated to probability one); it is stationary (also called memoryless) if σ(ρ) only depends on last(ρ).

A policy σ and an initial state s ∈ S yields a discrete-time Markov chain M σ s (see [5, Definition 10]), whose states are the finite paths of FPath M,s . The probability measure P r M σ ,s over paths of the Markov chain starting in s (with basic cylinders being generated by finite paths) defines a probability measure P r σ M,s over Path M,s , capturing the behavior of M from state s under policy σ.

Let ρ n = s 0 a0 -→ s 1 a1 -→ • • • an-1 ---→ s n and ρ n+1 = s 0 a0 -→ s 1 a1 -→ • • • s n an --→ s n+1 , the probability measure is inductively defined by P r σ M,s0 (ρ n+1 ) = P r σ M,s0 (ρ n ) a∈A(sn) σ(a|ρ n ) δ M (s n+1 |s n , a) .
One specifies properties on infinite paths as follows. Given a subset S ⊆ S of states and π = s 0 a0

-→ s 1 a1 -→ • • • ∈ Path M , π |= S iff s 0 ∈ S .
The atomic proposition {s} is more concisely denoted by s. One also uses Boolean operators ¬, ∧ and ∨ for building formulas. We finally use temporal operators F (for Finally) and G (for Globally). For a property ϕ, we let π |= F ϕ if there exists i ∈ N such that the suffix π ↑i of π verifies π ↑i |= ϕ. The dual operator G is defined by G ϕ ≡ ¬ F ¬ϕ. One also considers restricted scopes of these operators: π |= F n ϕ if there exists 0 i n such that π ↑i |= ϕ, and G n ϕ ≡ ¬ F n ¬ϕ. Given a property ϕ on infinite paths one denotes P r σ M,s ({π ∈ Path M,s | π |= ϕ}) more concisely by P r σ M,s (ϕ). Given a subset of target states T , reachability properties are specified by F T and safety properties by G ¬T . Our main goal is to compute the infimum and supremum reachability and safety probabilities, with respect to the policies, i.e., for ϕ ∈ {F T, G ¬T }:

P r min M,s (ϕ) = inf σ∈P ol M P r σ M,s (ϕ) and P r max M,s (ϕ) = sup σ∈P ol M P r σ M,s (ϕ). Since P r σ M,s (G ¬T ) = 1 -P r σ M,s (F T ), one immediately gets: P r max M,s (G ¬T ) = 1 -P r min M,s (F T ) , and P r min M,s (G ¬T ) = 1 -P r max M,s (F T
) . Thus we focus on reachability problems and without loss of generality, all the states of T may be merged in a single state called s + with A(s + ) = {loop + } such that δ M (s + |s + , loop + ) = 1. In the sequel, the vector (P r σ M,s (ϕ)) s∈S (respectively, (P r min M,s (ϕ)) s∈S and (P r max M,s (ϕ)) s∈S ) of probabilities will be denoted by P r σ M (ϕ) (respectively, P r min M (ϕ) and P r max M (ϕ)).

MEC decomposition and transient behaviour

In our approach, we first reduce an MDP by a qualitative analysis based on end components. We adopt here a slightly different definition of the usual one by allowing trivial end components (see later on). Preliminarily, the graph of an MDP M is defined as follows: the set of its vertices is S and there is an edge from s to s if there is some a ∈ A(s) with δ M (s |s, a) > 0.

Definition 1 (end component). Let M = (S, α M , δ M ). Then (S , α ) with ∅ = S ⊆ S and α ⊆ s∈S A(s) is an end component if (i) for all s ∈ S and a ∈ A(s) ∩ α , Supp(δ M (s, a)) ⊆ S ; (ii) the graph of (S , α ) is strongly connected.
Given two end components, one says that (S , α ) is smaller than (S , α ), denoted by (S , α ) (S , α ), if S ⊆ S and α ⊆ α . Given some state s, there is a minimal end component containing s namely ({s}, ∅). Such end components are called trivial end components. The union of two end components that share a state is also an end component. Hence, maximal end components (MEC) do not share states and cover all states of S. Furthermore, we consider bottom MEC (BMEC): a MEC (S , α ) is a BMEC if α = s∈S A(s). For instance ({s + }, {loop + }) is a BMEC. Every MDP contains at least one BMEC. The set of MECs of an MDP can be computed in polynomial time (see for instance [START_REF] Alfaro | Formal Verification of Probabilistic Systems[END_REF]). It defines a partition of S = Then for all n ∈ N, and for all s ∈ S, P r max

M,s (G nI ¬G 0 ) (1 -η I ) n . 3. For all s ∈ S, P r max M,s (G ¬G 0 ) = 0.
Proof. (Sketch) 1. One builds the partition of S by induction. We first let G 0 = M m=0 B m . Then, assuming that G 0 , . . . , G i have been defined, we let

G i+1 = {s ∈ S \ j i G j | ∀a ∈ A(s) ∃s ∈ j i G j δ M (s |s, a) > 0}.
The construction stops when some G i is empty. If G I is the last non-empty set, it can easily be checked that S = i I G i . 2. One observes that the path property G n ¬G 0 only depends on the prefix of length n. So there is only a finite number of policies up to n and we denote σ n the policy that achieves P r max M,s (G n ¬G 0 ). Observe also that after a path of length k < n leading to state s / ∈ G 0 , policy σ n may behave as policy σ n-k starting in s. The property may then be shown by using the fact that for all ] in order to decrease the complexity of the computation for reachability properties. We now introduce two variants of reductions for MDPs depending on the kind of probabilities we want to compute.

Characterization of minimal reachability probabilities

The reduction in the case of minimal reachability probabilities consists in merging all non-trivial MECs different from ({s + }, {loop + }) into a fresh state s -: all these states merged into s -will have a zero minimal reachability probability. Definition 3 (min-reduction). Let M be an MDP with the partition of S =

K i=k S k L =1 {t } M m=0 B m . We define M • = (S • , α M • , δ M • ) by:
-S • = {s -, s + , t 1 , . . . , t L }, and for all s ∈ S, s • is defined by: (1)

s • = t l if s = t , (2) s • = s + if s = s + , and (3)
s • = s -otherwise. -A • (s -) = {loop -}, A • (s + ) = {loop + } and for all 1 L, A • (t ) = A(t ). -For all 1 , L, a ∈ A • (t ), δ M • (s -|t , a) = δ M ( K i=k S k M m=1 B m |t , a), δ M • (s + |t , a) = δ M (s + |t , a), δ M • (t |t , a) = δ M (t |t , a), δ M • (s + |s + , loop + ) = δ M (s -|s -, loop -) = 1 .
An MDP M is called min-reduced if M = N • for some MDP N . The minreduction of an MDP is illustrated in Fig. 1-(b). The single trivial MEC ({t}, ∅) is preserved while MECs ({b, b }, {d, e}) and ({s, s }, {a, c}) are merged in s -. Proposition 4. Let M be an MDP and M • be its min-reduced MDP. Then for all s ∈ S, P r min M,s (F s + ) = P r min M • ,s • (F s + ).

We now establish another property of the min-reduced MDP that allows us to use Proposition 2.

Lemma 5. Let M • be the min-reduced MDP of an MDP M. Then every state s ∈ S • \ {s -, s + } is a trivial MEC.

In order to characterize P r σ M (F s + ) with a fixpoint equation, we define the set of S-vectors as

V = {x = (x s ) s∈S | ∀s ∈ S \ {s -, s + } 0 x s 1 ∧ x s+ = 1 ∧ x s-= 0}.
We also introduce the operator f min : V → V by letting for all x ∈ V: f min (x) s = min a∈A(s) s ∈S δ M (s |s, a)x s for every s ∈ S \ {s -, s + }, f min (x) s-= 0 and f min (x) s+ = 1.

We claim that there is a single fixed point of f min . In order to establish that claim, given a stationary deterministic strategy σ, we introduce the operator f σ : V → V defined for all x ∈ V by: f σ (x) s = s ∈S δ M (s |s, σ(s))x s for every s ∈ S \ {s -, s + }, f σ (x) s-= 0 and f σ (x) s+ = 1. Proposition 6. Let M be a min-reduced MDP. P r σ M (F s + ) is the unique fixed point of f σ . P r min M (F s + ) is the unique fixed point of f min and it is obtained by a stationary deterministic policy.

Characterization of maximal reachability probabilities

The reduction for maximal reachability probabilities is more complex. Indeed, we cannot merge any non-trivial MEC different from ({s + }, {loop + }) into the state s -anymore, since some of these states may have a non-zero maximal reachability probability. Hence, we consider a fresh state s k for each MEC S k and simply merge all BMECs B m 's different from ({s + }, {loop + }) into state s -.

Definition 7 (max-reduction). Let M be a MDP with the partition of S

= K i=k S k L =1 {t } M m=0 B m . Then the max-reduced M • = (S • , α M • , δ M • )
is defined by:

-S • = {s -, s + , t 1 , . . . , t L , s 1 , . . . , s K }. For all s ∈ S, one defines s • by: (1)

s • = t l if s = t l , (2) s • = s + if s = s + , (3) s • = s k if s ∈ S K , and (4)
s • = s -otherwise. -A • (s -) = {loop -}, A • (s + ) = {loop + } for all 1 L, A • (t ) = A(t ), and for all 1 k K, A • (s k ) = {a | ∃s ∈ S k a ∈ A(s) ∧ Supp(δ M (s, a)) S k }. -For all 1 , L, a ∈ A • (t ), 1 k, k K, b ∈ A • (s k ) ∩ A s with s ∈ S k , δ M • (s -|t , a) = δ M ( M m=1 B m |t , a), δ M • (s + |t , a) = δ M (s + |t , a), δ M • (t |t , a) = δ M (t |t , a), δ M • (s k |t , a) = δ M (S k |t , a), δ M • (s -|s k , b) = δ M ( M m=1 B m |s, b), δ M • (s + |s k , b) = δ M (s + |s, b), δ M • (t |s k , b) = δ M (t |s, b), δ M • (s k |s k , b) = δ M (S k |s, b), δ M • (s + |s + , loop + ) = δ M (s -|s -, loop -) = 1 .
Observe that M • is indeed an MDP since A • (s k ) cannot be empty (otherwise S k would be BMEC). Fig. 1-(c) illustrates the max-reduction of an MDP. The single trivial MEC ({t}, ∅) is preserved while MEC ({b, b }, {d, e}) is merged in s -. The MEC ({s, s }, {a, c}) is now merged into s 1 with only action g preserved.

The following propositions are similar to Proposition 4 and Lemma 5 for the min-reductions.

Proposition 8 [START_REF] Alfaro | Formal Verification of Probabilistic Systems[END_REF]Thm. 3.8]). Let M be an MDP and M • be its max-reduced MDP. Then for all s ∈ S, P r max M,s (F

s + ) = P r max M • ,s • (F s + ).
Lemma 9. Let M • be the max-reduced MDP of an MDP M. Then every state s ∈ S • \ {s -, s + } is a trivial MEC.

As for minimal reachability probabilities, we introduce operator f max : V → V by letting for all x ∈ V: f max (x) s = max a∈A(s) s ∈S δ M (s, a)(s )x s for all s ∈ S \ {s -, s + }, f max (x) s-= 0 and f max (x) s+ = 1.

We observe that Lemma 9 combined with Proposition 2 ensures that in a max-reduced MDP M, for any policy σ, S \ {s -, s + } is a set of transient states of M . This helps to prove that Proposition 6 also holds for max-reduced MDPs: Proposition 10. Let M be a max-reduced MDP. P r σ M (F s + ) is the unique fixed point of f σ . P r max M (F s + ) is the unique fixed point of f max and it is obtained by a stationary deterministic policy.

Discussion. Usually, algorithms that compute maximal and minimal reachability probabilities first determine the set of states for which those probabilities are 0 or 1, and merge them in states s -and s + respectively (see for instance [START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF]). For the case of minimal reachability probabilities, the MDP obtained after this transformation-which is a quotient of our M • -fulfills the hypotheses of Proposition 2 and our further development is still valid.

Unfortunately, it does not hold in the maximal case: for the MDP on the left of Fig. 1-(a), the obtained MDP, that we call M , simply merges {b, b } into s -, without merging {s, s } (since the maximal probability to reach s + from s or s is equal to 0.5, when choosing action b in s ). Moreover, Proposition 10 does not hold either in M for maximal probabilities 3 . In fact, the vector of maximal probabilities in M is only the smallest fixed point of f max . Indeed, the reader can check that the vector which is equal to 0 for s -, 0.7 for t, and 1 for all the other states is also a fixed point of f max , whereas the maximal reachability probability to reach s + from s or s is equal to 0.5. Notice that in the max-reduction M • of this MDP, the MEC ({s, s }, {a, c}) is merged into a single state, hence removing this non-unicity problem, as shown in Proposition 10.

While this issue does not preclude the standard computation of the probabilities, the approach we have followed enables us to solve the convergence issues of the previous methods. This is the subject of the next section.

Value iteration for reachability objectives

This section presents the value iteration algorithm used, for example in the PRISM model-checker [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF], to compute optimal reachability probabilities of an MDP. After stating convergence issues of this method, we give a new algorithm, called interval iteration algorithm, and the strong guarantees that it gives.

Convergence issues

The idea of the value iteration algorithm is to compute the fixed points of f min and f max (more precisely, the smallest fixed points of f min and f max ) by iterating them on a given initial vector, until a certain convergence criterion is met. More precisely, as recalled in [START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF], we let x (0) defined by x (0) s+ = 1 and x (0) s = 0 for s = s + (observe that x (0) is the minimal vector of V for the pointwise order), and we then build one of the two sequences x = (x (n) ) n∈N or x = (x (n) ) n∈N defined by x (0) = x (0) and for all n ∈ N,

x (n+1) = f min (x (n) ); -x (0) = x (0)
and for all n ∈ N, x (n+1) = f max (x (n) ). Since f min and f max are monotonous operators and due to the choice of the initial vector, x and x are non-decreasing bounded sequences, hence convergent. Let x (∞) and x (∞) be their respective limits. By continuity of f min and f max , x (∞) (respectively, x (∞) ) is a fixed point of f min (respectively, f max ). Due to Propositions 6 and 10, x (∞) (respectively, x (∞) ) is the vector P r min M (F s + ) (respectively, P r max M (F s + )) of minimal (respectively, maximal) reachability probabilities.

In practice, several stopping criteria can be chosen. In the model-checker PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of probabilistic real-time systems[END_REF], two criteria are implemented. For a vector x ∈ V, we let x = max s∈S |x s |. For x ∈ {x, x} and a given threshold ε > 0, the absolute criterion consists in stopping once x (n+1) -x (n) ε, whereas the relative criterion considers max s∈S (x

(n+1) s -x (n) s )/x (n) s
ε. However, as noticed in [START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF], no guarantees are obtained when using such value iteration algorithms, whatever the stopping criterion. As an example, consider the MDP (indeed the Markov chain) of Fig. 2. It is easy to check that (minimal and maximal) reachability probability of s + = 0 in state n is 1/2. However, if ε is chosen as 1/2 n (or any value above), the sequence of vectors computed by the value iteration algorithm will be x (0) = (1, 0, 0, . . . , 0, 0, . . . , 0), x (1) = (1, 1/2, 0, . . . , 0, 0, . . . , 0), x (2) = (1, 1/2, 1/4, . . . , 0, 0, . . . , 0), . . . , x (n) = (1, 1/2, 1/4, . . . , 1/2 n , 0, . . . , 0), at which point the absolute stopping criterion is met. Hence, the algorithm outputs x (n) n = 1/2 n as the reachability probability of s + = {0} in state n.

Example 11. The use of PRISM confirms this phenomenon. On this MDP, choosing n = 10 and threshold ε = 10 -3 < 1/2 10 , the absolute stopping criterion leads to the probability 9.77 × 10 -4 ≈ 1/2 10 , whereas the relative stopping criterion leads to the probability 0.198. It has to be noticed that the tool indicates that the value iteration has converged, and does not warn the user that a possible problem may have arisen. We consider a modification of the algorithm in order to obtain a convergence guarantee when stopping the value iteration algorithm. We provide (1) stopping criteria for approximation and exact computations and, (2) rate of convergence.

Stopping criterion for ε-approximation

Here, we introduce two other sequences. For that, let vector y (0) be the maximal vector of V, defined by y (0) s-= 0 and y (0) s = 1 for s = s -. We then define inductively the two sequences y and y of vectors by y (0) = y (0) and for all n ∈ N, y (n+1) = f min (y (n) ); y (0) = y (0) and for all n ∈ N, y (n+1) = f max (y (n) ). Because of the new choice for the initial vector, notice that y and y are nonincreasing sequences. Hence, with the same reasoning as above, we know that these sequences converge, and that their limit, denoted by y (∞) and y (∞) respectively, are the minimal (respectively, maximal) reachability probabilities. In particular, notice that x and y, as well as x and y, are adjacent sequences, and that x (∞) = y (∞) = P r min M (F s + ) and x (∞) = y (∞) = P r max M (F s + ) . Let us first consider a min-reduced MDP M. Then, our new value iteration algorithm computes both in the same time sequences x and y and stops as soon 0.5 0.5

1 2n 1 -1 n 1 1
Fig. 3. A Markov chain with less iterations for the initial state as y (n) -x (n) ε. In case this criterion is satisfied, which will happen after a finite (yet possibly large and not bounded a priori ) number of iterations, we can guarantee that we obtained over-and underapproximations of P r min M (F s + ) with precision at least ε on every component. Because of the simultaneous computation of lower and upper bounds, we call this algorithm interval iteration algorithm, and specify it in Algorithm 1. A similar algorithm can be designed for maximum reachability probabilities, by considering max-reduced MDPs and replacing min operations of lines 5 and 6 by max operations.

Theorem 12. For every min-reduced (respectively, max-reduced) MDP M, and threshold ε, if the interval iteration algorithm returns the vectors x and y on those inputs, then for all s ∈ S, P r min M,s (F s + ) (respectively, P r max M,s (F s + )) is in the interval [x s , y s ] of length at most ε.

Example 13. For the same example as the one in Example 11, our algorithm converges after 10548 steps, and outputs, for the initial state s = n, x n = 0.4995 and y n = 0.5005, given a good confidence to the user.

Notice that it is possible to speed up the convergence if we are only interested in the optimal reachability probability of a given state s 0 . Indeed, we can simply replace the stopping criterion y (n) -x (n) ε by y

(n) s0 -x (n) s0 ε.
Example 14. Let us look at the MDP (in fact a Markov chain) of Fig. 3 with initial state s 0 = n. Assume that we select threshold ε = 2 -(n-1) . For state s 0 , the algorithm stops after n-1 iterations with interval 1 3 , 1 3 (1 + 2 -(n-2) ) for the reachability probability. However, for the reaching probability of state 1, the interval after k iterations is

1 2n 0 i<k (1 -1 n ) i , 1 2n 0 i<k (1 -1 n ) i + (1 -1 n ) k . So it will stop when (1-1 n ) k 2 -(n-1) , i.e., k -(n-1) log 2 (1-1 n ) implying k = Θ(n 2 ).

Rate of convergence

We now establish guarantees on the rate of convergence of the interval iteration algorithm. Notice that the results also apply to the usual value iteration algorithm, even though the proof relies on the introduction of adjacent sequences. In the sequel, we assume that there is at least one transition probability 0 < δ < 1 (otherwise the problems are trivial).

Theorem 15. For a min-or max-reduced MDP M, and a convergence threshold ε, the interval iteration algorithm converges in at most I log ε log(1-η I ) steps, where I and η are introduced in Proposition 2.

Proof. Let σ be the policy corresponding to the minimal probability of satisfying G n ¬s -and σ be the policy corresponding to the minimal probability of satisfying F n s + . In particular, notice that P r σ M,s (G nI ¬s -) P r σ M,s (G nI ¬s -). Since G n ¬s -≡ G n ¬(s -∨ s + ) ∨ F n s + , with the disjunction being exclusive, we have for all s ∈ S,

P r min M,s (G nI ¬s -) -P r min M,s (F nI s + )) = P r σ M,s (G nI ¬s -) -P r σ M,s (F nI s + ) P r σ M,s (G nI ¬s -) -P r σ M,s (F nI s + ) = P r σ M,s (G nI ¬(s -∨ s + ) (1 -η I ) n
due to Proposition 2. It is easy to show by induction that x (n) = P r min M (F n s + ) and y (n) = P r min M (G n ¬s -). Then, we have y (nI) -x (nI) (1 -η I ) n . In conclusion, the stopping criterion is met when (1 -η I ) n ε, i.e., after at most I I log ε log(1-η I ) steps. A similar proof can be made for maximal probabilities. It may also be noticed, from similar arguments, that for all n, y ((n+1)I)x ((n+1)I)

(1 -η I ) y (nI) -x (nI) (and similarly for the maximum case), implying that the value iteration algorithm has a linear rate of convergence. Remark 16. One may use this convergence rate to delay the computation of one of the two adjacent sequences of Algorithm 1. Indeed assume that only x (n) is computed until step n. To use the stopping criterion provided by the adjacent sequences, one sets the upper sequence with y s-= 0 and then applies the algorithm. In the favorable cases, this could divide by almost 2 the computation time.

Stopping criterion for exact computation

In [START_REF] Chatterjee | Value iteration. In 25 Years of Model Checking[END_REF], a convergence guarantee was given for MDPs with rational transition probabilities. For such an MDP M, let d be the largest denominator of transition probabilities (expressed as irreducible fractions), N the number |S| of states, and M the number of transitions with non-zero probabilities. A bound γ = d 4M was announced so that, after γ 2 iterations, the obtained probabilities lie in intervals that could only contain one possible probability value for the system, permitting to claim for the convergence of the algorithm. So after γ 2 iterations, the actual probability might me computed by considering the rational of the form α/γ closest to the current estimate. However, no proof of this result is given in [START_REF] Chatterjee | Value iteration. In 25 Years of Model Checking[END_REF].

Using our simultaneous computation of under-and over-approximations of the probabilities, we provide an alternative stopping criterion for exact computation that moreover exhibits an optimal policy. Its proof is based on the fact that optimal probabilities are rational for which we can control the size of the denominator, and strongly relies on the existence of stationary optimal policies. Theorem 17. Let M be a reduced MDP with rational transition probabilities. Optimal reachability probabilities and optimal policies can be computed by the interval iteration algorithm in at most O((1/η) N N 3 log d).

The theorem also holds for the value iteration algorithm. Observe that our stopping criterion is significantly better than the bound d 8M claimed in [START_REF] Chatterjee | Value iteration. In 25 Years of Model Checking[END_REF] since N M and 1/η d. Furthermore M may be in Ω(N 2 ) even with a single action per state and 1/η may be significantly smaller than d as for instance in the extreme case η = 1 2 -1 10 n and d = 10 n for some large n.

Conclusion

We have provided a framework allowing to guarantee good properties when value iteration algorithm is used to compute optimal reachability probabilities of Markov decision processes. Our study pointed out some difficulties related to non-trivial end components in MDPs, that was not clearly described previously. Moreover, we gave results over the convergence speed, as well as criteria for obtaining exact convergence. As future works, it seems particularly interesting to test this algorithm on real instances, as it is done in [START_REF] Brázdil | Verification of Markov decision processes using learning algorithms[END_REF], where authors moreover apply machine learning techniques.

Fig. 1 -

 1 (a) shows the decomposition in MEC of an MDP. There are two BMECs ({s + }, {loop + }) and ({b, b }, {d, e}), one trivial MEC ({t}, ∅) and another MEC ({s, s }, {a, c}).

  where {t } is the set of states of a trivial MEC, B m is the set of states a BMEC and S k 's are the set of states of the other MECs. By convention, B 0 = {s + }. The next proposition is the key ingredient of our approach. Proposition 2. Let M be an MDP such that its MEC decomposition only contains trivial MECs and BMECs, i.e., S = L =1 {t } M m=0 B m . Then: 1. There is a partition S = 0 i I G i such that G 0 = M m=0 B m and for all 1 i I, s ∈ G i and a ∈ A(s), there is s ∈ j<i G j such that δ M (s |s, a) > 0. 2. Let η be the smallest positive probability occurring in the distributions of M.

Fig. 1 .

 1 Fig. 1. (a) An MDP and its MEC decomposition, (b) its min-reduction, and (c) its max-reduction

3

 3

Fig. 2 . 1 : 7 δ

 217 Fig. 2. A Markov chain with problems of convergence in value iteration

The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under Grant Agreement n601148 (CASSTING).

This is already observed in[START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF], but a wrong statement is made in[START_REF] Baier | Principles of Model Checking[END_REF] Thm. 10.100].

Acknowledgments. We thank the reviewer that pointed out the similarities between our approach and [2] (to be presented at the next ATVA, in Nov. 2014).


The 5th International Conference of The History of Medicine in Southeast Asia

Keywords: history of medicine, tropical medicine, malaria, prophylaxis, preventive medicine, colonialism, rubber plantations, French Indochina, Vietnam, social history, Michelin, hospitals, coolies, plantation workers, rubber industry, taylorism

Introduction

Setting up of healthcare system for Indochina's plantation workers only emerged as a priority to local colonial authorities in the mid-1920s, lagging years behind British Malaya and the Dutch East Indies. Basic healthcare had become not just an economic issue but also a social issue jeopardizing the future of the huge rubber tree plantations that had recently been opened by major French financial backers and industrial groups that had lost over half their workforce due to death, disease, repatriation or evasion in the space of just two years. This communication deals with healthcare with a focus on the allegedly "unique in the private sector" healthcare service first provided by Michelin in 1929 to cover over 6,000 native workers in its two plantations. This example is original because the Michelin plantations have often been decribed as the toughest, while the company was the symbol of paternalism in metropolitan France.

The analysis developed here draws heavily on an extensive and very well illustrated report drafted by Doctor Maurice Warnecke, a malaria expert, born in 1898, who was first assigned to the Department of medical assistance for Indochina in 1922 before joining Michelin in 1929 as head of the health department. His report looked to demonstrate the economic value of introducing an in-plantation healthcare scheme. The report never got publicly released -almost certainly because Michelin, at that time, was at loggerheads with other planters.

We start out by learning that both planters and the authorities failed to heed repeated warnings from the medical community until 1928. Up to this time, blame for the failure of sanitary measures was essentially laid on the native workers, with the local administration second in line. Planter's investment in healthcare came very late on -and not before a spate of worker deaths that, even today, remains a symbol of colonial violence.

We move on to look at what Michelin achieved after 1929, notably through the construction of an exemplary model hospital. We see how the investment effort helped galvanize the company's reputation, and we investigate if these investment, which was primarily oriented towards improving workers' physical condition rather psychological condition, was profitable.

I-A belated recognition of the appalling sanitary condition of the workforce

A-Disregarded warnings

The industrial and financial majors running rubber production in Indochina turned their eyes to the red-earth in Cochinchina as early as the 1910s, with a view to setting up huge capitalistically-engineered plantations within this area of dense forest ideal for rubber tree growth but harmful to workers' health. The growing workforce was given fixed-term contracts, and most came from the poor overpopulated regions of Tonkin. Michitake Aso recently demonstrated that despite the medical community's efforts from 1919 on to alert planters and local authorities on the need to take measures against malaria, almost nothing was done until 1925 when a medical entomology laboratory on malaria was opened. The planters systematically refused to comply with the rare legal provisions on health and waved away comments from the competent government departments. No money was actually allocated by the authorities to this field.

The situation got worse when tens of thousands of workers were transported in from Tonkin in under four years, starting in 1924. Planters essentially made efforts to issue quinine, which has been legislated for since 1922, and to educate coolies on how to preserve their own health. Once faced with the failure of this policy, the planters threw all responsibility on the natives themselves.

B-The coolie is the culprit

The behaviour of Michelin's top-echelon management is symptomatic of this mindset. The plantation doctor considers that the coolies' physical condition on arrival is appalling "because most of the time the people of Tonkin enlist only when at their wit's end and after suffering from malnutrition and a complete lack of hygiene". These indentured workers are depicted as "often depraved, trying to escape justice […], washed up, skirting around the medical examination, wholly inapt for work". The doctor also complains about the alleged "primitive lifestyle of Annam people when it comes to hygiene and their attitude to disease".

Natives are not only laid to blame, they are also supposed to learn, which starts through punishment. The doctor recommends that those who take off their bandage, forget to wash or be treated should be disciplined. For those suspected of feigning weakness or illness, the director of the Michelin plantation in Dầu Tiếng orders a fine amounting to the daily wage. Ipecacuanha was administered to workers suffering from bellyache to force them to vomit and deter them from complaining. Being provided with a mosquito net, which was essential to avoid bites, was not considered a right but a reward.

Coolies that refused to swallow their quinine pills had to take them dissolved in water, which has an incredibly bad taste. The white man was supposed to be a model. The European assistant have to take his own tablets in front of recently arrived workers. A large poster in the refectory of Michelin's hospital (see picture 1) portrays a huge Bibendum, the world-recognized symbol of the company, benevolently taking a coolie's shoulder and advising him to take his dose of quinine. Paternalism at its best, and undertones threatening violence! Racial prejudice served as a justification for the colonial system to impose tough working conditions and strict discipline in a much-monitored environment.

C-The administration's fault

Planters reproached the authorities for the lack of adequate hospital infrastructure in the territory. Above all, they were scathing on how labor law reform enacted by Governor-General Alexandre Varenne in October 1927 targeted the plantations. This law strengthened the power of planters on indentured workers but also contributed to an improvement in the coolies' health through specific obligations imposed on planters: prerecruitment checkups, food rations to be provided for free, healthcare, housing and sanitation. There was indeed urgent need to do something, as the numerous deaths among workers threatened to halt not just production but also the influx of workers -that was how bad the company's image had become.

D-A true hecatomb

Surveys led by the labour inspectorate and the Pasteur Institute arrived at much the same conclusion. About 90% of coolies of the red-earth heartland suffered from malaria and almost all had to be hospitalized once a month. The number of coolies either sick, dead or on the run reached almost half the entire workforce in some of the biggest plantations, which obviously also translated into a significant loss of earnings.

In Indochinese plantations as a whole, the death rate evolved as follows: 5.4% in 1927, 2.83% in 1929 and 1.72% in 1932. These average rates mask the diversity of on-theground situations. Data from 11 of the 20 biggest plantations (those counting over 700 workers) show that the death rate fluctuated between 12% and 47% in 1926 and 1927!

The head of Bù Đốp, where 47% of coolies died in 1927, managed to justify this figure by a "need to make sacrifices at the start of the plantation"! Phú Riềng, the Michelin site in the Red earth, was among these huge deadly plantations: 17 % of workers died in 1927 and another 15% the following year -all young men. The inexistent sanitary measures and relentless work required of the coolies go a large way to explaining these two-digit figures: malaria hit workers that were already on their knees.

Deaths alone don't sum up the losses. Close to a third of the workforce was unfit for work, and up to 20% of those tied up by a contract would be on the run, as was the case with Phú Riềng in 1927. Self-mutilation and suicides were also prominent.

Michelin's other plantation in Dầu Tiếng is often taken as symbol of colonial violence : according to figures released in 1965 by Điệp Liên Anh book's and repeated by various historians, 11 376 persons, a quarter of the workforce should have died there between 1924 and 1951. These statistics were made up, the actual death rate never exceeded 3 %.

Colonial brutality nevertheless was a reality... Alarmed by a productivity that was way under forecasts, Michelin realized in 1928 that it had to act. As Doctor Warnecke, who was recruited shortly after, said: "It is no longer possible to replace a worn-down coolie like a "spare part". There is no never-ending flow of workforce". He insisted on the vital need to improve both the physical and mental health of the coolies to ultimately make them more efficient. Michelin heard the first recommendation, not the second...

E-Sanitation works came late

The delay in starting sanitation work proves the lack of awareness of malaria-related risks.

While the Pasteur Institute demonstrated as early as 1918 that sanitation and keeping housing areas away from mosquito-breeding sites were the single most important preventive actions, most planters -Michelin included -simply ignored these factors when setting up their concessions, yet the outlays involved would have been relatively insignificant: even in plantations where drainage works were substantial (Snoul and Mimot for example), the costs amounted to barely 0.6% of total expenditure. At Michelin in Phú Riềng, the Pasteur Institute noted at the end of 1928 that the distribution of quinine was under-resourced and badly supervised, and that no anti-malaria initiative had been taken in the first two years. Work to drain the swamp and install drains did not start until November 1929. In other major concessions, similar work did not start until deep into the 1930s. While the 1927 regulation enabled the authorities to force planters to undertake such works, there is no evidence whatsoever of any such intervention.

II-Michelin's achievements and the consequent benefits

From early 1929 on, Michelin's management back in Clermont-Ferrand decided to create a « unique private sanitary facility in Indochina ».

The turning point was the recruitment of Doctor Warnecke and the forthright diagnosis he made on the sanitary and moral condition of workers. He was well aware that the improvement of the coolie's health could not be achieved only through prophylaxis or the setup of a healthcare infrastructure. There was also a need for better food, housing and hygiene ; education, leisure activities and spiritual life had to be encouraged ; special care should be given to women and children while the workload should be more proportionate to each one's might.

That the director of the antimalaria department of the colony came to Phú Riềng for his first on-ground experiments demonstrates how influential Michelin was. His recommendations were duly followed and proved very useful. A few weeks later, the Institute receives a 20000 piastres donation from Michelin, that was representing 10% of its annual budget. The company became the sole one in Indochina to hire an expert in antimalaria engineering, and it is the first to build coverded drains, much more effective. She is the first to replace the usual quinine pills with sweeter, candy-like tablets that were more easily accepted.

The attention paid to Michelin by the authorities is emblematic of the overall support brought to major plantations to the detriment of natives elsewhere.

It is only with the Varenne regulation that the first specific sanitary obligations imposed upon planters came into force. Ratios of nurses and infirmary beds were set according to the number of coolies ; above a certain threshold, the presence of a doctor was required.

The Michelin hospital, which opened in July 1929, has been time and again named as a model because of his size (see picture 2), its equipment and organization, but also because it remained for years the only one in Indochinese plantations. Four such facilities existed in Indochina in the latter in 1937, compared to close to 300 in Malaysia !

The hospital in Dầu Tiếng had 240 beds at first and was staffed with 20 native nurses.

Means and competences were centralized at the hospital to avoid the mistakes and late diagnosis which were previously common in the emergency units set up within the villages and were partially accountable for the numerous deaths.

Coolies were sorted out at their arrival on the plantation according to their working capacity and sick people at the hospital according to their disease. Hygiene had to be perfect and different units were created to deal with the various functions. Patients were followed up with very detailed medical cards. The facility also included a maternity ward, an efficient laboratory and other units.

The efforts undertaken after 1929 contributed to slightly improve the situation. While 10.2 % of Dầu Tiếng's workers were sick in November 1928, this figure had been lowered to 3.3% twelve months later. In Phú Riềng, the death rate declined from 17 % in 1927 to 3.3 all mentions the « absolutely deplorable planter's mentality » on Michelin's premises. He criticizes the sordid aspects of workers' housing and how the coolies were treated as prisoners regularly insulted and sometimes beaten.

Conclusion

Although Michelin committed as early as in 1926 to implement social measures similar to those set up for its employees in France, nothing was done until 1929. Other planters acted in the same way. The impact on the workers' health and fitness for work was however undervalued. The growing difficulty in renewing the workforce, the Varenne regulation of late 1927 and the soon-to-come economic crisis forced the planters to act.

Yet, there has never been any penalty even when they balked at taking initiatives.

Reacting more swiftly than his competitors, Michelin then invested significant amounts into a healthcare system, which proved profitable. Health-related costs actually dramatically decreased and the coolies' physical condition improved. Michelin's workers got better medical care than others but were mishandled and got the worst housing. Only their fitness for work mattered so as to increase the production.

Thanks to the better health of the coolies and to taylorization, productivity increased and so did the workers' workload, making Michelin's plantations some of the most profitable worldwide.

As a result, living and working conditions in the plantations have been portrayed up to now in a very negative way. This is especially true for Michelin's, which have often been described as the harshest and most inhuman plantations, while they were probably those with the highest level of commitment to a healthier environment.

In conclusion, I would like to express my warmest appreciation to the Scientific Committee of the Conference for accepting my paper. Special thanks are also due to professor Laurence Monnais for presenting my work to you today and to my brother for translating it into English.

HOMSEA-2014 -Eric Panthou paper

% in 1929, below the average rate for the colony, mostly thanks to advances in the fight against malaria. Unfit workers amounted to barely 5 % at the end of 1928 (and 3 % in May 1930) compared to 17% a year earlier.

While a day at the Michelin hospital cost 1.84 piastres, that is three times more than at a public facility, the company managed to keep its health expenditures below previous levels thanks to the decrease in hospitalizations. Most of all, this was a profitable investment as the number of coolies fit to work dramatically increased. The same kind of return on investment could be witnessed with the Michelin medical care offered to workers in France. 600,000 piastres, staff costs included, were spent by Michelin between 1926 and 1930 for its healthcare scheme, 200,000 were devoted to the hospital. To serve as a comparison, we know that the thirty five Michelin's Europeans employees costing 350,000 piastres to the company in 1928.

In Phú Riềng, in 1938, medical costs amounted to 4.6% of total expenditures, with 14,480 piastres. This was quite insignificant compared to an overall profit of 8.4 million.

The significant sums spent on healthcare and the very well organized system were at first commended by the authorities, such as the Department of Health Service, which considered in January 1930 that the hospital was « unique », « remarkable » and could be taken as model everywhere in Indochina and in the neighboring colonies.

Yet, even putting significant means in doesn't solve every problem. As a matter of fact, less than one month after Michelin had won praise from the government, almost all coolies rebelled in Phú Riềng ! The lack of reactivity from the nurses and the inadequate follow-up of patients was highlighted in various reports, including internal ones, and contributed to the worsening of preexisting pathologies. This situation arose from the pressure imposed upon nurses, which reflected the contradicting interests of the company : keep workers healthy but at the same time punish the « cheaters » and have as many coolies as possible at work. A 1937 report bemoaned Michelin's disregard for the rule compelling plantations with more than 1,000 workers to have an on-site doctor at any given time. The administration reminds the law but it does not oblige Michelin to apply it.

In 1937 again, the Governor General of Cochinchina acknowledged the company's achievements, such as this « wonderful » but « deserted » hospital. However, he most of

Illustrations