Marie Lévêque

Sébastien Dutour

Jacques Lluc

Pascal Lavieille

Marc Miscevic

Yves Bertin

Raphael Mari

Laura Fourgeaud

Marie Levêque

Experimental study of a Capillary Pumped Loop assisted with a mechanical pump placed at the evaporator inlet

Keywords: Capillary Pumped Loop, Hybrid loop, Mechanical pumping, Electronics cooling

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

Introduction

Capillary Pumped Loop (CPL) and Loop Heat Pipe (LHP) are heat transfer and transport systems highly relevant to the cooling of electronic systems [START_REF] Maydanik | Loop heat pipes[END_REF]. They can transfer tens of kW released at more than 100 W/cm 2 by multiple heat sources. These features are decisive in space applications and terrestrial transportation where electronic components integration is critically increasing.

The loop performance is mainly related to the capillary evaporator efficiency. The vaporisation of the working fluid within a porous wick leads to the formation of a complex liquid-vapor interface made of small menisci pumping the liquid at the pore scale. This process results in a quasi-uniform evaporator wall temperature with a high heat transfer coefficient between the evaporator wall and the fluid. Moreover, as the menisci could adjust their curvature according to the interface pressure drop, the liquid pumping at the evaporator inlet is adapted to the vaporisation rate. Thus, the evaporator thermal performance can be maintained for a large range of heat loads without any external flow control. However, the evaporator differential pressure available for pumping reaches a maximum inherent to the porous structure and fluid properties (the capillary limit). For instance, this limit is about 25 kPa for wick with 2 µm pore * corresponding author Email address: sebastien.dutour@laplace.univ-tlse.fr (Sébastien Dutour ) mean radius and with ammonia as the working fluid [START_REF] Kaya | Numerical simulation of transient operation of loop heat pipes[END_REF]. When the loop pressure drop exceeds this limit, the vapor deeply spreads within the wick. This can deteriorate the wick pumping leading to the evaporator dry-out and a critical temperature increase of the dissipative sources.

The LHP and CPL coupling with a mechanical pump is a way to overcome this capillary limit. More generally, it gives the opportunity of an important enhancement of the capillary two-phase loops performance. Schweickart et al. [START_REF] Schweickart | Testing of a controller for a hybrid capillary pumped loop thermal control system[END_REF] studied a hybrid loop configuration consisting of a CPL assisted by a volumetric pump. The CPL included eight parallel evaporators, ten meters of both liquid and vapor lines, six parallel condenser lines, a subcooler, and a thermally controlled reservoir. The mechanical pump was placed downstream the reservoir at the inlet of the evaporators. A specific controller was developed so that the flow rate was controlled as a function of the loop heat load. Tests have demonstrated a greater heat transport capability. However, this improvement appeared to be restricted to a 14% heat load increase because of many limitations other than the evaporators pressure drop such as evaporator liquid flooding.

A different configuration of a hybrid loop with two flat-type capillary driven evaporators and a volumetric gear pump was developed by Park et al. [START_REF] Park | Performance evaluation of pump-assisted capillary two-phase loop[END_REF], Crepinsek and Park [START_REF] Crepinsek | Effect of Operational Conditions on Cooling Performance of Pump-Assisted Capillary-Driven Two-Phase Loop[END_REF], [START_REF] Crepinsek | Experimental analysis of pump-assisted and capillary-driven dual-evaporators two-phase cooling loop[END_REF]. The objective was to transfer heat flux higher than 100 W cm -2 such as required by power electronics cooling. A liquid loop circulation starting and finishing at the reservoir was ensured by the mechanical pump located downstream the reservoir. The liq-uid flowed through the liquid chambers within the evaporators but, as the porous wick of the evaporators constituted one of the wall of these liquid chambers, part of the flow was sucked within the liquid line by capillary forces when vaporisation was established in the wick. Then, the vapor returned to the reservoir by a bypass line finally leading to a parallel hybrid loop. Actually, a successful operation was shown for heat load up to 1.2 kW and 102 W cm -2 with a total differential pressure close to 60 kPa. However, liquid flooding of the evaporators was observed at low and moderate heat loads leading to a significant decrease of the thermal performance. An active control scheme adjusting the flow rate in the main liquid branch was then developed by Bejarano and Park [START_REF] Bejarano | Active flow control for cold-start performance enhancement of a pump-assisted, capillary-driven, two-phase cooling loop[END_REF]. A more stable operation was actually reached but some temperature fluctuations due to some partially flooded evaporator regimes were not totally avoided. Using a close configuration of a parallel hybrid loop, Jiang et al. [START_REF] Jiang | Experimental investigation of pump-assisted capillary phase change loop[END_REF] provided some results indicating the effect of liquid charging [START_REF] Jiang | Effect of liquid charging process on the operational characteristics of pump-assisted capillary phase change loop[END_REF] and conducting a deep investigation of loop startup [START_REF] Jiang | Startup characteristics of pump-assisted capillary phase change loop[END_REF].

Another hybrid approach was proposed by Setyawan et al. [START_REF] Setyawan | Experimental investigation of the operating characteristics of a hybrid loop heat pipe using pump assistance[END_REF] in order to prevent the LHP evaporator dry-out which may occur during the startup process at high heat load. A small diaphragm pump was placed on a bypass of the liquid line directly entering within the evaporator core. The vapor outlet temperature monitoring was used to control the power supply to the pump. In this configuration, the pressure drop was not supported by the mechanical pump and thus, the maximum pumping pressure was still imposed by the porous wick. However, the modified LHP could handle startup at 200 W while the dryout limit was reached for a start-up at 140 W without the pump. This investigation demonstrated that the pump assistance of a LHP gave the opportunity to adjust the subcooling required by the wick, and then, the hybrid loop approach is also promising for some heat transfer limitation such as transient wick dry-out during the startup process.

For all hybrid configurations previously described, the control of the phase distribution in the evaporator appeared to be a critical issue. Actually, the pump assistance significantly affected the adaptation of the flow rate to the heat load of the capillary-driven evaporator so that partial liquid flooding in the wick deteriorated the evaporator conductance. Consequently, new coupling approaches have to be examined.

In this study, a CPL previously developed for power electronics cooling is assisted with a centrifugal pump located upstream the evaporator. This is a series configuration of a hybrid loop close to Schweickart et al. [START_REF] Schweickart | Testing of a controller for a hybrid capillary pumped loop thermal control system[END_REF] device. One of the advantages is that the evaporator design and the CPL architecture were unchanged contrary to the parallel hybrid architecture. However, in the present work, the pump is used as a differential pressure source in the liquid line which is a different approach from [START_REF] Schweickart | Testing of a controller for a hybrid capillary pumped loop thermal control system[END_REF] where the volumetric pump directly affected the liquid flow rate and the phase distribution in the evaporator. A control scheme of the rotational speed of the pump is proposed. The response to power cycle and the startup dynamics are investigated with the objective to demonstrate that the hybrid CPL (HCPL) behaves as a simple CPL system with operating pressure drop in the line far beyond the capillary limit and with preserved evaporator thermal efficiency. The leading mechanisms ruling out the HCPL performances are also discussed.

Experimental set-up

HCPL set-up

The HCPL consists of a vertical flat evaporator, a thermally regulated reservoir located above the evaporator and a counterflow double pipe condenser (see figure 1). The evaporator casing has two active faces which are in contact with a rectangular sintered nickel porous wick with trapezoidal vapor grooves directly machined on the whole wick surface. The maximum evaporator pressure gain was determined at given heat load, by carefully closing the valve located on the vapor line until the evaporator deprime. A constant value of 9 -10kPa was found for the heat load operating range. It is close but lower than the Laplace-Young theoretical value (10.5 kPa) assuming spherical menisci with the wick mean pore diameter. This is consistent with the fact that the theoretical value gives the pressure drop accros the interface which thus includes additional pressure drop in the wick and the vapor grooves and collectors.

The condenser is a double coaxial glass tube heat exchanger connected to a thermostatted bath chiller using a transparent coolant allowing to visualize the flow patterns and dynamics. It is located about 18 cm below the evaporator i.e. in an unfavorable position as the capillary force must overcome a total gravitational pressure difference of about 4 kPa. The reservoir configuration is such that the liquid flow between the condenser and the evaporator is maintained in the lower portion by a perforated plate. Then, a heater provides the saturation temperature regulation via a PID controller. The lines are thermally insulated. Power is uniformly applied to both sides of the evaporator. The maximum power input is imposed by the condenser design. Its value is found to be 1.6 kW with a cold source at 25 • C. The main geometrical features are provided in table 1. A very close CPL configuration was previously investigated by [START_REF] Kaled | Experimental study of a Capillary Pumped Loop for cooling power electronics: Response to high amplitude heat load steps[END_REF] while similar evaporators were used in [START_REF] Ayel | Experimental Analysis of a Capillary Pumped Loop for Terrestrial Application[END_REF], [START_REF] Accorinti | Steady-state analysis of a Capillary Pumped Loop for Terrestrial Application with methanol and ethanol as working fluids[END_REF].

The centrifugal pump is placed between the reservoir and the evaporator (liquid line 2). It was especially built to be entirely hermetic. The impeller is located in a sealed casing including two fluid connectors. It is driven by magnetic force.The rotational speed ranges from 4, 000 rpm to 30, 000 rpm with a maximal speed increase of 2, 000 rpm per second. The relation between the pump pressure gain ∆p, mass flow rate ṁ and rotational speed w is:

∆p = a w 2 -b w ṁ (1)
where a and b are constants given in table 1. Hence, by controlling the rotational speed, a given pressure gain can be reached for a large mass flow rate range as shown in figure 2. The maximum pressure gain is 60 kPa. The pump power is proportional to the rotational speed power three. The operating power is [1.5 -13] W. The selection of the pump according to CPL specification was performed using numerical simulations of the HCPL response versus the operating conditions [START_REF] Leveque | A theoretical investigation of a controlled hybrid mechanical/capillary pumped loop[END_REF] based on the CPL modeling provides by [START_REF] Dutour | Analytical and numerical results for the dynamics of capillary pumped loops and loop heat pipes subjected to high amplitude heat load steps[END_REF]. A schematic view of the HCPL instrumentation is also shown in figure 1. The evaporator wall temperature measurements are performed using K-type thermocouples (diameter 0.5 mm) inserted into small grooves of 0.6 mm diameter made in the evaporator casing. Additional thermocouples are conventionally placed on the external surface of pipes along lines. After calibration, the thermocouples accuracy is ± 0.1 K. Pressure transducers are placed on the loop to measure with an accuracy of ±100 Pa the pressure difference between the fluid entrance and exit of the evaporator, the centrifugal pump and lines. The pres- Kp.ǫ(t) sure in the saturation part of the reservoir is monitored by an absolute 0 -2 bar (accuracy : ± 400 Pa) transducer connected to the upper part of the reservoir. Combined with a 2 mm diameter platinum probe placed in the vapor, the pressure measurements are also used for the in situ detection of non-condensable gases. The liquid mass flow rate at the inlet and at the outlet of the reservoir are determined with an accuracy less than ± 1 % using Coriolis flowmeters. Data acquisition is carried out at a frequency of 40 Hz except for the flow rate which is performed every second.

1 T i ǫ(t)dt + + ω(t) calculation ∆pev,set ω(t) = 0
In order to remove non-condensable gases, the liquid methanol was preliminarily boiled in a separated device and high vacuum was reached in the HCPL before filling.

Evaporator differential pressure control scheme

An active pump control scheme (see figure 3) is used in order to maintain the capillary driven pumping even when the total pressure drop in the loop, ∆p loop , exceeds the capillary limit. The monitoring of the pressure drop in the loop is performed by measuring the differential pressure at the evaporator ∆p EV and at the pump ∆p p as ∆p loop is also given by the sum of both driving pressures :

∆p loop = ∆p EV + ∆p p (2)
Then, comparing this pressure drop to a set point for the evaporator pressure ∆p EV,set , two regimes can be achieved :

• when ∆p loop ≥ ∆p EV,set , the mechanical pump is started and an automatic control regulates the rotational speed ω such as ∆p EV remains as close as possible to the set point : the HCPL reaches the pump-assisted capillary-driven (PACD) regime.

• when ∆p loop < ∆p EV,set , the mechanical pump is switched off and then acts as a passive component from hydraulic point of view: the HCPL operates in a simple capillarydriven (CD) regime.

A proportional-integral (PI) controller is used during the PACD regime. Values of both constants K P and T I were experimentally adjusted observing the system response. ∆p ev,set has to be set lower than 9 -10 kPa (the maximum evaporator pressure gain) in order to prevent the evaporator dry-out and greater than 2 kPa (liquid hydrostatic pressure within the evaporator) in order to prevent the liquid flooding. The value of 6 kPa was chosen for all experiments.

Experimental procedure

Some important CPL performance limitations due to the capillary limit are (i) a restricted heat transport capacity, (ii) loop deprime during large amplitude heat load steps [START_REF] Kaled | Experimental study of a Capillary Pumped Loop for cooling power electronics: Response to high amplitude heat load steps[END_REF] and (iii) loop deprime when the startup process is achieved at high power [START_REF] Dupont | Increasing the CPL power at startup by using a check valve[END_REF]. Consequently, this study investigated the HCPL response to these sollicitations and compared it to the response obtained with the same CPL system but without pump assistance.

A control valve located in the vapor line enabled to increase the pressure losses in the loop. As a consequence, the maximum heat load before the CPL deprime could be artificially adjusted before starting the power cycle. Two different loop pressure drop operating regimes were used: a low pressure drop (LPD) regime with a fully open control valve and a high pressure drop (HPD) regime with an almost close valve plug. With a larger heat load operating range, the LPD regime was suitable in order to investigate the loop thermal performance. The HPD regime was used in order to test the system with a maximum loop pressure drop such as during the first experiments which were performed with objective to demonstrate that the HCPL improved the transport capacity. The reservoir temperature and the coolant temperature were respectively maintained to 65 • C and 25 • C. Then, heat load steps were applied to the evaporator. A moderate step amplitude of 0.2 kW was chosen in order to limit the flow inertia.

The influence of the transient when the heat load step became larger and during high power startup, was respectively performed in a second and a third series of experiments. Actually, in these operating conditions, CPL faced severe fluid dynamics and pressure drop change due to the fluid redistribution which allowed to test the robustness of the control strategy.

Experimental results and analysis

Heat transport capacity increase and evaporator thermal performances

Figure 4 confirms that the operating range of the CPL is drastically limited in the HPD regime. The first heat load step leads to a steady-state at 400 W but the liquid subcooling at the evaporator inlet is significantly deteriorated by boiling or vapor percolation as shown by the evaporator inlet temperature increase and the inlet flow rate oscillations. The evaporator dry-out is then observable during the next heat load step from 400 W to 600 W: at t = 45 min, the evaporator differential pressure suddenly drops just after reaching the capillary limit. Simultaneously, the mass flow rate at the evaporator inlet stops until the vapor fully invades the evaporator inlet. Finally, the wall temperature drastically increases and the power has to be switched off.

Figure 5 shows the HCPL response to the same previous power cycle shown in figure 4. A large increase of the operating range is observable since the HCPL is still functioning at 1.6 kW. Moreover, the total HCPL differential pressure has reached up to 60 kPa which corresponds to more than 6 the capillary limit and more than 4 the CPL heat transport capacity.

A more detailed analysis shows that the HCPL automatically switches from the CD to the PACD regime during the heat load step from 200 W to 400 W and vice versa. This demonstrated that the mechanical pump is successfully started or stopped by the control scheme. During the PACD regime, the evaporator differential pressure appears to be almost insensitive to the loop pressure drop increase while the liquid mass flow rate at the evaporator inlet is adjusting to the vaporisation rate at steadystate. Actually, the capillary evaporator is still acting as it would in a simple CPL system except that the additional loop pressure drop are taken up by the mechanical pump. Moreover the stability of the evaporator pressure highlights the efficiency of the regulation system and the suitable response time of the pump. Furthermore, the fluid temperature at the evaporator inlet shows that the pump maintains the liquid subcooling: at 400 W, T ev,in is 52 • C while T ev,in is close to the vapor temperature T ev,out on figure 4. The pump is thus able to prevent penetration of the vapor phase within the porous wick and boiling during the step transient.

In addition, figure 6 shows that, at steady-state, there is an increase of the subcooling with the heat flux in both CPL and HCPL configurations. These results were obtained in the LPD regime in order to maximize the heat load operating range. However, the subcooling becomes significantly larger at high heat load in the HCPL configuration. This is mainly due to the pressure increase at the inlet of the evaporator leading to a greater saturation temperature T sat (P ev,in ) increase than the liquid temperature increase T ev,in due to thermal conduction. As a consequence, the HCPL also allows to move away from the boiling limit. No significant discontinuity in the evaporator wall temperature measurements is observable between both regimes so that the thermal performance of the capillary driven evaporator seems to be unaffected by the pump assistance. Figure 7 shows the evaporator global conductance versus the heat load for both CPL and HCPL systems in the LPD regime. This con- ductance is a characteristic of the heat transfer including conduction through the evaporator casing and vaporisation in the porous wick. The definition is :

G ev = Qv T ev,wall -T v ( 3
)
where T ev,wall is the (average) external wall temperature, T v is the temperature of the vaporisation interface and Qv is the heat conducted to the vaporisation interface which was determined knowing the heat applied to the evaporator and the heat losses with ambient. T v was obtained by the experimental determination of the pressure p v in the vapor grooves assuming that T v is the saturation temperature at p v . Figure 7 definitively demonstrates that the pump assistance is not leading to the evaporator flooding as there is no significant deviation between both conductance series in the LPD regime. We thus conclude that the HCPL system maintains the evaporator thermal performance corresponding to the vaporisation regime in the wick on the full operating range. Beyond the performance enhancement, these results also give the opportunity to question the understanding of the heat transfer in a capillary-driven evaporator. Indeed, the HCPL allows studying the evaporator conductance versus the heat load, the evaporator pressure drop and the vapor temperature. Figure 8 shows the evaporator pressure gain corresponding to the steadystates presented on Figure 7. For the CPL, the pressure difference normally increases with the heat load while, for HCPL, the evaporator pressure gain is controlled when the loop pressure drop becomes greater than the set point. For a given heat load, the vaporisation in both tests thus occurred at different pressure drop and finally, at different vapor temperature. Both figures 7 and 8 then suggest that, for this device and within the considered operating range, the conductance is not really influenced by the pressure drop but it is mainly affected by the heat load. Here, the conductance increases with the heat load. However, at larger heat loads, Accorinti et al. [START_REF] Accorinti | Steady-state analysis of a Capillary Pumped Loop for Terrestrial Application with methanol and ethanol as working fluids[END_REF] showed that the conductance reached a maximum and then decreased with the heat load. This is consistent with the experimental results obtained by Liao and Zhao [START_REF] Liao | A visual study of phase-change heat transfer in a twodimensional porous structure with a partial heating boundary[END_REF] with a wick heated by a finned surface and more recently by Odagiri and Nagano [START_REF] Odagiri | Characteristics of phase-change heat transfer in a capillary evaporator based on microscale infrared/visible observation[END_REF] with heated grooves directly machinated in the porous wick. The weakly dependance of the conductance with the evaporator pressure drop is confirmed on figure 9 showing the conductance versus the evaporator pressure difference. The experiments were performed at a fixed heat load and for a given pressure drop in the loop by changing the evaporator set point ∆p EV,set from 2.4 kPa to 8.5 kPa. A small conductance increase is perceptible, however, it is not really significant compared to the modification observed with the heat load.

The increase of the evaporator conductance with the heat load at low heat load is still open issue. As observed by [START_REF] Odagiri | Characteristics of phase-change heat transfer in a capillary evaporator based on microscale infrared/visible observation[END_REF], the vaporisation in the wick results of heat transfer at both the meniscus and the porous wick scales. At very low heat load, the liquid superheat in the wick remains limited and the wick is saturated with liquid. Vaporisation takes place at the wick/groove interface. Some additional menisci could also persist between the casing and the grooves. In the case of a liquid full wick, the variation of the evaporator conductance with the heat load is introduced by the variation of the menisci curvature with the heat load i.e. a more curved meniscus leads to a thinner meniscus extension in contact to the wick resulting in heat transfer enhancement. However, with an increase of the heat load, nucleate boiling occurs in the wick. A two-phase zone is then developing within the wick as observed by [START_REF] Liao | A visual study of phase-change heat transfer in a twodimensional porous structure with a partial heating boundary[END_REF] and [START_REF] Odagiri | Characteristics of phase-change heat transfer in a capillary evaporator based on microscale infrared/visible observation[END_REF]. In this case, the evaporator conductance increase with the heat load is given by the increase of triple line/micro-region at the wick/casing interface as shown by Mottet et al. [START_REF] Mottet | International Journal of Heat and Mass Transfer Three dimensional liquid and vapour distribution in the wick of capillary evaporators[END_REF] and Nishikawara et al. [START_REF] Nishikawara | Numerical study on heat-transfer characteristics of loop heat pipe evaporator using three-dimensional pore network model[END_REF] with 3D pore-network simulations. The vapor presence at this interface is then driven by (i) the pores invasion due to the evaporator pressure difference increase, (ii) the bubble nucleation because the liquid reaches its superheat limit. Then, at larger heat load, the fraction of liquid pores in contact with the casing drastically decreases and finally a vapor pocket appears leading to a significant conductance decrease. According to these results, the conductance results plotted in figure 9 shows that the menisci curvature radius has a very small influence on the heat transfer regime in our experiments. This also suggests that, in the operating conditions, vapor and liquid should coexist in the wick, while bubbles nucleation should be the dominant process of the two-phase zone extension at the wick/casing interface resulting in the conductance increase with the heat load.

Robustness of the control strategy during large amplitude heat load step

Here, the evaporator dry-out is observed for the simple CPL configuration in the LPD regime when a heat load step from 0.2 kW to 1.4 kW is applied. Figure 10 shows the HCPL response to a step from 0.2 kW to 1.6 kW and thus, demonstrates that the HCPL is able to deal with larger heat load steps than a simple CPL.

A more detailed analysis indicates that, before the step, the HCPL operates in a steady-state CD regime as the pressure drop in the loop was lower than the evaporator set point. Then, the large amount of vapor consecutive to the heat load increase leads to an important mass flow rate overshoot in the liquid line (m ll ). As a consequence, the pressure drop in the loop significantly increases and the evaporator differential pressure reaches the capillary limit. Simultaneously, the inlet evaporator flow rate drops and penetration of the vapor phase within the wick can be detected by the increasing of the evaporator inlet temperature. The centrifugal pump starts few seconds after the heat load change and attempts to regulate the evaporator pressure drop. In this way, it limits the vapor percolation and moreover, it increases the liquid subcooling required to condensate the vapor and to re-establish by imbibition the capillary-driven regimes. With the evaporator differential pressure decrease, the rotational speed decreases and finally, the HCPL operates in a steady PACD regime. Additional tests in the HPD regime and step amplitude up to 2 kW have confirmed the robustness of the HCPL system in handling severe heat load transients.

Increasing the heat load at startup with pump assistance

Figure 11 shows a startup failure when 1.1 kW was applied at the evaporator in the LPD regime. As the evaporator was full of liquid, a large superheat (regime I) is achieved before nucleation occurs at t = 2 min 30 s. Then, a large amount of vapor is suddenly produced (regime II). The pressure in the grooves largely increase and some liquid is pushed out of the evaporator by the vapor. Some vapor also percolates the wick and spreads at the inlet of the evaporator as shown by the temperature increase and a negative flow rate. This reverse flow simul-taneously produces a large pressure drop in the pump. Here, the vapor condensation within subcooled liquid is not sufficient to re-flood the evaporator and then, the liquid supplying of the wick is stopped since t = 2 min 48 s. Finally, the wick dry-out appears at t = 4 min as shown by the wall temperature increase and the power is shut-down. In usual conditions, the vapor at the inlet of the evaporator is condensed before the total dry-out so that the liquid supply is rapidly provided to the wick and then capillary pumping is established less than 1 min after the nucleate boiling onset. The HCPL startup tests were performed in the same conditions (control valve open). The control scheme was unchanged (cf. figure 3). The pump assisted system systematically succeeded. Figure 12 shows a startup performed at high heat load i.e. 1.6 kW. The pump automatically starts just few seconds after the onset of boiling since the evaporator differential pressure exceeds the set point (6 kPa). The rotational speed of the pump ω then increases attempting to regulate the evaporator pressure drop. During this stage, the mechanical pump significantly injects some subcooled liquid from the reservoir to such an extend that at t = 2 min 30 s the liquid flooding of the evaporator occurs during almost 10 s. This is suggested by the severe decrease of the evaporator differential pressure which becomes lower than the hydrostatic value (regime I). However, the rotational speed simultaneously decreased and finally the vaporisation with capillary driven pumping and thus the PACD regime is achieved at t = 2 min 42 s as shown by the sudden stabilization of the liquid mass flow rate at the inlet of the evaporator. From now, the pump assistance adjusts the loop pressure drop due to the establishment of the vapor front in the condenser.

It is thus its ability to increase the liquid subcooling at the evaporator inlet when vapor transiently penetrate within the wick that explains that the pump assistance reduced the CPL startup failure at high heat loads. However, as the process variable in the control scheme is not the subcooling but the evaporator differential pressure, the HCPL could be inefficient. Actually, if HCPL is started in the HPD regime, the system startup fails as shown in Figure 13. In this test, the amount of vapor which percolates the wick is significantly larger than in the previous test as shown by a larger amplitude of the evaporator inlet reverse flow. The pump starts to regulate the evaporator differential pressure as expected but, it is not able to supply enough subcooled liquid to the evaporator before the dry-out and the power has then to be stopped at t = 2 min 36 s. Although the HCPL failed in the latest case, an optimisation of the control scheme should provide the way to enhance the operating range of the HCPL during the startup at very high heat load.

Conclusion

An original hybrid loop consisting of a CPL in series with a centrifugal pump located at the evaporator inlet has been investigated. This system has shown many intrinsic advantages, since under most conditions, the operating range of a simple CPL can be significantly extended.

In particular, the experiments have demonstrated that the total loop pressure drop reached up to 60 kPa during the PACD regime, corresponding to more than 6 times the evaporator capillary limit with methanol. We have simultaneously shown that the hybrid system still behaves as a simple CPL in the sense that pumping pressure and vaporisation are maintained at the evaporator so that the evaporator thermal efficiency and the internal adaptive mechanism to the heat load are fully preserved by the HCPL system. This stable behavior is quite new compared to previous hybrid devices.

Moreover, the HCPL robustness during high amplitude heat load steps and startup process have been demonstrated. By increasing the liquid pressure at the evaporator inlet, the pump assistance limits the amount of vapor which percolates the wick and increases the liquid subcooling required at the evaporator inlet to re-establish the capillary-driven regime. Although the evaporator dry-out has been reached at high heat flux and large pressure drop, the HCPL significantly increases the operating heat load range compared to the CPL configuration. An optimisation of the controller should provide the way to extend the operating range of the HCPL during the startup at very high power.

Finally, as the HCPL limit relies on the mechanical pump features, these results could mean that higher performance may be reached by using a powerful pump. Moreover, the HCPL should give the opportunity to develop capillary driven evaporators using working fluids with lower values of global warming potential even if their surface tension is weak.

Figure 1 :

 1 Figure 1: Schematic of the HCPL with instrumentation. CFM: Coriolis Flow Meter.

Figure 2 :

 2 Figure 2: The pump pressure gain with methanol vs the mass flow rate and rotational speed. Points correspond to experimental results and lines to the relation (1) outcome.

Figure 3 :

 3 Figure 3: Simplified block diagram of the HCPL control scheme.

Figure 4 :

 4 Figure 4: Example of evaporator dry-out and CPL deprime consecutive to the heat load increase in the HPD regime: evaporator differential pressure a), mass flow rates b) and temperature variation c) versus time.

Figure 5 :

 5 Figure 5: HCPL response to moderate heat load steps in the HPD regime: pressure differences and pump rotational speed a), mass flow rate at the evaporator inlet b) and temperature variation c).

Figure 6 :Figure 7 :

 67 Figure 6: Liquid subcooling at the evaporator inlet versus the heat load for CPL and HCPL systems in the LPD regime.

Figure 8 :

 8 Figure 8: Evaporator differential pressure versus the heat load for CPL and HCPL systems in the LPD regime.

Figure 9 :

 9 Figure 9: Evaporator conductance versus the evaporator differential pressure at fixed heat loads.

Figure 10 :

 10 Figure 10: HCPL time response to high amplitude heat load step in the LPD regime: pressure differences and pump rotational speed a), mass flow rate at the evaporator inlet b) and temperature variation c).

Figure 11 :

 11 Figure 11: Example of evaporator dry-out and CPL deprime consecutive to the startup process: evaporator differential pressure a), mass flow rates b) and temperature variation c) versus time.

Figure 12 :

 12 Figure 12: HCPL time response to high amplitude heat load startup: pressure differences and pump rotational speed a), mass flow rate at the evaporator inlet b) and temperature variation c).

Figure 13 :

 13 Figure 13: Example of HCPL failure consecutive to high amplitude heat load startup when large pressure drop was imposed to the loop (the vapor line valve plug was almost close): pressure differences and pump rotational speed a), mass flow rate at the evaporator inlet b) and temperature variation c).

Table 1 :

 1 Pa (tr/min) -2 b : 90 Pa kg -1 s (tr/min) -1 HCPL main features.

	Components	Dimensions
	Evaporator	320 × 81 × 20 mm
		wall thickness : 1 mm
	Wick	283 × 68 × 16 mm
		mean pore diameter : 6.8 µm
		permeability : 6.53 10 -13 m 2
		porosity : 73%
	Vapor line	i.d. : 12 mm
		length : 3.3 m
	Condenser	i.d. : 12 mm
		length : 7.2 m
	Liquid line 1	i.d. : 6 mm
	(reservoir inlet)	length : 1.5 m
	Reservoir	volume : 2 10 -3 m 3
	Liquid line 2	i.d. : 10 mm
	(evaporator inlet)	length : 1 m
	Pump	volume : 18 × 9 × 4 cm
		mass : 650 g
		a : 7.3 10 -5

Acknowledgment

Financial support from the IRT Saint-Exupéry is gratefully acknowledged.


Vincent Cheval

Steve Kremer

Itsaka Rakotonirina

The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols

Keywords: Formal verification, Cryptographic protocols, Complexity

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

The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols

Vincent Cheval, Steve Kremer, Itsaka Rakotonirina

To cite this version:

Vincent Cheval, Steve Kremer, Itsaka Rakotonirina. The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. Nigam, V., Ban Kirigin, T., Talcott, C., Guttman, J., Kuznetsov, S., Thau Loo, B., Okada, M. Logic, Language, and Security -Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, LNCS-12300, Springer, 2020, Lecture Notes in Computer Science, 10.1007/978-3-030-62077-6_10. hal-02961617

Introduction

Symbolic verification techniques for security protocols can be traced back to the seminal work of Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF]. Today, after more than 30 years of active research in this field, efficient and mature tools exist, e.g. PROVERIF [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF] and TAMARIN [START_REF] Schmidt | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] to only name the most prominent ones. These tools are able to automatically verify full fledged models of widely deployed protocols and standards, such as TLS [START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF][START_REF] Cremers | A comprehensive symbolic analysis of TLS 1.3[END_REF], Signal [START_REF] Kobeissi | Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach[END_REF][START_REF] Cohn-Gordon | On ends-to-ends encryption: Asynchronous group messaging with strong security guarantees[END_REF], the upcoming 5G standard [START_REF] Basin | A formal analysis of 5g authentication[END_REF], or deployed multi-factor authentication protocols [START_REF] Jacomme | An extensive formal analysis of multi-factor authentication protocols[END_REF]. We argue that the development of such efficient tools has been possible due to a large amount of more theoretical work that focuses on understanding the precise limits of decidability and the computational complexity of particular protocol classes [START_REF] Dolev | On the security of ping-pong protocols[END_REF][START_REF] Durgin | Undecidability of bounded security protocols[END_REF][START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is NP-complete[END_REF][START_REF] Durgin | Multiset rewriting and the complexity of bounded security protocols[END_REF][START_REF] Comon | Tree automata with one memory set constraints and cryptographic protocols[END_REF][START_REF] Kanovich | Bounded memory protocols[END_REF]. The abovementioned results extensively cover verification for the class of reachability properties. Such properties are indeed sufficient to verify authentication properties and various flavors of confidentiality, even in complex scenarios with different kinds of compromise [START_REF] Basin | Know your enemy: Compromising adversaries in protocol analysis[END_REF]. Another class of properties are indistinguishability properties. These properties express that an adversary cannot distinguish two situations and are conveniently modelled as observational equivalences in a cryptographic process calculus, such as the applied pi calculus. Such equivalences can indeed be used to model strong flavors of secrecy, in terms of non-interference or as a "real-or-random" experiment.

Equivalences are also the tool of choice to model many other privacy-preserving properties. Such properties include anonymity [START_REF] Abadi | Private authentication[END_REF], unlinkability properties [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF][START_REF] Filimonov | Breaking unlinkability of the ICAO 9303 standard for e-passports using bisimilarity[END_REF], as well as vote privacy [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF] to give a few examples. Equivalence properties are inherently more complex than reachability properties, and both the theoretical understanding and tool support are more recent and more brittle. This state of affairs triggered a large amount of recent works to increase our theoretical understanding and improve tool support.

In this paper we give an extensive overview of decidability and complexity results for several process equivalences. In particular, in this survey we give a unified view, allowing us to highlight subtle differences in the definitions of the decision problems across the literature (such as whether the term theory is part of the input or not) as well as the protocol models. Typically, models may vary in whether they allow for a bounded or unbounded number of sessions, the support of cryptographic primitives, whether they support else branches (i.e. disequality tests, rather than only equality tests), and various restrictions on non-determinism. Additionally, our technical report [START_REF] Cheval | The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols[END_REF] contains full proofs of all results that are novel or that required additional arguments to make up for the differences in stating the problem compared to the original work. All the results are summarised in Table 1, and we identify several open questions. Delaune and Hirschi [START_REF] Delaune | A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols[END_REF] also survey symbolic methods for verifying equivalence properties. However, they mainly discuss tool support whereas we focus on computational complexity.

Model

We will model protocols as processes in the applied pi calculus, and cryptographic primitives are modelled using terms equipped with rewrite rules. We assume the reader is familiar with these notions and only recall them briefly and informally. A fully-detailed model can be found in the technical report [START_REF] Cheval | The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols[END_REF].

Cryptographic primitives. As usual in symbolic protocol analysis we take an abstract view of cryptography and model the messages exchanged during the protocol as terms built over a set of function symbols each with a given arity. Terms are then either atomic values or function symbols applied to other terms, respecting the function's arity. Atomic values are either constants, i.e., function symbols of arity 0 or names. Constants, sometimes referred to as public names, model public values, such as agent identities or protocol tags. Names model secret values, such as keys or nonces, and are a priori unknown to the adversary. We assume an infinite set of constants and names. Example 1. For example the encryption of a plaintext m with a key k using a symmetric encryption scheme senc is modelled by the term senc(m, k).

The functional properties of the symbols are modelled by an equational theory. In this work we restrict ourselves to equational theories that can be oriented into a convergent rewriting system. This also implies that any term t has a unique normal from t↓.

Example 2. The rewrite rule sdec(senc(x, y), y) → x defines the behaviour of the encryption scheme: one can decrypt (apply sdec) a ciphertext senc(x, y) with the corresponding key y to recover the plaintext x. This behaviour is idealised by the absence of other rules for senc and sdec, modelling an assumption that no information can be extracted from a ciphertext except by possessing the decryption key. Similarly, asymmetric encryption can be modelled by the rewrite rule adec(aenc(x, pk(y)), y) → x where pk is a symbol of arity 1 modelling public keys. Such rewrite rules can express a broad range of other primitives like pairs (fst( x, y ) → x and snd( x, y ) → y), hash functions (no rewrite rule) or randomised encryption (adding an additional argument to senc to explicitly represent the randomness).

In this survey we call a theory the set of non-constant function symbols together with a rewriting system. Two classes of theories are particularly important for our results. The first is the class of subterm convergent theories [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF][START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF][START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF][START_REF] Ciobâcȃ | Computing knowledge in security protocols under convergent equational theories[END_REF][START_REF] Conchinha | Fast: an efficient decision procedure for deduction and static equivalence[END_REF], defined by a syntactic criterion on rewriting rules → r requiring that r is either a strict subterm of or a ground term in normal form. The second is the class of constructor-destructor theories [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF][START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF][START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF], partitioning function symbols into constructor (used to build terms) and destructors (only used in rewrite rules). In constructor-destructor theories any rewrite rule → r is such that = d(t 1 , . . . , t n ) where d is a destructor and t 1 , . . . , t n , r do not contain any destructor. Moreover, we assume a message predicate msg(t) which holds if u↓ does not contain any destructor symbol for all subterms u of t, i.e., all destructor applications in t succeeded yielding a valid message. This predicate is used to restrict to protocols that only send and accept such well-formed messages.

Protocols. Protocols are defined using processes in the applied pi calculus. The syntax of protocols is defined by the grammar of processes:

P, Q ::= 0 if u = v then P else Q c(x).P c u .P P | Q
Intuitively the 0 models a terminated process, a conditional if u = v then P else Q executes either P or Q depending on whether the terms u↓ and v↓ are equal, and P | Q models two processes executed concurrently. The constructs c(x).P and c u .P model, respectively, inputs and outputs on a communication channel c. When the channel c is known to the attacker, e.g. when it is a constant, executing an output on c adds it to the adversary's knowledge and inputs on c are fetched from the adversary possibly forwarding a previously stored message, or computing a new message from previous outputs. Otherwise the communication is performed silently without adversarial interferences.

To model an unbounded number of protocol sessions we also add the two constructs P, Q ::= new k.P !P

The replication !P models an unbounded number of parallel copies of P , and new k.P creates a fresh name k unknown to the attacker; in particular !new k.P models an unbounded number of sessions, each with a different fresh key. The fragment of the calculus without replication is referred to as finite or bounded. Another notable subclass is the original pi-calculus [START_REF] Milner | A calculus of mobile processes[END_REF], referred to as the pure fragment, that can be retrieved with the empty theory (only names, constants and an empty rewrite system).

Semantics in an adversarial environment. The behaviour of processes is formalised by an operational semantics. The detailed presentation differs from one work to another [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF][START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF] and we only give a high-level overview here. It takes the form of a transition relation (P, Φ) α -→ (P , Φ ) on configurations (P, Φ) where P is the process to be executed, and Φ is called a frame and records the attacker knowledge. A frame is a substitution of the form {ax 1 → t 1 , . . . , ax n → t n } where t i are previous outputs and ax i are special variables called axioms that serve as handles to the adversary for building new terms. The label α of the transition step is called an action and is either an unobservable action τ which represents an internal action, such as the evaluation of a conditional or a communication on a private channel; an input action ξ c (ξ t ) where ξ c (resp. ξ t ) represents the attacker's computation of the input's public channel (resp. of the term to be input), see recipes in the next section; an output action ξ c ax i where ξ c is again the attacker's computation of the channel, and the underlying output term is added to the frame as axiom ax i . We refer to the technical report [START_REF] Cheval | The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols[END_REF] for full details of the semantics but provide additional intuition through the following example. Suppose that an agent S wants to send a nonce N to a recipient R. Assuming S and R already share a secret k s , S encrypts N and k s with the public key of R, i.e. pk(k R ) where k R is the corresponding private key. When receiving a message, R acknowledges the nonce only if the plaintext contains the shared secret. This is modelled by the following process:

P = S | R with S = c M where M = aenc( N, k s , pk(k R )) and R = c(x). if snd(adec(x, k R )) = k s then c ack else 0 with k s , k R , N ∈ N and c ∈ Σ 0 .
The 0 processes are omitted. The fact that the public key should be known to the attacker is modelled by a frame Φ 0 = {ax 0 → pk(k R )}. A "normal" execution of the protocol would be, with informal notations:

(S | R, Φ 0 ) c ax1 ----→ (0 | R, Φ 1 ) with Φ 1 = Φ 0 ∪ {ax 1 → M } (1) c(ax1) ----→ (0 | if snd(adec(M, k R )) = k s then c ack else 0, Φ 1 ) (2) τ -→ (0 | c ack , Φ 1 ) (3) c ax2 ----→ (0 | 0, Φ 1 ∪ {ax 2 → ack}) (4)
Here the attacker is passive and only forwards messages. More precisely in transition (1), S sends M which is added to the frame as reference ax 1 . This models that the attacker spies on the communication network and gets access to all messages sent on public channels like c. In transition (2) the attacker forwards M to R, i.e. inputs ax 1 . Transition ( 3) is an internal test of R which leads to the final acknowledgement output (4). An active attacker would also have the capability of forging new messages and inserting them in the execution flow. For example transition (2) can be replaced by the input c(aenc( a,b ,ax0))

-----------→ with a, b ∈ Σ 0 : rather than forwarding M the attacker encrypts the pair of constants a, b with the public key of R (using reference ax 0 ) and sends it to R. In this modified execution the subsequent test would however fail. Finally let us mention that for constructor-destructor theories, all attacker-crafted terms must be valid messages, i.e. satisfy the predicate msg [START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF][START_REF] Chrétien | From security protocols to pushdown automata[END_REF].

When defining security against an active attacker we quantify over all such transitions which means we consider all possible executions in an active adversarial environment. Thus even the bounded fragment yields an infinite transition system if the theory contains a non-constant function symbol (as this allows to build an unbounded number of messages).

3 Complexity of static equivalence (passive attacker)

Static equivalence

Attacker knowledge. As explained above, frames Φ = {ax 1 → t 1 , . . . , ax n → t n } record the outputs t i performed during the execution of a process. They therefore enable adversarial deductions as they aggregate: for example after observing a ciphertext and the decryption key, the attacker can also obtain the plaintext by decrypting. Formally we say that one can deduce all terms of the form ξΦ↓ where ξ is called a recipe that is a term built from function symbols, axioms ax i ∈ dom(Φ), and constants. Recipes were mentioned in the previous section, in the operational semantics, as the way to specify attacker's computations. The fact that recipes cannot contain names models that names are assumed unknown to the adversary initially. For example in Φ = {ax 1 → senc(t, k), ax 2 → k} the term t is deducible by the recipe sdec(ax 1 , ax 2 ), regardless of k being a name (which is not allowed to occur directly in the recipe).

Indistinguishability. Some security properties against a passive attacker, i.e. a simple eavesdropper, can then be modelled as an observational equivalence of two frames: intuitively no equality test can be used to distinguish them. For example, in a protocol that outputs a sequence of messages t 1 , . . . , t n , the "real-or-random" confidentiality of a key k can be modelled as the equivalence of

Φ = {ax 1 → t 1 , . . . , ax n → t n , ax → k} Ψ = {ax 1 → t 1 , . . . , ax n → t n , ax → k }
where k is a fresh key. More formally, two frames Φ, Ψ with same domain are statically equivalent when for all recipes ξ 1 , ξ 2 we have that

ξ 1 Φ↓= ξ 2 Φ↓ ⇐⇒ ξ 1 Ψ↓= ξ 2 Ψ↓ .
In constructor-destructor theories we also require that msg(ξ 1 Φ) iff msg(ξ 1 Ψ ), modelling an assumption that the adversary can observe destructor failures.

Example 3. If k, k are names, Φ = {ax → k} and Ψ = {ax → k } are equivalent, capturing the intuition that random keys cannot be distinguished. However, for the constant 0, Φ = {ax 1 → senc(0, k), ax 2 → k} and Ψ = {ax 1 → senc(0, k), ax 2 → k } are not equivalent since ξ 1 = sdec(ax 1 , ax 2 ) and ξ 2 = 0 are equal in Φ but not in Ψ .

Complexity results

We study the following decision problem referred to as STATEQ:

INPUT: A theory, two frames of same domain.

QUESTION: Are the two frames statically equivalent for this theory? General case. As rewriting is Turing-complete, unsurprisingly static equivalence is undecidable in general for convergent rewriting systems [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF]. It is also proved in [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF] that the DEDUCIBILITY problem (given a term t and a frame Φ, is t deducible in Φ?) reduces to STATEQ. As a consequence, the results of [START_REF] Anantharaman | Intruders with caps[END_REF] imply that static equivalence is also undecidable for so-called optimally-reducing rewrite systems, a subclass of rewrite systems that have the finite-variant property [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF].

Subterm convergent theories. Historically, complexity results for static equivalence only considered fixed theories [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF][START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF], that is, the theory was not part of the input of the problem and its size was seen as a constant in the complexity analysis. This was consistent with most formalisms and verification tools at the time, which would not allow for user-defined theories and only consider a fixed set of cryptographic primitives, such as in the spi-calculus for example [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus. Information and computation[END_REF]. In particular fixed theories are considered in the following result:

Theorem 1 ([2]
). For all fixed subterm convergent theories STATEQ is PTIME.

Generic PTIME-completeness results would make no sense when the theory is not part of the input, since the complexity may depend of it. Typically when using an empty theory the complexity changes: Theorem 2 ( [START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF]). In the pure pi-calculus, STATEQ is LOGSPACE.

However, in some sense, the PTIME bound is optimal since it is possible to provide a hardness result for a large class of fixed subterm convergent theories: Theorem 3. For all fixed theories containing symmetric encryption, STATEQ is PTIMEhard.

Proof (Sketch). We proceed by reduction from HORNSAT. Let X the set of variables of a Horn formula ϕ = C 1 ∧ . . . ∧ C n , and k x names for all x ∈ X ∪ {⊥}. Then to each clause C = x 1 , . . . , x n ⇒ x, x ∈ X ∪ {⊥} we associate the term

t C = senc(. . . senc(senc(k x , k x1 ), k x2 ), . . . , k xn ) .
Putting k x under several layers of encryption ensures that k x is deducible if all the keys k x1 , . . . , k xn are deducible as well. In particular k ⊥ is deducible from the terms t C1 , . . . , t Cn iff the formula ϕ is unsatisfiable. Hence given two constants 0,1, and

Φ = {ax 1 → t C1 , . . . , ax n → t Cn }, we have that the frames Φ ∪ {ax → senc(0, k ⊥ )} and Φ ∪ {ax → senc(1, k ⊥ )} are statically equivalent iff ϕ is satisfiable.
However tools have improved since then and automated provers like KISS [START_REF] Ciobâcȃ | Computing knowledge in security protocols under convergent equational theories[END_REF], YAPA [START_REF] Baudet | YAPA: A generic tool for computing intruder knowledge[END_REF] or FAST [START_REF] Conchinha | Fast: an efficient decision procedure for deduction and static equivalence[END_REF] are able to handle user-defined theories. It is therefore interesting today to refer to complexity analyses that account for the size of the rewrite system: Theorem 4 ( [START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF]). STATEQ is coNP-complete for subterm convergent theories.

Beyond subterm convergence. Although we are not aware of complexity results for the decision of static equivalence for classes larger than subterm theories, there exist decidability results. Some of the abovementioned tools, like KISS and YAPA, can actually handle most convergent rewriting system; but they naturally fail to terminate in general by undecidability of the problem. However it is proved in [START_REF] Ciobâcȃ | Computing knowledge in security protocols under convergent equational theories[END_REF] that the termination of KISS is guaranteed for theories modelling blind signatures or trapdoor commitment (that are typically not subterm).

4 Complexity of dynamic equivalences (active attacker)

Equivalences

We expect security protocols to provide privacy against attackers that actively engage with the protocol. This can be modelled by behavioural equivalences, defining security as the indistinguishability of two instances of the protocol that differ on a privacysensitive attribute. There exist several candidate equivalences for modelling this notion of indistinguishability. We study two of them here and refer to [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF] for details.

Trace equivalence. The first one is trace equivalence. Referring to the operational semantics described in Section 2, we call a trace t a sequence of transition steps

t = (A 0 α1 -→ A 1 α2 -→ • • • αn --→ A n )
If tr is the word obtained after removing unobservable actions (i.e. τ 's) from the word α 1 • • • α n , the trace t may be written A 0 tr = ⇒ A n instead. Processes P 0 and P 1 are then trace equivalent when for all traces P i tr = ⇒ (P, Φ), i ∈ {0, 1}, there exists P 1-i tr = ⇒ (P , Φ ) such that the frames Φ and Φ are statically equivalent. Automated verification of trace equivalence has been studied intensively for security protocols [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF][START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF][START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF] and received strong tool support [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Cheval | Apte: an algorithm for proving trace equivalence[END_REF][START_REF] Cheval | The deepsec prover[END_REF][START_REF] Cortier | Efficiently deciding equivalence for standard primitives and phases[END_REF][START_REF] Cortier | A type system for privacy properties[END_REF]. We refer to this problem as TRACEEQ:

INPUT: A theory, two processes. QUESTION: Are the two processes trace equivalent? Labelled bisimilarity. Some other tools prove stronger equivalences, like observational equivalence for PROVERIF [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF][START_REF] Cheval | Proving more observational equivalences with proverif[END_REF] for example. There exist several flavours of more operational bisimulation-based properties but the one usually considered in securityprotocol analysis is labelled bisimilarity because it coincides with observational equivalence in the applied pi-calculus [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF]. Formally it is an early, weak bisimulation that additionally requires static equivalence at each step; that is, it is the largest symmetric binary relation ≈ on processes such that A ≈ B implies that (1) the frames of A and B are statically equivalent, and (2) for all actions α and all transitions A α -→ A , there exists a trace B α = ⇒ B such that A ≈ B . We refer to the following problem as BISIM:

INPUT: A theory, two processes. QUESTION: Are the two processes labelled bisimilar?

Classical fragments of the calculus

In addition to the assumptions on the rewriting system (e.g. subterm convergence as in Section 3), there are several common restrictions made on the processes.

Conditionals and patterns.

A typical restriction on conditionals is the class of positive processes that only contains trivial else branches [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF][START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF]. In particular for succintness we often write [u = v]P instead of if u = v then P else 0.

When the rewrite system is constructor-destructor, some conditionals may also be encoded within inputs [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF][START_REF] Chrétien | From security protocols to pushdown automata[END_REF]. For that the syntax for inputs is generalised as c(v).P where v is a term without destructors (but may contain variables), called a pattern. In terms of semantics, such inputs only accept terms that match the pattern, i.e. inputs t such that t ↓= uσ ↓ for some substitution σ, and then proceeds to execute P σ. In this paper, to ensure that protocols can be effectively implemented we require that it is possible to test with a sequence of positive conditionals that a term t matches the pattern u, and that all variables of u can be extracted by applying destructors to u. We thus define the patterned fragment to be the class of processes without conditionals but using pattern inputs, and where outputs do not contain destructor symbols; it is a subset of the positive fragment.

Ping pong protocols. These protocols [START_REF] Chrétien | From security protocols to pushdown automata[END_REF][START_REF] Dolev | On the security of public key protocols[END_REF][START_REF] Hüttel | Recursive ping-pong protocols[END_REF] intuitively consist of an unbounded number of parallel processes receiving one message and sending a reply. Although the precise formalisms may differ from one work to another, the mechanisms at stake are essentially captured by processes P = !P 1 | • • • |!P n where

P i = c i (x). [u i 1 = v i 1 ] • • • [u i ni = v i ni ]new k 1 • • • new k ri . c i w i
In particular ping-pong protocols are positive.

Simple processes. A common middleground in terms of expressivity and decidability is the class of simple processes, for example studied in [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF]. Intuitively, they consist of a sequence of parallel processes that operate each on a distinct, public channelincluding replicated processes that generate dynamically a fresh channel for each copy. Formally they are of the form

P 1 | • • • | P m | ! ch P m+1 | • • • | ! ch P n
where ! ch P = ! new c P . c P c P . P

where each P i does not contain any parallel operator (|) nor replication (!) and uses a unique, distinct communication channel c Pi . Unlike ping pong protocols, each parallel process may input several messages and output messages that depend on several previous inputs. There exists a generalisation of simple processes called determinate processes, mentioned later in Section 5.

Complexity results: bounded fragment

The bounded fragment is a common restriction to study decidability, as removing replication bounds the length of traces. However, as the attacker still has an unbounded number of possibilities for generating inputs, the transition system still has infinite branching in general. Additional restrictions are also necessary on the cryptographic primitives (as static equivalence is undecidable in general). For subterm convergent, constructor-destructor theories for example:

Theorem 5 ( [START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF]). TRACEEQ and BISIM are decidable in coNEXP for subterm convergent constructor-destructor theories and bounded processes.

We do not detail the decision procedures as they are quite involved. In a nutshell, they use a dedicated constraint-solving procedure to show that, whenever trace equivalence is violated, there exists an attack trace whose attacker-input terms are at most of exponential size; in particular this shows non-equivalence to be decidable in NEXP. As before, we may also study the problem for fixed theories to investigate their influence on the complexity; typically with the empty theory: Theorem 6 ( [START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF]). In the pure pi-calculus, TRACEEQ (resp. BISIM) is Π 2 -complete (resp. PSPACE-complete) for bounded processes, and for bounded positive processes.

However, unlike static equivalence, fixing the theory does not make it possible to obtain a bound that is better than the general one:

Theorem 7 ([22]

). There is a subterm-convergent constructor-destructor theory s.t. TRACEEQ and BISIM are coNEXP-hard for bounded positive processes.

The theory in question [START_REF] Cheval | DEEPSEC: Deciding equivalence properties in security protocols theory and practice[END_REF] encodes binary trees and a couple of ad hoc functionalities. We show in the technical report [START_REF] Cheval | The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols[END_REF] that, provided we discard the positivity requirement, the proof is possible with symmetric encryption and pairs only. This shows that the problem remains theoretically hard even with a minimal theory.

Complexity results: unbounded case

Equivalence is undecidable in general since the calculus is Turing-complete even for simple theories. For example, Hüttel [START_REF] Hüttel | Deciding framed bisimilarity[END_REF] shows that Minsky's two counter machines can be simulated within the spi-calculus (and hence the applied pi-calculus with symmetric encryption only). It is not difficult to adapt the proof to a simulation using only a free symbol, i.e., a function symbol h of positive arity and an empty rewrite system. These two encodings can be performed within the finite-control fragment, typically not Turing-complete in the pure pi-calculus (i.e. without this free function symbol) [START_REF] Dam | On the decidability of process equivalences for the π-calculus[END_REF].

Ping pong protocols. While equivalence is undecidable for ping-pong protocols [START_REF] Chrétien | From security protocols to pushdown automata[END_REF][START_REF] Hüttel | Recursive ping-pong protocols[END_REF] some decidability results exist under additional assumptions. For example [START_REF] Hüttel | Recursive ping-pong protocols[END_REF] studies a problem that can be described in our model essentially as BISIM for ping-pong protocols with 2 participants or less (i.e. n ≤ 2 in the definition). This is proved decidable under some model-specific assumptions which we do not detail here. We also mention a result for patterned ping-pong protocols (cf. Section 4.2) without a limit on the number of participants [START_REF] Chrétien | From security protocols to pushdown automata[END_REF]. Given a constructor-destructor theory, a ping-pong protocol P is said to be deterministic when each P i (using the same notations as in the definition) can be written under the form

P i = c i (u i ). new k 1 • • • new k ri .c i v i
where u 1 , . . . , u n is a family of patterns verifying:

(1) binding uniqueness: for all i, u i does not contain two different variables;

(2) pattern determinism: for all i = j, if u i and u j are unifiable then c i = c j . There is an additional, minor restriction on the structure of u i and v i that is omitted here, and we refer to [START_REF] Chrétien | From security protocols to pushdown automata[END_REF] for details.

Theorem 8 ([27]

). For a theory limited to randomised symmetric and asymmetric encryption and digital signature, TRACEEQ is decidable in primitive recursive time for deterministic ping-pong protocols.

Decidability is obtained by a reduction of the problem to the language equivalence of deterministic pushdown automata, which is decidable in primitive recursive time. A complexity lower bound for this problem is open (beyond the PTIME-hardness inherited from static equivalence, recall Theorem 3).

Simple processes. We now study a decidability result for patterned simple processes [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF]. In this work the theory is limited to symmetric encryption and pairs, and the processes must be type compliant and acyclic. Formalising the last two assumptions is quite technical and beyond the scope of this survey. We refer to the technical report [START_REF] Cheval | The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols[END_REF] for more intuition and details. Compared to our other models, there is also a restriction to atomic keys, i.e. for all encryptions senc(u, v) in the process, v is either a constant, name or variable. This restriction is also enforced to attacker's recipes in the semantics by strenghtening the msg predicate.

Theorem 9 ([26]

). For a theory limited to pairs and symmetric encryption, TRACEEQ is coNEXP for patterned, simple, type-compliant, acyclic processes with atomic keys.

The proof shows that equivalence of such (unbounded) processes is violated iff it is violated for a exponential number of sessions, and then uses a coNP decidability result in the bounded fragment [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF]. However complexity was not the focus of [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF] and the authors only claimed a triple exponential complexity for their procedure. Besides no lower bounds were investigated, but we proved that the problem was coNEXP-complete.

Theorem 10. For a theory limited to pairs and symmetric encryption, TRACEEQ is coNEXP-hard for patterned, simple, type-compliant, acyclic processes with atomic keys.

The reduction shares some similarities with the proof of coNEXP-hardness for trace equivalence of bounded processes (Theorem 7), compensating the more deterministic structure of simple processes by the use of replication.

Proof (Sketch). We proceed by reduction from SUCCINT 3SAT. This is a common NEXP-complete problem that, intuitively, is the equivalent of 3SAT for formulas of exponential size represented succinctly by boolean circuits. Formally a formula ϕ with 2 m clauses and 2 n variables x 0 , . . . , x 2 n -1 is encoded by a boolean circuit Γ :

{0, 1} m+2 → {0, 1} n+1 in the following way. If ϕ = 2 m -1 i=0
1 i ∨ 2 i ∨ 3
i and 0 ≤ i ≤ 2 m -1 and 0 ≤ j ≤ 2, we let x k be the variable of the literal j+1 i and b its negation bit; then Γ ( ī j) = b k where ī, j, k are the respective binary representations of i, j, k. SUCCINT 3SAT is the problem of deciding, given a circuit Γ , whether the formula ϕ it encodes is satisfiable.

Let then ϕ be a formula with 2 m clauses and 2 n variables x 0 , . . . , x 2 n -1 and Γ a boolean circuit encoding this formula. We construct two simple, type-compliant, acyclic processes that are trace equivalent iff ϕ is unsatisfiable. Using pairs u, v we encode binary trees: a leaf is a non-pair value and, if u and v encode binary trees, u, v encodes the tree whose root has u and v as children. Given a term t, we build a process P (t) behaving as follows:

(1) P (t) first waits for an input x from the attacker. This term x is expected to be a binary tree of depth n with boolean leaves, modelling a valuation of ϕ (the i th leaf of x being the valuation of x i ).

(2) The goal is to make P (t) verify that this valuation satisfies ϕ; if the verification succeeds the process outputs t. Given two constants 0 and 1, P (0) and P (1) will thus be trace equivalent iff ϕ is unsatisfiable. (3) However it is not possible to hardcode within a process of polynomial size the verification that the valuation encoded by x satisfies the 2 m clauses of ϕ. Hence we replicate a process that, given x, verifies one clause at a time. Intuitively, the attacker will guide the verification of the 2 m clauses of ϕ, and whenever the i th clause has been successfully verified, the process reveals the binary representation of i (encrypted using a key unknown to the attacker). ( 4) In particular, the attacker gets the encryption of all integers 0, . . . , 2 m -1 only if she has successfully verified that the initial input x indeed encodes a valuation satisfying all clauses of ϕ. It then suffices to design a process that outputs t if the attacker is able to provide all such ciphertexts. This can be encoded by a replicated process that, upon receiving the encryption of two integers that differ only by their least significant bit, reveals the encryption of these integers with the least significant bit truncated. The verification ends when the encryption of the empty binary representation is revealed.

Variations of the model

In this section we discuss a few variants of the model such as other notions of equivalence or different semantics of the process calculus.

Diff equivalence. The most well-known variant of equivalence properties in security protocols is diff-equivalence, different variants of which are proved by the state-of-theart PROVERIF and TAMARIN. Intuitively, diff-equivalence can be seen as an analogue of trace equivalence where two equivalent traces are also required to follow the exact same execution flow. Consider for example the processes

P = c u | c v and Q = c u | c v .
Given the trace of P outputting u first and then v, a proof of trace equivalence could match it with either of the two traces of Q. However diff-equivalence only considers the trace of Q outputting u first and then v .

Theorem 11 ([16]). If two processes are diff-equivalent then they are also labelled bisimilar (and therefore trace equivalent).

The converse does not hold in general, which may lead to so-called false attacks (non-diff-equivalent processes that are, for example, trace equivalent). Regarding decidability and complexity, we call the following problem DIFFEQ: INPUT: A theory, two processes. QUESTION: Are the two processes diff equivalent? Although undecidable in general, it is known to be decidable in the bounded, positive fragment [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF]. More precisely it is shown that for all fixed subterm convergent theories, diff-equivalence is reducible to a coNP constraint-solving problem.

Theorem 12 ([12]). For all fixed subterm convergent theories, DIFFEQ is coNP for positive bounded processes.

It is also known that DIFFEQ is coNP-hard for a theory containing only a free binary symbol h [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF]. A simple proof justifies that DIFFEQ is actually coNP-hard even for the empty theory and, hence, for any fixed theory: Theorem 13. In the pure pi-calculus, DIFFEQ is coNP-complete for positive bounded processes.

Proof. By reduction from SAT we consider a formula ϕ = m i=1 C i in CNF and x = x 1 , . . . , x n its variables. For each clause C i , let k i be a name and define

CheckSat i (x) = [x i1 = b i1 ]c k i | • • • | [x ip = b ip ]c k i
where x i1 , . . . , x ip are the variables of C i and b i1 , . . . , b ip their respective negation bit. That is, at least one output of k i is reachable in CheckSat i (x) if x is a valuation of ϕ that satisfies C i . In particular if we define

CheckSat = c(x 1 ). . . . c(x n ).(CheckSat 1 (x) | • • • | CheckSat m (x)) Final (t) = c(y 1 ).[y 1 = k 1 ] . . . c(y m ).[y m = k m ] c t
then for two distinct constants ok, ko, we have the processes CheckSat | Final (ok) and CheckSat | Final (ko) diff-equivalent iff ϕ is unsatisfiable.

As far as we know the complexity of diff-equivalence has only been studied for fixed theories. However the coNP-completeness [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF] can be adapted to parametric theories; inspecting the proof we observe that (1) in the complexity bounds, the dependencies in the theory are polynomial and (2) the proof uses the fact that static equivalence is PTIME for fixed theories (Theorem 1) but the arguments still hold if we only assume static equivalence to be coNP. Theorem 14. DIFFEQ is coNP-complete for subterm convergent theories and positive bounded processes.

Equivalence by session. We also briefly mention another equivalence, between diffequivalence and trace equivalence (but incomparable with labelled bisimilarity) [START_REF] Cheval | Exploiting symmetries when proving equivalence properties for security protocols[END_REF]. Known as equivalence by session, it was originally presented as a sound proof technique for trace equivalence in the bounded fragment, that was inducing less false attacks than diff-equivalence. We call this problem SESSEQ:

INPUT: A theory, two processes. QUESTION: Are the two processes equivalent by session? Surprisingly, despite practical improvements by order of magnitudes of the verification time compared to trace equivalence [START_REF] Cheval | Exploiting symmetries when proving equivalence properties for security protocols[END_REF], this performance gap is not reflected in the theoretical, worst-case complexity. The same reduction as trace equivalence can indeed be used to prove equivalence by session coNEXP-hard. More details about the complexity of this problem can be found in the technical report [START_REF] Cheval | The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols[END_REF].

Theorem 15. SESSEQ is coNEXP-complete for constructor-destructor subterm convergent theories and positive bounded (resp. bounded) processes.

The case of determinacy. We now mention the fragment of determinate processes, a generalisation of simple processes. In this fragment of the calculus, most of the studied equivalences coincide and their complexity also drops exponentially. This class has been investigated significantly [START_REF] Baelde | Partial order reduction for security protocols[END_REF][START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][START_REF] Cheval | Exploiting symmetries when proving equivalence properties for security protocols[END_REF] although several variants coexist in the literature, as discussed in [START_REF] Babel | On the semantics of communications when verifying equivalence properties[END_REF]. For example the results of [START_REF] Baelde | Partial order reduction for security protocols[END_REF][START_REF] Cheval | Exploiting symmetries when proving equivalence properties for security protocols[END_REF] hold for action-determinate processes, meaning that the processes never reach an intermediary state where two inputs (resp. outputs) on the same communication channel are executable in parallel; whereas a more permissive definition is used in [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF]. There also exists a notion that is stricter than all of these, referred as strong determinacy [START_REF] Babel | On the semantics of communications when verifying equivalence properties[END_REF]. A process is strongly determinate when (1) it does not contain private channels, (2) it is bounded, (3) all its syntactic subprocesses are strongly determinate, (4) in case the process is of the form P | Q there exist no channels c such that both P and Q contain an input (resp. an output) on c. For example this process is action-determinate but not strongly-determinate:

if a = b then c(x) else 0 | if a = b then 0 else c(x) .
Note in particular that bounded simple processes are strongly determinate.

Theorem 16 ([21,24]). Two labelled bisimilar (resp. equivalent by session) processes are trace equivalent. The converse is true for action-determinate processes.

In [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF] it is shown that, for bounded, simple, positive processes, the equivalence problem could be reduced to the same coNP constraint-solving problem mentioned in the paragraph on diff-equivalence. Their arguments can be generalised from simple to strongly-determinate processes in a straightforward manner; however it is not clear whether this would also be true for action-determinate processes or processes with else branches. In particular we obtain for this fragment: Theorem 17 ([21]). TRACEEQ, BISIM and SESSEQ are coNP-complete for subterm convergent theories and bounded, strongly determinate, positive processes. The coNP completeness also holds for all fixed subterm convergent theories.

Variations of the communication model. Although all symbolic models rely on the same fundamental ideas, several variations exist in the semantics of communication, as noted in [START_REF] Babel | On the semantics of communications when verifying equivalence properties[END_REF]. The differences lie in the modelling of silent communications between parallel processes. In the original semantics [START_REF] Abadi | The applied pi calculus: Mobile values, new names, and secure communication[END_REF], called classical in [START_REF] Babel | On the semantics of communications when verifying equivalence properties[END_REF], communications on a same public channel between parallel processes can either be an internal, synchronous, and silent action, or be intercepted by the attacker. This is also the semantics used in the popular PROVERIF tool [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]. On the contrary, the so-called private semantics only allows private, unintercepted communications on channels that are unknown to the attacker, modelling an attacker that continuously eavesdrops on the network (rather than an attacker that has the capability of eavesdropping any communication). The private semantics is actually used in tools such as TAMARIN [START_REF] Schmidt | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] and AKISS [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF] and also in the presentation of equivalence by session [START_REF] Cheval | Exploiting symmetries when proving equivalence properties for security protocols[END_REF]. While both semantics are equivalent when it comes to reachability properties, they surprisingly happen to be incomparable for equivalence properties [START_REF] Babel | On the semantics of communications when verifying equivalence properties[END_REF]. All the complexity results of this paper are with respect to the private semantics. Although we did not expand on studying all the variations of complexity induced by using different semantics, most of the analyses presented in this survey are robust to these changes. Indeed, all complexity results for the bounded fragment hold for both semantics. In the unbounded case, only the private semantics has been considered in the underlying models [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF][START_REF] Chrétien | From security protocols to pushdown automata[END_REF].

Summary of the results

Table 1 summarises the results of and highlights open questions (including a few results only detailed in the technical report [START_REF] Cheval | The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols[END_REF] for space reasons). Cells for which the complexity results are not tight are colored in grey. For instance, for subterm-convergent constructor-destructor theories and bounded processes, DIFFEQ is known coNEXP and coNP-hard, but the precise complexity remains unknown. We also include in this table some complexity results with the theory seen as a constant of the problem (denoted as "fixed" in the theory columns). The corresponding cells contain bounds applying to all theories of the class; e.g. for BISIM of bounded processes, with fixed subtermconvergent constructor-destructor theories, the problem is decidable in coNEXP and PSPACE-hard; despite the gap between the two bounds, they are optimal since there exist theories for which the problem is either coNEXP-hard or PSPACE. Therefore this cell is not highlighted in grey. In our opinion the most interesting open questions are:

Can upper bounds on constructor-destructor subterm convergent theories be lifted to more general subterm convergent theories? Without the positivity assumption, can we tighten the complexity for diff equivalence, and strongly determinate processes? This last question might allow to better understand why strongly determinate processes benefit from optimisations that improve verification performance that much. Finally, as witnessed by the contrast between the high complexity of equivalence by session and its practical efficiency, worst-case complexity may not always be an adequate measure.

Table 1 .

 1 Summary of the results. Colored cells indicate configurations with open problems.All results for diff-equivalence also coincide with the results for trace equivalence, labelled bisimilarity, and equivalence by session for strongly-determinate processes.

	STATEQ	DIFFEQ	BISIM	SESSEQ	TRACEEQ
	theory process

The research leading to these result has received funding from the ERC under the EU's H2020 research and innovation program (grant agreements No 645865-SPOOC), as well as from the French ANR project TECAP (ANR-17-CE39-0004-01). Itsaka Rakotonirina benefits from a Google PhD Fellowship.


Antoine Lejay

A COURSE ON ROUGH PATHS -WITH AN INTRODUCTION TO REGULARITY STRUCTURES (PETER K. FRIZ AND MARTIN HAIRER)

This review concerns the book A course on rough paths -With an introduction to regularity structures by P.K. Friz and M Hairer which contains an introduction to both the theory of rough paths and the theory of regularity structures and develop their

In a broad sense, the rough paths theory can be seen as a natural extension of the theory of ordinary differential equations which plays well in a stochastic context. Regularity structures -for which M. Hairer was awarded a Field medal in 2014extend the notion of Stochastic Partial Differential Equations (SPDE) in a way well suited to deal with singularities. The book [START_REF] Friz | A Course on Rough Paths: With an Introduction to Regularity Structures[END_REF] under review is an introduction to both theories which are part of approaches sometimes called "pathwise stochastic calculus".

In relation with arbitrage-free theory, Itô's stochastic calculus is among the core tools that quantitative analysts and academics should master. Therefore, why consider other theories of integration? Actually, there is a full room for pathwise stochastic calculus in mathematical finance as it allows to ' deal with stochastic differential equations driven by a fractional Brownian motion or other Gaussian processes, ' set up "cubature formula" or other numerical Monte Carlo methods for efficient option pricing, ' develop innovative, state-of-art machine learning techniques, ' integrate anticipating stochastic processes, ' solve rough volatility models, ' model the evolution of interest rate with singular SPDE, ' perform stochastic control, ' etc

In addition, rough paths theory reveals insights on some aspects of classical stochastic calculus and allows one to set up other kind of stochastic calculus. Developed initially by T. Lyons at the end of the '90 [START_REF] Lyons | Differential equations driven by rough signals[END_REF][START_REF] Lyons | System control and rough paths[END_REF], the rough paths theory is connected to many topics ranging from algebra to machine learning. It combines both theoretical and practical results. This explains its richness and why it is now expanding in many directions. This book is divided in 15 chapters. Chapters 2-6 cover the basics of the rough paths theory in relation with stochastic calculus, although the former may be developed without any reference to the later. This presentation is however helpful to understand how to define pathwise integrals of type Y t " ş t 0 f pB s qdB s and differential equations of type X t " a `şt 0 f pX s qdB s against α-Hölder continuous paths B like Brownian paths where α ă 1{2. To do so, the core idea is to extend the path B to a so-called "rough path" B that lives in a larger, non-commutative space. A rough path is defined by both algebraic and analytic properties. This non-unique extension specifies a choice of the Lévy area, the area between the path and its chord. This is exactly the information needed to define integrals in pathwise manners. As a bonus, B Þ Ñ Y and B Þ Ñ X are continuous in the suitable spaces. These continuity properties explain the practical importance of the rough paths theory and why it naturally extends of smooth calculus. These chapters allow one to better understand the features of these non-linear and non-trivial extensions. For Brownian rough paths, connections with Itô, Stratonovich and anticipating calculus are also presented. A deterministic version of the Doob-Meyer decomposition is also given. It encompasses the role of the roughness properties of the paths.

Chapters 7-8 contain the statement regarding existence, uniqueness/non-uniqueness and continuity of solutions to Rough Differential Equations. Chapter 9 considers Stochastic Differential Equations driven by Brownian motions, the relation with Wong-Zakai results and how the continuity properties yield short proofs to support and large deviations theorems. Chapters 10-11 deal with differential equations driven by Gaussian rough paths and their features such as Malliavin calculus and concentration of measure properties. Chapter 12 contains some applications of the rough paths theory to first and second-order SPDE. It serves also as a transition toward the theory of regularity structure.

Chapters 13-15 are devoted to the theory of regularity structures. Existence and uniqueness results are given after a thorough presentation of the algebraic foundations. Here, the main idea is to extend distributions through some Taylor development in a way allowing multiplication and integration them against singular kernels. The central piece is the reconstruction theorem that defines the solution from these suitable approximations defined in abstract spaces. Chapter 15 illustrates how the theory of regularity structures gives a rigorous meaning to the KPZ equation, a very singular and ill-posed semilinear stochastic PDE. Such a breakthrough result solved a long-standing open problem.

Written by two leading researchers, this book offers an excellent introduction to both rough paths and regularity structures, with an up-to-date presentation of these two major theories. Effectively written, packed with exercises and applications -several of them are related to the aforementioned topics regarding mathematical finance -, it is well fitted for a newcomer in the field and provides a secure base from where to explore alternative formulations of theses theories or other specific developments such as in machine learning (not covered by this book) or in other fields.

Date: October 8, 2020. Université de Lorraine, CNRS, Inria, IECL, F-54000 Nancy, France, antoine.lejay@univ-lorraine.fr. 1


Pedro Javier Ortiz Suárez

Benoît Sagot

Laurent Romary Asynchronous

A concrete example for a start BERT

OSCAR

Language and standards -why?

• A general issue of reproducibility

• Can we compare two linguistic descriptions • E.g. two etymological assumptions in a dictionary entry • An acuter context created by the machine learning revival

• Comparing results of AI components

• Issues related to segmentation, categorisation (noun, verbs, feminine, dual, etc.), dependencies towards other linguistic descriptions (lexica, lower linguistic levels)

• Reproducibility of results

Standards

• What they are

• Reference background for the management of a technical process • The three pillars of a standard: consensus, publicity, maintenance • A constraint for each, a benefit for all!

• Reading it, understanding it, implementing it…

• What they aren't

• Something coming from nowhere… participating is always an option • Mandatory documents: rather a common ground for a transaction • Regulations: unless a state or an international organisation takes it up

• The need for standards developing organizations (SDO)

• Ensure that the three pillars of standardisation are in place

• Standards are like the EU: you need to understand how they work to appreciate them…

Standards and AI

• A new committee has been set up • Numerous ongoing activities:

• Concepts and terminology, Framework for Artificial Intelligence (AI) Systems Using Machine Learning (ML), Risk Management, Assessment of the robustness of neural networks, Overview of ethical and societal concerns, Governance implications of the use of artificial intelligence by organizations

• Overview:

• Very high level endeavour • Requires domain-specific standardisation activities => language

Language and standards -where?

• Various levels of specialisation • ISO TC 37: Language and terminology (language codes, language resources, translation and interpretation)

• TEI -Text Encoding Initiative

• Consortium dedicated to textual content

• Drama, Transcription of spoken language, dictionaries, manuscripts, etc.

• Based on XML -defines a vocabulary of around 600 elements

Language and standards -what and how?

• All levels of linguistic documentation, description, representation

  (and ISO 15924, ISO 3166-1, UN M.49…)

Dealing with variety: lexical resources

• A variety of contexts and forms • Basic digital literacy

• Even for very simple issues related to online presence (authorship, affiliation)

• Concrete knowledge of existing standards for language resources

• Preventing the development of (any) new formats, unless strongly supported by evidence

• Active contributions