Giuseppe Morello
email: gmorello@iac.es

Camilla Danielski

Subhajit Sarkar

The Ariel 0.6 -7.8 µm stellar limb-darkening coefficients

Keywords: planets and satellites: atmospheres, stars: planetary systems, instrumentation: photometers, instrumentation: spectrographs, telescopes

We provide here tables of stellar limb-darkening coefficients (LDCs) for the Ariel ESA M4 space mission. These tables include LDCs corresponding to different wavelength bins and white bands for the NIRSpec, AIRS-Ch0 and AIRS-Ch1 spectrographs, and those corresponding to the VISPhot, FGS1 and FGS2 photometers. The LDCs are calculated with the open-source software ExoTETHyS for three complete grids of stellar atmosphere models obtained with the ATLAS9 and PHOENIX codes. The three model grids are complementary, as the PHOENIX code adopts more modern input physics and spherical geometry, while the models calculated with ATLAS9 cover wider ranges of stellar parameters. The LDCs obtained from corresponding models in the ATLAS9 and PHOENIX grids are compared in the main text. All together the models cover the following ranges in effective temperature (1 500 K ≤ T eff ≤ 50 000 K), surface gravity (0.0 dex ≤ log g ≤ 6.0 dex), and metallicity (-5.0 ≤ [M/H] ≤ 1.0).

Introduction

Observations of exoplanetary transits are affected by the specific intensity decrease from the centre to the edge of the projected stellar disc, so-called limb-darkening effect [START_REF] Mandel | Analytic Light Curves for Planetary Transit Searches[END_REF]. While the planet's projection moves onto the stellar disc, the fraction of occulted stellar flux varies over time, instead of being equal to the planet-to-star area ratio. Furthermore, the limb-darkening is a wavelength-dependent effect, meaning that it is crucial to account for it when modelling transit light-curves at multiple frequencies [START_REF] Charbonneau | Using Stellar Limb-Darkening to Refine the Properties of HD 209458b[END_REF][START_REF] Morello | High-precision Stellar Limb-darkening in Exoplanetary Transits[END_REF][START_REF] Morello | A SEA BASS on the Exoplanet HD 209458b[END_REF][START_REF] Danielski | The homogeneous characterisation of Ariel host stars[END_REF]. A precise determination of the limb-darkening will consequently enable a precise characterisation of an exoplanet's atmosphere.

One of the Ariel mission requirements is to meet a photometric precision of 10-50 parts per million (ppm) relative to the stellar flux of the observed targets [46,[START_REF] Edwards | An Updated Study of Potential Targets for Ariel[END_REF]. Here we provide grids of limb-darkening coefficients (LDCs) for the Ariel instruments, adopting the four-coefficient law introduced by Claret (2000) [START_REF] Claret | A new non-linear limb-darkening law for LTE stellar atmosphere models[END_REF], hereinafter referred to as "claret-4". In particular, we used the software ExoTETHyS [START_REF] Morello | The ExoTETHyS Package: Tools for Exoplanetary Transits around Host Stars[END_REF][START_REF] Morello | ExoTETHyS: Tools for Exoplanetary Transits around host stars[END_REF] to compute LDCs with the there-called ATLAS 2000 [START_REF] Claret | A new non-linear limb-darkening law for LTE stellar atmosphere models[END_REF], PHOENIX 2012 13 and PHOENIX DRIFT 2012 [START_REF] Claret | New limb-darkening coefficients for PHOENIX/1D model atmospheres. I. Calculations for 1500 K ≤ T e f f ≤ 4800 K Kepler, CoRot, Spitzer, uvby, UBVRIJHK, Sloan, and 2MASS photometric systems[END_REF][START_REF] Claret | New limb-darkening coefficients for Phoenix/1d model atmospheres. II. Calculations for 5000 K ≤ T e f f ≤ 10 000 K Kepler, CoRot, Spitzer, uvby, UBVRIJHK, Sloan, and 2MASS photometric systems[END_REF] model grids. The spectral responses of the Ariel instruments were obtained through ExoSim [START_REF] Sarkar | ExoSim: the Exoplanet Observation Simulator[END_REF]. We considered wavelength bins of 0.05 µm for the NIRSpec and AIRS-Ch1 spectrometers, and 0.02 µm for AIRS-Ch0. The tables attached to this manuscript contain the most up to date LDCs which can be used by the Ariel community during the preparatory studies. We note that, the underlying stellar and instrumental models are likely to be updated by the launch of the Ariel spacecraft. Finally, whether a specific set of LDCs is not available here (e.g., adopting different limb-darkening laws, wavelength bins, or to interpolate between the stellar parameters of the grid), it can be computed with the python package ExoTETHyS1 .

The manuscript is structured as follows. Section 2 introduces the stellar limbdarkening effect, and discusses its historical overview, putting particular emphasis on its application to the study of exoplanetary transits. Section 3 briefly describes the ExoTETHyS limb-darkening subpackage used to calculate the LDCs for the Ariel mission. Section 4 provides information about the Ariel science instruments. Section 5 summarises this paper's content.

2 The stellar limb-darkening effect

Limb-darkening laws

The phenomenon of limb-darkening is easily understood starting from the formal solution of the radiative transfer equation along a ray, which shows that the emerging intensity is a weighted average of the source function over optical depth. Historically, the approximation that was usually adopted is the Eddington-Barbier one, which describes the source function of the continuum radiation as a polynomial of optical depth in a medium with plane-parallel geometry. In this case, the intensity emerging at an angle θ with respect to the surface normal is equal to the source function at optical depth µ = cos θ. The first parametrization proposed to model stellar limbdarkening is the linear law [START_REF] Schwarzschild | [END_REF]:

I λ (µ) I λ (1) = 1 -a(1 -µ), (1)
as derived from the first-order Eddington-Barbier approximation. It was later realised that the linear law does not fully capture the centre-to-limb intensity variation, thus a quadratic law was preferred [START_REF] Kopal | Detailed effects of limb darkening upon light and velocity curves of close binary systems[END_REF]:

I λ (µ) I λ (1) = 1 -a 1 (1 -µ) -a 2 (1 -µ) 2 . (2)
Later, many researchers have proposed a long list of other limb-darkening laws, which are not only polynomial functions of µ (see [START_REF] Kipping | Efficient, uninformative sampling of limb darkening coefficients for two-parameter laws[END_REF][START_REF] Espinoza | Limb darkening and exoplanets -II. Choosing the best law for optimal retrieval of transit parameters[END_REF] for reviews). We highlight here the power-2 law [START_REF] Hestroffer | Centre to limb darkening of stars. New model and application to stellar interferometry[END_REF]:

I λ (µ) I λ (1) = 1 -c(1 -µ α ), (3)
which outperforms other biparametric laws, especially for the M-dwarf models [START_REF] Morello | High-precision Stellar Limb-darkening in Exoplanetary Transits[END_REF][START_REF] Maxted | Comparison of the power-2 limb-darkening law from the STAGGER-grid to Kepler light curves of transiting exoplanets[END_REF]. The search for the simplest law that accurately describes the stellar intensity profile was motivated by both the aim of linking the LDCs to physical parameters, and the fact that fewer coefficients are more easily manageable as free parameters. However, no biparametric law turns out to be sufficiently accurate for all stellar types and wavelengths at the level of precision in the data achieved with modern instruments [START_REF] Espinoza | Limb darkening and exoplanets -II. Choosing the best law for optimal retrieval of transit parameters[END_REF][START_REF] Morello | High-precision Stellar Limb-darkening in Exoplanetary Transits[END_REF]. For this reason we strongly recommend the use of the claret-4 law [START_REF] Claret | A new non-linear limb-darkening law for LTE stellar atmosphere models[END_REF]:

I λ (µ) I λ (1) = 1 - 4 k=1 a k (1 -µ k/2 ), (4)
since it has proven highly reliable in all the investigations carried out so far [START_REF] Howarth | New limb-darkening coefficients and synthetic photometry for model-atmosphere grids at Galactic, LMC and SMC abundances[END_REF][START_REF] Magic | The Stagger-grid: A grid of 3D stellar atmosphere models. IV. Limb darkening coefficients[END_REF][START_REF] Claret | Gravity and limbdarkening coefficients for compact stars: DA, DB, and DBA eclipsing white dwarfs[END_REF][START_REF] Morello | The ExoTETHyS Package: Tools for Exoplanetary Transits around Host Stars[END_REF]. The above limb-darkening laws may not reproduce the behaviour of some spectral lines at high-resolution (R > 10 4 ), whereas more complex intensity profiles, including limb-brightening effects, can occur [START_REF] Czesla | The center-to-limb variation across the Fraunhofer lines of HD 189733. Sampling the stellar spectrum using a transiting planet[END_REF]. The discussion of these cases is not relevant to the Ariel instruments, which provide optical broadband photometry and infrared low-resolution spectroscopy with R ∼ 15-100.

Plane-parallel versus spherical geometry

The earliest models of stellar atmospheres assumed plane-parallel geometry (e.g., [START_REF] Kurucz | Model atmospheres for G, F, A, B, and O stars[END_REF][START_REF] Wade | Linear and quadratic limb-darkening coefficients for a large grid of LTE model atmospheres[END_REF][START_REF] Diaz-Cordoves | Linear and non-linear limb-darkening coefficients for LTE model atmospheres[END_REF][START_REF] Claret | Linear and non-linear limb-darkening coefficients for the photometric bands R I J H K[END_REF][START_REF] Claret | A new non-linear limb-darkening law for LTE stellar atmosphere models[END_REF][START_REF] Claret | A new non-linear limb-darkening law for LTE stellar atmosphere models III[END_REF][START_REF] Claret | Testing the limb-darkening coefficients measured from eclipsing binaries[END_REF][START_REF] Sing | Stellar limb-darkening coefficients for CoRot and Kepler[END_REF][START_REF] Howarth | New limb-darkening coefficients and synthetic photometry for model-atmosphere grids at Galactic, LMC and SMC abundances[END_REF][START_REF] Reeve | Limb-darkening coefficients from line-blanketed non-LTE hot-star model atmospheres[END_REF]). Recently, several models that take into account the spherical geometry of the stellar surface have appeared in the literature (e.g., [START_REF] Claret | Gravity and limb-darkening coefficients for the Kepler, CoRoT, Spitzer, uvby, UBVRIJHK, and Sloan photometric systems[END_REF][START_REF] Claret | New limb-darkening coefficients for PHOENIX/1D model atmospheres. I. Calculations for 1500 K ≤ T e f f ≤ 4800 K Kepler, CoRot, Spitzer, uvby, UBVRIJHK, Sloan, and 2MASS photometric systems[END_REF][START_REF] Claret | New limb-darkening coefficients for Phoenix/1d model atmospheres. II. Calculations for 5000 K ≤ T e f f ≤ 10 000 K Kepler, CoRot, Spitzer, uvby, UBVRIJHK, Sloan, and 2MASS photometric systems[END_REF][START_REF] Neilson | Spherically-symmetric model stellar atmospheres and limb darkening. I. Limb-darkening laws, gravity-darkening coefficients and angular diameter corrections for red giant stars[END_REF][START_REF] Neilson | Spherically symmetric model stellar atmospheres and limb darkening. II. Limb-darkening laws, gravity-darkening coefficients and angular diameter corrections for FGK dwarf stars[END_REF][START_REF] Claret | Theoretical gravity and limb-darkening coefficients for the MOST satellite photometric system[END_REF][START_REF] Magic | The Stagger-grid: A grid of 3D stellar atmosphere models. IV. Limb darkening coefficients[END_REF][START_REF] Claret | A new method to compute limb-darkening coefficients for stellar atmosphere models with spherical symmetry: the space missions TESS, Kepler, CoRoT, and MOST[END_REF][START_REF] Claret | Gravity and limbdarkening coefficients for compact stars: DA, DB, and DBA eclipsing white dwarfs[END_REF]). The intensity profiles obtained with spherical geometry show a characteristic steep drop-off, such that the intensities are almost zero at small but finite µ values (see Figure 1). We note that the intensity drop-off in the infrared is more abrupt than the one in the UV and visible. This behaviour is well understood [ [START_REF] Wittkowski | Tests of stellar model atmospheres by optical interferometry. VLTI/VINCI limb-darkening measurements of the M4 giant ψ Phe[END_REF][START_REF] Espinoza | Limb darkening and exoplanets: testing stellar model atmospheres and identifying biases in transit parameters[END_REF][START_REF] Morello | High-precision Stellar Limb-darkening in Exoplanetary Transits[END_REF]. The rays connecting the observer with the star surface at small µ values intersect only the outermost atmospheric shells, which have negligible emissivity compared to more internal shells. Instead, any optical ray intersects all the layers of a plane-parallel atmosphere, so that the emerging intensity always includes the contributions of inner layers down to optical depth of unity. Consequently, the intensity profile appears to be a smooth function of µ with a non-zero limit at µ = 0.

Limb-darkening laws such as those of Equations 1-4 were designed to approximate the stellar intensity profiles obtained with plane-parallel geometry, but they cannot reproduce the steep drop-off resulting from spherical geometry. Some authors have suggested applying a cut-off in µ, i.e. discarding the points with µ < µ 0 when fitting the intensity profile with a limb-darkening law [START_REF] Claret | The limb-darkening for spherically symmetric NextGen model atmospheres: A-G main-sequence and sub-giant stars[END_REF][START_REF] Claret | New limb-darkening coefficients for PHOENIX/1D model atmospheres. I. Calculations for 1500 K ≤ T e f f ≤ 4800 K Kepler, CoRot, Spitzer, uvby, UBVRIJHK, Sloan, and 2MASS photometric systems[END_REF][START_REF] Morello | The ExoTETHyS Package: Tools for Exoplanetary Transits around Host Stars[END_REF]. The truncated profiles are referred to as quasi-spherical models. Claret (2018) [START_REF] Claret | A new method to compute limb-darkening coefficients for stellar atmosphere models with spherical symmetry: the space missions TESS, Kepler, CoRoT, and MOST[END_REF] replaced the after drop-off intensities with zeroes, instead of discarding them. Also, the drop-off radius corresponds to what would appear as the stellar radius in observations of exoplanetary transits, interferometric imaging, or lunar occultation. Therefore, the spherical intensity profiles should be rescaled so that µ = 0 at the inflection point of the intensity profile [START_REF] Wittkowski | Tests of stellar model atmospheres by optical interferometry. VLTI/VINCI limb-darkening measurements of the M4 giant ψ Phe[END_REF][START_REF] Espinoza | Limb darkening and exoplanets: testing stellar model atmospheres and identifying biases in transit parameters[END_REF][START_REF] Morello | High-precision Stellar Limb-darkening in Exoplanetary Transits[END_REF].

Optimisation fitting methods

The optimisation method plays an important role when fitting for LDCs. The simplest approach is the standard least-squares fit to the precalculated intensities. The leastsquares method is sensitive to the choice of sampling of the intensity profile. The cause of sampling dependence is the impossibility to obtain a perfect match to the reference profile with the chosen parametrization, especially when using one or twocoefficient laws, and/or considering spherical geometry. A uniform sampling in µ gives more weight to the regions on the edge of the stellar disc. In fact, the radial distance of a µ-point from the center of the disc is

r = 1 -µ 2 , (5)
where r = 1 (µ = 0) denotes the contour of the disc. In the case of uniform sampling in µ, 50% of the weight is attributed to the annulus with r > 0.866. Typically the situation is even more unbalanced, given that the spherical models adopt a finer sampling near the intensity drop-off. In contrast, a uniform sampling in r tends to undersample the region where the effect of limb-darkening is more pronounced. The matter of optimal sampling to calculate the LDCs has been widely debated in the previous literature [START_REF] Heyrovský | Computing Limb-darkening Coefficients from Stellar Atmosphere Models[END_REF][START_REF] Claret | Testing the limb-darkening coefficients measured from eclipsing binaries[END_REF][START_REF] Claret | Gravity and limb-darkening coefficients for the Kepler, CoRoT, Spitzer, uvby, UBVRIJHK, and Sloan photometric systems[END_REF][START_REF] Parviainen | LDTK: Limb Darkening Toolkit[END_REF]. Flux-conservation has been considered as an additional condition or alternative to least-squares fitting [START_REF] Wade | Linear and quadratic limb-darkening coefficients for a large grid of LTE model atmospheres[END_REF][START_REF] Claret | A new non-linear limb-darkening law for LTE stellar atmosphere models[END_REF][START_REF] Howarth | On stellar limb darkening and exoplanetary transits[END_REF]. It requires that the integral of the flux over the disc obtained with the limb-darkening law is exactly equal to the stellar flux of the model, a requirement that is not automatically satisfied by the best-fit least-squares solution.

2.4 The Synthetic-Photometry/Atmosphere-Model LDCs Howarth (2011) [START_REF] Howarth | On stellar limb darkening and exoplanetary transits[END_REF] raised the question of which is the best set of LDCs to be adopted in the light-curve analyses of exoplanetary transits. He generated syntheticphotometry/atmosphere-model (SPAM) light-curves for well-studied systems, using as inputs the empirically determined geometric parameters, and the intensity distribution corresponding to the known stellar parameters (approximated by a set of claret-4 LDCs, Equation 4). Light-curve fitting was then performed with one or two LDCs as free parameters (e.g., Equations 1-2). The resulting SPAM-LDCs were significantly different from those obtained by fitting on the intensity profile with various optimisation methods.

The follow-up work by Morello et al. (2017) [START_REF] Morello | High-precision Stellar Limb-darkening in Exoplanetary Transits[END_REF] on this study used full spherical intensity models with numerical integration to generate synthetic light-curves, and different configurations for light-curve fitting. They noted that the intensity profiles inferred by light-curve fitting reproduce the behaviour of the models well inside the disc, but often deviate at the smaller µ values. The corresponding transit depths and orbital parameters can also be significantly biased. The apparent good quality of the light-curve fitting can be deceptive.

Part of the problem is due to the inadequacy of a given limb-darkening law to approximate the model intensity distribution on the whole stellar disc. Therefore, different optimisation methods, including SPAM optimisation, attribute different weights to the regions of the disc. The residuals of the light-curve fits do not necessarily provide a useful diagnostic, because the strong degeneracies between LDCs and geometric parameters can lead to an excellent match to the transit light-curves, even with the wrong parameter values.

All these historical issues have been addressed in the ExoTETHyS package [37] which we briefly describe in the upcoming section. Table 1 Information about the stellar model grids adopted in this work. P-P = plane-parallel, S1 = spherical 1D geometry.

The ExoTETHyS package

We state here the conditions that must be fulfilled by an optimal set of LDCs for a mission dedicated to the characterisation of transiting exoplanets:

1. if the optimal LDCs are kept fixed during light-curve fitting, the best-fit transit depth and orbital parameters should be unbiased; 2. the LDCs can be computed directly from stellar intensity profiles, e.g., without the need for lengthy calculations involving ad hoc synthetic light-curves.

The software ExoTETHyS.SAIL is a calculator of LDCs that has been designed to meet the above requirements [START_REF] Morello | ExoTETHyS: Tools for Exoplanetary Transits around host stars[END_REF]. It performs a weighted least-squares fit to the normalised stellar intensities (I λ (µ)/I λ (1)). The weigths are proportional to the sampling interval in r, with a cut-off of r ≤ 0.99623 for the intensity profiles obtained with spherical geometry, after rescaling (see Section 2.2). Flux-conservation poses no additional constraints when fitting normalised intensities, since the absolute flux can be matched by adjusting the multiplicative factor (approximately equal to I λ (1)). The absolute flux value does not affect the transit light-curve morphology and the relevant astrophysical parameters.

In particular, the LDCs calculated according to the claret-4 law (Equation 4) have been tested to guarantee a precision of <10 ppm over the whole light-curve model at all wavelengths [START_REF] Morello | The ExoTETHyS Package: Tools for Exoplanetary Transits around Host Stars[END_REF]. This level of precision is up to 2 orders of magnitude better than that obtained with other existing software that use different optimisation algorithms. It is worth noting that the improvement of ExoTETHyS.SAIL over other algorithms is particularly significant in the infrared, given its capability of better dealing with the more abrupt intensity drop-off (see Section 2.2).

Stellar atmosphere models

At the time of writing, the ExoTETHyS package contains 3 databases with pre-computed stellar model intensities that fully cover the wavelength range of the Ariel instruments (see Table 1).

The ATLAS 2000 database includes the largest variety of stellar types, covering wide ranges in effective temperature, surface gravity, and metallicity. The corresponding models of stellar atmospheres were calculated by [START_REF] Kurucz | ATLAS9 Stellar Atmosphere Programs and 2 km/s grid. ATLAS9 Stellar Atmosphere Programs and 2 km/s grid[END_REF][START_REF] Kurucz | Model Stellar Atmospheres and Real Stellar Atmospheres[END_REF] [START_REF] Kurucz | ATLAS9 Stellar Atmosphere Programs and 2 km/s grid. ATLAS9 Stellar Atmosphere Programs and 2 km/s grid[END_REF][START_REF] Kurucz | Model Stellar Atmospheres and Real Stellar Atmospheres[END_REF] using the ATLAS9 software. The intensity spectra produced with these models were previously used by Claret (2000) [START_REF] Claret | A new non-linear limb-darkening law for LTE stellar atmosphere models[END_REF]. We selected those models with microturbulent velocity of 2 km/s. Some other models with different values of the microturbulent velocity were available for stars with solar metallicity, but they were not included in the ExoTETHyS database as the variations of the LDCs with this parameter are negligible. 1.95-3.9 R ≥100 AIRS-Ch1 3.9-7.8 R ≥30

Table 2 Nominal wavelength ranges and required binned spectral resolving power for the 6 Ariel science instruments (Ariel Payload Requirements Document, ARIEL-RAL-PL-RS-001, Issue 3.0, 31 July 2020).

The PHOENIX 2012 13 database focuses on stars of later types, such as the typical exoplanet host stars, and with solar metallicity. The corresponding models of stellar atmospheres were generated with the PHOENIX code, assuming phase equilibrium (DUSTY/COND physics).

The PHOENIX DRIFT 2012 database is specific to the coolest stars down to 1 500 K. The corresponding models of stellar atmospheres were generated with the PHOENIX code, including a detailed computation of high-temperature condensate clouds (DRIFT physics) [START_REF] Witte | Dust in brown dwarfs and extra-solar planets. II. Cloud formation for cosmologically evolving abundances[END_REF].

The two PHOENIX databases were produced expressly for computing LDC tables [START_REF] Claret | New limb-darkening coefficients for PHOENIX/1D model atmospheres. I. Calculations for 1500 K ≤ T e f f ≤ 4800 K Kepler, CoRot, Spitzer, uvby, UBVRIJHK, Sloan, and 2MASS photometric systems[END_REF][START_REF] Claret | New limb-darkening coefficients for Phoenix/1d model atmospheres. II. Calculations for 5000 K ≤ T e f f ≤ 10 000 K Kepler, CoRot, Spitzer, uvby, UBVRIJHK, Sloan, and 2MASS photometric systems[END_REF].

For targets whose LDCs can be obtained from both ATLAS and PHOENIX tables, we recommend using the PHOENIX values, as they rely on newer input physics and chemistry, and more realistic geometry. For stars with T eff = 3 000 K , the DRIFT models are more accurate than DUSTY/COND. We refer to the relevant literature for the comparison between the ATLAS and PHOENIX algorithms [START_REF] Kurucz | Model atmospheres for G, F, A, B, and O stars[END_REF][START_REF] Allard | Model Atmospheres for M (Sub)Dwarf Stars. I. The Base Model Grid[END_REF][START_REF] Allard | The Limiting Effects of Dust in Brown Dwarf Model Atmospheres[END_REF][START_REF] Castelli | Is missing Fe I opacity in stellar atmospheres a significant problem?[END_REF][START_REF] Witte | Dust in brown dwarfs and extra-solar planets. II. Cloud formation for cosmologically evolving abundances[END_REF][START_REF] Husser | A new extensive library of PHOENIX stellar atmospheres and synthetic spectra[END_REF]. Section 4 adds the comparison between intensity profiles obtained in the Ariel passbands.

New grids of stellar atmosphere models with updated input physics and chemistry are being prepared and will be available for the upcoming phases of the Ariel mission. The new information will be incorporated into the ExoTETHyS package.

LDCs for the Ariel mission

The Ariel instruments include 3 broadband photometers at 0.5-1.1 µm, and 3 infrared spectrometers covering the 1.1-7.8 µm wavelength range. Table 2 reports basic information on these instruments. The known spectral response (Figure 2) of the Ariel instruments has been taken into account for the calculation of the LDCs. The response for each instrument was obtained by multiplying the detector quantum efficiency and the total transmission of the optical train, as obtained through ExoSim [START_REF] Sarkar | ExoSim: the Exoplanet Observation Simulator[END_REF].

We provide tables of LDCs for all the instruments of the Ariel mission. These tables have been pre-calculated for the users convenience and can be found in the supplementary material provided online. Table 3 shows an example with the content of a file (e.g., name of instrument, stellar model, wavelength range, etc.). We performed calculations on wavelength bins of 0.05 µm for the NIRSpec and AIRS-Ch1 spectrometers, and 0.02 µm for AIRS-Ch0. These wavelength bins are narrower than or equal to those corresponding to the required binned spectral resolving power of Fig. 2 The calculated photon-to-electron conversion efficiencies (PCEs) for the 6 Ariel science instruments.

PHOENIX 2012 13 AIRS ch0 the instruments (see Table 2). This information is subject to small changes during the detailed definition phase C. Figures 3 and4 compare the limb-darkening profiles calculated with the ATLAS 2000 and PHOENIX 2012 13 databases for a solar-like star and a M dwarf, respectively. The two sets of profiles for the solar-like star are in good agreement for the 6 Ariel instruments, although the discrepancy in the visible photometry might be significant at >10 ppm level. The M dwarf profiles show greater disagreement, most likely due to the enhanced effect of molecular absorption. The comparison between all the analogous models from the two grids is beyond the scope of this paper.

T eff (K) log g (dex) [M/H] (dex) λ1 (µm) λ2 (
• • • • • • • • • • • • • • • • • • • • • • • • • • 3000.0 1.
• • • • • • • • • • • • • • • • • • • • • • • • • •

Conclusions

We discussed here the stellar limb-darkening effect on the study of transiting exoplanets and their atmospheres. We documented an open-source software, part of the ExoTETHyS package, which has been specifically designed to achieve a precision of a few parts per million in modelling the transit light-curves. By using ExoTETHyS and the spectral responses of the Ariel instruments, obtained through ExoSim, we provide pre-calculated tables of limb-darkening coefficients over 0.6-7.8 µm. The software is also available to calculate limb-darkening coefficients with settings personalised by the user, e.g., different spectral bins. The current calculations rely on ATLAS9 and PHOENIX stellar intensity spectra, which cover an overall effective temperature range of 1500-50000 K, surface gravity range of 0.0-6.0 dex, and metallicity of -5.0-1.0 dex. New grids of stellar atmosphere models covering the Ariel wavelength range of 0.6-7.8 µm are being prepared for inclusion in ExoTETHyS.

Fig. 1

 1 Fig. 1 Left panel: Normalised intensities vs. µ for a solar-like star integrated over the AIRS-Ch1 white band. Note the intensity drop-off obtained with the "original" PHOENIX models (orange) due to the spherical geometry, then rescaled (red). The ATLAS models (blue) assume plane-parallel geometry. The vertical dashed line indicates the point where the PHOENIX models are truncated in the LDCs fit with ExoTETHyS. Right panel: Analogous plot with normalised intensities vs. r.

Fig. 3

 3 Fig.3Limb-darkening profiles for a solar-like star using the LDCs from the ATLAS 2000 (blue) and PHOENIX 2012 13 (red) tables provided in the supplemental material. The left panels show the results obtained for the VISPhot, FGS1 and FGS2 photometers. The right panels show the results for the white band integrated spectrometers.

Fig.

  Fig. Analogous to Figure 3, but for an M dwarf.

Table 3

 3 The first line contains the stellar model database and the Ariel instrument name. The second line defines the column entries of the following lines: stellar effective temperature, surface gravity, metallicity, wavelength intervals, and claret-4 LDCs, respectively.

	Example	of	LDCs	table	extracted	from	supplementary	file
	ARIEL grid ldc phoenix cond airsch0.txt.

Main GitHub repository https://github.com/ucl-exoplanets/ExoTETHyS

Acknowledgements The authors would like to thank A. Claret and E. Pascale for useful discussions. G.M. was supported by the LabEx P2IO, the French ANR contract 05-BLANNT09-573739. S.S. was supported by United Kingdom Space Agency (UKSA) grant: ST/S002456/1.


Hernán Melgratti

Claudio Antares Mezzina

G Michele Pinna

Keywords: Petri Nets, Reversible CCS, Concurrency

Reversible CCS (RCCS) is a well-established, formal model for reversible communicating systems, which has been built on top of the classical Calculus of Communicating Systems (CCS). In its original formulation, each CCS process is equipped with a memory that records its performed actions, which is then used to reverse computations. More recently, abstract models for RCCS have been proposed in the literature, basically, by directly associating RCCS processes with (reversible versions of) event structures. In this paper we propose a detour: starting from one of the well-known encoding of CCS into Petri nets we apply a recently proposed approach to incorporate causally-consistent reversibility to Petri nets, obtaining as result the (reversible) net counterpart of every RCCS term.

Towards a truly concurrent semantics for reversible CCS 1 Introduction

CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] is a foundational calculus for concurrent systems. Typically, systems are described as the parallel composition of processes (i.e., components) that communicate by sending and receiving messages over named channels. Processes are then defined in terms of communication actions performed over specific channels: we write a and a to respectively represent a receive and a send over the channel a. Basic actions can be composed through prefixing (i.e., sequencing) ( . ), choice ( + ) and parallel ( ) operators. The original formulation of the semantics of CCS adheres to the so called interleaved approach, which only accounts for the executions that arise from a single processor; hence, parallelism can be reduced to non-deterministic choices and prefixing. For instance, the CCS processes a b and a.b + b.a are deemed equivalent, i.e., it does not distinguish a process that can perform a and b concurrently from one that sequentialises their execution in any possible order (interleaving/schedule). Successive works have addressed the problem of equipping CCS with true concurrent semantics in the style of Petri nets and Event Structures. It has been shown that every CCS process can be associated with a Petri net that can mimic its computations. Different flavours of Petri nets have been used in the literature; for instance, occurrence nets [START_REF] Goltz | Semantics of Systems of Concurrent Processes[END_REF], a variant of Conditions/Events nets [START_REF] Degano | A distributed operational semantics for CCS based on condition/event systems[END_REF], and flow nets [START_REF] Boudol | Flow models of distributed computations: Three equivalent semantics for CCS[END_REF]. The works in [START_REF] Winskel | Event Structures. In Petri Nets: Applications and Relationships to Other Models of Concurrency[END_REF] and [START_REF] Boudol | Flow models of distributed computations: Three equivalent semantics for CCS[END_REF] have additionally shown that the computation of a CCS process can be represented by using event structures.

Many efforts were made in the last decades to endow computation models with reversible semantics [START_REF] Aman | Foundations of reversible computation[END_REF][START_REF] Mezzina | Software and reversible systems: A survey of recent activities[END_REF] and, in particular, two different models have been proposed for CCS: RCCS [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Krivine | A verification technique for reversible process algebra[END_REF] and CCSK [START_REF] Phillips | Reversing algebraic process calculi[END_REF]. Both of them incorporate a logging mechanism in the operational semantics of CCS that enables the undoing of computation steps. Moreover, it has been shown that they are isomorphic [START_REF] Lanese | Static versus dynamic reversibility in CCS[END_REF] since they only differ on the information that they log: while RCCS relies on some form of memory/monitor, CCSK uses keys. Previous approaches have also developed true concurrent semantics for reversible versions of CCS. For instance, it has been shown that CCSK can be associated with reversible bundle event structures [START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF][START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF]. However, we still lack a Petri net model for RCCS processes. We may exploit some recent results that connect reversible occurrence nets with reversible event structures [START_REF] Melgratti | Reversing place transition nets[END_REF][START_REF] Melgratti | Reversible occurrence nets and causal reversible prime event structures[END_REF][START_REF] Melgratti | A distributed operational view of reversible prime event structures[END_REF] to indirectly recover a Petri net model from the reversible bundle event structures defined in [START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF]. However, we follow a different approach, which is somehow more direct:

1. we encode (finite) CCS processes into a generalization of occurrence nets, namely unravel nets, in the vein of Boudol and Castellani [START_REF] Boudol | Flow models of distributed computations: Three equivalent semantics for CCS[END_REF]; 2. we show that unravel nets can be made causally-consistent reversible by applying the approach in [START_REF] Melgratti | Reversible occurrence nets and causal reversible prime event structures[END_REF]; 3. we finally shows that the reversible unravel nets derived by our encoding are an interpratation of RCCS terms.

An interesting aspect of the proposed encoding is that it highlights that all the information needed for reversing an RCCS process is already encoded in the structure of the net corresponding to the original CCS process, i.e., RCCS memories are represented by the structure of the net. Concretely, if an RCCS process R is a derivative of some CCS process P , then the encoding of R is retrieved from the encoding of P , what changes is the position of the markings.

Consider the CCS process P = a.0 that executes a and then terminates. It can be encoded as the Petri net on the left in Figure 1 (the usage of the apparently redundant places in the postset of a will be made clearer in Section 3).

The reversible version of P is R = a.0, where denotes an initially empty memory. According to RCCS semantics, R evolves to R = * , a, 0 • 0 by executing a. The memory * , a, 0 • in R indicates that it can go back to the initial process R by undoing a. Note that the net corresponding to P (on the left) has already all the information needed to reverse the action a; morally, a can be undone by firing it in the opposite direction (i.e., by consuming tokens from the postset and producing them in its preset), or equivalently, by performing a reversing transition a that does the job, as shown in the net drawn in the middle Organization of the paper. After setting up some notation, we recall CCS and RCCS (Section 2). In Section 3 we summarise the basics of Petri nets, unravel nets and present their reversible counterpart. In Section 4, describe the encoding of CCS into unravel nets and introduce the mapping from RCCS terms into reversible unravel nets. In the final section we draw some conclusions and discuss future developments.

Preliminaries. We denote with N the set of natural numbers.

CCS and reversible CCS

Let A be a set of actions a, b, c, . . ., and A = {a | a ∈ A} the set of their coactions. We denote the set of all possible actions with Act = A ∪ A. We write α, β for the elements of Act τ = Act ∪ {τ }, where τ / ∈ Act stands for a silent action. The syntax of (finite) CCS is reported in Figure 2. A prefix (or action) is either an input a, an output a or the silent action τ . A term of the form i∈I α i .P i represents a process that (non-deterministically) starts by selecting and performing some action α i and then continues as P i . We write 0, the idle process, in lieu of i∈I α i .P i when I = ∅ ; similarly, α i .P for a unitary sum in which I is the singleton {i}. The term P Q represents the parallel composition of the processes P and Q. An action a can be restricted so to be visible only

Q α -→ P Q (par-l) Q α -→ Q P Q α -→ P Q (par-r) P α -→ P Q ᾱ -→ Q P Q τ -→ P Q (syn) P α -→ P α / ∈ {a, ā} P \a α -→ P \a (r-res)
Fig. 3: CCS semantics inside process P , written P \a. Restriction is the only binder in CCS: a occurs bound in P \a.

We write n(P ) for the set of names of a process P , and, respectively, fn(P ) and bn(P ) for the sets of free and bound names. The set P denotes the set of all CCS processes. Definition 1 (CCS Semantics). The operational semantics of CCS is defined as the LTS (P, Act τ , →) where the transition relation → is the smallest relation induced by the rules in Figure 3.

Let us comment on rules of Figure 3. Rule act transforms an action α into a label. Rules par-l and par-r permit respectively the left and the right process of a parallel composition to propagate an action. Rule syn regulates the syncrhonization allowing two process in parallel to handshake. Rule hide forbids a restricted action to be further propagated.

Reversible CCS. Reversible CCS (RCCS) [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Krivine | A verification technique for reversible process algebra[END_REF] is a reversible variant of CCS. Processes in RCCS are equipped with a memory, in which a process keeps information about its past actions. The syntax of RCCS is in Figure 4, where CCS processes are defined as in the original formulation. A reversible process is either a monitored process m P with m a memory and P a CCS process, the parallel composition R S of the reversible processes R and S, and the restriction R\a in which a is restricted to R. A memory is a (possible empty) stack of events that encodes the history of actions previously performed by a process; whose top-most element corresponds to the very last action performed by the monitored process. Memories can contain three different kinds of events4 : partial synchronisations * , α, Q , full synchronisations m, α, Q , and memory

(CCS Processes) P, Q ::= i∈I αi.Pi | (P Q) | P \a (RCCS Processes) R, S ::= m P | (R S) | R\a (Memories) m ::= * , α, Q • m | m, α, Q • m | 1 • m | 2 • m |
Fig. 4: RCCS syntax splits 1 and 2 . The action α and the process Q in a synchronisation (either partial or full) record the selected action α of a choice and the discarded branches Q. The (technical) distinction between partial and full synchronisation will be made clear when describing the semantics or RCCS. Events 1 and 2 represent the split of a process in two parallel ones. The empty memory is represented by . Let us note that in RCCS memories serves also as unique process identifiers.

As for CCS, the only binder in RCCS is restriction (at the level of both CCS and RCCS processes). We extend functions n, fn and bn to RCCS processes and memories accordingly. We define M the set of all the possible memories and P R the set of all RCCS processes. Definition 2 (RCCS Semantics). The operational semantics of RCCS is defined as a pair of LTSs on the same set of states and set of labels: a forward LTS (P R , M × Act τ , →) and a backward LTS (P R , M × Act τ , ). Transition relations → and are the smallest relations induced by the rules in Figure 5 (left and right columns, respectively). Both relations exploit the structural congruence relation ≡, which is the smallest congruence on RCCS processes containing the rules in Figure 6. We define = → ∪ .

Let us comment on the forward rules (Figure 5, left column). Rule r-act allows a monitored process to perform a forward action. The action goes along with the memory m of the process. Since at this point we do not know whether the process will synchronise or not with the context a partial synchronisation event of the form * , α z z , i∈I\z α i .P i is put on top of the memory. The '*' will be replaced by a memory, say, m 1 if the process will eventually synchronise with a process monitored by m 1 . Let us note that the discarded process Q is recorded in the memory. Moreover, along with the prefix we also store its position 'z' within the sum. This piece of information is redundant for RCCS, and indeed was not present in the original semantics. However, it will be of help when encoding a RCCS process into a net, and when proving the operational correspondence. We remark that this simple modification does not intact the original semantics of RCCS. Rules r-par-l and r-par-r propagate an action through a parallel composition. Rule r-syn allows two parallel processes to synchronize. To do so, they have to match both the action α and then the two partial synchronisation of the two processes are updated to two full synchronisation through the operator '@'. Let R be a monitored process and m 1 and m 2 two memories, then R m2@m1 stands for the process obtained from R by substituting all occurrences

m i∈I αi.Pi m:α z ---→ * , α z z , i∈I\{z} αi.Pi • m Pz (r-act) * , α z z , i∈I\{z} αi.Pi • m Pz m:αz m i∈I αi.Pi (r-act • ) (r-par-l) R m:α --→ R R S m:α --→ R S R m:α R R S m:α R S (r-par-l • ) (r-par-r) S m:α --→ S R S m:α --→ R S S m:α S R S m:α R S (r-par-r • ) (r-syn) R m 1 :α ---→ R S m 2 : ᾱ ---→ S R S m1,m2:τ ------→ R m 2 @m 1 S m 1 @m 2 R m 1 :α R S m 2 : ᾱ S R S m1,m2:τ R S (r-syn • ) (r-res) R m:α --→ R α / ∈ {a, ā} R\a m:α --→ R \a R m:α R α / ∈ {a, ā} R\a m:α R \a (r-res • ) (r-equiv) R ≡ R R m:α --→ S S ≡ S R m:α --→ S R ≡ R R m:α S S ≡ S R m:α S (r-equiv • ) Fig. 5: RCCS semantics of * , α, Q • m 1 by m 2 , α, Q • m 1 .
Rule r-res propagates actions through restriction provided that the action is not on the restricted name. Rule r-equiv allows one to exploit structural congruence of Figure 6. Structural rule split allows a monitored process with a top-level parallel composition to split into a left and right branch, duplicating the memory. Structural rule res allows one to push restriction outside monitored processes. Structural rule α allows one to exploit α-conversion, denoted by = α .

Definition 3 (Initial Process and Coherent process). A RCCS process of the form P is called initial. Every process R derived from an initial process is called coherent process.

Petri nets, Unravel Nets and Reversible Unravel Nets

A Petri net is a tuple N = S, T, F, m , where S is a set of places and T is a set of transitions (with S ∩ T = ∅), F ⊆ (S × T ) ∪ (T × S) is the flow relation, and m ∈ ∂S is called the initial marking.

Petri nets are depicted as usual: transitions are boxes, places are circles and the flow relation is depicted using directed arcs. The presence of tokens in places

(split) m (P Q) ≡ 2 • m P 1 • m Q (res) m P \a ≡ (m P )\a if a / ∈ fn(m) (α) R ≡ S if R =α S
Fig. 6: RCCS Structural laws is signaled by a number of '•' in it. The marking represents the state of the distributed and concurrent system modeled by the net, and it is distributed. Given a net N = S, T, F, m and x ∈ S ∪T , we define the following multisets:

• x = {y | (y, x) ∈ F } and x • = {y | (x, y) ∈ F }. If x is a place then • x and x • are (multisets) of transitions; analogously, if x ∈ T then • x ∈ ∂S and x • ∈ ∂S. A transition t ∈ T is enabled at a marking m ∈ ∂S, denoted by m [t , whenever • t ⊆ m.
A transition t enabled at a marking m can fire and its firing produces the marking m = m -• t + t • . The firing of t at a marking m is denoted by m [t m . We assume that each transition t of a net N is such that • t = ∅, meaning that no transition may fire spontaneously. Given a generic marking m (not necessarily the initial one), the firing sequence (shortened as fs) of N = S, T, F, m, starting at m is defined as: (i) m is a firing sequence (of length 0), and (ii

) if m [t 1 m 1 • • • m n-1 [t n m n is a firing sequence and m n [t m , then also m [t 1 m 1 • • • m n-1 [t n m n [t m is
N = {lead (σ) | σ ∈ R N m }. Given a fs σ = m [t 1 m 1 • • • m n-1 [t n m ,
we write X σ = n i=1 t i for the multiset of transitions associated to fs, which we call an execution of the net and we write

E(N ) = {X σ ∈ ∂T | σ ∈ R N m }
for the set of the executions of N . Observe that an execution simply says which transitions (and the relative number of occurrences of them) has been executed, not their (partial) ordering. Given a fs σ

= m [t 1 m 1 • • • m n-1 [t n m n • • • , with ρ σ we denote the sequence t 1 t 2 • • • t n • • • . Definition 4. A net N = S, T, F, m is said to be safe if each marking m ∈ M N is such that m = [[m]].
The notion of subnet will be handy in the following. A subnet is obtained by restricting places and transitions, and correspondingly the flow relation and the initial marking. Unravel nets describe the dependencies among the transitions in the executions of a concurrent and distributed device and are similar to flow nets [START_REF] Boudol | Flow event structures and flow nets[END_REF][START_REF] Boudol | Flow models of distributed computations: Three equivalent semantics for CCS[END_REF]. Flow nets are safe nets where, for each possible firing sequence, each place can be marked just once. This requirement implies that the subnet obtained by the transitions executed in the firing sequence is a causal net and also that all the transitions t are such that • t = ∅.

In an UN conflicting pair of transitions t and t are those that are never together in an execution, i.e. ∀X ∈ E(N ). {t, t } ⊆ X. Given a place s in an unravel net, if • s contains more than one transition, then the transitions in • s are in conflict.

It is worthwhile to observe that the classical notion of occurrence net [START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part 1[END_REF][START_REF] Winskel | Event Structures. In Petri Nets: Applications and Relationships to Other Models of Concurrency[END_REF] is indeed a particular kind of UN namely one where the conflict relation is inherited along the transitive closure of the flow relation and it can can be inferred from the structure of the net itself. A further evidence that unravel nets generalize occurrence nets is implied also by the fact that flow nets generalize occurrence nets as well [START_REF] Boudol | Flow event structures and flow nets[END_REF].

An unravel net N = S, T, F, m is complete whenever ∀t ∈ T ∃s t ∈ S.

• s t = {t} ∧ s t • = ∅.
Thus in a complete UN the execution of a transition t is signaled by the marked place s t . Given an UN N , it can be turned easily into a complete one by adding for each transition the suitable place, without changing the executions of the net, thus we consider complete UNs only. Completeness comes handy when defining the reversible counterpart of an UN.

Reversible unravel nets. The definition of reversible unravel net follows the one of reversible occurrence net [START_REF] Melgratti | Reversible occurrence nets and causal reversible prime event structures[END_REF] and generalize reversible occurrence nets as unravel nets generalize occurrence nets. The transitions in U are the reversing ones; hence, we often say that a reversible unravel net N is reversible with respect to U . A reversing transition u is associated with a unique non-reversing transition t (condition 1) and its effects are intended to undo t. The second condition ensures that there is an injective mapping h : U → T which in turn implies that each reversible transition has exactly one reversing transition. The third requirement guarantees that there are no isolated conditions and the final one states that the subnet obtained forgetting all the reversing transitions is indeed an unravel net.

Definition 7. A reversible unravel net (rUN for short) is a quintuple N = S, T, U, F, m such that 1. U ⊆ T and ∀u ∈ U . ∃! t ∈ T \ U such that • u = t • and u • = • t, 2. ∀t, t ∈ T . • t = • t ∧ t • = t • ⇒ t = t , 3. t∈T ( • t ∪ t • ) = S,
Along the lines of [START_REF] Melgratti | Reversible occurrence nets and causal reversible prime event structures[END_REF], we can prove that the set of reachable markings of a reversible unravel net is not influenced by performing a reversing transition. Let N = S, T, U, F, m be an rUN. Then M N = M N | T \U . A consequence of this fact is that each marking can be reached by using just forward events. Let N = S, T, U, F, m be an rUN and σ be an fs. Then, there exists an fs σ such that X σ ⊆ T \ U and lead (σ) = lead (σ ).

Given an unravel net and a subset of transitions to be reversed, it is straightforward to obtain a reversible unravel net. Proposition 1. Let N = S, T, F, m be a complete unravel net and U ⊆ T the set of transitions to be reversed. Define

- → N U = S , T , U , F , m where S = S , U = U × {r}, T = (T × {f}) ∪ U , F = {(s, (t, f)) | (s, t) ∈ F } ∪ {((t, f), s) | (t, s) ∈ F } ∪ {(s, (t, r)) | (t, s) ∈ F } ∪ {((t, r), s) | (s, t) ∈ F } and m = m. Then - → N U is a reversible unravel net.
The construction above simply adds as many events (transitions) as transitions to be reversed in U . The preset of each added event is the postset of the corresponding event to be reversed, and its postset is the preset of the event to be reversed. We write -→ N instead of -→ N T when N = S, T, F, m , i.e., when every transition is reversible.

In Figure 7a we show a non-complete unravel net, whose complete version is in Figure 7b. The reversible unravel net obtained by reversing every transition is depicted in Figure 7c.

CCS processes as unravel nets

We now recall the encoding of CCS terms into Petri nets due to Boudol and Castellani [START_REF] Boudol | Flow models of distributed computations: Three equivalent semantics for CCS[END_REF]. We just recall that originally the encoding was on proved terms instead of plain CCS. The difference between proved terms and CCS is that somehow in a proved term the labels carry the position of the process who did the action. Hence, we will use decorated version of labels. For instance, â.b denotes an event b which past was a. That is, if we want to indicate the event b of the term a.b we will write â.b. Analogously, labels carry also information about the syntactical structure of a term, actions corresponding to subterms of a choice and of a parallel composition are also decorated with an index i that indicates the subterm that performs the actions. An interesting aspect of this encoding is that these information is reflected in the name of the places and the transitions of the nets, which simplifies the formulation of the behavioural correspondence of a term and its associated net. We write ( ) for the function that removes decorations for a name, e.g., (â. b.c) = c. We now are in place to define and comment the encoding of a CCS term into a net. The encoding is inductively defined on the structure of the CCS process. For a CCS process P , its encoded net is N (P ) = S P , T P , F P , m P . The net corresponding to the inactive process 0, is just a net with just one marked place and with no transition, that is: Definition 8. The net N (0) = {0}, ∅, ∅, {0} is the net associated to 0 and it is called zero.

To ease notation in the constructions we are going to present, we adopt following conventions: let X ⊆ S ∪ T be a set of places and transitions, we write â.X for the set {â.x | x ∈ X} containing the decorated versions of places and transitions in X. Analogously we lift this notation to relations: if R is a binary relation on (S ∪ T ), then α.R = {(α.x, α.y) | (x, y) ∈ R} is a binary relation on (α.S ∪ α.T ).

The net N (α.P ) corresponding to a process α.P extends N (P ) with two extra places α.P and â.α and one transition α. The place α.P stands for the process that executes the prefix α and follows by P . The place â.α is not in the original encoding of [START_REF] Boudol | Flow models of distributed computations: Three equivalent semantics for CCS[END_REF]; we have add it to ensure that the obtained net is complete, which is essential for the definition of the reversible net. This will become clearer when commenting the encoding of the parallel composition. It should be noted that this addition does not interfere with the behaviour of the net, since all added places are final. Also a new transition, named α is created and added to the net, and the flow relation is updated accordingly. Figures 8a, 8b and 8c report the respectively the encoding of the inactive process, of the process b.0 and a.b.0. Moreover the aforementioned figures systematically show how the prefixing operator is rendered into Petri nets. As a matter of fact, the net a.b.0 is built starting from the net corresponding to b.0 by adding the prefix a. We note that also the label of transitions is affected by appending the label of the new prefix at the beginning. This is rendered in Figure 8c where the transition mimicking the action b is labeled as â.b indicating that an a was done before b. In what follows we will often omit such representation from figures. Definition 9. Let P a CCS process and N (P ) = S P , T P , F P , m P be the associated net. Then N (α.P ) is the net S α.P , T α.P , F α.P , m α.P where

S α.P = {α.P, α.α} ∪ α.S P T α.P = {α} ∪ α.T p F α.P = {(α.P, α), (α, α.α)} ∪ {(α, α.b) | b ∈ m 0P } ∪ α.F P m α.P = {α.P }
For a set X of transitions we write i X for { i x | x ∈ X}, which straightforwardly lifts to relations.

The encoding of the parallel goes along the line of the prefixing one. Also in this case we have to decorate the places (and transitions) with the position of the term in the syntax tree. To this end, each branch of the parallel is decorated with i with i being the i-th position. Regarding the transitions, we have to add all the possible synchronisations among the processes in parallel. This is why, along with the transitions of the branches (properly decorated with i ) we have to add extra transitions to indicate the possible synchronisation. Naturally a synchronisation is possible when one label is the co-label of the other transition. Figure 9a shows the net corresponding to the process a.b a.c. As we can see, the encoding builds upon the encoding of a.b and a.c, by (i) adding to all the places and transitions whether the branch is the left one or the right one and (ii) adding an extra transition and place for the only possible synchronisation. We add an extra place (in line with the prefixes) to mark the fact that a synchronisation has taken place. Let us note that the extra places a, a and τ are used to understand whether the two prefixes have been executed singularly (e.g., no synchronisation) or they contributed to do a synchronisation. Suppose, for example, that the net had not such places, and suppose that we have two tokens in the places 0 â.b and

S P1 P2 = 0 S P1 ∪ 1 S P2 ∪ {s {t,t } | t ∈ T P1 ∧ t ∈ T P2 ∧ (t) = (t )} T P1 P2 = 0 T P1 ∪ 1 T P2 ∪ {{t, t } | t ∈ T P1 ∧ t ∈ T P2 ∧ (t) = (t )} F P1 P2 = 0 F P1 ∪ 1 F P2 ∪ {({t, t }, s {t,t } ) | t ∈ T P1 ∧ t ∈ T P2 ∧ (t) = (t )} ∪{( i s, (t 1 , t 2 )) | (s, t i ) ∈ F Pi } ∪ {( i s, (t 1 , t 2 )) | (s, t i ) ∈ F Pi } m P0 P 2 = 0 m P0 ∪ 1 m P1
The encoding of choice operator is similar to the parallel one. The only difference is that we do not have to deal with possible synchronisations since the branches of a choice operator are mutually exclusive. Figure 9b reports the net corresponding to the process a.b + ā.c. As in the previous examples, the net is built upon the subnets representing a.b and ā.c. Definition 11. Let N (P i ) be the net associated to the processes P i for i ∈ I. Then + i∈I P i is the net S + i∈I Pi , T + i∈I Pi , F + i∈I Pi , m + i∈I Pi where:

S + i∈I Pi = ∪ i∈I + i S Pi T + i∈I Pi = ∪ i∈I + i T Pi F + i∈I Pi = {(+ i x, + i y) | (x, y) ∈ F Pi } ∪ {(+ j s, + i t) | s ∈ m Pj ∧ • t ∈ m Pi ∧ i = j} m + i∈I Pi = ∪ i∈I + i m Pi .
We write T a for the set {t ∈ T | nm( (t)) = a}. The encoding of the hiding operator simply removes all transitions whose labels corresponds to actions over the restricted name. Definition 12. Let P a CCS process and N (P ) = S P , T P , F P , m P be the associated net. Then N (P \ a) is the net S P \a , T P \a , F P \a , m P \a where

S P \a = \ a S P T P \a = \ a (T P \ T a ) F P \a = {(\ a s, \ a t) | (s, t) ∈ F P , t ∈ T a P } ∪ {(\ a t, \ a s) | (t, s) ∈ F P , t ∈ T a P } m P \a = \ a m P .
Figure 10 shows a more complex example, the net corresponding to the process a.a a + b. In this case, the process on the right of the parallel composition can synchronise with the one on the left one in two different occasions. This is why there are two different transitions representing the synchronisation. Also, since the right process of the parallel is a choice operator, it can happen that the right branch of it is executed, thus interdicting the synchronisation. Let us note that since the right branch of the parallel operator is a choice one, composed by two branches, the encoding labels these branches with ' 1 + 0 ' and ' 1 + 1 ' to indicate respectively the left and right branch of the choice operator, which is the right branch of a parallel operator. The following proposition is instrumental for our result. We are now in place to define what is the net corresponding to a RCCS process. So far we have spoken about encoding CCS processes into nets. We remark that since RCCS is built upon CCS processes, also the encoding of RCCS is built upon the encoding of CCS. To do so, we first need the notion of ancestor, that is the initial process from which an RCCS process is derived. Let us note that since we are considering coherent RCCS processes (see Definition 3), an RCCS process has always an ancestor. The ancestor ρ(R) of an RCCS process R can be calculated syntactically from R, since all the information about the past are

ρ( P ) = P ρ( , α z z , i∈I\{z} αi.Pi • m P ) = ρ(m i∈I αi.Pi) ρ( i • m P ) = i • m P ρ(P1 P2) = ρ(m P 1 P 2 ) where ρ(Pi) = i • m P i ∧ i ∈ {1, 2} ρ(P \ a) = ρ(P ) \ a
Fig. 11: The ancestor of an RCCS process stored into memories. The only point in which a process has to wait for its sibling is when a memory fork 1 or 2 is met.

Definition 13. Given a coherent RCCS process R, its ancestor ρ(R) is inductively defined as in Figure 11.

The idea behind the ancestor process is that the encoding of an RCCS process and of its ancestor should give the same net, what changes is the position where the markings are placed. And such position is derived by the information stored into memories. We then define the marking function µ(•) defined inductively as follows:

µ( P ) = {P } µ(P 0 P 1 ) = 0 µ(P 0 ) ∪ 1 µ(P 1 ) µ(P \ a) = \ a µ(P 1 ) µ( m , α i , Q • m P ) = µ(m + i α.P ) ∪ {s t,t | t = m + i α ∧ t = m + i α} µ( * , α i , Q • m P ) = µ(m + i α.P ) ∪ µ(m + i α)
We are now in place to define what is the reversible net corresponding to an RCCS process: Definition 14. Let R be an RCCS term with ρ(R) = P . Then ---→ N (R) is the net S, T, F, µ(R) where N (P ) = S, T, F, m .

Proposition 3. Let R be an RCCS term with ρ(R) = P . Then - - - → N (R) is a reversible unravel net.
In a few words Proposition 3 tells us that the reversible net corresponding to a coherent RCCS R is that one of its ancestor. The contribution of R to the construction of its net relies in the markings, that is the computational history contained in R is what determines the markings. This is rendered in Figures 12a and12b where the two nets are the same since the two processes R 1 and R 2 shares the same origin. What changes is the where markings are placed, since R 1 and R 2 represents different computation from the origin process.

We can now state our main result in terms of bisimulation: is a bisimulation. Let us note that all the transitions in the generated net have a unique name, which is the path from the root to the term in the abstract syntax tree. There is a one to one correspondence between this path and the memory of a process which can mimic the same action/transition.

Conclusions and future works

On the line of previous research we have equipped a reversible process calculus with a non sequential semantics by using the classical encoding of process calculi into nets. What comes out from the encoding is that the machinery to reverse a process was already present in the encoding.

Our result relies on unravel nets, that are able to represent or -causality. The consequence is that the same event may have different pasts. Unravel nets are naturally related to bundle event structures [START_REF] Langerak | Bundle event structures: a non-interleaving semantics for LOTOS[END_REF][START_REF] Langerak | Causal ambiguity and partial orders in event structures[END_REF], where the dependencies are represented using bundles, namely finite subsets of conflicting events, and the bundle relation is usually written as X → e. Starting from an unravel net S, T, F, m , and considering the transition t ∈ T , the bundles representing the dependencies are • s → t for each s ∈ • t, and the conflict relation can be easily inferred by the semantic one definable on the unravel net. This result relies on the fact that in any unravel net, for each place s, the transitions in • s are pairwise conflicting. The reversible bundle structures add to the bundle relation (defined also on the reversing events) a prevention relation, and the intuition behind this relation is the usual one: some events, possibly depending on the one to be reversed, are still present and they prevent that event to be reversed. The problem here is that in an unravel net, differently from occurrence nets, is not so easy to determine which transitions depend on the happening of a specific one, thus potentially preventing it from being reversed. An idea would be to consider all the transitions in s • for each s ∈ t • , but it has to be carefully checked if this is enough. Thus, which is the proper "reversible bundle event structure" corresponding to the reversible unravel nets has to be answered, though it is likely that the conditions to be posed on the prevention relations will be similar to the ones considered in [START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF][START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF]. Once that also this step is done, we will have the full correspondence between reversible processes calculi and non sequential models.

Fig. 1 : 0 of Figure 1 .

 101 Fig. 1: Encoding of R = a.0

  Let A be a set, a multiset of A is a function m : A → N. The set of multisets of A is denoted by ∂A. We assume the usual operations on multisets such as union + and difference -. We write m ⊆ m if m(a) ≤ m (a) for all a ∈ A. For m ∈ ∂A, we denote with [[m]] the multiset defined as [[m]](a) = 1 if m(a) > 0 and [[m]](a) = 0 otherwise. When a multiset m of A is a set, i.e. m = [[m]], we write a ∈ m to denote that m(a) = 0, and often confuse the multiset m with the set {a ∈ A | m(a) = 0} or a subset X ⊆ A with the multiset X(a) = 1 if a ∈ A and X(a) = 0 otherwise. Furthermore we use the standard set operations like ∩, ∪ or \. The multiset m such that [[m]] = ∅ is denoted with abuse of notation as ∅.

Fig

  Fig. 2: CCS Syntax

  a firing sequence. The set of firing sequences of a net N starting at a marking m is denoted by R N m and it is ranged over by σ. Given a fs σ = m [t 1 σ [t n m n , start(σ) is the marking m, lead (σ) is the marking m n and tail (σ) is the fs σ [t n m n . Given a net N = S, T, F, m, , a marking m is reachable iff there exists a fs σ ∈ R N m such that lead (σ) is m. The set of reachable markings of N is M

Definition 5 .Definition 6 .

 56 Let N = S, T, F, m be a Petri net and let T ⊆ T be a subset of transitions and S = • T ∪ T • . Then, the subnet generated by T N | T = S , T , F , m , where F is the restriction of F to S and T , and m is the multiset on S obtained by m restricting to the places in S . Unravel nets. To define unravel nets we need the notion of causal net. A safe Petri net N = S, T, F, m is a causal net (CA for short) when ∀s ∈ S. | • s| ≤ 1 and |s • | ≤ 1, F * is acyclic, T ∈ E(N ), and ∀s ∈ S • s = ∅ ⇒ m(s) = 1.Requiring that T ∈ E(N ) implies that each transition can be executed and F * acyclic means that dependencies among transitions are settled. A causal net has no isolated and unmarked places as ∀s ∈ S • s = ∅ ⇒ m(s) = 1. An unravel net (UN for short) N = S, T, F, m is a safe net such that for each execution X ∈ E(N ) the subnet N | X is a causal net.

and 4 .

 4 N | T \U is a complete unravel net and S, T, F, m is safe one.

Fig. 7 :Fig. 8 :

 78 Fig. 7: An UN N , its complete version N and the associated rUN -→ N

Fig. 9 :

 9 Fig.9: Example of nets corresponding to CCS parallel and choice operator. We omit the trailing 0

Fig. 10 :

 10 Fig. 10: A complex example: N (a.a a + b)

Proposition 2 .

 2 The nets defined in Definition 8, Definition 9, Definition 10, Definition 11 and Definition 12 are complete unravel nets.

Fig. 12 :

 12 Fig.12: Example of nets corresponding to RCCS processR 1 = * , a 1 , 0 • 1 • b 2 • ā.c and R 2 = * , b 1 , 0 • m 2 , a 1 , 0 • 1 • b m 1 , a 1 , 0 • 2 • c with m i = i •

In this paper we use the original RCCS semantics with partial synchronisation. Later versions, e.g.[START_REF] Krivine | A verification technique for reversible process algebra[END_REF], use communication keys to univocally identify actions.

â.b. Now, how can we understand whether these two tokens are the result of the firing sequence a,a or they are the result of the τ transition? It is impossible, but by using the aforementioned extra-places, which are instrumental to tell if a single prefix has executed, we can distinguish the τ from the firing sequence a,a and then reverse accordingly.

Partially supported by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement 778233, by the French ANR project DCore ANR-18-CE25-0007 and by the Italian INdAM -GNCS 2020 project Sistemi Reversibili Concorrenti: dai Modelli ai Linguaggi, and by the UBACyT projects 20020170100544BA and 20020170100086BA.


Pagdame Tiebekabe
email: pagdame.tiebekabe@ucad.edu.sn

Ismaïla Diouf
email: ismaila.diouf@ucad.edu.sn

On solutions of the Diophantine equation L n + L m = 3 a

Keywords: AMS Subject Classifications: 11B39, 11J86 Linear forms in logarithm, Diophantine equations, Fibonacci sequence, Lucas sequence, perfect powers

Let (Ln) n≥0 be the Lucas sequence given by L0 = 2, L1 = 1 and Ln+2 = Ln+1 + Ln for n ≥ 0. In this paper, we are interested in finding all powers of three which are sums of two Lucas numbers, i.e., we study the exponential Diophantine equation Ln + Lm = 3 a in nonnegative integers n, m, and a. The proof of our main theorem uses lower bounds for linear forms in logarithms, properties of continued fractions, and a version of the Baker-Davenport reduction method in Diophantine approximation.

Introduction

The determination of perfect powers of Lucas and Fibonacci sequences does not date from today. The real contribution of determination of perfect powers of Lucas and Fibonacci sequences began in 2006. By classical and modular approaches of Diophantine equations, Bugeaud, Mignotte, and Siksek [START_REF] Bugeaud | Classical and modular approaches to exponential Diophantine equations. I. Fibonacci and Lucas perfect powers[END_REF] defined all perfect powers of Lucas and Fibonacci sequences by solving the equations F n = y p and L n = y p respectively. From there, many researchers tackled similar problems. It is in the same thought that, others have determined the powers of 2 of the sum/difference of two Lucas numbers [START_REF] Bravo | Powers of Two as Sums of Two Lucas Numbers[END_REF], powers of 2 of the sum/difference of Fibonacci numbers [START_REF] Bravo | On the Diophantine Equation F n + F m = 2 a[END_REF], powers of 2 and of 3 of the product of Pell numbers and Fibonacci numbers.

Pagdame Tiebekabe and Ismaïla Diouf

We move our interest on the powers of 3 as a sum of two Lucas numbers. This paper follows the following steps : We first give the generalities on binary linear recurrence, then we demonstrate an important inequality on Lucas numbers and finally determine and reduce a coarse bound by section 3. The section 4 is devoted to the reduction of the obtained bound in section 3 and discussion of possible different cases. We know from Bravo and Lucas [START_REF] Bravo | Powers of Two as Sums of Two Lucas Numbers[END_REF] that the only solutions of the Diophantine equation F n + F m = 2 a in positive integers n, m and a with n ≥ m are given by

2F 1 = 2, 2F 2 = 2, 2F 3 = 4, 2F 6 = 16,
and

F 2 + F 1 = 2, F 4 + F 1 = F 4 + F 2 = 4, F 5 + F 4 = 8, F 7 + F 4 = 16.
and in [START_REF] Bravo | On the Diophantine Equation F n + F m = 2 a[END_REF] that all solutions of the Diophantine equation L n + L m = 2 a in nonnegative integers n ≥ m and a, are

2L 0 = 4, 2L 1 = 2, 2L 3 = 8, L 2 + L 1 = 4, L 4 + L 1 = 8, and L 7 + L 2 = 32.
Here in this paper, we determine all the solutions of the following Diophantine equation:

L n + L m = 3 a (1.1)
in nonnegative integers n ≥ m and a.

We are interested in finding all powers of three which are sums of two Lucas numbers, i.e., we study the exponential Diophantine equation L n + L m = 3 a in nonnegative integers n, m, and a. The proof of our main theorem uses lower bounds for linear forms in logarithms, properties of continued fractions, and a version of the Baker-Davenport reduction method in Diophantine approximation.

We notice that many authors have already tackled this type of problems.

Preliminaries

H n+k = a 1 H n+k-1 + a 2 H n+k-2 + • • • + a k H n for all n ≥ 0 with a 1 , . . . , a k ∈ C, fixed.
We suppose that a k = 0 (otherwise, the sequence {H n } n≥0 satisfies a recurrence of order less than k). If a 1 , . . . , a k ∈ Z and H 0 , . . . , H k-1 ∈ Z, then we can easily prove by induction on n that H n is an integer for all n ≥ 0. The polynomial f

(X) = X k -a 1 X k-1 -a 2 X k-2 -• • • -a k ∈ C, is called the characteristic polynomial of (H n ) n≥0 . We suppose that f (X) = m i=1 (X -α i ) σi ,
where α 1 , . . . , α m are distinct roots of f (X) with respectively σ 1 , . . . , σ m their multiplicities.

Definition 2.2. We define the sequences (A n ) n≥0 and (B n ) n≥0 for all positive integers N by

A n+2 = aA n+1 + A n , A 0 = 0, A 1 = 1 B n+2 = aB n+1 + B n , B 0 = 2, B 1 = a. For a = 1, (A n ) n≥0 = (F n ) n≥0 and (B n ) n≥0 = (L n ) n≥0
, which are Fibonacci and Lucas sequences respectively, defined above.

On solutions of the Diophantine equation L n + L m = 3 a Remark 2.3. If k = 2, the sequence (H n ) n≥0 is called a binary recurrent sequence. In this case, the characteristic polynomial is of the form

f (X) = X 2 -a 1 X -a 2 = (X -α 1 )(X -α 2 ). Suppose that α 1 = α 2 , then H n = c 1 α n 1 + c 2 α n
2 for all n ≥ 0. Definition 2.4. The binary recurrent sequence {H n } n≥0 is said to be non degenerated if c 1 c 2 α 1 α 2 = 0 and α 1 /α 2 is not a root of unity.

Binet's formula for the general term of Fibonacci and Lucas sequences is obtained using standard methods for solving recurrent sequences, which are given by :

F n = α n -β n α -β and L n = α n + β n where (α, β) = 1 + √ 5 2 , 1 - √ 5 2
are the zeros of the characteristic polynomial X 2 -X -1.

Definition 2.5. For all algebraic numbers γ, we define its measure by the following identity :

M(γ) = |a d | d i=1 max{1, |γ i |},
where γ i are the roots of

f (x) = a d d i=1 (x -γ i ) is the minimal polynomial of γ.
Let us define now another height, deduced from the last one, called the absolute logarithmic height. It is the most used one.

h(γ) = 1 d log |a d | + d i=1 log max{1, |γ i |} = 1 d log M(γ).
the usual logarithmic absolute height of γ.

The following properties of the logarithmic height, will also be used in the next section:

• h(γ ± η) ≤ h(γ) + h(η) + log 2. • h(γη ±1 ) ≤ h(γ) + h(η).
• h(γ s ) = |s|h(γ).

Inequalities involving the Lucas numbers

In this section, we state and prove important inequalities associated with the Lucas numbers that will be used in solving the equation (1.1).

Proposition 2.7. For n ≥ 2, we have

0.94 α n < (1 -α -6 )α n ≤ L n ≤ (1 + α -4 )α n < 1.15 α n (2.1)
Proof. This follows directly from the formula

L n = α n + (-1) n α -n .
Pagdame Tiebekabe and Ismaïla Diouf

Linear forms in logarithms and continued fractions

In order to prove our main result, we have to use a Baker-type lower bound several times for a non-zero linear forms of logarithms in algebraic numbers. There are many of these methods in the literature like that of Baker and Wüstholz in [START_REF] Baker | Logarithmic and Diophantine Geometry[END_REF]. We recall the result of Bugeaud, Mignotte, and Siksek which is a modified version of the result of Matveev [START_REF] Matveev | An explicit lower bound for a homogeneous rational linear form in the logarithms of algebraic numbers, II[END_REF]. With the notation of section 2, Laurent, Mignotte, and Nesterenko [START_REF] Laurent | Formes linéaires en deux logarithmes et déterminants d'interpolation, (French) (Linear forms in two logarithms and interpolation determinants)[END_REF] proved the following theorem:

Theorem 2.8. Let γ 1 , γ 2 be two non-zero algebraic numbers, and let log γ 1 and log γ 2 be any determination of their logarithms.

Put D = [Q(γ 1 , γ 2 ) : Q]/[R(γ 1 , γ 2 ) : R],
and

Γ := b 2 log γ 2 -b 1 log γ 1 ,
where b 1 and b 2 are positive integers. Further, let A 1 , A 2 be real numbers > 1 such that

log A i ≥ max h(γ i ), | log γ i | D , 1 D , (i = 1, 2).
Then, assuming that γ 1 and γ 2 are mutiplicatively independent, we have

log |Γ| > -30.9 • D 4 max log b , 21 D , 1 2
2 log A 1 • log A 2 , where b = b 1 D log A 2 + b 2 D log A 1 .
We shall also need the following theorem due to Matveev, Lemma due to Dujella and Pethő and Lemma due to Legendre [START_REF] Dujella | A generalization of a theorem of Baker and Davenport[END_REF][START_REF] Matveev | An explicit lower bound for a homogeneous rational linear form in the logarithms of algebraic numbers, II[END_REF].

Λ := η b1 1 • • • η b l l -1 = l i=1 η bi i -1.
Let A 1 , . . . , A l reals numbers such that

A j ≥ max{Dh(η j ), | log(η j )|, 0.16}, 1 ≤ j ≤ l.
Assume that Λ = 0, So we have

log |Λ| > -3 × 30 l+4 × (l + 1) 5.5 × d 2 × A 1 ...A l (1 + log D)(1 + log nB) Further, if L is real, then log |Λ| > -1.4 × 30 l+3 × (l) 4.5 × d 2 × A 1 ...A l (1 + log D)(1 + log B).
During our calculations, we get upper bounds on our variables which are too large, so we have to reduce them. To do this, we use some results from the theory of continued fractions. In particular, for a non-homogeneous linear form with two integer variables, we use a slight variation of a result due to Dujella and Pethő, (1998) which is in itself a generalization of the result of Baker and Davemport [2].

For a real number X, we write X := min{| X -n |: n ∈ Z} for the distance of X to the nearest integer.

On solutions of the Diophantine equation L n + L m = 3 a Lemma 2.10. (Dujella and Pethő, [START_REF] Dujella | A generalization of a theorem of Baker and Davenport[END_REF]) Let M a positive integer, let p/q the convergent of the continued fraction expansion of κ such that q > 6M and let A, B, µ real numbers such that A > 0 and B > 1. Let ε := µq -M κq . If ε > 0 then there is no solution of the inequality

0 < mκ -n + µ < AB -m
in integers m and n with log(Aq/ε) log B m M.

Lemma 2.11. (Legendre) Let τ real number such that x, y are integers such that

τ - x y < 1 2y 2 . then x y = p k q k is the convergence of τ . Further, τ - x y > 1 (q k+1 + 2)y 2 .

Main Results

Our main result can be stated in the following theorem.

L n = 3 a 2 .
This equation has no solution because, ∀n > 0, L n ∈ Z. So from now, we assume n > m.

If n ≤ 200, the search with SageMath in the range 0 ≤ m < n ≤ 200 gives the solutions (n, m, a) ∈ {(1, 0, 1), (4, 0, 2)}. Now for the rest of the paper, we assume that n > 200 . Let first get a relation between a and n which is important for our purpose. Combining (1.1) and the right inequality of (2.1), we get:

3 a = L n + L m ≤ 2α n + 2α m < 2 n+1 + 2 m+1 = 2 n+1 (1 + 2 n-m ) ≤ 2 n+1 (1 + 1/2) < 2 n+2 .
Taking log both sides, we obtain a log 3 ≤ (n + 2) log 2 =⇒ a ≤ (n + 2)c 1 where c 1 = log 2 log 3 .

Rewriting equation (1.1) as:

L n + L m = α n + β n + L m = 3 a =⇒ α n -3 a = -β n -L m .

Pagdame Tiebekabe and Ismaïla Diouf

Taking absolute value both sides, we get

|α n -3 a | = |β n + L m | ≤ |β| n + L m < 1 2 + 2α m ∵ |β| n < 1 2
, and L m < 2α m .

Dividing both sides by α n and considering that n > m, we get:

1 -α -n • 3 a < α -n 2 + 2α m-n < 1 α n-m + 2 α n-m ∵ 1 2α n < 1 α n-m ; n > m Hence 1 -α -n • 3 a < 3 α n-m (3.1)
Let's take

γ 1 := α, γ 2 := 3, b 1 := n, b 2 := a, Γ := a log 3 -n log α
in order to apply Theorem 2.8. Therefore equation (3.1) can be rewritten as:

1 -e Γ < 3 α n-m where e Γ = α -n 3 a . (3.2) Since Q( √ 5
) is the algebraic number field containing γ 1 , γ 2 ; so we can take D := 2. Using equation (1.1) and Binet formula for Lucas sequence, we have :

α n = L n -β n < L n + 1 ≤ L n + L m = 3 a
which implies 1 < 3 a α -n and so Γ > 0. Combining this with (3.2), we get

0 < Γ < 3 α n-m (3.3)
where we used the fact that x ≤ e x -1, ∀x ∈ R. Applying log on right and left hand side of (3.3), we get

log Γ < log 3 -(n -m) log α. (3.4)
Logarithm height of γ 1 and γ 2 are:

h(γ 1 ) = 1 2 log α = 0.2406 • • • , h(γ 2 ) = log 3 = 1.09862 • • • , thus we can choose log A 1 := 0.5 and log A 2 := 1.1.
Finally, by recalling that a ≤ (n + 2)c 1 ; c 1 = 0.63093, we get :

b := b 1 D log A 2 + b 2 D log A 1 = n 2.2 + a = 0.45n + a < 0.45n + (n + 2)c 1 < 2n.
It is easy to see that α and 3 are multiplicatively independent. Then by Theorem 2.8, we have Let us find a second linear form in logarithm. For this, we rewrite (1.1) as follows:

log Γ ≥ -30.9 • 2 4 max log(2n), 21 2 , 1 2
2 • 0.5 • 1.1 log Γ > -272 max log(2n), 21 2 , 1 2 2 . ( 3
α n (1 + α n-m ) -3 a = -β n -β m .
Taking absolute values in the above relation, we get

|α n (1 + α m-n ) -3 a | < 2, β = (1 - √ 5)/2, |β| n < 1 and |β| m < 1; ∀n > 200, m ≥ 0.
Dividing both sides of the above inequality by α n (1 + α m-n ), we obtain

1 -3 a α -n (1 + α m-n ) -1 < 2 α n i.e |Λ| < 2 α n . (3.7)
All the conditions are now met to apply a Matveev's theorem (Theorem 2.9).

• Data:

t := 3; γ 1 := 3; γ 2 := α; γ 3 := 1 + α m-n b 1 := a; b 2 := -n, b 3 = -1. As before, K = Q( √ 5) contains γ 1 , γ 2 , γ 3 and has D := [K : Q] = 2.
Before continuing with the calculations, let's check whether Λ = 0. Λ = 0 comes from the fact that if it was zero, we would have

3 a = α n + α m (3.8)
Taking the conjugate of the above relation in Q( √ 5), we get :

3 a = β n + β m . (3.9)
Combining (3.8) and (3.9), we get :

α n < α n + α m = |β n + β m | ≤ |β| n + |β| m < 2.
Recall that n > 200. This relation is impossible for n > 200. Hence Λ = 0.

• Calculation of h(γ 3 )

Let us now estimate h(γ 3 ) where

γ 3 = 1 + α m-n γ 3 = 1 + α m-n < 2 and γ -1 = 1 1 + α m-n < 1 so | log γ 3 | < 1. Notice that h(γ 3 ) ≤ |m -n| log α 2 + log 2 = log 2 + (n -m) log α 2 .
Pagdame Tiebekabe and Ismaïla Diouf

• The calculation of A 1 and A 2 gives :

A 1 := 2.2
and

A 2 := 0.5
and we can take

A 3 := 2 + (n -m) log α since h(γ 3 ) := log 2 + (n -m) log α 2 • Calculation of B
Since a < (n + 2)c 1 , it follows that, B = max{1, n, a}. Thus we can take B = n + 1.

The Matveev's theorem gives the lower bound on the left hand side of (3.7) by replacing the data. We get :

exp (-C(1 + log(n + 1)) • 2.2 • 0.5 • (2 + (n -m) log α))
where

C := 1.4 • 30 6 • 3 4.5 • 2 2 (1 + log 2) < 9.7 × 10 11 .
Replacing in equation (3.7), we get: The continued fraction of the irrational number γ is : and let denote p k /q k its convergent. An inspection using SageMath gives the following inequality 4977896525362041575 = q 41 < 1.2 × 10 20 < q 42 = 805929983250536127817. Since Λ = 0, then z = 0. Two cases arise : z < 0 and z > 0. For each case, we will apply Lemma 2.10.

exp (-C(1 + log(n + 1)) • 2.2 • 0.5 • (2 + (n -m) log α)) < |Λ| < 2 α n which leads to n log α -log 2 < C((1 + log(n + 1)) • 1.1 • (2 + (n -m) log α) < 2C log n • 1.1 • (2 + (n -m) log α) then n log α -log 2 < 1.26 × 10 12 log n • (2 + (n -m) log α) (3
[a 0 ,
• Case 1 : z > 0 From (4.4), we obtain 0 < z ≤ e z -1 < 2 α n . Replacing (4.3) in the above inequality, we get:

0 < a log 3 -n log α -log ρ(n -m) ≤ 3 a α -n ρ(n -m) -1 -1 < 2α -n

Definition 2 . 6 .

 26 ( Absolute logarithmic height) For a non-zero algebraic number of degree d on Q where the minimal polynomial on Z is f (x) = a d d i=1 (xγ i ), we denote by

Theorem 2 .

 2 9. (Matveev [8]) Let n ≥ 1 an integer. Let L a field of algebraic number of degree D. Let η 1 , . . . , η l non-zero elements of L and let b 1 , b 2 , . . . , b l integers, B := max{|b 1 |, ..., |b l |}, and

Theorem 3 . 1 .

 31 The only solutions (n, m, a) of the exponential Diophantine equation L n + L m = 3 a in nonnegative integers n ≥ m and a, are : (1, 0, 1) and (4, 0, 2) i.e L 1 + L 0 = 3, and L 4 + L 0 = 9. Proof. First, we study the case n = m, next we assume n > m and study the case n ≤ 200 with SageMath in the range 0 ≤ m < n ≤ 200 and finally we study the case n > 200. Assume throughout that equation (1.1) holds. First of all, observe that if n = m, then the original equation (1.1) becomes

. 5 ), 1 2 2 . ( 3 . 6 )

 5236 Combining (3.4) and (3.5), we obtain the following important result (n -m) log α < 276 max log(2n), 21 2 On solutions of the Diophantine equation L n + L m = 3 a

2 . 4 .

 24 .10) where we used inequality 1 + log(n + 1) < 2 log n, which holds for n > 200. Now, using(3.6) in the right term of the above inequality (3.10) and doing the related calculations, we get n < 7.3 × 10 14 log n max log(2n), 21 2 (3.11) If max{log(2n), 21/2} = 21/2, it follows from (3.11) that n < 8.04825 • 10 16 log n =⇒ n < 3.5 • 10 18 . On the other hand, if max{log(2n), 21/2} = log(2n), then from (3.11), we get n < 7.3 • 10 14 log n log 2 (2n) and so n < 7.2 • 10 19 . We can easily see that for the two possible values of max{log(2n), 21/2}, n < 7.2 • 10 19 . All the calculations done so far can be summarized in the following lemma. Lemma 3.2. If (n, m, a) is a solution in positive integers of (1.1) with conditions n > m and n > 200, then inequalities a ≤ n + 2 < 1.2 × 10 20 hold. On solutions of the Diophantine equation L n + L m = 3 a Reducing of the bound on n Dividing across inequality (3.3) : 0 < a log 3 -n log α < 3 α n-m by log α, we get 0 < aγ -n < 7 α n-m ; where γ :

Furthermore, a

 a M := max {a i |i = 0, 1, ..., 42} = 161 Now applying Lemma 2.11 and properties of continued fractions, we obtain|aγ -n| > 1 (a M + 2)a . (4.2)Combining equation (4.1) and (4.2), we get1 (a M + 2)a < |aγ -n| < 7 α n-m =⇒ 1 (a M + 2)a < 7 α n-m =⇒ α n-m < 7 • (161 + 2)a < 1.3692 • 10 23 .Applying log above and divide by log α, we get :(n -m) ≤ log (7 • 163 • a) log α < 111.To improve the upper bound on n, let consider z := a log 3 -n log α -log ρ(u) where ρ = 1 + α -u . (4.3) From (3.7), we have |1 -e z | < 2 α n . (4.4)

hence 0 < a log 3 -

 3 n log α -log ρ(n -m) < 2α -n and by diving above inequality by log α 0 < a log 3 log α -n -log ρ(n -m) log α < 5 • α -n . (4.5) Taking, γ := log 3 log α , µ := -log ρ(n -m) log α , A := 5, B := α, inequality (4.5) becomes 0 < aγ -n + µ < AB -n .

  a 1 , a 2 , ......] = [1, 2, 3, 1, 1, 2, 3, 2, 4, 2, 1, 11, 2, 1, 11, ......]

Pagdame Tiebekabe and Ismaïla Diouf

Since γ is irrational, we are now ready to apply lemma 2.10 of Dujella and Pethö on (4.5) for n -m ∈ {1, ..., 111}.

Since a ≤ 1.2 × 10 20 from lemma 3.2, we can take M = 1.2 × 10 20 , and we get n < log(Aq/ε) log B where q > 6M and q is the denominator of the convergent of the irrational number γ such that ε := ||µq|| -M ||γq|| > 0.

With the help of SageMath, with conditions z > 0, and (n, m, a) a possible zero of (1.1), we get n < 112 which contradicts our assumption n > 200. Then it is false.

• Case 2 : z < 0

Since n > 200, then 2 α n < 1 2 . Hence (4.4) implies that |1 -e |z| | < 2. Also, since z < 0, we have

Replacing (4.3) in the above inequality and dividing by log 3, we get:

In order to apply lemma 3.2 on (4.6) for n -m ∈ {1, 2, ..., 111}, let's take again M = 1.2 × 10 20 . With the help of SageMath, with conditions z < 0, and (n, m, a) a possible zero of (1.1), we get n < 111 which contradicts our assumption n > 200. Then it is false. This completes the proof of our main result (Theorem 3.1).

Acknowledgement

The author is thankful to the referee for his valuable suggestions which improved the presentation of the paper. The authors also thank the professor Maurice Mignotte for his remarks and diponibility.

This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.