Patricia Bouyer
email: patricia.bouyer@lsv.fr

Mauricio González
email: mauricio.gonzalez@lsv.fr

Nicolas Markey
email: nicolas.markey@irisa.fr

Mickael Randour
email: mickael.randour@umons.ac.be

Multi-weighted Markov Decision Processes with Reachability Objectives

In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.

Introduction

Importing formal methods in connected fields. Formal methods can help providing algorithmic solutions for control design. The electric-vehicle (EV) charging problem is an example of such an application area. This problem, usually presented as a control problem (see eg. [START_REF] Beaude | Reducing the Impact of EV Charging Operations on the Distribution Network[END_REF]), can actually be modelled using Markov decision processes (MDP) [START_REF] Donadee | Stochastic Optimization of Grid to Vehicle Frequency Regulation Capacity Bids[END_REF][START_REF] Daniel | Practicality of Nested Risk Measures for Dynamic Electric Vehicle Charging[END_REF][START_REF] González | Stratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévision[END_REF]. Probabilities provide a way to model the non-flexible part of the energy network (consumption outside EV, for which large databases exist-and from which precise statistics can be extracted); we can then express an upper bound on the peak load as a safety condition (encoded as a reachability condition in our finite-horizon model), the constraint on the charging of all vehicles as a quantitative reachability objective, and various optimization criteria (e.g. minimizing the ageing of distribution transformers, or the energy price) as optimization of random cost variables.

Due to the specific form of the constructed model (basically acyclicity of the model), an ad-hoc method could be implemented using the tool PRISM, yielding interesting practical results as reported in [START_REF] González | Stratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévision[END_REF] and in a forthcoming paper. However, the computability of an optimal strategy in a general MDP, as well as the corresponding decision problem, was unexplored.

Markov decision processes. MDPs have been studied for long [START_REF] Puterman | Markov Decision Processes: Discrete Stochastic Dynamic Programming[END_REF][START_REF] Filar | Competitive Markov Decision Processes[END_REF]. An MDP is a finite-state machine, on which a kind of game is played as follows. In each state, several decisions (a.k.a. actions) are available, each yielding a distribution over possible successor states. Once an action is selected, the next state is chosen probabilistically, following the distribution corresponding to the selected action. The game proceeds that way ad infinitum, generating an infinite play. The way actions are chosen is according to a strategy (also called policy in the context of MDPs). Rewards and/or costs can be associated to each action or edge, and various rules for aggregating individual rewards and costs encountered along a play can be applied to obtain various payoff functions. Examples of payoff functions include:

• sum up all the encountered costs (or rewards) along a play, until reaching some target (finite if the target is reached, infinite otherwise)-this is the so-called truncated-sum payoff;

• sum up all the encountered costs (or rewards) along a play with a discount factor at each stepthis is the so-called discounted-sum payoff;

• average over the encountered costs (or rewards) along a play-this is the so-called mean-payoff.

Those payoff functions have been extensively studied in the literature; discounted-sum and mean-payoff have been shown to admit optimal memoryless and deterministic strategies, which can be computed using linear programming, yielding a polynomial-time algorithm. Alternative methods, such as value iteration or policy improvement, can be used in practice. On the other hand, the shortest-path problem, which aims at minimizing the truncated-sum, has been fully understood only recently [START_REF] Baier | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes[END_REF]: one can decide in polynomial time as well whether the shortest-path is finite, or whether it is equal to +∞ (if one cannot ensure reaching the target almost-surely), or whether it can be smaller than any arbitrary small number (if a negative loop can be enforced-note that in the context of stochastic systems, such a statement may be misleading, but it corresponds to a rough intuition), and corresponding strategies can be computed.

Multi-constrained problems in MDPs. The paradigm of multi-constrained objectives in stochastic systems in general, and in MDPs in particular, has recently arisen. It allows to express various (quantitative or qualitative) properties over the model, and to synthesize strategies accordingly. This new field of research is very rich and ambitious, with various types of objective combinations (see for instance [START_REF] Baier | Trade-off analysis meets probabilistic model checking[END_REF][START_REF] Randour | Variations on the Stochastic Shortest Path Problem[END_REF] for recent overviews). For recent developments on MDPs, one can cite:

• Pareto curves, or percentile queries, of multiple quantitative objectives: given several payoff functions, evaluate which tradeoff can be made between the probabilities, or the expectations, of the various payoff functions. In [START_REF] Chatterjee | Markov Decision Processes with Multiple Long-Run Average Objectives[END_REF][START_REF] Brázdil | Markov Decision Processes with Multiple Long-Run Average Objectives[END_REF][START_REF] Chatterjee | Unifying two views on multiple mean-payoff objectives in Markov decision processes[END_REF], solutions based on linear programming are provided for mean-payoff objectives. The percentile-query problem for various quantitative payoff functions is studied in [START_REF] Randour | Percentile queries in multi-dimensional Markov decision processes[END_REF].

• probability of conjunctions of objectives: given several payoff functions, evaluate the probability that all constraints are satisfied. This problem is studied in [START_REF] Haase | The Odds of Staying on Budget[END_REF] for reachability (that is, for the truncated-sum payoff function), a PSPACE lower bound is proved for that problem, already with a single payoff function.

• the "beyond worst-case" paradigm: satisfy both a safety constraint on all outcomes, and various performance criteria. Variations of this problem for various payoff functions have been studies in [START_REF] Clemente | Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives[END_REF][START_REF] Bruyère | Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games[END_REF][START_REF] Berthon | Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes[END_REF].

• conditional expectations [START_REF] Baier | Maximizing the Conditional Expected Reward for Reaching the Goal[END_REF] or conditional values-at-risk [START_REF] Kretínský | Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes[END_REF], which measures likelihoods of properties under some assumptions on the system, have recently been investigated.

Our contributions. The general multi-constrained problem, arising from the EV-charging problem as modelled in [START_REF] González | Stratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévision[END_REF], takes as an input an MDP with two weights, w 1 and w 2 , and requires the existence (and synthesis) of a strategy ensuring that some (absorbing) target state be reached, with a percentile constraint on the truncated sum of w 1 (lower bound parameterized by ε), and an expectation constraint on the truncated sum of w 2 . The initial EV-charging problem corresponds to the instance of that problem when ε = 0, where w 1 represents the energy that is used for charging and w 2 represents the ageing of the transformer.

As defined above, our problem integrates both the "beyond worst-case" paradigm of [START_REF] Bruyère | Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games[END_REF], and percentile queries as in [START_REF] Chatterjee | Unifying two views on multiple mean-payoff objectives in Markov decision processes[END_REF] (mixing probabilities and expectations). While in [START_REF] Chatterjee | Unifying two views on multiple mean-payoff objectives in Markov decision processes[END_REF] linear programs are used for solving percentile queries (heavily relying on the fact that mean-payoff objectives are tail objectives), we need different techniques since the truncated-sum payoff is very much prefix-dependent; actually, the PSPACE-lower bound of [START_REF] Haase | The Odds of Staying on Budget[END_REF] immediately applies here as well (even without a constraint on the expectation of w 2 ). We develop here a methodology to describe the cartography of the problem, that is, the set of values of the parameter ε for which the problem has a solution. Our approach is based on two sequences of optimization problems which, in some cases we characterize, allow to have the (almost) full picture. We then discuss computability issues.

Preliminary definitions

Let S be a finite set. We write Dist(S) for the set of distributions over S, that is, the set of functions

δ : S → [0, 1] such that ∑ s∈S δ (s) = 1. A distribution over S is Dirac if δ (s) = 1 for some s ∈ S.

Definition of the model

In this paper, we mainly focus on doubly-weighted Markov decision processes, but the technical developments mainly rely on simply-weighted Markov decision processes. We therefore define the setting with an arbitrary number of weights.

Definition 1. Let k ∈ N. A k-weighted Markov decision process (kw-MDP) is a tuple M = (S, s init , , E, (w i ) 1≤i≤k )
, where:

• S is a finite set of states;

• s init ∈ S is the initial state;

• ∈ S is the target state;

• E ⊆ S × Dist(S) is a finite set of stochastic edges;

• for each 1 ≤ i ≤ k, the function w i : S × S → Q assigns a rational weight to each transition of the complete graph with state space S.

A (finite, infinite) path in M from s is a (finite, infinite) sequence of states s 0 s 1 s 2 . . . such that s 0 = s and for every i, there is δ i ∈ Dist(S) such that (s i , δ i ) ∈ E and δ i (s i+1 ) > 0. Finite paths are equivalently called histories. We write Paths M (s) (resp. Paths M ∞ (s)) for the set of paths (resp. infinite paths), in M from state s. Given a history h = s 0 s 1 s 2 . . . s N and ≤ N, the w i -accumulated weight of h after steps is defined as Acc w i (h) = ∑ j=1 w i (s j-1 , s j ). This notion extends straightforwardly to infinite paths.

A (randomized) strategy in M is a function σ assigning to every history h = s 0 s 1 s 2 . . . s N a distribution over s N E = {δ ∈ Dist(S) | (s N , δ ) ∈ E}. A strategy σ is said to be pure whenever the distributions it prescribes are Dirac. A path s 0 s 1 s 2 . . . is an outcome of σ whenever for every strict prefix s 0 s 1 s 2 . . . s N , there exists δ ∈ s N E such that σ (h)(δ ) > 0 and δ (s N+1 ) > 0. Basically, the outcomes of a strategy are the paths that are activated by the strategy. We write out M (σ , s) (resp. out M ∞ (σ , s)) for the set of finite (resp. infinite) outcomes of σ from state s.

Given a strategy σ and a state s, we denote with P M σ ,s the probability distribution, according to σ , over the infinite paths in Paths M ∞ (s), defined in the standard way using cylinders based on finite paths from s. If f is a measurable functions from P M σ ,s to R, we denote by E M σ ,s ( f ) the expected value of f w.r.t. the probability distribution P M σ ,s , that is,

E M σ ,s ( f ) = f dP M σ ,s .
In all notations, we may omit to mention the superscript M when it is clear in the context, and may omit to mention the starting state s when it is s init , so that P σ corresponds to P M σ ,s init . Example 1. Consider the 2w-MDP M of Figure 1. It has four states s 0 , s 1 , s 2 and , and five edges, labelled with their names (here a, b, c, d and e). Weights label pairs of states (but are represented here only for pairs of states that may be activated). Edges a, b, d and e have Dirac distributions, while edge c has a stochastic choice (represented by the small black square). For readability we do not write the exact distributions, but in this example, they are assumed to be uniform.

Payoff functions

We are interested in quantitative reachability properties (also called truncated-sum in the literature), which we formalize as follows. Let ρ = s 0 s 1 s 2 • • • ∈ Paths(s 0 ). We use standard LTL-based notations for properties; for instance, we write ρ |= F (resp. ρ |= F I , when I is an interval of N) when there is j (resp. j ∈ I) such that s j = , and ρ |= G ¬ (resp. ρ |= G I ¬ , when I is an interval of N) when s j = for every j (resp. for every j ∈ I). We will often use expressions ∼ N (in {<, ≤, =, ≥, >} × N for defining intervals of N.

If ρ |= F and 1 ≤ i ≤ n, we define the i-th payoff function TS w i (ρ) as Acc N w i (ρ) where N is the least index such that ρ |= F =N . If ρ |= F then TS w i (ρ) = +∞. The function ρ → TS w i (ρ) is measurable, hence for every ν in {<, ≤, =, ≥, >} × Q, P σ ,s 0 ({ρ ∈ Paths ∞ (s 0 ) | TS w i (ρ) ν}) (simply written as P σ ,s 0 (TS w i ν)) and E σ ,s 0 (TS w i ) are well-defined. We write ρ |= (TS w i ν) whenever TS w i (ρ) ν.

In the rest of the paper, we assume that is a sink state, and that there is a single loop on whose weights are all equal to 0. This is w.l.o.g. since we will study payoff functions TS w i , which only consider the prefix up to the first visit to .

Example 2. Consider again the example of Figure 1. Consider the strategy σ which selects a or b uniformly at random in s 0 , and always selects c in s 1 . Then,

P σ ,s 0 F = 1 P σ ,s 0 TS w 1 ≥ 1 = 1 2 E σ ,s 0 TS w 2 = 1 2 • 5 + 1 2 • ∞ ∑ i=1 -i 2 i = 1 + 1 2

The problem

The problem that we tackle in this paper arises from a recent study of an EV-charging problem [START_REF] González | Stratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévision[END_REF].

The general problem we will define is a relaxed version of the original problem, combining several stochastic constraints (a percentile query over some payoff function and a constraint on the expectation of some payoff function) together with a worst-case obligation. While various payoff functions could be relevant, we focus on those payoff functions that were used for the EV-charging problem, that is, quantitative reachability (i.e., the truncated-sum payoff). We will see that the developed techniques are really specific to our choice of payoff functions.

In this paper, we focus on a combination of sure reachability of the goal state, of a percentile constraint on the proportion of paths having high value for the first payoff, and of a constraint on the expected value of the second payoff.

Let M = (S, s init , , E, (w 1 , w 2 )) be a 2w-MDP. Let ν 1 , ν 2 ∈ Q. For every ε ≥ 0, we define the problem Problem M ,ν 1 ,ν 2 (ε) as follows: there exists a strategy σ ε such that

1. for all ρ ∈ out M ∞ (σ ε , s init ), it holds ρ |= F ; 2. P M σ ε ,s init TS w 1 ≥ ν 1 ≥ 1 -ε; 3. E M σ ε ,s init TS w 2 < ν 2 .
We aim at computing the values of ε for which Problem M ,ν 1 ,ν 2 (ε) has a solution. For the rest of this section, we assume that there is a strategy

σ such that E σ ,s init TS w 2 < ν 2 . Otherwise Problem M ,ν 1 ,ν 2 (ε)
trivially has no solutions, for any ε. This can be decided using the algorithm recently developed in [START_REF] Baier | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes[END_REF].

Example 3. To illustrate the problem, we consider again the example given in Figure 1. Consider ε = 0.5, ν 1 = 1 and ν 2 = 4.3. The only way to satisfy the threshold constraint on w 1 is that at least half of the paths use a, impacting 2.5 over the expectation of w 2 . The other paths have to go to s 1 , and then take c for some time (provided the play goes back to s 1 ) in order to decrease the expectation of w 2 , before it becomes possible to take d and then e (so that the strategy is surely winning). This strategy uses both randomization (at s 0 ) and memory (counting the number of times c is taken before d can be taken).

We call the cartography of our problem the function which associates to every ε ∈ Link with the electric-vehicle (EV) charging problem. The (centralized) EV-charging problem consists in scheduling power loads within a time interval [0; T ] (T being a fixed time bound) with uncertain exogenous loads, so as to minimize the impact of loading on the electric distribution network (measured through the ageing of the transformer, which depends on the temperature of its winding). Following standard models, time is discretized, and the instantaneous energy consumption at time t can be written as the sum of the non-flexible load nf t (consumption outside EV) and the flexible load f t , corresponding to the EV charging. The flexible loads at each time are controllable actions, while the non-flexible part is known, or statistically estimated using past databases.

[0; 1], either true if Problem M ,ν 1 ,ν 2 (ε)
A first constraint on the transformer is given by its capacity: f t + nf t ≤ L max (where L max is a constant) for every 0 ≤ t ≤ T . A second constraint represents the charge required for charging all vehicles on schedule: ∑ T t=0 f t ≥ LoC max , where LoC max is a constant. The flexible load f t can thus be seen as a weight function w 1 .

While greedy solutions can be used to solve the above constraints, the ageing of thansformer has not been taken into account so far. Using a standard model for the ageing of a transformer (see [START_REF] Beaude | Reducing the Impact of EV Charging Operations on the Distribution Network[END_REF][START_REF] González | Stratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévision[END_REF] for details), it can be expressed as a weight function w 2 based on a discrete model in which states aggregate information on the system at the the two last timepoints. Globally, a 2w-MDP M can be built, such that a controller for the EV-charging problem coincides with a solution to Problem M ,LoC max ,ν 2 (0), for some bound ν 2 for the expected ageing of the transformer.

Approximated cartography

We fix a 2w-MDP M = (S, s 0 , , E, w 1 , w 2 ) and two thresholds ν 1 , ν 2 ∈ Q. We introduce two simpler optimization problems related to Problem M ,ν 1 ,ν 2 (ε), from which we derive informations on the good values of ε for which that problem has a solution. As we explain below, our approach is in general not complete. However, we observe that the true part of the cartography of our problem is an interval of the form γ; 1]; under some hypotheses, we prove that our approach allows to approximate arbitrarily the bound γ, but may not be able to decide if the interval is left-open or left-closed.

Optimization problems

Let N be an integer. We write φ + N for the property F ≤N ∧ TS w 1 ≥ ν 1 (which specifies that the target is reached in no more than N steps, with a w 1 -weight larger than or equal to ν 1 ), and φ - N for the property F ≤N ∧ TS w 1 < ν 1 (which means that the target is reached in no more than N steps, with a w 1 -weight smaller than ν 1 ). We write ψ N for the property G ≤N ¬ (the target is not reached during the N first steps). By extension, we write φ + , φ -and ψ for the properties F ∧ TS w 1 ≥ ν 1 , F ∧ TS w 1 < ν 1 and G ¬ . Finally, we may also (abusively) use such formulas to denote the set of paths that satisfy them.

For every N and every path ρ of M of length at least N, it holds that:

ρ |= φ + N ∨ φ - N ∨ ψ N .
Moreover, observe that φ + N ⊆ φ + and φ + ⊆ φ + N ∨ψ N . As a consequence, for every N and every strategy σ , P σ (φ + N ) ≤ P σ (φ + ) ≤ P σ (φ + N ∨ ψ N ).

First optimization problem

We define

val N = inf P σ φ - N ∨ ψ N | σ s.t. E σ TS w 2 < ν 2
and for every α > 0, we fix a witnessing strategy σ N,α for val N up to α (i.e. E σ N,α (TS w 2 ) < ν 2 and

P σ N,α (φ - N ∨ ψ N ) ≤ val N + α).
Remark. Note that, since we assume that there is a strategy σ such that E σ (TS w 2 ) < ν 2 , the constraint of this optimization problem is non-empty. Note also that if σ is a strategy such that E σ (TS w 2 ) < ν 2 , then P σ (F ) = 1, since for every path ρ, TS w 2 (ρ) = +∞ whenever ρ |= F .

It is not hard to see that the sequence (val N ) N∈N is non-increasing (see Appendix). We let γ = lim N→+∞ val N . We then have:

Lemma 2. For every ε < γ, Problem M ,ν 1 ,ν 2 (ε) has no solution.
Proof. Fix ε < γ, and assume towards a contradiction that Problem M ,ν 1 ,ν 2 (ε) has a solution.

Fix a winning strategy σ ε for Problem M ,ν 1 ,ν 2 (ε). By the first winning constraint, there exists N ε such that any outcome ρ ∈ out ∞ (σ ε ) satisfies F ≤N ε (thanks to König's lemma). Furthermore, since E σ ε (TS w 2 ) < ν 2 , then σ ε belongs to the domain of the optimization problem defining val N ε . Hence, we have

val N ε ≤ P σ ε φ - N ε ∨ ψ N ε = 1 -P σ ε φ + N ε = 1 -P σ ε φ + ≤ ε.
This is then a contradiction with ε < γ ≤ val N ε . Hence, we deduce that for every ε < γ, Problem M ,ν 1 ,ν 2 (ε) has no solution.

Lemma 3. For every N, for every

ε > val N ≥ γ, Problem M ,ν 1 ,ν 2 (ε) has a solution.
Proof. Let N be an integer, and ε > val N . Let σ N be a strategy such that

P σ N φ - N ∨ ψ N < ε and E σ N TS w 2 < ν 2
Let σ Att be an attractor (memoryless) strategy on M , that is, a strategy which enforces reaching ; write M for a positive upper-bound on the accumulated weight w 2 when playing that strategy (from any state). For k ≥ N, define σ k N as: play σ N for the first k steps, and if is not reached, then play σ Att . We show that we can find k large enough such that this strategy is a solution to Problem M ,ν 1 ,ν 2 (ε).

The first condition is satisfied, since either the target state is reached during the k first steps (i.e. while playing σ N ), or it will be surely reached by playing σ Att . Since

P σ k N (φ + N ) = 1 -P σ k N (φ - N ∨ ψ N ) and P σ k N (φ + N ) ≤ P σ k N (φ + ), it is the case that P σ k N (φ + ) ≥ 1 -ε,
which is the second condition for being a solution to Problem M ,ν 1 ,ν 2 (ε). Finally, thanks to the law of total expectation, we can write:

E σ k N TS w 2 = E σ k N TS w 2 | F ≤k • P σ k N (F ≤k ) + E σ k N TS w 2 | G ≤k ¬ • P σ k N (G ≤k ¬ ) ≤ E σ k N Acc k w 2 | F ≤k • P σ k N (F ≤k ) + E σ k N Acc k w 2 + M | G ≤k ¬ • P σ k N (G ≤k ¬ )
(since the global impact of playing the strategy σ Att is bounded by M)

= E σ k N Acc k w 2 + M • P σ k N (G ≤k ¬ )
(by linearity of expectation and the law of total expectation again)

= E σ N Acc k w 2 + M • P σ N (G ≤k ¬ ) (since σ k N coincides with σ N on the k first steps) Now, since E σ N (TS w 2 )
is finite, it is the case that P σ N (F ) = 1. Hence:

• lim k→+∞ E σ N (Acc k w 2 ) = E σ N (TS w 2 )
, and

• lim k→+∞ P σ N (G ≤k ¬ ) = 0. Let η = ν 2 -E σ N (TS w 2 ) > 0. One can choose k large enough such that E σ N Acc k w 2 -E σ N TS w 2 < η/2 and P σ N G ≤k ¬ < η/2M.
We conclude that:

E σ k N TS w 2 < E σ N TS w 2 + η < ν 2 .
The strategy σ k N therefore witnesses the fact that problem Problem M ,ν 1 ,ν 2 (ε) has a solution.

Second optimization problem

We now define

val N = inf P σ φ - N | σ s.t. E σ TS w 2 < ν 2 .
Notice that for any N, val N ≤ val N . For every α > 0, we fix a witness strategy σ N,α for val N up to α (so that E σ N,α (TS w 2 ) < ν 2 and P σ N,α (φ - N ) ≤ val N + α). This time, it can be observed that the sequence (val N ) N∈N is non-decreasing. We let γ = lim N→+∞ val N . From the results and remarks above, we have val N ≤ γ ≤ γ for any N. From Lemma 2, we get: Lemma 4. For any N and any ε < val N ≤ γ, Problem M ,ν 1 ,ν 2 (ε) has no solution.

While the status of problem M ,ν 1 ,ν 2 (γ) is in general unknown, we still have the following properties: Proposition 1.

• If Problem M ,ν 1 ,ν 2 (γ) has a solution, then the sequence (val N ) N is stationary and ultimately takes value γ. The converse need not hold in general;

• γ = γ does neither imply that Problem M ,ν 1 ,ν 2 (γ) has a solution, nor that Problem M ,ν 1 ,ν 2 (γ) has no solution. of Problem M ,ν 1 ,ν 2 (γ) remains uncertain. However, it remains to discuss two things: first, the limits γ and γ are a priori unknown, hence the cartography is not effective so far. The idea is then to use the sequences (val N ) N and (val N ) N to approximate the limits. We will therefore discuss cases where the two limits coincide (we then say that the approach is almost-complete), allowing for a converging scheme and hence an algorithm to almost cover the interval [0, 1] with either red (there are no solutions) or green (there is a solution), that is, to almost compute the full cartography of the problem. Second, we should discuss the effectiveness of the approach.

Summary

Almost-completeness of the approach

In this section, we discuss the almost-completeness of our approach, and describe situations where one can show that γ = γ def = γ, which allows to reduce the unknown part of the cartography to the singleton {γ}.

The situations for completeness we describe below are conditions over cycles, either on weight w 1 or on weight w 2 . When we assume that cycles have positive w i -weights, we mean it for every cycle, except for cycles containing , which we assumed are self-loops with weight 0.

When all cycles have a positive w 2 -weight

In this subsection, we assume that the w 2 -weight of each cycle of M is positive (this is the case for instance when the w 2 -weight of each edge is 1, i.e., when w 2 counts the number of steps). We let n be the number of states of M . Lemma 5. There exists a constant κ ≥ 0 such that, for any strategy σ satisfying E σ (TS w 2 ) < ν 2 , and any N > n, it holds:

P σ φ - N ∨ φ + N ≥ 1 - n N -n • κ.
Proof. Assuming otherwise, the impact of all runs that do not belong to φ - N ∨ φ + N would be too large for the constraint on TS w 2 . Indeed, applying the law total expectation, we can write for every N > n:

E M σ TS w 2 = E M σ TS w 2 | F ≤N • P M σ F ≤N + E M σ TS w 2 | G ≤N ¬ • P M σ G ≤N ¬
Write W 2 for the minimal (possibly negative) w 2 -weight appearing in M , and c 2 for the minimal (positive by hypothesis) w 2 -weight of cycles in M . Noticing that, along any path, at most n edges may be outside any cycle, we get

E M σ TS w 2 | F ≤N ≥ n •W 2 and E M σ TS w 2 | G ≤N ¬ ≥ n •W 2 + N -n n • c 2 .
We get:

E M σ TS w 2 ≥ n •W 2 • P M σ F ≤N + P M σ G ≤N ¬ + N -n n • c 2 • P M σ G ≤N ¬
Since the left-hand side is strictly smaller than ν 2 , we get

P M σ G ≤N ¬ = P M σ ψ N = 1 -P M σ φ + N ∨ φ - N ≤ n N -n • ν 2 -W 2 • n c 2 .
Lemma 6. For any constant κ satisfying Lemma 5, and any N > n, we have

0 ≤ val N -val N ≤ n N -n • κ.
Proof. We already remarked that val N ≤ val N . Now, from Lemma 5, for every strategy σ such that E σ TS w 2 < ν 2 , it holds for any N > n that

P σ ψ N < n N -n • κ.
From this lemma, we get that:

lim N→+∞ val N = 1 -sup{P σ φ + N 0 ∨ G ≤N 0 ¬ ∧ F >N 0 | σ s.t. E σ TS w 2 < ν 2 = inf{P σ φ - N 0 ∨ G ¬ | σ s.t. E σ TS w 2 < ν 2 (because a path not satisfying φ + N 0 ∨ G ≤N 0 ¬ ∧ F >N 0 satisfies φ - N 0 ∨ G ¬ ) = inf{P σ φ - N 0 | σ s.t. E σ TS w 2 < ν 2 (since P σ (G ¬ ) = 0 when E σ (TS w 2 ) < ν 2 ) = val N 0
Hence we conclude that γ = γ (and both limits are reached after finitely many steps).

Remark. This result requires the w 1 -positivity of cycles, as witnessed by the remark at the end of the previous section.

Also, one could think that assuming w 1 -negativity of cycles would be very similar, but this is not the case, as witnessed by the 2w-MDP defined by s a,-1,0

---→ s and s b,1,0 --→ . Then, for every N ≥ 2, val N = 0 while val N = 1.

Effectiveness of the approach

We now explain how the two optimization problems can be solved. We first unfold our original 2w-MDP M up to depth N as a tree, keeping a copy of M below each leaf; write T N for this new 2w-MDP.

There is a natural one-to-one mapping from paths in M and paths in T N , from which we derive another one-to-one mapping ι N between strategies in M and strategies in T N . Furthermore two corresponding strategies assign the same probabilities and the same accumulated weights to the paths. As a consequence, for any N, any κ N ∈ {φ + N , φ - N , ψ N }, and any strategy σ in M , we have

P M σ κ N = P T N ι N (σ ) κ N .
We do not formalize the relation between M and T N further, as it is rather straightforward.

Our two optimization problems can then be rephrased in T N as follows:

val N = inf P T N ι N (σ ) φ - N ∨ ψ N σ s.t. E T N ι N (σ ) TS w 2 < ν 2 and val N = inf P T N ι N (σ ) φ - N σ s.t. E T N ι N (σ ) TS w 2 < ν 2 .
From T N , we build the finite tree T N as follows: we keep the first N levels of T N , add a fresh state (at level N + 1), and from each leaf at level N, corresponding to some state s of M , we add an edge to labelled by the w 2 -stochastic shortest path value from s in M , that is, inf σ {E M σ ,s (TS w 2 )}. Those can be computed [START_REF] Baier | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes[END_REF] (note that each can either be -∞ or a finite value, or +∞ if cannot be almost-surely reached).

Every strategy σ N in T N can then be partly mimicked in T N (up to the N-th level of the tree); at level N, there is a single transition, which directly reaches while increasing weight w 2 by the shortest-path value mentioned above. We write σ N for this strategy in T N derived from σ N . Then

we have

E T N σ N (TS w 2 ) ≤ E T N σ N (TS w 2 )
, since the transitions from the nodes at level N to the state in T N somehow acts as an"optimal" strategy after the first N levels.

Conversely, for every strategy σ N in T N such that E T N σ N (TS w 2 ) < ν 2 :

• if E T N σ N (TS w 2 ) = -∞, then for every r ∈ R, one can extend σ N into a strategy σ N,r in T N such that E T N σ N,r (TS w 2 ) < r; • otherwise, if E T N σ N (TS w 2 ) = -∞, then one can extend σ N into a strategy σ N in T N such that E T N σ N (TS w 2 ) = E T N σ N (TS w 2 ).
Hence the set of strategies σ N in T N such that E T N σ N (TS w 2 ) < ν 2 coincides with the set of strategies obtained as a pruning of a strategy σ N in T N such that E T N σ N (TS w 2 ) < ν 2 . Our two optimization problems can then be rephrased as:

val N = inf P T N σ N φ - N ∨ ψ N | σ N s.t. E T N σ N TS w 2 < ν 2 and val N = inf P T N σ N φ - N | σ N s.t. E T N σ N TS w 2 < ν 2
Since T N is a (finite) tree, each strategy σ N in that MDP is memoryless, and can be represented as a probability value given to each edge appearing in the tree.

For each node n of T N , corresponding to some state s of M , and for each edge e = (s, δ ) from s, we consider a variable p n,e , intended to represent the probability of taking edge e at node n. In particular, we will have the constraints 0 ≤ p n,e ≤ 1 and ∑ e=(s,δ ) p n,e = 1. We write P = (p n,e ) n,e for the tuple of all variables.

The two optimization problems above can then be written as:

inf P P(P) Q(P) < ν 2 ∧ n,e 0 ≤ p n,e ≤ 1 ∧ n ∑ e=(s,δ )
p n,e = 1 where P(P) and Q(P) are polynomials (of degree at most N).

Such polynomial optimization problems are in general hard to solve, and we have not been able to exploit the particular shape of our optimization problem to get efficient specialized algorithms. For each N, arbitrary under-approximations of val N and over-approximations of val N can be obtained by binary search, using the existential theory of the reals: the latter problem can be solved in polynomial space, but the number of variables of our problem is exponential in N. Using Lemmas 3 and 4, we get informations about the cartography of our problem. We can get approximations of γ and γ by iterating this procedure for larger values of N.

Remark. In case the constraint on the expectation of w 2 can be relaxed (for instance if it is trivially satisfied), then the problem (over T N ) becomes a simple optimal reachability problem in an MDP, for which pure strategies are sufficient (we have seen that this cannot be the case in our setting). The above optimization problem then simplifies into a linear-programming problem, with a much better complexity.

7 The special case of Problem M ,ν 1 ,ν 2 (0)

While the previous developments cannot give a solution to Problem M ,ν 1 ,ν 2 (0) since it requires not only to show that γ = γ = 0, but also that there is a solution to the limit point γ (which we do not have in general). We dedicate special developments to that problem. In this section, we assume (w.l.o.g.) that weights take integer values.

Problem M ,ν 1 ,ν 2 (0) can be rephrased as follows: there exists a strategy σ 0 such that:

1. for all ρ ∈ out M ∞ (σ 0 , s init ), TS w 1 (ρ) ≥ ν 1 ; 2. E M σ ε ,s init TS w 2 < ν 2 .
Note that this problem is somehow a "beyond worst-case problem", as defined in [START_REF] Randour | Percentile queries in multi-dimensional Markov decision processes[END_REF], with a strong constraint on all outcomes, and a stochastic constraint (here defined using expected value).

We describe a solution in the case all cycles of M have non-negative w 1 -weights, which is inspired from [START_REF] Randour | Percentile queries in multi-dimensional Markov decision processes[END_REF]Theorem 13]. As we explain below, our solution extends to multiple weights (with nonnegative cycles) with strong constraints (like the one for w 1 ). However, it is not correct when w 1 may have negative cycles as well. In that case, the status of the problem remains open.

We "unfold" the 2w-MDP M = (S, s init , , E, w 1 , w 2 ) into a 1w-MDP N = (Q, q init , Q , T, w), explicitly keeping track of w 1 in the states of N :

• Q = S × {-M, -M + 1, . . . , 0, 1, . . . , M + ν 1 + 1, ∞}, where M = W • (|S| + 1), W is the maximal
absolute value of all weights w 1 (s, s ) in M , and ν 1 is the integral part of ν 1 ;

• q init = (s init , 0);

• Q = {( , k) | k = ∞ or k ≥ ν 1 }; • T = ((s, c), (s , c )) (s, s ) ∈ E and c = ∞ if c + w 1 (s, s ) > M + ν 1 + 1 or c = ∞ c = c + w 1 (s, s )
otherwise ;

• w((s, c), (s , c )) = w 2 (s, s ).

There is a natural one-to-one correspondence λ between paths in M and those in N : λ (s 0 s 1 . . . s k . . . ) = (s 0 , 0)(s 1 , c 1 ) . . . (s k , c k ) . . . where, for every k, c k = c k-1 + w 1 (s k-1 , s k ) if this value is less than or equal to M + ν 1 + 1, and c k = ∞ otherwise. Notice that thanks to our hypothesis on cycles, c k may never be less than -M. Also, by construction, if (s 0 , 0)(s 1 , c 1 ) . . . (s k , c k ) . . . is a path in N such that c k = ∞, then for every j ≥ k, c j = ∞; in that case, in the corresponding path s 0 s 1 . . . s k . . . in M , it is the case for every j ≥ k that Acc j w 1 (s 0 s 1 . . . s k . . . ) ≥ ν 1 (indeed, once the accumulated weight has become larger than M + ν 1 , it can never be smaller than ν 1 again, thanks to the hypothesis on cycles).

Conversely, if c k < ∞, then Acc k w 1 (s 0 s 1 . . . s k . . . ) = c k .
From that correspondence over paths, strategies in M can equivalently be seen as strategies in N via a mapping ι. Using this correspondence: Lemma 11. There is a solution to Problem M ,ν 1 ,ν 2 (0) if, and only if, in N there is a strategy τ such that:

1. for all ρ ∈ out N ∞ (τ, q init ), ρ |= F Q ; 2. E N τ,q init TS Q w < ν 2 .
Furthermore, if σ is a solution to Problem M ,ν 1 ,ν 2 (0), then τ = ι(σ ) is a solution to the above problem in N ; and if τ is a solution to the above problem in N , then σ = ι -1 (τ) is a solution to Problem M ,ν 1 ,ν 2 (0).

We can further show that Problem M ,ν 1 ,ν 2 (0) has a solution if, and only if, the stochastic w 2 -shortestpath for reaching Q in N from s init is smaller than ν 2 . This latter problem can be decided in PTIME [START_REF] Baier | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes[END_REF]. However, the size of N is exponential (more precisely, it is pseudo-polynomial in the size of M ). In the end: Theorem 12. One can decide Problem M ,ν 1 ,ν 2 (0) in pseudo-polynomial time, when cycles of M have a non-negative w 1 -weight.

Remark. Notice that we could also have assumed that all cycles have non-positive w 1 -weight: the construction of N would be similar, but with state space S × {-∞, ν 1 -1 -M , ..., 0, 1, ..., M + 1} where M = W • (|S| + 1) and W is the largest absolute value w 1 -weight in M . The rest of the argumentation follows the same ideas as above.

Notice also that our algorithm is readily adapted to the case where we may have several constraints similar to those on w 1 (for each extra variable, one should assume that either each cycle is non-negative, or each cycle is non-positive). It suffices to keep track of the extra weights in the states, and take as target all states where the constraints are fulfilled.

Conclusion

In this paper, we investigated a multi-constrained reachability problem over MDPs, which originated in the context of electric-vehicle charging [START_REF] González | Stratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévision[END_REF]. This problem consists in finding a strategy that surely reaches a quantitative goal (e.g., all vehicles are fully charged and the load of the network remains below a given bound at any time) while satisfying a condition on the expected value of some variable (the life expectancy of the transformer is high or the expected cost of charging all vehicles is minimized). We developed partial solutions to the problem by providing a cartography of the solutions to (a relaxed version of) the problem. We identified realistic conditions under which the cartography is (almost) complete. However, even under these conditions, the general decision problem (given ε, does Problem(ε) have a solution?) remains open so far. Also, the case of MDPs not satisfying these conditions remains also open, but we believe that our approximation techniques may give interesting informations which suffice for practical applications such as electric-vehicle charging.

Our approach for Problem(0), which amounts to explicitly keep track of the worst-case constraint on w 1 , immediately extends to multiple weights with worst-case constraints (with the same assumptions on cycles-note that the more general setting could not be solved, which has to be put in parallel with the undecidability result of [START_REF] Randour | Percentile queries in multi-dimensional Markov decision processes[END_REF]Theorem 12]) for the multi-dimensional percentile problem for truncated sum payoffs. The cartography for the relaxed problem Problem(ε) requires solving sequences of intermediary optimization problems, which can be expressed as polynomial optimization problems with polynomial constraints. It could be extended to several such weights as well (either by putting an assumption on the w 1 -weights of every cycle, or just on the w 2 -weight of every cycle). A nice continuation of our work would consist in computing (approximations of) Pareto-optimal solutions in such a setting. Improving the complexity and practicality of our approach is also on our agenda for future work.

A Proofs Lemma 13. For every N, it holds val N+1 ≤ val N .

Proof. Fix some α > 0, and consider strategy σ N,α . Clearly, φ - N+1 ⊆ ψ N ∨ φ - N , and ψ N+1 ⊆ ψ N . Hence

val N+1 ≤ P σ N,α φ - N+1 ∨ ψ N+1 ≤ P σ N,α φ - N ∨ ψ N ≤ val N + α.
This allows to conclude that val N+1 ≤ val N .

Lemma 14. For every N, we have val N ≤ val N+1 .

Proof. Fix some α > 0, and consider strategy σ N+1,α . It is clear that φ

- N ⊆ φ - N+1 , hence val N ≤ P σ N+1,α φ - N ≤ P σ N+1,α φ - N+1 ≤ val N+1 + α.
We conclude that val N ≤ val N+1 .

Proposition 1.

• If Problem M ,ν 1 ,ν 2 (γ) has a solution, then the sequence (val N ) N is stationary and ultimately takes value γ. The converse need not hold in general;

• γ = γ does neither imply that Problem M ,ν 1 ,ν 2 (γ) has a solution, nor that Problem M ,ν 1 ,ν 2 (γ) has no solution.
Proof. Pick a solution σ to Problem M ,ν 1 ,ν 2 (γ) and an integer N corresponding to the size of the outcome tree of σ (due to the fact that all outcomes of σ eventually hit the goal state, thanks to Kőnig's lemma, the tree is finite). Then, since no ε < γ can be such that σ is a solution to Problem M ,ν 1 ,ν 2 (ε), one can show that:

P σ φ + N = 1 -γ and P σ φ - N ∨ ψ N = P σ φ - N = γ
hence val N ≤ γ. This proves that the sequence (val N ) N is stationary (equal to γ after some index N).

For the second claim, consider the 2w-MDP of Figure 3, with ν 1 = 1 and ν 2 = 2.1. For every N, val N = 0, but val N = 1/2 N . Both sequences converge to 0, but Problem M ,ν 1 ,ν 2 (0) has no solution. Note that the sequence (val N ) N is not stationary.

s 0 s 1 a 0, 1 0, 1 b - 1 , 1 c 0 , 0 Figure 3: A 2w-MDP M with no solutions to Problem M ,1,2.1 (0) Lemma 10. lim N→+∞ sup{P σ φ + N 0 ∨ G ≤N 0 ¬ ∧ F (N 0 ;N] | σ s.t. E σ TS w 2 < ν 2 = sup{P σ φ + N 0 ∨ G ≤N 0 ¬ ∧ F >N 0 | σ s.t. E σ TS w 2 < ν 2
Proof. For the sake of readability, we let Σ ν 2 be the set of strategies σ satisfying condition E σ TS w 2 < ν 2 .

For any strategy σ , we have

P σ φ + N 0 ∨ F (N 0 ;N] ≤ P σ φ + N 0 ∨ F >N 0 , so that sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F (N 0 ;N] ≤ sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F >N 0 .
This proves the inequality

lim N→+∞ sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F (N 0 ;N] ≤ sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F >N 0 .
Fix δ > 0 and pick σ ∈ Σ ν 2 such that:

sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F >N 0 -δ < P σ φ + N 0 ∨ F >N 0 .
Since σ must reaching almost-surely, there must exist N 1 such that for any

N ≥ N 1 , sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F >N 0 -δ < P σ φ + N 0 ∨ F (N 0 ;N] .

It follows sup

σ ∈Σ ν 2

P σ φ + N 0 ∨ F >N 0 -δ < sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F (N 0 ;N]
We conclude that for every δ > 0 sup

σ ∈Σ ν 2 P σ φ + N 0 ∨ F >N 0 -δ ≤ lim N→+∞ sup σ ∈Σ ν 2 P σ φ + N 0 ∨ F (N 0 ;N]
As this holds for every δ > 0, we get the converse inequality, which proves the lemma.

Lemma 11. There is a solution to Problem M ,ν 1 ,ν 2 (0) if, and only if, in N there is a strategy τ such that:

1. for all ρ ∈ out N ∞ (τ, q init ), ρ |= F Q ; 2. E N τ,q init TS Q w < ν 2 .
Furthermore, if σ is a solution to Problem M ,ν 1 ,ν 2 (0), then τ = ι(σ ) is a solution to the above problem in N ; and if τ is a solution to the above problem in N , then σ = ι -1 (τ) is a solution to Problem M ,ν 1 ,ν 2 (0).

Proof. Let σ be a solution to Problem M ,ν 1 ,ν 2 (0), and let τ = ι(σ ). Assume towards a contradiction that there is ρ ∈ out N ∞ (τ, q init ) such that ρ |= F Q . Write ρ = (s 0 , 0)(s 1 , c 1 ) . . . (s k , c k ) . . . By correspondence of the strategies, the path λ -1 (ρ) belongs to out M ∞ (σ , s init ), hence λ -1 (ρ) |= TS w 1 ≥ ν 1 and ρ |= F ({ } × {0, 1, . . . , M, ∞}). However, since ρ |= F Q , ρ must end up in some state ( , c) / ∈ Q , hence with c < ν 1 . Justified by the previous discussion, ρ never visits a state (s, ∞), hence for every k, c k = Acc k w 1 (λ -1 (ρ)). This is a contradiction. Now, the expectation of w 2 in M is the same as that of w in N , hence the second condition is also satisfied. Strategy τ is therefore a solution to the above problem.

Conversely, pick a strategy τ in N which is solution to the problem described in the Lemma. Let σ = ι -1 (τ). Since any path ρ ∈ out N ∞ (τ, q init ) satisfies F Q , we get that any path ρ ∈ out M ∞ (σ , s init ) satisfies F and P M σ (TS w 1 ≥ ν 1 ) = 1 (this is easy to prove). The constraint on the expectation of w 2 is also straightforward. This concludes the proof.

Theorem 12. One can decide Problem M ,ν 1 ,ν 2 (0) in pseudo-polynomial time, when cycles of M have a non-negative w 1 -weight.

Proof. We show that there is a solution to that problem if, and only if, the shortest-path w-value π for reaching Q in N from s init is smaller than ν 2 . This latter problem can be decided in PTIME [START_REF] Baier | Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes[END_REF]. However, the size of N is exponential (more precisely, it is pseudo-polynomial in the size of M ). Hence the announced complexity.

The right-to-left implication is obvious. Assume now that the shortest-path w-value π is smaller than ν 2 . Let 0 < η < ν 2π. We distinguish between two cases:

• either π is -∞: we then let σ SP be a strategy achieving expected value smaller than ν 2η;

• or π is finite: we then let σ SP be a strategy achieving expected value π.

In both cases,

E N σ SP ,q init TS Q w + η < ν 2 .
Note that all the states activated by σ SP belong to the attractor of Q , since the probability to reach that set is 1. Let σ Att be a (memoryless) attractor strategy from every activated state to Q . The trees rooted at each state s and generated by σ Att are finite, and one can bound the maximal accumulated w-weight by some uniform bound K.

Following the proof of Lemma 3, for k ≥ N, we define σ k as follows: play σ Att for the first k steps, and if has not been reached after k steps, then play σ Att . We show that we can find k large enough such that this strategy is a solution to our problem.

The first condition is satisfied, since either the target state is reached during the first k steps (i.e., while playing σ SP ), or it is surely reached when playing σ Att . Now, thanks to the law of total expectation, we can write: is finite, it is the case that P N σ SP F Q = 1. Hence:

E N σ k TS Q w = E N σ k TS Q w F ≤k Q • P N σ k (F ≤k Q ) + E N σ k TS Q w G ≤k ¬Q • P N σ k (G ≤k ¬Q ) ≤ E N σ k Acc k w F ≤k Q • P N σ k (F ≤k Q ) + E N σ k Acc k w + K G ≤k ¬Q • P N σ k (G ≤k
• lim k→+∞ E N σ SP Acc k w = E N σ SP TS Q w
, and

• lim k→+∞ P N σ SP (G ≤k ¬Q ) = 0. One can choose k large enough so that

E N σ SP Acc k w -E N σ SP TS Q w
< η/2 and P N σ SP (G ≤k ¬Q ) < η/2K.

We conclude that:

E N σ k TS Q w < E N σ SP TS Q w + η < ν 2 .
Strategy σ k is therefore a witness strategy for our problem.

Figure 1 :

 1 Figure 1: An example of a 2w-MDP

  has a solution, or false otherwise. It is easily seen that the cartography is a threshold function, and can be characterized by an interval I = γ; 1] (which may be left-open or leftclosed): In what follows, we describe an algorithmic technique to approximate this interval, and under additional conditions, to compute the bound γ. Whether the bound belongs to the interval remains open in general.

Figure 2

 2 Figure2summarizes the previous analysis. The picture seems rather complete, since only the status

Figure 2 :

 2 Figure 2: A partial cartography of our problem

  ¬Q ) (since the global impact of playing the strategy σ Att is bounded by K)= E N σ k Acc k w + K • P N σ k (G ≤k ¬Q )(by linearity of expectation and the law of total expectation again)= E N σ SP Acc k w + K • P N σ SP (G ≤k ¬Q ) (since σ k coincides with σ SP on the first k steps) Now, since E N σ SP TS Q w

Acknowledgement. We thank the anonymous reviewers for their careful reading of our submission.

Patricia Bouyer, Mauricio González and Nicolas Markey are supported by ERC project EQualIS. Mickael Randour is an F.R.S.-FNRS Research Associate, and he is supported by the F.R.S.-FNRS Incentive Grant ManySynth.

Hence, for any strategy σ and any N > n,

Taking the infimum over σ , first in the left-hand side, and then in the right-hand side, we get the expected bound.

Corollary 7. γ = γ.

Remark. Notice that the result does not hold without the assumption. Indeed, consider the 2w-MDP defined by the two deterministic edges s a,0,0 --→ s and s b,-1,0

---→ , with ν 1 = 0. Then, for every N, val N = 0, while val N = 1.

When all cycles have a positive w 1 -weight

We assume that each cycle of M has a positive w 1 -weight. We first notice that: Lemma 8. There exists an integer N 0 such that for every path ρ from s init of length N ≥ N 0 not visiting the goal state, it holds Acc N w 1 (ρ) ≥ ν 1 . In particular, if ρ satisfies

Using this remark, we can prove:

Proof. We fix the index N 0 as in Lemma 8. For any N ≥ N 0 and any path ρ of length larger than N, we have

From the first equivalence, we infer that for every N ≥ N 0 , val N = val N 0 .

Let N > N 0 , and write:

We claim that: