extfieldsofstudy:
Computer Science
Mathematics

text:
Symbolic Approximation of Weighted Timed Games

Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation schema on this class.

Introduction
The design of programs verifying some real-time specifications is a notoriously difficult problem, because such programs must take care of delicate timing issues, and are difficult to debug a posteriori. One research direction to ease the design of real-time software is to automatise the process. The situation may be modelled into a timed game, played by a controller and an antagonistic environment: they act, in a turn-based fashion, over a timed automaton [2], namely a finite automaton equipped with real-valued variables, called clocks, evolving with a uniform rate. A simple, yet realistic, objective for the controller is to reach a target location. We are thus looking for a strategy of the controller, that is a recipe dictating how to play so that the target is reached no matter how the environment plays. Reachability timed games are decidable [4], and EXPTIME-complete [19].
Weighted extensions of these games have been considered in order to measure the quality of the winning strategy for the controller [9,1]: when the controller has several winning strategies in a given reachability timed game, the quantitative version of the game helps choosing a good one with respect to some metrics. This means that the game now takes place over a weighted (or priced) timed automaton [5,3], where transitions are equipped with weights, and locations with rates of weights (the cost is then proportional to the time spent in this location, with the rate as proportional coefficient). While solving the optimal reachability problem on weighted timed automata has been shown to be PSPACE-complete [6] (i.e. the same complexity as the non-weighted version), weighted timed games are known to be undecidable [12]. This has led to many restrictions in order to regain decidability, the first and most interesting one being the class of strictly non-Zeno cost with only non-negative weights (in transitions and locations) [9]: this hypothesis requires that every execution of the timed automaton that follows a cycle of the region automaton has a weight far from 0 (in interval [1, +∞), for instance).
Negative weights are crucial when one wants to model energy or other resources that can grow or decrease during the execution of the system to study. In [16], we have recently extended the strictly non-Zeno cost restriction to weighted timed games in the presence of negative weights in transitions and/or locations. We have described there the class of divergent weighted timed games where each execution that follows a cycle of the region automaton has a weight far from 0, i.e. in (−∞, −1] ∪ [1, +∞). We were able to obtain a doubly-exponential-time algorithm to compute the values and almost-optimal strategies, while deciding the divergence of a weighted clocks of X is a conjunction of atomic constraints of the form x ⊲⊳ c, where ⊲⊳ ∈ { , <, =, >, } and c ∈ Q (we allow for rational coefficients as we will refine the granularity in the following). Guard g is the closed version of a satisfiable guard g where every open constraint x < c or x > c is replaced by its closed version x c or x c. A valuation ν : X → R 0 satisfies an atomic constraint x ⊲⊳ c if ν(x) ⊲⊳ c. The satisfaction relation is extended to all guards g naturally, and denoted by ν |= g. We let Guards(X) denote the set of guards over X. We rely on the crucial notion of regions, as introduced in the seminal work on timed automata [2]: intuitively, a region is a set of valuations that are all time-abstract bisimilar. We will need some refinement of regions, with respect to a granularity 1/N , with N ∈ N. Formally, with respect to the set X of clocks and a constant M , a 1/N -region r is a subset of valuations characterised by the vector (ι x ) x∈X = (min(M N, ⌊ν(x)N ⌋)) x∈X ∈ [0, M N ] X and the order of fractional parts of ν(x)N , given as a partition X = X 0 ⊎ X 1 ⊎ · · · ⊎ X m of clocks: a valuation ν is in this 1/N -region r if (i) ⌊ν(x)N ⌋ = ι x , for all clocks x ∈ X; (ii) ν(x) = 0 for all x ∈ X 0 ; (iii) all clocks x ∈ X i satisfy that ν(x)N have the same fractional part, for all 1 i m. We denote by Reg N (X, M ) the set of 1/N -regions, and we write Reg(X, M ) as a shorthand for Reg 1 (X, M ). We recover the traditional notion of region for N = 1. E.g., the figure on the right depicts regions Reg({x, y}, 2) as well as their refinement Reg 3 ({x, y}, 2). For any integer guard g, either all valuations of a given 1/N -region satisfy g, or none of them do. A 1/N -region r ′ is said to be a time successor of the 1/N -region r if there exist ν ∈ r, ν ′ ∈ r ′ , and d > 0 such that ν ′ = ν + d. Moreover, for Y ⊆ X, we let r[Y := 0] be the 1/N -region where clocks of Y are reset. On the left, a weighted timed game. Locations belonging to Min (resp. Max) are depicted by circles (resp. squares). The target location is ℓ3, whose output weight function is null. It is easy to observe that location ℓ1 (resp. ℓ5) has value +∞ (resp. −∞). As a consequence, the value in ℓ4 is determined by the edge to ℓ3, and depicted in blue on the right. In location ℓ2, the value associated with the transition to ℓ3 is depicted in red, and the value in ℓ2 is obtained as the minimum of these two curves. Observe the intersection in x = 2/3 requiring to refine the regions.
Weighted timed games. A weighted timed game (WTG) is then a tuple G = L = L Min ⊎ L Max , ∆, wt, L T , wt T where L Min and L Max are finite disjoint subsets of locations belonging to Min and Max, respectively, ∆ ⊆ L × Guards(X) × 2 X × L is a finite set of transitions, wt : ∆ ⊎ L → Z is the weight function, associating an integer weight with each transition and location, L T ⊆ L Min is a subset of target locations for player Min, and wt T : L T × R X 0 → R ∞ is a function mapping each target location and valuation of the clocks to a final weight of R ∞ = R ⊎ {−∞, +∞} (possibly 0, +∞, or −∞). The addition of target weights is not standard, but we will use it in the process of solving those games: anyway, it is possible to simply map each target location to the weight 0, allowing us to recover the standard definition. Without loss of generality, we suppose the absence of deadlocks except on target locations, i.e. for each location ℓ ∈ L\L T and valuation ν, there exists (ℓ, g, Y, ℓ ′ ) ∈ ∆ such that ν |= g, and no transitions start in L T .
The semantics of a WTG G is defined in terms of a game played on an infinite transition system whose vertices are configurations of the WTG. A configuration is a pair (ℓ, ν) with a location and a valuation of the clocks. Configurations are split into players according to the location. A configuration is final if its location is a target location of L T . The alphabet of the transition system is given by R 0 × ∆ and will encode the delay that a player wants to spend in the current location, before firing a certain transition. For every delay d ∈ R 0 , transition δ = (ℓ, g, Y, ℓ ′ ) ∈ ∆ and valuation ν, there is an edge (ℓ, ν) d,δ − − → (ℓ ′ , ν ′ ) if ν + d |= g and ν ′ = (ν + d)[Y := 0]. The weight of such an edge e is given by d × wt(ℓ) + wt(δ). An example is depicted on Figure 1.
A finite play is a finite sequence of consecutive edges ρ = (ℓ 0 , ν 0 ) − −− → · · · (ℓ k , ν k ). We denote by |ρ| the length k of ρ. The concatenation of two finite plays ρ 1 and ρ 2 , such that ρ 1 ends in the same configuration as ρ 2 starts, is denoted by ρ 1 ρ 2 . We let FPlays G be the set of all finite plays in G, whereas FPlays Min G (resp. FPlays Max G ) denote the finite plays that end in a configuration of Min (resp. Max). A play is then a maximal sequence of consecutive edges (it is either infinite or it reaches L T ).
A strategy for Min (resp. Max) is a mapping σ : FPlays Min A strategy σ is memoryless if for all finite plays ρ, ρ ′ ending in the same configuration, we have that σ(ρ) = σ(ρ ′ ). For all strategies σ Min and σ Max of players Min and Max, respectively, and for all configurations (ℓ 0 , ν 0 ), we let play G ((ℓ 0 , ν 0 ), σ Max , σ Min ) be the outcome of σ Max and σ Min , defined as the only play conforming to σ Max and σ Min and starting in (ℓ 0 , ν 0 ).
The objective of Min is to reach a target configuration, while minimising the accumulated weight up to the target. Hence, we associate to every finite play ρ = (ℓ 0 , ν 0 ) − −− → · · · (ℓ k , ν k ) its cumulated weight, taking into account both discrete and continuous costs: Then, the weight of a play ρ, denoted by wt G (ρ), is defined by +∞ if ρ is infinite (does not reach L T ), and wt Σ (ρ) + wt T (ℓ T , ν) if it ends in (ℓ T , ν) with ℓ T ∈ L T . Then, for all locations ℓ and valuation ν, we let Val G (ℓ, ν) be the value of G in (ℓ, ν), defined as Val G ((ℓ, ν)) = inf σ Min sup σ Max wt G (play((ℓ, ν), σ Max , σ Min )), where the order of the infimum and supremum does not matter, since WTGs are known to be determined 1 . We say that a strategy σ ⋆ Min of Min is ε-optimal if, for all (ℓ, ν), and all strategies σ Max of Max, wt G (play((ℓ, ν), σ Max , σ ⋆ Min )) Val G (ℓ, ν) + ε. It is said optimal if this holds for ε = 0. A symmetric definition holds for optimal strategies of Max. If the game is clear from the context, we may drop the index G from all previous notations.
As usual in related work [1,9,10], we assume that the input WTGs have guards where all constants are integers, and all clocks are bounded, i.e. there is a constant M ∈ N such that every transition of the WTG is equipped with a guard g such that ν |= g implies ν(x) M for all clocks x ∈ X. We denote by w L max (resp. w ∆ max , w e max ) the maximal weight in absolute values of locations (resp. of transitions, edges) of . We also assume that the output weight functions are piecewise linear with a finite number of pieces and are continuous on each region. Notice that the zero output weight function satisfies this property. Moreover, the computations we will perform in the following maintain this property as an invariant, and use it to prove their correctness.
Region and corner abstractions. The region automaton, or region game, R N (G) (abbreviated as R(G) when N = 1) of a game G = L = L Min ⊎ L Max , ∆, wt, L T , wt T is the WTG with locations S = L × Reg N (X, M ) and all transitions ((ℓ, r), g ′′ , Y, (ℓ ′ , r ′ )) with (ℓ, g, Y, ℓ ′ ) ∈ ∆ such that the model of guard g ′′ (i.e. all valuations ν such that ν |= g ′′ ) is a 1/N -region r ′′ , time successor of r such that r ′′ satisfies the guard g, and r ′ = r ′′ [Y := 0]. Distribution of locations to players, final locations and weights are taken according to G. We call path a finite or infinite sequence of transitions in this automaton, and we denote by π the paths. A play ρ in G is projected on a path π in R N (G), by replacing every edge (ℓ, ν) where r (resp. r ′ ) is the 1/N -region containing ν (resp. ν ′ ): we say that ρ follows the path π. It is important to notice that, even if π is a cycle (i.e. starts and ends in the same location of the region game), there may exist plays following it in G that are not cycles, due to the fact that regions are sets of valuations. By projecting away the region information of R N (G), we simply obtain: On top of regions, we will need the corner-point abstraction techniques introduced in [8]. A valuation v is said to be a corner of a 1/N -region r, if it belongs to the topological closure r and has coordinates multiple of 1/N (v ∈ (1/N )N X ). We call corner state a triple (ℓ, r, v) that contains information about a location (ℓ, r) of the region-game R N (G), and a corner v of the 1/N -region r. Every region has at most |X| + 1 corners. We now define the corner-point abstraction C N (G) of a WTG G as the WTG obtained as a refinement of R N (G) where guards on transitions are enforced to stay on one of the corners of the current 1/N -region: the locations of C N (G) are all corner states of R N (G), associated to each player accordingly, and transitions are all ((ℓ, r, v), g ′′ , Y, (ℓ ′ , r ′ , v ′ )) such that there exists t = ((ℓ, r), g, Y, (ℓ ′ , r ′ )) a transition of R N (G) such that the model of guard g ′′ is a corner v ′′ satisfying the guard g (recall that g is the closed version of g), v ′ = v ′′ [Y := 0], and there exist two valuations ν ∈ r, ν ′ ∈ r ′ such that ((ℓ, r), ν) the latter condition ensures that the transition between corners is not spurious). Because of this closure operation, we must also define properly the final weight function: we simply define it over the only valuation v reachable in location (ℓ, r, v) (with ℓ ∈ L T ) by wt T ((ℓ, r, v), v) = lim ν→v,ν∈r wt T (ℓ, ν) (the limit is well defined since wt T is piecewise linear with a finite number of pieces on region r).
The WTG C N (G) can be seen as a weighted game (with final weights), i.e. a WTG without clocks (which means that there are only weights on transitions), by removing guards, resets and rates of locations, and replacing the weights of transitions by the actual weight of jumping from one corner to another: a transition (((ℓ, r), v), g ′′ , Y, ((ℓ ′ , r ′ ), v ′ )) becomes an edge from ((ℓ, r), v) to ((ℓ ′ , r ′ ), v ′ ) with weight d × wt(ℓ) + wt(t) (for all possible values of d, which requires to allow for multi-edges 2 ). Note that delay d is necessarily a rational of the form α/N with α ∈ N, since it must relate corners of 1/N -regions. In particular, this proves that the cumulated weight wt Σ (ρ) of a finite play ρ in C N (G) is indeed a rational number with denominator N .
We will call corner play a play ρ in the corner-point abstraction C N (G): it can also be interpreted as a timed execution in G where all guards are closed (as explained in the definition above). It straightforwardly projects on a finite path π in the region game R N (G): in this case, we say again that ρ follows π. Figure 2 depicts a play, its projected path in the region game and one of its associated corner plays.

Fig. 2.
A play ρ (in blue), its projected path π in the region game (in red), and one of its associated corner plays ρ ′ (in green) Corner plays allow one to obtain faithful information on the plays that follow the same path: If π is a finite path in R N (G), the set {wt Σ (ρ) | ρ finite play following π} is an interval bounded by the minimum and the maximum values of the set {wt Σ (ρ) | ρ finite corner play of C N (G) following π}.
Value iteration. We will rely on the value iteration algorithm described in [1] for a WTG G.
If V represents a value function-i.e. a mapping from configurations of L × R X 0 to a value in R ∞ -we denote by V ℓ,ν the image V (ℓ, ν), for better readability, and by V ℓ the function mapping each valuation ν to V ℓ,ν . One step of the game is summarised in the following operator F mapping each value function V to a value function ranges over valid edges in G. Then, starting from V 0 mapping every configuration to +∞, except for the targets mapped to wt T , we let V i = F (V i−1 ) for all i > 0. The value function V i represents the value Val i G , which is intuitively what Min can guarantee when forced to reach the target in at most i steps.
More formally, we define wt i G (ρ) the weight of a maximal play ρ at horizon i, as wt G (ρ) if ρ reaches a target state in at most i steps, and +∞ otherwise. Using this alternative definition of the weight of a play, we can obtain a new game value The mappings V 0 ℓ are piecewise linear for all ℓ, and F preserves piecewise linearity over regions, so all iterates V i ℓ are piecewise linear with a finite number of pieces. In [1], it is proved that V i ℓ has a number of pieces (and can be computed within a complexity) exponential in i and in the size of G when wt T = 0. This result can be extended to handle negative weights in G and output weights wt T = 0.

Results
We consider the value problem that asks, given a WTG G, a location ℓ and a threshold α ∈ Z∪{−∞, +∞}, to decide whether Val G (ℓ, 0) α. In the context of timed games, optimal strategies may not exist. We generally focus on finding ε-optimal strategies, that guarantee the optimal value, up to a small error ε. Moreover, when the value problem is undecidable, we also consider the approximation problem that consists, given a precision ε ∈ Q >0 , in computing an ε-approximation of Val G (ℓ, 0). In the one-player case, computing the optimal value and an ε-optimal strategy for weighted timed automata is known to be PSPACE-complete [6]. In the two-player case, the value problem of WTGs (also called priced timed games in the literature) is undecidable with 3 clocks [12,10], or even 2 clocks in the presence of negative weights [15] (for the existence problem asking if a strategy of player Min can guarantee a given threshold). To obtain decidability, one possibility is to limit the number of clocks to 1: then, there is an exponential-time algorithm to compute the value as well as ε-optimal strategies in the presence of non-negative weights only [7,20,17], whereas the problem is only known to be PTIME-hard. A similar result can be lifted to arbitrary weights, under restrictions on the resets of the clock in cycles [13].
The other possibility to obtain a decidability result [9,16] is to enforce a semantical property of divergence (originally called strictly non-Zeno cost): it asks that every play following a cycle in the region automaton has weight far from 0. It allows the authors to prove that playing for only a bounded number of steps is equivalent to the original game, which boils down to the problem of computing the value of a tree-shaped weighted timed game G using the value iteration algorithm.
Other objectives, not directly related to optimal reachability, have been considered in [11] for weighted timed games, like mean-payoff and parity objectives. In this work, the authors manage to solve these problems for the so-called class of δ-robust WTGs that they introduce. This class includes the class we consider, but is decidable in 2-EXPSPACE.
In [16], we generalised the strictly non-Zeno cost property of [9,16] to weighted timed games with both positive and negative weights: we called them divergent weighted timed games. This article relaxes the divergence property, to introduce almost-divergent weighted timed games. We first define formally these classes of games. A cycle π of R(G) is said to be a positive cycle (resp. a 0-cycle, or a negative cycle) if every finite play ρ following π satisfies wt Σ (ρ) 1 (resp. wt Σ (ρ) = 0, or wt Σ (ρ) −1). A strongly connected component (SCC) S of R(G) is said to be positive (resp. negative) if every cycle π ∈ S is positive (resp. negative). An SCC S of R(G) is said to be non-negative (resp. non-positive) if every play ρ following a cycle in S satisfies either wt Σ (ρ) 1 or wt Σ (ρ) = 0 (resp. either wt Σ (ρ) −1 or wt Σ (ρ) = 0).

Definition 1.
A WTG G is divergent if every SCC of R(G) is either positive or negative. As a generalisation, a WTG G is almost-divergent when every SCC of R(G) is either non-negative or non-positive.
In [16], we showed that we can decide in 2-EXPTIME the value problem for divergent WTGs. Unfortunately, it is shown in [10] that this problem is undecidable for almost-divergent WTGs (already with non-negative weights only, where almost-divergent WTGs are called simple). They propose a solution to the approximation problem, again with non-negative weights only. Our first result is the following extension of their result: Theorem 1. Given an almost-divergent WTG G, a location ℓ and ε ∈ Q >0 , we can compute an ε-approximation of Val G (ℓ, 0) in time doubly-exponential in the size of G and polynomial in 1/ε.

Moreover, deciding if a WTG is almost-divergent is PSPACE-complete.
To obtain this result, we follow an approximation schema that we now outline. First, we will always reason on the region game R(G) of the almost-divergent WTG G. The goal is to compute an ε-approximation of Val R(G) (s 0 , 0) for some state s 0 = (ℓ 0 , r 0 ), with r 0 the region where every clock value is 0. As already recalled, techniques of [1] allow one to compute the (exact) values of a WTG played on a finite tree, using operator F . The idea is thus to decompose as much as possible the game R(G) in a WTG over a tree. First, we decompose the region game into SCCs (left of Figure 3).
During the approximation process, we must think about the final weight functions as the previously computed approximations of the values of SCCs below the current one. We will keep as an invariant that final weight functions are piecewise linear functions with a finite number of pieces, and are continuous on each region.
For an SCC of R(G) and an initial state s 0 of R(G) provided by the SCC decomposition, we show that the game on the SCC is equivalent to a game on a tree built from a semi-unfolding (see middle of Figure 3) of R(G) from s 0 of finite depth, with certain nodes of the tree being kernels. These kernels are some parts of R(G) that contain all cycles of weight 0. The semi-unfolding is stopped either when reaching a final location, or when some location (or kernel) has been visited for a certain fixed number of times: such locations deep enough are called stop leaves.
Our second result is a more symbolic approximation schema based on the value iteration only. It is more symbolic in the sense that it does not require the SCC decomposition, the computation of kernels nor the semi-unfolding of the game in a tree.
Then the sequence (Val k G ) k 0 converges towards Val G and for every ε ∈ Q >0 , we can compute an integer P such that Val P G is an ε-approximation of Val G for all configurations.
Remark 1. In a weighted-timed game, it is easy to detect the set of states with value +∞: these are all the states from which Min cannot ensure reachability of a target location ℓ ∈ L T with wt T (ℓ) < +∞. It can therefore be computed by an attractor computation, and is indeed a property constant on each region. In particular, removing those states from R(G) does not affect the value of any other state and can be done in complexity linear in |R(G)|. We will therefore assume that the considered WTG have no configurations with value +∞.

Kernels of an almost-divergent WTG
The approximation procedure described before uses the so-called kernels in order to group together all cycles of weight 0. We study those kernels and give a characterisation allowing computability. Contrary to the non-negative case, the situation is more complex in our arbitrary case, since weights of both locations and transitions may differ from 0 in the kernel. Moreover, it is not trivial (and may not be true in a non almost-divergent WTG) to know whether it is sufficient to consider only simple cycles, i.e. cycles without repetitions.
To answer these questions, let us first analyse the cycles of R(G) that we will encounter. Since we are in an almost-divergent game, by Lemma 2, all cycles π = t 1 · · · t n of R(G) (with t 1 , . . . , t n transitions of R(G)) are either 0-cycles, positive cycles or negative cycles. Additionally, in an SCC S of R(G), we cannot find both positive and negative cycles by definition. Moreover, we can classify a cycle by looking only at the corner plays following it.
Proof. If π is a 0-cycle, every such corner play ρ will have weight 0, by Lemma 2. Reciprocally, if such a corner play exists, all corner plays following π have weight 0: otherwise the set {wt Σ (ρ) | ρ play following π} would have non-empty intersection with the set (−1, 1) \ {0} which would contradict the almost-divergence.
An important result is that 0-cycles are stable by rotation. This is not trivial because plays following a cycle can start and end in different valuations, therefore changing the starting state of the cycle could a priori change the plays that follow it and their weights.
First, since there are finitely many corners, by constructing a long enough play following an iterate of π ′ π, we can obtain a corner play that starts and ends in the same corner. Formally, we define two sequences of region corners (v i ∈ first(π)) i and (v ′ i ∈ first(π ′ )) i . We start by choosing any v 0 ∈ first(π). Let v ′ 0 be a corner of first(π ′ ) such that v ′ 0 is accessible from v 0 by following π. For every i > 0, let v i be a corner of first(π) such that v i is accessible from v ′ i−1 by following π ′ , and let v ′ i be a corner of first(π ′ ) such that v ′ i is accessible from v i by following π. We stop the construction at the first l such that there exists This process is bounded since first(π) has at most |X| + 1 corners. For every 0 i l, let w i be the weight of a play ρ i from v i to v ′ i along π, and let w ′ i be the weight of a play ρ ′ i from v ′ i to v i+1 along π ′ . The concatenation of the two plays has weight w i + w ′ i = 0, since it follows the 0-cycle π 1 . Therefore, all corner plays from v i to v ′ i following π have the same weight w i , and the same applies for w ′ i . For every 0 i < l, the concatenation of Since π 2 is a cycle, and the game is almost-divergent, all possible values of w i+1 − w i have the same sign.
Finally, we can construct a corner play This implies that the terms w i+1 − w i , of constant sign, are all equal to 0. As a consequence, the concatenation of ρ ′ k and ρ k+1 is a corner play following π 2 of weight 0. By Lemma 3, we deduce that π 2 is a 0-cycle.
We will now construct the kernel K as the subgraph of R(G) containing all 0-cycles. Formally, let T K be the set of transitions of R(G) belonging to a simple 0-cycle, and S K be the set of states covered by T K . We define the kernel K of R(G) as the subgraph of R(G) defined by S K and T K . Transitions in T \T K with starting state in S K are called the output transitions of K. We define it using only simple 0-cycles in order to ensure its computability. However, we now show that this is of no harm, since the kernel contains exactly all the 0-cycles, which will be crucial in the approximation schema we present in Section 6.

Proposition 1. A cycle of R(G) is entirely in K if and only if it is a 0-cycle.
Proof. We prove that every 0-cycle is in K by induction on the length of the cycles. The initialisation contains only cycles of length 1, that are in K by construction. If we consider a cycle π of length n > 1, it is either simple or it can be rotated and decomposed into π ′ π ′′ , π ′ and π ′′ being smaller cycles. Let ρ be a corner play following π ′ π ′′ . We denote by ρ ′ the prefix of ρ following π ′ and ρ ′′ the suffix following π ′′ . It holds that wt Σ (ρ ′ ) = −wt Σ (ρ ′′ ), and in an almost-divergent SCC this implies wt Σ (ρ ′ ) = wt Σ (ρ ′′ ) = 0. Therefore, by Lemma 3 both π ′ and π ′′ are 0-cycles, and they must be in K by induction hypothesis. Note that this reasoning proves that every cycle contained in a longer 0-cycle is also a 0-cycle.
We now prove that every cycle in K is a 0-cycle. By construction, every transition t ∈ T K is part of a simple 0-cycle. Thus, to every transition t ∈ T K , we can associate a path π t such that tπ t is a simple 0-cycle (rotate the simple cycle if necessary). We can prove (using both Lemmas 3 and 4) the following property by relying on another pumping argument on corners: If t 1 · · · t n is a path in K, then t 1 t 2 · · · t n π tn · · · π t2 π t1 is a 0-cycle of R(G). Now, if π is a cycle of R(G) in K, there exists a cycle π ′ such that ππ ′ is a 0-cycle, therefore π is a 0-cycle.

Semi-unfolding of almost-divergent WTGs
Given an almost-divergent WTG G, we describe the construction of its semi-unfolding T (G) (as depicted in Fig. 3). This crucially relies on the absence of states with value −∞, so we explain how to deal with them first:

Lemma 5. In an SCC of R(G), the set of configurations with value −∞ is a union of regions computable in time linear in the size of R(G).
Proof (Sketch of proof). If the SCC is non-negative, the cumulated weight cannot decrease along a cycle, thus, the only way to obtain value −∞ is to jump in a final state with final weight −∞. We can therefore compute this set of states with an attractor for Min.
If the SCC is non-positive, we let S R f (resp. S −∞ f ) be the set of target states where wt T is bounded (resp. has value −∞). We also define T R f (resp. T −∞ f ), the set of transitions of R(G) whose end state belongs to S R f (resp. S −∞ f ). Notice that the kernel cannot contain target states since they do not have outgoing transitions. We can prove that a configuration has value −∞ iff it belongs to a state where player Min can ensure the LTL formula on transitions: . The procedure to detect −∞ states thus consists of four attractor computations, which can be done in time linear in |R(G)|.
We can now assume that no states of G have value −∞, and that the output weight function maps all configurations to R. Since wt T is piecewise linear with finitely many pieces, wt T is bounded. Let sup |wt T | denote the bound of |wt T |, ranging over all target configurations.
We now explain how to build the semi-unfolding T (G). We only build the semi-unfolding T (G) of an SCC of G starting from some state (ℓ 0 , r 0 ) ∈ S of the region game, since it is then easy to glue all the semi-unfoldings together to get the one of the full game. Since every configuration has finite value, we can prove that values of the game are bounded by |R(G)|w e max + sup |wt T |. As a consequence, we can find a bound γ linear in |R(G)|, w e max and sup |wt T | such that a play that visits some state outside the kernel more than γ times has weight strictly above |R(G)|w e max + sup |wt T |, hence is useless for the value computation. This leads to considering the semi-unfolding T (G) of G (nodes in the kernel are not unfolded, see Figure 3) such that each node not in the kernel is encountered at most γ times along a branch: the end of each branch is called a stop leaf of the semi-unfolding. In particular, the depth of T (G) is bounded by |R(G)|γ, and thus is polynomial in |R(G)|, w e max and sup |wt T |. Leaves of the semi-unfolding are thus of two types: target leaves that are copies of target locations of G for which we set the target weight as in G, and stop leaves for which we set their target weight as being constant to +∞ if the SCC G is non-negative, and −∞ if the SCC is non-positive.

Approximation of almost-divergent WTGs
Approximation of kernels. We start by approximating a kernel G by extending the region-based approximation schema of [10]. In their setting, all runs in kernels had weight 0, allowing a simple reduction to a finite weighted game. In our setting, we have to approximate the timed dynamics of runs, and therefore resort to the corner-point abstraction (as shown to the right of Fig. 3).
Since output weight functions are piecewise linear with a finite number of pieces and continuous on regions, they are Λ-Lipschitz-continuous 3 , for a given constant Λ 0. We let B = w L max |L||Reg(X, M )| + Λ. Let N be an integer. Consider the game C N (G) described in the preliminary section, with locations of the form (ℓ, r, v) with v a corner of the 1/N -region r. Two plays ρ of G and ρ ′ of C N (G) are said to be 1/N -close if they follow the same path π in R N (G). In particular, at each step the configurations (ℓ, ν) in ρ and (ℓ ′ , r ′ , v ′ ) in ρ ′ (with v ′ a corner of the 1/N -region r ′ ) satisfy ℓ = ℓ ′ and ν ∈ r ′ , and the transitions taken in both plays have the same discrete weights. Close plays have close weights, in the following sense: , with ν 0 ∈ r 0 , since both players have the ability to stay 1/N -close all along the plays, a bisimulation argument permits to obtain that the values of the two games are also close in (ℓ 0 , ν 0 ) and ((ℓ 0 , r 0 , v 0 ), v 0 ): Using this result, picking N an integer larger than B/ε, we can thus obtain |Val Recall that C N (G) can be considered as an untimed weighted game (with reachability objective). Thus we can apply the result of [14], where it is shown that the optimal values of such games can be computed in pseudo-polynomial time (i.e. polynomial time with weights encoded in unary, instead of binary). We then define an ε-approximation of Val G , named Val ′ N , on each 1/N -region by interpolating the values of its 1/N -corners in C N (G) with a piecewise linear function: therefore, we can control the Lipschitz constant of the approximated value for further use.

Lemma 8. Val ′
N is an ε-approximation of Val G , that is piecewise linear with a finite number of pieces and 2B-Lipschitz-continuous over regions.
Approximation of almost-divergent WTGs. We now explain how to approximate the value of an almost-divergent WTG G, thus proving Theorem 1. First, we compute a semi-unfolding T (G) as described in the previous section. Then we perform a bottom-up computation of the approximation. As already recalled, techniques of [1] allow us to compute exact values of a tree-shape WTG. In consequence, we know how to compute the value of a non-kernel node of T (G), depending of the values of its children. There is no approximation needed here, so that if all children are εapproximation, we can compute an ε-approximation of the node. Therefore, the only approximation lies in the kernels, and we explained before how to compute arbitrarily close an approximation of a kernel's value. We crucially rely on the fact that the value function is 1-Lipschitz-continuous 4 . This entails that imprecisions will sum up along the bottom-up computations, as computing an ε-approximation of the value of a game whose output weights are ε ′ -approximations yields an (ε + ε ′ )-approximation. Therefore we compute approximations with threshold ε ′ = ε/α for kernels in T (G), where α is the maximal number of kernels along a branch of T (G): α is smaller than the depth of T (G), which is bounded by Proposition 2.
The subregion granularity considered before for kernel approximation crucially depends on the Lipschitz constant of output weights. The growth of these constants is bounded for kernels in T (G) by Lemma 8. For non-kernel nodes of T (G), using a careful analysis of the algorithm of [1], we obtain the following bound: Lemma 9. If all the output weights of a WTG G are Λ-Lipschitz-continuous over regions (and piecewise linear, with finitely many pieces), then Val i G is ΛΛ ′ -Lipschitz-continuous over regions, with Λ ′ polynomial in w L max and |X| and exponential in i. The overall time complexity of this method is doubly-exponential in the size of the input game and polynomial in 1/ε.

Symbolic approximation algorithm
The previous approximation result suffers from several drawbacks. It relies on the SCC decomposition of the region automaton. Each of these SCCs have to be analysed in a sequential way, and their analysis requires an a priori refinement of the granularity of regions. This approach is thus not easily amenable to implementation. We instead prove in this section that the symbolic approach based on the value iteration paradigm, i.e. the computation of iterates of the operator F recalled in page 6, is an approximation schema. This is stated in Theorem 2, for which we now sketch a proof in this section.
Notice that configurations with value +∞ are stable through value iteration, and do not affect its other computations. Since Theorem 2 assumes the absence of configurations of value −∞, we will therefore consider in the following that all configurations have finite value in G.
Consider first a game G that is a kernel. By the results of Section 6, there exists an integer N such that solving the untimed weighted game C N (G) computes an ε/2-approximation of the value of 1/N corners. Using the results of [14] for untimed weighted games, we know that those values are obtained after a finite number of steps of (the untimed version of) the value iteration operator. More precisely, if one considers a number of iterations P = |L||Reg N (X, M )|(|X| + 1)(2(|L||Reg N (X, M )|(|X| + 1) − 1)w e max + 1), then Val P CN (G) ((ℓ, r, v), v) = Val CN (G) ((ℓ, r, v), v). From this observation, we deduce the following property of P :

Lemma 10. If G is a kernel with no configurations of infinite value, then |Val
Proof. We already know that Val P CN (G) ((ℓ, r, v), v) = Val CN (G) ((ℓ, r, v), v) for all configurations ((ℓ, r, v), v) of C N (G). Moreover, Section 6 ensures |Val G (ℓ, ν)−Val CN (G) ((ℓ, r, v), v)| ε/2 whenever ν is in the 1/N -region r. Therefore, we only need to prove that |Val P G (ℓ, ν) − Val P CN (G) ((ℓ, r, v), v)| ε/2 to conclude. This is done as for Lemma 7, since Lemma 6 (that we need to prove Lemma 7) does not depend on the length of the plays ρ and ρ ′ , and both runs reach the target state in the same step, i.e. both before or after the horizon of P steps.
Once we know that value iteration converges on kernels, we can use the semi-unfolding of Section 5 to prove that it also converges on non-negative SCCs when all values are finite.

Lemma 11. If G is a non-negative SCC with no configurations of infinite value, we can compute
The idea is to unfold every kernel of the semi-unfolding game T (G) according to its bound in Lemma 10. More precisely, let α be the maximum number of kernels along one of the branches of T (G). In a bottom-up fashion, we can find for each kernel K in T (G) a bound P K such that, for all configurations (ℓ, ν), |Val K (ℓ, ν) − Val P K K (ℓ, ν)| ε/α. We thus unfold K in T (G) with depth up to P K . After each kernel has been replaced this way, T (G) is no longer a semi-unfolding, it is instead a (complete) unfolding of R(G), of a certain bounded depth P + . This new bound P + is bounded by the former depth of T (G) to which is added α times the biggest bound P K we need for the kernels. Now, T (G) is a tree of depth P + whose value at its root is ε-close to the value of G. Finally, the value computed by Val P+ G is bounded between Val G and Val T (G) , which allows us to conclude.
The bound P K for a kernel K depends linearly in Λ, the Lipschitz constant of value functions on locations of T (G) reachable from K. Once K has been replaced by its unfolding of depth P K , the Lipschitz constant of the value function at the root of T (G) are thus bounded exponentially in Λ. This means that we ensure a bound for P + that is at most polynomial in 1/ε, and that is of the order of a tower of α exponentials.
Proving the same property on non-positive SCCs requires more work, because the semiunfolding gives output weight −∞ to stop leaves, which doesn't integrate well with value iteration (initialisation at +∞ on non-target states). However, by unfolding those SCCs slightly more (at most |R(G)| more steps), we can obtain the desired property with a similar bound P − . for all configurations (ℓ, ν) of G. Now, if we are given an almost-divergent game G and a precision ε, we can add the bounds for value iteration obtained from each SCC by Lemmas 11 and 12, and obtain a final bound P such that for all k P , Val k G is an ε-approximation of Val G . Discussion. Overall, this leads to an upper bound complexity that is polynomial in 1/ε and of the order of a tower of n exponentials, with n polynomial in the size of the input WTG. However, we argue that this symbolic procedure is more amenable to implementation than the previous approximation schema. First, it avoids the three already mentioned drawbacks (SCC decomposition, sequential analysis of the SCCs, and refinement of the granularity of regions) of the previous approximation schema. Then, it allows one to directly launch the value iteration algorithm on the game G, and we can stop the computation whenever we are satisfied enough by the approximation computed: however, there are no guarantees whatsoever on the quality of the approximation before the number of steps P given above. Finally, this schema allows one to easily obtain an almost-optimal strategy with respect to the computed value.

Lemma 12. If G is a non-positive SCC with no configurations of infinite value, we can compute
If G is not guaranteed to be free of configurations of value −∞, then we must first perform the SCC decomposition of R(G), and, as G is almost-divergent, identify and remove regions whose value is −∞, by Lemma 5. Then, we can apply the value iteration algorithm.
As a final remark, notice that our correctness proof strongly relies on Section 6, and thus would not hold with the approximation schema of [10] (which does not preserve the continuity on regions of the computed value functions, in turn needed to define output weights on 1/N -corners).

Conclusion
We have given an approximation procedure for a large class of weighted timed games with unbounded number of clocks and arbitrary integer weights that can be executed in doubly-exponential time with respect to the size of the game. In addition, we proved the correctness of a symbolic approximation schema, that does not start by splitting exponentially every region, but only does so when necessary (as dictated by [1]). We argue that this paves the way towards an implementation of value approximation for weighted timed games.
Another perspective is to extend this work to the concurrent setting, where both players play simultaneously and the shortest delay is selected. We did not consider this setting in this work because concurrent WTGs are not determined, and several of our proofs rely on this property for symmetrical arguments (mainly to lift results of non-negative SCCs to non-positive ones). Another extension of this work is the exploration of the effect of almost-divergence in the case of multiple weight dimensions, and/or with mean-payoff objectives.

A Proofs of Section 2
Proof (Proof of Lemma 2). The set {wt Σ (ρ) | ρ finite play following π} is an interval as the image of a convex set by an linear function (see [6,Sec. 3.2] for an explanation). The good properties of the corner-point abstraction allows us to conclude, since for every play ρ following π, one can find a corner play following π of smaller weight and one of larger weight, and for every corner play ρ following π and every ε > 0, one can find a play following π whose weight is at most ε away from wt Σ (ρ) [8].

A.1 Undecidability of value −∞
We prove that given a WTG G (not necessarily almost-divergent) and an initial location ℓ 0 , it is undecidable whether Val G (ℓ 0 , 0) = −∞. We reduce it to the existence problem on turn-based WTG: given a WTG G (without output weight function), an integer threshold α and a starting location ℓ 0 , does there exist a strategy for Min that can guarantee reaching the unique target location ℓ t from ℓ 0 with weight < α. In the non-negative setting, it is proved in [7] that the problem is undecidable for the comparison α. In the negative setting, formal proofs are given for all comparison signs in [15].
Consider G ′ the WTG built from G by adding a transition from ℓ t to ℓ 0 , without guards and resetting all the clocks, of discrete weight −α. We add a new target location ℓ ′ t , and add transitions of weight 0 from ℓ t to ℓ ′ t . Location ℓ t is then given to Min. Let us prove that Val G ′ (ℓ 0 , 0) = −∞ if and only if Min has a strategy to guarantee a weight < α in G.
Assume first Val G ′ (ℓ 0 , 0) = −∞. If Val G (ℓ 0 , 0) = −∞, we are done. Otherwise, Min must follow in G ′ the new transition from ℓ t to ℓ 0 to enforce a cycle of negative value, and thus enforce a play from (ℓ 0 , 0) to ℓ t with weight less than α. Therefore, there exists a strategy for Min in G that can guarantee a weight < α.
Reciprocally, if there exists a strategy for Min that can guarantee a weight < α, then Min can force a negative cycle play and Val G ′ (ℓ 0 , 0) = −∞.

A.2 Decision of the almost-divergence of a WTG
First, we state that a WTG G is not almost-divergent if and only if R(G) contains an SCC with either both a positive play following one of its cycles and a negative play following one of its cycles, or a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles. We will now explain how we can test both of those properties (and thus if a game is not almost-divergent) in PSPACE.
A corner play following a cycle of the region game is said to be simple if it does not visit the same corner twice (but the first and last corners can be the same). A simple corner play following a cycle has length bounded by |S| × (|X| + 1). By Lemma 2, R(G) contains an SCC with either both a positive play following one of its cycles and a negative play following one of its cycles if and only if R(G) contains both a positive corner play following one of its cycles and a negative corner play following one of its cycles. We will extend this to simple corner plays.

Lemma 13. R(G) contains an SCC with either both a positive play following one of its cycles and a negative play following one of its cycles if and only if R(G) contains an SCC with both a positive simple corner play following one of its cycles and a negative simple corner play following one of its cycles.
Proof. All that is left to prove is that, in an SCC of R(G), if all simple corner plays following a cycle have non-negative weight (resp. non-positive weight), then all corner plays following a cycle have non-negative weight (resp. non-positive weight).
By contradiction, we consider ρ, the shortest corner play following a cycle π, such that wt Σ (ρ) < 0 (resp. wt Σ (ρ) > 0). Corner play ρ cannot be simple, so it must contain a simple loop. That loop is a simple corner play following a cycle of R(G), so it must have non-negative weight (resp. nonpositive weight). This means that ρ without that loop satisfies wt Σ (ρ) < 0 (resp. wt Σ (ρ) > 0), and therefore was not the shortest corner play with the desired property.
We can test the existence of such simple corner plays in a SCC of R(G) in NPSPACE, by guessing them corner after corner and by keeping the cumulated weight in memory. The check that both plays are in the same SCC is a reachability check in a timed automaton, which can be done in PSPACE. We described a similar procedure in [16] where we were testing the existence of a non-negative corner play and a non-positive one in the same SCC instead of a negative one and a positive one. Now, we will assume in this second part that this test failed, so every SCC of R(G) either satisfies that all plays following a cycle have non-negative weight or satisfies that they all have non-positive weight. We will now explain how to check if R(G) contains a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles. Let B = (|S| × (|X| + 1)) 2 . Lemma 14. R(G) contains a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles if and only if R(G) contains a cycle π of length at most B such that there is a corner play following π with weight zero and another one with non-zero weight.
Proof. By Lemma 2, R(G) contains a play with weight in (−1, 0) ∪ (0, 1) following one of its cycles if and only if that cycle satisfies that there is a corner play following it with weight zero and another one with non-zero weight.
We only need to show that if there are no such cycles of length at most B, then there are no such cycles of any length. Therefore, we assume that no cycle of length less than B allows a play with weight in (−1, 0) ∪ (0, 1). By contradiction, let π be the shortest cycle such that there exist two corner plays ρ and ρ ′ following π, with wt Σ (ρ) = 0 and wt Σ (ρ ′ ) = 0. Then |π| > B. Let v i be the i-th corner of ρ, and v ′ i be the i-th corner of ρ ′ . There are at most (|S| × (|X| + 1)) 2 different pairs (v i , v ′ i ), which implies that there must be two indexes, j and k, such that (v j , v ′ j ) = (v k , v ′ k ) and j < k. The portion of ρ between indexes j and k follows a cycle, and have opposite weight to the play constructed by considering ρ and removing the loop between indexes j and k. Since the sum of their weight is 0 and they both follow cycles of R(G) in the same SCC, both of those plays have weight 0. The portion of π between indexes j and k is a cycle shorter than π, and it contains a corner play of weight 0, therefore all of its corner plays have weight 0, and the portion of ρ ′ between indexes j and k has weight 0 too. But then the cycle defined by taking π and removing the loop between indexes j and k contains a corner play of weight 0 (derived from ρ), and a corner play of weight non-zero (derived from ρ ′ ), and that contradicts π being the shortest cycle with that property.
Once again, we can check the existence of such a cycle of length bounded by B in NPSPACE by guessing it and its two relevant corner plays on-the-fly and storing the cumulated weight of each. This imply that deciding if a game G is almost divergent is decidable in coNPSPACE = NPSPACE = PSPACE (using the theorems of Immerman-Szelepcsényi [18,22] and Savitch [21]).
Let us now show the PSPACE-hardness (indeed the coPSPACE, which is identical) by a reduction from the reachability problem in a timed automaton. We consider a timed automaton with a starting state and a different target state without outgoing transitions. We construct from it a weighted timed game by distributing all states to Min, and equipping all transitions with weight 0, and all states with weight 0. We also add a loop with weight 1 on the initial state, one with weight −1 on the target state, and a transition from the target state to the initial state with weight 0, all three resetting all clocks and with no guard. Then, the weighted timed game is not almost-divergent if and only if the target can be reached from the initial state in the timed automaton.
Proof. We prove the property by induction on n. For n = 1, the property is immediate since t 1 π t1 is a 0-cycle. Consider then n such that the property holds for n, and prove it for n + 1. We will exhibit two corner plays following t 1 · · · t n+1 π tn+1 · · · π t1 of opposite weight and conclude with Lemma 3.
Let v 0 be a corner of last(t n+1 ). Since t n+1 π tn+1 is a 0-cycle, there exists w ∈ Z, a corner play ρ 0 following t n+1 ending in v 0 with weight w and a corner play ρ ′ 0 following π tn+1 beginning in v 0 with weight −w. We name v ′ 0 the corner of last(t n ) where ends ρ ′ 0 . We consider any corner play ρ 1 following t n+1 from corner v ′ 0 . The corner play ρ ′ 0 ρ 1 follows the path π tn+1 t n+1 that is also a 0-cycle by Lemma 4, therefore ρ 1 has weight w. We denote by v 1 the corner where ends ρ 1 . By iterating this construction, we obtain some corner plays ρ 0 , ρ 1 , ρ 2 , . . . following t n+1 and ρ ′ 0 , ρ ′ 1 , ρ ′ 2 , . . . following π tn+1 such that ρ ′ i goes from corner v i to v ′ i , and ρ i+1 from corner v ′ i to v i+1 , for all i 0. Moreover, all corner plays ρ i have weight w and all corner plays ρ ′ i have weight −w. Consider the first index l such that v l = v k for some k < l, which exists because the number of corners is finite.
We apply the induction to find a corner play following t 1 · · · t n π tn · · · π t1 , going through the corner v ′ k in the middle: more formally, there exists w α , a corner play ρ α following t 1 · · · t n ending in v ′ k with weight w α and a corner play ρ ′ α following π tn · · · π t1 beginning in v ′ k with weight −w α . We apply the induction a second time with corner v ′ l−1 : there exists w β , a corner play ρ β following t 1 · · · t n ending in v ′ l−1 with weight w β and a corner play ρ ′ β following π tn · · · π t1 beginning in v ′ follows the cycle t 1 · · · t n t n+1 π tn+1 π tn · · · π t1 . Since the game is almost-divergent, and those two corner plays are in the same SCC, both have weight 0. The second corner play of weight 0 ensures that the cycle t 1 · · · t n+1 π tn+1 · · · π t1 is a 0-cycle, by Lemma 3.

C Proofs of the semi-unfolding (Section 5)
Proof (Proof of Lemma 5). We detail the case of non-negative SCCs. Let us prove that a configurations has value −∞ if and only if it belongs to a state where player Min can ensure the LTL formula on transitions: , then from s, Max must be able to avoid S −∞ f , and eventually enforce either S R f reachability or staying in K forever. In both cases, Max can ensure a value above −∞.

C.1 Semi-unfolding construction
In order to prove Proposition 2, we will construct the desired semi-unfolding T (G) of a (nonnegative or non-positive SCC) G.
If (ℓ, r) is in K, we let K ℓ,r be the part of K accessible from (ℓ, r) (note that K ℓ,r is an SCC as K is a disjoint set of SCCs). We define the output transitions of K ℓ,r as being the output transitions of K accessible from (ℓ, r). If (ℓ, r) is not in K, the output transitions of (ℓ, r) are the transitions of R(G) starting in (ℓ, r).
Formally, we define a tree T whose nodes will either be labelled by region graph states (ℓ, r) ∈ S\S K or by kernels K ℓ,r , and whose edges will be labelled by output transitions in R(G). The root of the tree T is labelled with (ℓ 0 , r 0 ), or K ℓ0,r0 (if (ℓ 0 , r 0 ) belongs to the kernel), and the successors of a node of T are then recursively defined by its output transitions. When a state (ℓ, r) is reached by an output transition, the child is labelled by K ℓ,r if (ℓ, r) ∈ K, otherwise it is labelled by (ℓ, r). Edges in T are labelled by the transitions used to create them. Along every branch, we stop the construction when either a final state is reached (i.e. a state not inside the current SCC) or the branch contains 3|R(G)|w e max + 2 sup |wt T | + 2 nodes labelled by the same state ((ℓ, r) or K ℓ,r ). Since R(G) has a finite number of states, T is finite. Leaves of T with a location belonging to L T are called target leaves, others are called stopped leaves.
We now transform T into a WTG T (G), by replacing every node labelled by a state (ℓ, r) by a different copy (l, r) of (ℓ, r). Those states are said to inherit from (ℓ, r). Edges of T are replaced by the transitions labelling them, and have a similar notion of inheritance. Every non-leaf node labelled by a kernel K ℓ,r is replaced by a copy of the WTG K ℓ,r , output transitions being plugged in the expected way. We deal with stopped leaves labelled by a kernel K ℓ,r by replacing them with a single node copy of (ℓ, r), like we dealt with node labelled by a state (ℓ, r). State partition between players and weights are inherited from the copied states of R(G). The only initial state of T (G) is the state denoted by (l 0 , r 0 ) inherited from (ℓ 0 , r 0 ) in the root of T (either (ℓ 0 , r 0 ) or K ℓ0,r0 ). The final states of T (G) are the states derived from leaves of T . If R(G) is a non-negative (resp. non-positive) SCC, the output weight function wt T is inherited from R(G) on target leaves and set to +∞ (resp. −∞) on stopped leaves.

C.2 Semi-unfolding correctness
We will now prove that Proposition 2 holds on this T (G).

Lemma 16. All finite plays in R(G) have cumulated weight (ignoring output weights) at least −|R(G)|w e
max in the non-negative case, and at most |R(G)|w e max in the non-positive case. Moreover, values of the game are bounded by |R(G)|w e max + sup |wt T |. Proof. Suppose first that R(G) is a non-negative SCC. Consider a play ρ following a path π. π can be decomposed into π = π 1 π c 1 · · · π n π c n such that every π c i is a cycle, and π 1 . . . π n is a simple path in R(G) (thus Proof. Note that by construction, all finite paths in T (G) from the initial state to a stopped leaf can be decomposed as π ′ π 1 · · · π 3|R(G)|w e max +2 sup |wtT |+1 with all π i being cycles. Additionally, those cycles cannot be 0-cycles by Proposition 1, since they take at least one transition outside of K. Therefore the restriction of ρ to π 1 · · · π 3|R(G)|w e max +1 has weight at least 3|R(G)|w e max + 2 sup |wt T | + 1 (in the non-negative case) and at most −3|R(G)|w e max − 2 sup |wt T | − 1 (in the nonpositive case). The beginning of the play, following π ′ , has cumulated weight at least −|R(G)|w e max (in the non-negative case) and at most |R(G)|w e max (in the non-positive case), by Lemma 16.
Two plays ρ = ((ℓ 1 , r 1 ), ν 1 ) and T (G), respectively, are said to mimic each other if every (l i , r i ) is inherited from (ℓ i , r i ) and every transitiont i is inherited from the transition δ i . Combining Lemmas 17 and 16, we obtain Lemma 18. If R(G) is a non-negative (resp. non-positive) SCC, every play from the initial state and with cumulated weight less than |R(G)|w e max +2 sup |wt T |+1 (resp. greater than −|R(G)|w e max − 2 sup |wt T | − 1) can be mimicked in T (G) without reaching a stopped leaf. Conversely, every play in T (G) reaching a target leaf can be mimicked in R(G).
Proof. We prove only the non-negative case. Let ρ be a play of R(G) with cumulated weight less than |R(G)|w e max + 2 sup |wt T | + 1. Consider the branch of the unfolded game it follows. If ρ cannot be mimicked in T (G), then a prefix of ρ reaches the stopped leaf of that branch when mimicked in T (G). In this situation, ρ starts by a prefix of weight at least 2|R(G)|w e max + 2 sup |wt T | + 1 by Lemma 17 and then ends with a suffix play of weight at least −|R(G)|w e max by Lemma 16, and that contradicts the initial assumption. The non-positive case is proved exactly the same way, and the converse is true by construction.
Then, the plays of R(G) starting in an initial configuration that cannot be mimicked in T (G) are not useful for value computation, which is formalised by Proposition 3: Proof. By Lemma 1, we already know that Val G (ℓ 0 , ν 0 ) = Val R(G) ((ℓ 0 , r 0 ), ν 0 ). Recall that we only left finite values in R(G) (in the final weight functions, in particular), and more precisely |Val R(G) ((ℓ 0 , r 0 ), ν 0 )| |R(G)|w e max + sup |wt T | by Lemma 16. We first show that the value is also finite in T (G). Indeed, if Val T (G) ((l 0 , r 0 ), ν 0 ) = +∞, since we assumed all output weights of R(G) bounded, we are necessarily in the non-negative case, and Max is able to ensure stopped leaves reachability. ((l 0 , r 0 ), ν 0 ) = +∞, then there are no winning strategies in R(G) for Min ensuring weight less than |R(G)|w e max + sup |wt T | + 1 from (ℓ 0 , r 0 ). Thus, we can obtain the contradiction Val R(G) ((ℓ 0 , r 0 ), ν 0 ) > |R(G)|w e max + sup |wt T |. Proof (Proof of Claim 1). By contradiction, consider a strategy σ Min of Min ensuring weight A |R(G)|w e max + sup |wt T | + 1 in R(G). Then, for all σ Max , the cumulated weight of play R(G) (((l 0 , r 0 ), ν 0 ), σ Min , σ Max ) (reaching target configuration (ℓ, ν)) is at most A − wt T (ℓ, ν) |R(G)|w e max + 2 sup |wt T | + 1, and by Lemma 18 this play does not reach a stopped leaf when mimicked in T (G), which is absurd.

Claim 2.If Val T (G)
Then, strategies and plays of T (G) starting from (l 0 , r 0 ) can be mimicked in R(G), therefore Val R(G) ((ℓ 0 , r 0 ), ν 0 ) Val T (G) (s 0 , ν 0 ): If R(G) is non-negative, for all ε > 0 we can fix an ε-optimal strategy σ Min for Min in T (G). It is a winning strategy, so every play derived from σ Min in T (G) reaches a target leaf, and can be mimicked in R(G) by Lemma 18. Therefore, σ Min can be mimicked in R(G), where it is also winning, with the same weight. From this we deduce Val R(G) ((ℓ 0 , r 0 s 0 , ν 0 ). If R(G) is non-positive, the same reasoning applies by considering an ε-optimal strategy for Max in T (G).
This proof not only holds on an SCC, but also on full almost-divergent WTGs, by simply stacking the semi-unfoldings of each SCC on top of each others.
Note that the semi-unfolding procedure of an SCC depends on sup |wt T |, where wt T can be the value function of an SCCs under the current one. Assuming all configurations have finite value, we can extend the reasoning of Lemma 16 and bound all values in the full game by |R(G)|w e max + sup |wt T |, which let us bound uniformly the unfolding depth of each SCC and gives us a bound on the depth of the complete semi-unfolding tree: |R(G)|(5|R(G)|w e max + 2 sup |wt T | + 2) + 1

D.1 Proofs of the approximation of kernels
Proof (Proof of Lemma 6). Since ρ and ρ ′ follow the same locations ℓ of G, one reaches a target location if and only if the other does. In the case where they do not reach a target location, both weights are infinite, and thus equal. We now look at the case where both plays reach a target location, moreover in the same step. Consider the region path π of the run ρ: π can be decomposed into a simple path with maximal cycles in it. The number of such maximal cycles is bounded by |L × Reg(X, M )| and the remaining simple path has length at most |L × Reg(X, M )|. Since all cycles of a kernel are 0-cycles, the parts of ρ that follow the maximal cycles have weight exactly 0.
Consider the same decomposition for the play ρ ′ . Cycles of π do not necessarily map to cycles over locations of C N (G), since the 1/N -regions could be distinct. However, Lemma 2 shows that, for all those cycles of π, there exists a sequence of finite plays of G whose weight tends to the weight of ρ ′ . Since all those finite plays follow a cycle of the region game R(G) (with G being a kernel), they all have weight 0. Hence, the parts of ρ ′ that follow the maximal cycles of π have also weight exactly 0. Therefore, the difference |wt G (ρ) − wt CN (G) (ρ ′ )| is concentrated on the remaining simple path of π: on each transition of this path, the maximal weight difference is 1/N × w L max since 1/N is the largest difference possible in time delays between plays that stay 1/N -close (since they stay in the same 1/N -regions). Moreover, the difference between the output weight functions is bounded by Λ/N , since the output weight function wt T is Λ-Lipschitz-continuous and the output weight function of C N (G) is obtained as limit of wt T . Summing the two contributions, we obtain as upper bound the constant B/N . Lemma 7). Let us prove that both Val G (ℓ, ν)

Proof (Proof of
Val CN (G) ((ℓ, r, v), v) + α and Val CN (G) ((ℓ, r, v), v) Val G (ℓ, ν) + α, with α = B/N . By definition and determinacy of turn-based WTG, this is equivalent to proving these two inequalities: play(((ℓ, r, v), v), σ ′ Max , σ ′ Min ))| α. To show the first inequality, it suffices to show that for all σ ′ Min , there exists σ Min such that for all σ Max , there is σ ′ Max verifying (β). For the second, it suffices to show that for all σ ′ Max , there exists σ Max such that for all σ Min , there is σ ′ Min verifying (β). We will detail the proof for the first, the second being syntactically the same, with both players swapped.
We build σ Min , f , and g by induction on the length n of plays, over prefixes of plays of length n− 1, n and n, respectively. For n = 0 (plays of length 0 are those restricted to a single configuration), we let f (ℓ, ν) = ((ℓ, r, v), v) and g ((ℓ, r, v), v) = (ℓ, ν), leaving the other values arbitrary (since we will not use them).
We then fix a strategy σ Max of Max in the game G, which determines a unique play play((ℓ, ν), σ Max , σ Min ). We construct a strategy σ ′ Max of Max in the game C N (G) by building the unique play play (((ℓ, r, v), v), σ ′ Max , σ ′ Min ) we will be interested in, such that each of its prefixes is in relation, via f or g, to the associated prefix of play((ℓ, ν), σ Max , σ Min ). Thus, we only need to consider a prefix of play ρ ′ ∈ FPlays Max CN (G) that starts in ((ℓ, r, v), v) and is consistent with σ ′ Min , and σ ′ Max built so far. Consider the play ρ = g(ρ ′ ), starting in (ℓ, ν) and consistent with σ Min , and σ Max (by assumption). For the decision (d, δ) = σ Max (ρ) (letting ρ + be the extended prefix), the definition of f and g ensures that there exists a decision (d ′ , δ ′ ) after ρ ′ that results in an extended play ρ ′ + that is 1/N -close, via f or g, with ρ + . We thus can choose σ ′ Max (ρ ′ ) = (d ′ , δ ′ ). We finally have built two plays play((ℓ, ν), σ Max , σ Min ) and play((ℓ ′ , ν ′ ), σ ′ Max , σ ′ Min ) that are 1/Nclose, as needed, which concludes this proof. Lemma 8). By construction, the approximated value is piecewise linear with one piece per 1/N -region. To prove the Lipschitz constant, it is then sufficient to bound the difference between Val CN (G) ((ℓ, r, v), v) and Val CN (G) ((ℓ, r, v ′ ), v ′ ), for v and v ′ two corners of a 1/N -region r. We can pick any valuation ν in r and apply Lemma 7 twice, between ν and v, and between ν and v ′ . We obtain |Val CN (G) ((ℓ, r, v)

D.2 Computing the value of an acyclic WTG
Note that for a piecewise linear functions with finitely many pieces, being Λ-Lipschitz-continuous over regions is equivalent to being continuous over regions and having all partial derivatives bounded by Λ in absolute value.

Lemma 19.
If for all ℓ ∈ L, V ℓ is piecewise linear with finitely many pieces that have all their partial derivatives bounded by Λ in absolute value, then for all ℓ ∈ L, F (V ) ℓ is continuous over regions and piecewise linear with finitely many pieces that have all their partial derivatives bounded by max(Λ, |wt(ℓ)| + (n − 1)Λ) in absolute value.
Proof. We will show that for every region r, F (V ) restricted to r has those properties. Note that they are transmitted over finite min and max operations. The continuity over regions is easy to prove because it is stable by inf and sup. We now use the notations and definitions of [1] to bound the partial derivatives.There exists a partition cost function (P, F ) that represents V , with P an ndimensional nested tube partition and F a mapping from the leaf nodes of P to linear expressions over variables in X. Intuitively, P defines a finite arborescence of convex spaces, defined by linear inequalities, whose root is the whole region r and whose leaves partition r into cells. A crucial property of those cells ( [1,Theorem 4]) is that, for a given valuation ν, the delays t that need to be considered in the sup or inf operation of F (V ) (ℓ,ν) correspond to the intersection points of the diagonal half line containing the time successors of ν and borders of cells (if ν b is such a valuation, t = ν b − ν ∞ is the associated delay). In particular, there is a finite number of such borders, and the final F (V ) ℓ function can be written as a finite nesting of finite min and max operations over linear terms, each corresponding to a choice of delay and a transition to take. Formally, there are several cases to consider to define those terms, depending on delay and transition choices. For each available transition δ, those terms can either be: 1. If a delay 0 is taken and all clocks in Y ⊆ X are reset by δ, then If a delay t > 0 (leading to valuation ν b on border B) is taken and the clocks in Y are reset by δ, then wt Σ ((ℓ, ν) In the first case, the resulting partial derivatives are 0 for clocks in Y , and the same as the partial derivatives in V ℓ ′ for all other clocks, which allows us to conclude that they are bounded by Λ. We now consider the second case. We argue that the second case could be decomposed as a delay followed by a transition of the first case, meaning that we can assume Y = ∅ without loss of generality.
There are again two cases: the border B being inside a region or on the frontier of a region. If the border is not the frontier of a region, it is the intersection points of two affine pieces of V ℓ ′ whose equations (in the space R n+1 whose n first coordinates are the clocks (x 1 , . . . , x n ) and the last coordinate correspond to the value V ℓ ′ (x 1 , . . . , x n )) can be written y = n i=1 a i x i + b (before the border) and y = n i=1 a ′ i x i + b ′ (after the border). Therefore, valuations of the borders all fulfil the equation Consider that ℓ is a location of Min (the very same reasoning applies to the case of a location of Max). Since F computes an infimum, we know that the function mapping the delay t to the weight obtained from reaching ν +t is decreasing before the border and increasing after. These functions are locally affine which implies that their slopes verify: We deduce from these two inequalities that A 0. The case where A = 0 would correspond to the case where the border contains a diagonal line, which is forbidden, and A > 0. Consider now a valuation of coordinates ν = (x 1 , . . . , x n ) and another valuation of coordinates ν ′ = (x 1 , . . . , x k−1 , x k + λ, x k+1 , . . . , x n ). The delays t and t ′ needed to arrive to the border starting from these two valuations are such that ν + t and ν ′ + t ′ both verify (2). We can then It is now possible to compute the partial derivative of F (V ) ℓ in the k-th coordinate using We may compute it by using the equations of the affine pieces before or after the border. We thus obtain In the case where a k a ′ k , the first equation, with (3), allows us to obtain that the partial derivative is at most a k . We may then lower wt(ℓ) by − n i=1 a ′ i to obtain that the partial derivative is at least a ′ k . Since a k and a ′ k are bounded in absolute value by Λ, so is the partial derivative. We get the same result by reasoning on the second equation if a ′ k a k . We now come back to the case where the border is on the frontier of a region. Then, it is a segment of a line of equation x k = c for some k and c. V ℓ ′ contains at most three values for points of B: The limit coming from before the border, the value at the border, and the limit coming from after the border. The computation of F (V ) computes values obtained from all three and takes the min (or the max). Now, let y = n i=1 a i x i + b be the equation defining the linear piece of V ℓ ′ before the border (resp. at the border, after the border). Consider now a valuation of coordinates ν = (x 1 , . . . , x n ) and another valuation of coordinates ν ′ = (x 1 , . . . , x j−1 , x j + λ, x j+1 , . . . , x n ). The delays t and t ′ needed to arrive to the border starting from these two valuations are such that ν + t and ν ′ + t ′ both verify x k = c. We can then deduce that t ′ − t = 0 if j = k and t ′ − t = −λ if j = k. It is now possible to compute the partial derivative of F (V ) ℓ in the j-th coordinate using We may compute it by using the equations of the linear piece before the border (resp. at the border, after the border). Then, Then, the partial derivatives are bounded, in absolute value, by |wt(ℓ)| + (n − 1)Λ.
As a corollary, we can now obtain Lemma 9, or more precisely: Lemma 20. Consider an acyclic WTG G of depth i with all the output weights being Λ-Lipschitzcontinuous over each region (and piecewise linear, with finitely many pieces). Then, A weighted timed game G with two clocks x and y, and the portion of its region game R(G) accessible from configuration (ℓ0, (0, 0)). Locations of Min (resp. Max) are depicted as circles (resp. squares). The states of R(G) are labeled by their associated region, location and weight, and transitions are labeled by a representation of their guards and resets. Since each location ℓ of G leads to a unique states (ℓ, r) of R(G), we will refer to states by their associated location label.
Therefore, R(G) only contains non-negative SCCs and is almost-divergent. Since all states are in the attractor of Min towards L T , all cycles are non-negative and the output weight function is bounded (on all reachable regions), there are no configurations in R(G) with value +∞ or −∞.
We let the kernel K be the sub-game of R(G) defined by π 2 , and we construct a semi-unfolding T (G) of R(G) of equivalent value. Following Appendix C, we should unfold the game until every stopped branch contains a state seen at least 3|R(G)|w e max + 2 sup |wt T | + 2 = 3 * 3 * 4 + 2 * 1 = 38 times. We will unfold with bound 4 instead of 38 for readability (it is enough on this example). Thus the infinite branch (ℓ 1 ℓ 2 ) ω is stopped when ℓ 1 is reached for the fourth time, as depicted in Figure 6. Fig. 6. The kernel K (with input state ℓ1), and a semi-unfolding T (G) such that ValG(ℓ0, (0, 0)) = Val T (G) (ℓ0, (0, 0)). We denote ℓi, ℓ ′ i and ℓ ′′ i the locations in K, K ′ and K ′′ .
Let us now compute an approximation of Val T (G) . Let us first remove the states of value +∞: ℓ ′′′ 1 and ℓ ′′ 2 . Then, we start at the bottom and compute an (ε/3)-approximation of the value of ℓ ′′ 1 in the game defined by K ′′ ℓ1 and its output transition to ℓ ′′ t . Following Section 6, we should use N 3(4 + 1)/ε and compute values in the 1/N -corners game C N (K ′′ ℓ1 ) in order to obtain an (ε/3)-approximation of the value function. For ε = 15 we will use N = 1 (in this case the computation happens to be exact and would also hold with a small ε) We construct this corner game, and obtain the finite (untimed) weighted game in Figure 7.
Following Section 6 one last time, we should use N 3(5+3)/ε and compute values in the 1/Ncorners game C N (K ℓ1 ). This time, let us use N = 3 to showcase an example where the computed value is not exact. We can construct a finite (untimed) weighted game as in Figure 7, and obtain a value for each 1/3-corner of state ℓ ′ 1 . From these results, we define a piecewise-linear function by interpolation, as depicted in Figure 9. .

D.4 Complexity analysis
We will express complexities according to several parameters: |L|, |X|, greatest guard constant M , greatest location and transition weight constants w L max and w ∆ max . We also need to keep track of the output weight functions' characteristics. Recall that the output weight functions must be piecewise linear with finitely many pieces and Lipschitz-continuous over regions. We define three parameters, its Lipschitz constant Λ, its number of linear pieces J and a bound U (that we call additive bound) on its additive constant, such that if (x 1 , . . . , x |X| ) → |X| i=1 a i x i + b defines one of those linear pieces, then |b| U and ∀1 i |X|, |a i | Λ.
Note that |L|, |X| and J are all polynomial in the size of the input, but M , w L max , w ∆ max , Λ and U are exponential in the size of the input if constants are encoded in binary.
We start with simple estimates: Tree Let us recall the complexity of the value iteration algorithm, used to compute the exact value of an acyclic WTG: Input: An acyclic game of depth i. Algorithm schema: Computes F i (V 0 ) = Val i = Val. Output: A Λ ′ -Lipschitz-continuous function with J ′ pieces and additive bound U ′ that is the game's value.
-Λ ′ is of the form Λ Λ ′′ with Λ ′′ polynomial in w L max and |X| and exponential in i. -J ′ is of the form J |X| J ′′ with J ′′ polynomial in M and |L| and exponential in |X| and i.
-U ′ is of the form U + U ′′ with U ′′ polynomial in M , w L max , w ∆ max and i.


Evaluation of E-Learning Web Sites Using Fuzzy Axiomatic Design Based Approach

High quality web site has been generally recognized as a critical enabler to conduct online business. Numerous studies exist in the literature to measure the business performance in relation to web site quality. In this paper, an axiomatic design based approach for fuzzy group decision making is adopted to evaluate the quality of e-learning web sites. Another multi-criteria decision making technique, namely fuzzy TOPSIS, is applied in order to validate the outcome. The methodology proposed in this paper has the advantage of incorporating requirements and enabling reductions in the problem size, as compared to fuzzy TOPSIS. A case study focusing on Turkish e-learning websites is presented, and based on the empirical findings, managerial implications and recommendations for future research are offered.

Introduction
E-Learning, one of the e-service applications, is a wide set of applications and processes that manage diverse types of electronic media to deliver vocational education and training (Aladwani and Palvia, 2002). For e-learning service providers, the Internet serves as the primary interface with the e-learners, since the e-learning web site has a much more extended function, compared to conventional web sites, which only disseminate information about services and products. Consequently, the web site quality should be considered as a critical success factor for e-learning service providers. Especially, in the case of vital education or training services, the web site quality and its evaluation should be studied in a more detailed manner from e-learners' perspective (Colette, 2001).
In a number of publications, quantitative methods are adopted for the evaluation of web site quality, with statistical methods ranking as the most widely used assessment tools In another study, the authors integrate fuzzy AD and fuzzy AHP into QFD (Quality Function Deployment) principles for routing of shipping investment decisions in crude oil tanker market (Celik et al., 2009c). Celik (2009)  The aim of this paper is to attain a group consensus on functional requirements of an ideal e-learning web site. A case study is then conducted in order to evaluate several elearning web sites according to these functional requirements with group fuzzy AD. Fuzzy AD methodology is based on the conventional AD; however, crisp ranges are replaced by fuzzy numbers that represent linguistic terms. For measuring intangible criteria such as reliability, responsiveness, etc., fuzzy AD is applied to translate linguistic terms into performance measures. Also, group consensus is sought throughout the study and therefore, fuzzy AD model is enhanced with a group decision making tool.
The paper is organized as follows. In next section, e-learning web site evaluation criteria are defined. Section 3 briefly describes the proposed fuzzy AD based evaluation methodology. A case study is conducted in e-learning web sites evaluation and the outcomes are explained in Section 4. The concluding remarks are given in the last section.

Evaluation criteria for e-learning web sites
Internet-oriented applications aim at satisfying current educational needs by closing the gap between traditional educational techniques and future trends in technology-blended education (Tzouveli et al., 2008), enabling a new type of education on online platforms. E-Learning refers to Internet technologies used to deliver a broad array of solutions that support the instructional process in a networked environment through the establishment of an interactive virtual classroom (Poon et al., 2004). The expected outcomes of online teaching and learning are largely dependent on the quality of the teaching processes and the effectiveness of online access. To this end, e-learning systems must be designed and constructed cautiously, especially while applying a scientific approach with well-designed procedures and techniques. The ultimate goal is to accomplish an effective and high quality learning system, comparable with the traditional educational systems (Colette, 2001). Web sites appear as the primary interface to the end user (e-learner) and user satisfaction vis-àvis human-computer interaction determines the quality of the e-learning provider. An organization with a poor web site or ineffective services may project weaken the organization's image and position. Hence, determining evaluation criteria for e-learning web sites is important in order to determine user needs (Ahn et al., 2007). In this context, an e-learning web site quality has to be analyzed in a more detailed manner.
Literature offers numerous studies investigating e-service and e-learning web site evaluation criteria. Webb and Webb (2004) states that a business to customer (e-learning provider to e-learner, in our context) web site quality is directly affected by service quality and information quality. According to Ahn et al. (2007), even though web site evaluation criteria may vary, the main categories include system, information, and service quality.
System quality (such as interface design and functionality), is an engineering oriented performance characteristic while information quality (such as completeness and timeliness) has both engineering and operational characteristicsService quality refers to availability of communication, mechanisms for accepting consumer complaints and their timely resolution with responsiveness, assurance, and follow-up services. According to the survey conducted by Poon et al. (2004), five main factors influence the effectiveness of e-learning process: students' behavior, characteristics of lecturers, interactive application, technology or system, and the institutions. On the other hand, Mahdavi et al. (2008) state that elearner satisfaction can be classified into four dimensions: content, personalization, learning community, and learner interface. Kim and Lee (2008) Ahn et al. (2007) state that technology-focused approach considers the web site as an information system, while service-focused approach sees a web site as a service provider.
Following criteria were determined with a point of view combining the two approaches:  Right and Understandable Content (C1): This criterion includes credibility, clearness and succinctness. While using educational web sites, authority is a particular concern, as high quality content must be assured. Instructional objectives should also be assured. In addition, the content should be easily understood, unambiguous and succinct.
 Complete Content (C2): This criterion includes accuracy and coverage. The purpose of this assessment is to guarantee that the content is actually correct: up to date, factual, detailed, exact and comprehensive. This criterion also assesses the existence of tests, quizzes and exams for adequate evaluation procedures.    User Interface (C7): This criterion includes the design appearance, consistency, the information structure and the organization of the web site. Applications of the right design principles are essential. A consistent interface allows the e-learners to follow the required tasks easily. The information structure and organization of the web site should also be easy to follow and to be understood by the e-learners.

Fuzzy Axiomatic Design based Group Decision-Making
In line with the multi-dimensional characteristics of web site quality, MCDM methodology is a powerful tool widely used for evaluating and ranking problems containing multiple, usually conflicting criteria. Over the years, several behavioral scientists, operational researchers and decision theorists have proposed a variety of methods describing how an evaluator might arrive at a preference judgment while choosing among the multiple alternatives. Hence, this work attempts to model the e-learning web site evaluation in an MCDM framework. In addition, the subjectivity and vagueness in the assessment process is dealt with fuzzy logic (Zadeh, 1975). Multiple decision makers (DMs) are often preferred rather than a single DM to avoid the bias and to minimize the partiality in the decision process (Herrera et al., 2001). Therefore, fuzzy MCDM with group decision is increasingly employed in literature, as evaluation criteria become more intangible and the decision making becomes more complex to make for single DM. For example, Chen and Cheng (2005) apply fuzzy MCDM with group decision to information systems personnel selection. Wang and Parkan (2008) consider fuzzy preference aggregation problem in group decision and they apply it to the broadband internet service selection. Recently, Yeh and Chang (2009) develop a hierarchical weighting method in order to assess the weights of a large number of evaluation criteria by pairwise comparisons. This paper proposes a set of evaluation criteria for e-learning web sites, as well as a methodology to evaluate these web sites. Main steps of the proposed methodology are recapitulated in Figure 1. The first step in the methodology is determining e-learning web site evaluation criteria. In this study, criteria described in Section 2 are employed. These Techniques employed in the study, namely Fuzzy AD, fuzzy AHP, Chen's aggregation methodology and fuzzy TOPSIS are now described.

Fuzzy Axiomatic Design
AD, a systematic method offering a scientific base for design, was introduced by Suh (1990) and its application areas include software design, quality system design, general system design, manufacturing system design, ergonomics, engineering systems, office cell design, and e-commerce strategies. AD is based on two axioms. The independence axiom states that the independence of functional requirements should be maintained and information axiom states that among the designs that satisfy the functional requirements, the design with the minimum information content is the best design. Information content, on which MCDM technique is based, represents a function of probability of satisfying a functional requirement . Therefore, the design with the highest probability to meet these requirements is the best design. Information content of a design with probability of success for a given is defined as follows: Fig. 1. This is the caption for the figure. If the caption is less than one line then it is centered. Long captions are justified manually.

Literature survey Expert experiences Web search
Step 1. Determining e-learning website evaluation criteria Step 3. Determining e-learning web site alternatives Step 4.a. Evaluating of web site alternatives Step 4.b. Evaluating of functional requirements Step 5. Fuzzification and aggregation of experts' opinions Step 2. Determining criteria weights with fuzzy AHP

Expert opinions Expert opinions
Step 6. Calculating information contents Step 7. Calculating weighted information contents Step 8. Ranking of the e-learning web site alternatives Step 9. Comparing the obtained results with fuzzy TOPSIS

Expert opinions FAD implementation
According to Suh (2001), logarithm is employed in calculating the information contents, so as to attain additivity.
On the other hand, the probability of success is given by the design range (the requirements for the design) and the system range (the system capacity). Figure 2 illustrates the design and system ranges as well as the common area. The intersection of the ranges offers the feasible solution. Therefore, the probability of success can be expressed as: where and represent the lower and upper limits of the design range and where represents the probability distribution function of the system for a given .
The probability of success is equal to the common area . Consequently, the information content can be expressed as follows: Also, if the probability distribution function is uniform, the probability of success becomes: Therefore, the information content can also be written as: Fuzzy AD methodology is based on the conventional AD. However, crisp ranges are replaced by fuzzy numbers that represent linguistic terms ( Figure 3). In this study, triangular fuzzy numbers (TFNs) are employed. Intersection of TFNs representing design and system ranges presents the common area (Kulak and Kahraman, 2005a). Firstly, the information content is calculated as in a non-fuzzy environment. Then information content in a fuzzy environment is calculated as follows: In this study, the calculation of the weighted information content is adapted from Kahraman and Cebi (2008). This model requires determination of weights of criteria and sub-criteria. Total weighted information content for first level criteria is calculated as follows: where n is the number of first level criteria and ∑ = 1 . Likewise, information content for second level criteria (sub-criteria for criterion ) is calculated as follows: where is the number of sub-criteria for criterion and ∑ = 1 for = 1, … .
Finally, according to information axiom, alternatives are ranked with increasing order of information content.

Fuzzy AHP
It is not possible to assume that e-learning website evaluation criteria are of equal importance. There are many methods that can be employed to determine weights, such as eigenvector, weighted least square, entropy methods and diverse MCDM methods. In this study, the fuzzy extension of the one of the most outstanding MCDM approaches, AHP (Saaty, 1980) is used to determine the decision criteria weights. Despite its wide range of applications, the conventional AHP approach may not fully reflect a style of human thinking. One reason is that decision makers usually feel more confident to give interval judgments rather than expressing single numeric values. Furthermore, knowledge concepts and models contain tacit values and uncertainty, causing assessment and evaluation to be more difficult. This difficulty is handled by applying AHP in fuzzy environment to solve prioritisation and evaluation problems.
Firstly advocated by Zadeh (1965), fuzzy set theory has become important to deal with the ambiguity in a system. In this study, firstly linguistic terms are used to represent the expert assessments, then triangular fuzzy numbers, 1 to 9 as given in Table 1, are used to represent subjective pair-wise comparisons of evaluation processes in order to capture the vagueness.
The four step computational procedure is given as follows: 1. Compare the performance score. Triangular fuzzy numbers (1 , 3 , 5 , 7 , 9 ) are used to indicate the relative strength of each pair of elements in the same hierarchy.
3. Solve the fuzzy eigenvalue. A fuzzy eigenvalue, λ, is a fuzzy number solution to: where is a × fuzzy matrix containing fuzzy numbers and is a non-zero × 1 fuzzy vector containing fuzzy number . To perform fuzzy multiplications and additions by using the interval arithmetic and α-cut, the equation = is equivalent to: where: for 0 < ≤ 1 and all , , with = 1, 2, … , , = 1, 2, … , .
The α-cut is known to incorporate the experts or decision-maker(s) confidence over his/her preference or the judgments. The degree of satisfaction for the judgment matrix is estimated by the index of optimism . A larger value of the index indicates a higher degree of optimism. The index of optimism is a linear convex combination (Lee, 1999) defined as: When is fixed, the following matrix can be obtained after setting the index of optimism, , in order to estimate the degree of satisfaction: The eigenvector is calculated by fixing the value and identifying the maximal If is less than 0.10, the comparisons are acceptable, otherwise not. is the average index for randomly generated weights (Saaty, 1980).

4.
The priority weight of each criterion can be obtained by multiplying the matrix of evaluation ratings by the vector of attribute weights and summing over all attributes.
Then the degree of similarity between the standardized triangular fuzzy numbers and can be measured by the similarity function: where ( , ) ∈ [0,1]. The larger the value of ( , ), the greater is similarity between the standardized triangular fuzzy numbers and . The equation ( , ) = ( , ) is valid for the degree of similarity.

The aggregation result of the fuzzy opinions is
where operators ⨂ and ⨁ are the fuzzy multiplication operator and the fuzzy addition operator, respectively. The method is independent of the type of membership functions being used (Chen, 1998;Celik et al., 2009).

Fuzzy TOPSIS
In our methodology, another MCDM method, namely TOPSIS is applied in order to compare with fuzzy AD outcome. TOPSIS is proposed by Chen and Hwang (1992)    added-value of online access.
However, as the number of available online programs increases, the decision process becomes complex. Therefore, the need arises to evaluate the quality of e-learning providers as a pre-requisite of achieving high quality of e-learning in Turkey. In this study web sites of e-learning providers are considered given that the interface greatly influences the e-learner satisfaction with the e-learning system.
The methodology described in Figure 1 is applied to a case study. The goal of this case study is to evaluate and rank the quality performances of e-learning web sites, with the The e-learning web site evaluation process is performed by applying the following steps: Step 1.

Step 2. Determination of criteria weights for e-learning web site evaluation
DMs apply pairwise comparison to evaluate criteria as given in Table 2 and fuzzy AHP given in Section 3.2 is employed with the index of optimism value = 0.5 in order to determine e-learning web site criteria weights. The obtained results are shown in Table 3.
Step 3. Determination of alternatives  To assess the quality of e-learning web sites, 12 web sites given in Table 4 were designated, taking into account experts' opinions in the sector and research conducted through the search engines in January 2008. The first six of these web sites operate worldwide and the remaining six are active only in Turkey. Since the sites all offer mostly common services, the comparison is coherent.

Step 4. DMs' evaluation of web site alternatives and functional requirements
Linguistic terms employed in evaluating e-learning web sites needs to be translated into fuzzy numbers in order to operate on the judgments. In this study, 5-level fuzzy scale is used to assess the alternatives and another 5-level fuzzy scale is used to assess the   Table 7. Evaluation of alternatives by DM2. Table 8. Evaluation of alternatives by DM3.
functional requirements, as a bare minimum for functional requirements. Table 5, Figure 4 and Figure 5 describe the linguistic terms, their abbreviations and fuzzy membership functions.
As given in Table 5, in the evaluation process, 5-level scale was employed to translate linguistic terms into fuzzy numbers. The judgments of the experts on alternatives are illustrated in Tables 6,7 and 8.
The functional requirements of e-learning web sites are defined by three experts and illustrated in Table 9. Step

Fuzzification and aggregation of DMs' opinions
DMs' judgments on functional requirements and alternatives given in Step 4 are first translated into fuzzy numbers and then aggregated using the methodology described in Section 3.3. Table 10 displays aggregated evaluations on functional requirements and alternatives.

Computation of common area and information contents
Once fuzzified evaluations of DMs' judgments are aggregated, fuzzy AD methodology described in section 3.1 is applied to compute the common areas, which are shown in Table   11. The greater the common area, better is the response of the alternative to the functional requirements.    Table 11. Common areas (Ac)

Step 7. Calculation of the weighted information contents
Weighted information contents, given in Table 13, are calculated as described in section 3.1.
Step 8. Ranking the e-learning website alternatives The final ranking is also given in Table 13. Final results demonstrate that two web sites (W6 and W12) are eliminated, meaning that they do not meet the necessary functional requirements. The evaluation results point out that web site W11 web site has the best performance overall, followed by web site W2.
Step 9. Comparison with Fuzzy TOPSIS As described in Section 3.4, fuzzy TOPSIS is applied to the aggregated decision matrix in order to compare and justify the outcome of fuzzy AD. Tables 14 and 15 demonstrate distances from FPIRP and FNIRP and total distances. E-Learning web sites were ranked in increasing order of performance index. As seen in Table 16, the outcome of the fuzzy AD methodology is justified with fuzzy TOPSIS. W11 is ranked as the best alternative with both methodologies. Alternatives W6 and W12 are     and W12 are considered as well. This comparison of the outcome proves fuzzy AD to be a more suitable methodology to evaluate a large number of alternatives, since a bare minimum for the alternatives can be defined and unsuitable alternatives can easily be eliminated.

Concluding remarks
Current developments of information systems facilitate greatly the diffusion of knowledge. Knowledge and education form the source of more than 50% of the personal national incomes of especially developed western countries and a well educated manpower working at the jobs related with information (Kızılsu, 2006). On the other hand, the advances in information systems and internet change the nature of education (Poon et al., 2004). Therefore, education activities transfer to electronic platforms for higher speed and less effort. Consequently, the web sites hosting the e-learning system become an important interface for the end-user and web site quality directly affects e-learning provider's performance. Therefore, a performance analysis based on MDCM techniques is applied to measure the quality of e-learning web sites. More precisely, in this paper, a group decision based fuzzy AD methodology was applied to the problem of ranking e-learning web sites.
The proposed methodology is expected to provide additional contribution and decision support to the managers working in the learning and e-business industries, due to its advantages over already established techniques, such as fuzzy TOPSIS. Specifically, the proposed methodology incorporates functional requirements into the ranking and selection process, and can identify the alternatives that do not comply with the requirements.
For future research, the set of alternatives can be further extended and a two-stage MCDM analysis consisting of pre-assessment and detailed evaluation can be applied in order to thoroughly review e-learning web site alternatives. Given that service web sites are increasing in number, pre-assessment stage will eliminate rapidly the unsuitable candidates with general criteria and minimum assessment of alternatives, preferably with a single expert. A more meticulous evaluation with fewer alternatives will be realized with a hierarchic structure of criteria and a more detailed assessment of a group of expert. Also, criteria set may be altered to evaluate web sites other than e-learning, such as e-commerce, hospital, and bank web sites, based on the proposed methodology, since the general scheme of criteria can be applied to all web sites with only a few changes.