Raphaël Lallement

Juan Cortés

Mamoun Gharbi

Alexandre Boeuf

Rachid Alami

Carmelo J Fernandez-Agüera

Iván Maza

Carmelo J Fernandez-Ag Üera

Combining Assembly Planning and Geometric Task Planning

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The motivation for the work described in this chapter comes from context of the ARCAS European Project 1 funded by the European Commission. One of the goals of this project is to build a structure by using a team of aerial robotic manipulators (AROMAs). The practical interest of this system can be found in situations where it is required to build a structure in places with difficult access by conventional means. Actually, the problem of automatically finding a proper place for the construction of the structure is also addressed in the project.

Assembly planning is the process of creating a detailed assembly plan to craft a whole product from separate parts by taking into account the final product geometry, available resources to manufacture that product, fixture design, feeder and tool descriptions, etc. In this context, different planning problems such as structure assembly planning, task planning and motion planning have to be solved in a highly dimensional space due to the many degrees of freedom of the robots and the complexity of the tasks. To have simple yet interesting structures to assemble the project focused on structures made of bars. An example can be seen in Fig. 1. The simplicity comes from the clipping mechanism: when two pieces are brought together they clip ensuring a strong link. On the other hand the complexity comes from the need for cooperative transport of certain long bars requiring two (or more) AROMAs to strongly cooperate. Moreover the robots are using arms which must be compliant to avoid any problems. To carry out the assembly of the structures, the complete system must exhibit a set of properties:multi-robot plans, cooperative transport, perception and localization and visual servoing. Fig. 1 An example of the type of structures considered in the ARCAS project. There are 12 parts composing a cube, but there also exist a variant with four additional diagonal bars for a total of 16 parts.

Assembly, symbolic and motion planning traditionally belong to decoupled different research areas and have been widely studied separately in the last decades. However, there is a growing interest on how to properly connect these planners or how to design coupled planners.

This chapter proposes a joint solution for these planning problems which embeds geometric reasoning at different levels in order to reduce the computational complexity. The chapter is structured as follows. Section 2 presents related work on the connection of assembly planners to task planners. The assembly planning problem covers three main assembly subproblems: sequence planning, line balancing, and path planning. This chapter is focused on a single AROMA, and hence, the line balancing subproblem related to the allocation of assembly operations to robots is out of the scope of our work. The approaches followed to solve the other subproblems are described in Section 3. Section 4 describes in more detail the proposed architecture and how each component relates to each other. It also defines the information exchanged between the planner and introduces the heuristic used during the experiments to guide Assembly Planning. Section 5 describes how the approach works for a team of AROMAs whereas Section 6 presents how the symbolic plans can be refined to deal with intricate constraints. Finally, the conclusions in Section 7 close the chapter.

Related Work

Efficient assembly plans can reduce time and costs significantly. The assembly planning problem has been shown to be an NP-complete problem [START_REF] Kavraki | On the complexity of assembly partitioning[END_REF] and covers two main assembly subproblems in a single robot context: sequence planning and path planning.

The Assembly Sequence Planning (ASP) problem concerns with finding a sequence of collision-free operations that bring the assembly parts together, having given the geometry of the final structure. A systematic overview on the ASP is presented in [START_REF] Jiménez | Survey on assembly sequencing: a combinatorial and geometrical perspective[END_REF], which includes a survey of the elements of sequence planning, such as finding a feasible sequence, determining an optimal sequence according to one or more operational criteria, representing the space of feasible assembly sequences in different ways, applying search and optimization algorithms, and satisfying precedence constraints existing between subassemblies. This problem is addressed in Section 3.1.

A taxonomy for assembly and task planning is described in [START_REF] Gottschlich | Assembly and task planning: a taxonomy[END_REF]. However, the taxonomy presents both planners in a decoupled manner. The problems that an autonomous robotic assembly system must tackle both regarding assembly planning and task planning are summarized in [START_REF] Rosell | Assembly and task planning using petri nets: A survey[END_REF]. This paper also reviews the approaches that use Petri Nets as a formalism to develop the corresponding planners, but the coupling between both is not described.

In [START_REF] Mosemann | Automatic decomposition of planned assembly sequences into skill primitives[END_REF], the output of an assembly planner is used directly as input to a symbolic planner that decomposes it. Once given the assembly plan, the system allows them to complete motion planning in real time. However, since there is no feedback, the system must assume that the given assembly plan is compatible with geometric restrictions. Manipulation primitive nets are introduced in [START_REF] Thomas | Assembly planning and task planning -two prerequisites for automated robot programming[END_REF] to deal with uncertainties occurring during assembly task execution.

In [START_REF] Knepper | Ikeabot: An autonomous multi-robot coordinated furniture assembly system[END_REF], the assembly planner computes a blueprint by reasoning about the holes used to attach the parts together. It then sends the blueprint to the symbolic planner using an object-oriented language which is then translated into a PDDL problem and solved using the Fast-Forward solver. This builds a set of actions which is then dispatched in the group with sometimes coordinated (multi-robot) manipulations. So the geometry is only taken in account when computing the blueprint, not to ensure the feasibility for the coordinated motion: a robot could block or be blocked by others.

Finally, [START_REF] Heger | Robust robotic assembly through contingencies, plan repair and re-planning[END_REF] uses a 3-layer architecture: an assembly planner generates the assembly graph and finds a good sequence. Then a two-stage executive layer turns the task tree into instances which in turns are transformed into robot behaviours. The last step is the execution on the different robots, which is controlled by the behaviours layer. The system uses motion planning and an exception-handling mechanism to ensure its robustness. Although it will not be as optimal as a planning-based system, the authors claim it to be significantly faster.

Dealing with and merging symbolic and geometric constraints when planning is a growing field that has been a focus to a number of researchers over the few last years. Different approaches have been proposed like [START_REF] Plaku | Sampling-based motion and symbolic action planning with geometric and differential constraints[END_REF] where the search at geometric level is guided by the symbolic planner. Other approaches focused on different aspects like [START_REF] Nedunuri | Smtbased synthesis of integrated task and motion plans from plan outlines[END_REF] where a placement graph is built in other to apply a Satisfiability Modulo Theories solver on the actions represented in the graph. Similarly, [START_REF] Garrett | FFRob: An efficient heuristic for task and motion planning[END_REF] builds a conditional-reachability graph representing different configurations reachable by the robot (with or without object in hand) and the FastForward algorithm is used to guide the search and find solutions in the graph.

In [START_REF] Dornhege | Lazy evaluation and subsumption caching for search-based integrated task and motion planning[END_REF] and [START_REF] Dornhege | Integrating task and motion planning using semantic attachments[END_REF], the authors use semantic attachments, which are external procedures called by the symbolic planner to assess the feasibility of a symbolic action at the geometric level (e.g. if a collision free path exists between 2 positions). [START_REF] Karlsson | Combining task and path planning for a humanoid two-arm robotic system[END_REF] extends this approach by adding a geometric backtracking: in order to assess the feasibility of an action, the geometric planner can change the geometric choices made for the previous actions.

Reference [START_REF] Pack | Hierarchical task and motion planning in the now[END_REF] uses a goal-driven task planner that enables calls to external procedures during the planning phase. In case of failure, this procedure provides a reason of the failure to the planner and enables it to find an alternative plan. The idea of using failure reasoning to guide symbolic planning is also stressed out in [START_REF] Erdem | Combining high-level causal reasoning with low-level geometric reasoning and motion planning for robotic manipulation[END_REF] where a causal reasoner is used to find a symbolic plan, then a motion planner tries to solve the underlying motion problem, and if the latter fails, a temporal constraint is added to the symbolic domain and the causal reasoner tries to find a new plan. [START_REF] Srivastava | Combined task and motion planning through an extensible planner-independent interface layer[END_REF] uses off-the-shelf planners and formulates a novel representational abstraction enabling to combine them: each action in the symbolic plan can have multiple instantiations at geometric level corresponding to the different geometrical choices possible.

In [START_REF] Lagriffoul | Constraint propagation on interval bounds for dealing with geometric backtracking[END_REF] a task-plan is computed, and interval bounds which are constraints on object/robot positions are used to prune out geometric choices. Another approach, proposed in [START_REF] Lozano-Pérez | A constraint-based method for solving sequential manipulation planning problems[END_REF], is to formalise the problem as geometric constraints between agents and objects, and to use a Constraint Satisfaction Problem solver to find the solution. Reference [START_REF] Muñoz-Morera | Combining a hierarchical task network planner with a constraint satisfaction solver for assembly operations involving routing problems in a multi-robot context[END_REF] addresses the combination of a symbolic hierarchical task network planner and a constraint satisfaction solver for the vehicle routing problem in a multi-robot context for structure assembly operations. Each planner has its own problem domain and search space, and the article describes how both planners interact in a loop sharing information in order to improve the cost of the solutions.

We have proposed various contributions to the problem of combining symbolic and geometric reasoning in order to produce pertinent and feasible robot plans. In Asymov [START_REF] Gravot | aSyMov: a planner that deals with intricate symbolic and geometric problems[END_REF][START_REF] Cambon | A hybrid approach to intricate motion, manipulation and task planning[END_REF] we essentially proposed a principled way to link the two planners thanks to a geometric level able to tackle the so-called "manipulation planning problem" [START_REF] Alami | A geometrical approach to planning manipulation tasks. the case of discrete placements and grasps[END_REF] and that allows to explicitly take into account the topological changes occurring, in the configuration space, when a robot grabs or releases an object. Asymov provided a well founded translation of pick and place actions (and similar actions) into 'transit' and 'transfer' motion planning requests even in multi-object and multi-robot contexts.

More recently we focused on a complementary approach [START_REF] Lavindra De Silva | Towards combining HTN planning and geometric task planning[END_REF][START_REF] De | A new approach to combined symbolic-geometric backtracking in the context of human-robot interaction[END_REF]: exploiting the capacity of the Hierarchical Task Network (HTN) [START_REF] Nau | Automated Planning: Theory & Practice[END_REF] techniques to encode domain knowledge, and developing a geometric motion planner capable of planning actions with several levels of abstraction opening to more elaborate action instantiations. Such a combination provides several key features: a clean interface which corre-sponds to the anchoring problem and allows to better exhibit and master the links between the incremental processes of producing the symbolic plan and its geometric counterpart.

In [START_REF] Lavindra De Silva | Towards combining HTN planning and geometric task planning[END_REF] we presented a geometric backtracking algorithm which allows to reconsider the previous geometric choices by trying different alternatives to the previously computed actions and tests the validity of this alternatives by computing their geometric effects. In [START_REF] Gharbi | Combining symbolic and geometric planning to synthesize human-aware plans: toward more efficient combined search[END_REF], a more elaborate management of the ramification problem is proposed allowing the integrated planner to exploit: (1) the ability of the geometric planner to provide several instantiations of the same action, (2) the ability to encode domain expert knowledge at both levels, (3) well-informed cost estimation of actions.

Description of the Planners

The overall planning approach is composed of three planners: (1) an assembly sequence planner that computes the assembly sequence from the assembled structure, (2) the symbolic planner, HATP (Hierarchical Agent-based Task Planner), is responsible for the task allocation, and finally (3) a motion planner, to compute the trajectories for each action in the symbolic plan. These planners are described in this section.

Assembly Sequence Planner

Figure 2 shows the architecture of the assembly planner [START_REF] Muñoz-Morera | Architecture for the automatic generation of plans for multiple UAS from a generic mission description[END_REF] developed to take into account the effect of external forces such as gravity and physical interactions between the parts of the structure to be built. It uses simulations to predict the stability of partially assembled structures and applies that information to expand the graph of possible plans.

The assembly planner is built on top of two main components: A classical planning engine and a physics simulation engine.

• Planning engine: a generic planning library has been developed. The library allows transparent substitution of simple search strategies such as depth-first or breadth-first. It provides support for heuristics for more advanced strategies as well. At a technical level, the framework takes the form of a set of template classes that can be inherited or instantiated with specific policies, and abstracts the generic process of planning. A higher level component is responsible for writing a dynamic graph tree, selecting a search strategy, and representing states and actions that describe the application specific problem set. In the case of assembly planner, an action would be the removal of a piece from the structure along a discrete direction and a state would correspond to a partial assembly of the structure that is stable and self-sustaining.

Fig. 2 Architecture of the assembly planner developed to take into account the effect of external forces such as gravity and physical interactions between the parts of the structure to be built

• Physics engine: This component is built using the Bullet Physics library2 . It is applied to compute whether a subassembly is stable (i.e. it is self-sustaining and can remain indefinitely in the given configuration without external support).

When given a set of pieces and their locations in the structure, it performs a rigid body simulation on them and checks the results. If after a fixed period, all the pieces of the structure remain in their starting configuration (position and orientation), the subassembly is considered stable.

The planner actually solves the problem of disassembly, and then returns the reverse plan as a valid assembly plan. It uses a best-first search strategy, based on heuristics that can be refined for successive iterations of re-planning. The search graph used for planning is given in implicit form. This avoids the need to precompute and store the whole tree in memory. In order to get the possible actions that can be performed at a given state, the planner invokes the simulator and retrieves a list of all the pieces that can be safely removed from the remaining set.

As a final step, the planner will try to combine successive actions into parallel operations that can be executed at the same time by separate agents. The engine tests consecutive operations combined into a single action. This process also lets the engine compute conditional relations between operations. Let it be two consecutive operations A, the first, and B, the latter. If the order of execution of A and B can be reversed, then they can also be carried out in parallel. If the order can not be reversed, then operation A is considered to be a precondition for operation B. Note that preconditions computed in this manner are actually a super set of the absolute precondition relations between all actions (i.e. there may be alternative plans where B can be performed before A). However, this technique guarantees that all variants of the plan resulting from recombining the operations according to these relations are also stable. This property can be highly valuable for integration with planners in other domains.

Symbolic Planner

A symbolic planner is required to get the actual set of actions to execute the assembly plan. It will compute the best sequence of actions to fulfill the plan for a given set of agents and their properties (payload, actuator, and so on).

Our system uses Hierarchical Task-Network (HTN) planning [START_REF] Ghallab | Automated Planning: Theory and Practice[END_REF], for its expressiveness and efficiency. An HTN planner computes the symbolic plan from a domain that is a description of the different possible ways to solve the problem, and it is provided by a domain expert. The domain is composed of tasks, and task can be of one of two types: action or method. An action is a task that the system can actually achieve (such as go to, pick, place, and so on). On the other hand, a method is composed of several sets of partially-ordered tasks (again actions or methods), each set represents a way to solve the method at hand. The domain is composed of several methods encapsulating other methods and actions, hence creating a hierarchy.

The planning goal is expressed as a task to accomplish. The principle of HTN planning is to decompose this top-level task into one of its possible decompositions (i.e. as set of partially ordered tasks). This process goes on until all tasks are decomposed into actions. In addition to this process, there is also a mechanism of variable binding: it is indeed possible to let some task parameter as free variable, the planning process will then try different values and keep the best one. Finally the choices for which decomposition and which value for a variable are done randomly and it creates backtrack points. The most famous HTN planner is SHOP2 [START_REF] Nau | SHOP2: An HTN planning system[END_REF].

Our implementation is called HATP [START_REF] Lallement | HATP: An HTN planner for robotics[END_REF], which stands for Hierarchical Agentbased Task Planner. It is a total-order HTN, which means that we can have the current symbolic state anytime during planning. One of HATP main characteristic is its object-oriented and user-friendly language which ease the development of new domain. It uses a state variable representation, and every object in the environment is represented with an entity. The language is rich and contains many features such as set manipulation. Please refer to [START_REF] Lavindra De Silva | The HATP hierarchical planner: Formalisation and an initial study of its usability and practicality[END_REF] for more details.

Our planner is "agent-based" because agents are special entities used to compute streams of actions in addition to the usual solution (tree) decomposition. Each stream represents an agent. It contains its actions and causal links to order them, and to link them with the other agents stream.

HATP is implemented in C++ and special care was taken when designing the internal structures to ensure that it is easy to extend the planner with new functionalities. The most notable one is the tight integration with a Geometric Task Planner.

Interleaved Task and Motion Planning

GTP (Geometric Task Planner) encapsulates a motion planner, including a level of abstraction. For instance, it allows to plan a 'placeReachable' action, which is a combination of fast trajectory, approach trajectory, ungrasp and escape trajectory.

Using this planner, we developed a system that can check the geometric feasibility of symbolic plan as it is built [START_REF] De | A new approach to combined symbolic-geometric backtracking in the context of human-robot interaction[END_REF]. The principle is that, when the symbolic planner adds an action to the symbolic plan, its geometric counterpart is tried in the current geometric state. If the geometric action is feasible, the planning process continues, otherwise a backtrack is triggered: either change the symbolic plan or try another solution for one of the previous geometric actions.

In addition to the symbolic plan, a geometric counterpart is built and maintained to ensure that the current geometric state matches the current symbolic state. To update the symbolic state, some literals are computed by GTP (e.g. an object isOn a table, and so on) and sent to HATP to update the symbolic state. This ensures the consistency of the symbolic state and allows to tackle the ramification problem: when an unexpected side effect occurs, it is detected. We also implemented some other functionalities, as further described in [START_REF] Gharbi | Combining symbolic and geometric planning to synthesize human-aware plans: toward more efficient combined search[END_REF].

Integration of Symbolic-Geometric Planning with Assembly Planning

Integrating the assembly planner and the Symbolic-Geometric Planner (SGP) together, we were able to compute symbolic plans with associated trajectories that could be executed on the system. However, there was a combinatorial problem, since the assembly plan was given as a dependency tree where each part would specify which other part must be assembled before the symbolic planner had to find an actual assembly sequence. For instance in the cube structure in Fig. 1, the four first bars that compose the first level can be assembled in 4! = 24 different orders.

With the two other levels. this number explodes. Indeed, the worst case scenario is n! where n is the number of parts in the structure. The proposed solution is to have a tighter integration between SGP and the assembly planner.

Principles

As it has been explained in the previous section, the assembly planner takes as input a model of the structure as it should be assembled, and computes the assembly sequence using an assembly-by-disassembly approach: it tries all the ways to disassemble the structure to guess the assembly sequence and the dependencies between the parts. To improve this search, two additional tools are used, a physics engine to ensure the stability and self-sustainability of the structure at each step, and a heuristic search. The heuristic used consists in computing the risk of collision in order to find an assembly sequence with less chances of collisions (self-collisions between the parts or collisions with the obstacles). To obtain this information, bounding volumes are placed around the objects and collisions between those volumes are used. Once a solution is found, the assembly sequence is sent to HATP along with the dependencies between the parts. Thanks to the heuristic search, this assembly plan is supposedly the most likely to succeed. It is possible, when solving the problems individually, that solutions to one problem are incompatible with the other domains (e.g. it might not be possible to compute paths for an otherwise correct assembly plan). Thus, it is important to keep a loop of information between the planners. This loop can also hint each planner into the right direction to get better plans. For example, information from the symbolic planner can help the assembly planner choose a sequence of operations with better odds of succeeding on later phases of planning. At the other end of the system, a complete assembly plan can save the symbolic and geometric planners a good deal of computation, because it provides them with a smaller search space, with far less degrees of freedom.

The approach followed in this work, illustrated in Fig. 3, is to feed a structure to the assembly planner, which will generate a single assembly plan, and to feed this plan to the symbolic planner, which in turn will invoke the geometric planner as needed. The assembly planner is guided by an heuristic that can be modified with information from HATP. When an assembly plan results unfeasible during HATP or GTP phases, information about the causes of the failure can be fed back to AP to improve the heuristic and have better chances of finding a successful assembly plan.

We decided to send only one plan at a time, in order to reduce the search space HATP has to work with. Sending an explicit graph representation (e.g. an AND/OR graph) of all plans is impractical for large structures in general. The number of possible states follows a growth rate of the order of O(n!) with n being the number of pieces in the structure. Hence, a simple structure as the cube used in this work (16 pieces) can easily get a graph with too much nodes to be able to compute it, reaching the trillions. In addition to that, evaluating each plan has an important cost, because we have to try it in both GTP and HATP, which can be time consuming.

Our approach not only reduces the search space for both planners, it also allows each of them to address the part of the problem it fits better. For instance, GTP would have a hard time figuring out stability issues within a structure, but the assembly planner is specifically designed for that. Complementary, the assembly planner can only solve linear straight paths for assembling each piece, but GTP can find more Fig. 3 Complete planning architecture including assembly planning, symbolic planning and geometric task planning. The assembly planner sends the assembly plan computed thanks to the heuristic, then HATP plans the symbolic action and assesses their feasibility at geometric level thanks GTP. If the symbolic plan can not be found or if it is not geometrically feasible, the part that prevents it is sent to the heuristic, which is updated, and a new assembly plan is computed. complex solutions if they exist. While geometric analysis might be used to predict some precedence relationships between assembly operations that must be fulfilled, it misses a family of limitations of mechanical nature such as balance and friction issues (where extracting a piece in a given direction might drag other pieces out of place). The case shown in Fig. 4 demonstrates a structure where pure geometrical reasoning can not anticipate the cause of instability, since the behaviour depends on physical properties of the bodies (i.e. their masses) and there is no direct contact between the critical pieces. Since AP performs rigid body simulations on the resulting subassemblies, the problem would be detected early, and would never reach the HATP or GTP phases, thus saving a lot of computation time that would be wasted otherwise. Note that this is different from physics based geometric planning, since we are studying a stability condition inherent to the structure itself and independent from the path that agents follow while actually executing the assembly sequence. In a similar fashion, HATP can handle multi-agent domains and allocate tasks in parallel easily, while adding this to the assembly planner would increase complexity and computation time.

Fig. 4 Example of structure with potential instability. The stability depends on the order of operations where there is no contact between critical pieces. If the red block was to be removed before the green one, the structure would become unstable and the blue block would fall.

Formalisation

A planning session starts with HATP requesting an assembly plan from the assembly planner for a given structure. Such request would simply contain the name of the structure that the assembly planner needs to analyze, and a request ID that must be the same for further requests in the same session.

The assembly planner will retrieve the current world state (mainly obstacles) from the same model that GTP uses, and a description of the structure as it should be (from a CAD 3D model), and generates an assembly plan for it. Then, it will answer with a response in the form of a tuple PR = S, D , where:

• S = {s 1 , ..., s n } is the ordered sequence of assembly operations s i that must be performed to assemble the structure. Each element s i describes the type of operation and the pieces involved. At the moment, only putting the pieces in place is supported as a type of operation, but this can be generalized to other operations as screwing them in or securing them in other ways. An operation has the form s i = (id,type, pieces...), where the first element is a number to identify the mo-ment when the operations should be done (the smaller the number the earlier it must be done), then comes the type of operation, and finally the list of pieces. • D = {d 1 , ..., d m } is a set of dependencies between assembly operations. Each element d j is a tuple made of the target operation and the set of all other operations that must necessarily be performed before that one, with d j = t l , p k which reads as the set of operations p k that must be achieved before the operation t l , where t l is just the identifier of an operation s l . The set p k contains the list of identifiers for operations from S.

Making precedence relationships between operations explicit allows the symbolic planner to perform more than one operation of the sequence at the same time in multi-agent environments, with one or more assembly operations starting before all previous operations in the sequence are finished.

See below an example of such plan, for the cube in Fig. 1, where in order to assemble the vertical bar we need the four operations that put the horizontal (bottom) bars: PR = (0, place, horizontal bottom bar 0), . . . , (4, place, vertical bar 5), . . . . . . , 4, 0, 1, 2, 3 , . . .

When HATP starts, it requests the assembly plan and upon receiving it, starts the decomposition. The first step is to detect which operation to achieve first and to do so it uses the identifier, starting at 1 and going up to the number n of operations. For each operation an Assemble task is called: it detects the type of operation and execute it for all the parts listed. Then it uses the dependencies D to add causal links and in multi-agent scenario uses those links to parallelize some operations.

Heuristics

The assembly planning search space is tremendously high even for structures with a small number of pieces (ten to twenty), so we use a heuristics based best first to navigate it efficiently. While choosing heuristics to guide the assembly planning process, the goal is to reach an assembly plan with high probability of being successful during the symbolic and geometric planning phases. By feeding information from the later phases back into the assembly planner's heuristic, the odds are improved but both domains remain decoupled.

Different heuristics can be used in assembly planning for this purpose. We used a measurement of the free space available around each piece in the directions of assembly, in order to give preference to the least occluded one. The reasoning behind this heuristic is that occluded pieces are more likely to introduce difficulties during assembly by posing obstacles to the agents. For any given piece, its geometry is projected along various directions (possible assembly directions) and each collision detected will increase the cost associated to the removal of that piece. If replanning is needed, these costs can be increased according to information received from the symbolic planner. In this fashion, occlusion would be more costly if the associated piece is directly linked with the reason why the first plan was discarded.

For future work, other heuristics such as using a bounding sphere of the size of the agents may be tested.

Multi-AROMA Planning

The current implementation of GTP has a limitation: it does not allow to plan trajectories in parallel, it is only possible to plan trajectories where no other robot move or cooperatively transport one of the parts (which is considered by GTP as one "agent" acting, not two individual trajectories). The method used for trajectory planning of individual AROMAs will be described in Chapter ??. To cope with this limitation, we generate fully sequential symbolic plans that can later be transformed into plans with parallelism thanks to a post-process, as long as the dependencies between the parts are respected. The actions that GTP can plan are: goto, pick, place and pickAndPlace. The latter is more efficient than a pick followed by a place because the different step to compute the trajectories, grasp and position are interleaved. (It is still important to allow separate pick and place if we need to add actions in between.) In addition to those actions with a geometric counterpart we have a monitor action, which triggers in the supervisor a visual servoing low-level task. It could be interesting to plan it in GTP, so the position of the monitoring UAV is taken into account when planning the others trajectories, but again GTP can not plan actions in parallel. Consequently, there is no point in planning the monitoring trajectory, so in our current implementation it is just considered a symbolic task during the planning process. Figure 5 presents an extract from a plan where a monitoring task must be carried out in parallel of an assembly task. When the robot must place the part, the action is actually called PlaceInSupport because of the domain representation we use when HATP and GTP communicate to assemble parts. The idea is that HATP needs a way to tell GTP where to place the bars, and we refer to the end position as "supports". Those supports are extracted from the final configuration of each part in the assembled structured (from the same model the assembly planner uses). In this particular example, the interesting points are the causal links, they force the monitoring task to last as long as the assembly task (place in support).

Figure 6 shows another extract from a plan, this time however it is focused on the action necessary to execute a cooperative transport. Our strategy is to elect a master and create a group, each other AROMA necessary is added to the group. To assign all the AROMAs in the group (master and others alike) we use the payload of each AROMA and compare the sum to the masses of the parts to transport. However if we only limit ourselves to this comparison, we will end up trying many groups just by changing the order of the AROMAs in the group (for instance a group with UAV1 and UAV2, and another UAV2 and UAV1, two different groups for HATP, but with the similar meaning). Testing all the possible orders is useless since the order of the AROMAs in the group does not change the efficiency of the group. Moreover, it represents a very big number of attempts: N! in fact, where N is the number of AROMAs in the problem. To address this issue, we have a mechanism that stores the group that were tested on each part, and prevents to try the same group with a different order on the same piece.

Fig. 6 Extract of a plan with a cooperative transport. In order for a group of AROMAs to cooperatively transport a bar we must assign them into the group, then they must all go to the part and grab it, then the group transports the bar. When it is finally clipped to the structure only then the AROMAs are released and can go do other actions.

Refining Symbolic Plans and Dealing with intricate constraints

We illustrate in Fig. 7 the interplay between the symbolic planner and GTP to build a valid plan to assemble two simple structures: the small green and the big blue structures. As the plan is computed, it can fail because geometry constraints not seen by the high-level planner prevent an action (cluttered space, or any other problem) or it can be due to a symbolic choice that leads to impossible execution. During the planning process both "green then blue" and "blue then green" orders are tried, however, only one is feasible. Without geometric projection, there would be no difference at the symbolic level, while in fact, if the big (blue) structure is assembled first, then the small (green) one cannot be assembled because, in this specific con-text, the robot can not reach the position to place the last horizontal bar. So, only the order depicted in the picture leads to a possible plan. Fig. 7 Action stream and geometric states for the assembly of two structures. The AROMA assembles first the small green structures then proceeds with the big blue. Only this order is feasible because the AROMA must hold the bars in their middle and the long blue horizontal bar prevents it to place the last bar of the small green structure. Please notice that the actions are called Pick and Place as two separate actions but this is done only for a matter of clarity for the picture. The black arrows are pointing at the geometric state corresponding to the symbolic state.

Conclusions

This chapter has presented the algorithms used to solve the cooperative assembly planning problem. All the planners presented have been validated in simulation. The first planner, and the first step to solve the problem at stake, is the assembly planner. It builds an assembly plan that describes how the assembly must be done. However, it does not describe how to carry the assembly out using the available agents. To face this particular issue, we propose an approach based on combining several planning techniques to enrich the planning capabilities. The task planner is based on HTN (for its powerfulness and expressiveness) combined with an objectoriented language to ease the development of new domains. The domain model is such that sub-assemblies, multi-AROMA tasks and heavy parallelism are possible. Thanks to GTP, the geometric feasibility of the actions is ensured, and thanks to the physics engine from the assembly planner, the stability of the structure is guaranteed at each step of the assembly. The symbolic planner adds monitoring actions to increase the chances of success when actually executing the plan. The symbolic solution plan has a motion associated to each action, but is completely sequential. However, it is possible to have parallelism in the plan thanks to a post process as long as the dependencies between the parts are respected.

Fig. 5

 5 Fig. 5 Extract of a plan with a monitoring task. The AROMA UAV1 picks and places the bar Top02, while the UAV2 monitors this assembly.

http://bulletphysics.org


Thanh Nguyen

Evaluation of dimensional reduction methods on urban vegetation classification performance using hyperspectral data

I. Introduction

Urban vegetation : a critical issue

In a context of urbanization of urban spaces, urban vegetation is a major issue particularly to the local and global climatic concerns of the territories. Many services are rendered by urban vegetation, such as the improvement of air quality, the cooling power of the heat island or even habitats for biodiversity (Buyadi, 2015). Differentiating various vegetations types or species is therefore relevant to improve the mitigation of urban heat islands (adapting water supplies) and manage sanitary issues (release of allergic pollens). Mapping and monitoring urban vegetation is a critical issue for decision makers and many studies highlight remote sensing as a powerful approach.

Exploring the potential of hyperspectral imagery

Vegetation monitoring, especially in cities, requires high spectral and spatial resolutions to discriminate vegetation types. Compared to multispectral images, hyperspectral data offers the possibility of studying complex and dynamic environments such as cities and discriminating various natural or anthropogenic elements (Adeline, 2014). However, hyperspectral data can exhibit spectral redundancies that may affect the performance of classification algorithms. Moreover, high spectral and spatial dimensionality may be highly time consuming. Many studies claim to reduce the spectral dimension of the dataset in order to optimize the efficiency of classification methods in discriminating urban vegetation type for instance (Zhou et al, 2015;Erudel et al, 2017). The objective of this study is to evaluate the influence of three different methods of dimension reduction on the performance of urban vegetation classifications.

II. Data and Methodology

Study area

The studied site is the city center of Toulouse (43°36'16''N, 1°26'39''E) -France. The urban area is strongly artificialized and the vegetation is strongly interlocked between buildings and houses, present along the roads or in the yards of building.

Data

Airborne hyperspectral data were acquired using the Hyspex sensor (2m spatial resolution, > 480 spectral bands ranging from 0.4 to 2.5µm) in July 2015. In order to assess the potential of the future Hypxim spaceborne sensor (192 bands), hyspex data have been resampled accordingly to Hypxim specificities at 4m and 8m spatial resolution. Atmospheric corrections were applied using the Cochise method (Poutier et al, 2002).

A field observation made it possible to identify and locate, using a differential GPS (with an absolute geometric accuracy below 10 cm), 510 trees in the swath of the hyperspectral dataset. 19 different types of tree families have been identified. These points of trees are used as learning and validation datasets with no redundancy between both, but training data (class representativeness) exhibit strong heterogeneous sizes (some tree families are well represented while others exhibits only few points).

Methodological approach

The purpose of the hyperspectral images dimensional reduction is to select or extract an optimal subset from spectral bands that are relevant for the issue at stake. Reducing dataset dimensionality helps to reducing the redundancy of the variables and facilitate further processing and interpretation of the data (Khoder, 2013). and Bruzzone, 2002).

The accuracy assessment of the SVM classification is based on the overall accuracy (OA = number of well-ordered pixels/ total number of pixels) and the Kappa Index of Agreement (KIA) as it compares the correct proportion observed with the correct proportion linked to luck (KIA = 1 : classification not linked to luck, KIA = 0 : Classification linked to luck).

III. Results

Vegetation indices selection

The K-Best method contributes to select 30 vegetation indices of which 23 are related to chlorophyll contents. The method using the correlation matrix (Figure 2

IV. Discussion & Conclusion

This study aimed at evaluating the influence of reduction dimension methods on urban vegetation (tree) classifications. As a first challenge, 19 classes of tree families have been considered. Preliminary results shown that the SVM classifier perform better when using the MNF method followed by defined features selection methods. This paper demonstrates the ability of dimension reduction method to improve detailed urban vegetation classification using the hyperspectral imagery. Even if resolution improvement increases OA and KIA scores, confusions between vegetation types remain. Over and under estimations of some classes can be explained by the internal spectral variability of a single tree family. Here, we hypothesize that trees can have exhibit different spectral characteristics (due to the species considered or their sun exposure, the water availability, etc.) while belonging to the same family (e.g. Magnoliaceae family : Tulips tree from Virginia and Magnolia may have different spectral signatures). The finer the spatial resolution and the timing of observation, more these variabilities tend to dissipate (Xie et al. 2008).

Omission and commission errors can also inherit from the unbalanced training samples that influence the classifier performance. These preliminary results will be completed with some forthcoming works. Various different classifiers (SVM, Random Forest, and Deep Learning) will be assessed and compared. Results from Hypxim datasets will also be compared with those computed from Hyspec 2m data (492 spectral bands) and simulated Sentinel-2 imageries. Furthermore, vegetation types will be simplified and detailed into 5 and 38 classes respectively. The overall goal of this contribution would be to determine define and criticize the most performant methodological design (classifier, reduction dimension method) according to the training dataset available, on the one hand, and the selected vegetation nomenclature, on the other hand.

Potentialities of future spaceborne Hypxim imageries (to be launch in 2021) would thus be evaluated for urban vegetation classification. Sensing, vol. 53, no. 2, p. 1082Sensing, vol. 53, no. 2, p. -1095Sensing, vol. 53, no. 2, p. . 2015

Figure 1 :

 1 Figure 1 : General methodology of dimension reduction comparison. VI: vegetation indices. In light grey : feature selection approach. In dark grey : feature extraction approach.

  ) allow selecting 40 vegetation indices among which almost 50% are Chlorophyll related. Although, the latter selection method introduces others biophysical indicators, the global separability of classes is similar of K-Best selection. Furthermore, the 13 indices obtaining the ANOVA highest F-score in both methods represent Chlorophyll (38.25 < score-F > 14.46). May be inferred that Chlorophyll is the principal factor for vegetation families' discrimination in this study area.

Figure 2 :

 2 Figure 2: F-Score results of selected vegetation indices by correlation matrix feature selection method

Table 1 :

 1 Performances of SVM on vegetation classifications using different dimension reductionmethods applied on Hypxim hyperspectral imageries (at both 4m and 8m)

Influence of reduction dimension methods on vegetation classifications

  SVM classifier applied on the 4m resolution Hypwim dataset reduced using the MNF gives an overall accuracy score of 51.92% (KIA : 0.41) (Table1). At 8m, the OA is 46.92% (KIA : 0.35). Features selection methods provide lower OA of 45.77% (KIA : 0.33) and 45% (KIA : 0.32) for the confusion matrix and the K-Best methods respectively. Results from the PCA are the worst ones with OA below 30% (Table1) and similar to those results obtained with non-reduced hyperspectral images.

	Datasets	Spatial	Overall	KIA
		resolution	Accuracy (OA)
	Hypxim (192	4m	31.62 %	0.19
	spectral bands)
		8m	28.21 %	0.16
	Reduced with PCA	4m	28.08 %	0.01
		8m	27.70 %	0.04
	Reduced with MNF	4m	51.92%	0.41
		8m	46.92 %	0.35
	Reduced with VI	4m	45.77 %	0.33
	(correlation matrix)
	Reduced with VI (K-	4m	45 %	0.32
	best)

  Melgani et L. Bruzzone. Support vector machines for classification of hyperspectral remote-sensing images. In : Geoscience and Remote Sensing Symposium. IGARSS'02. 2002 IEEE International. IEEE, 2002. p. 506-508. 2002 L. Poutier, C. Miech, X. Lenot, et al. "COMANCHE and COCHISE: two reciprocal atmospheric codes for hyperspectral remote sensing". In : 2002 AVIRIS Earth Science and Applications Workshop Proceedings. 2002. Y. Tarabalka, J.A. Benediktsson, J. Chanussot et al. "Multiple spectral-spatial classification approach for hyperspectral data". IEEE Transactions on Geoscience and Remote Sensing, vol. 48, no 11, p. 4122-4132. 2010 Y. Xie, Z. Sha, & M. Yu. Remote sensing imagery in vegetation mapping: a review.

	K. Adeline, "Classification des matériaux urbains
	en présence de végétation éparse par
	télédétection hyperspectrale à haute résolution
	spatiale". Thèse de doctorat. Toulouse, ISAE.
	2014
	S. N. A. Buyadi, W. M. N. W. Mohd, et A. Misni.,
	"Vegetation's Role on Modifying Microclimate
	of Urban Resident". Procedia-Social and
	Behavioral Sciences, vol. 202, p. 400-407, 2015
	J. Degerickx et al. "Mapping Functional Urban
	Green Types Using Hyperspectral Remote
	Sensing." 2017 Joint Urban Remote Sensing
	Event (JURSE), 2017
	T. Erudel et al. "Criteria Comparison for
	Classifying Peatland Vegetation Types Using In
	Situ Hyperspectral Measurements." Remote
	Sensing, vol. 9, no. 8, p. 748, 2017
	J. Khoder. "Nouvel algorithme pour la réduction de
	la dimensionnalité en imagerie hyperspectrale".
	Thèse de doctorat. Université de Versailles-
	Saint Quentin en Yvelines. 2013
	F. Journal of
	plant ecology, 1(1), 9-23. 2008
	Y. Zhou et al. "Dimension Reduction Using Spatial
	and Spectral Regularized Local Discriminant
	Embedding	for	Hyperspectral	Image
	Classification."	IEEE	Transactions	on
	Geoscience and Remote


Nathalie Bertrand

Patricia Bouyer

Anirban Majumdar

Reconfiguration and message losses in parameterized broadcast networks

Keywords:

Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some given state of the broadcast protocol. Coverability is known to be undecidable for static networks, i.e. when the number of nodes and communication topology is fixed along executions.

In contrast, it is decidable in PTIME when the communication topology may change arbitrarily along executions, that is for reconfigurable networks. Surprisingly, no lower nor upper bounds on the minimal number of nodes, or the minimal length of covering execution in reconfigurable networks, appear in the literature.

In this paper we show tight bounds for cutoff and length, which happen to be linear and quadratic, respectively, in the number of states of the protocol. We also introduce an intermediary model with static communication topology and non-deterministic message losses upon sending. We show that the same tight bounds apply to lossy networks, although, reconfigurable executions may be linearly more succinct than lossy executions. Finally, we show NP-completeness for the natural optimisation problem associated with the cutoff.

Introduction

Parameterized verification. Systems formed of many identical agents arise in many concrete areas: distributed algorithms, populations, communication or cache-coherence protocols, chemical reactions etc. Models for such systems depend on the communication or interaction means between the agents. For example pairwise interactions are commonly used for populations of individuals, whereas selective broadcast communications are more relevant for communication protocols on ad-hoc networks. The capacity of the agents, and thus models that are used to represent their behaviour also vary.

Verifying such systems amounts to checking that a property holds independently of the number of agents. Typically, a consensus algorithm should be correct for any number of participants. We refer to these systems as parameterized systems, and the parameter is the number of agents. The verification of parameterized systems started in the late 80's and recently regained attention from the model-checking community [START_REF] Suzuki | Proving properties of a ring of finite-state machines[END_REF][START_REF] German | Reasoning about systems with many processes[END_REF][START_REF] Esparza | Keeping a crowd safe: On the complexity of parameterized verification (invited talk)[END_REF][START_REF] Bloem | Decidability of Parameterized Verification[END_REF]. It can be seen as particular cases of infinite-state-system verification, and the fact that all agents are identical can sometimes lead to efficient algorithms [START_REF] Emerson | Symmetry and model checking[END_REF].

28:2

Reconfiguration and message losses in parameterized broadcast networks

Broadcast networks. This paper targets the application to protocols over ad-hoc networks, and we thus focus on the model of broadcast networks [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF]. A broadcast network is composed of several nodes that execute the same broadcast protocol. The latter is a finite automaton, where transitions are labeled with message sendings or message receptions. Configuration in broadcast networks is then comprised of a set of agents, their current local states, together with a communication topology (which represents which agents are within radio range). A transition represents the effect of one agent sending a message to its neighbours.

Parameterized verification of broadcast networks amounts to checking a given property independently of the initial configuration, and in particular independently of the number of agents and communication topology. A natural property one can be interested in is coverability: a state of the broadcast protocol is coverable if some execution leads to a configuration in which one node is in that local state. When considering error states, a positive instance for the coverability problem thus corresponds to a network that can exhibit a bad behaviour.

Coverability is undecidable for static broadcast networks [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF], i.e. when the communication topology is fixed along executions. Decidability can be recovered by relaxing the semantics and allowing non-deterministic reconfigurations of the communication topology. In reconfigurable broadcast networks, coverability of a control state is decidable in PTIME [START_REF] Delzanno | On the complexity of parameterized reachability in reconfigurable broadcast networks[END_REF]. A simple saturation algorithm allows to compute the set of all states of the broadcast protocol that can be covered.

Cutoff and covering length. Two important characteristics of positive instances of the coverability problem are the cutoff and the covering length. First, the cutoff is the minimal number of agents for which a covering execution exists. The notion of cutoff is particularly relevant for reconfigurable broadcast networks since they enjoy a monotonicity property: if a state can be covered from a configuration, it can also be from any configuration with more nodes. Second, the covering length is the minimal number of steps for covering executions. It weighs how fast a network execution can go wrong. Both the cutoff and the covering length are somehow complexity measures for the coverability problem. Surprisingly, no upper nor lower bounds on these values appear in the literature for reconfigurable broadcast networks.

Contributions.

In this paper, we prove a tight linear bound for the cutoff, and a tight quadratic bound for the covering length in reconfigurable broadcast networks. Both are expressed in the number of states of the broadcast protocol. These are obtained by refining the saturation algorithm that computes the set of coverable states, and finely analysing it.

Another contribution is to introduce lossy broadcast networks, in which the communication topology is fixed, however errors in message transmission may occur. In contrast with broadcast networks with losses that appear in the literature [START_REF] Delzanno | Verification of ad hoc networks with node and communication failures[END_REF], in our model, message losses happen upon sending, rather than upon reception. This makes a crucial difference: reconfiguration of the communication topology can easily be encoded by losses upon reception, whereas it is not obvious for losses upon sending. Perhaps surprisingly, we prove that the set of states that can be covered in reconfigurable semantics agrees with the one in static lossy semantics. Using the same refined saturation algorithm, we prove that same tight bounds hold for lossy broadcast networks: the cutoff is linear, and the covering length is quadratic (in the number of states of the broadcast protocol). The two semantics thus appear quite similar, yet, we show that the reconfigurable semantics can be linearly more succinct (in terms of number of nodes) than the lossy semantics.

Finally, we study a natural decision problem related to the cutoff: decide whether a state is coverable (in either semantics) with a fixed number of nodes. We prove it to be NP-complete.

N. Bertrand, P. Bouyer and A. Majumdar

28:3

Outline. In Section 2, we define the broadcast networks, with static, reconfiurable and lossy semantics. In Section 3, we present our tight bounds for cutoff and covering length. In Section 4, we show our succinctness result. In Section 5, we give our NP-completeness result.

∆ ⊆ (Q × {!a, ?a | a ∈ Σ} × Q) is the transition relation.
For ease of readability, we often write q !a -→ q (resp. q ?a -→ q ) for (q, !a, q ) ∈ ∆ (resp. (q, ?a, q ) ∈ ∆). We assume all broadcast networks to be complete for receptions: for every q ∈ Q and a ∈ Σ, there exists q such that q ?a -→ q .

A broadcast protocol is represented in Figure 1. In this example and in the whole paper, for concision purposes, we assume that if the reception of a message is unspecified from some state, it implicitly represents a self-loop. For example here, from q 1 , receiving a leads to q 1 again.

q 0 q 1 q 2 q 3 q 4 r 1 ⊥ !a ?a !b 1 ?a !b 2 ?b 1 ?b 2 ?b i Figure 1
Example of a broadcast protocol.

Broadcast networks involve several copies, or nodes, of the same broadcast protocol P. A configuration is an undirected graph whose vertices are labelled with a state of Q. Transitions between configurations happen by broadcasts from a node to its neighbours.

Formally, given a broadcast protocol P = (Q, I, Σ, ∆), a configuration is an undirected graph γ = (N, E, L) where N is a finite set of nodes; E ⊆ N × N is a symmetric and irreflexive relation describing the set of edges; finally, L : N → Q is the labelling function. We let Γ(P) denote the (infinite) set of Q-labelled graphs. Given a configuration γ ∈ Γ(P), we write

n ∼ n whenever (n, n ) ∈ E and we let Neigh γ (n) = {n ∈ N | n ∼ n } be the neighbourhood
of n, i.e. the set of nodes adjacent to n. Finally L(γ) denotes the set of labels appearing in

nodes of γ. A configuration (N, E, L) is called initial if L(N) ⊆ I.
The operational semantics of a static broadcast network for a given broadcast protocol P is an infinite-state transition system T (P). Intuitively, each node of a configuration runs protocol P, and may send/receive messages to/from its neighbours. From a configuration γ = (N, E, L), there is a step to γ = (N , E , L ) if N = N, E = E, and there exists n ∈ N and a ∈ Σ such that (L(n), !a, L (n)) ∈ ∆, and for every n ∈ N, if n ∈ Neigh γ (n), then (L(n ), ?a, L (n )) ∈ ∆, otherwise L (n ) = L(n ): a step reflects how nodes evolve when one of them broadcasts a message to its neighbours. We write γ n,!a --→ s γ , or simply γ → s γ (the s subscript emphasizes that the communication topology is static).

An execution of the static broadcast network is a sequence ρ = (γ i ) 0≤i≤r of configurations (N, E, L i ) such that γ 0 is an initial configuration, and for every 0 ≤ i < r, γ i → s γ i+1 . We

C O N C U R 2 0 1 9

28:4

Reconfiguration and message losses in parameterized broadcast networks write #nodes(ρ) for the number of nodes in γ 0 , #steps(ρ) for the number r of steps along ρ, and for any node n ∈ N, #steps(ρ, n) for the number of broadcasts, called the active length, of node n along ρ. Note that, along an execution, the number of nodes and the communication topology are fixed. The set of all static executions is denoted Exec s (P).

Coverability problem.

Given a broadcast protocol P and a subset of target states F ⊆ Q, we write COVER s (P, F )

for the set of all covering executions, that is, executions that visit a configuration with a node labelled by a state in F :

COVER s (P, F ) = {(γ i ) 0≤i≤r ∈ Exec s (P) | L(γ r ) ∩ F = ∅}.
The coverability problem is a decision problem that takes a broadcast protocol P and a subset of target states F as inputs, and outputs whether COVER s (P, F ) is nonempty. For broadcast networks, the coverability problem is a parameterized verification problem, since the number of initial configurations is infinite. It is known that coverability is undecidable for static broadcast networks [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF], since one can use the communication topology to build chains that may encode values of counters, and hence simulate Minsky machines [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF].

If the broadcast protocol P allows to cover the subset F , we define the cutoff as the minimal number of nodes required in an execution to cover F . Similarly, we define the covering length as the length of a shortest finite execution covering F . Those values are important to characterize the complexity of a broadcast protocol: assuming a safe set of states, coverability of the complement set represents bad behaviours, and cutoff and covering length measure the size of minimal witnesses for violation of the safety property.

Reconfigurable broadcast networks

To circumvent the undecidability of coverability for static broadcast networks, one attempt is to introduce non-deterministic reconfiguration of the communication topology. This solution also allows one to model arbitrary mobility of the nodes, which is meaningful, e.g. for mobile ad-hoc networks [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF].

Under this semantics, configurations are the same as under the static semantics. Transitions between configurations however are enhanced by the ability to modify the communication topology before performing a broadcast. Formally, from a configuration γ = (N, E, L), there is a step to γ = (N , E , L ) if N = N, and there exists n ∈ N and a ∈ Σ such that

(L(n), !a, L (n)) ∈ ∆, and for every n ∈ N, if n ∈ Neigh γ (n), then (L(n), ?a, L (n )) ∈ ∆, otherwise L (n ) = L(n ):
a step thus reflects that the communication topology may change from E to E followed by the broadcast of a message from a node to its neighbours in the new topology. We write γ n,!a --→ r γ , or simply γ → r γ .

Similarly to the static case, we write Exec r (P) and COVER r (P, F ) for, respectively the set of all reconfigurable executions in P, and the set of all reconfigurable executions in P that cover F . We will also use the same notations #nodes(ρ), #steps(ρ) and #steps(ρ, n) as in the static case. N. Bertrand, P. Bouyer and A. Majumdar

28:5

A noticeable property of reconfigurable broadcast networks is the following copycat property. Such a monotonicity property was originally shown in [START_REF] Esparza | Parameterized verification of asynchronous shared-memory systems[END_REF] for asynchronous sharedmemory systems, and it also applies to our context.

Proposition 2 (Copycat for reconfigurable semantics). Given ρ :

γ 0 → r γ 1 • • • → r γ s an
execution, with γ s = (N, E, L), for every q ∈ L(γ s ), for every n q ∈ N such that L(n q ) = q, there exists t ∈ N and an execution ρ :

γ 0 → r γ 1 • • • → r γ t with γ t = (N , E , L ) such that |N | = |N|+1, there is an injection ι : N → N with for every n ∈ N, L (ι(n)) = L(n)
, and for the extra node n fresh ∈ N \ ι(N), L (n fresh ) = q, and #steps(ρ , n fresh ) = #steps(ρ, n q ).

Intuitively, the new node n fresh will copy the moves of node n q : it performs the same broadcasts (but to nobody) and receives the same messages. More precisely, when n q broadcasts in ρ, it does so also in ρ and then we disconnect all the nodes and n fresh repeats the broadcast (no other node is affected because of the disconnection); when n q receives a message in ρ, we connect n fresh to the same neighbours as n q (i.e., ι(n) ∼ n fresh if and only if n ∼ n q ) so that n fresh also receives the same message in ρ .

Relying on the copycat property, when reconfigurations are allowed, the coverability problem becomes decidable and solvable in polynomial time.

Theorem 3 ([2]

). Coverability is decidable in PTIME for reconfigurable broadcast networks.

More precisely, a simple saturation algorithm allows one to compute in polynomial time, the set of all states that can be covered. Despite this complexity result, to the best of our knowledge, no bounds on the cutoff or length of witness executions are stated in the literature.

Broadcast networks with messages losses

Communication failures were studied for broadcast networks, assuming non-deterministic message losses could happen: when a message is broadcast, some of the neighbours of the sending node may not receive it [START_REF] Delzanno | Verification of ad hoc networks with node and communication failures[END_REF]. As observed by the authors, the coverability problem for such networks easily reduces to the coverability problem in reconfigurable networks by considering a complete topology, and message losses are simulated by reconfigurations.

Thus, message losses upon reception are equivalent to reconfiguration of the communication topology.

We propose an alternative semantics here: when a message is broadcast, it either reaches all neighbours of the sending node, or none of them. This is relevant in contexts where broadcasts are performed in an atomic manner and may fail. In contrast to message losses upon reception, it is not obvious to simulate arbitrary reconfigurations of the communication topology with such message losses.

Formally, from a configuration γ = (N, E, L), there is a step to γ = (N , E , L ) if N = N, E = E and there exists n ∈ N and a ∈ Σ such that (L(n), !a, L (n)) ∈ ∆, and either (a) for

every n = n, L (n ) = L(n ) (no one has received the message, it has been lost), or (b) if n ∈ Neigh γ (n), then (L(n ), ?a, L (n )) ∈ ∆, otherwise L (n ) = L(n ): a step thus reflects that
the broadcast message may be lost when it is sent. We write γ n,!a --→ l γ or simply γ → l γ .

Similarly to the static and reconfigurable semantics, #steps(ρ, n) is the number of broadcasts (including lost ones) by node n along ρ; and we write #nonlost_steps(ρ, n) for the number of successful broadcasts by node n along ρ.

For lossy executions also, we use the following notations: Exec l (P) and COVER l (P, F ).

Any lossy execution can be seen as a reconfigurable execution. Indeed, a lossy execution

C O N C U R 2 0 1 9

28:6

Reconfiguration and message losses in parameterized broadcast networks with communication topology E can be transformed into a reconfigurable one in which the communication topology of each configuration is either ∅ or E, depending on whether the next broadcast is lost or not. Therefore, with slight abuse of notation, we write Exec l (P) ⊆ Exec r (P). Figure 2 gives an example of a lossy execution for the broadcast protocol of Figure 1.

Note that in the third transition, some node indeed performs a lossy broadcast, emphasized by the subscript "lost". As before, the colored nodes broadcast a message in the step leading to the next configuration.

q0 q0 q0 q0 q0 !a -→ l q1 q0 q0 q1 q0 !b 1 -→ l q2 r1 ⊥ q1 q0 !b 1 -→ l lost q2 r1 ⊥ q2 q0 !a -→ l q2 ⊥ q0 q3 r1 !b 2 -→ l q2 ⊥ ⊥ q4 Figure 2
Example of a lossy execution on the protocol from Figure 1.

Tight bounds for reconfigurable and lossy broadcast networks

In this section, we will show tight bounds for the cutoff and the minimal length of a witness execution for the coverability problem. These hold both for the reconfigurable and the lossy semantics.

Upper bounds on cutoff and covering length for reconfigurable networks

First, we will refine the polytime saturation algorithm of [START_REF] Delzanno | On the complexity of parameterized reachability in reconfigurable broadcast networks[END_REF], which computes all states which can be covered in the reconfigurable semantics. We will then show that, based on the underlying computation, one can construct small witnesses for the two semantics (linear number of nodes and quadratic number of steps). While it would be enough to show the result for the lossy semantics (since, given a broadcast protocol P, Exec l (P) ⊆ Exec r (P)),

for pedagogical reasons, we provide the two proofs, starting with the simplest one for reconfigurable semantics.

Let us fix for the rest of this section, a protocol P = (Q, I, Σ, ∆). We slightly modify the algorithm given in [START_REF] Delzanno | On the complexity of parameterized reachability in reconfigurable broadcast networks[END_REF] as follows: we include at most one state to the set S in each iteration.

Additionally, we associate a labelling function c : S → N with the set S in every iteration.

More formally, we consider the modification of the previous saturation algorithm as shown in Algorithm 1.

N. Bertrand, P. Bouyer and A. Majumdar

28:7

Algorithm 1 Refined saturation algorithm for coverability if ∃(q 1 , !a, q 2 ) ∈ ∆ s.t. q 1 ∈ S and q 2 ∈ S then else if ∃(q 1 , !a, q 2 ) ∈ ∆ and (q 1 , ?a, q 2 ) ∈ ∆ s.t. q 1 , q 2 , q 1 ∈ S and q 2 ∈ S then end if 9: end while 10: return S In Algorithm 1, the variable c counts the number of nodes that are sufficient to cover the current set S, as we will prove later.

Lemma 4 ([2]

). Algorithm 1 terminates and returns the set of coverable states. In particular, COVER r (P,

F ) = ∅ iff F ∩ S = ∅.
Let S 0 , S 1 , . . . , S m be the sets after each iteration of the algorithm, with S 0 = I and S m = S. We fix an ordering on the states in S on the basis of insertion in S: for all 1 ≤ i ≤ m, q i is such that q i ∈ S i \ S i-1 . In the following, we show the desired upper bounds, proving that there exists an execution of size O(n) and length O(n 2 ) covering at the same time all states of S m .

Theorem 5. Let P = (Q, I, Σ, ∆) be a broadcast protocol, and

F ⊆ Q. If COVER r (P, F ) = ∅ (that is, if F ∩ S = ∅), then there exists ρ ∈ COVER r (P, F ) with #nodes(ρ) ≤ 2|Q| and #steps(ρ) ≤ 2|Q| 2 .
Theorem 5 is a consequence of the following Lemma. Lemma 6. For every step i of Algorithm 1, there exists an initial configuration γ 0 , a configuration γ and a reconfigurable execution ρ :

γ 0 * -→ r γ such that L(γ) = S i , #nodes(ρ) = c(S i ), and max n #steps(ρ, n) ≤ i.
Proof. The lemma is proved by induction on i. The base case i = 0 is obvious: take the initial configuration γ 0 with |I| nodes, and label each node with a different initial state; its size is |I|, and the length of the execution is 0, hence so is the maximum active length.

To prove the induction step, we distinguish two cases: depending on whether q i+1 was added as the target state of a broadcast transition q !a -→ for some q ∈ S i ; or whether q i+1 is the target state of a reception from some q ∈ S i with matching broadcast between two states already in S i .

Case 1: There exists q ∈ S i with q !a -→ q i+1 . We apply the induction hypothesis to step i, and exhibit an execution ρ :

γ 0 * -→ r γ such that L(γ) = S i , #nodes(ρ) = c(S i ) and max n #steps(ρ, n) ≤ i.
Applying the copycat property (see Proposition 2), we construct an execution ρ : γ 0 * -→ r γ such that γ 0 has one node more than γ 0 , and, focusing on the nodes (since we are in a reconfigurable setting, edges in the configuration are not important), γ coincides with γ, with an extra node n labelled by q. We then disconnect all nodes and extend with a transition γ n,!a --→ r γ , which makes only progress node n from q to q i+1 ; the resulting execution is denoted ρ . Then:

1. L(γ ) = S i ∪ {q i+1 } = S i+1 , C O N C U R 2 0 1 9

28:8

Reconfiguration and message losses in parameterized broadcast networks 2. #nodes(ρ ) = c(S i ) + 1 = c(S i+1 ), 3. max n #steps(ρ , n) ≤ max n #steps(ρ, n) + 1 ≤ i + 1; Indeed, the active length of the copycat node along ρ coincides with the active length of some existing node along ρ, and it is increased only by 1 in ρ . This proves the induction step in the first case.

Case 2: There exists q, q , q ∈ S i with q ?a -→ q i+1 and q !a -→ q . The idea is similar to the previous case, but one should apply the copycat property twice, to both q and q . We formalize this.

We apply the induction hypothesis to step i, and exhibit an execution ρ : γ 0 * -→ r γ such that L(γ) = S i , #nodes(ρ) = c(S i ) and max n #steps(ρ, n) ≤ i. Applying the copycat property (see Proposition 2) twice, to both q and q , we construct an execution ρ : γ 0 * -→ r γ such that γ 0 has two nodes more than γ 0 , and, focusing on the nodes, γ coincides with γ, with one extra node n labelled by q and one extra node n labelled by q . We then connect nodes n and n and disconnect all other nodes, and extend with a transition γ n ,!a ---→ r γ ; this makes node n progress from q to q i+1 and node n progress from q to q ; all other nodes are unchanged; the resulting execution is denoted ρ . Then:

1. L(γ ) = S i ∪ {q , q i+1 } = S i+1 since q ∈ S i , 2. #nodes(ρ ) = c(S i ) + 2 = c(S i+1 ), 3. max n #steps(ρ , n) ≤ max n #steps(ρ, n) + 1 ≤ i + 1;
Indeed the active length of any of the copycat node along ρ coincides with the active length of some existing node along ρ, and it is increased by at most 1 in ρ . This proves the induction step in the second case, which allows to conclude the proof of the lemma.

To conclude the proof of Theorem 5, we recall that Algorithm 1 is sound and complete: S m is the set of states that can be covered. Hence, from Lemma 6, we deduce that if COVER r (P, F ) = ∅, then there is ρ ∈ COVER r (P, F ) such that:

1. L(γ) = S m ; 2. #nodes(ρ) = c(S m ) ≤ |I| + 2m ≤ |I| + 2(|Q| -|I|) = 2|Q| -|I|; 3. max n #steps(ρ, n) ≤ m ≤ |Q| -|I|.
Therefore #steps(ρ) ≤ #nodes(ρ) • max n #steps(ρ, n) ≤ 2|Q| 2 , so that we established the desired bounds for Theorem 5.

Upper bounds on cutoff and covering length for lossy networks

Perhaps surprisingly, Algorithm 1 also computes the set of states that can be covered by lossy executions. Concerning coverable states, the reconfigurable and lossy semantics thus agree. In Section 4, we will show that reconfigurable covering executions can be linearly more succinct than lossy covering executions. N. Bertrand, P. Bouyer and A. Majumdar

Lemma 7. Algorithm 1 returns the set of coverable states for lossy broadcast networks. In

28:9

Before going to the proof of Theorem 8, we show a copycat property for the lossy broadcast networks, as a counterpart of Proposition 2 for the lossy semantics. Since the communication topology is static in lossy networks, the following proposition explicitly relates the communication topologies in the initial execution and its copycat extension. Proposition 9 (Copycat for lossy semantics). Given ρ : γ 0 → l γ 1 • • • → l γ r an execution, with γ r = (N, E, L), for every q ∈ L(γ r ), for every n q ∈ N such that L(n q ) = q, there exists s ∈ N and an execution ρ :

γ 0 → l γ 1 • • • → l γ s with γ s = (N , E , L ) such that |N | = |N|+1
, there is an injection ι : N → N with for every n ∈ N, L (ι(n)) = L(n), and for the extra node n fresh ∈ N \ ι(N), L (n fresh ) = q, for every n ∈ N, n fresh ∼ ι(n) iff n q ∼ n, #steps(ρ , n fresh ) = #steps(ρ, n q ), and #nonlost_steps(ρ , n fresh ) = 0.

Proof. First notice that, from our definition of lossy semantics, the topology should be the same in γ 0 and in γ r , hence we can write γ 0 = (N, E, L 0 ), and more generally, for every i, γ i = (N, E, L i ). Define N as a finite set such that |N | = |N| + 1, and fix an injection ι : N → N . Write n fresh for the unique element of N \ ι(N). Set L 0 (ι(n)) = L 0 (n) for every n ∈ N, and L 0 (n fresh ) = L 0 (n q ). Define the edge relation E by its induced edge relation ∼

such that ι(n) ∼ ι(n ) iff n ∼ n , and n fresh ∼ ι(n ) iff n q ∼ n .
The idea will then be to make n fresh follow what n q is doing. Roughly, if n q is receiving a message to progress, then we will connect n fresh to a relevant node to also receive the message; if n q is broadcasting a message, then we will make n fresh broadcast a message and lose, so that no other node is impacted.

Formally, we will show by induction on i that for every 0 ≤ i ≤ r, there is an execution

ρ i : γ 0 → l γ 1 • • • → l γ f (i) for some f (i), such that L i (ι(n)) = L i (n) for every n ∈ N and L i (n fresh ) = L i (n q ).
The initial case i = 0 is obvious. We then assume that we have constructed a relevant ρ i for some i < r, and we will extend it to ρ i+1 as follows. We make a case distinction depending on the nature of the step γ i → l γ i+1 : Assume γ i n,!a --→ l γ i+1 is a broadcast message with n q = n, then ρ i+1 is obtained by extending ρ i with the broadcast γ f (i)

ι(n),!a ----→ γ f (i)+1
, with the condition that it should be lost if and only if it was lost in the original execution. For checking correctness, we distinguish two cases: the broadcast message was not lost, and n q ∼ n. Then, it is the case that n fresh ∼ ι(n), hence n fresh also receives the message. By resolving properly the nondeterminism, we can make the label of n fresh become the same as the label of n q in γ f (i)+1 . Note also that all nodes in ι(N) can progress to the same states as those of N in γ i+1 ; the broadcast message was lost, or n q ∼ n, then it is the case that the label of n q has not been changed in γ i n,!a --→ l γ i+1 , and so will the label of the fresh node in γ f (i) .

Assume γ i n q ,!a ---→ l γ i+1 is a broadcast message, then we extend ρ i with the two steps

γ f (i) ι(n q ),!a -----→ γ f (i)+1 n fresh ,!a ----→ γ f (i)+2
(resolving nondeterminism in a similar way as in

γ i n q ,!a ---→ l γ i+1
), and we make the last broadcast lossy whereas the broadcast from ι(n q ) is lossy if and only if it was lossy in γ i → l γ i+1 . This concludes the induction. Notice that in the constructed execution, node n fresh does not make any real sending.

For any configuration γ = (N, E, L) and a node n, we write L(n) = × if n is not important anymore in the execution, in other words all the required conditions in γ such that γ * -→ l γ are still satisfied whatever L(n) is.

C O N C U R 2 0 1 9

28:10 Reconfiguration and message losses in parameterized broadcast networks

Recall the saturation algorithm and the ordering of the sets and the states: S 0 = I, S 1 , . . . , S m = S are the sets after each iteration and q i is the state such that q i ∈ S i \ S i-1 for all 1 ≤ i ≤ m. We will refine the construction from the proof of Lemma 6 (in the context of reconfigurable broadcast networks), and build inductively a lossy execution covering all states in S i . Since the topology is static, some nodes which have "finished their jobs" will remain connected to other nodes, and may therefore continue to change states (contrary to Lemma 6 where they could be fully disconnected). Hence, in every such execution, every state q ∈ S i (which is then covered by the execution) will have a main corresponding node, whose label will remain q. All nodes which are not the main node of a state will be assigned ×, since their labels will become meaningless.

We formalize this idea in the lemma below. However, for better understanding, we also illustrate this inductive construction of a witness execution in Figure 4 on the simple broadcast protocol from Figure 3. Configurations are represented vertically: they involve 10 nodes, and the communication topology is given for the first configuration only, for the sake of readability. To save space, several broadcasts (of the same message type, from different nodes) may happen in a macrostep that merges several steps. This is for instance the case in the first macrostep, where a is being broadcast from the node in set S 1 , as well as from the first node in set S 2 . Dashed arrows are used to represent that a node is not involved in some macrostep and thus stays in the same state. In the execution, the nodes that are performing a real broadcast are colored yellow, the ones which receive a message are colored gray, and blue nodes indicate the main nodes for the coverable states. Lemma 10. For every step i of the refined saturation algorithm, there exists a configuration γ = (N, E, L) and an execution ρ : γ 0 * -→ l γ such that:

L(γ) \ {×} = S i and #nodes(ρ) = c(S i ), max n #steps(ρ, n) ≤ i and max n #nonlost_steps(ρ, n) ≤ 1,
for every q ∈ S i , there exists n main q ∈ N such that L(n main q ) = q and #nonlost_steps(ρ, n main q ) = 0,

n main q ∼ n implies L(n) = ×, and if n / ∈ {n main q | q ∈ S i }, then L(n) = ×.
Proof. We do the proof by induction on i. The case i = 0 is obvious, by picking one main node per initial state in I, and by disconnecting all nodes; hence forming an initial configuration satisfying all the requirements.

To prove the induction step, we distinguish two cases: depending on whether q i+1 was added as the target state of a broadcast action !a from some q ∈ S i ; or whether q i+1 is the target state of a reception from some q ∈ S i with matching broadcast between two states already in S i .

Case 1: There exists q ∈ S i with q !a -→ q i+1 . We apply the induction hypothesis to step i, and exhibit the various elements of the statement. Applying the copycat property for lossy broadcast systems (that is, Proposition 9) with node n main q , we build an execution

ρ : γ 0 * -→ l γ such that γ = (N, E, L ) with |N | = |N| + 1
, and an appropriate injection ι.

The fresh node n fresh is connected to nodes to which n main q was connected before; hence, by induction hypothesis, it is only connected to nodes labelled with ×. Then we extend ρ with γ n fresh ,!a ----→ γ and lose the message (this is for condition #nonlost_steps(ρ, n main q ) = 0 to be satisfied). We declare n main qi+1 = n fresh . All requirements for γ are easily checked to be satisfied (when a node is labelled with × in γ , then it remains labelled by × in γ ).

Case 2: There exist q, q , q ∈ S i such that q ?a -→ q i+1 and q !a -→ q . We apply the induction hypothesis to step i, and exhibit the various elements of the statement. Applying twice the copycat property (that is, Proposition 9), once with node n main q and once with N. Bertrand, P. Bouyer and A. Majumdar 28:11 q 0 q 1 q 2 q 3 q 4 q 5 q 6

!a ?a !b ?b !c ?c

Figure 3 Illustrating example for the saturation algorithm. and an appropriate injection ι. The two fresh nodes n fresh and n fresh are only connected to ×-nodes in γ (by induction hypothesis on n main q and n main q respectively). We transform γ 0 into γ 0 by connecting the two nodes n fresh and n fresh . By Proposition 9, we know that those two nodes don't perform any real sending (i.e., #nonlost_steps(ρ , n fresh ) = 0 and #nonlost_steps(ρ , n fresh ) = 0), hence this new connection will not affect the labels of the nodes, and we can safely apply the same transitions as in ρ from γ 0 to get an execution C O N C U R 2 0 1 9 28:12 Reconfiguration and message losses in parameterized broadcast networks ρ : γ 0 * -→ l γ , where γ coincides with γ , with an extra connection between nodes n fresh and n fresh . Then, we extend ρ with γ n fresh ,!a ----→ γ . We assume it is a real sending, hence:

S 0 S 1 S 2 S 3 S 4 S 5 S 6 q 0 q 0 q 0 q 0 q 0 q 0 q 0 q 0 q 0 q 0 q 1 × q 2 q 2 q 2 q 0 q 0 q 0 q 2 q 2 q 2 q 1 q 1 q 1 q 2 q 3 × q 4 q 4 q 4 q 2 q 4 q 4 q 3 q 5 × q 6 q 0 q 1 × q 2 q 3 × q 4 !a lost
q 0 q 1 q 2 q 3 q 4 • • • !a 1 ?b 1 !a 2 ?b 2 !a n ?b n !b 1 !b 2 !b n
node n fresh can progress from state q to q i+1 , and node n fresh can progress from q to q . All other nodes which are connected to n fresh are labelled by × in γ , hence cannot be really affected by that sending. We relabel n fresh to ×, and declare n main qi+1 = n fresh . The expected conditions of the statement are easily checked to be satisfied by this new execution.

Bounds are then obtained similarly to the reconfigurable case, see page 8.

Matching lower bounds for reconfigurable and lossy networks

In this section, we show that the linear bound on the cutoff and the quadratic bound on the length of witness executions are tight, both for the reconfigurable and the lossy broadcast networks.

Theorem 11. There exists a family of broadcast protocols

(P n ) n with P n = (Q n , I n , Σ n , ∆ n ),
and target states Proof. Consider P n , as depicted in Figure 5 with 2n+1 states and F n = { }. Any covering reconfigurable execution involves at least n+1 nodes, and has at least n 2 +5n 2 steps. Indeed, intuitively, the process responsible for broadcasting b i is blocked in q 2i-1 , so that n such processes are needed, plus one process in ; moreover, n+2-i broadcasts of a i and one broadcast of each b i happen.

F n ⊆ Q n with |Q n | ∈ O(n), such that for every n, COVER r (P n , F n ) = ∅, COVER l (P n , F n ) = ∅,

Succinctness of reconfigurations compared to losses

In this section, we show that reconfigurable executions can be linearly more succinct than lossy executions, in terms of number of nodes. Given the tight linear bound on cutoff, this is somehow optimal.

Theorem 12. There exists a family of broadcast protocols

(P n ) n with P n = (Q n , I n , Σ n , ∆ n )
and target states F n ⊆ Q n such that for every n:

there exists a reconfigurable covering execution in P n with 3 nodes; and any lossy covering execution in P n requires O(n) nodes.

Proof. P n is depicted in Figure 6. It has 3n+2 states and we let F n = { }. A covering reconfigurable execution of size 3 is given in Figure 7. Colored nodes broadcast a message in the step leading to the next configuration. Along that execution, the top node always remains at q 0 and alternatively broadcasts a to the middle node and disconnects; the middle node follows the chain of q i states and alternatively broadcasts b i 's to the bottom node which gradually progresses along the chain of states r i and reaches .

N. Bertrand, P. Bouyer and A. Majumdar 28:13

q 0 q 1 q 2 q 3 q 4 • • • q 2n r 1 ⊥ r 2 • • • !a ?a !b 1 ?a !b 2 ?a !b n ?b 1 ?b 2 ?b n ?b i Figure 6
Example where reconfigurable semantics needs less nodes than lossy semantics.

q0 q0 q0 !a -→ r q1 q0 q0 !b 1 -→ r q2 r1 q0 !a -→ r q3 r1 q0 !b 2 -→ r • • • !b n -→ r q2n q0
Figure 7 Covering reconfigurable execution with 3 nodes on the protocol from Figure 6.

Let us argue that in the lossy semantics, O(n) nodes are needed to cover . Obviously, one node, say n , is needed to reach the target state, after having received sequentially all the b i 's (which should then correspond to real broadcasts). Towards a contradiction, assume there is a node n which makes n progress twice, that is, n is connected to n and performs at least two real broadcasts, say !b i and !b j with i < j. Node n needs to receive j -i > 0 times the message a after the real !b i has occurred, hence there must be at least one node in state q 0 connected to n after the real !b i by n. This is not possible, since this node has received the real !b i while being in q 0 , leading to ⊥ if i > 1, otherwise ⊥ or r 1 . Hence, each broadcast !b i needs to be sent by a different node. This requires at least n+1 nodes, say {n i | 1 ≤ i ≤ n} ∪ {n }: node n i is responsible for broadcasting (with no loss) b i and n progresses towards . Notice that n might be the node responsible for broadcasting all the a's. We conclude that n+1 is a lower bound on the number of nodes needed to cover in the lossy semantics.

To complete this example, observe that n+1 nodes do actually suffice in lossy semantics to cover . Let N = {n i | 1 ≤ i ≤ n} ∪ {n } and consider the static communication topology defined by n i ∼ n for every i. In the covering lossy execution, node n initially broadcasts a's, so that all its neighbours, the n i 's can move to q 2i-1 , using lost sendings. Then the each node n i broadcasts its message b i to n , starting with n 1 until n n , so that n reaches .

Complexity of deciding the size of minimal witnesses

We now consider the following decision problem of determining the minimal size of coverability witnesses for both the reconfigurable and lossy semantics.

Minimum number of nodes for coverability (MinCover) Input: A broadcast protocol P, a set of states F ⊆ Q, and k ∈ N. Question: Does there exist a reconfigurable/lossy execution ρ covering some state in F , and with #nodes(ρ) = k? By the copycat properties (for both semantics), if there is a covering execution of size less than k, then there is one of size exactly k.

C O N C U R
Theorem 13. MinCover is NP-complete for both reconfigurable and lossy broadcast networks.

The NP-hardness of MinCover is proved by reduction from SetCover, which is known to be NP-complete [START_REF] Karp | Reducibility among combinatorial problems[END_REF]. Recall that SetCover takes as input a finite set of elements U, a collection S of subsets of U and an integer k, and returns yes iff there exists a subcollection of S of size at most k that covers U.

Given an instance of the SetCover problem (U, S, k) with U = {a 1 , a 2 , . . . , a n } and S = {S 1 , S 2 , . . . , S m }, we build a protocol P = (Q, I, Σ, ∆) as depicted in Figure 8, where we assume S i = {a i1 , a i2 , . . . } for every i.

We can then show that U has a cover using S of size k if and only if there exists a reconfigurable/lossy execution for P covering F and with k+1 nodes.

For the NP-membership, it suffices to observe that the length of a minimal covering execution is polynomially bounded, thanks to Theorem 5 and 8. Moreover, configurations and updates of configurations by given transitions can be represented in and computed in a compact way. It is thus possible to implement a guess-and-check NP-algorithm for the MinCover problem, that non deterministically guesses an execution with k nodes of maximal length that is polynomially bounded in the size of the broadcast protocol.

Conclusion

In this paper, we have given a tight linear bound on the cutoff and a tight quadratic bound on the covering length for reconfigurable broadcast networks. We have also proposed a new semantics for broadcast networks with a static topology, where messages can be lost at sending. Similar tight bounds can be proven for that new semantics. Proofs are based on a refinement of the saturation algorithm of [START_REF] Delzanno | On the complexity of parameterized reachability in reconfigurable broadcast networks[END_REF], and on fine analysis of copycat lemmas. As a side result of these constructions, we get that the set of states which can be covered by the two semantics is actually the same, but that the reconfigurable semantics can be linearly more succinct (in terms of number of nodes). We also prove the NP-completeness for the existence of a witness execution with the minimal number of nodes.

As future work, we want to pursue the study of the model with stochastic losses, and design analysis algorithms for various quantitative questions. Also, in this work we have not studied the tradeoff between number of nodes and length of covering computation. The precise interplay between number of nodes and length of covering execution is a possible direction for future work.

Figure 7 (

 7 Figure 7 (with n = 2) gives an example of reconfigurable execution for the broadcast protocol of Figure 1 (which covers ). Note that the communication topology indeed evolves along the execution. Here the colored nodes broadcast a message in the step leading to the next configuration.

1 :

 1 S := I; c(S) := |I|; S := ∅ 2: while S = S do 3: S := S; c := c(S) 4:

5 :S

 5 := S ∪ {q 2 }; c(S) := c + 1 6:

7 :S

 7 := S ∪ {q 2 }; c(S) := c + 2 8:

  particular, COVER l (P, F ) = ∅ iff F ∩ S = ∅. Indeed, we have Exec l (P) ⊆ Exec r (P). Therefore COVER l (P, F ) = ∅ implies COVER r (P, F ) = ∅ and by Lemma 4, we conclude F ∩ S = ∅. The other direction of Lemma 7 is a consequence of the following theorem. Theorem 8. Let P = (Q, I, Σ, ∆) be a broadcast protocol, and F ⊆ Q. If S ∩ F = ∅, then there exists ρ ∈ COVER l (P, F ) with #nodes(ρ) ≤ 2|Q| and #steps(ρ) ≤ 2|Q| 2 .

Figure 4

 4 Figure 4 Applying saturation algorithm on protocol in Figure 3 in lossy semantics. Configurations are represented vertically; for readability, macrosteps merge several broadcasts.

Figure 5

 5 Figure 5 Broadcast protocol with linear cutoff and quadratic covering length.

  and any witness reconfigurable or lossy execution has size O(n) and length O(n 2 ).

Figure 8

 8 Figure 8 Illustration of the reduction to prove NP-hardness of MinCover.

2 0 1 9 28:14 Reconfiguration and message losses in parameterized broadcast networks

  !a 11 , !a 12 , • • • !a 21 , !a 22 , • • • !a m1 , !a m2 , • • •

	s 1			s 2		. . .	s m
	q 1	?a 1	q 2	?a 2	q 3	?a 3	• • •	q n	?a n

Funding

The second author was supported by ERC project EQualIS (308087).