Rodrigo T Saad
email: rsaad@laas.fr

Silvano Dal

Bernard Berthomieu
email: bernard.berthomieu@laas.fr

An Experiment on Parallel Model Checking of a CTL Fragment

We propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, multi-core architectures. This model-checking algorithm takes benefit from a parallel state space construction algorithm, which we described in a previous work, and shares the same basic set of principles: there are no assumptions on the models that can be analyzed; no restrictions on the way states are distributed; and no restrictions on the way work is shared among processors. We evaluate the performance of different versions of our algorithm and compare our results with those obtained using other parallel model checking tools. One of the most novel contributions of this work is to study a space-efficient variant for CTL model-checking that does not require to store the whole transition graph but that operates, instead, on a reverse spanning tree.

Introduction

Several model-checking methods address the state-explosion problem from a purely algorithmic perspective, for instance with the use of abstractions on the set of states (such as stubborn sets or symmetries) or symbolic techniques. Despite the fact that considerable progress has been made at the theoretical level, there are still classes of systems that cannot benefit from these advanced methods, like for example models that rely on real time constraints or on dynamic priorities. In this case, it is interesting to take benefit from the computation power-and increased amount of primary memory-provided by multi-processor and multi-core computers in order to handle very large state spaces.

In this paper, we propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, multi-core architectures. We target shared-memory computers with a moderate number of cores (say 4 to 64) operating on a large shared memory space (typically from 16GB to 1TB of RAM). This description fits many available mid-range servers, but is also quite close to tomorrow's mainstream desktop computers.

Our model-checking algorithm takes benefit from a parallel state space construction algorithm defined in a previous work [START_REF] Saad | Mixed Shared-Distributed hash tables approaches for parallel state space construction[END_REF] and share the same principles.

First, we make no specific assumptions on the models that can be analyzed (we only assume that we know how to compute the successors of a given state and test them for equality). Second, we put no restrictions on the way states are distributed: in our solution, every process keeps a local share of the global state space and we do not rely on an a-priori static partition of the states. Finally, we put no restrictions on the way work is shared among processors; this means that our algorithm plays nicely with traditional work-sharing techniques, such as work-stealing or stack-slicing.

In this paper, we extend this state space construction algorithm by adding model checking capabilities. While the leading parallel model-checking tools are based on LTL model-checking, (see Sect. 5) we advocate the use of CTL. The choice of CTL derives from a number of desirable properties that we want for our parallel algorithm.

First, it must take advantage of parallelism and be compatible with our parallel state space generator. For this reason, the logic should preferably be branching time rather than linear time since model checking algorithms for linear time logics are strongly tied to depth-first-search (dfs) exploration techniques; and that dfs algorithms are "inherently sequential" (they belong to the class of P-complete problems [START_REF] Reif | Depth-first search is inherently sequential[END_REF][START_REF] Raymond Greenlaw | Limits to Parallel Computation: P-Completeness Theory[END_REF]). Parallel techniques for LTL model checking have been quite investigated however [START_REF] Barnat | DiVinE: Parallel Distributed Model Checker[END_REF][START_REF] Laarman | Multi-Core nested Depth-First search[END_REF] so we will compare our approach with these.

Secondly, we want an on-the-fly algorithm; only states essential for answering the model-checking problem should be enumerated. For this reason, model checking should be local rather than global; properties will be interpreted at the initial state rather than at all states.

Next, because the full state space may have to be enumerated (e.g. when checking a property that is true), we want it to be space-efficient. Hence, we shall accept that a small amount of information is recomputed every time it is needed rather than kept in storage.

For all these reasons, we decided to select a fragment of Computation Tree Logic (CTL) with state subformulas restricted to atomic propositions. This fragment strictly includes the logic used by popular tools like Uppaal. Though obviously less expressive than CTL, it implements a good trade-off between expressiveness and cost of verification when used to check large state spaces.

While not yet implemented in our tool, it is possible to adapt our algorithm to model-check full CTL; more expressive logics will be considered in further work.

Contributions. We follow the classical approach of Clarke and Emerson [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF] for CTL model-checking. During model-checking, we label each state of the system with the subformulas that are true at this given state. Labels are computed iteratively until we reach a fix-point, that is until we cannot add new labels. We consider two variants of this algorithm that differ by the amount of information on the transition relation that is stored. Both variants have two passes: a forward pass performs a constrained exploration of the state graph in which we start labeling each state with local information; a second, backward pass, propagates information towards the root of the state graph and checks if the resulting graph admits an infinite path.

In the first version of the algorithm, that we call RG (for reverse graph), we assume that, for every reachable state, we have a constant time access to the list of all its "parents". In other words, we store the reverse transition relation of the state space. Algorithm RG is simply a parallel version of the algorithm in [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF] that uses our parallel state space construction method. Our experimental results show that, even with this simple approach, we obtain a very good parallel implementation (that is with a good speedup) and a very good model-checking tool (that is with a good execution time when compared with other tools on a similar setup).

In the second version, we assume that we have direct access to only one of the parents, meaning that we may have to recompute some transitions dynamically. We call this second version RPG, for reverse parental graph. The advantage of the RPG version is to save memory space. Indeed, if we use the symbol S to denote the number of reachable states, the RG algorithm as a space complexity in the order of O(S 2 ) in the worst-case, while it is of the order of O(S) for the RPG version. We show, in our benchmarks, that the RPG version allows to compute bigger examples without sacrificing execution time.

Outline of the paper. In the next section, we summarize the parallel state space generation algorithm [START_REF] Saad | Mixed Shared-Distributed hash tables approaches for parallel state space construction[END_REF] that is used in our work. The model checking algorithms are defined in Sect. 3 using pseudo-code, while our parallel implementation is described in Sect. 4. Before concluding, we discuss the related work and compare our performances with the DiVinE [START_REF] Barnat | DiVinE: Parallel Distributed Model Checker[END_REF] tool, a state of the art parallel model checker for LTL.

Parallel State Space Generation

State space generation is often a preliminary step for model checking behavioral formulas. This is a very basic operation: take a state that has not been explored; compute its successors and check if they have already been found before; iterate until there is no more new state to explore. Hence, a key point for performance is to use an efficient data structure for storing the set of generated states and for testing membership in this set. In [START_REF] Saad | Mixed Shared-Distributed hash tables approaches for parallel state space construction[END_REF], we propose an algorithm for parallel state space construction based on an original concurrent data structure, called a localization table (LT ), that aims at improving spatial and temporal balance.

This approach is close in spirit to algorithms based on distributed hash tables, with the distinction that states are dynamically assigned to processors; i.e. we do not rely on an a-priori static partition of the state space. In our solution, every process keeps a share of the global state space in a local data structure. Data distribution and coordination between processes is made through the LT , that is a lockless, thread-safe data structure. The localization table is used to dynamically assign newly discovered states and can be queried to return the identity of the processor that owns a given state. With this approach, we are able to consolidate a network of local state repositories into an (abstract) distributed one without sacrificing memory affinity-data that are "logically connected" and physically close to each other-and without incurring performance costs associated to the use of locks to ensure data consistency.

The performance of our state space construction algorithm was evaluated on different benchmarks and compared with the results obtained using other solutions proposed in the literature. A first implementation of our algorithm showed promising results as we observed performances that are consistently better-both in terms of absolute speedup and memory footprint-than with other parallel algorithms. For example, this algorithm does consistently better than algorithms based on the use of static partitioning or than a similar approach based on the concurrent hash map implementation provided in the Intel Threading Building Blocks (TBB) library.

State space generation has a direct impact on the performance of the modelchecking algorithm. For one thing, state space generation alone is enough to model-check reachability properties (of the form A2(φ)). Moreover, for more complicated properties (see our benchmark results in Sect. 4), the time needed to explore the state space still makes up a big part of the model checking time.

Parallel Model Checking for a CTL Fragment

We build our model checking algorithm on top of the parallel state space generation algorithm of [START_REF] Saad | Mixed Shared-Distributed hash tables approaches for parallel state space construction[END_REF], described in the previous section. Our other design choices follow from our goal to target models with very large state spaces. More particularly, we choose to restrict ourselves to a fragment of CTL and to disallow the nesting of operators; that is, every subformula-denoted φ, ψ, . . . -is a (boolean composition of) atomic propositions.

The logic used for model-checking essentially relies on three operators: Exist Until (EU), E (ψ ∪ φ), that is true if there exists a trace (a path) in the state space such that ψ has to hold until, at some position, φ holds; Always Until (AU), A (ψ ∪ φ), that is true if the "until condition" holds on every trace; and finally the leadsto formula, ψ ; φ, that is true if, for every trace, whenever ψ holds then necessarily φ will hold later. The last property can be expressed as A2(¬ ψ ∨ A3(φ)) in CTL. From the interpretation given in Table 1, we see that these operators define an expressive fragment of CTL (and also LTL).

Model-checking procedures for these operators will be described in Sections 3.2 to 3.4. In our implementation, we consider two variants-RG and RPG-of the algorithms. Both versions are based on two elementary phases: (1) a forward constrained exploration of the state graph using the state space construction discussed in Sect 2; followed by (2) a backward traversal and label propagation phase ensuring that the resulting graph is acyclic.

The backward traversal phase is only needed for AU and leadsto formulas, since checking EU formulas amounts to performing a constrained exploration of the state space (for instance, the formula A2(φ) is true if no state satisfies ¬φ, which can be checked during the exploration phase). Consequently, our algorithm is not completely on-the-fly for these cases because the presence of a cycle is detected after the (constrained) state space is constructed, delaying the discovery of an invalid path. The last column of Table 1 indicates, for each formula, whether the backward phase is necessary.

Formulas Interpretation in CTL Forward Backward E (ψ ∪ φ) E (ψ ∪ φ) x A (ψ ∪ φ) A (ψ ∪ φ) x x E3(φ) E (True ∪ φ) x A3(φ) A (True ∪ φ) x x E2(φ) ¬A3(¬φ) x x A2(φ) ¬E3(¬φ) x ψ φ A2(¬ψ ∨ A3φ) x x A2A3(φ) true φ x x
Fig. 1. List of Supported Formulas.

Concepts and Notations

We assume that we perform model-checking on a Kripke System KS (S, R, s 0 ). We will use, interchangeably, the notation KS for the Kripke structure (S, R, s 0 ) and G for the directed graph G(S, R), also called the state graph. In the RPG version of our algorithm, we make use of the Parental Graph of a Kripke System, that is a reverse spanning tree of the (currently computed) state graph.

Definition 1 (Parental Graph). The directed graph, P G(V p , E p ), is a parental graph of G(V, E) if: (1) P G if a subgraph of G that has the same vertices, that is V p = V and E p ⊆ E, and (2) for every vertex v ∈ V , if v is not the root of G then v has an in-degree of one in P G.

A simple way to obtain a parental graph, P G, when exploring the state graph, G, is to keep for every state, s, a vertex to the state in G that was used to generate s (and forget the others). The parental graph has nice properties. If P G is a parental graph of G and G is acyclic then so is P G. Moreover, the set of leaves of P G subsumes that of G; a leaf of G is necessarily a leaf of P G.

In the remainder of the text, the expression |S| is used to denote the cardinality of S (the number of reachable states), while |R| is the number of transitions. We assume that every state s ∈ S is labeled with a value, denoted suc(s), that records the out-degree of s in KS . The value of suc(s) is set during the forward exploration phase. Initially, suc(s) is the cardinality of the set of successors of s in KS , that is suc(s) = |{s | s R s }|. We decrement this label during the backward traversal of the state graph; when the value of suc(s) reaches zero, we say that s is cleared from the state graph. In our pseudo-code, we use the expression suc(s).dec() to decrement the value of the label suc for the state s in KS , and the expression suc(s).set(i) to set the label of s to some integer value i.

When we deal with the reverse parental graph version of our algorithm, we assume that we implicitly work with one particular parental graph of KS , denoted PKS . In this case, we assume that every state s ∈ S is also labeled with a value, denoted sons(s), that records the out-degree of s in KS . We also label each state s ∈ S with a state, denoted father(s), that is the (unique) predecessor of s in PKS . (The label father(s) makes sense only if s is not the initial state, s 0 , of KS .) Initially, the value of sons(s) is set to zero. The label will be incremented during the forward exploration, when we build PKS (that is, we select the transitions from KS that will be stored in PKS ). This operation is denoted sons(s).inc() in our pseudo-code. We will decrement the value of sons(s) during the backward traversal phase.

Checking EU properties

Checking EU properties for the initial state is standard, except that we perform the forward phase concurrently, on all states. this can be done on the fly in a single, forward pass. To check the formula E (ψ ∪ φ), we explore the state space until a state is found such that either (1) φ holds and no more state has to be explored, or (2) ¬ψ ∧ ¬φ holds. In the first case, the algorithm reports success; all states obeying φ terminate a (possibly empty) path of states rooted at the initial state and all obeying ψ. In the second case, we have found a counterexample; a state obeying neither ψ nor φ, meaning that the property is false at the initial state. The check function is the same for the two versions of our algorithm, whether based on the reverse graph or the reverse parental graph data structure.

Checking AU Properties

For checking the formula A (ψ∪φ), as for EU properties, we stop exploring a path when we find a state such that (1) φ holds or (2) ¬ψ ∧ ¬φ holds. If an occurrence of case (2) is found, we have a counter-example to the property false. Otherwise, we start backward traversal phase in order to detect cycles. Indeed, the property A (ψ ∪ φ) is false if there is an infinite path of states (starting from s 0 ) that all obey ψ. We call this second phase the clearing phase, because it consists in recursively removing leaf nodes from the graph. This process ends either when the only remaining state is the initial state (meaning that the property is true), or when no states with out-degree zero can be found (in which case we know that there is a cycle). The validity of this method follows from the fact that a finite Directed Acyclic Graph (DAG) has at least one leaf.

We give the pseudo-code for checking A (ψ ∪ φ) in Listing 1.1. The inputs are the atomic properties ψ and φ and the initial state s 0 . The algorithm makes use of a stack A to collect the states at which φ holds during the forward exploration phase. The procedure uses two auxiliary functions, forward check a and backward check a, that depends on the version of the algorithm. We start by defining these helper functions for the Reverse Graph version.

Algorithm for the Reverse Graph version (RG). We give the pseudo-code for the function forward check a (for the RG version) in Listing 1.2. The last parameter of this function, A, is a stack that is used to collect the leaf nodes of the state graph, that is the states where φ holds. These states are the starting points in our backward traversal of the graph.

During the forward exploration phase (function forward check a) each state s is labelled with its number of successors in the initial state graph (the Kripke structure). During the backward traversal phase (function backward check a), this label is decremented each time a successor of s is removed; decrementations are done in parallel. Intuitively, a state can be removed as soon as it is cleared. We never actually remove a state from the graph. Instead, when a processor changes the label of a state s to 0, we also decrement the labels of all the parents of s in the graph. Hence the choice of storing the reverse of the transition function in the data structure.

In the function backward check a, see Listing 1.2, we start by clearing all the states in A which are, by construction, the states s such that suc(s) is nil. When a state is cleared, we decrement the labels of all its parents (suc(s ).dec()) and check which ones can be cleared (suc(s ) == 0). The algorithm stops if the initial state, s 0 , can be cleared or if there are no more states to update. Algorithm for the Reverse Parental Graph version (RPG). The function for the RPG version is only slightly more complicated, because we need to recompute some successors in the transition relation: we can only access one of the parents of a state in constant time (which we call the father of the state). The pseudo-code for the forward exploration phase (function forward check a) is essentially the same as in Listing 1.2; this is why it is omitted here. Compared to the RG version, we only need to add two additional statements when adding a new state (around line 15 in Listing 1.2): assuming that the state s is generated from a state s , we set the value of the father for the newly generated state (f ather(s).set(s )) and increment the number of sons of the father sons(s).inc()). This information is used during the backward traversal to track non cleared leaves.

We give the pseudo-code for the backward traversal phase in Listing 1.3. During this phase, we follow the parental graph structure to "propagate" the cleared states toward the root of the state graph. The algorithm alternates between two behaviors, clearing and collecting. The clearing behavior is similar to the pseudo-code for the RG algorithm, with the difference that we decrement only the father of a state and not all the predecessors. When there are no more labels to decrement-and if the root state is not yet cleared-the algorithm starts looking for states that can be cleared. For this, we test all the states s such that sons(s) == 0; that is, such that all the sons of s have been cleared (in the parental graph). In this case, to check if s can be cleared, we have to recompute all its successors in KS and check whether they have also been cleared (if their suc label is zero). The advantage of this strategy is that we do not have to consider all the states in the graph but just a subset of them. Indeed, we know that if KS is a acyclic (is a DAG) then P G has at least one leaf that is also a leaf in G [START_REF] Saad | Parallel Model Checking for Multiprocessor Architecture[END_REF]. Hence, this subset is enough to test the presence of a cycle. Conversely, the drawback of this approach is that we may try to clear the same vertex several times, which may be time consuming.

Checking Leadsto Properties

To check the formula ψ φ, we need to prove that no cycle can be reached from a state where ψ holds, without first reaching a state where φ holds. Indeed, otherwise, we can find an infinite path where φ never holds after an occurrence of ψ. Figure 2 shows an example of graph for which the formula is valid. This observation underlines the link between checking the formula ψ φ locallyfor the initial state-and checking the validity of A3(φ) globally-at every state where ψ holds. As a consequence, we can use an approach similar to the one used for AU properties in the previous section. The main difference is that, instead of clearing the initial state, we have to clear all the states where ψ holds. Hence, the pseudo-code for the leadsto formulas is similar to that of AU formulas (this is why it is omitted here), the main difference is in the termination condition: the function returns true if all the states where ψ holds are cleared.

Correctness and Complexity of our Algorithms

Proofs of correctness (termination, completeness and soundness) and a precise study of the complexity of our algorithms can be found in [START_REF] Saad | Parallel Model Checking for Multiprocessor Architecture[END_REF]. We just discuss here the worst-case complexity in the sequential case, and for formulas A (ψ ∪φ). The results for this case can be generalized to our whole logic. (Inside asymptotic notations, we use the symbols S and R when we really mean |S| and |R|.)

The algorithm given in Sect. 3.3 may inspect every state in the Kripke Structure KS and, for every transition, it may update one label. Therefore, its worstcase time complexity is in the order of O(S + R) for the RG algorithm. The complexity is higher in the RPG version since, for each altered state, we may have to recompute the successors for all the reachable states s such that sons(s) is nil. Hence, solving a simple recurrence, we can prove that the time complexity is in the order of O(S • (R -S)) for the RPG version. Since the number of transitions in KS is bounded by |S| 2 , we obtain a complexity in the order of O(S 2 ) for the RG version and of O(S 3 ) for the RPG variant. Concerning the space complexity, the RPG version is in the order of O(S), while the RG version is linear in the size of the graph, that is in the order of O(S + R) (or O(S 2 )).

We show in our experiments that the decision to favor "space-efficiency" (in the case of the RPG version) is quite interesting. In particular, on some examples, the RPG version may run faster than the RG version because it needs to "write less information" in main memory, an effect that is not visible if we only look at the theoretical complexity. More importantly, memory is one of the key resources used during model-checking. Indeed, it is common to exhaust the available memory during verification.

In the code presented in Sect. 3, no underlying computational model was make precise. The code can be easily adapted to a Parallel RAM model, following a Single Program Multiple Data (SPMD) programming style. In this section, we discuss the details surrounding the parallel implementation of our algorithms, then report on a set of experiments performed to evaluate their effectiveness.

Parallel Implementation of our Algorithm

In a SPMD context, all processing units will execute the same functions (the one defined in Listings 1.1-1.3). Following this approach, the (forward) exploration phase and the (backward) cycle detection phase can both be easily parallelized. Then, for the model-checking function themselves-for instance the function check a-we only need to synchronize the termination of the forward exploration with the start of the backward label propagation. At each point, a processing unit can terminate the model-checking process if it can prove (or disprove) the validity of the formula before the end of the exploration phase. Actually, most of the burden of parallelizing our algorithm is hidden inside the use of our specialized, lock-free data structures.

We consider a shared memory architecture where all processing units share the state space (using the mixed approach presented in [START_REF] Saad | Mixed Shared-Distributed hash tables approaches for parallel state space construction[END_REF]) and where the working stacks are partially distributed (such as the stacks W and A used in our pseudo-code). For most of our pseudo-code, it is enough to rely on atomic compare and swap primitives to protect from parallel data races and other synchronization issues; typically, compare-and-swap primitives will be used when we need to test the value of a label or when we need to update the label of a state (for instance with expressions like sons(s).dec()). Together with the compareand-swap primitive, we use our combination of distributed, local hash tables with a concurrent localization table to store and manage the state space.

For the RG version of the algorithm, we can ensure the consistency of our algorithm by protecting all the operations that manipulate a state label. (We made sure, in our pseudo-code, that every operation only affects one state at a time.) The parallel version of RPG is a bit more involved. This problem is related to the behavior of the collecting operations of the backward exploration (see the comment on line 14 of Listing 1.3)-and in particular the function testthat needs to check all the successors of a state to see if they are cleared. First, this code is not atomic and it is not practical to put it inside a critical section (it would require a mutex for every state). If two processors collect the same state, then the father of this state could be decremented twice, during the clearing operations. Second, collecting must be performed after all processors have finished the clearing operations, otherwise the algorithm may end prematurely (see [START_REF] Saad | Parallel Model Checking for Multiprocessor Architecture[END_REF] for a complete explanation.) We solve the concurrency issues for the RPG version through the synchronization of all processors before both clearing and collecting. Then, we take advantage of our distributed local state repositories to avoid problems due to concurrent access; each processor can perform the collecting operations only over the states that it owns. Finally, we use a work-stealing strategy (see [START_REF] Saad | Mixed Shared-Distributed hash tables approaches for parallel state space construction[END_REF]) to balance the work-load between the different phases of our algorithm; for instance, whenever a thread has no more state to clear, it tries to "steal" non-cleared states from other processors.

Experimental Results

We have implemented the parallel versions of our model-checking algorithm and evaluated their performances on several benchmarks. Experimental results presented in this section were obtained on a Sun Fire x4600 M2 Server configured with 8 dual core opteron processors and 208 GB of RAM memory, running the Solaris 10 operating system. (The complete set of experiments can be found in [START_REF] Saad | Parallel Model Checking for Multiprocessor Architecture[END_REF].) We give results obtained on 8 classical models-a Token Ring protocol; the Peg-Solitaire board-game; . . . -with a mix of valid and invalid properties. We experimented with all the formulas: reachability (E3φ), safety (A2φ and E2φ), liveness (A3φ) and leadsto (ψ φ).

Speedup Analysis: we study the relative speedup and the execution time for our algorithms. In addition, we also give the separate speedup obtained in each phase of the algorithm-during the exploration (forward) and cycle detection (backward) phases-in order to better analyze the advantages of our approach. Figure 3 shows speedup analysis for the RPG version of our algorithm. We only show the results for two models-a Token Ring with 22 bases (TK22) and a Solitaire game with 33 pegs-since they are representative of the results obtained with our complete benchmark. These models have different execution profiles which impacts significantly the overall performance. The main difference is the time spent in the backward traversal phase. Figure 4 shows a series of bar charts putting in evidence the time required for each phase of the algorithm (exploration and cycle detection). In addition, we compare our approach (RG and RPG) with a third algorithm (NO GRAPH) that uses the same code as RG but recomputes predecessor states instead of storing them (this is possible only because, for this particular benchmark, we know how to compute the predecessors of a state). We have observed two main categories of behaviors in this analysis. negligible backward traversal: the time spent in the backward exploration phase is negligible compared to the overall execution time (e.g. model TK22 in Fig. 3,4). This is the case, for instance, if the property is false and the cycle detection phase terminates early. In this category of experiments, there are no significant differences between RG and RPG, mainly because the gain in performance during the forward exploration phase outweighs the extra work performed during the cycle detection phase; complete backward traversal: the cycle detection phase needs to run through all the state space (e.g. model SOLITAIRE in Fig. 3,4). We observe a significant difference in performance between the RG and RPG versions in this case. The extra work performed by the RPG version becomes the dominant factor.

These experiments confirm that RPG is a good choice when we are limited by the memory space: although it may require more computations (in our examples, we may loose a factor of 5 in execution time), it can be applied on models that are not tractable with the RG version because of the space needed to store the transitions. For instance, for the Peg Solitaire model with 37 pegs (that has 3.10 9 states and 3.10 10 transitions), the RPG only needs 15 GB of memory while, with the RG version, we would need 240 GB of memory just to store the transitions.

Related work and Comparisons With Other Tools

Several works address the problem of designing efficient, parallel model-checking algorithms. Most of the proposals follow an "automata-theoretic approach" for LTL model checking. In this context, the difficulty is to adapt the cycle detection algorithms (Tarjan or Nested-DFS), which are inherently sequential. Two works stand out: one with a mature implementation, DiVinE [START_REF] Barnat | DiVinE: Parallel Distributed Model Checker[END_REF], with the owcty + map algorithm; another with a prototype, named LTSmin, with the mc-ndfs algorithm [START_REF] Laarman | Multi-Core nested Depth-First search[END_REF]. They mostly differ by the algorithm used to detect cycles.

DiVinE combines two algorithms, owcty and map, that result in "a parallel on-the-fly linear algorithm for model checking weak LTL properties" (weak LTL properties are those expressible by an automata that has no cycle with both accepting and no-accepting states on its path). If the LTL property does not meet this requirement, the algorithm complexity may be quadratic. The multicore nested DFS (mc-ndfs) algorithm [START_REF] Laarman | Multi-Core nested Depth-First search[END_REF] is a recent extension of the swarm [START_REF] Holzmann | Swarm verification[END_REF] distributed algorithm to a multi-core setting. The authors in [START_REF] Laarman | Multi-Core nested Depth-First search[END_REF] propose a multicore version with the distinction that the storage state space is shared among all workers in conjunction with some synchronization mechanisms for the nested search. Even if, in the worst-case, all the processors may duplicate the same work, this approach has a linear complexity (given a fixed number of processors).

In contrast with the number of solutions proposed for parallel LTL model checking, just two specifically target CTL model checking on shared memory machines: Inggs and Barringer work [START_REF] Inggs | CTL* model checking on a sharedmemory architecture[END_REF] supports CTL * , while van de Pol and Weber work [START_REF] Van De Pol | A Multi-Core solver for parity games[END_REF] supports the µ-calculus.

Comparison with DiVinE. We now compare our algorithms with DiVinE [START_REF] Barnat | DiVinE: Parallel Distributed Model Checker[END_REF], which is the state of the art tool for parallel model checking of LTL. The results given here have been obtained with DiVinE 2.5.2, considering only the best results given by the owcty or map, separately. This benchmark (experimental data and examples are available in report [START_REF] Saad | Parallel Model Checking with Lazy Cycle Detection-MCLCD[END_REF]) is based on the set of models borrowed from DiVinE on which, for a broader comparison, we check both valid and non valid properties. Figure 5 shows the exact set of models and formulas that are used. All experiments were carried out using 16 cores and with an initial hash table sized enough to store all states. The DiVinE experiments were executed with flag (-n) to remove counter-example generation.

Figure 6 shows for each model the execution time (T.) in seconds and the memory peak (M.) (in GB). Figure 7 summarizes these results using the normalized weighted sum of the memory footprint and the execution time, separated for valid and non valid formulas.

Algorithms owcty and map show better overall results when the formula is not valid (FALSE). By contrast, reverse holds the best execution time when the formula is valid. Regarding the RPG version of our algorithm, our results show that it holds the best memory footprint among all results, it uses on average 2 to 4 times less memory than map and owcty when the formula is valid. In addition, regardless of its "cubic" worst-case complexity, it shows good results when compared to map and owcty. For instance, it is able to verify a valid formula on average using 4 times less memory than owcty with a limited slowdown (≈ 1.8 times slower).

To conclude, for the set of models and formulas used in this benchmark, both RPG and RG delivered good results when compared to DiVinE. For instance, RG has a better performance in both time and memory usage when compared with DiVinE (map and owtcy). Finally, RPG proved to be the most space conscious algorithm-the one to choose for the biggest models-without sacrificing too much the execution time.

Conclusion

We have described ongoing works concerning parallel (enumerative) model-checking algorithms for finite state systems. We define two versions of a new model check- ing algorithm that support an expressive fragment of both CTL and LTL. These algorithms are based on the standard, semantic model-checking algorithm for CTL but specifically target parallel, shared memory machines. Our two versions differ by the amount of information they need to store: a Reverse Graph (RG) version that explicitly stores the complete transition relation in memory, and a Reverse Parental Graph (RPG) that relies on a spanning tree.

We use the reverse parental graph structure as a mean to fight the state explosion problem. In this respect, this approach has a similar impact-on the space-than algorithmic techniques like sleep sets (used with partial-order meth-ods), but with the difference that we do not take into account the structure of the model. Moreover, our approach is effective regardless of the formalism used to model the system. For instance, it is particularly useful in cases where it is not possible to compute the "inverse" of the transition relation.

Our prototype implementation shows promising results for both the RG and RPG versions of the algorithm. The choice of a "labeling algorithm" based on the out-degree number has proved to be a good match for shared memory machines and a work stealing strategy; we consistently obtained speedups close to linear with an average efficiency of 75%. Our experimental results also showed that the RPG version is able to outperform the RG version for some categories of models.

Using our work, one can easily obtain a parallel algorithm for checking any CTL formula Φ by running one instance of our algorithms (for the AU and EU formulas) for each subformula of Φ. But this approach, as such, is too naive. For future works, we are considering improvements of our algorithms that support full CTL formulas without having to manage several copies of our labels (sons and suc) in parallel, which could have an adverse effect on memory consumption.

  function BOOL c h e c k a ( ψ : pred , φ : pred , s0 : s t a t e ) S t a c k A ← new S t a c k ( ∅ ) ; // Start with the forward exploration i f f o r w a r d c h e c k a ( ψ , φ , s0 , A) then // If all forward constraints are respected return b a c k w a r d c h e c k a ( s0 , A) //start the backward phase e l s e return FALSE // We found a problem during the forward exploration Listing 1.1. Algorithm for the formula A (ψ ∪ φ)-function check a

Listing 1 . 2 .

 12 function BOOL f o r w a r d c h e c k a ( ψ : pred , φ : pred , s0 : s t a t e , A : S t a c k ) S e t S ← new S e t ( s0 ) ; S t a c k W ← new S t a c k ( s0 ) ; while (W i s n o t empty ) do s ← W. pop ( ) ; i f ( s φ ) then s u c ( s ) . s e t ( 0 ) ; // We clear state s from KS A . push ( s ) e l s i f ( s ψ ) then // We tag s with its number of successors s u c ( s ) . s e t ( number o f s u c c e s s o r s o f s in KS) ; i f ( s u c ( s ) = 0 ) // Check if s is not a dead state return FALSE f o r a l l s ' s u c c e s s o r o f s in KS do // and continue the exploration i f ( s ' / ∈ S ) then S ← S ∪ { s ' } ; // s' is a new state W. push ( s ' ) e l s e return FALSE return TRUE function BOOL b a c k w a r d c h e c k a ( s0 : s t a t e , A : S t a c k ) while (A i s n o t empty ) do s ← A . pop ( ) ; i f ( s = s0 ) then // The property is true if return TRUE // we reach the initial state f o r a l l s ' p a r e n t o f s in KS do // Otherwise we check if the s u c ( s ' ) . d e c ( ) ;// predecessors of s can be cleared i f ( s u c ( s ' ) = 0 ) then A . push ( s ' ) return FALSE Forward and backward exploration for A (ψ ∪ φ) with Reverse Graph

Listing 1 . 3 .

 13 function BOOL b a c k w a r d c h e c k a ( s0 : s t a t e , A : S t a c k ) o v e r ← FALSE while ( n o t o v e r ) while (A i s n o t empty ) do //Clearing s ← A . pop ( ) ; i f ( s = s0 ) then // The property is true if return TRUE // we reach the initial state s ' ← f a t h e r ( s ) ; // Otherwise we check if s o n s ( s ' ) . d e c ( ) ; // the father of s can be cleared s u c ( s ' ) . d e c ( ) ; i f ( s u c ( s ' ) = 0 ) then A . push ( s ' ) //Collecting: if we have no more states to clear in A we try to find // candidates among the states with no children in PKS f o r a l l s s u c h t h a t s o n s ( s ) = 0 and s u c ( s ) = 0 in KS do i f t e s t ( s ) then s u c ( s ) . s e t ( 0 ) ; A . push ( s ) i f (A i s empty ) then o v e r ← TRUE //No good candidate was found, end backward search return FALSE function BOOL t e s t ( s : s t a t e ) f o r a l l s ' s u c c e s s o r o f s in KS do i f s u c ( s ' ) = 0 then return FALSE // at least one successor is not cleared return TRUE Backward exploration for A (ψ ∪ φ) with Reverse Parental Graph

Fig. 2 .

 2 Fig. 2. Formula a b.

Fig. 3 .Fig. 4 .

 34 Fig. 3. Speedup and execution time analysis for Token Ring and Solitaire models.

Fig. 5 .

 5 Fig. 5. Formulas and Models for our Comparison. M Formula owcty map reverse parental T.(s) M.(Gb) T.(s) M.(Gb) T.(s) M.(Gb) T.(s) M.(Gb) AN F1: false 61.3 3.3 110.2 5.5 28.8 2.8 94.4 1.8 F2: true 79.5 7.4 110.5 4.8 26.4 2.9 50.4 1.8

Fig. 7 .

 7 Fig. 7. Comparison with divine (reverse = RG, parental = RPG).

  Fig. 6.Table of results.

				3	3.3	110.2	5.5	28.8	2.8	94.4	1.8
			F2: true 79.5	7.4	110.5	4.8	26.4	2.9	50.4	1.8
			F1: false 1.6	1.1	1.4	1.1	42.4	5.1	74.2	3.3
		LA	F2: false 1.4	1.1	1.7	1.2	47.6	5.6	327.2	3.6
			F3: true 153.6 14.1 282.8 12.1	51.0	5.6	370.4	3.7
		RE	F1: true 12.0 F2: false 13.2	1.8 1.8	20.1 1.2	1.3 0.3	5.0 3.4	0.7 0.7	12.0 7.8	0.6 0.6
			F1: false 8.5	0.9	7.0	0.5	2.2	0.3	1.4	0.2
		SZY	F2: false 9.8	0.9	6.6	.5	4.2	0.3	39.6	0.3
			F3: true	9.0	0.9	24.7	0.6	3.8	0.3	32.8	0.3
	Weighted Norm Exec. Time	0.1 0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1				Weighted Norm Mem. Usage	0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1
			m a p o w c t y r e v e r s e p a r e n t a l	m a p o w c t y r e v e r s e p a r e n t a l		m a p o w c t y r e v e r s e p a r e n t a l	m a p o w c t y r e v e p a r r e n s e t a l
			Valid (TRUE)	Not Valid(FALSE)			Valid (TRUE)	Not Valid (FALSE)

This work was partially supported by JU Artemisia project CESAR, AESE project Topcased and Région Midi-Pyrénées


F Mériaux

S M Perlaza

S Lasaulce

Z Han

H V Poor

Achievability of Efficient Satisfaction Equilibria in Self-Configuring Networks

Keywords: Supermodular games, Power control, Efficient Satisfaction Equilibrium, Games in Satisfaction Form

In this paper, a behavioral rule that allows radio devices to achieve an efficient satisfaction equilibrium (ESE) in fully decentralized self-configuring networks (DSCNs) is presented. The relevance of ESE in the context of DSCNs is that at such state, radio devices adopt a transmission/receive configuration such that they are able to simultaneously satisfy their individual quality-of-service (QoS) constraints. An ESE is also an efficient network configuration, i.e., individual QoS satisfaction is achieved by investing the lowest possible effort. Here, the notion of effort refers to a preference each radio device independently establishes among its own set of actions. In particular, the proposed behavioral rule requires less information than existing rules, as in the case of the classical best response dynamics and its variants. Sufficient conditions for convergence are presented in a general framework. Numerical results are provided in the context of a particular uplink power control scenario, and convergence from any initial action profile to an ESE is formally proved in this scenario. This property ensures the proposed rule to be robust to the dynamic arrival or departure of radio devices in the network.

Introduction

A decentralized self-configuring network (DSCN) is basically an infrastructureless communication system in which radio devices autonomously choose their own transmit/receive configuration in order to guarantee reliable communication. In particular, a transmit/receive configuration can be described in terms of power allocation polices, coding-modulation schemes, scheduling policies, decoding order, etc. Typical examples of DSCNs are wireless sensor networks, short range networks in the ISM bands (e.g., Wi-Fi, Bluetooth, ZigBee, etc,), femto-cell networks (e.g., femto cells in LTE-A) and adhoc networks in general. The underlying feature of DSCNs is that transmitters directly communicate with their respective receivers without the intervention of a central controller. Thus, the main limitation of these networks to actually provide QoS is the mutual interference arising from the uncoordinated interaction of radio devices subject to mutual interference. Within this context, the notion of QoS provisioning translates into the need for designing behavioral rules such that radio devices autonomously adapt their transmission configurations in order to meet the minimum requirements for their communications to take place satisfactorily. In particular, similar reconfigurable capabilities have been already mentioned in [START_REF] Haykin | Cognitive radio: Brain-empowered wireless communications[END_REF] in the context of cognitive radios.

In general, the decentralized nature of the QoS provisioning task in DSCN has fostered the use of tools from game theory (GT) [START_REF] Lasaulce | Game Theory and Learning in Wireless Networks: Fundamentals and Applications[END_REF][START_REF] Han | Game Theory in Wireless and Communication Networks: Theory, Models and Applications[END_REF], strategic learning theory [START_REF] Rose | Learning equilibria with partial information in decentralized wireless networks[END_REF], distributed optimization and variational inequality theory [START_REF] Scutari | Convex optimization, game theory, and variational inequality theory in multiuser communication systems[END_REF] to the analysis of QoS provisioning in this scenario. In this paper, we focus on a particular formulation of the QoS provisioning problem, namely games in satisfaction form [START_REF] Perlaza | Quality-of-service provisioning in decentralized networks: A satisfaction equilibrium approach[END_REF]. More specifically, we provide behavioral rules that allow radio devices to achieve an efficient satisfaction equilibrium (ESE) in DSCNs. The notion of ESE, as introduced in [START_REF] Perlaza | Quality-of-service provisioning in decentralized networks: A satisfaction equilibrium approach[END_REF], refers to a network state in which all the network devices are able to satisfy their individual QoS constraints by investing the minimum effort. Often, we associate the notion of high effort with transmit/receive configurations that might represent an additional waste of energy to satisfy the individual QoS constraints. In this context, one of the main contributions of this paper is the introduction of a behavioral rule that allows the network to achieve an ESE using only local information. Another important contribution is a set of sufficient conditions to observe the convergence to an ESE of the proposed rule.

In order to show the potential of our contributions in the context of DSCNs, we consider a particular scenario of power control in the uplink of a single-cell system in which devices must guarantee a minimum signal to interference plus noise ratio (SINR). Interestingly, we highlight that in this particular scenario, the proposed behavioral rule converges to an ESE independently of the initial state of the network. This result contrasts with the existing literature. For instance, in [START_REF] Altman | S-modular games and power control in wireless networks[END_REF], Altman et al. studied the problem in the general framework of compact sublattices as action sets. Therein, under the assumption that a solution to the problem exists, they established that a simple behavioral rule known in game theory as the best response dynamics (BRD) [START_REF] Fudenberg | Game Theory[END_REF] only converge to the solution from particular starting points. When the transmit power sets are continuous, Yates et al. proved that the BRD converge from any initial point in [START_REF] Yates | A framework for uplink power control in cellular radio systems[END_REF]. In the case of discrete actions sets, an algorithm close to the BRD is proposed in [START_REF] Wu | Distributed power control algorithms for wireless networks[END_REF]. However, there are still conditions on the starting point to ensure the convergence of the algorithm.

The remainder of this paper unfolds as follows. In Sec. 2, we revisit the notion of satisfaction equilibrium (SE) and ESE and we formulate the QoS provisioning problem in the most general terms. In Sec. 3, we describe our main contribution: a behavioral rule that allows DSCNs to converge to an ESE, when action sets correspond to compact sublattices. In Sec. 4, we present numerical results in a particular scenario as described above in order to verify our theoretical contributions. Finally, we conclude our work in Sec. 5.

2 QoS Provisioning and Games in Satisfaction Form

QoS Problem Formulation

Consider a DSCN comprising a set K = {1, . . . , K} of K transmitter/receiver pairs to which we refer as links. Each radio device autonomously chooses its optimal transmit/receive configuration in order to satisfy its own QoS requirements. Here, we denote by k ∈ K the k-th link, independently of whether it is the transmitter or the receiver that is the device performing the self-adaptation of the link configuration. We denote by a k the transmit/receive configuration adopted by the link k, and we denote by A k the set of all its possible choices. For all k ∈ K, A k is assumed to be a compact sublattice, as in [START_REF] Altman | S-modular games and power control in wireless networks[END_REF][START_REF] Yao | S-modular games, with queueing applications[END_REF]. A = A 1 ×. . .×A K represents the set of all configuration profiles. This structure has the advantage of comprising both compact continuous sets and discrete sets1 . We denote by a -k = (a 1 , . . . , a k-1 , a k+1 , . . . , a K ) the vector obtained by dropping the k-th component of the vector a. We denote the space in which the vector a -k exists by A -k . With a slight abuse of notation, we write the vector a as (a k , a -k ), in order to emphasize its k-th component. A transmit/receive configuration can be described by parameters such as the power allocation policy, modulation scheme, constellation size, decoding order, scheduling policy, etc. The instantaneous performance of radio device k is determined by a set of

Q k functions        u (1) k : A → R, . . . u (Q k ) k : A → R. (1)
Typical performance metrics are transmission rate, transmission delay, bit error rate, energy efficiency, or any combination of those. We denote the minimum and maximum acceptable values of the performance metric u

(q k ) k by Γ (q k ,min) k and Γ (q k ,max) k
, respectively. Thus, we say that the configuration profile a ∈ A satisfies the QoS constrains of the DSCN if for all link k the following set of inequalities are satisfied :

       Γ (1,min) k < u (1) k (a k , a -k ) < Γ (1,max) k , . . . Γ (Q k ,min) k < u (Q k ) k (a k , a -k ) < Γ (Q k ,max) k . ( 2
)
Note that the performance metrics of link k depend not only on its own configuration a k but also on the configurations a -k adopted by all the other links. Thus, in order to ease our notation, we define the correspondence f k : A -k → 2 A k that determines all the possible configurations of player k that satisfies its QoS constraints. That is

∀a k ∈ A k a k ∈ f k (a -k ) ⇔ ∀q ∈ {1, . . . , Q k }, Γ (q,min) k < u (q) k (a k , a -k ) < Γ (q,max) k . ( 3
)
The problem of all the links wanting to satisfy their QoS constraints at the same time can naturally be described as a game.

Game Formulation

As defined in [START_REF] Perlaza | Quality-of-service provisioning in decentralized networks: A satisfaction equilibrium approach[END_REF], a game in satisfaction form is fully described by the following triplet

Û G = K, {A k } k∈K , {f k } k∈K . (4)
In this triplet, K represents the set of players, A k is the strategy set of player k ∈ K, and the correspondence f k determines the set of actions of player k that allows its satisfaction given the actions played by all the other players.

A strategy profile is denoted by vector a = (a 1 , . . . , a K ) ∈ A. In general, an important outcome of a game in satisfaction form is the one where all players are satisfied, that is, an SE. The notion of SE was formulated as a fixed point in [START_REF] Perlaza | Quality-of-service provisioning in decentralized networks: A satisfaction equilibrium approach[END_REF] as follows:

Definition 1 (Satisfaction Equilibrium). An action profile a + is an equilibrium for the game

Û G = K, {A k } k∈K , {f k } k∈K if ∀k ∈ K, a + k ∈ f k a + -k . (5)
As we shall see, the SE is often not unique and thus, there might exist some SEs that are of particular interest. In the following, we introduce the notion of an efficient SE (ESE). For this intent, we consider a cost function for each player of the game, in order to model the notion of effort or cost associated with a given action choice. For all k ∈ K, the cost function

c k : A k → [0, 1] satisfies the following condition : ∀(a k , a k ) ∈ A 2 k , it holds that c k (a k ) < c k (a k ) , (6)
if and only if, a k requires a lower effort than action a k when it is played by player k. Under the notion of effort, the set of SEs that are of particular interest are those that require the lowest individual efforts. We formalize this notion of equilibrium using the following definition.

Definition 2 (Efficient Satisfaction Equilibrium

). An action profile a * is an ESE for the game

Û G = K, {A k } k∈K , {f k } k∈K , with cost functions {c k } k∈K , if ∀k ∈ K, a * k ∈ f k a * -k (7)
and ∀k ∈ K, ∀a k ∈ f k (a * -k ), c k (a k ) ≥ c k (a * k ). (8)
Note that the effort associated by each player with each of its actions does not depend on the choice of effort made by other players. Here, we have left players to individually choose their cost functions, which adds another degree of freedom to the modeling of the QoS problem in DSCNs. Note also that a game in satisfaction form is not a game with a constrained set of actions, as is the case in the formulation presented in [START_REF] Debreu | A social equilibrium existence theorem[END_REF]. Here, a player can use any of its actions independently of all the other players. The dependency on the other players' actions enters through whether the player under study is satisfied or not.

Power Control Game

In the rest of this paper, we use the context of uplink power control in a singlecell as a case study. Although most of our results apply in a general context, we concentrate in the uplink power control problem as presented in [START_REF] Wu | Distributed power control algorithms for wireless networks[END_REF][START_REF] Yates | A framework for uplink power control in cellular radio systems[END_REF], to illustrate our results.

Consider K transmitter/receiver pairs denoted by index k ∈ K. For all k ∈ K, transmitter k uses power level p k ∈ A k , with A k generally defined as a compact sublattice For each player k ∈ K, we denote p min k and p max k the minimum and the maximum power levels in A k , respectively. For every couple (i, j) ∈ K 2 , we denote by g ij the channel gain coefficient between transmitter i and receiver j. The considered metric for each pair k is the Shannon rate given by

u k (p k , p -k ) = log 2 Å 1 + p k g kk σ 2 k + j =k p j g jk ã [bps/Hz], (9)
where σ 2 k is the noise variance at receiver k. The QoS requirement for each pair k is to have a channel capacity u k (p k , p -k ) higher than a given threshold Γ k bps/Hz. The satisfaction correspondence of link k is then

f k (p -k ) = {p k ∈ A k | u k (p k , p -k ) ≥ Γ k } = ® p k ∈ A k | p k ≥ (2 Γ k -1) σ 2 k + j =k p j g jk g kk
´.

(10)

Convergence to an Efficient Satisfaction Equilibrium

In this section, we provide sufficient conditions for convergence of the BRD and the robust blind response dynamics (RBRD) to an ESE of the game Û G = K, {A k } k∈K , {f k } k∈K , with cost functions {c k } k∈K .

Best Response Dynamics

In the context of a game in satisfaction form Û G = K, {A k } k∈K , {f k } k∈K , with cost functions {c k } k∈K , we define the best response (BR) correspondence of player k, given that the other players adopt the reduced action profile a -k , as follows:

BR k (a -k ) = arg min

a k ∈f k (a -k ) c k (a k ). ( 11
)
We consider a BRD defined as the behavioral rule in which players sequentially update their action following the Gauss-Seidel method [START_REF] Bertsekas | Parallel and Distributed Computation: Numerical Methods[END_REF]. At step n + 1 of the algorithm, all the players sequentially update their actions with the following rule: a

(n+1) k = BR k (a (n+1) 1 , . . . , a (n+1)
k-1 , a

(n) k+1 , . . . , a (n) K ). ( 12
)
For a discrete set of actions, the BRD can be compared to the asynchronous version of the Minimum Feasible Value Assignment (MFVA) algorithm presented in [START_REF] Wu | Distributed power control algorithms for wireless networks[END_REF]. The difference is that in [START_REF] Wu | Distributed power control algorithms for wireless networks[END_REF], players only move to their optimal satisfying action if they are not satisfied with actions played at the previous step. In the BRD, players move to their optimal satisfying action independently of their satisfaction at the previous step.

Convergence of the BRD

To study the convergence of the BRD, we first define some notation of interest.

and said to be submodular if

g(a ∧ b) + g(a ∨ b) ≤ g(a) + g(b). (14)
In the case of the cost function defined in [START_REF] Haykin | Cognitive radio: Brain-empowered wireless communications[END_REF], c k depends only on the actions of player k. Hence, c k is both supermodular and submodular. As a result, ( 13) and ( 14) are equalities.

Definition 4 (Ascending and descending properties). The correspondence f k is said to possess the ascending property (respectively the descending property) if for any two elements a -k and a -k of the set

A -k , with a -k = a -k ∧ a -k implies that ∀a k ∈ f k (a -k ) and ∀a k ∈ f k (a -k ), ß min(a k , a k ) ∈ f k (a -k ), max(a k , a k ) ∈ f k (a -k ), (15)
or for the descending property

ß max(a k , a k ) ∈ f k (a -k ), min(a k , a k ) ∈ f k (a -k ). ( 16
)
An important consequence of the ascending (or descending) property is that

∀a -k ∈ A -k , f k (a -k ) = ∅. ( 17
)
The definition of an ascending set can easily be understood in the context of distributed power control. In such a context, the ascending property means that if all the other players increase their powers, player k also has to increase its own power if it wants to remain satisfied. Also note that if the ascending property is ensured, then there is always at least one satisfying power level for player k, whatever the other players are playing. In particular, when all the players are at maximum power levels, there exists a satisfying power for player k, which is a strong assumption. The proof of Prop. 1 comes from Th. 1 in [START_REF] Altman | S-modular games and power control in wireless networks[END_REF] and Th. 2.3 in [START_REF] Yao | S-modular games, with queueing applications[END_REF]. We simply have to verify that the right assumptions hold for the ascending case and the descending case:

-Let f k (•) be ascending for all k ∈ K. c k is a cost function player k wants to minimize, in particular c k is a submodular function, and thus -c k is a supermodular function player k wants to maximize and Th. 1 from [START_REF] Altman | S-modular games and power control in wireless networks[END_REF] holds, i.e., (i, ii, iii) in Prop. 1 are ensured when the sets are ascending. -Let f k (•) be descending for all k ∈ K. A similar reasoning can be made: c k is a submodular function player k wants to minimize and the same theorem holds as well, i.e., (i, ii, iii) in Prop. 1 are ensured when the sets are descending.

In both ascending and descending cases, (iv) in Prop. 1 is obtained from Th. 2.3 in [START_REF] Yao | S-modular games, with queueing applications[END_REF].

BRD in the Uplink Power Control Game

In the general framework of compact sublattices as strategy sets (including continuous and discrete action sets), the BRD converge only from given starting points (see [START_REF] Altman | S-modular games and power control in wireless networks[END_REF][START_REF] Yao | S-modular games, with queueing applications[END_REF]). However, in the uplink power control problem, it has been shown in [START_REF] Scutari | Potential games: A framework for vector power control problems with coupled constraints[END_REF][START_REF] Yates | A framework for uplink power control in cellular radio systems[END_REF] that when strategy sets are continuous, the BRD converge from any initial point. When strategy sets are discrete, the convergence of the BRD from any initial point to an equilibrium is not guaranteed. In [START_REF] Wu | Distributed power control algorithms for wireless networks[END_REF], it is shown that the MFVA converges only when all the transmitters start at their lowest power levels. In the following, we consider a 3-player uplink power control game to illustrate the non-convergence of the BRD from a particular initial action profile.

Example 1. In this example, we refer to the notation introduced in Sec. 2.3. Let us consider K = 3 pairs of transmitters/receivers. For all k ∈ K, transmitter k uses power level a k ∈ {p min , p max }. Given the constraints from Sec. 2.3, let consider channel gains such that

f 1 (p min , p min ) = f 3 (p min , p min ) = {p min , p max }, f 1 (p min , p max ) = f 3 (p min , p max ) = {p min , p max }, f 1 (p max , p min ) = f 3 (p max , p min ) = {p max }, f 1 (p max , p max ) = f 3 (p max , p max ) = {p max }, (18)
and

f 2 (p min , p min ) = {p min , p max }, f 2 (p min , p max ) = {p max }, f 2 (p max , p min ) = {p min , p max }, f 2 (p max , p max ) = {p max }. (19)
We can check that f k has the ascending property for all k ∈ K. For each pair k, the cost of the power level is given by the identity cost function c k (a k ) = a k . This game has two ESEs:

-(p min , p min , p min ) where all the players transmit at their lowest power level.

No player has interest in deviating from its action since any other action has a higher cost (even though the player would remain satisfied). -(p max , p max , p max ) where all the players have to transmit at maximum power to be satisfied. If one deviates from its action, it will not be satisfied anymore.

But depending on the initial action profile of the BRD, the BRD may not converge to an ESE. For instance, assume that the BRD start at p (0) = (p max , p min , p max ). At step 1, player 1 chooses the action that minimizes c 1 (•) given the previous actions of the other players p (0)

-1 = (p min , p max ), i.e., p (1)
2 ) = (p min , p max ), i.e., p

3 = BR 3 (p min , p max ) = p min . ( (1)
) 22
At step 2, player 1 chooses the action that minimizes c 1 (•) given the previous actions of the other players p

-1 = (p max , p min ), i.e., p

1 = BR 1 (p max , p min ) = p max . ( (2)
) 23
Player 2 chooses the action that minimizes c 2 (•) given the most recent actions of the other players (p

(2) 1 , p (1)
-(1,2) ) = (p max , p min ), i.e., p (2)
2 = BR 2 (p max , p min ) = p min . ( 24
)
Player 3 chooses the action that minimizes c 3 (•) given (p

(2) 1 , p (2)
2 ) = (p max , p min ), i.e., p

3 = BR 3 (p max , p min ) = p max . ( (2)
) 25
The algorithm is back at the starting point, and it is clear that it will continue in this infinite loop.

Robust Blind Response Dynamics

The BRD have significant drawbacks. First, it was just shown that in a K-player game with K > 2, the dynamics may not converge to an ESE depending on the initial action profile. Second, to determine the BR, each player has to know the set f k (a -k ) ∀a -k ∈ A -k . To overcome these drawbacks, we propose a new algorithm that requires less information about the game for each player and can still be proven to converge to an ESE. Let us start by defining the robust blind response (RBR) by RBR k : A → A k , such that :

(a k , a -k ) →    a k , if a k ∈ f k (a -k ), a k ∈ f k (a -k ) and c k (a k ) ≤ c k (a k ), a k , if a k ∈ f k (a -k ) and a k / ∈ f k (a -k ), a k , otherwise, (26)
with action a k being randomly chosen in A k , such that ∀a k ∈ A k , Pr (a k = a k ) > 0. Each time the RBR is used, a player k ∈ K randomly chooses an action in its strategy set A k without taking into account the constraints of other players. Player k only has to know if the new action and the previous one allow the satisfaction of its individual constrains and to compare their respective costs. If both actions allow the satisfaction of the constraints, it chooses the one with the lowest cost. If the new action allows the satisfaction of the individual constraints whereas the previous one does not, it moves to the new action. Otherwise, it keeps the same action. When all the players sequentially use the RBR such that ∀k ∈ K

a (n+1) k = RBR k (a (n+1) 1 , . . . , a (n+1) k-1 , a (n) k+1 , . . . , a (n) K ), (27)
we refer to these dynamics as the RBR dynamics (RBRD). Our main result in this section is stated in the following theorem. Proof. Applying Prop. 1, we know that there exists an ESE for the game Û G = K, {A k } k∈K , {f k } k∈K . The convergence of the RBRD to an ESE is proven in two steps. First, we show for (i, ii, ii) that the RBRD converge to a fixed point. Second, we explain why this fixed point has to be an ESE.

-(i) Assume that the dynamics start from an SE: a SE and this SE is not an ESE (otherwise, the convergence is trivial). Let player k ∈ K be the first player to actually change its action at step n to a

k ; necessarily this action has a lower cost than a SE k because a satisfied player can only move to another satisfying action with a lower cost. Let the next player to move be denoted by j. From its point of view (a

(n) k , a SE -{k,j} ) = (a (n) k , a SE -{k,j} ) ∧ a SE -j .
Hence, due to the ascending property of f j and the strict monotony of c j , necessarily its new action a (n ) j ≤ a SE j , and so forth. For each k ∈ K the sequence {a

(n)
k } n∈N is decreasing in a compact set. Thus, the algorithm converges to a limit. -(ii) Assume that the dynamics start from action profile a max = (a max 1 , . . . , a max K ) and this point is not an SE (otherwise refer to (i)). Let player k update its action first, at step n. Necessarily, its updated action a

(n) k is lower than a max k . Then ∀j = k, j ∈ K (a max {-j,k} , a (n)
k ) = (a max {-j,k} , a (n) k ) ∧ a max -j . (28)
Due to the ascending property of f j and the strict monotony of c j , the update of player j is hence lower than a max j , and so forth. Again, for each player k ∈ K, the sequence of action {a

(n)
k } n∈N is decreasing in a compact set and the algorithm converges to a limit. -(iii) In a two-player game, assume the dynamics start from a random action profile (a

(0) 1 , a (0)
2 ). Assume player 1 is the first player that updates its action to get satisfied, at step n. The action profile is then (a

(n) 1 , a (0)
2 ). In the next move, either the same player 1 decreases its action, remaining satisfied, or player 2 moves to an action that satisfies it, leading to an action profile (a

(n) 1 , a (n ) 2 ).
If this profile is an SE, the dynamics converge according to (i). Otherwise player 1 is no longer satisfied and has to update its action. If a

(n ) 2 < a (0)
2 , then due to the ascending property and the strict monotonicity of c 1 , player 1 will only move to a lower action than a (n) 1 . Then player 2 will also have to move to a lower action than a (n ) 2

for analogous reasons, and so forth. The sequences {a (n) 1 } n∈N and {a (n) 2 } n∈N are hence decreasing in a compact set, so they converge to a limit. If a

(n ) 2 > a (0)
2 , the sequences are increasing in a compact set and converge as well.

We now have to prove that a fixed point is an ESE. Consider that a * is a fixed point for RBR k , ∀k ∈ K. By the definition of RBR k this means that there exists no

a k ∈ A k such that a k ∈ f k (a * -k ) and c k (a k ) ≤ c k (a * k )
, which is exactly the definition of the ESE. This completes the proof.

The main advantage of these dynamics over BRD in a general framework is that the former require only local information and the knowledge of an explicit expression for f k is no longer relevant. Only the knowledge of whether the corresponding player is satisfied or not is sufficient to implement the RBR.

RBRD in the Uplink Power Control Game

A very interesting property occurs for the RBR in the uplink power control game with discrete action sets.

Theorem 2. In the power allocation game defined above in Sec. 2.3, with discrete action sets, i.e., ∀k ∈ K, A k = {p Proof. We show in this proof that from any starting point of the dynamics, there is a non-null probability that the dynamics move to a particular SE with a given way. Note that the particular sequence of events we describe here is not always the way the dynamics run. It is simply a sequence that can occur with a non-null probability, but there are many other possible sequences that lead to an SE.

Assume p (0) = (p

(0) 1 , . . . , p (0)
k ) is the starting power profile of the dynamics. Consider all the unsatisfied players at this point and assume that they all move to their maximum possible power levels (this may happen with a non-null probability). These levels satisfy them since the ascending property gives us

∀k ∈ K, ∀p -k ∈ A -k , p max k ∈ f k (p -k ). ( 29
)
This increase of power levels may cause some of the satisfied players at the starting point not to be satisfied anymore. We also assume that these players move to their maximum power levels. And the same is done until no unsatisfied player remains. So we get a power profile made of the highest power levels for some of the players and the initial power levels for the others, and every player is satisfied at this point: it is an SE. Finally, from (i) of Th. 1, the dynamics converge to an ESE, which completes the proof.

Th. 2 highlights a very interesting property of the RBRD when players enter or quit the game (or when the channel coefficients vary). Indeed, if K transmitters are in any given ESE p * and a new transmitter enters the game, a new game starts with K + 1 players. Thus, from Th. 2, it can be stated that convergence to a new ESE, if it exists, is ensured from the new starting point (p * , p k+1 ).

Numerical Results

In this section, we provide numerical results for the uplink power control game with discrete action sets as defined in Sec. 2.3.

In Fig. 1, we show the sequences of actions converging to an ESE for the RBRD in a 2-player power control game. The colored region is the satisfaction region, i.e., the region allowing both players to be satisfied. The coloring of this region follows the sum of the costs for each player. The RBR first converges to the satisfaction region, then converges to an ESE while remaining in the satisfaction region.

Power Index of Player 1 Power Index of Player 2 The scenario we consider in Fig. 2 and Fig. 3 highlights the advantages of RBRD over the BRD in a 3-player game: during the first 200 steps, only transmitters 1 and 3 are in the game, then transmitter 2 joins them for the 200 next steps, and finally transmitter 3 leaves for the last 200 steps. On each of the two figures, we show the sequence of power indices for the three players, knowing that each action set is made of N k = 32 possible power levels from 10 -6 W to 10 -2 W. We also show the satisfaction states of the three players: for each step of the dynamics, if all the player are satisfied, the satisfaction state is 1, otherwise it is 0. Fig. 2 and Fig. 3 correspond to the behavior of the BRD and the RBRD, respectively. The channel parameters and the starting points of the two simulations are exactly the same. Channel gains are g 22 = 10 -5 , g 11 = g 33 = g 13 = g 21 = g 32 = 10 -6 , g 12 = g 23 = g31 = 10 -7 , and transmitters 1, 2, and 3 start at power levels 10 -3 W, 10 -5/2 W, and 10 -9/4 W, respectively. The utility constraints Γ 1 , Γ 2 , and Γ 3 are taken as 1.2 bps/Hz, 1.5 bps/Hz, and 1.2 bps/Hz, respectively. The variance of the noise is fixed at 10 -10 W for all the transmitters. It is interesting to notice that the BRD converge to ESE during the first and third phase but when transmitter 2 enters the game in the second phase, the BRD do not converge to an ESE. Instead, they enter a loop and we can see that the transmitters are not satisfied. Concerning the RBRD, although their convergence time is longer, they converge in the three phases and another interesting fact is that transmitters are satisfied during a longer amount of time compared to the BRD.

Conclusion and Future Work

In this work, we have proposed a behavior rule that converges to an ESE in the general framework of compact sublattices as actions sets. Compared to the BRD, the proposed rule requires far less information although its convergence time is longer. Applying this rule to the uplink power control game with discrete actions sets has been shown to be of great interest since the dynamics are proven to converge to an ESE from any starting action profile. This particular feature allows the proposed rule to be robust to the entrance or the exit of players in the power control game. However, a strong assumption of this work is to assume that for every player, for any action profile of the other players, there exists an action satisfying the considered player. In the power control game, it would be more relevant to take into account scenarios in which the power levels of the other players are too high and a given player cannot be satisfied for any action it can play. Hence, a natural perspective of this work is to relax this assumption and study the convergence of the dynamics in this context.

  Let a = (a 1 , . . . , a N ) and b = (b 1 , . . . , b N ) be two action profiles and let c = a ∨ b denote the maximum of (a, b) component wise, i.e., c = (c 1 , . . . , c N ) with c n = max(a n , b n ) ∀n ∈ {1, . . . , N }. In a similar way, a ∧ b denotes min(a, b) component wise. Definition 3 (S-modularity). The function g: A → R is said to be supermodular if for any a, b ∈ A g(a ∧ b) + g(a ∨ b) ≥ g(a) + g(b),

Proposition 1 .

 1 Assume that for all k ∈ K, f k (•) is nonempty and compact for all the values of their arguments, f k (•) has either the ascending or the descending property and f k (•) is continuous. Then the following holds: -(i) An ESE exists. -(ii) If the dynamics start with the action profile associated with the highest or lowest effort in c k (•), for all k ∈ K, the BRD converge monotonically to an ESE. -(iii) If the dynamics start from an SE, the trajectory of the best response converges to an ESE. It monotonically evolves in all components. -(iv) In a two-player game, the BRD converge to an ESE from any starting point.

1 = 2 =

 12 BR 1 (p min , p max ) = p min . (20) Player 2 chooses the action that minimizes c 2 (•) given the most recent actions of the other players (p BR 2 (p min , p max ) = p max . (21) Player 3 chooses the action that minimizes c 3 (•) given (p

Theorem 1 .

 1 Assume that for all k ∈ K, f k (•) is nonempty and compact for all the values of their arguments, f k (•) has the ascending property and it is continuous, and c k (•) is strictly increasing. Then, the following holds:-(i)If the dynamics start from an SE, the sequence of RBRs converges to an ESE. It monotonically decreases in all components. -(ii) If the dynamics start with the actions associated with the highest effort in c k (•), ∀k ∈ K, the sequence of RBRs converges monotonically to an ESE. -(iii) In a two-player game, the sequence of RBRs converge to an ESE from any starting point.

( 1 )

 1 k , . . . , p N k k } with N k the number of power levels in action set A k , the RBRD converge to an ESE from any starting point.

Fig. 1 .

 1 Fig. 1. Sequence of power indices for the RBRD in the uplink 2-player power control game. The colored region is the satisfaction region, i.e., the region where the two players mutually satisfy their constraints.

Fig. 2 .Fig. 3 .

 23 Fig. 2. Sequences of power indices and satisfaction states for the BRD in the 3-player uplink power control game.

The results of Sec. 3.2 and Sec. 3.4 apply to the general framework of compact sublattices whereas the results of Sec. 3.5 apply only to discrete configuration sets.