Nicolas Caniart
email: caniart@labri.fr

MERIT: an Interpolating Model-Checker

We present the tool MERIT, a CEGAR model-checker for safety properties of counter-systems, which sits in the Lazy Abstraction with Interpolants (LAWI) framework. LAWI is parametric with respect to the interpolation technique and so is MERIT. Thanks to its open architecture, MERIT makes it possible to experiment new refinement techniques without having to re-implement the generic, technical part of the framework. In this paper, we first recall the basics of the LAWI algorithm. We then explain two heuristics in order to help termination of the CEGAR loop: the first one presents different approaches to symbolically compute interpolants. The second one focuses on how to improve the unwinding strategy. We finally report our experimental results, obtained using those heuristics, on a large amount of classical models.

Motivations

Lazy Abstraction with interpolants (LAWI) [8] is a generic technique to verify the safety of a system. It builds a tree by unwinding the control structure of the system. Each edge of this tree represents a transition between two control points, and each node is labeled by an over-approximation of the actual reachable configuration at that node.

LAWI follows the CEGAR [3] paradigm. It loops over three steps: explore, check, and refine. The explore step expands the reachability tree by unwinding the control structure. At first, one starts from a very coarse abstraction of the system, ignoring the transition effect, just checking the reachability of control locations marked as bad. For that reason, reaching a bad location does not necessarily mean that the system is unsafe. The check step looks at a branch leading to a bad location, and tries to prove that it is spurious, that is, not feasible in the actual system. If it fails, then the system is unsafe and an error trace is reported. If it succeeds, then the unwinding must be refined to eliminate this spurious path. The refine step consists in labeling each node on the branch by an interpolant that over-approximates more closely the actual configurations. This explains the term lazy [5]: the refinement occurs only on a branch, not on the whole tree.

Since the unwinding is in general infinite, the algorithm might not terminate. To help termination, LAWI uses a covering relation between nodes. Under some conditions one can guarantee that any configuration reachable from a node s is also reachable from a node t in the tree. Node t then covers node s, which prevents from having to explore the subtree rooted at s, thus limiting the tree growth. LAWI terminates when all leaves in the unwinding tree are covered. However, since nodes are relabeled during the refine step, a covered node may be uncovered, so that termination can still not be guaranteed.

Interpolation with Symbolic Computation. Let us explain more precisely how to refine a spurious path s 0 τ1 -→ s 1 τ2 -→ • • • τn -→ s n , where each s i is a node of the unwinding and each τ i a transition of the system. An interpolant for this path [START_REF] Mcmillan | Lazy Abstraction with Interpolants[END_REF] is given by sets I 0 , I 1 , . . . , I n such that I 0 over-approximates the initial set of states, τ k (I k ) ⊆ I k+1 for any k and I n = ∅. Such a path interpolant witnesses that the path is spurious. In general, there are several path interpolants. The choice of the interpolant affects the algorithm behavior (and termination), since the covering relation depends on it.

In [START_REF] Mcmillan | Lazy Abstraction with Interpolants[END_REF] theorem proving and Craig interpolation is used to compute interpolants. Our work focuses on model-checking counter-systems [START_REF] Minsky | Computation : Finite and Infinite Machines[END_REF] with unbounded variables. The transition relations are encoded in the Presburger logic. So far, Craig interpolation algorithms are known only for fragments of this logic [START_REF] Jain | Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations[END_REF]. In [START_REF] Esparza | Abstraction refinement with Craig interpolation and symbolic pushdown systems[END_REF] it is showed how to compute interpolants symbolically. We have chosen to first experiment symbolic computation techniques in our model-checker, using the TaPAS tools [START_REF] Leroux | Tapas : The Talence Presburger Arithmetic Suite[END_REF]: an interface to various automata-or formula-based symbolic set representations.

The MERIT model-checker

MERIT is a model-checker for counter-systems based on the LAWI framework. We discuss its architecture, and present two improvements to the generic algorithm that we both implemented in MERIT.

Open architecture An interesting feature of the LAWI algorithm is that it offers a clear split between operations that work only on the control graph of the transition system, and those that compute interpolants. Thanks to this, we were able to use virtually any kind of techniques to compute interpolants: theorem proving, SMT-solvers, or symbolic computation. All operations or queries made on interpolants are implemented behind the interface of a single module, called a refinery. Changing the way interpolants are computed is just a matter of changing the refinery. We currently have one fully functional refinery based on the TAPAS framework [START_REF] Leroux | Tapas : The Talence Presburger Arithmetic Suite[END_REF] and we are working on an SMTsolver based refinery. Optimizing the interpolants. MERIT implements the classical symbolic weakest preand strongest post-conditions computations, which provide path interpolants [START_REF] Esparza | Abstraction refinement with Craig interpolation and symbolic pushdown systems[END_REF]. They are named weakest (resp. strongest) since they are the maximal (resp. minimal) sets of configurations that can appear on a path interpolant. MERIT also implements two original, and in practice more efficient techniques, that we both experimented.

-The first uses post-symbolic computation to find the closest node from the root of the refined branch where the reachability set becomes empty. From that node, it replays the trace backwards, computing the weakest path interpolant. This way, we obtain shorter branches than when using a weak-pre computation, but weaker interpolants on the higher part of the branch than when using a post computation. The idea of the heuristic is to make it easier to cover nodes by producing large interpolants high in the tree. -The second one is the dual of the first: it starts with a backward symbolic computation, and it then tightens interpolants on the lower part of the branch using strongest interpolants. Experimental results for the later technique, called cut-post, are given in Table 1. Tuning the unwinding strategy: BFS vs. DFS. Our experiments also show that the strategy used to expand the tree has an impact on the algorithm termination. In [START_REF] Mcmillan | Lazy Abstraction with Interpolants[END_REF] it is suggested to use a DFS strategy to expand the tree. Indeed a DFS strategy seems more adequate than a BFS one: suppose that the algorithem has to visit nodes at depth d. With systems having control locations of out-degree k, it is then necessary to compute and store at least k d nodes. In practice models with few control locations and high out-degree emerge naturally 1 .

The problem comes from the fact that a naive implementation of the DFS expansion strategy can behaves like a BFS. Indeed, in [START_REF] Mcmillan | Lazy Abstraction with Interpolants[END_REF] a node is expanded by adding all its children at once: e.g. a node t gets 3 children u, v, w. Because those nodes have not been refined, they are labeled by the full variable domain. Thus each of them can cover any node added after itself (provided they correspond to the same control location). The DFS proceeds by expanding u. Suppose now that children of u are all covered by either v or w. The DFS is therefore stopped and we have to explore a new branch (in v subtree). Again, the children of v may become covered by w. We see how a "BFS-like" behavior arises. This phenomenon does occur in practice and a combinatorial blowup indeed impairs the algorithm termination.

To fix this problem, we add only one child at a time. This way we add less nodes labeled by the full variable domain, which prevents from covering uselessly. The termination condition becomes more complicated. We also have to check that we did not forget to fully expand all internal nodes. Nonetheless our experiments show that, using this strategy, our tool can cope with models where the original strategy fails. The impact on the tool performance can be drastic, as showed in Table 1.

Experimental results

MERIT has been tested with a pool of about 50 infinite-state systems, ranging from broadcast protocols to programs with dynamic data-structures. The benchmark suite we use is available on the tool webpage (cf. Availability section, p. 4). The verification was successful in about 80% of the tests and MERIT detected 100% of the unsafe models.

The use of the "append one child at a time" unwinding strategy and the cut-pre or cut-post refinement techniques presented in Sec. 2 allowed MERIT to almost double the number of models it can tackle. Table 1 presents the results obtained (1) with the original algorithm, the weakest pre-conditions refinement (column Original Pre), the one child at a time algorithm with the same refinement technique (column 1 child Pre), as well as the one child algorithm with the cut-post refinement method (column 1 child cut-post). This shows how much we improved from the original algorithm. We also compare our tool to the tools FAST2 and ASPIC3 because they make use of acceleration [START_REF] Boigelot | On Iterating Linear Transformations Over Recognizable Sets of Integers[END_REF] techniques which are particularly efficient on the models we use to test MERIT. However MERIT is more efficient than FAST and ASPIC on many models. rithm [START_REF] Mcmillan | Lazy Abstraction with Interpolants[END_REF]. The models we experimented are particularly suited for acceleration techniques. However MERIT was able to tackle many models without using acceleration. Short-term goals: One of our short term goals is to get a fully functionnal SMT-Solver based refinery, to see how such a technique can compete with symbolic ones. Mid-term goals: We noticed that some refinement techniques are complementary: they succeed on different sets of models and the union of those sets almost covers the whole set of models. We tried hybrid refinement techniques that combine them. This allowed MERIT tackle more models. However the problem of choosing, on the fly, the proper interpolation technique for a branch is still an open problem. Finally, our experiments showed that some difficult examples would benefit from acceleration [START_REF] Caniart | Accelerating interpolation-based modelchecking[END_REF] techniques like the train model in Tab. 1. However combining LAWI and acceleration is still an open question. Acceleration is costly and the trade-off between that cost and the benefit for the cover relation has to be investigated.

Conclusion & Development perspectives

The presentation of the tool will be conducted around the model we use in the example section below.

A Availability

MERIT is available under free software license and can be downloaded from http:// www.labri.fr/~caniart/merit.html. The software is built on top of many libraries. For this reason we also provide pre-built binaries for the Linux platform.

Benchmarks The results for the complete benchmarks suite we use is provided at http://www.labri.fr/~caniart/benchmark-cav10.html.

B Merit input

Merit input format is the same as the one of the tool Fast4 . Briefly, this format consists of two parts: a description of the model through the declaration of a set of variables, control locations and transitions; a strategy in which a little script language allows to define sets of states (regions), test for set intersection, and parametrize Fast behaviour. It will ignore anything else. Fast syntax only allows for linear constraints in guards, actions (updates) and region definitions. The sample below sums up the fragment of the FAST format syntax that MERIT understands, as well as the formal grammar for the linear constraints that can be used in FAST guards, updates and regions definitions. Names between < > in the input sample refer to the corresponding rule in the grammar. In the grammar, # ∈ {≤, <, =, >, ≥}, VAR refers to a variable declared in the var statement (l. 2) and LOC to a location name declared in the state statement (l. 3). The complete reference of the Fast input format syntax is provided in the Fast User Manual 2 . Figure 1 provides the complete description of a model in FAST syntax.

Input processing

The input is parsed by MERIT to build the transition system augmented with one initial and one error location (resp. denoted '.' and '!'). Those locations are connected to the transition system according the INIT and ERROR regions. MERIT looks for those two regions in the strategy; they respectively define the sets of initial and bad states. The INIT set is used as a guard on the edge that leaves the '.' location and connects it to the original transition system. This transition is denoted INIT?. Similary the ERROR region is used on the ERROR? transition that connects the original transition system to the '!' location 5 . We now present, on a simple model, how the tuning in the exploration and refinement processes improves the original algorithm. We will look at a model of the MESI cache coherence protocol. Its description in FAST language is given on fig. 1. The corresponding transition system, augmented with the '.' and '!' locations, is depicted on fig. 2(b).

C Interesting points on a running example

First, to give an intuition of how LAWI works, we will go through a few iterations of the three algorithm steps: explore, check, and refine. Then we explain in more details the issue in the original unwinding strategy we talked about in sec. 2. Finally we will discuss the influence of the interpolant computation techniques.

C.2 How the DFS may degenerate

We have reached the point where we can explain why we claim that the unwinding strategy that consist in adding all children of node at once can be harmful for the algorithm termination. The exploration DFS will now visit node 6. This node is mapped to location 's' in the system and is labeled by Z d . Candidates to cover 6 are nodes 4 and 5. Both have been refined and their labels no longer entails Z d . Node 6 is then expanded. Nodes 18 to 22 are thus added to the unwinding. The branch 1

INIT? ---→ 2 LOAD ---→ 6 ERROR?
----→ 18 is refined, and then we visit node 19. The problem here is that node 19 can be covered by node 7 which has not been refined yet. Thus we will not visit 19 subtree yet. For the same reason, neither will we visit nodes 20 to 22 sub-trees. So no nodes below 6 will be expanded for now. We then have to visit node 7. Again we first refine the branch 1

INIT? ---→ 2 READINV -----→ 7 ERROR?
----→ 23. This refinement uncovers nodes 19 to 22. But when we visit nodes 24 to 27 we can then cover them by any of the nodes we just uncovered. So, again, none of the nodes below 7 are expanded. Because each time we try to expand a node mapped to location 's', we can find a node to cover it, the unwinding tree cannot grow in depth. Instead it grows in width and the more it grows the more nodes labeled with Z d we have. The number of nodes grows exponentially, but we gain very little information on the actual system behaviour, since very few refinements are made. This phenomenon slows down the algorithm convergence terribly, eventually preventing its termination. and the weakest pre-conditions interpolant computation technique, MERIT requires 85 refinements to conclude to the system safety. With the order we used to explain the unwinding process, only 25 refinements are required ! If tools like FAST allow the user to specify an order in which fire the transition, MERIT does not. It fires them in the reverse order they are read in the input model file. So far, we did not make any attempt to find ways to compute a "best order" in which fire the transitions. Moreover, since we have fully automatic techniques in mind, the benchmark results we present do not use any experimentally chosen "best order".

C.4 Influence of the interpolant computation technique

We now look at the influence of the interpolant computation technique. On the same example, we compare the weakest pre-condition and the so called cut-post computation techniques. With this later technique, when an interpolant for a branch π = s 0 , . . . , s n is computed, we first search for the node s k where π becomes unsatisfiable. It proceeds by computing the weakest pre-conditions for each nodes starting from the error node s n up towards s 0 (cf. fig. 3). Once s k is found, the interpolant for π is the sequence of sets I i = Z d for i = 0, . . . , k; I i = post τi (I i-1 ) for i > k.

π : As one can see, with this interpolant computation method we obtain very precise information on the system on nodes in the bottom of the unwinding tree, while retaining a very coarse abstraction on nodes near the unwinding tree root. It is then easier to cover nodes deep in the tree with nodes that are near the root. Note however that the interpolant computed with the cut-post technique are not as precise as the ones computed with the post technique, even on the lower part of the tree. This is because we start our computation from Z d , not the actual set of configurations of the system: we use post τ k+1 (Z d ) instead of post τ k+1 (C k ) where C k is the exact set of configurations reachable after transitions τ 1 . . . τ k have been fired. In practice, this interpolant computation technique proved to be the most efficient. But there are still some cases where these interpolant are not precise enough, as shown by the last line in the Table 1: on the ILLINOIS cache coherence protocol, this technique fails.

s 0 s 1 • • • s k s k+1 • • • s n-2 s n-

  region expr | region && expr | region statepred | region && statepred | statepred | expr expr := pred | expr && pred | expr pred | ( expr ) statepred := state = LOC pred := lsum # lsum updatelist := update | updatelist , update update := VAR ′ = lsum lsum := term | lsum + term | lsumterm term := VAR | NUMBER | NUMBER × VAR

Fig. 1 .

 1 Fig. 1. Model of the MESI Cache Coherence Protocol in Fast language

Fig. 2 .

 2 Fig. 2. Verification of the MESI model

1 s n τ1 τ k+1 τn- 1 τn 2 )Fig. 3 .

 123 Fig. 3. Computation of a cut-post interpolant for a path s 0 , . . . , s n

Table 1 .

 1 In this paper we presented MERIT, a model-checker tool that use symbolic interpolant computation techniques. It implements the Lazy Abstraction with Interpolants algo-Legend: V = # of variables; T: # of transitions; O: outcome, S means safe, U unsafe, ? tool does not know ; N: # tree nodes, R: # refinements. TOUT means time-out, MOUT memory outage. Benchmark results

					Original Pre	1 child Pre	1 child cut-post FAST ASPIC
	MODEL	V	T	O	N	R	TIME	N	R TIME	N	R TIME TIME TIME
	ILLINOIS 5	9	S	4152 415 2.12 777 388 1.72	-	-TOUT 1.75	?
	insert	48 51	S	74	11 1.28	70 11 1.35 70 11 1.25 3.97 0.14
	MESI	5	4	S	287 57 1.42 107 53 1.05 35 17 1.13 1.71	?
	merge	847 1347 S 6661 944 27.77 5413 952 40.34 189 30 3.79 TOUT 2.27
	MOESI	6	4	S	27	5	1.23	11 5 1.14 35 17 1.16 1.36	?
	train	7 12	S 20878 4302 268.64 205 101 1.51 1531 765 13.55 2.29	?
	deleteAll 18 19 U	13	2	1.10	13 2 0.98 13 2 1.18 1.0	0.11

Like for distributed system models, where the global control structure encoded by variables.

Available at http://www.lsv.ens-cachan.fr/Software/fast/

Available at http://laure.gonnord.org/pro/aspic/aspic.html

Available at http://www.lsv.ens-cachan.fr/Software/fast/

More than one transition may actually leave locations '.' and '!'. So MERIT appends an index to those transitions names. This will not be the case in the forthcoming example, and we ignore those indices here.

Availability MERIT is available under free software license at http://www.labri. fr/~caniart/merit.html.

C.1 How LAWI works

LAWI first step, explore is responsible for unwinding the transition system. Explore proceeds as follows: it picks a node in the unwinding tree. It first tries to cover that node. If it cannot, it will then expand it, i.e. add some childs to it. Again this may fail if the control location this node is mapped to in the transition system has no out-going transitions. Finally the explore step ensures that the node is not an error node. If it is the case then we jump to the check step. If not, a new node is chosen and the exploration goes on. Nodes to explore are chosen using a DFS traversal of the tree.

Initially the unwinding consists of a single node 1 mapped to the initial location '.'. As we said we first try to cover it, but cannot since it is the only node in the tree. So the node is expanded: only the INIT? transition can be fired from '.'. A single child is then added to 1, leading to a new node 2 mapped to location 's' (cf. fig. 2(a)). Exploration goes on from 2. Again this node cannot be covered: it is not mapped to the same location as the only other one in the tree, so it is expanded. This adds five new nodes to the tree: 3 to 7, mapped respectively to '!', and the last four to 's'. Since the unwinding is expanded through a DFS traversal, node 3 is picked for expansion. Node 3 has no outgoing transition so it cannot be expanded. But it is mapped to the error location: we then stop the exploration to check the spuriousness of the path from 1 to 3: 1

Assume we use the strongest post-condition interpolant computation method. Recall that all nodes are initially labeled by the full variable domain, denoted Z d where d is the number of variables in the system. We then check the trace spuriousness computing

∅ is an interpolant for the path and the path is spurious. We then go to the refinement step.

Refinement consists in updating labels of each node on the path. We intersect its current label with the corresponding set in the interpolant: node 1 is relabeled by Z d ∩ I 0 = Z d , node 2 by Z d ∩ INIT, and node 3 by ∅. After labels have been updated, the algorithm tries to cover the nodes on the path. None can be covered for now. Refinement is terminated, we go back to the system exploration.

The DFS continues on its traversal of the tree. The next node to be visited is 4. It is expanded and nodes 8 to 12 are added to the tree. The DFS then visits node 8 and first tries to cover it. The only other node mapped to location '!' in the tree is 4 which is now labeled by ∅. Obviously 4 cannot cover 8. It cannot be expanded either but it is an error node. We then need to check that the path from 1 to 8 is not an actual error path in the system. We again jump to the check step.

The path 1

----→ 8 is again spurious since we can compute an interpolant for it:

does not satisfy the guard of transition SHARE. Nodes labels are updated and we try to cover nodes on the path. This time we can cover 8 by 3, 4 by 2. We then go back to exploration.

The same happens with node 5 because INIT does not satisfy the guard of transtion WRITESHARED. Node 5 is covered by node 2 and node 13 by node 3.

C.3 MERIT unwinding strategy

We now describe how MERIT unwinds the control-structure and how it helps preventing the DFS traversal from degenerating into a BFS. The unwinding tree built by the algorithm is (partially) depicted on fig. 2(c).

Like in the previous case we start with a single node in the tree: 1 mapped to the '.' location. Node 1 is expanded which adds node 2 mapped to 's'. In turn 2 is expanded, but this time we only add a single child. Assuming children are added in the same order as before, the new node 3, is mapped to location '!'. Like before, 3 cannot be covered and since no transition leaves the '!' location, it cannot be expanded either. But it is an error node and a first refinement is made on the branch 1

Assume we use weakest pre-conditions interpolant computation method this time. The branch labels are updated as follows: node 3 is relabeled with I 2 = ∅, 2 with I 1 = pre ERROR? (∅) = ERROR and 1 with

Note another difference with the previous strategy: the DFS traversal responsible for expanding and visiting all nodes in the tree has now ran out of node. And there is no uncovered leaf. But obviously the tree labels do not provide an invariant for the safety of the system. An additional condition to the safe termination of the algorithm is that all nodes not labeled by ∅ nor covered must have as many children as the location they are mapped to have outgoing transitions.

According to these conditions, the algorithm has not finished yet. We have to choose a node to start a new DFS to further explore the system. MERIT implements different heuristics for that. We will present here the one that gives the best experimental results. The node is selected by a BFS traversal of the tree, that selects the highest possible node in the tree. The idea behind this heuristic is to explore a completely different sub-tree in the system. Following this heuristic, node 2 is selected to be the root of the new DFS.

So 2 is expanded a second time and it is added a second child: 4, mapped to location 's'. Then 4 is expanded with its first child 5 which is mapped to the error location. The branch 1

----→ 5 is then refined. Node 5 is labeled by ∅, node 4 by ERROR, node 2 is further refined so that it does not entails ERROR and 2 cannot cover 4, and finally 1 remains the same.

Then 2 is expanded a third time and we add node 6 and 7 to the unwinding tree. Visiting 7 triggers the refinement of the branch 1

Node 7 is labeled by ∅, node 6 by ERROR and can thus be covered by 4. Similarly nodes 8 and 10 are covered by 4.

Finally, nodes 4 get expanded a second time and nodes 11 and 12 are added to the tree and the branch 1

----→ 13 has to be refined. This time node 12 and 13 labels will be refined as well as node 4. Update of this later label will uncover nodes 6, 8, and 8. This is not a surprise: we may have eliminated covers by nodes that have not been refined, but we cannot prevent uncovers when a node is further refined.

Transitions firing order An interesting fact one can note here, is that if we had chosen to fire transitions in an alternate order, for instance READINV, LOAD, WRITESHARED, SHARE, we may have made different cover/uncover. The impact of the order in which transitions are fired can be important: with the MESI model, using the above order


Pierre Marquet
email: pierre.marquet@unilim.fr

Counterpoint: Is Pharmacokinetic or Pharmacodynamic Monitoring of Calcineurin Inhibition Therapy Necessary?

Individual dose adjustment of cyclosporine (CsA) or tacrolimus (TAC), which are criticaldose drugs widely used in transplantation, is important not only to prevent acute rejection but also to try and prolong graft (and patient) survival. New therapeutic regimens such as calcineurin inhibitor (CNI) sparing strategies have recently strengthened the need for fine individual dose adjustment of these drugs.

A good treatment-personalization strategy should employ a marker or a set of markers with 1) strong relationships with therapeutic and/or adverse effects; 2) low intra-individual variability; 3) established, and ideally validated, target values; and 4) easy and fast measurement.

So far, dose individualization has mainly been based on pharmacokinetics (PK), which monitors the handling of the drug by the body, but pharmacodynamics (PD), which focuses on the biologic effect of the drug on its target [START_REF] Burkhart | Pharmacodynamics in the development of new immunosuppressive drugs[END_REF], might also be useful as a replacement or as an adjunct.

Early on in the use of CsA, pre-dose (trough, C 0 ) concentration monitoring became the standard of care [START_REF] Marin | Is C2 monitoring or another limited sampling strategy superior to C0 monitoring in improving clinical outcomes in adult liver transplant recipients?[END_REF]. However, no trial has been conducted in transplantation to determine whether C 0 monitoring is superior to no therapeutic monitoring with respect to efficacy or toxicity [START_REF] Marin | Is C2 monitoring or another limited sampling strategy superior to C0 monitoring in improving clinical outcomes in adult liver transplant recipients?[END_REF] and it would not be ethically acceptable now given the obvious improvements brought to transplant patients by TDM. However, it has long been recognized that C 0 monitoring is suboptimal, and retrospective analysis of transplant populations monitored on C 0 has shown that the full inter-dose area under the concentration-time curve (AUC 0-12h ), abbreviated AUCs (AUC 0-6h or AUC 0-4h ), or Cmax has a stronger link with the residual inefficacy or toxicity episodes than C 0 . Because of the impracticability of routine AUC 0-12h monitoring, limited sampling strategies have been proposed as a more practical approach. In 2002, the CONCERT International Consensus Statement even recommended monitoring all de novo and maintenance renal and liver transplant recipients with the CsA blood concentration measured 2 hours post-dose (C 2 ), based on the findings that C 2 is the best single time-point predictor of AUC 0-4h , which represents the period of greatest inter-individual variability of CsA pharmacokinetics, the best surrogate for Cmax, and which coincides with the period of maximal calcineurin and interleukin-2 (IL2) inhibition [START_REF] Marin | Is C2 monitoring or another limited sampling strategy superior to C0 monitoring in improving clinical outcomes in adult liver transplant recipients?[END_REF][START_REF] Levy | Consensus on Neoral C(2): Expert Review in Transplantation (CONCERT) Group. Patient management by Neoral C(2) monitoring: an international consensus statement[END_REF]. A recent paper critically reviewed the randomized trials comparing C 2 and C 0 monitoring in terms of clinical benefits (4). In de novo renal, hepatic, and cardiac transplant recipients the most consistent finding was a higher mean CsA dose in the early postoperative period in C 2 monitored patients, with no significant effect on the rate of acute rejection for a majority of these studies.

In stable transplant recipients, the majority of studies showed that C 2 monitoring resulted in a reduction in mean CsA dose, without obvious clinical benefit. Therefore, clinical evidence of the superiority of limited sampling strategies or C 2 over C 0 monitoring is still weak (2). C 0 monitoring has been standard of care since tacrolimus approval, although its therapeutic ranges have since changed. A recent consensus conference emphasized the lack of concentration-controlled trials investigating the relationships between tacrolimus concentrations and clinical outcome, and from which tacrolimus target blood concentrations could be derived [START_REF] Wallemacq | Opportunities to optimize tacrolimus therapy in solid organ transplantation: report of the European consensus conference[END_REF]. However, a large randomized trial demonstrated that a regimen based on TAC with low therapeutic ranges may be advantageous for renal function, allograft survival, and acute rejection rates, as compared with regimens based on low-dose cyclosporine, lowdose sirolimus, or standard-dose cyclosporine without induction [START_REF] Ekberg | Reduced exposure to calcineurin inhibitors in renal transplantation[END_REF]. No randomized trial investigated the efficacy of alternative strategies to TAC C 0 monitoring, such as other time points or AUC 0-12 Bayesian estimation. Therefore, although C 0 may not be a good surrogate to TAC inter-dose AUC in all situations, based on the available evidence it is still impossible to conclude whether one particular TDM strategy is more effective than the others [START_REF] Wallemacq | Opportunities to optimize tacrolimus therapy in solid organ transplantation: report of the European consensus conference[END_REF].

CNI concentrations in lymphocytes or in the transplanted organ might better predict efficacy than whole blood concentrations. Preliminary data suggest that in the early post-transplantation period, CsA intracellular concentrations or AUC 0-12h in peripheral blood mononuclear cells (PBMC) would be lower in patients experiencing acute rejection or would decrease during the week preceding the acute rejection episode, and that TAC concentrations in PBMC would exhibit a very high inter-individual variability [START_REF] De Jonge | New insights into the pharmacokinetics and pharmacodynamics of the calcineurin inhibitors and mycophenolic acid: possible consequences for therapeutic drug monitoring in solid organ transplantation[END_REF]. However, at the present time, the extemporaneous isolation of PBMC from whole blood is laborious, LC-MS/MS is the only technique allowing the measurement of drug concentrations in such small sample volumes (even more so in patients with leucopenia), and these concentrations must be standardized per million cells or using a marker of cell number, all of which are rather imprecise.

Studies in liver transplant recipients receiving TAC or CsA showed that intra-hepatic CNI concentrations were lower in patients with, than in those without, acute rejection, and that there was an excellent correlation of TAC intra-graft concentration with the severity of rejection, contrary to TAC whole blood concentrations [START_REF] De Jonge | New insights into the pharmacokinetics and pharmacodynamics of the calcineurin inhibitors and mycophenolic acid: possible consequences for therapeutic drug monitoring in solid organ transplantation[END_REF]. However, the determination of tissue CNI concentrations is unlikely to make its way into clinical practice [START_REF] De Jonge | New insights into the pharmacokinetics and pharmacodynamics of the calcineurin inhibitors and mycophenolic acid: possible consequences for therapeutic drug monitoring in solid organ transplantation[END_REF]. The absence or weak inhibition of IL2 production in whole blood [START_REF] Stein | Inhibition of stimulated interleukin-2 production in whole blood: a practical measure of cyclosporine effect[END_REF] or in CD8+ lymphocytes (9) were described to be linked with a high acute rejection incidence in renal and liver transplant patients, respectively. Also, patients with a high pre-transplantation IL2 secretion were at higher risk of acute rejection after liver transplantation [START_REF] Boleslawski | Defective inhibition of peripheral CD8+ T cell IL-2 production by anti-calcineurin drugs during acute liver allograft rejection[END_REF]. However, to our knowledge no attempt has been made so far to try and individualize the CNI dose based on this biomarker.

The inhibition of calcineurin phosphatase activity (CaN) can be measured reproducibly in PBMC isolated by Ficoll density gradient centrifugation. Most studies have shown that CaN correlates with blood CsA concentrations (in particular C 2 ) in kidney transplant patients and with tacrolimus C 2 , but not C 0 , in liver and renal transplantation [START_REF] Yano | Pharmacodynamic monitoring of calcineurin phosphatase activity in transplant patients treated with calcineurin inhibitors[END_REF]. However, not all studies have found a correlation between CaN and CNI blood concentrations, which might be due to the imprecision of CaN measurement, as well as imprecision of standardization by the number of cells or the protein content. However, the intra-individual variability in CaN in patients on CNI would be much larger than the assay variability, suggesting that PD monitoring should be performed on each occasion in each patient. Unfortunately, calcineurin activity measurement in PBMC currently takes almost 24 hours, which is not practical for routine use.

Pre-dose CaN has been found to be an acceptable surrogate of the area under the CaN-time curve in renal and liver transplantation. Moreover, in both conditions as well as ex-vivo, CsA displayed deeper CaN inhibition than TAC [START_REF] Blanchet | Distribution of calcineurin activity in blood cell fractions and impact of tacrolimus inhibition[END_REF], which is not consistent with the greater invitro and clinical immunosuppressive effect of TAC, and suggests that this drug may have another mechanism of action. Anyway, owing to its inhibitory effect on hepatitis C virus replication not shared by TAC, CsA is also suspected to have a secondary mechanism of action. The relationships between CaN and clinical outcome are not clear. Conflicting results were found between CaN and graft-versus-host disease in stem cell graft recipients. In a rather small group of patients on TAC, nephrotoxicity was linked with lower CaN and acute rejection with higher CaN; however, CaN did not seem to be more predictive than C 0 [START_REF] Fukudo | Pharmacodynamic analysis of tacrolimus and cyclosporine in living-donor liver transplant patients[END_REF]. More generally, in patients on a CNI, the residual CaN in lymphocytes probably results from their pre-transplant CaN; the degree of activation of T lymphocytes; the intra-lymphocyte concentrations of CNI; and the intrinsic sensitivity of calcineurin to the CNI [START_REF] Marquet | Pretransplantation calcineurin activity: towards individualized therapy?[END_REF]. Also, the relationships of enzyme inhibition with biologic function and, eventually, graft outcome remain to be clearly established.

Another approach is to assess, by flow cytometry on T-lymphocytes stimulated in wholeblood cultures, the expression and down-regulation of cell surface markers (e.g., CD25, CD71) as an estimate of cell activation, the percentages of cells expressing intracellular cytokines (IL2, TNFα, INFγ) as an indicator of T-cell function, and T-cell proliferation [START_REF] Burkhart | Pharmacodynamics in the development of new immunosuppressive drugs[END_REF]. In liver transplant recipients on CsA or TAC, pre-transplantation IL2 expression by CD8+ T cells (but not calcineurin activity) was higher in patients who subsequently developed acute rejection [START_REF] Boleslawski | Defective inhibition of peripheral CD8+ T cell IL-2 production by anti-calcineurin drugs during acute liver allograft rejection[END_REF]. The same was true for intra-cellular IL2 at the time of the rejection episode, and a positive correlation was found between the percentage of IL2 expressing T cells and calcineurin activity. TNFα and IL2 expression correlates with transplant patients' age, and in healthy volunteers lymphocyte proliferation is higher in women [START_REF] Böhler | Cytokines correlate with age in healthy volunteers, dialysis patients and kidney-transplant patients[END_REF], suggesting that a variety of factors can influence these biomarkers, many of which have probably not been investigated yet.

Interestingly, T-lymphocyte activation and proliferation are not specifically linked with CNI effects as they are also affected by IMPDH or mTOR inhibition. Consequently, these tests might be used as markers of cellular immunosuppression rather than as markers of CNI effects, provided that their link with acute rejection and/or graft function is further demonstrated. However, such flow cytometry tests are still expensive, laborious, lengthy (up to 3-day incubation), and require that blood samples be analyzed within 24 hours of collection, which is far from being routinely applicable.

Finally, the detection and quantification by real-time PCR of mRNAs encoding inflammatory cytokines following ex-vivo cell activation might be used to monitor T-cell response. A weak expression of the NFAT-regulated IL2, INFγ, and GM-CSF genes was closely linked with the frequency of infections and cancer in kidney transplant recipients on CsA [START_REF] Sommerer | Pharmacodynamic monitoring of cyclosporine a in renal allograft recipients shows a quantitative relationship between immunosuppression and the occurrence of recurrent infections and malignancies[END_REF]. In patients with CsA dose tapering, expression of the same genes measured at 2 hours post-dose significantly increased after CsA dose reduction [START_REF] Sommerer | Ciclosporin A tapering monitored by NFAT-regulated gene expression: a new concept of individual immunosuppression[END_REF]. However, the superiority of gene expression measurement over classic therapeutic drug monitoring has not been demonstrated. Such methods still need to be tested for their clinical pertinence [START_REF] Burkhart | Pharmacodynamics in the development of new immunosuppressive drugs[END_REF].

To summarize the data, immunosuppression biomarkers have sometimes exhibited association with CNI exposure and/or clinical outcome, but the best parameters and methods to measure immune cell function in a fast and cost-effective way have still to be defined [START_REF] Burkhart | Pharmacodynamics in the development of new immunosuppressive drugs[END_REF]. All these tests suffer from long and cumbersome work-up and none have been validated prospectively by comparison to traditional TDM so far, nor used in clinical practice. The relationships between enzyme inhibition and biologic function, T-cell function and cellular rejection, acute graft rejection and graft function or survival (Figure 1) are probably not straightforward and need to be investigated in large patient populations before PD monitoring can be considered for individual dose adjustment.

In conclusion, PK monitoring of cyclosporine and tacrolimus has been improved over the years by a try-and-error process. Although formal clinical evidence is weak, TAC monitored on C 0 and/or CsA monitored on C 2 have become the basis of immunosuppression in most countries, associated with very low rejection rates during the first year post-transplant. However, it could possibly (and in the present era of CNI minimization, may need to) be improved further by means of more sophisticated approaches, such as AUC Bayesian estimation, preferably after validation by randomized prospective trials. Treatment personalization in transplantation may ultimately rely on the choice of the best drugs and the best starting doses using pre-transplant pharmacodynamic and/or pharmacogenetic tests, as well as on post-transplant pharmacokinetic and pharmacodynamic monitoring to compensate for post-transplantation changes, environmental factors and intra-individual variability [START_REF] Marquet | Pretransplantation calcineurin activity: towards individualized therapy?[END_REF].

However, clinical evidence in favor of CNI PD monitoring is currently at the lowest level and clinical experience is close to nil. Before it can be envisaged as a treatment personalization tool in organ transplantation, many questions still have to be answered, starting with the best marker of immunity to use, the influence of the physiological changes and immune system stimulation occurring post-transplantation, the effects of each immunosuppressive drug and their combinations on these biomarkers, and leading up to the relationships between such markers and clinical outcome. Continued efforts should also be made for a better understanding of the impact of pharmacogenetics on immunosuppressant benefit/risk ratio.

Figure legend

  CsA and TAC bind to intra-cellular proteins called immunophilins, and the CNIimmunophilin complex then inhibits calcineurin phosphatase activity. Calcineurin is involved in T-cell activation through dephosphorylation of the nuclear factor of activated T-cells (NFAT), enabling its translocation to the nucleus where it binds to the IL2 and interferon-γ (INF-γ) gene promoter regions, resulting in an increased secretion of the corresponding cytokines by the lymphocytes. Calcineurin also directly activates the lymphocytes by upregulating the expression of T-cell surface receptors, including the IL-2 receptor α chain CD25 and the transferin receptor CD71.Different approaches to pharmacodynamic monitoring of CNI therapy have been explored.

Figure 1 :

 1 Figure 1: flow-chart of the pharmacokinetic fate and pharmacodynamic effects of calcineurin


Roberto Battiti
email: battiti@dit.unitn.it

Marco Conti
email: marco.conti@iit.cnr.it

Enrico Gregori
email: enrico.gregori@iit.cnr.it

Mikalai Sabel
email: msabel@dit.unitn.it

Price-based Congestion-Control in Wi-Fi Hot Spots

Wireless networks are now proliferating due to the success of the IEEE 802.11b protocol, also known as "Wi-Fi" (Wireless Fidelity). A Wi-Fi network is characterized by a set of base stations (also called access points) placed throughout the environment and connected to the traditional wired LANs. This technology allows nomadic users a broadband access to the Internet if they are in the transmission range of an access point. A new business model, named Wi-Fi Hot Spots, is now emerging to exploit the potentialities of this technology. A hot spot is a "critical" business area, e.g., airports, stations, hotels, where users can have wireless access by subscribing a contract with the hot spot operator, or with a wireless Internet service provider (WISP). Due to the random access nature of the Wi-Fi technology, if the number of users connected to the same access point increases, the QoS experienced may quickly degrade. This generates complains from the users that, as a consequence, may change their WISP. In order to be competitive, a Wi-Fi hot spot operator needs simple and effective mechanisms to control the congestion therefore guaranteeing the QoS, and (at the same time) maximizing his/her revenues. In this paper we present and evaluate a price-based policy for the access control in a Wi-Fi hot spot. Our policy, named Price-based Congestion Control (PCC), controls the hot spot traffic by dynamically determining the access cost as a function of the current load in the hot spot. We develop a theoretical framework to compute for any load condition the access cost to maintain the hot spot in its optimal operating point, for any load condition. The effectiveness and robustness of the PCC policy has been evaluated by simulating a Wi-Fi hot spot. Both in saturated and notsaturated conditions the PCC policy provides a better channel utilization than the legacy Wi-Fi policy.

Introduction

Wi-Fi broadband Internet access is mushrooming and competing with legacy wireless (cellular) networks to support nomadic and data-centric applications. Telecom operators and service providers are gradually changing their marketing strategies and complementing their traditional offer with Wi-Fi. To reach an efficient use of the scarce bandwidth resources, market mechanisms appropriate for the Wi-Fi technology have been proposed ([IEEE802], [START_REF]Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications: Higher-Speed Physical Layer Extension, in the 2GHz Band[END_REF]).

A well-designed market should encourage spectrum efficiency and innovation. The two driving forces characterizing the Wi-Fi evolution are: the low cost-barrier for a service provider to enter in the market (no expensive infrastructure is required to start with), and the emerging tendency (mainly in USA) to deregulate the spectrum environment to create a secondary wireless market [START_REF] Crowcroft | BOURSE -Broadband Organisation of Unregulated Radio Systems through Economics[END_REF], secondary with respect to the primary cellular market.

In this work we propose a price-based policy for access control in a Wi-Fi hot spot. We consider a WLAN Operator and we investigate policies to control the traffic generated by its hot-spot users in order to maximize the revenues. The idea is to control the hot spot traffic by implementing a congestion-control pricing policy. At any given time instant, the access cost depends on the current load in the hot spot. When congestion increases, the WLAN Operator increases the access cost until some users give up transmitting. The objective is to maintain the quality of service, and to maximize the revenues.

In this paper, we assume a per-packet cost model, i.e., the user will be charged for the number of successfully transmitted and received packets. By increasing or decreasing the per-packet cost the WLAN Operator will control the number of active users and hence the congestion in the hot-spot. The aim is to drive the hot spot to operate in a status that maximizes the operator revenues and maintains the system in the most efficient state, i.e., the maximum aggregated throughput. Specifically, we identify as the optimal operating point of the system, the status corresponding to the maximum aggregated throughput. The rational for this choice is based on the following observations: -when the offered load is below this point, the WLAN Operator can stimulate additional traffic, thus increasing the revenues without congesting the system; -when the offered load is higher than this point, to maintain the same revenues of the optimal operating point, the WLAN Operator must increase the costs and thus the users have to pay more for a worse quality of service. This policy, of course, cannot be acceptable by the users that can hence migrate to another WLAN Operator implementing a more fair policy and therefore providing a better quality at a lower cost.

For example, a simple cost model which drives the system towards the optimal operating point can be the following. The cost model has only two values: a low and constant cost, say C 0 , whenever the load is below the maximum aggregated throughput of the system, and a very high value, say C infinite whenever the load exceeds the maximum aggregated throughput. The flat access cost stimulates the users to access the system until it is not overloaded, while the "infinite" cost C infinite forces the users to stop transmitting when the load exceeds the offered load. Obviously, this policy needs to be refined to avoid sharp fluctuations in the offered load as all users will give up when the C infinite is announced. Simple mechanisms to smooth these fluctuations can be introduced. For example gradually increasing the costs, or the cost increase can be announced to subsets of randomly selected users.

In this paper we discuss a Price-based Congestion Control (PCC) policy that can be implemented in an 802.11 based WLAN hot-spot. To define the PCC policy we exploit some results derived in [START_REF] Conti | Optimization of bandwidth and energy consumption in Wireless Local Area Networks[END_REF]. The cited work presents a distributed mechanism for controlling the congestion in a IEEE 802.11 network to guarantee that the system operates below the optimal operating point. Furthermore, the proposed mechanism asymptotically (with respect to the number of active stations) drives the system close to the optimal operating point. The main drawback of that approach is the requirement that all the network stations use a network interface card obtained by modifying the Wi-Fi cards. Obviously, this constraint is not acceptable in a WLAN hot spot in which the WLAN operator cannot force the use of modified Wi-Fi cards. In this paper, we exploit some of the ideas presented in [START_REF] Conti | Optimization of bandwidth and energy consumption in Wireless Local Area Networks[END_REF] to construct a "centralized" congestion control policy that only requires additional hardware/software in the Access Point while the users adopt standard Wi-Fi cards.

The paper is organized as follows. In Section 2, we present the main Wi-Fi characteristics and summarize previous results about Wi-Fi modeling that are relevant for this paper. In Section 3, we introduce the theoretical framework of the Price-based Congestion Control policy. The performance of the PCC policy are investigated, via simulation, in Section 4.

Wi-Fi

Wi-Fi cards implement the IEEE 802.11b standard. The 802.11b standard extends the 802.11 standard by introducing a higher-speed Direct Sequence Spread Spectrum (DSSS) Physical Layer in the 2.4 GHz frequency band. Specifically, 802.11b enables transmissions at 5.5 Mbps and 11 Mbps, in addition to 1 Mbps and 2 Mbps supported by 802.11. On top of the DSSS physical layer, the IEEE 802.11b standard implements a MAC layer that offers two different types of service: a contention-based and contention-free service. Hereafter, we focus on the contention-based service only. This service is implemented by the Distributed Coordination Function (DCF). According to the DCF, before transmitting a data frame, a station must sense the channel to determine whether another station is transmitting. If the medium is found to be idle for an interval longer than the Distributed InterFrame Space (DIFS), the station continues with its transmission. If the medium is busy, the transmission is deferred until the end of the ongoing transmission, and then the backoff procedure is activated. A random interval, (the backoff time) is selected and used to initialize the backoff timer. The backoff timer is decreased for as long as the channel is sensed as idle, stopped when a transmission is detected on the channel, and reactivated when the channel is sensed as idle again for more than a DIFS. The station is enabled to transmit its frame when the backoff timer reaches zero.

To guarantee fair access to the shared medium, a station that has just transmitted a packet and has another packet ready for transmission must perform the backoff procedure before initiating the second transmission.

The backoff time is slotted: its value is an integer number of slots uniformly chosen in the interval (0, CW-1). CW is defined as the Backoff Window, also referred to as Contention Window. At the first transmission attempt CW=CWmin, and it is doubled at each retransmission up to CWmax. In the 802.11b standard CWmin and CWmax are 32 and 1024, respectively. Obviously, it may happen that two or more stations start transmitting simultaneously and a collision occurs. In the CSMA/CA scheme, stations cannot detect a collision by hearing their own transmissions (as in the CSMA/CD protocol used in wired LANs). Therefore, an immediate positive acknowledgement scheme is employed to ascertain the successful reception of a frame. In detail, upon reception of a data frame, the destination station initiates the transmission of an acknowledgement frame (ACK) after a time interval called Short InterFrame Space (SIFS). The SIFS is shorter than the DIFS in order to give priority to the receiving station over other possible stations waiting for transmission. If the ACK is not received by the source station, the data frame is assumed to have been lost, and a retransmission is scheduled. The ACK is not transmitted if the received packet is corrupted. A Cyclic Redundancy Check (CRC) algorithm is used for error detection. After an erroneous frame is detected (due to collisions or transmission errors), a station must remain idle for at least an Extended InterFrame Space (EIFS) interval before it reactivates the backoff algorithm. Specifically, the EIFS shall be used by the DCF whenever the physical layer has indicated to the MAC that a frame transmission was begun that did not result in the correct reception of a complete MAC frame with a correct CRC value. Reception of an error-free frame during the EIFS re-synchronizes the station to the actual busy/idle state of the medium, so the EIFS is terminated and normal medium access (using DIFS and, if necessary, backoff) continues following reception of that frame. A MAC data frame contains the control information (hereafter denoted as MAC hdr ), a variable length data payload, which contains the upper layers data information, and the CRC field. The MAC hdr contains the MAC addresses in addition to other control information.

The values for the protocol parameters are summarized in Table 1, where τ is the air propagation time In that paper it is also shown that the ppersistent IEEE 802.11 protocol closely approximates the standard protocol (at least from the protocol capacity standpoint) if the average backoff interval is the same. This is obtained when the following equation holds:

p E B = [ ]+ ( ) 1 1 (1)
where E B [ ] is the average backoff interval.

Due to its memory-less backoff algorithm, the p-persistent IEEE 802.11 protocol is suitable for analytical studies. By exploiting the similarity of this protocol with the standard one, the analytical results derived from the p-persistent model can be used to infer the behavior of the standard protocol.

In this section, we assume a system with a variable number, M, of active stations accessing the channel according to the p-persistent IEEE 802.11 protocol. The stations transmit messages whose length (expressed as number of 802.11 time slots) is a random variable L with average l.

The behavior of the 802.11 channel access scheme can be described as a sequence of virtual transmission times. A virtual transmission time is the interval between two successful transmissions and, as shown in Figure 1, it includes a successful transmission and may include several collision intervals and idle periods. 1In the following we use the following notation: • Idle p _ is the number of consecutive empty slots; • Coll is the time the channel is busy due to a collision given that a transmission attempt occurs, also referred to as collision interval (see Figure 1). Obviously, Coll is equal to zero if the transmission attempt is successful, otherwise it is equal to the collision length; • t slot is the time duration of a time slot;

• E[ ] denotes the average operator, i.e., given a random variable X , E X [ ] is its average; Lemma 1. For M >> 1 and l > 1 the optimal operating point, corresponds to the system status that satisfies the following equation:

DIFS

E Idle p t E Coll slot _ [ ]⋅ = [ ] (2)
Closed form expressions for the E Idle p _ [ ] and E Coll [ ] in a p-persistent IEEE 802.11 with M active stations are derived (by exploiting classical probabilistic arguments) in [START_REF] Cali | Dynamic Tuning of the IEEE 802.11 Protocol to Achieve a Theoretical Throughput Limit[END_REF]. The formulas indicate that the optimal operating point is a function of the number of active stations (M), the length of transmitted packets, and the average congestion window (i.e., the p value). Therefore, by fixing the p value, and the length of transmitted packets, it is possible to determine the number of stations that must be active (in a hot spot) in order to maintain the system in the optimal operating point. Therefore, Equation (2) provides an effective tool that can be used by the Access Point to control the congestion status of the network. It is worth noting that the perspective of the PCC policy is complementary to the policies developed in the previous works ([CG02], [BCG02]). In those papers p is a variable whose value is dynamically set, while M cannot be modified. On the contrary, in this paper the p value (i.e., the average backoff window size) cannot be controlled, while the Access Point can try to modify the value of M (by increasing or decreasing the transmission cost). In detail, for each network condition, the Access Point tries to drive the M value to the optimal operating point, say M opt , that guarantees the satisfaction of Equation (2).

The Price-based Congestion Control (PCC) policy

To simplify the presentation, we assume that the PCC policy takes its decisions (i.e., the new price to be communicated to the hot spot users) at the end of each virtual transmission time. However, it is also possible to implement the same policy taking as a reference other events occurring on the channel, or assuming a periodic re-computation (and announcement) of the optimal price. As shown in the Section 4, the periodic announcement is the most robust solution for PCC.

The PCC policy operates in two steps. In the first step, it identifies the percentage increase/decrease in the number of active stations in the controlled hot spot to drive the system to the optimal operating point. In the second step, the policy identifies the price level to achieve the desired increase/decrease in the number of active stations. Before presenting the PCC policy in detail, we introduce some assumptions. i) After each successful transmission the AP decides the transmission-cost c to be applied to the future transmissions.

The time it takes to the AP to compute the new cost and to communicate it to the clients is assumed to be negligible. ii) To model the users behavior, we introduce a probability function P c

give up

_ ( ) . Specifically, P c

give up _ ( ) represents the probability that a user does not accept the c transmission-cost announced by the AP, and leaves the network for a random time. It is reasonable to assume that P c

give up _ ( ) is monotone not decreasing, i.e., when the cost increases the probability that a user gives up increases or remain the same. The AP estimates the P c

give up _ ( ) from the system history, by observing the users' reaction to changes in the price level. 2 iii) We model the arrival of new customers (new clients plus the clients that make a new attempt after a give-up period) in the hot spot through a Poisson process, with rate λ. λ is estimated by applying a moving window estimator to the recent history of the system.

end of the (n-1)-th virtual transmission interval n-th successful transmission collision and idle periods end of the n-th virtual transmission interval n-th virtual transmission interval

E Coll [ ] and E Idle _ p [ ] updating E Coll [ ] n E Idle _ p [ ] n M n M n -1 c n -1 c n

Figure 2: PCC policy behavior

Step 1. Percentage increase/decrease in the number of active stations The behavior of the PCC policy is shown in Figure 2. As mentioned before, PCC operates at the end of each virtual transmission time. As shown in Figure 1, this time interval (from the channel status standpoint) consists of one or more

P c

give up _ ( ) can be computed offline by exploiting the statistics collected on a daily (or longer) basis.

idle periods, and one or more busy periods. An idle period is made up of consecutive idle slots, while the busy period is an interval in which the channel is busy due to either a collision or a successful transmission.

To explain the behavior of the PCC policy, we focus on the end of the n-th virtual transmission interval. In addition, let's assume that, after computing E Idle p n _ [ ] and E Coll n [ ] , Equation (2) does not hold. Hence, the aim of PCC is to estimate the desirable number of stations that should be active in the future in order to equate the collision and idle costs. Specifically, we denote with M n the number of active stations that will guarantee (in the future) the balance between the idle-period length, and the collision cost, thus satisfying Equation (2). By assuming that M n stations will be active in the future, by applying the Taylor formula to the closed formulas, we can express E Idle p n _ [ ] +1 and E Coll n [ ] +1 as follows3 ([BCG02], [CG02]):

E Idle p p M p M E Coll l p M n n n n n [ _ ] , [ ] + + ≈ -⋅ ⋅ ≈ ⋅ ⋅ 1 1 1 2 (3)
where l is the average collision length (in time units) given that two stations collide. By exploiting (3), PCC increases or decreases the M value to have

E Idle p E Coll n n [ _ ] [ ] + + = 1 1 .
The following lemma directly defines M n .

Lemma 2. In a network adopting the p-persistent 802.11 access protocol, in which the message lengths {Li}, normalized to t slot , are a sequence of i.i.d. random variables, the M value corresponding to the optimal operating point is:

M l l p opt ≅ + ⋅ 1 2 (4)
Proof. Equation ( 4) is obtained by equating the expressions of E Idle p n _ [ ] +1 and E Coll n [ ] +1 defined by (3).

Lemma 2 provides to the AP the expression of the desirable M value. However, to exploit this expression the AP must have an estimate of the average backoff window size used in the WLAN (see Equation ( 1)). 4 This may be difficult to determine. To avoid this problem, in the following we present a method that computes the percentage increase/decrease of M without requiring any knowledge of p. To this end, we express M n as a function of an unknown quantity x, such that

M M x n n = + ( ) -1 1 (5)
where x denotes the percentage increase/decrease in the M n-1 value.

By using Equations (5), (3) and (2), we obtain Lemma 3. This Lemma provides a closed formula to estimate the x value starting from quantities that are easy to estimate.

= - + ⋅ ( ) + ( ) + ⋅ ⋅ + ( ) 2 4 1 2 2 [ ] [ ] [ _ ] [ ] (6)
Proof. By substituting (5) in the expressions of E Idle p n _ [ ] +1 and E Coll n [ ] +1 defined by (3), and by assuming

E Idle p E Coll n n [ _ ] [ ] + + = 1 1
, after some algebraic manipulations, we obtain:

x t E Coll t E Coll t E Idle p E Coll slot n slot n slot n n = - + ⋅ ( ) ± ( ) + ⋅ ⋅ + ( ) 2 4 1 2 2 [ ] [ ] [ _ ] [ ] (7
) Equation ( 7) provides two possible solutions to the problem, but only the solution given by ( 6) is correct for the PCC policy. This can be verified by focusing on the case in which

E Idle p n _ [ ] is equal to E Coll n [ ] .
In this case only by applying Equation (6) we obtain the correct value x=0, as the system is already in the optimal operating point.

Once the desirable percentage increase/decrease in the M value, the PCC computes the cost level that must be applied in the future to stimulate/discourage the users to access the system in order to approach the desired M value.

It is worth noting that Equation (6) completely defines the percentage increase/decrease in the M value in terms of quantities that the Access Point estimates by measurements on the network. These measurements may introduce fluctuations. To avoid harmful fluctuations, smoothing factors are normally introduced. Specifically, E Idle p n _ [ ] , and

E Coll n

[ ] can be computed as:

E Idle p E Idle p E Idle p n n n _ _ _ [ ] = ⋅ [ ] + - ( )⋅ ( ) [ ] - α α 1 1 (8) E Coll E Coll E Coll n n n [ ] = ⋅ [ ] + - ( )⋅ ( ) [ ] - α α 1 1
where α is a smoothing factor and E Idle p n

_ ( ) [
] and E Coll n ( ) [ ] are the average length of the idle periods and collision costs during the n-th virtual transmission time, respectively. The use of a smoothing factor is widespread in the network protocols to obtain reliable estimates from the network estimates by avoiding harmful fluctuations, e.g. RTT estimation in TCP. Previous work has shown that α = 0 9

. is a good compromise between accuracy and promptness [START_REF] Cali | Dynamic IEEE 802.11: design, modeling and performance evaluation[END_REF]. For this reason we assume α = 0 9

. as the default value. A similar approach can be used to avoid cost fluctuation. In this case the smoothing strategy must be modified to avoid frequent (small) modification in the transmission cost.

Step 2. The cost level that stimulate/discourage new users In the Step 1, the AP has identified the percentage increase/decrease of M (i.e., x). In this second step, the x value is used to determine the transmission cost to apply for the future transmissions in order to have M M x n n = + ( )

-1 1 active stations. The basis of this analysis is given by:

λ ⋅ [ ] ⋅ - ( ) + ⋅ - ( ) = - E t P c M P c M v n give up n give up n 1 1 1 _ _ ( ) ( ) ( 9
)
where E t v n [ ] denotes the average length of the virtual transmission time and it is estimated by applying a smoothing factor, α , see also Equation ( 8). The rationale behind Formula ( 9) is the following. The first term in the left hand side (l.h.s.) of ( 9) represents the expected number of users that accept to start a new session if a transmission cost equal to c is applied. The second term in the l.h.s of (9) represents the number of active users that accept to continue their transmissions given that they will pay a cost per-packet equal to c for future transmissions.

With some algebraic manipulation of Equation ( 9) we finally obtain:

P c E t M x E t M give up v n n v n n _ ( ) max , = ⋅ [ ] - ⋅ ⋅ [ ] +           - - 0 1 1 λ λ . ( 10
)
Equation ( 10) identifies the new c value, say c new , to achieve the optimal operating point. To use Equation (10) the AP requires the knowledge of M n-1 , i.e., the current number of active stations. In principle the AP can estimate this number by observing the MAC addresses of the stations with an active session. This is a conservative estimate because it may happen that some stations are connected to the Access Point but are not currently transmitting any data. However, we can avoid this problem, and at the same time further simplifying Equation (10), by noting that the intervals between successive updating of the price are quite small (in the order of a second). Hence, the number of new stations5 that connects to the access point during a measurement interval is expected to be low. Therefore, we can avoid the complexity in Equation (10) by neglecting in Equation (9) the impact of stations that will wake up in the future, and simply concentrating on optimizing the system for the current number of active stations. The impact of stations that will wake up in the next future will be taken into account in the successive price computations phases. According to this simplifying assumption, Equation (9) reduces to:

M P c M n give up n -⋅ - ( ) = 1 1 _ ( ) (11)
and by substituting (5) in ( 9) we obtain:

P c x give up _ ( ) = - (12)
Equation ( 12) provides a simple way to identify the new price without requiring any explicit knowledge of the number of the active stations. Unfortunately, (big) errors can be introduced if P c

give up _ ( ) is not a continuous function in the range [0,1]. For example in the case in which all users have the same threshold, say c , P c

give up _ ( ) is:

P c c c c c give up _ ( ) = < ≥     0 1 (13)
In this case, given a value x (0<x<1), any choice of the c value introduces a big approximation with negative effects on the overall system behavior. If the AP announces a price c, such that c c < , the system remains congested (as no station gives up) and the QoS remains low. On the other hand, by announcing a price c, such that c c ≥ , all stations give up and the system utilization, and hence the provider revenue, drops to zero.

The problem pointed out in the previous example occurs whenever P c

give up _ ( ) is defined only for a (small) subset of the price values. Hence given a value x it may not exist a c value that satisfies P c x give up _ ( ) =but we have two possible approximations, c low and c up , such that: P c x give up low low

_ ( )= - , P c x
give up up up _ ( )=and x x x low up < < . To eliminate (or at least to reduce this error) we propose to use selective announcements to a randomly selected number of users. Specifically, the algorithm operates as follows:

-the AP selects the price c up ; -for each station that is currently connected, the AP announces the new price according the following probability distribution:

Pr , Pr c c x x c c x x low up up up = { }= - = { } = 1
For example, in the 0-1 threshold case (see Equation ()), x up = 1, and if we wish to obtain a x = 0 40 . reduction in the number of active stations, the AP announces the high cost, c c up = , to x x up = 0 40

. of the stations. This policy based on selective announcements to randomly selected stations may be questionable in a real Wi-Fi hot spot. However, the focus of this work is to provide some theoretical foundations to define price-based congestion control policies in a Wi-Fi environment. The discussion of how such a policy can be implemented in a real environment is for further studies.

In the following sections we show the effectiveness of PCC policy by simulating the performance of a Wi-Fi network with or without the PCC policy.

PCC Performance Analysis

In this section we will extensively validate the capacity of the PCC policy to drive a Wi-Fi network close to the optimal operating point. We investigate the performance of a Wi-Fi hot spot in which there are M stations. A station can be either active, or in the sleep state. An active station accesses the channel whenever it has a frame to transmit. A station enters the sleep state when the AP announces a transmission price that is too high for the station to accept. Specifically, in our experiments we randomly assigned to each station a threshold for the maximum price it accepts to pay. When the price exceeds its threshold a station enters in the sleep state, and all packets in its queue are discarded. A station remains in the sleep state for an exponentially distributed random time. The average "sleep time" is the same for all stations and it is equal to 1 sec. When the station wakes up it starts to fill its queue again.

In our study, the maximum price accepted by a station is sampled from a truncated (to zero) normal distribution with average 50 and a standard deviation equal to 10, if not mentioned otherwise.

We perform two types of experiments: saturated and not-saturated. In saturated mode each station always has a nonempty queue, and therefore it is always willing to transmit. In not-saturated mode, each station generates new packets to transmit according to a Poisson distribution. The rate of the Poisson distribution is selected such that a station's bandwidth requirement is only a small fraction of the channel capacity. A large number of stations is therefore required to saturate the channel. Hence, in the not-saturated model, each station alternates between ON (i.e., with packets to transmit), and OFF (i.e., no packets to transmit) states.

The performance indices computed via simulation, have been estimated with the independent-replication technique. The deviation among the estimates achieved in the different runs are generally very small, and hence the error-bars are often not visible.

As said at the beginning of Section 3, the PCC policy may operate at different time instants. Hereafter, we analyze two different possibilities: updating at the virtual transmission time boundaries (denoted as Tv), and periodic updating (denoted as Tp). The periodic updates occur every 102.4 msec, i.e., a typical value for Wi-Fi beacon signal frequency.

Long packets

The main target of this performance study is to investigate the relationship between the channel utilization and the network congestion. In our experiments, several congestion levels are simulated by running a set of experiments with different M values.

As explained in Section 2, the MAC data frame contains in addition to the MAC hdr , a variable length data payload, hereafter referred to as packet. The results presented in this section are obtained with packets sizes sampled from a normal distribution with an average packet size of 1500 bytes (value typical for wired networks). The minimum packet size is 0, while the maximum size of 2130 bytes is below the limit of the Wi-Fi standard, i.e., 2312 bytes.

The effectiveness of the proposed PCC policy is shown in Figures 3 and4. These figures show the channel utilization levels achieved by adopting the PCC system, and compare this index with the utilization levels achieved with the legacy Wi-Fi approach (no pricing). The results show that the PCC policy significantly increases the Wi-Fi channel utilization as the network congestion increases. Simulative runs performed in our not-saturated scenario show that for networks with less than M=15 stations the price mechanism is never active, and the performance with or without the PCC policy are similar. After this congestion level, the PCC mechanism becomes more and more effective. In this case there are not significant differences between the Tv and the Tp policies. On the other hand, results under saturated conditions show interesting and relevant differences between the Tv and the Tp policies. Specifically, we observe that in few "unlucky" runs the PCC policy with the Tv updating enters in a deadlock state. In detail, for small M values, it may happen that during a run all the stations give up due the price announced by the access point. In this case, a virtual transmission interval never ends (there are no successful transmissions), and hence no new price announcement will occur. This is the reason of the very wide error-bars that appear in Figure 4 associated to Tv plots.

The deadlock problem cannot occur with the Tp updating policy, and hence in this case the error-bars are always very small.

Mixed-packets

In the previous section we assumed a traffic made of long messages only. As shown by TCP-traffic studies [Ste 94], on a byte count basis, 90% of the traffic is made up of maximum size packets while the remaining 10% consists of very short packets. This means that, on a packet-count basis about 50% of the packets are long messages (up to 1500 bytes), and the remaining 50% are short packets 40-byte long. Hence, in a more realistic environment the message length distribution should be bimodal. For this reason, hereafter we evaluate our system by assuming a mixed distribution of the packet lengths. In detail, we assume 50% long messages and 50% short messages. Short messages have a 2-slot constant length (about 40 bytes of payload). The length of long messages is sampled from the same normal distribution used in Section 4.1. the PCC policy is effective when the network congestion increases; ii)

the Tv and Tp updating policies have the same asymptotic (with respect to M) behavior; iii) the Tp policy is always deadlock free, while the Tv policy may produce deadlocks both in the saturated, and in the not-saturated conditions. These events are highlighted by wide error-bars on the Tv plots and correspond to deadlocks occurred in some simulative runs.

Conclusions

In this paper we proposed and evaluated a Price-based Congestion Control (PCC) policy that can be applied to dynamically control the network contention level in a Wi-Fi hot spot. The basic idea is to control the traffic inside the hot spot by determining the access cost as a function of the current load in the hot spot. By increasing/decreasing the perpacket transmission cost, the hot spot operator encourages/discourages her/his customers. In the paper we developed a theoretical framework to compute the access cost to maintain the hot spot in its optimal operating point, for any load condition. Via simulation, we evaluated the performance of a Wi-Fi hot spot with or without the PCC policy. The performance analysis was carried out both in saturated and not-saturated conditions. Results obtained show that the PCC policy is effective for all the network and traffic configurations analyzed. In detail, we considered two implementations of PCC depending on the event that triggers the notification of the new price to the users: periodic and virtual-transmissiontime updating. The results show that the periodic updating policy is robust while the virtual-transmission-time updating may generate deadlock conditions. Several assumptions used in our implementation of the PCC policy may be considered unrealistic (e.g., detailed knowledge of the channel status in terms of idle and collision periods) or too complex (e.g., the per-packet transmission cost) for a real setting. It is worth pointing out that the main scope of this paper is to demonstrate the feasibility of a price-based policy for congestion control in a Wi-Fi hot spot. In this sense, our results constitute a theoretical foundation for price-based congestion control in Wi-Fi networks. The definition of a realistic implementation of a PCC policy is beyond the scope of this paper and it represents the next step of this research activity.

Figure 1 :

 1 Figure 1: Structure of a virtual transmission time By exploiting the analytical tractability of the p-persistent IEEE 802.11 the following property, relevant for defining our congestion pricing policy, was proved ([CG02], [BCG02]):

Figure 4 :

 4 Figure 3: not saturated (long packets)

Figure 6 :

 6 Figure 5: not-saturated scenario (mixed traffic)

Table 1 . IEEE 802.11b parameter values.

 1 The behavior of a IEEE 802.11 network can be closely approximated by an equivalent p-persistent IEEE 802.11 protocol [CCG00]. A p-persistent IEEE 802.11 protocol differs from the standard protocol only in the selection of the backoff interval. Instead of the binary exponential backoff used in the standard, the backoff interval of the p-persistent IEEE 802.11 protocol is sampled from a geometric distribution with parameter p.

	Slot Time _	τ	MAC hdr	CRC	Bit Rate(Mbps)
	t slot
	20 µsec	1 µsec 240 bits (2.4 t slot )	32 bits (0.32 t slot )	1, 2, 5.5, 11
	DIFS	SIFS	ACK	CW MIN	CW MAX
	50 µsec	10 µsec	112 bits	32 t slot	1024 t slot
	2.1 Wi-Fi Modeling

It is worth noting that, hereafter, the channel idle period that follows a collision (at least a DIFS), and the SIFS, ACK and DIFS intervals that follow a successful transmission are counted as overheads associated to a collision or to a successful transmission.

The new M value will of course influence the future average backoff window (and hence the p value), hereafter we assume that the impact of the M change on p is negligible. The accuracy of this assumption increases with the increase of the M value.

This number includes also the stations that reconnect after a give-up period.

This research is partially supported by the Province of Trento (Italy) in the framework of the WILMA (Wireless Internet and Location Management) project (http://www.wilmaproject.org/)


Benyuan Liu

Don Towsley

On the Coverage and Detectability of Large-scale Wireless Sensor Networks

I. INTRODUCTION

Advances in sensor and communication technologies have made it possible to manufacture small sensors with sensing, processing, and wireless communication capabilities in a costeffective fashion. A sensor network can be formed by deploying specialized sensors in the region of interest to perform certain sensing and networking tasks. Application scenarios of wireless sensor networks include battlefield surveillance, environment monitoring, and etc. Many of the above application scenarios involve a large number of sensors deployed in a vast geographical area.

Coverage and detectability are two fundamental measures of the performance of a sensor network. In general, sensing coverage represents how well an area is monitored by sensors; and detectability represents the capability that a sensor network detects an object that moves through the network. Formal definitions of the coverage and detectability will be introduced shortly. Characterizations of these two measures present important implications to protocol design and performance of sensor networks.

While most of previous related work on the sensor network coverage and detectability focuses on protocol design [START_REF] Tian | A coverage-preserving node scheduling scheme for large wireless sensor networks[END_REF][2][3][4] [START_REF] Ye | Energy efficient robust sensing coverage in large sensor networks[END_REF], the goal of our work is to define and characterize the coverage and detectability, and examine the implications of the results. To represent the coverage and detectability of a sensor network, we define the following quantities.

Area coverage ( f a ): the fraction of the geographical area that is in the sensing area of one or more sensors. The sensing area of a sensor is the area within which the sensor can provide a valid sensing measurement. This is usually represented by a circle centered at the sensor with a radius of the sensor's sensing range.

Node coverage fraction ( f n ): the fraction of sensors whose sensing areas are fully covered by collections of other sensors. This quantity represents the redundancy level of sensors from a coverage perspective. It has a direct effect on the performance of energy-efficient protocols which turn off redundant sensors while preserving area coverage [START_REF] Tian | A coverage-preserving node scheduling scheme for large wireless sensor networks[END_REF].

Detectability (p d ): the probability that no path exists for an object to penetrate a large-scale sensor network from left to right or from top to bottom without being detected. An object is detected by a sensor if it enters the sensing area of the sensor. We consider the worst-case scenario for sensor networks and assume that an object can take arbitrary paths. This research has been supported in part by NSF under awards ANI-9809332, EIA 0080119, and NSF ITR-0085848.

A penetrating path without being detected should not intersect the sensing areas of any sensors. Detectability of a sensor network is of interest in application scenarios such as soldiers crossing a battlefield in military operations and animal tracking in environment monitoring.

In this work, we consider grid-based sensor networks where sensors are deployed in a square lattice and random sensor networks where sensors are deployed at random locations in a field. We characterize the asymptotic behaviors of the coverage and detectability of sensor networks. Consequently, the requirements of the sensor density to achieve a target area coverage can be derived. While grid-based sensor networks provide efficient area coverage, random networks offer robustness and reliability upon sensor failures at the cost of coverage redundancy. For a random sensor network, we observe that only a small fraction of sensors are covered by other sensors when the density is not high enough. We show that the detectability of a 2-dimensional large scale sensor network exhibits a phase transition at a critical sensor density. Below the critical density, a penetrating path that will not be detected exists almost surely. Above the critical density, the network can detect any crossing object almost surely. Therefore, in order to effectively detect any crossing object, sensors should be deployed at a density higher than the critical value.

II. GRID-BASED SENSOR NETWORKS

In this section, we study the coverage and detectability of grid-based sensor networks. The whole network is divided into a large array of squares, as shown in Fig. 1. Each square has a side length of D. In this model, sensors can only be located at the center of each square. A square is occupied if there is a sensor located at the center. Every sensor has a finite sensing range, within which it can provide reliable sensing measurements. We assume that all the sensors are homogeneous, i.e, they have the same sensing range r. The simple grid-based model has often been used in research [START_REF] Servetto | Constrained random walks on random graphs: Routing algorithms for large scale wireless sensor network[END_REF] [START_REF] Kleinberg | The Small-World Phenomenon: An Algorithmic Perspective[END_REF] to obtain closed-form results and provide insights to more general scenarios.

For the deployment of the sensors, we assume that the occupations of the squares follow a spatial Bernoulli process with probability p. An empty square represents one of the following scenarios: (i) no sensor is deployed in the square (ii) the sensor located in the square fails (iii) the sensor located in the square is turned off due to protocol operations. We now present results for r D¡ 2 and r ¢ D¡ 2, respectively.

1. r D¡ 2: A square is occupied with probability p, with each sensor covering an area of πr 2 . We have

f a ¢ pπr 2 ¡ D 2 .
In this case, a location is covered by at most one sensor node. There is no overlap between any two sensor nodes. Therefore, f n ¢ 0.

Since r D¡ 2, no grid line is in the sensing area of any sensor. An object moving on grid lines will not be detected by sensors. Therefore, there always exists a path along which an object can cross the sensor network without being detected. Thus, P d ¢ 0.

2. r ¢ D¡ 2 In this case, area coverage ( f a ) and node coverage ( f n ) exhibit the same behavior as in the case r D¡ 2. However, detectability of the network exhibits different behaviors.

Two squares are called nearest neighbors if they have one side in common but not if they only touch at one corner. Since r ¢ D¡ 2, an object cannot pass through two nearest occupied neighbors without being detected. A cluster is defined to be a group of neighboring occupied squares. In order not to be detected, an object cannot pass through a cluster but should move around the perimeter of the cluster.

The detectability of a sensor network can be related to the percolation of the sensors in the network. According to percolation theory [START_REF] Stauffer | Introduction to Percolation Theory[END_REF], there exists a critical threshold p c , where a phase transition occurs with respect to the size of the largest cluster.

More specifically, when the probability is above the threshold (p p c ), there exists a unique unbounded cluster almost surely. The unbounded cluster extends from top to bottom and from left to right. Therefore, an object cannot penetrate the network without being detected.

When the probability is below the threshold (p p c ), all clusters are bounded almost surely. In this case, there always exists a path along which an object can penetrate the network without being detected. Otherwise, there must be a unbounded cluster percolating through the network, contradicting the assumption. Therefore,

P d ¢ ¡ 0 a.s. if p p c 1 a.s. if p p c ( 1
)
where p c ¢ 0¢ 5928 [START_REF] Stauffer | Introduction to Percolation Theory[END_REF]. Note that because of the "zero-one" law of the phase transition, the detectability cannot be anything other than 0 or 1.

III. RANDOM SENSOR NETWORKS

In this section, we study the coverage and detectability of large scale random sensor networks, where sensors are randomly distributed in a vast geographical area. In this case, the locations of sensors are described by a stationary Poisson point process. Therefore, a random sensor network can be described by a Poisson Boolean model B£ λ¤ r¥ , where r represents the common sensing range of the sensors and λ represents the density of the underlying Poisson point process.

A. One-dimensional case

In the one-dimensional straight-line scenario, sensors are randomly placed on a straight line, each covering a segment of length 2r. In this case, the area coverage refers to the fraction of the line that is covered by one or more sensors. Using the well-known covered volume fraction result in stochastic geometry, we can obtain f a ¢ 1 ¦ e § 2λr .

In sensor network planning, a designer may want to determine the minimum density required in order to achieve a target area coverage. Using the above area coverage result, we can derive the required sensor density in order to achieve a desired area coverage f a , λ ¢ ¨¦ ln£ 1 ¦ f a ¥ ¡ 2r.

A sensor is covered if its sensing area is covered by other sensors; and the sufficient and necessary condition is that the distance between its immediate left and right neighbors is smaller than 2r. Since the distance follows a 2-nd order Erlang distribution, the node coverage is

f n ¢ 1 ¦ e § 2λr ¦ 2λre § 2λr (2)
On an one-dimensional line, there is no location that an object can cross without being detected if the distances between adjacent sensors are all smaller than 2r. There is an infinite number of sensors on an one-dimensional straight line, the detectability can be computed as follows:

P d ¢ lim n© ∞ £ 1 ¦ e § 2λr ¥ n ¢ 0 (3)

B. Two-dimensional infinite plane case

For a random point in the two-dimensional plane, denote the number of sensors covering the location as N. The random variable N follows a Poisson distribution with parameter λπr 2 , i.e., P£ N ¢ n¥ ¢ e § λπr 2 £ λπr 2 ¥ k ¡ k!; and the area coverage is

f a ¢ 1 ¦ e § λπr 2 .
In order to achieve a desired area coverage f a (0 f a 1) almost surely, the node density should be λ

¢ ¦ ln£ 1 ¦ f a ¥ ¡ πr 2 .
Figure 2 depicts the analytical (the curve) and simulation results (the points) of the area coverage as a function of node density. In the simulation, we approximated an infinite plane by a domain of 10000 x 10000 pixels. The density of the sensor nodes is measured in pixels § 2 . The sensing range of each sensor is set to be 10 pixels. From the figure we observe that the simulation results agree with the analytical results very well. Note that in random sensor networks, a location may be covered by several sensors. The expected number of sensors covering any random location is simply λπr 2 . This makes the sensor network more robust and reliable upon sensor failures. Of course, the robustness and reliability are achieved at the cost of the redundancy of the sensors. Figure 3 shows the simulation results of node coverage ( f n ) as a function of node density. We observe that node coverage remains below 1% until the density of the sensor nodes increases to a very high value, 2 10 § 3 . At this density, 47% of the whole area is covered by sensors. To provide a visual illustration of the area coverage and node coverage at this density, we illustrate part of the network in Figure 4. This part is randomly chosen within the domain and contains a large number of sensors, it is representative of the whole network. In the illustration, each sensor is represented by a circle with a radius of the common sensing ranging, while filled circles represent those sensors whose sensing areas are fully covered by other sensors. We observe that the density is quite high and sensors that are covered by other sensors are sparsely distributed in the network. This result suggests that in scenarios where sensors cannot be deployed at a high density due to cost or other reasons, the fraction of nodes that can be turned off without reducing the area coverage is small.

In the same token as for a two-dimensional grid-based sensor network, the detectability of a two-dimensional random sensor network can be related to the continuum percolation [START_REF] Meester | Continuum percolation[END_REF] of the sensors. There is a critical density λ c at which an unbounded occupied cluster emerges. Below the critical density λ c , all clusters are almost surely finite in size. An object can penetrate the network by moving between the boundaries of the clusters. Above the critical density λ c , an unbounded occupied sensor cluster percolates the whole network, which will detect any object trying to cross the network. Therefore,

P d ¢ ¡ 0 a.s. if λ λ c 1 a.s. if λ λ c ( 4
)
The critical density (λ c ) depends on the sensing range of the sensors and can be obtained using simulation.

IV. CONCLUSIONS

We characterize the asymptotic behaviors of the coverage and detectability of large-scale sensor networks. We also studied a number of other issues, for example, coverage and detectability of a 2-dimensional finite-width strip sensor network, probability and algorithm to find a path between two random locations without being detected, and etc. The results are not presented here due to space limitations.

Fig. 1 .

 1 Fig. 1. A gird-bases sensor network

Fig. 2 .Fig. 3 .

 23 Fig. 2. Area coverage as a function of node density

Fig. 4 .

 4 Fig. 4. Part of the sensor network at node density of 2 ¡ 10¢ 3