Hélène Collavizza

Vinh Le

Nguyen
email: lvnguyen@polytech.unice.fr

Olivier Ponsini
email: ponsini@i3s.unice.fr

Michel Rueher
email: michel.rueher@gmail.com

Antoine Rollet
email: rollet@labri.fr

Software Tools for Technology Transfer manuscript

Keywords: embedded systems, validation, constraintbased bounded model checking, counterexample generation

Safety property checking is mandatory in the validation process of critical software. When formal verication tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is an important issue in practice. We investigate in this paper the capabilities of constraint-based bounded model checking for program verication and counterexample generation on real applications. We introduce DPVS (Dynamic Post-condition Variable driven Strategy), a new backjumping strategy we developed to handle an industrial application from a car manufacturer, the Flasher Manager. This backjumping strategy is used to search a faulty path and to collect the constraints of such a path. The simplied control ow graph (CFG) of the program is explored in a backward way, starting from the post-condition and jumping to the most promising node where the variables of the post-condition are dened. In other words, the constraints are collected by exploring the CFG in a dynamic and non-sequential backward way.

The Flasher Manager application has been designed and simulated using the Simulink platform. However, this module is concretely embedded as a C program in a car computer, thus we have to check that the safety properties are preserved on this C code. We report experiments on the Flasher Manager with our constraint-based bounded model checker, and with CBMC, a state-ofthe-art bounded model checker. Experiments show that DPVS and CBMC have similar performances on one property of the Flasher Manager; DPVS outperforms CBMC to nd a counterexample for two properties; two of the properties of the Flasher Manager remain intractable for CBMC and DPVS.

A preliminary version of this paper appeared in Proceedings of SAC 2011 [13]. This work was partially

Introduction

In modern critical systems, software is often the weakest link. Thus, more and more attention is devoted to the software verication process (see for instance [START_REF] Bochot | Model checking ight control systems: The Airbus experience[END_REF] and the SLAM project [START_REF] Ball | A Decade of Software Model Checking with SLAM[END_REF]). Software verication includes automatic or semi-automatic formal proofs, functional and structural testing, manual code review and analysis. In practice, formal proof methods that ensure the absence of all bugs in a design are usually too expensive, or require important manual eorts. Thus, automatic generation of counterexamples violating a property on a limited model of the program is an important issue. Typically,

this is an open challenge in real time applications where bugs must be found for realistic time periods.

Bounded Model Checking (BMC) techniques have been widely used in semiconductor industry for nding deep bugs in hardware designs [START_REF] Biere | Symbolic model checking without bdds[END_REF] and are also applicable for software [START_REF] Silva | A survey of automated techniques for formal software verication[END_REF]. In BMC, falsication of a given program property is checked for a given bound k. BMC [START_REF] Ganai | Accelerating high-level bounded model checking[END_REF] mainly transforms the unwound program and the property into a propositional formula φ such that φ is satisable iff there exists a counterexample of depth less than k. A SAT-solver or an SMT-solver is used for checking the satisability of φ.

Constraint-based bounded model checking

We investigate in this paper the capabilities of constraintbased BMC for program verication and counterexample generation on real applications. The goal is to verify the conformity of a program with its specication, that is, to demonstrate that the specication is a consequence of the program under the boundedness restrictions. The key idea in constraint-based BMC is to use constraint stores to represent both the specication and the program, and to explore execution paths of bounded length over these constraint stores. The initial constraint store consists of the pre-condition and the negation of the post-condition. The constraint-based symbolic execution incrementally renes this constraint store by adding constraints generated from program conditions and assignments. Like in standard BMC, we assume a bound on the program inputs (e.g., the array length, the size of the integers and the variable values) and on the number of iterations for loops. Boundedness guarantees termination but it may induce incompleteness: indeed, the verier is inconclusive if executable paths with a length greater than the specied bound exist. The input program is correct if each constraint store produced by the symbolic execution implies the post-condition and the loop unwinding assertion (terminating a loop early) does not fail.

The main dierence between constraint-based BMC and standard BMC (i.e., BMC based on SAT or SMT solvers) [START_REF] Silva | A survey of automated techniques for formal software verication[END_REF] lies in the representation of the program and the assertions: the standard BMC approach generates a big Boolean formula whereas we generate the constraints on the y. We proposed in a previous work a constraintbased BMC framework named CPBPV [START_REF] Collavizza | CPBPV: A Constraint-Programming Framework for Bounded Program Verication[END_REF][START_REF] Collavizza | A constraint-programming framework for bounded program verication[END_REF]. CPBPV is based on a depth rst search strategy that explores the Control Flow Graph (CFG) of a program starting from the pre-condition. CPBPV incrementally adds the constraints associated to the nodes of the CFG, pruning unfeasible paths as early as possible. CPBPV has been successful on classical benchmarks, such as sorting algorithms or the binary search algorithm. However, CPBPV was unable to prove or to disprove any of the properties of the Flasher Manager application. Therefore, we investigated new search strategies and designed DPVS (Dynamic Post-condition Variable driven Strategy), a backjumping strategy that is used to search a faulty path and to collect the constraints of such a path.

The CFG is explored in a backward way, starting from the post-condition and jumping to the most promising node where the variables of the post-condition are dened. In other words, the constraints are collected by exploring the CFG in a dynamic and non-sequential backward way. This helps to detect inconsistencies as early as possible.

The contribution of this paper is twofold: i) We provide a new industrial application which is still a challenge for state-of-the-art bounded model checkers. While software BMC has widely been applied on device drivers, this application comes from the automotive industry. This type of application is generally simulated or veried using platforms such as Simulink or SCADE, but we are interested in the correction of the C code which is actually embed-ded in the car computer 1 . All the source code of this new kind of application is publicly available.

ii) We introduce DPVS : a dynamic backjumping search strategy. It behaves well on this application: DPVS and CBMC have similar performances on three properties of the Flasher Manager but DPVS outperforms CBMC to nd a counterexample for two other properties.

Outline of the paper

We rst recall the basics on constraint-based bounded model checking. Then, we introduce the search strategy we have developed to handle the Flasher Manager application. Next, we describe the Flasher Manager application, a real time industrial application from a car manufacturer. We describe the Simulink module of the Flasher Manager and the properties we have to check. We also explain how the Simulink module and the properties have been translated into C programs which are used as inputs to the bounded model checkers. Finally, we report experiments on the Flasher Manager application with DPVS and with CBMC.

Constraint-based BMC

We rst recall some basics on Constraint Programming (CP) techniques [START_REF]Handbook of Constraint Programming[END_REF] that are useful to understand the rest of the paper; the reader familiar with CP techniques can skip the next subsection.

In a second part, we introduce constraint-based BMC and the DPVS strategy. [START_REF]Handbook of Constraint Programming[END_REF], Part II).

Basics on CP

The key features of CP are:

1 Otherwise, the compiler from Simulink to C should be formally veried.

Domain ltering that considers each constraint separately and removes values that are trivially inconsistent; Search strategies that try to exploit the structure of the problem; Global constraints that use (ecient) specic polynomial algorithms for some subclasses of constraints.

To illustrate the intuition behind domain ltering consider the following example: variables/domains:

x 1 ∈ {1, 2}, x 2 ∈ {0, 1, 2, 3}, x 3 ∈ {2, 3}; constraints: {x 1 > x 2 , x 1 + x 2 = x 3 , alldifferent(x 1 , x 2 , x 3 )}.
A naive search process would explore the following tree, starting by assigning 1 to variable x 1 :

However, if we just consider constraint x 1 > x 2 , we can remove values {2, 3} from the domain of variable x 2 .

That is what domain ltering does in the rst step. Then, the search process starts on the following reduced search tree:

Value 1 is assigned to variable x 1 and the ltering process is restarted. Now, if we consider constraint x 1 + x 2 = x 3 the domains of variables x 2 and x 3 become empty. So, we will backtrack and assign value 2 to variable x 2 . The ltering process will use again constraint x 1 + x 2 = x 3 to remove value 0 from the domain of variable The eciency of the solver highly depends on search strategies. These strategies use heuristics for choosing the variable to instantiate and for choosing the value for the selected variable. First fail is one of the most popular heuristic. The intuition behind First fail is: "to succeed, try rst where you are most likely to fail".

CP framework & BMC: overview

The goal of BMC is to mechanically check properties of models. In BMC, the falsication of a given property is checked for a given bound k. BMC mainly involves three steps:

1. The program is unwound k times.

2. The unwound program and the property are translated into a big propositional formula φ. φ is satisable iff there exists a counterexample of depth less than k.

3. A SAT-solver or SMT-solver is used for checking the satisability of φ.

In our CP framework, the falsication of a given property is also checked for a given bound and also involves three steps:

1. The program is unwound k times.

2. An annotated and simplied CFG is built.

3. This CFG and the specication are translated into constraints on the y. Unfeasible paths are pruned as early as possible.

The main dierence between the two approaches are:

Standard BMC builds a big propositional formula whereas CP-based BMC generates constraints on the y, according to the exploration strategy of the CFG.

Standard BMC uses ecient SAT-solvers (or more recently SMT-solvers) whereas CP-based BMC uses a set of solvers, some of which are well suited for handling numeric expressions.

CP framework & BMC: details

More precisely, consider a program P with pre-condition pre, post-condition post which is a conjunction of some properties, and a particular property prop from post 8 .

The following pre-processing steps are rst performed:

1. P is unwound k times yielding program P uw ; 2. P uw is then translated into DSA Puw , its DSA (Dynamic Single Assignment) form [START_REF] Barnett | Weakest-precondition of unstructured programs[END_REF], where each variable is assigned exactly once on each program path;

3. DSA Puw is simplied according to the specic property prop by applying slicing techniques 9 ; 4. the CFG (called G) of the simplied DSA Puw is built; 5. the domains of all the variables of G are ltered by propagating constant values along G.

Then, G is explored and a constraint system is generated on the y as follows:

1. A constraint system CS is created and initialized with the constraints associated with the pre-condition pre and the negation of the property to be proven ¬prop. To increase performances, our constraint framework is parametrized with a list of solvers which are tried in sequence, starting with the least expensive and the least general one. Our prototype implementation uses a linear programing solver, a mixed integer-programming system and a nite domain constraint solver. In step 2, the feasibility check is only a partial consistency test: it may not detect some inconsistencies. In contrast, in step 3, the constraint system solving relies on a complete decision procedure.

As we already mentioned, the main dierence with standard BMC that uses a SAT or SMT solver is that our constraint-based BMC approach builds the constraint 8 post is a conjunction, so its negation (which is added into the constraint system) is a disjunction. Practically, it is often more ecient to handle each conjunct individually. 9 We perform a static backward program slicing similar to the cone-of-inuence computed in hardware model checking, i.e. we only keep program statements that may modify directly or indirectly the value of the variables in the property to check. system on the y during CFG exploration. A major lever to improve our method is therefore the way the CFG is explored. Thus, we developed search strategies that best meet the following objectives:

1. cut unfeasible paths as early as possible; 2. when there is a counterexample, explore the faulty path as early as possible.

The rst strategy we have developed was a naive depth rst search strategy, called CPBPV [START_REF] Collavizza | A constraint-programming framework for bounded program verication[END_REF]. This strategy was successful on academic benchmarks, in particular for programs with a strong pre-condition like the binary search program. However, this strategy fails on the Flasher Manager application because it has no precondition and its main function manages many functionalities while the properties to be proven cover a small subset of these functionalities (see discussion in Sect. 5).

We have thus developed the DPVS search strategy that takes benets of the post-condition to explore the CFG in a bottom-up way. This is detailed in the next subsection.

DPVS: a dynamic backjumping search strategy

Contrary to CPBPV, DPVS is a non-sequential bottomup strategy which has been designed to nd counterexamples for program properties. In DPVS, the exploration of G is guided by the variables. The rst explored node is the post-condition. Then DPVS jumps to a node where a variable of the post-condition occurs, and so on. At each step, the explored node provides constraints on a variable of the post-condition or a variable linked to a variable of the post-condition. Practically, DPVS uses a queue of variables with various ordering heuristics. This strategy is based on the following observation: when the program is in an SSA-like form 10 , a path can be built in a dynamic way. In other words, the CFG does not have to be explored in a top-down or bottomup sequential way: nodes can just be collected as needed.

When a path is correct or not executable, that is to say when the collected constraints and the negation of the post-condition are inconsistent, this strategy can detect the inconsistency before all the nodes of the path have been explored. Of course, when a path is faulty, all the nodes of the path have to be visited for generating a valid counterexample.

Next section explains how DPVS works in an informal way. 10 SSA (Static Single Assignment) form is an intermediate representation used in compilation: it is a semantics-preserving transformation of a program in which each variable is assigned exactly once [START_REF] Cytron | Eciently computing static single assignment form and the control dependence graph[END_REF]. Because our method is dynamic and proceeds path after path, we actually use DSA form: variables are dened once on each path only [START_REF] Barnett | Weakest-precondition of unstructured programs[END_REF]. The constraint based dynamic exploration of G works as follows. DPVS uses a constraint store S and a queue of variables Q. Q is initialized with the variables in prop, written V (prop) in the following; S is initialized with pre and the negation of prop. As long as Q is not empty, DPVS dequeues the rst variable v and searches for a program block where variable v is dened. All new variables of the denition of variable v, except input variables, are enqueued on Q. The denition of variable v as well as all conditions required to reach the denition of v are added to the constraint store S. If S is inconsistent, DPVS backtracks and searches for another denition; [START_REF] Collavizza | A constraint-programming framework for bounded program verication[END_REF] where variable c 1 is dened. Constraint c 1 = c 0 + d 0 + e 0 is added to the constraint store and variable c 0 is added to Q. Then, the search process selects node [START_REF] Barnett | Weakest-precondition of unstructured programs[END_REF] where variable c 0 is dened. To reach node (4), the condition in node 0 must be true. Thus, this condition is added to the constraint store S and the other alternative (a 0 < 0) is cut o. At this stage (see Fig. 2), S contains the following constraints: {c 1 < d 0 +e 0 ∧c 1 = c 0 +d 0 +e 0 ∧c 0 = a 0 ∧a 0 ≥ 0} which can be simplied to {a 0 < 0 ∧ a 0 ≥ 0}. This constraint store is inconsistent and thus DPVS selects node [START_REF] Botella | Symbolic execution of oating-point computations[END_REF] where variable c 0 is also dened. To reach node [START_REF] Botella | Symbolic execution of oating-point computations[END_REF], the condition in node 0 must be false. Thus, the negation of this condition is added to the constraint store S and the other alternative is cut o. Now (see Fig. 3), constraint store S contains the constraints {c

1 < d 0 + e 0 ∧ c 1 = c 0 + d 0 + e 0 ∧ c 0 = b 0 ∧ a 0 < 0 ∧ d 0 = 1 ∧ e 0 = -a 0 } which can be simplied to {a 0 < 0 ∧ b 0 < 0}. This constraint
store is consistent and the solver will compute a solution, e.g., {a 0 = -1, b 0 = -1}. These values of the input variables are a test case that demonstrates that program f oo violates property p 1 . DPVS was able to nd this counterexample without ever visiting nodes ( 5), ( 6) and (7).

This small example illustrates how DPVS works in a general way. It can also help to understand the intuition behind this new strategy: DPVS collects incrementally all the information on the variables that occur in postcondition to detect inconsistencies as early as possible;

this is especially ecient when a small subset of the constraint system is inconsistent.

Next subsection details algorithm DPVS. DPVS either returns an instantiation of the input variables of P satisfying constraint system S or it returns ∅ if S does not have any solution. Solutions are computed by function solve (line 28), using the nite domain solver (CP). Function solve is a complete decision procedure over the nite domains. On the contrary, function isfeasible used in line 33 only performs a partial consistency test. In other words, it detects some inconsistencies but not all of them. However, function isfeasible is much faster than function solve; this is the reason why we chose to perform only this test each time the constraints derived from the denition of a variable are added to the constraint store. This partial consistency check can either be done with the nite domain solver (CP) or with the linear programming solver (LP) on a linear relaxation of the constraint system. Thus, the solve function is called only once when the end of a path has been reached.

Soundness of Algorithm 1

It is easy to show that Sol , the solution computed by DPVS, is actually a counterexample. Indeed, these values of the input data satisfy the constraints generated from:

pre, the required pre-condition; ¬prop, the negation of a conjunct of the post-condition; one denition of all variables in V (prop) and one definition of all variables (except the input variables) introduced by these denitions; all conditions required to reach the above mentioned denitions.

Thus, there exists at least one executable path which takes as input values Sol and computes an output that violates the property prop.

Conversely, if there exists a counterexample violating prop, then there exists at least one executable path in the CFG corresponding to this case. Algorithm 1 guaranties that: any node with a denition of a variable involved in prop is explored (with the corresponding constraints added to S); any conditional node ancestor of an explored node is considered with the appropriate predicate added to

S;

any node with a denition of a variable used in an explored node is also explored (with the corresponding constraints added to S).

Consequently, a consistent constraint system S corresponding to the faulty path has been built and solved by Algorithm 1. The solution of this constraint system provides a counterexample of prop.

Otherwise, when no solution can be found, we can state that there does not exist any input values violating property prop; in other words, no counterexample can be found with the boundedness hypothesis.

Q = ∅ 1: v ← POP(Q) 2: for all n ∈ def _nodes[v] do 3: Cut ← false; SAVE(S, Q, M, choice) 4: S1 ← S∧ cstr (def [v, n]) {% def [v, n] denotes the denition of v in node n} 5: Vnew ← V (def [v, n]) \ M 6: PUSH(Q, Vnew ); add(Vnew , M ) 7:
for all anc ∈ cond _anc[n] do This real time industrial application from a car manufacturer has been provided by Geensoft / Dassault Systems 12 . The Flasher Manager application was designed and simulated using the Simulink platform. Its specication was given by Geensoft and consists of four main properties. The Flasher Manager is concretely embedded as a C program in a car computer, thus our aim is to check that the four properties are preserved on this C program. This is a challenging software verication problem: its complexity comes from the size of the C function generated from the Simulink module and from the number of clock cycles required for verifying each property.

We rst describe the Simulink module of the Flasher Manager, then the properties we have to check and last, we explain how the Simulink module and the properties have been translated as a C program in order to use a bounded model checker for the verication. A description of this application with all source code can be found at the address: http://hal.archives-ouvertes. fr/hal-00720921.

Description of the Simulink module

The Flasher Manager is a controller that drives several functions related to the ashing lights of a car. Each function is enabled by some input commands, activates one or two ashing lights, and is described by its duration and its ashing period (i.e., time-units required to oscillate from 1 to 0 or 0 to 1). The next subsections detail these points for the three main functionalities of the Flasher Manager. Figure 4 shows a simplied Simulink model (i.e., inputs/outputs) and Fig. 5 provides a more detailed model. Then, when the input falls back to 0, the corresponding output light stops ashing. The light starts oscillating immediately when the command is enabled, and stops immediately when the command is disabled. These are the Flashers_left and Flashers_right functions.

Lock and unlock of the car

The driver has the ability to lock and unlock the car from the distance using an RF-key. The state of the unlock and lock buttons of the key is reported to Boolean inputs ULK and LK respectively.

When an RF-key is pressed, the manager indicates the state of the doors to the user using the following convention:

If the unlock button is pressed while the car is unlocked, nothing shall happen.

If the unlock button is pressed while the car is locked, both lights shall ash with a period of 2 time-units during 20 time-units (fast ashes for a short time).

More precisely, when the ULK input is activated, the oscillation starts two cycles after the activation, produces an output sequence of the form [10101...010] on both lights and stops on the 22 nd cycle after the activation. This is the Unlock_flash function.

If the lock button is pressed while the car is unlocked, both lights shall go on for 10 time-units, and then shall go o for another 10 time-units, producing an output sequence of the form [11111111110000000000] on both lights.

If the lock button is pressed while the car is locked, both lights shall ash during 60 time-units with a period of 2 time-units (fast ashes for a long time).

More precisely, when the LK input is activated, the oscillation starts the next cycle, produces an output sequence of the form [10101...010] on both lights that stops on the 61 st cycle. This is the Lock_flash function. It is typically used to locate the car in an overlled place.

Note that in the initial state, the doors are locked.

Warning function

Finally, the driver has the ability to press the warning button. When the warning is on, both lights ash with a period of 6 time-units (slow ashes). This is the Warning function. The W input is a push-down button. In the initial state of the manager, the warning is o. A rising edge of W activates the warning and the next rising edge of W deactivates the warning.

Properties

We worked on the following four properties of the Flasher Manager module. Restrictions For checking these properties, we adopted the following restrictions in accordance with the designers of the Flasher Manager module:

1. L and R inputs cannot both be TRUE on the same cycle; 2. LK and ULK inputs cannot both be TRUE on the same cycle.

First restriction means that we do not consider a degraded use when the lever of the indicators is damaged.

Second restriction excludes a misuse of the RF-key.

The next subsection describes how the four properties have been modeled as C programs in order to be checked with bounded model checkers.

Programs under verication

We rst describe the C function built from the Simulink model, then we give the general principles to model the properties as C programs using this function, and last we detail each property.

Function f1

The Simulink model of the Flasher Manager was automatically translated into a C function, named f1, using a Geensoft proprietary tool. This function f1, together with the scheme of the Simulink model and an informal textual description of the properties of the module, is the material that was provided to us by the designers. Function f1 involves 81 Boolean variables including 6 inputs and 2 outputs and 28 integer variables. It contains 300 lines of code and mainly consists of nested conditionals including linear operations and constant assignments, as illustrated by the piece of code displayed in Fig. 6.

A call to function f1 simulates one cycle of the Simulink module: state variables and output variables are modied according to the values of the input variables. In order to verify the properties using a BMC tool, we associate a C program to each property. Such a program starts with a call to the function that initializes the module, and then mainly consists of a loop that:

1. reads the inputs, 2. calls function f1, 3. states some assertions on the outputs; these assertions may depend on current and previous values.

In step 1, unknown input values are represented by a call to function nondet_in(). This is the syntax required by the BMC tools we use. Statement int v=nondet_in() is translated by our BMC tools as the creation of a variable v with an initial domain that contains the whole set of machine integers (the integer format can be set as an option of the BMC tools). In step 3, we use some assert statements which are checked in sequence by the BMC tools.

For each property, the loop must be checked for a number of iterations that is tractable, but nevertheless meaningful. BMC tools make a bounded verication. Generally, the bound is progressively increased until an error is found, or the size of the formula is too large and exceeds the capacity of the tool. For the Flasher Manager module, the longest function is the Lock_flash function: it requires 61 cycles. However, in our experiments (see Sect. 4), properties often require much more cycles.

Property 1

To check the property 1, we have to show that whatever input commands are, if the warning is on, the lights must ash as described by the Warning function: both lights shall oscillate with a time period of 6 time-units. The If Won is TRUE, then the lights shall oscillate with a time period of 6 time-units, producing an output sequence of the form [111000111000...]. We use a variable count that counts the number of cycles since Won is true. Value of variable count is set to 0 on each rising edge of W (line 20), and is increased when Won is true (line 34). count/3 brings the oscillation back to a one time-unit oscillation. Since the oscillation starts with 1, the lights shall be TRUE when (count/3)%2==0 and shall be FALSE when (count/3)%2==1. The assert statements at lines 31 and 33 are stating this.

Property 3

Property 3 concerns the behavior of the module when the ashing function is deactivated, i.e., input signal F is FALSE. We wrote two versions of this property: Properties 3a and 3b. Property 3a corresponds to the original property which states that F=FALSE deactivates the Flashers_left, Flashers_right and Warning functions, but does not deactivate the functions related to lock and unlock commands. However, we restricted LK and ULK inputs so that they are ignored while a ashing function due to a previous lock or unlock of the car is not yet completed. Even with this restriction on the combinations of LK and ULK inputs, Property 3a is not tractable because of combinatorial explosion (see Sect. to the resolution of the constraint problems issued from our experiments. Thus, each experiment was ran with the default solver of each tool and with the z3 SMT solver [START_REF] De Moura | Z3: An ecient SMT solver[END_REF] as an alternative solver.

First, we outline in Sect. 4.1 the strategies and tools involved in the experiments, then we detail the results, property by property, in Sect. 4.2.

Strategies and tools

DPVS is a strategy that we devised for constraint-based bounded model checking. DPVS was presented in details in Sect. 2.4; here, we only give an insight into the implementation. We also briey recall the main features of CBMC and z3. Our prototype works from an XML representation of imperative programs. This allows our tool not to be tied to a single programming language. Simple translators from actual programming languages into the XML format are available, e.g., for C and Java. The current prototype imposes many restrictions on the C programs. Especially, input data are restricted to Booleans, integers and arrays of these primitive types. Pointers are not handled.

Run-time errors e.g., division by zero are not checked for. However, the prototype has all the C language features required for the Flasher Manager properties. In particular, function calls are inlined.

As presolving, DPVS performs constant propagation and program slicing. Slicing is done backward on the CFG in DSA form. It removes all assignments of variables not relevant to the property to check. Useless nodes are removed from the CFG.

Comet has a default nite domain constraint solver which we used in the experiments; this default solver is denoted by CP in the results. However, Comet also allows to call other solvers in the form of external libraries. Thus, we developed an interface to call z3 instead of Comet's default solver.

CBMC

CBMC [START_REF] Clarke | A tool for checking ANSI-C programs[END_REF] is a state-of-the-art bounded model checker for ANSI-C and C++ programs. It allows the verication of array bounds (buer overows), pointer safety, exceptions, and user-specied assertions. CBMC builds a propositional formula whose models correspond to execution paths of bounded length k violating some property of a program. This formula is then checked for satisability using a SAT solver. If the formula is satisable, the given property does not hold; otherwise, the property is guaranteed to hold up to k steps.

CBMC also oers the option to use z3 instead of the embedded SAT solver, but this is yet an experimental 13 See http://dynadec.com feature. For the experiments, we used CBMC version 3.6 since this was the latest version to correctly work with z3.

CBMC was called without any specic option except for specifying the unfolding bound with --unwind, the size of integers (32 bits) and the function to check with --function. In particular, all optional checks were disabled. Moreover, CBMC implements its own slicing techniques. We chose the one that gave the best results in the experiments when increasing loop unfoldings.

z3

SMT-based model checking has been proposed as a generalization of SAT-based model checking to address the state space explosion problem. The idea is that parts of the model could be more easily expressed and more eciently solved in more general, but still decidable, theories than propositional logic. SMT solvers integrate dedicated solvers for the dierent theories and share some of the motivations of constraint programming. SMT-based model checking has already been used with success in [START_REF] Armando | Bounded model checking of software using SMT solvers instead of SAT solvers[END_REF][START_REF] Cordeiro | SMT-based bounded model checking for embedded ANSI-C software[END_REF].

For the experiments, we used the SMT [START_REF] De Moura | Z3: An ecient SMT solver[END_REF]

Results

We report in the following sections on the time spent by the tools to check the Flasher Manager properties. We give both presolving and search times when relevant.

For DPVS, presolving time is used for building the simplied unfolded control ow graph from the XML representation of the program of a property.

For CBMC, presolving time is the time spent to translate the C program into a Boolean formula.

Presolving time also includes applying several simplication techniques (e.g., cone of inuence, constant propagation), which may dier according to the tool.

Search time is the time actually spent for searching for a solution, that is total time of the experiment minus presolving time. For CBMC, it corresponds to the time spent in the solver (SAT or SMT), whereas for DPVS it covers the time needed to dynamically explore the control ow graph and to solve the constraint systems.

A time limit of 10 minutes was allowed for each experiment, beyond which we stopped the experiment and reported a time-out (T.O.). CBMC performs very well on this property where a counterexample can be found with very few unfoldings.

DPVS behaves also well: the presolving simplications require more time but the search process is very fast.

Note that the implementation of the presolving in DPVS has not been optimized at all.

On this property, the search time is much more important when z3 is used instead of the native solvers of the dierent systems.

Property 2

This property is much more complex than Property 1:

it involves nested loops and numerous conditional statements with combinations of disjunctions and conjunctions. None of the used tools could check the property within the 10-minute time limit, even for 10 unfoldings. CBMC did not nish building the Boolean formula. DPVS could build and simplify the control ow graph in around 40 s, but it reached the time limit during search. This property is not easy to reformulate in a more tractable form without losing its semantics. It shows that a relatively simple application as the Flasher Manager is still challenging for modern bounded model checking tools.

Property 3

The unrestricted version of Property 3, Property 3a, could not be checked within the 10-minute time limit. At least 120 unfoldings are required to include one sequence of all the lock and unlock related functions. However, for 100 unfoldings, CBMC fails to build the Boolean formula within the time limit. DPVS could build and simplify within the time limit the control ow graph for 100 unfoldings but DPVS failed to nish the graph exploration.

There are less combinations on the inputs for Property 3b since lock and unlock inputs are set to false.

Figure 13 shows that DPVS and CBMC could check the property up to 300 unfoldings within the time limit.

On small number of unfoldings, CBMC performs better than DPVS, but DPVS scales better than CBMC : at around 100 unfoldings and above, DPVS is faster. DPVS could even check the property for 400 unfoldings.

As with Property 1, the use of z3 increases the search time by a factor ranging from 2 to 4. Neither DPVS nor CBMC found any counterexample within the unfolding bounds. This means that DPVS had to explore all executable paths relevant to this property.

Property 4

Property 4 is false if there are combinations of inputs so that one of the light remains always lit. However, in bounded model checking we cannot show that a light is actually always lit. We can only increase as much as possible the unfolding bound and show that on the corresponding time duration a light remains lit. Figure 14 reports the CPU time required to nd a counterexample to Property 4 when the number of unfoldings increases. DPVS outperforms CBMC for this property. DPVS allows to reach up to 1600 unfoldings whereas CBMC fails at 200 unfoldings within the 10-minute time limit. In typical settings, 1600 cycles of the Flasher Manager control loop are more than 13 minutes of working, which seems to be a reasonnable bound according to the Flasher Manager designers.

Presolving and search times for CBMC and DPVS are given in Fig. 15. DPVS search time is very low compared to presolving time. In bounded model checking, the bound is usually progressively increased. So, in an optimized system the total checking time could benet from an incremental building of the control ow graph from one unfolding bound to another, instead of rebuilding the graph from scratch for each bound as done here.

DPVS & CPBPV

We designed DPVS because CPBPV was not able to prove or disprove any property of the Flasher Manager application at a reasonable depth. We evaluated various strategies in our framework, but only DPVS worked. In particular, performances of a sequential backward strategy were even worse than those of the depth-rst strategy of CPBPV.

We also tested DPVS on other well known examples: the Tritype program for triangle classication [START_REF] Collavizza | A constraint-programming framework for bounded program verication[END_REF], On the contrary, DPVS and CPBPV have very different performances on the Binary search example. The characteristic of this example is that it is correct, which means that all executable paths must be explored, and above all, it has a very strong pre-condition. Thus a top-down strategy like CPBPV is well adapted to take advantage of this pre-condition for cutting unfeasible paths, i.e., paths where the array is not sorted. CPBPV incrementally adds the decisions taken along a path. This is particularly well adapted for the Binary search program, which has a strong pre-condition. This pre-condition combined with the decisions taken along a path have a strong impact on feasibility of the next conditions and help to prune infeasible paths. This benchmark clearly shows that neither DPVS nor CBMC work well on all problems. Of course, this is due to the combinatorial complexity behind the used algorithms. However, we can point out that DPVS and CBMC are much more ecient than CPBPV for (partially) proving properties on real applications without a complete formal specication.

There are no pointers in the code of the Flasher Manager application. However, in a new version of DPVS, we implemented a point-to analysis quite similar to the one done in Euclide [START_REF] Gotlieb | Euclide: A Constraint-Based Testing Framework for Critical C Programs[END_REF]. Thanks to constraint propagation, slicing is still ecient. Experiments on academic benchmarks are encouraging but they still have to be validated on more complex applications.

Related work

Standard bounded model checkers transform a program and a property into a Big Boolean formula and use SAT solvers to prove that the property holds or to nd a counterexample [START_REF] Silva | A survey of automated techniques for formal software verication[END_REF]. SMT solvers are now used in most of the state-of-the-art BMC tools to directly work on high-level formula (see [START_REF] Armando | Bounded model checking of software using SMT solvers instead of SAT solvers[END_REF][START_REF] Ganai | Accelerating high-level bounded model checking[END_REF][START_REF] Cordeiro | SMT-Based Bounded Model Checking for Embedded ANSI-C Software[END_REF] and CBMC ). Many improvements have been studied for high-level BMC, such as the one proposed in [START_REF] Ganai | Accelerating high-level bounded model checking[END_REF], in particular during the unfolding step and to reuse previously learned lemmas. But to the best of our knowledge, these approaches do not explore the CFG in a dynamic bottom-up approach that collects non consecutive program blocks.

Constraint Logic Programming (CLP) was used for test generation of programs (e.g., [START_REF] Gotlieb | Automatic test data generation using constraint solving techniques[END_REF][START_REF] Jackson | Finding bugs with a constraint solver[END_REF][START_REF] Sy | Automatic test data generation for programs with integer and oat variables[END_REF][START_REF] Albert | Test Data Generation of Bytecode by CLP Partial Evaluation[END_REF]) and provides a nice implementation tool extending symbolic execution techniques [START_REF] Botella | Symbolic execution of oating-point computations[END_REF]. Gotlieb et al. showed how to represent imperative programs as constraint logic programs: InKa [START_REF] Gotlieb | Automatic test data generation using constraint solving techniques[END_REF] was a pioneer in the use of CLP for generating test data for C programs.

GATeL [START_REF] Marre | Test sequences generation from lustre descriptions: Gatel[END_REF] JAUT [START_REF] Charreteur | Constraint-based test input generation for java bytecode[END_REF] is a constraint-based tool for generating automatically unit tests for Java bytecode programs. Like in CPBPV and in DPVS, the constraints are generated on the y in JAUT. However, the exploration strategy is a sequential backward strategy since the goal of JAUT is to generate test input for executing some specic locations in a program.

To sum up, besides the fact that our system is not dedicated to generating test cases but to disproving properties, the main dierence between our approach and all these systems is that DPVS is based on a dynamic backjumping strategy.

Conclusion

In this paper, we have introduced DPVS, a dynamic constraint based strategy for bounded model checking.

Experiments with DPVS are very encouraging: DPVS behaves very well on a non trivial real application. Generating test cases for realistic time periods is a critical issue in real time applications. For the Flasher Manager application, DPVS generated counterexamples for more signicant time periods than CBMC. These results are impressive since DPVS is still an unoptimized prototype whereas CBMC is a state-of-the-art solver.

In this paper, we have also provided a new industrial case study. We have proposed models of the dierent properties to prove 15 and evaluated dierent tools and strategies. Although this application seems quite simple in regard to other applications like ABS controllers, some properties could neither be proven nor disproven by the tools we evaluated. So, it is still a challenge for state-ofthe-art bounded model checkers.

The backjumping strategy of DPVS is well adapted for problems with a strong post-condition. In contrast, 14 Euclide [START_REF] Gotlieb | Euclide: A Constraint-Based Testing Framework for Critical C Programs[END_REF] could not handle the Flasher Manager application due to a bug. On academic benchmarks and on the well-known TCAS (Trac Collision Avoidance System) application, CBMC, DPVS and CPBPV outperformed Euclide (see [START_REF] Nguyen | Stratégies dynamiques pour la génération de contre-exemples[END_REF]). the top-down strategy of CPBPV is much more ecient for problems with a strong pre-condition, like the Binary search benchmark. Clearly, it would be worth investigating new strategies combining the capabilities of DPVS and CPBPV.

Future work also concerns extending our prototype to be able to evaluate the proposed approach on a larger class of programs. We are working on a new version that is interfaced with a oating-point number solver [START_REF] Botella | Symbolic execution of oating-point computations[END_REF].

Our system does not handle run-time errors. However, tools dedicated to reporting possible run-time errors and based on abstract interpretation (ASTRÉE [START_REF] Cousot | Varieties of static analyzers: A comparison with ASTRÉE[END_REF],

FLUCTUAT [START_REF] Delmas | Towards an industrial use of uctuat on safety-critical avionics software[END_REF] for instance) could be used in conjunction with DPVS.

We are also working on a solver more adapted to software verication problems, for instance a solver that handles disequalities in a more ecient way. Let us explain this point on a small example. Consider a test such that x == y, the negation of this test corresponds to the constraint x = y. If the domains are large, consistency checks with CP may be very costly; if we want to use LP, we have to create two choice points: x < y and x > y.

  x 2 and the global constraint alldifferent to remove value 2 from the domain of variable x 3 . Thus, we only needed two assignments to nd the unique solution. The nal search tree is: Global Constraints are very important to solve dicult problems. The alldifferent global constraint [30] is one of the most famous global constraint. It uses matching algorithms for bipartite graph and network ow algorithms to handle a set of constraints of the form x i = x j . In program verication, we can use a linear programming solver (LP) as a global constraint for handling a set of linear constraints.

Fig. 1 .

 1 Fig. 1. Program foo

Fig. 2 .

 2 Fig. 2. Simplied CFG for p 1 , step 1

Fig. 3 .

 3 Fig. 3. Simplied CFG for p 1 , step 2

Algorithm 1 :

 1 DPVSFunction DPVS (S, Q, M, choice) returns a counterexample Require:

Fig. 4 .

 4 Fig. 4. Simplied Simulink model of the Flasher Manager

3. 1 . 1 Fig. 5 .

 115 Fig. 5. Detailed Simulink model of the Flasher Manager

Property 1 :

 1 "Warning function has priority over other ashing functions." Property 2: "When the warning button has been pushed and then released, the Warning function resumes to the Flashers_left (or Flashers_right) function, if this function was active when the warning button was pushed." Property 3: "When the F signal (for asher active) is o, then the Flashers_left, Flashers_right and Warning functions are disabled. On the contrary, all the functions related to the lock and unlock of the car are maintained." Property 4: "Lights should never remain lit innitely."

Fig. 6 .

 6 Fig. 6. Piece of code of function f1

C

  program used to model this property (called prop1) is shown in Fig. 7: Each iteration of the main loop (line 8) is a clock cycle where input values are read (lines 9 to 15) and function f1 is called (line 25). Note that lines 11 and 13 apply the restrictions mentioned in Sect. 3.2.

3. 3 . 4 2 Property 2

 3422 Property concerns a scenario that hosts three successive events: a direction change, a warning activation, and a warning deactivation. Since Property 1 is false (because lock and unlock functions have priority on the warning), we set the entries LK and ULK to FALSE to simplify the modeling. Experimental results (see Sect. 4.2.2) show that even this simplied version is not tractable. The C program associated with property 2 (called prop2 and shown in Fig. 8), works as follows: It uses counter countR (resp. countL) to count the number of cycles since R (resp. L) has been TRUE. Note that countL has the initial value -2 because a left direction change activates the left light on the next cycle of the rising edge of L. The rst loop (line 11) is used to repeat the scenario. When the warning is activated, and a right or left direction change is also active (line 22), then another loop starts and stops when the warning is cut down (line 24). When the warning has been cut and a right or left direction change is active, the lights shall behave as the Flashers_left or Flashers_right functions (lines 38 to 49).

Fig. 9 .Fig. 12 .

 912 Fig. 9. Function under verication for Property 3b: left, right and warning ashing functions

4. 1

 1 .1 DPVS DPVS is implemented in Comet [27]: a hybrid optimization platform for solving complex combinatorial optimization problems. Comet combines the methodologies used for constraint programming, linear and integer programming, constraint-based local search, and dynamic stochastic combinatorial optimization with a language for modeling and searching 13 .

Fig. 13 .

 13 Fig. 13. Total time in seconds for checking Property 3b (without lock and unlock functions) when varying the number of unfoldings

Fig. 14 .

 14 Fig. 14. Total time in seconds for checking Property 4 when varying the number of unfoldings

Fig. 15 .

 15 Fig. 15. Presolving and search times in seconds for checking Property 4 when varying the number of unfoldings

  is a testing environment for Lustre and SCADE programs which belongs to the family of CLPbased test generation and verication tools. The LUS-TRE language is declarative and describes synchronous data-ow computations. GATeL interprets the language constructs as Boolean and integer interval constraints. Test sequence generation is automated using constraint logic programming techniques. Recently, in [6], the authors added explicit constraints to manage the clock type hierarchy as well as constraints reecting properties of state-machines built by SCADE. In other words, the authors provide a CLP interpretation of the multi-clocked kernel of the SCADE language. The constraint management rules are based on sequential backward derivations. Denmat et al. developed TAUPO, a successor of InKa which uses dynamic linear relaxations [19]. It increases the solving capabilities of the solver in the presence of non-linear constraints but the authors only published experimental results for a few academic C programs. Euclide [22] is also a successor of InKa. It has three main functions: structural test data generation, counterexample generation and partial program proving for critical C programs. Euclide combines standard constraint programming techniques and specic techniques to handle oating-point numbers and linear constraints. C programs are translated into an Euclide program. After a constraint propagation step, the constraint solvers of Euclide start a variable labelling step to nd a solution. That is to say, all constraints are posted before the propagation and search processes start. So, the search strategy of Euclide only concerns the choice of values for variables whereas in DPVS, the search selects the constraints that have to be posted 14 .

  3 , or-tools 4 ) and academic solvers (e.g., Gecode 5 , Choco 6 , Minion 7 ) are avail-

	able. There are many successful industrial applications,
	e.g., timetabling (Dutch railway), hardware verication
	(Intel), scheduling, planning (see

  [START_REF] Armando | Bounded model checking of software using SMT solvers instead of SAT solvers[END_REF]. Nodes of G are translated and added to CS on the y. If the current node n is non-conditional, then it is simply translated as a constraint and added to CS.

	If n is a conditional node, then its condition is tem-
	porarily added to CS to check its feasibility. If it is
	not consistent with CS, the corresponding path is
	cut.
	3. When the end of an execution path has been reached,
	CS is solved. If a solution is found, this solution is
	a counterexample since it satises the constraints of
	the pre-condition, of the program path and of the
	negation of the post-condition. If CS does not have
	any solution, the program is correct along this path
	(under the boundedness hypothesis).

Table 1 .

 1 Presolving, search, and total times in seconds for checking Property 1 with 10 unfoldings

	Tool	Presolving	Search	Total
	CBMC	0.89	0.23	1.12
	CBMC z3	0.85	2.7	3.55
	DPVS DPVS z3	3.89	0.08 0.34	3.97 4.23
	All the properties of the experiments are expressed
	as safety properties. In bounded model checking, the
	greater is the number of unfoldings the more condent
	one can be that the property holds. For the experiments,
	we started with a bound of 10 unfoldings which we in-
	creased next until we reached the given time limit.
	All benchmarks were run on a 64-bit Linux quad-core
	Intel Xeon (3.16 GHz) platform with 16 GB of RAM.
	However, tools were run on a single core and did not
	take advantage of the three supplementary cores. More-
	over, to our knowledge, CBMC 3.6 only exists in 32-bit
	version.
	4.2.1 Property 1
	Property 1 states that the warning function should have
	priority over the other ashing functions. This prop-
	erty does not hold: the lock and unlock ashing func-
	tions have priority over the warning function. All the
	tools found a counterexample with our starting bound
	of 10 unfoldings. Actually, 3 unfoldings are enough for
	the shortest counterexample. The results are shown in

Table 1 .

 1 z3 subscripts denote versions of the tools that use z3 instead of the native solvers of the tools.

Table 2 .

 2 Total time in seconds for checking Property 3b (without lock and unlock functions) when varying the number of unfoldings

	Unfoldings	CBMC	CBMC z3	DPVS	DPVS z3
	10	0.56	0.7	3.04	3.44
	50	6.56	7.11	16.59	21.02
	100	44.71	53.72	37.47	55.92
	200	202.18	288.76	94.8	155.33
	300	510.91	T.O.	152.88	307.65
	400	T.O.	T.O.	248.31	576.18

Table 3 .

 3 Presolving, search, and total times in seconds for checking Property 4 when varying the number of unfoldings

	Unfoldings	CBMC

Table 4 .

 4 Time in seconds for checking the Binary search benchmark when varying the array length (with 16-bit integers)

	Array length	CBMC	DPVS	CPBPV
	4	5.732	0.529	0.107
	8	110.081	35.074	0.298
	16	T.O.	T.O.	1.149
	32	T.O.	T.O.	5.357
	64	T.O.	T.O.	27.714
	128	T.O.	T.O.	153.646
	the TCAS program from avionics [23], and the Binary
	search that determines whether a value v is present in a
	sorted array t. DPVS and CPBPV have similar perfor-
	mances on the two rst examples, and compare favorably
	with CBMC. The main impact on performances for both
	DPVS and CPBPV is the way we combine the solvers,
	i.e., CP and LP solvers.

Table 4

 4 reports the results of the experiments on a correct version of the Binary search program. CBMC and DPVS cannot handle well this benchmark. CBMC wastes a lot of time in building and exploring the whole formula. DPVS strategy is not well adapted for this very specic program. On the contrary, the top-down strategy used in CPBPV outperforms the other checkers.

http://www-01.ibm.com/software/integration/ optimization/cplex-optimizer/

http://dynadec.com/

http://code.google.com/p/or-tools

http://www.gecode.org

http://www.emn.fr/z-info/choco-solver/

http://minion.sourceforge.net

Notation (n) is used for statement nodes, and n for conditional nodes in the CFG of Fig.2 and 3. Statement line numbers are given before corresponding constraints.

See http://www.geensoft.com/en

All these programs, as well as the source code of the Flasher Manager application, are publicly available at http:// hal.archives-ouvertes.fr/hal-00720921.

Acknowledgements. The authors would like to thank Geensoft for providing the Flasher Manager application and especially Thierry Gueguen and Samuel Devulder for their help.

supported by the ANR-07-SESUR-003 project CAVERN and the ANR-07-TLOG-022 project TESTEC.

Experimental results

This section presents our experiments with constraintbased BMC for checking the properties of the Flasher Manager (see Sect. 3.2 and 3.3). For each property, we compare the results obtained with DPVS [START_REF] Collavizza | A dynamic constraint-based bmc strategy for generating counterexamples[END_REF] to those obtained with CBMC [START_REF] Clarke | A tool for checking ANSI-C programs[END_REF], a state-of-the-art bounded


A Vergne
email: avergne@telecom-paristech.fr

L Decreusefond

P Martins
email: martins@telecom-paristech.fr

Reduction algorithm for simplicial complexes

In this paper, we aim at reducing power consumption in wireless sensor networks by turning off supernumerary sensors. Random simplicial complexes are tools from algebraic topology which provide an accurate and tractable representation of the topology of wireless sensor networks. Given a simplicial complex, we present an algorithm which reduces the number of its vertices, keeping its homology (i.e. connectivity, coverage) unchanged. We show that the algorithm reaches a Nash equilibrium, moreover we find both a lower and an upper bounds for the number of vertices removed, the complexity of the algorithm, and the maximal order of the resulting complex for the coverage problem. We also give some simulation results for classical cases, especially coverage complexes simulating wireless sensor networks.

I. INTRODUCTION

Wireless sensor networks attract more and more research attention due to the extent of their applications as well as the decreasing costs and sizes of the electronic circuits. Fields where wireless sensor networks can be used range from battlefield surveillance to target enumeration in agriculture and include environmental monitoring. In most applications, the topology of the network, such as its connectivity and its coverage, is a critical factor. Moreover, sensors are autonomous systems: they are not plugged in nor physically connected to each other. Battery life is thus a key problem and energy saving a crucial point in wireless sensor networks management. Sensors are often deployed in large numbers, exceeding the number of necessary sensors. A first approach to reduce energy consumption would logically be to turn off sensors randomly. However by doing so one could modify the topology of the sensor network by creating a coverage hole or breaking the connectivity. Therefore, we first have to know the network's topology before we can figure out energy saving methods. To guarantee the full knowledge of the topology one solution is to deploy the sensors according to a regular pattern (hexagon, square grid, rhombus or equilateral triangle) [START_REF] Bai | Deploying wireless sensors to achieve both coverage and connectivity[END_REF]. However the target field does not always allow such a precise deployment. Furthermore, the topology may not be time-invariant: sensors could be destroyed, their batteries could die, or their communication could be disturbed by seasonal changes. Another approach is then to consider a random deployment that may create clusters of sensors or on the contrary, may leave holes of coverage. There is thus extensive research on the coverage problem in wireless sensor networks. Location-based [START_REF] Fang | Locating and bypassing routing holes in sensor networks[END_REF] and ranged-based [START_REF] Zhang | Detecting coverage boundary nodes in wireless sensor networks[END_REF] methods require exact location information for the former or exact distance between sensors for the latter. Connectivity-based schemes seem of greater interest since they do not require such knowledge. In [START_REF] Ghrist | Coverage and hole-detection in sensor networks via homology[END_REF], Ghrist et al. introduced the so-called Vietoris-Rips complex, which is only based on the proximity graph between sensors, and determined the coverage by computing the homology of this complex. Coverage computation via homology boils down to simple linear algebra computations. It is used in [START_REF] Silva | Coordinate-free coverage in sensor networks with controlled boundaries via homology[END_REF], [START_REF] Muhammad | Decentralized computation of homology groups in networks by gossip[END_REF] and [START_REF] Zomorodian | Computing persistent homology[END_REF] as a tool for a network operator to evaluate the quality of its network. A distributed version of some of these algorithms is presented in [START_REF] Yan | Accuracy of homology based approaches for coverage hole detection in wireless sensor networks[END_REF], [START_REF] Yan | Connectivity-based distributed coverage hole detection in wireless sensor networks[END_REF] in order to detect coverage holes. From a mathematical point of view, moments of various variables, such as the Betti numbers or the Euler characteristic of the covered region, can be obtained in specific regimes [START_REF] Kahle | Random geometric complexes[END_REF], or explicitly in one dimension [START_REF] Decreusefond | On the one dimensional Poisson random geometric graph[END_REF] and in any dimension by means of Malliavin calculus [START_REF] Decreusefond | Simplicial homology of random configurations[END_REF].

In this paper, we present an algorithm which returns which sensors can be turned off without modifying the topology of the network. Given a simplicial complex, our algorithm suppresses vertices in an optimized order, keeping the complex homology unchanged. We can see an example of execution of the algorithm in Figure 1 We show that the algorithm reaches a Nash equilibrium: Every vertex in the final abstract simplicial complex is needed to maintain the homology. We evaluate a lower and an upper bound for the number of removed vertices. The average complexity of the algorithm is analyzed for two kind of random simplicial complexes: Erdös-Rényi complexes and Poisson random geometric complexes. We show that this complexity is polynomial for the former and (slighlty) exponential for the latter. We also give the maximal order of the resulting complex for the coverage problem. This is the first reduction algorithm based on simplicial complexes using homology aimed at energy savings in wireless sensor networks. A classical approach to power management in networks is the usage of the connectivity graph, such as in the dominating graphs problem [START_REF] Haynes | Fundamentals of domination in graphs[END_REF]. However, graphs are 2-dimensional objects. One vertex has full knowledge of its neighbors, but there is no representation of the interaction between these neighbors. Therefore there is no notion of coverage in graphs. Simplicial complexes allow us to represent higher order relations, and are thus more convenient for the representation of wireless sensor networks. Several works may seem at first glance related to our approach but they do not exactly fit with our purposes. In [START_REF] Dłotko | Distributed computation of coverage in sensor networks by homological methods[END_REF], [START_REF] Kaczyński | Homology computation by reduction of chain complexes[END_REF], the authors use reduction of chain complexes to compute homology, reducing the work domain, which make it inapplicable to a coverage problem. Witness complexes reduction, which is a reduction to a chosen number of points, is used in [START_REF] Silva | Topological estimation using witness complexes[END_REF] to compute topological invariant. In this work, as in the work on reduction of chains complexes, authors use reduction to compute the homology, whereas we use homology results to reduce optimally a simplicial complex. Finally, the authors of [START_REF] Campos-Nañez | A game-theoretic approach to efficient power management in sensor networks[END_REF] present a game theoretic approach to power management where they define a coverage function. However this method requires precise location information as well as coverage knowledge. Moreover, authors aim at identifying sub-optimal solutions that does not guarantee an unmodified coverage. The paper is organized as follows: in Section 2, we introduce simplicial homology concepts and variables that we will use in the next sections. Section 3 is devoted to the description of our reduction algorithm. In Section 4, we discuss its mathematical properties. Some simulation results are given in Section 5.

II. SIMPLICIAL HOMOLOGY

Graphs can be generalized to more generic combinatorial objects known as simplicial complexes. While graphs model binary relations, simplicial complexes represent higher order relations. A simplicial complex is a combinatorial object made up of vertices, edges, triangles, tetrahedra, and their ndimensional counterparts. Given a set of vertices V and an integer k, a k-simplex is an unordered subset of k + 1 vertices [v 0 , v 1 . . . , v k ] where v i ∈ V and v i = v j for all i = j. Thus, a 0-simplex is a vertex, a 1-simplex an edge, a 2-simplex a triangle, a 3-simplex a tetrahedron, etc.

Any subset of vertices included in the set of the k+1 vertices of a k-simplex is a face of this k-simplex. Thus, a k-simplex has exactly k+1 (k-1)faces, which are (k-1)-simplices. For example, a tetrahedron has four 3-faces which are triangles. A simplicial complex is a collection of simplices which is closed with respect to the inclusion of faces, i.e. all faces of a simplex are in the set of simplices, and whenever two simplices intersect, they do so on a common face. An abstract simplicial complex is a purely combinatorial description of the geometric simplicial complex and therefore does not need the property of intersection of faces. For details about algebraic topology, we refer to [START_REF] Hatcher | Algebraic Topology[END_REF].

One can define an orientation for an abstract simplicial complex, where a change in the orientation corresponds to a change in the sign of the coefficient:

[v 0 , . . . , v i , . . . , v j , . . . , v k ] = -[v 0 , . . . , v j , . . . , v i , . . . , v k ].
Definition 1: Given an abstract simplicial complex X, for each integer k, C k (X) is the vector space spanned by the set of oriented k-simplices of X.

Definition 2: The boundary map ∂ k is defined to be the linear transformation

∂ k : C k → C k-1 which acts on basis elements [v 0 , . . . , v k ] of C k via ∂ k [v 0 , . . . , v k ] = k i=0 (-1) i [v 0 , . . . , v i-1 , v i+1 , . . . , v k ].
This map gives rise to a chain complex: a sequence of vector spaces and linear transformations . . .

∂ k+2 -→ C k+1 ∂ k+1 -→ C k ∂ k -→ C k-1 ∂ k-1 -→ . . . ∂1 -→ C 0 ∂0 -→ 0. Definition 3: The k-th boundary group of X is B k (X) = im ∂ k+1 . Definition 4: The k-th cycle group of X is Z k (X) = ker ∂ k .
A standard result asserts that for any integer k,

∂ k • ∂ k+1 = 0. It follows that B k ⊂ Z k .
Definition 5: The k-th homology group of X is the quotient vector space:

H k (X) = Z k (X) B k (X) .
Definition 6: The k-th Betti number of X is the dimension:

β k = dim H k = dim Z k -dim B k .
We can compute the Betti numbers in a simple case. Let X be the simplicial made up of 5 vertices

[v 0 ], . . . , [v 4 ], 6 edges [v 0 , v 1 ], [v 0 , v 2 ], [v 1 , v 2 ], [v 1 , v 4 ], [v 2 , v 3 ] and [v 3 , v 4 ], and one triangle [v 0 , v 1 , v 2 ]. v 0 v 1 v 2 v 3 v 4

Fig. 2. A geometric representation of X

The boundary maps associated to the simplicial complex X are in matrix formulation:

∂ 1 =       [v 0 v 1 ] [v 0 v 2 ] [v 1 v 2 ] [v 1 v 4 ] [v 2 v 3 ] [v 3 v 4 ] [v 0 ] -1 -1 0 0 0 0 [v 1 ] 1 0 -1 -1 0 0 [v 2 ] 0 1 1 0 -1 0 [v 3 ] 0 0 0 0 1 -1 [v 4 ] 0 0 0 1 0 1       , ∂ 2 =         [v 0 , v 1 , v 2 ] [v 0 , v 1 ] 1 [v 0 , v 2 ] -1 [v 1 , v 2 ] 1 [v 1 , v 4 ] 0 [v 2 , v 3 ] 0 [v 3 , v 4 ] 0        
.

The boundary map ∂ 0 is the null function on the set of vertices. Then we can compute:

β 0 (X) = dim ker ∂ 0 -dim im ∂ 1 = 5 -4 = 1 β 1 (X) = dim ker ∂ 1 -dim im ∂ 2 = 2 -1 = 1
There are several famous types of abstract simplicial complexes, here we focus on two particular abstract simplicial complexes defined on a metric space.

Definition 7 ( Cech complex): Given (X, d) a metric space, ω a finite set of points in X, and a real positive number. The Cech complex of parameter of ω, denoted C (ω), is the abstract simplicial complex whose k-simplices correspond to (k + 1)-tuples of vertices in ω for which the intersection of the k + 1 balls of radius centered at the k + 1 vertices is non-empty. Thus the Cech complex characterizes the coverage of a domain as we can see in Figure 3.

Definition 8 (Vietoris-Rips complex): Given (X, d) a metric space, ω a finite set of points in X, and a real positive number. The Vietoris-Rips complex of parameter of ω, denoted R (ω), is the abstract simplicial complex whose ksimplices correspond to unordered (k + 1)-tuples of vertices in ω which are pairwise within distance less than of each other.

In general, unlike the Cech one, Vietoris-Rips complexes are not topologically equivalent to the coverage of an area. However, the following gives us the relation between coverage and Vietoris-Rips complexes:

Lemma 1: Given (X, d) a metric space, ω a finite set of points in X, and a real positive number, Only graph description is required to build a Vietoris-Rips complex. In the same way we can build an abstract simplicial complex from any graph: each k-simplex is included in the complex if every one of its (k -1)-faces already are.

R √ 3 (ω) ⊂ C (ω) ⊂ R 2 (ω).
The Betti numbers are used to count the number of kdimensional holes. For example, β 0 counts the number of 0-dimensional holes, that is the number of connected components. And β 1 counts the number of holes in the plane. If we are in dimension d, the k-th Betti number for k ≥ d has no geometric meaning.

III. REDUCTION ALGORITHM

In this section, we present the reduction algorithm. The algorithm takes as input a fully described abstract simplicial complex: all k-simplices must be enumerated for every integer k. Then the algorithm aims at removing superfluous vertices while maintaining the homology type of the abstract simplicial complex.

There are several levels of knowledge of the homology type: you might want to maintain only the same first k 0 -th homology group and Betti numbers. For the ease of presentation, we restrict ourselves to dimension 2, so we consider only the first two Betti numbers: β 0 is the number of connected components, β 1 is the number of holes in the plane. We have thus two different algorithms, for k 0 = 1 and k 0 = 2, but the main idea can be extended to greater dimensions.

The first algorithm, henceforth referred to as the connectivity algorithm, aims at maintaining β 0 . The connectivity algorithm takes as inputs the abstract simplicial complex, plus the list of connected active vertices that are to stay connected.

The second algorithm, called the coverage algorithm, aims at maintaining β 0 and β 1 . It takes as inputs in addition to the abstract simplicial complex, the list of connected vertices which define the boundary of the area that is to stay covered.

A. Degree calculation

The first part of the algorithm is the calculation of a degree that we define for every k 0 -simplex, with k 0 the number of Betti numbers to be kept unchanged:

Definition 9: For k integer, the degree of a k-simplex [v 0 , v 1 , . . . , v k ] is the size of the greatest simplex it is part of:

D[v 0 , v 1 , . . . , v k ] = max{d | [v 0 , v 1 , . . . , v k ] ⊂ d-simplex}. We immediately have D[v 0 , v 1 , . . . , v k ] ≥ k for any k- simplex.
We can see examples of value of the degree for 2-simplices in figure 4. For the remainder of the paper, let s k (X), or s k , be the number of k-simplices of the abstract simplicial complex X.

v 0 v 1 v 2 D[v 0 , v 1 , v 2 ] = 3 v 0 v 1 v 2 v 3 D[v 0 , v 1 , v 2 ] = 4
Let us denote D 1 , . . . , D s k 0 the s k0 degrees of a complex, their computation is done as shown in Algorithm 1.

Algorithm 1 Degree calculation

for i = 1 → s k0 do Get (v 0 , . . . , v k0 ) the vertices of the i-th k 0 -simplex k = k 0 while (v 0 , . . . , v k0 ) are vertices of a (k + 1)-simplex do k = k + 1 end while D i = k end for return D 1 , . . . , D s k 0

B. Indices computation

The second part of the algorithm is the computation of the indices that we define for each vertex:

Definition 10: The index of a vertex v is the minimum of the degrees of the k 0 -simplices it is a vertex of:

I[v] = min{D[v 0 , v 1 , . . . , v k0 ] | v ∈ [v 0 , v 1 , . . . , v k0 ]},
with k 0 the number of Betti numbers to be kept unchanged. If a vertex v is not a vertex of a k 0 -simplex then I[v] = 0.

We can see in figure 5 an example of value of indices in an abstract simplicial complex.

v 0 v 1 v 2 v 3 v 4 D[v 0 , v 1 , v 2 ] = D[v 0 , v 1 , v 3 ] = D[v 0 , v 2 , v 3 ] = D[v 1 , v 2 , v 3 ] = 4 D([v 1 , v 3 , v 4 ]) = 3 I[v 0 ] = I[v 2 ] = 4 and I[v 1 ] = I[v 3 ] = I[v 4 ] = 3

Algorithm 2 Indices computation

for i = 1 → s 0 do I[v i ] = 0 for j = 1 → s k0 do if v i is vertex of k 0 -simplex j then if I[v i ] == 0 then I(v i ) = D j else I[v i ] = min{I[v i ], D j } end if end if end for end for return I[v 1 ], . . . , I[v s0 ]
The index of a vertex is an indicator of the density of vertices around the vertex: an index of k 0 indicates that at least one k 0 -simplex of the vertex is not a face of any (k 0 + 1)simplices; whereas a high index shows that each k 0 -simplices of the vertex is part of higher simplices.

An index of zero indicates that the vertex is not a part of a any k 0 -simplex: the vertex is isolated up to the k 0 -th degree. For k 0 = 1, that means that the vertex is disconnected. For k 0 = 2, the vertex is only linked to other vertices by edges, therefore is inside a coverage hole.

C. Optimized order for the removal of vertices

We now consider the entire algorithm and look for an optimized order to remove vertices which are superficial to the homology.

First, we consider the particular vertices. The active or boundary vertices that are given as inputs and define the area of interest for the homology computation are critical vertices that are requested to remain in the last complex. They are flagged as irremovable by a negative index.

Then the indices give us an order for the removal of vertices: the greater the index of a vertex, the more likely it is superfluous for the homology of the abstract simplicial complex. So the vertices with the greatest index are candidates for removal: one is chosen randomly. The removal of a vertex leads to the degradation of all the k-simplices it was a vertex of, to (k -1)-simplices for every integer k.

We need to ensure that the homology is unchanged, so we compute the k 0 first Betti numbers thanks to the boundary maps once before the algorithm runs, then every time a vertex is removed. This computation is instantaneous since the complex is already built, and only adjacency matrices defining the complex are needed. If the homology changes, the vertex is put back into the abstract simplicial complex, with a negative index to flag it as critical. Otherwise, the removal of the vertex is confirmed. The degrees of the k 0 -simplices and the indices of the vertices are recalculated for the new abstract simplicial complex.

Lemma 2: When a vertex of index I > k 0 is removed, only the vertices sharing an I-simplex with it, and of index I can have their index changed to I -1.

Proof: Let w be the removed vertex of index I, and v any vertex of the abstract simplicial complex. Since w is removed, I is the maximum index of the complex.

If v does not share any simplex with w, none of the degrees of its k 0 -simplex will change, and neither will its index.

Thus let us consider that the maximum common simplex of v and w is a k-simplex. If k < I then w have index k < I, which is absurd. Then we can assume that k ≥ I. Either the index of v is strictly less than I and thus comes from a simplex not shared with w, therefore it is unmodified by the removal of w. Or the index of v is I, it either still comes from a I-simplex not shared with w and remains unmodified, or it comes from a common I-simplex. In the latter, after the removal of w, the index of v becomes I -1.

The algorithm goes on removing vertices until every remaining vertex has its index below or equal to k 0 -1. We give in Algorithm 3 the whole algorithm for the conservation of the k 0 first Betti numbers.

Definition 11 (Dominating set): As defined in [START_REF] Haynes | Fundamentals of domination in graphs[END_REF], a set S ⊆ V of vertices of a graph G = (V, E) is called a dominating set if every vertex v ∈ V is either an element of S or is adjacent to an element of S.

Algorithm 3 Reduction algorithm input: Abstract simplicial complex X, list L C of critical vertices (active or boundary). Computation of β 0 (X), β 1 (X), . . . , β k0-1 (X) Computation of D 1 (X), . . . , D s k 0 (X)

Computation of I[v 1 (X)], . . . , I[v s0 (X)] for all v ∈ L C do I[v] = -1 end for I max = max{I[v 1 (X)], . . . , I[v s0 (X)]} while I max > k 0 -1 do Draw w a vertex of index I max X = X\{w} Computation of β 0 (X ), β 1 (X ), . . . , β k0-1 (X ) if β i (X ) = β i (X) for any i = 0, . . . , k 0 -1 then I[w] = -1 else Computation of D 1 (X ), . . . , D s k 0 (X ) for i → 1 : s 0 do if I[v i (X )] ≥ 0 then Computation of I[v i (X )] end if end for I max = max{I[v 1 (X )], . . . , I[v s 0 (X )]} X = X end if end while return X
Definition 12 (Full domain hypothesis): Let us call the full domain hypothesis when the critical vertices define the whole input space: for the connectivity algorithm, that means that the active vertices are a dominating set of the initial abstract simplicial complex. For the coverage algorithm, that means that all the vertices are in the convex hull defined by the boundary vertices.

Lemma 3: Under the full domain hypothesis, the algorithm can stop when all vertex indices are below or equal to k 0 instead of k 0 -1.

Proof: Let us suppose the input data satisfies the full domain hypothesis. Let v be a vertex of index k 0 , which means that at least one of the k 0 -simplex it is vertex of is not a face of any (k 0 +1)-simplex. The removal of this vertex would lead to the removal of this particular k 0 -simplex. Since we need to maintain the homology on the entire domain, this would lead to a k 0 -dimensional hole, and an increment of β k0-1 .

IV. PROPERTIES

Theorem 4 (Nash equilibrium): Our algorithm reaches a Nash equilibrium as defined in [START_REF] Campos-Nañez | A game-theoretic approach to efficient power management in sensor networks[END_REF]: every vertex in the final abstract simplicial complex is needed to maintain its homology.

Proof: In the final abstract simplicial complex, every vertex is of index less than or equal to k 0 -1. By the definition of a computed index, it is impossible for an index to be strictly less than k 0 if nonzero or negative. We then differentiate two types of vertices: vertices of index -1 and 0.

First, negative indices are given to vertices to flag them as critical. Either a vertex is of negative index because it is an active/boundary vertex, in which case it is required to stay in the complex. Or a vertex is of negative index if its removal leads to a change in the Betti numbers.

Then, a vertex of index 0 is an isolated vertex. If it isolated up to the k 0 -th of degree, its removal will decrease the k 0 th Betti number. For example, the removal of a first degree isolated vertex, that is a disconnected one, would lead to the decrement of β 0 . As well, the removal of a vertex inside a hole will lead to the union of 2 or more holes.

In the case of lemma 3, its proof shows that the vertices of indices k 0 are needed to maintain the homology.

Theorem 5 (Upper and lower bounds): Let E k be the set of vertices that have indices k. The number of removed vertices M is bounded by:

Imax k=k0 1 [E k =∅] ≤ M ≤ Imax k=k0 |E k |.
Proof: Let us begin with the upper bound, the algorithm runs until all indices are less than or equal to k 0 -1. So the maximum number of vertices the algorithm can remove is the number of vertices that initially have their index strictly greater than k 0 -1. This is an optimal upper bound since this number of removed vertices is reached in the following case:

Let a k-simplex, with k > k 0 , be the initial abstract simplicial complex, and n C of its vertices be the initial critical vertices, necessarily n C ≤ k +1. The n C critical vertices have negative indices, the k + 1 -n C other vertices have an index of k, and they are all removed.

v 0 I[v 0 ] = 4 v 1 I[v 1 ] = -1 v 2 I[v 2 ] = -1 v 3 I[v 3 ] = 4 Before v 0 v 1 I[v 1 ] = -1 v 2 I[v 2 ] = -1 v 3
After Fig. 6. Example of this case with k = 3 and n C = 2, the 2 nodes v 0 and v 3 are removed by the algorithm.

For the lower bound, we have seen in Lemma 2 that the removal of a vertex of index I max can only decrease the index of vertices of index I max . In the worst case, it decreases all indices I max and the value of I max changes, not necessarily to I max -1 depending on the critical vertices. Thus we can see, that at least one vertex per index value can be removed, hence the result.

The lower bound is reached in the previous case if n C = k. Theorem 6 (Complexity): The complexity of the algorithm is upper bounded by:

(n -n C )s k0 n + H k=k0+1 s k ,
with n C being the number of initial critical vertices, s k the number of k-simplices in the abstract simplicial complex, n = s 0 the total number of vertices, and H the highest simplex in the complex.

Proof: For the computation of the degrees of every k 0 -simplex, the algorithm traverses all the k-simplices for k 0 < k ≤ H to see if the k 0 -simplex is included in it. Since there is s k k-simplices, the computation of the degrees is of complexity s k0 H k=k0+1 s k . For the computation of the indices, the algorithm traverses, for every one of the n vertices, the k 0 -simplices it is vertex of, which is at most all the k 0 -simplices. The complexity of the computation of all the indices is therefore s k0 n.

These computations are done before every removal of vertices, which is at most the total number of vertices minus the number of initial critical vertices, hence the result.

Corollary 7: The complexity of the algorithm is upper bounded by 2 n when n goes to infinity.

Proof: This is a direct consequence of Theorem 6 since the number of k-simplices s k can be upper bounded by n k+1 .

Corollary 8: If we apply our algorithm to a Cech complex C (ω), defined with the maximum norm, based on a Poisson point process of parameter λ on a torus of side a in dimension d. The complexity of the algorithm is of the order of O((1 + ( 2 a ) d ) n ) on average when n goes to infinity.

Proof: According to [START_REF] Decreusefond | Simplicial homology of random configurations[END_REF], we have:

E λ [s k-1 | s 0 = n] = n k k d 2 a d(k-1) , Cov λ [s k-1 , s l-1 | s 0 = n] = k∧l i=1 n k + l -i k + l -i k k i k + l -i + 2 (k -i)(l -i) i + 1 d 2 a d(k+l-i-1)
.

Plugging this into the complexity formula of Theorem 6 gives the result. We define the Erdös-Rényi complex based on the eponymous random graph:

Definition 13 (Erdös-Rényi complex): Given n an integer and p a real number in [0, 1], the Erdös-Rényi complex of parameters n and p, denoted G(n, p), is an abstract simplicial complex with n vertices which are connected randomly. Each edge is included in the complex with probability p independent from every other edge. Then a k-simplex, for k ≥ 2, is included in the complex if and only if all its faces already are.

Corollary 9: The complexity of the algorithm for the Erdös-Rényi complex based on the graph G(n, p) is of the order of O(n 2(k0+2) ) on average when n goes to infinity.

Proof: In the Erdös-Rényi complex, the expected values of the number of k-simplices and of the product of numbers of k-simplices are given in [START_REF] Bollobás | Cliques in random graphs[END_REF]:

E λ [s k-1 ] = n k p ( k 2 ) , E λ [s k-1 s l-1 ] = k∧l i=0 n k k i n -k l -i p ( k 2 )+( l 2 )-( i 2 ) .
The results then comes from the complexity formula of Theorem 6.

Theorem 10 (Highest order simplex): In the case of the algorithm applied to a Vietoris-Rips complex or a Cech complex in dimension d, the highest order simplex of the final complex is at most a (2d -1)-simplex, excluding critical vertices.

Proof: Let k be an integer strictly greater than 2d-1, and let us suppose that the k + 1 non-critical vertices v 0 , . . . , v k form a k-simplex.

Since we are in dimension d, we can consider the vertex the furthest on each of the 2d directions. Note that two of these vertices can be the same vertex. Let us reorder the vertices such that v 0 , . . . , v i-1 with i ≤ 2d are the extremity vertices defined above. Then v i , . . . , v k must fall in the covered area of v 0 , . . . , v i-1 . Such vertices can be removed without changing the homology of the complex, therefore they can not be in the final complex hence a contradiction.

Corollary 11: In the case of the algorithm applied to a Vietoris-Rips complex or a Cech complex under the full domain hypothesis in 2 dimensions, to make the final simplicial complex planar, it is necessary and sufficient to remove edges that are second diagonals of a square.

Proof: This is a direct consequence of Theorem 10. Theorem 12: For the algorithm applied to a Vietoris-Rips complex or a Cech complex under the full domain hypothesis, the set of remaining vertices in the final complex is a dominating set of the set of vertices in the initial complex.

Proof: Let be the parameter of the Vietoris-Rips complex. The area inside the coverage boundary is covered by the final abstract simplicial complex: each point of this area is at distance lower than from at least three vertices of the final complex, znd is thus adjacent to them. This is true for every vertex of the initial complex.

The proof is the same in the case of the Cech complex.

V. SIMULATION RESULTS

Our simulations aim to illustrate our algorithm. The results are highly dependent on the chosen parameters: for the connectivity algorithm the percentage of removed vertices is linked to the probability that the active vertices are connected without any intermediary in the complex; for the coverage algorithm, it is linked to the ratio initial number of vertices on number of vertices needed for the coverage. We simulated our algorithm on two types of complexes: the connectivity algorithm on the Erdös-Rényi complex, and the coverage algorithm on the Vietoris-Rips complex. We can see in Figure 7 one realization of the connectivity algorithm on a Erdös-Rényi complex of parameter n = 15 and p = 0.3, with a random set of active vertices. A vertex is active with probability p a = 0.5 independently from every other vertices. We chose a small number of vertices for the figure to be readable. Active vertices are circled, and nonactive vertices which are kept to maintain the connectivity between active vertices are starred. With the parameters n = 60 vertices, and p = 0.2, on average on 1000 configurations without disconnectivity with p a taking values between 0.1 and 0.5 (200 configurations each), the algorithm removed 98% of the non-active vertices: p a % of removed vertices 0.1 94.96% 0.2 97.14% 0.3 98.59% 0.4 99.43% 0.5 99.87%

The behaviour of the connectivity algorithm on a Vietoris-Rips complex is analogous.

For the coverage algorithm on a Vietoris-Rips complex, we simulated the set of vertices using a Poisson point process: Definition 14: A Poisson point process ω with intensity λ on a Borel set X is defined by: i) For any A ∈ B(X), the number of vertices in A, ω(A), is a random variable following a Poisson law of parameter λS(A), P(ω(A) = k) = e λS(A) (λS(A)) k k! • ii) For any disjoint A, A ∈ B(X), the random variables ω(A) and ω(A ) are independent. With the parameters, chosen to ensure coverage, = 1, λ = 5.1 and a = 2, on average on 1000 configurations, the algorithm removed 69.35% of the non-boundary vertices.

Fig. 3 .

 3 Fig. 3. A sensor network and its associated Cech complex.

Fig. 4 .

 4 Fig. 4. Example of values of degrees of triangles

Fig. 5 .

 5 Fig. 5. Example of values of indices

Fig. 7 .

 7 Fig. 7. A Erdös-Rényi complex before and after the connectivity algorithm.

Fig. 8 .

 8 Fig.8. A Vietoris-Rips complex before and after the coverage algorithm.

  .

	2
	1.8										1.8
	1.6										1.6
	1.4										1.4
	1.2										1.2
	1										1
	0.8										0.8
	0.6										0.6
	0.4										0.4
	0.2										0.2
	0										0
	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6	1.8	2	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6	1.8	2

2 Fig.

1

. A sensor network before and after the coverage reduction algorithm.