Student Member, IEEE Florian Requena

Member, IEEE Nicolas Barbot

Member, IEEE Darine Kaddour

Senior Member, IEEE Etienne Perret

Wireless Complex Permittivity Measurement Using Resonant Scatterers and a Radar Approach

Keywords: Complex permittivity, Radar, Resonant, Scatterer, Wireless measurement

In this paper, a method to characterize complex permittivity of dielectric is presented. The back-scattered signal from a resonant scatterer placed in contact with the dielectric is used to estimate the dielectric properties. The proposed method was tested in simulation and validated in practice using different dielectric samples and different dielectric thicknesses. This method is wireless, non-destructive, with no restriction on the sample thickness and is done using a VNA and an antenna. Discussions on the geometry of the resonator as well as the calibration step is proposed in order to improve the sensing capability of the approach. Monte-Carlo simulation has been performed to define a confidence interval for the values extracted with the proposed approach in the range 1 to 3.5 for permittivity and 0 to 0.2 for tan δ with a SNR of 20dB. For example, a permittivity εr = 3.54 ± 0.06 and tan δ = 0.0024 ± 0.003 has been measured for Rogers RO4003C and εr = 2.31 ± 0.05 and tan δ = 0.004 ± 0.002 for Duroid RT5880 with different thicknesses. It is also shown in simulation that the approach is compatible with materials having loss tangents up to 0.5, and real permittivity up to 10.

I. INTRODUCTION

M ICROWAVE sensors interest has increased over the last decades. Various sensors able to measure quantities such as temperature [START_REF] Requena | Thermal modeling of resonant scatterers and reflectometry approach for remote temperature sensing[END_REF], humidity [START_REF] Feng | Low-cost printed chipless rfid humidity sensor tag for intelligent packaging[END_REF], gas [START_REF] Yang | A novel conformal rfid-enabled module utilizing inkjet-printed antennas and carbon nanotubes for gas-detection applications[END_REF], strain [START_REF] Thai | Novel design of a highly sensitive rf strain transducer for passive and remote sensing in two dimensions[END_REF] without batteries or electronic chips have been published. This wireless approch based on radio-frequency (RF) waves caught the curiosity for sensor applications due to its low-profile (often planar and single layer sensors), its accuracy, its price and finally its infinite life-time of operation due the to absence of electronic parts. The RF waves also provide advantages such as wireless measurements that allow the reading of multiple sensors at the same time, in realtime, even with obstacles [START_REF] Requena | Chipless RFID temperature and humidity sensing[END_REF]. Such RF approaches have also been developed to do metrology. We can cite for example the characterization of the materials thermal dilatation [START_REF]Contactless characterization of metals' thermal expansion coefficient by a free-space rf measurement[END_REF] or the complex permittivity [START_REF] Alahnomi | Review of recent microwave planar resonator-based sensors: Techniques of complex permittivity extraction, applications, open challenges and future research directions[END_REF].

Concerning the complex permittivity measurements, numerous works can be found in the litterature [START_REF] Krupka | Frequency domain complex permittivity measurements at microwave frequencies[END_REF], [START_REF] Alahnomi | Review of recent microwave planar resonator-based sensors: Techniques of complex permittivity extraction, applications, open challenges and future research directions[END_REF], [START_REF] Kiani | Microwave sensor for detection of solid material permittivity in single/multilayer samples with high quality factor[END_REF], [START_REF] Massoni | Enhanced cavity sensor in SIW technology for material characterization[END_REF]. These methods can be divided in two main categories Manuscript received X; revised X; accepted X. Date of publication X; date of current version X. This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No 772539). This work is also supported by Univ. Grenoble Alpes. (Corresponding author: Requena Florian.). The authors are with Univ. Grenoble Alpes, Grenoble INP, LCIS, F-26000 Valence, France. E. Perret is also with Institut Universitaire de France, Paris, France.

: resonant and non-resonant approaches. In non-resonant approaches, coaxial measurements are commonly used and standardized [START_REF] Ute | Mesure de la permittivite et de la permeabilite de materiaux homogenes et isotropes a pertes dans le domaine des micro-ondes. methode de mesure en guide coaxial circulaire[END_REF]. The coaxial method consists in measuring the transmission and reflection coefficients of a coaxial transmission line filled with the dielectric under-test [START_REF] Nicolson | Measurement of the intrinsic properties of materials by time-domain techniques[END_REF], [START_REF] Baker-Jarvis | Improved technique for determining complex permittivity with the transmission/reflection method[END_REF]. The transmission/reflection principle is also transposed to other techniques such as waveguides [START_REF] Bakhtiari | Open-ended rectangular waveguide for nondestructive thickness measurement and variation detection of lossy dielectric slabs backed by a conducting plate[END_REF] or free-space measurements [START_REF] Shimabukuro | A quasioptical method for measuring the complex permittivity of materials[END_REF]. These techniques are simple to implement, work on wide frequency band but the major drawback is their low accuracy, especially on the losses extraction for lowloss dielectrics. On the other hand, resonant methods allow to have higher accuracies and to measure lower losses but are restricted in the frequency response. Cavity measurements [START_REF] Li | Precise calculations and measurements on the complex dielectric constant of lossy materials using tm/sub 010/cavity perturbation techniques[END_REF], [START_REF] Dmowski | Contactless measurement of silicon resistivity in cylindrical te01n mode cavities[END_REF] are widely used for dielectric characterization. Besides, various resonator topologies have been published in the litterature. We can cite, open resonator [START_REF] Cullen | The accurate measurement of permittivity by means of an open resonator[END_REF], [START_REF] Hirvonen | Measurement of dielectrics at 100 ghz with an open resonator connected to a network analyzer[END_REF] and dielectric rod resonators short circuited at both ends by two parallel conducting plates [START_REF] Hakki | A dielectric resonator method of measuring inductive capacities in the millimeter range[END_REF], [START_REF] Kobayashi | Microwave measurement of dielectric properties of low-loss materials by the dielectric rod resonator method[END_REF]. For the solid dielectric materials which are exclusively dealt with in this paper, a major problem is the accurate machining of a specimen of the material to fit closely into the resonator or waveguide.

In the recent years, planar microstrip resonators using the under-characterization material as a substrate were introduced in [START_REF] Lobato-Morales | Wireless sensing of complex dielectric permittivity of liquids based on the RFID[END_REF], [START_REF] Wiltshire | Passive split ring resonator tag configuration for RFID-based wireless permittivity sensing[END_REF], [START_REF] Perret | Permittivity characterization based on radar cross measurements[END_REF]. This technique allows a wireless measurement based on a radar principle and allows to avoid the machining drawback. While in [START_REF] Lobato-Morales | Wireless sensing of complex dielectric permittivity of liquids based on the RFID[END_REF], the RF access lines conventionally used to connect to a VNA [START_REF] Krupka | Frequency domain complex permittivity measurements at microwave frequencies[END_REF] were replaced by antennas, [START_REF] Perret | Permittivity characterization based on radar cross measurements[END_REF] and [START_REF] Wiltshire | Passive split ring resonator tag configuration for RFID-based wireless permittivity sensing[END_REF] present an approach where only a resonant target is present without any antenna. In [START_REF] Wiltshire | Passive split ring resonator tag configuration for RFID-based wireless permittivity sensing[END_REF], the resonant target (open metal ring on a known dielectric substrate) is realized on PCB. Here, the material to be characterized is a small dielectric slab of a few mm length, positioned in the opening of the ring. This method offers the advantages of being easy to implement and low-cost like wireless test-benches (only one antenna and a VNA are needed). In addition, it offers advantages (real-time and accurate measurements) making it a potential solution for dielectric characterization. Contrary to [START_REF] Hakki | A dielectric resonator method of measuring inductive capacities in the millimeter range[END_REF], [START_REF] Kobayashi | Microwave measurement of dielectric properties of low-loss materials by the dielectric rod resonator method[END_REF] the sample under test does not need to be precisely positioned in the test bench (e.g. the distance between the antenna and the resonator can be changed easily). In these works, the permittivity [START_REF] Perret | Permittivity characterization based on radar cross measurements[END_REF], or the complex permittivity [START_REF] Lobato-Morales | Wireless sensing of complex dielectric permittivity of liquids based on the RFID[END_REF], [START_REF] Wiltshire | Passive split ring resonator tag configuration for RFID-based wireless permittivity sensing[END_REF] is directly linked to the resonance impacting both its frequency and its attenuation. However in [START_REF] Lobato-Morales | Wireless sensing of complex dielectric permittivity of liquids based on the RFID[END_REF], [START_REF] Wiltshire | Passive split ring resonator tag configuration for RFID-based wireless permittivity sensing[END_REF], measurements or simulations are used to fit a model which describes the resonance frequency behavior.

In this paper, the complex permittivity is related to the resonance with a theoretical approach and an analytical formula is obtained. In addition, the characterization frequency band, can be increased by using different resonators operating at different frequencies. As in [START_REF] Perret | Permittivity characterization based on radar cross measurements[END_REF], the approach is based on the use of an independent metallic resonator which is attached to the dielectric plate to be measured and whose thickness is assumed to be known. However, here a more general approach is introduced in order to determine the dielectric losses. Compared to [START_REF] Wiltshire | Passive split ring resonator tag configuration for RFID-based wireless permittivity sensing[END_REF], the sensitivity is maximized by using no other dielectric than the one to characterize. Besides, there is no need to machine the dielectric : its dimensions should largely cover the metallic resonator.

In Section II the equations relating the resonance to the complex permittivity will be introduced. Section III focuses on the complex permittivity extraction from radar measurements. Section IV and V present simulations and measurements of several samples as well as discussions on the accuracy and sensitivity of the proposed approach. Finally, Section VI will conclude the paper.

II. COMPLEX RESONANCE FREQUENCY

The principle of the measurement is illustrated in Fig. 1a, which shows the measurement method based on the acquisition of a backscattered signal from a resonator in contact with the dielectric to be characterised. In this study the loop resonator shown in Fig. 1b will be used.

Using the Singularity Expansion Method (SEM), it can be shown that in the time domain, the signal back-scattered u(t) by a resonator can be written as an exponentionally damped sinusoidal as follows :

u(t) = Ae -σ(t-2τ ) cos(ω(t -2τ ))Γ(t -2τ ) ( 1
)
where A is the amplitude of the back-scattered signal, Γ is the Heavyside function and τ the propagation constant. This signal is illustrated Fig. 2. Let define the complex resonance frequency s = σ + jω to analyze the radar response of a resonant target in terms of damping factor σ and angular resonant frequency ω. The back-scattered signal can be rewritten as :

u(t) = A × Re e -s(t-2τ ) × Γ(t -2τ ), (2)
where Re defines the real part. If a simple loop resonator is used (as illustrated in Fig. 1) for our radar target, its resonance frequency f r is defined by [START_REF] Rance | Contactless characterization of coplanar stripline discontinuities by rcs measurement[END_REF]:

f r = c 2L 1 + ε r -1 2 q , ( 3
)
where c is the speed of light in vacuum, L the length of the resonant scatterer, q the filling factor which is a coefficient to take into account the support thickness [START_REF] Chen | Characteristics of coplanar transmission lines on multilayer substrates: Modeling and experiments[END_REF] and ε r the permittivity of the dielectric under-test. For this reason, the resonance frequency of a resonator placed on a lossless dielectric is associated to the variable s r by : Even in the lossless case σ r is linked to metallic losses and radiation losses so it is not zero. When a dielectric presents RF losses, its permittivity can be written as ε = ε r (1j tan δ), where tan δ is the dielectric loss tangeant, hence the complex resonance frequency can be introduced :

s r = σ r + jω r = σ r + j2π c 2L 1 + ε r -1 2 q . ( 4
)
f d = c 2L 1 + ε r (1 -j tan δ) -1 2 q , (5)
which gives the expression of the complex resonance frequency in the case of electrical loss s d :

s d = σ r + jBe - j 2 tan   tan δqε r 2 + q(ε r -1)   , (6)
where

B = ω 0 1 + ε r -1 2 q 1 + tan δqε r 2 + q(ε r -1) 2 1/4 .
Note that the subscript d is used hereafter to designate expressions where the losses of the dielectric to be characterized are taken into account. For low losses, (tan δ ≪ 1) which is usually the case for RF substrates, the complex resonance frequency f d can be written :

f d ≃ F 0 1 - j 2 X - 3 8 X 2 , (7)
where

F 0 = c 2L 1 + ε r -1 2 q = f 0 1 + ε r -1 2 q and X = tan δqε r 2 + q(ε r -1)
. Therefore, the variable s d at the complex resonance frequency f d is now given by :

s d = σ d + jω d = σ 0 + 1 2 W 0 X + jW 0 1 - 3 8 X 2 , ( 8
)
where W 0 = 2πF 0 . After identification, the damping factor and frequency at resonance for a lossy dielectric (σ d , ω d ) can be expressed by :

                   σ d = σ 0 + ω 0 2 1 + ε r -1 2 q
tan δqε r 2 + q(ε r -1)

ω d = w 0 1 + ε r -1 2 q 1 - 3 8 tan δqε r 2 + q(ε r -1) 2 (9a) (9b)
.

Note that in (9b) only ε r and tan δ are unknown. Indeed, (σ 0 , ω 0 ) and (σ d , ω d ) are the damping factor and the resonance frequency measured for a loop resonator with no support and with the dielectric under-test respectively. Note that the length L does not affect the measurement. Also, different lengths can be used to charaterize the losses at different resonance frequencies. The coefficient q can be directly calculated using [START_REF] Chen | Characteristics of coplanar transmission lines on multilayer substrates: Modeling and experiments[END_REF] or obtained through simulations as explained later in Section IV. It is possible from the measurement of the backscattered signal of a resonator (see Fig. 2) to extract the values of damping factors and resonance frequencies. Several techniques allow the extraction of these coefficients from the backscattered electromagnetic signature of a resonant scatterer. Approaches applied to the time domain representation of the signal [START_REF] Sarkar | Using the matrix pencil method to estimate the parameters of a sum of complex exponentials[END_REF] or to a frequency domain representation [START_REF] Ali | Extraction of aspect-independent parameters using spectrogram method for chipless frequency-coded rfid[END_REF] are both considered in the litterature. Fig. 2 presents an example of time domain back-scattered signal (in simulation) obtained from the loop illustrated in Fig. 1. In this figure we can see both the backscattered signal obtained by simulation and the signal reconstructed from the extraction of the damping factors and the resonance frequencies based on [START_REF] Sarkar | Using the matrix pencil method to estimate the parameters of a sum of complex exponentials[END_REF].

For a rectangular loop of this type, there is a trade-off between the RCS level and the quality factor value. This tradeoff is primarily related to the width of the gap g between the two larger arms of the rectangular loop. The smaller the gap, the higher the quality factor and the lower the RCS. An optimisation on CST allowed to obtain a good compromise where the objective remains however to have a quality factor above 100 in air.

III. PERMITTIVITY EXTRACTION

Equation (9b) can be re-written as :

           tan δ = 2(σ d -σ 0 ) 1 + ε r -1 2 q ω 0 2 + q(ε r -1) qε r ω 1 + ε r -1 2 q = 1 - 3 2 σ 2 1 + ε r -1 2 q , ( 10
) where ω = ω d ω 0 and σ = σ d -σ 0 ω 0 . By letting Y = 1 + ε r -1 2
q, the second equation can be expressed as a quadratic equation aY 2 + bY + c with :

       a = 3 2 σ 2 b = ω c = -1 . ( 11
)
The real positive solution Y is :

Y = -ω + ω 2 + 6σ 2 3σ 2 . ( 12
)
Then the real part of the permittivity ε r can be found using [START_REF] Nicolson | Measurement of the intrinsic properties of materials by time-domain techniques[END_REF] with :

ε r = 1 + 2 Y 2 -1 q = 1 + 2 q   -ω + ω 2 + 6σ 2 3σ 2 2 -1   (13)
and the losses can be found using (9b) and ( 13) with :

tan δ = 4σ -ω + ω 2 + 6σ 2 3σ 2 5/2 q + 2 -ω + ω 2 + 6σ 2 3σ 2 -1 2 . ( 14
)
These formulas are used to extract ε r and tan δ. The dielectric characterization requires 2 measurements for the loop resonator : the first with no support and the second with the dielectric under test.

IV. SIMULATIONS

Simulations have been carried out using CST MW to validate the introduced equations. A farfield E-probe with the Time domain solver is used. The loop resonator configuration of Fig. 1 has been used. As previously explained, for a rectangular loop of this type, there is a trade-off between the RCS level and the quality factor value. An optimisation on CST allowed to obtain a good compromise. Fianl dimensions are L = 50mm, w = 1.4mm and g = 2mm. The metal is 1mm thick. The loop is placed on the dielectric material to be characterized with permittivity ε r and loss tangent tan δ. The dielectric height is 1mm so q ≃ 0.58 based on [START_REF] Chen | Characteristics of coplanar transmission lines on multilayer substrates: Modeling and experiments[END_REF]. The excitation is a plane wave polarized along the ⃗ y-axis (see Fig. 1b). The probe used to obtain the backscattered signal is placed 1 meter away from the resonator. The simulated back-scattered E-fields for different values of ε r and tan δ are plotted in Fig. 3. These simulations show the impact of the variation of the dielectric parameters on both the resonance frequency and the damping factor.

Based on these simulations, the Matrix Pencil method [START_REF] Sarkar | Using the matrix pencil method to estimate the parameters of a sum of complex exponentials[END_REF] is used to extract the complex natural resonance (CNR) s = σ + jω. For each configuration the resonance frequency f = ω/2π as well as the damping factor σ are plotted in Fig. 4. The correspondence betewen the values of the complex permitivity and the number (noted "Run ID") associated to the simulation is given in Table . I. We can see that resonance frequency decreases with an increase of the real and also of the imaginary part of the permittivity. The damping factor mostly increases with the imaginary part of the permittivity (losses). Fig. 4 also presents results obtained with (9b) which show a good agreement with the simulations.

The study of the error obtained from (9b) will be realized in the measurement section. Indeed in simulation, even if the structure is relatively simple, the error will be directly linked to the models used in the EM simulator to take into account the losses, which is not what we seek to study in this article.

Based on the values of the simulated frequency resonance and damping factor, the complex permittivity can be extracted using ( 13) and [START_REF] Bakhtiari | Open-ended rectangular waveguide for nondestructive thickness measurement and variation detection of lossy dielectric slabs backed by a conducting plate[END_REF]. Estimated ε r and tan δ are plotted in Fig. 5. Again, we can notice that the extracted values are in good agreement with the simulated ones.

A discussion will be made concerning the sensitivity and accuracy of the proposed method based on the resonant scatterer. As shown in (9b), the only factor that impacts the results is the coefficient q. Indeed, the higher the value of q, the larger the shifts in the signal amplitude or on the resonance frequency. Thus better sensibility on the complex permittivity extraction can be expected. To increase q, the loop geometry as well as the dielectric under-test thickness should be considered when designing the resonator [START_REF] Chen | Characteristics of coplanar transmission lines on multilayer substrates: Modeling and experiments[END_REF]. A simulation with two different gap values for the loop is presented in Fig. 6. We can see that a smaller gap induces a higher value for q and so higher shifts in the resonance frequency is observed. The study of the variation of the resonance frequency as a function of q, more exactly the computation of d(ω r /ω 0 )/dq by derivating (9b) [see Fig. 8] allows to show analytically that the resonance frequency of the resonator on the dielectric varies the more when the value of q is high. This explains why the error obtained is smaller for thick substrate where q is large in this case. Similarly, the greater the thickness of the substrate, the lower the resonance frequency and therefore the greater the frequency variation compared to the case without the dielectric. Measuring this larger offset leads to less error. Futhermore, Fig. 7 presents the simulated filling factor q for different dielectric heights and different resonator metal thicknesses. We should notice that [26, eq. ( 21)] offers a good agreement with simulations for very thin metal (the metal thickness is considered infinitely thin). When the resonator's metal is thicker, [26, eq. ( 21)] is no more valid to determine q with accuracy. For this reason, extracted values of q obtained from simulations and shown in Fig. 7 will be used in the section V for dielectric characterization. Contrary to the classical cavity method, this approach does not require thin dielectric sample to work. Indeed, as shown in Fig. 7, the thicker the dielectric, the larger the value of q, which improves the final estimation of the complex permittivity.

ε = 1 ε = 1.5 ε = 2 ε = 2.5 ε = 3 ε = 3.5
Run ID tan δ tan δ estimated ( 14) Simulated tan δ Fig. 5. εr and tan δ estimated with ( 13) and ( 14) respectively. The different values used for the study and corresponding to a ID number are shown in Table I.

V. MEASUREMENTS

The proposed approach will be validated by measurements using different samples. The different samples and dielectric thicknesses evaluated in practice are given in Table. II. The "Red" test sample was characterized using the cavity method for complex permittivity measurements (the Damaskos, Inc. Model 08 Thin Sheet Tester that measures the dielectric properties of low loss materials over the approximate band of 800-4000 MHz in a non-destructive manner).

The following protocol was used for the measurements : firstly, the loop resonator is measured in the air using a monostatic configuration inside an anechoic chamber (see Fig. 1 and Fig. 9). The VNA 5222A by Agilent was used. The source power of VNA is equal to 0 dBm. The frequency sweep ranging from 2 to 3 GHz with 4001 points is considered. A mono-static configuration with Satimo (QH800) quad ridged [24, eq. ( 21)]

ε = 2 ε = 3 ε = 4 ε = 5
Fig. 7. Filling factor q as a function of the dielectric height and the metal thickness. × markers correspond to a metal thickness of 0.01mm, + markers to a thickness of 0.5mm and ⃝ markers to 1mm. □ is the q calculated using [26, eq. ( 21)].

open boundary antennas (0.8-12 GHz) is used. We have used a dual linear antenna for this measurement, however any simpler (linear polarization) and less expensive (e.g. a Vivaldi antenna realized on PCB) would achieve the same performance for this application. Indeed, to keep the same SNR, with a less directive antenna, it is sufficient to decrease the antenna-resonator distance. Compared to [START_REF] Perret | Permittivity characterization based on radar cross measurements[END_REF] where a bistatic configuration was used for the measurement, the results presented here were obtained with a mono-static configuration, which is simpler to implement and for which it is shown to be sufficient to achieve the required degree of accuracy for the introduced extraction. The loop resonators were obtained by cutting a 0.5mm thick metal plate with a laser. Dimensions are L = 50.82mm, w = 1.43mm and g = 2.07mm. In the case, high purity copper metal has been chosen for the fabrication (more than 99% purity) [29].

Tape was used to suspend the loop in the air (see Fig. 9a) to be as close as possible to a free-space condition. The tape was also used to attach the loop to the samples as can be seen in Fig. 9b. Indeed, the use of tape for measurement is very significant in minimising the gap between the dielectric and the loop. This is especially true since these two elements are never perfectly planar (especially the metallic loop) and therefore the tape helps to keep them in touch during the measurement. The way in which the tape was used to clamp the loop was studied both in simulation and in practice to have as little impact as possible on the backscattered signal. The configuration chosen is shown in Fig. 9a and provides the best compromise between a very low impact on the resonant frequency, damping factor and a very good maintenance of the loop on the dielectric. It is however important to note that to consider as much as possible the presence of the tape in the method, we used tape both for the measurement in air (Fig. 9a) and when the loop is placed on the dielectric. This is a way to reduce the effect of tape in the measurement method introduced.

Matrix Pencil Method [START_REF] Sarkar | Using the matrix pencil method to estimate the parameters of a sum of complex exponentials[END_REF] is used on the S-parameters to evaluate (σ 0 , ω 0 ). Secondly, the loop resonator was taped to the sample under-test as illustrated in Fig. 9b. Matrix Pencil is used once again on the S-parameters to evaluate (σ r , ω r ). Finally, ( 13) and ( 14) are used to estimate the complex permittivity of the sample. The value of q is obtained based on the results presented in Fig. 7 for the corresponding dielectric thickness and for the 0.5mm metal thickness resonator used in practice. An example of measured S-parameters is given in Fig. 10 for different substrates. For each of them, the extracted dielectric parameters are given in Table II. We can see that the estimated complex permittivity is close to the provider's informations for the different samples and different dielectric thicknesses. There is only a difference in the losses of the Duroid RT5880. Indeed, the measured losses for the Duroid RT5880 (both heights) using the proposed approach grant losses 4 times larger at 2.5GHz than the ones given by the provider at 10GHz. Although some of the difference may be attributable to the difference in frequencies, it is also possible that the limitations of the approach to the minimum loss tangents that can be measured can be observed here. We were also interested in evaluating the maximum loss tangent values that the method can extract. Indeed, this method relies on the extraction of the resonance frequency and the damping factor, and this extraction will be impacted by a too high loss tangent value. In simulation we have observed with the loop used that it becomes difficult to characterise dielectrics with loss tangents greater than 0.4. This shows that in order to reach higher values, it is necessary to work on the design of the loop resonator, or even to opt for another resonator.

It is also important to notice that these values are frequency dependent (especially tan δ in this frequency band). The proposed method allows to measure the complex permittivity at the resonance frequency of the scatterer when it is placed on the sample to characterize. For this reason, designing different resonator lengths is a solution to determine the complex permittivity at multiple frequencies. Scatterers used in the paper were designed to have their fundamental resonance frequency close to 3GHz in the air. Now that the approach is validated in practice, a second approach is presented in order to correct systematic errors. When the resonator is taped to the dielectric, a small air gap could always be present in between the resonator and the dielectric changing the effective permittivity seen by the resonator. Also, tape induced a constant frequency shift due to its presence. When resonators are taped several times to the same dielectric, we notice that the resonance frequency does not vary a lot meaning that the air gap (with tape) is constant between measurements. The improvement proposed here is to use a known dielectric for calibration to estimate the "in-air" resonator values. Then the estimated "in-air" values are used to characterize a second dielectric under-test. For a known dielectric and so its (ε cal , tan δ cal ), we can write :

                     ω 0 = w cal 1 + ε cal -1 2 q 1 - 3 8 tan δ cal qε cal 2 + q(ε cal -1) 2 σ 0 = σ cal + ω 0 2 1 + ε cal -1 2 q tan δ cal qε cal 2 + q(ε cal -1)
. [START_REF] Shimabukuro | A quasioptical method for measuring the complex permittivity of materials[END_REF] For this reason, the initial measurement in air can be replaced by a measurement on a known dielectric and (15) can be used to determine (σ 0 , tan δ 0 ). By using this procedure to estimate the RT5880 using the RO4003C (both with a thickness of around 0.8mm) as a calibration dielectric permits to measure ε RT = 2.32 and tan δ RT = 0.003 at 2.6GHz hence improving a little the results.

Note that in such a case the two dielectrics don't need to have the same thickness. Indeed, the value corresponding to the measurement of the loop and the dielectric of reference is computed using [START_REF] Shimabukuro | A quasioptical method for measuring the complex permittivity of materials[END_REF] with the filling factor q corresponding to this dielectric and so its thickness. Then the permittivity is estimated with ( 13) and ( 14) with the filling factor of the dielectric under-test.

VI. DISCUSSIONS

The resonance frequency and damping factor are related to the geometry and materials constituting the resonator. Indeed, from a theoretical point of view, and this is also what makes this method so interesting, the quantities involved in the extraction (resonance frequency and quality factor) are aspect-independent parameters [START_REF] Ali | Extraction of aspect-independent parameters using spectrogram method for chipless frequency-coded rfid[END_REF], which means that they are not linked to the measurement bench (such as the gain of the antennas, the distance, the orientation of the antennas...). It is therefore possible to carry out measurements at two different distances (measurement without and with dielectric), but this is of very limited interest in practice. Note that this measurement can easily be implemented in controlled environment for metrology measurements. In this respect, the maximum distance that can be used with this technique will depend on the environment and the measurement time (linked in particular to the averaging used) and the precision of the measurement equipment. However, a notable limitation of the approach occurs at the level of dielectrics with significant losses. Indeed, we could see in simulation (not shown in the paper) that for loss tangent higher than 0.5, it is no longer possible to extract the quality factor. This means that it is no longer possible to access the material losses. As far as the range of values on the real part of the permittivity is concerned, we did not observe such limitations. Indeed, we were able to test that a material with a permittivity of 10 was perfectly compatible with the introduced approach.

In practice, if the distance between the resonator and the antenna increases, the SNR will decrease, so the estimation of the poles and then the complex permittivity will be impacted. Monte-Carlo (MC) simulation for a SNR of 20dB on the Sparameters is shown in Fig. 11. Noise was added on the time response signal of the simulated loop on a lossy dielectric substrate. The simulated permittivity and losses range respectively from 1 to 3.5 and 0 to 0.1. This simulates the effect on complex permittivity extraction when the distance between the antenna and the resonator is increased. We can see in these numerical simulations shown in Fig. 11 the impacts in terms of errors and uncertainties on the extracted permittivity.

We can see that a SNR of 20dB does not introduce errors or uncertainties sufficient to modify the extraction. However, as expected, it will introduce slight uncertainties on the loss tangent. By lowering the SNR to 5dB, similar results were obtained on the extracted permittivity. The measurement of the SNR in practice and the use of the presented MC simulation can allow the user to estimate the uncertainties on his measurement setup (noise, distance for antenna-resonator,...).

Sensing is improved when the estimation is robust to the noise, which is illustrated by the MC simulations presented Fig. 11. Sensing is also improved with higher variations of the measurand (higher variation usually means peaks easier to measure but also less correlated to noise). These variations of the resonance frequency in term of sensibility can be compared to others works [START_REF] Kiani | Microwave sensor for detection of solid material permittivity in single/multilayer samples with high quality factor[END_REF]. Note that the present manuscript does not try to improve the sensitivity S [30, eq. ( 3)] but is rather on the theory and setup used to measure the complex permittivity. However, in Fig. 6, a simulation is made to illustrate how the

ε = 1 ε = 1.5 ε = 2 ε = 2.5 ε = 3 ε = 3.5
Run ID Extracted tan δ Fig. 11.

Simulated complex permittivity in red and extracted complex permittivity in blue with a MC simulation with a SNR of 20dB. The simulated permittivity and losses range respectively from 1 to 3.5 and 0 to 0.1. design of the loop can be improve to obtain higher values of S. In this simulation and for a gap g=0.5mm (plain line), a value of S = (f 1f 2 ) f 1 ∆ε = 8.19% is obtained. We can see that this design introduced a sensitivity 2.5 times higher than the most sensitive permittivity sensor presented in [START_REF] Kiani | Microwave sensor for detection of solid material permittivity in single/multilayer samples with high quality factor[END_REF]. Note also that, the present work allows in addition to measure the losses of the dielectric which is not done in [START_REF] Kiani | Microwave sensor for detection of solid material permittivity in single/multilayer samples with high quality factor[END_REF]. Sensitivities S obtained in measurements are given in Table II. A comparison of sensitivities S of different works is given in Table III. Table II also illustrates the impact of the resonator geometry already discussed in Section IV. Indeed, we can see that considering one dielectric, the sensitivity S increases with the thickness of the sample under-test as q increases. Lastly, in [START_REF] Requena | Thermal modeling of resonant scatterers and reflectometry approach for remote temperature sensing[END_REF], section X, it was shown that different resonator topologies can be used to improve even more this sensibility. The dipole over a ground plane shown in [START_REF] Requena | Thermal modeling of resonant scatterers and reflectometry approach for remote temperature sensing[END_REF] can be used to obtain even higher sensitivity but it was not presented in the current paper since its utilization as a complex permittivity sensor seems more difficult to implement. The dipole resonator needs to be printed on the dielectric under test while the loop can be manually placed as it is done in the manuscript.

The MC simulation allows to define a confidence interval in the complex permittivity values extracted with the proposed approach. Indeed Fig. 12 presents the error between simulated values (entered in CST) and extracted values (with the introduced approach) for different simulated complex permittivity values. It is interesting to note that this error mainly characterises the accuracy of the model and indeed the values obtained here are very close to the deviation that could be calculated between the values entered on CST and extracted by the model presented in Fig. 5 (in this case no noise has been added contrary to the results in Fig. 11). Thus, further work on the model (for certain permittivity or loss ranges, for example through a calibration), could further improve the accuracy of the approach. It is also interesting to consider the uncertainties obtained through the MC simulation (see Fig. 11). Indeed, as can be seen in this figure, this uncertainty (for a confidence level of one standard deviation, i.e. approximately 68%) is very low compared to the errors shown in Fig. 12. This shows that the noise added in the MC simulation has very little effect on the value extracted by the approach, which shows a very good accuracy. Taking these elements into account, we can say that the real value (entered in CST) is located (in the worst-case scenario) in a confidence interval which can be estimated based on the errors plotted in Fig. 12 and the uncertainty directly computed with the MC simulation. As the uncertainty is very small compared to the error, a confidence interval equal to +/-the error can be used here to give an idea of the accuracy that can be expected with this approach.

We note also that the results obtained in terms of measurement error are similar to those described in [START_REF] Orloff | Dielectric characterization by microwave cavity perturbation corrected for nonuniform fields[END_REF] where complex permittivity is sensed using a cavity method. Indeed, in [START_REF] Orloff | Dielectric characterization by microwave cavity perturbation corrected for nonuniform fields[END_REF], epoxy was characterized with a permittivity of 2.93±0.11 and losses tangent of 0.028 ± 0.002. We can notice that the proposed approach allows to have similar results on the losses (also ±0.002 in this work). The same applies to permittivity. The measurement results of the samples are collected in Table IV where the confidence interval has been added for each value in order to give a more precise idea on the quality of the results obtained.

VII. CONCLUSION

In this paper, a method based on a radar approach to measure the materials' complex permittivity is introduced. A loop resonator is used to derivate the complex permittivity expression from back-scattered signals. Simulations and measurements have been realized to validate the proposed non destructive method on different dielectric slabs in the frequency band 2-3 GHz. Discussions on the resonator and dielectric geometries have been done in order to improve the accuracy of the extraction. Also, an additional calibration step using already known dielectric has been proposed and validated in practice to improve the estimations.

Fig. 1 .

 1 Fig. 1. a) Principle of the measurement of the scatterer. b) Loop resonator considered in this study. The support is the dielectric under-test defined by ε = εr(1 -j tan δ).

Fig. 2 .

 2 Fig. 2.Time domain back-scattered signal from a loop resonator in simulation.

Fig. 3 .

 3 Fig. 3. Simulated back-scattered E-field in amplitude for εr = [1 : 0.5 : 3.5] and tan δ ∈ [0, 0.005, 0.05, 0.2] for the loop resonator of Fig. 1 impringed by a plan wave. Dielectric height is 1mm.

εεFig. 4 .

 4 Fig. 4. Comparision between simulations and equations : a) Damping factor b) resonance frequency.

ε = 1 ε

 1 = 1.5 ε = 2 ε = 2.5 ε = 3 ε = 3

Fig. 6 .

 6 Fig.6. Influence of the gap g of the loop on the extraction of the complex permittivity: gap g = 0.5mm (q = 0.77) [plain line] and g = 2mm (q = 0.6) [dashed line]. The blue curves correspond to a permittivity of ε = 1 and the red ones to a permittivity of ε = 3.55 * (1 -j0.0021).

Fig. 8 .

 8 Fig.8. The study of the variation of the resonance angular frequency ω as a function of the filling factor q.

Fig. 9 .

 9 Fig. 9. Testbench used for the measurement. a) Initial measurement to evaluate (σ 0 , ω 0 ). b) Measurement of the "Red" test sample where the loop has been positioned over of the sample with tape.

Fig. 10 .

 10 Fig. 10. Measurement of the S 11 parameters for a loop resonator in air (blue) and on the different substrates.

ε = 1 ε

 1 = 1.5 ε = 2 ε = 2.5 ε = 3 ε = 3

ε 2 ε = 1 εFig. 12 .

 2112 Fig. 12. Error for a) real part and b) losses between simulated and extracted ones. The simulated permittivity and losses range respectively from 1 to 3.5 and 0 to 0.1.

TABLE I CORRESPONDENCE

 I BETWEEN SIMULATIONS "RUN ID" AND (εr, tan δ).

	Run ID	1 2	3	4	5	6	7	8	9 10	11	12	13	14	15	16	17 18	19	20	21	22	23	24
	εr	1 1	1	1	1.5 1.5	1.5	1.5 2 2	2	2	2.5 2.5	2.5	2.5 3	3	3	3	3.5 3.5	3.5	3.5
	tan δ	0 0.005 0.05 0.2 0	0.005 0.05 0.2 0 0.005 0.05 0.2 0	0.005 0.05 0.2 0	0.005 0.05 0.2 0	0.005 0.05 0.2

TABLE II COMPARISON

 II OF THE COMPLEX PERMITTIVITY OF THE SAMPLE GIVEN BY THEIR PROVIDER AND MEASURED BY THIS APPROACH

		Thickness (mm)	εr (provider)	tan δ (provider)	εr (cavity method)	tan δ (cavity method)	εr (this approach)	tan δ (this approach)	Sensitivity S (this approach)
	Rogers RO4003C	0.813 1.524	3.55 3.55	0.0021 @2.5GHz 3.72 0.0021 @2.5GHz 3.49	0.0029 @2.5GHz 3.54 0.0014 @3GHz 3.59	0.0024 @2.4GHz 0.0031 @2.2GHz	5.15% 6.45%
	Duroid RT5880	0.787 1.575	2.33 2.33	0.0012@10GHz 0.0012@10GHz	2.29 2.29	0.0018 @2.5GHz 2.31 0.0018 @2.5GHz 2.31	0.004 @2.6GHz 0.004 @2.5GHz	4.61% 5.94%
	Red	1.958	4.24	0.0173 @3.1GHz 4.25	0.018 @3.1GHz	4.27	0.012 @2.2GHz	10.71%

TABLE III COMPARISON

 III OF THE SENSITIVITY S OF DIFFERENT WORKS

	Frequency (GHz) Sensitivity S
	[32], [33] [34] [35] [9] This work 3 7.6 2.1 4.5 5.65	2.6% 2.7% 2.2% 3.25% 5.1% to 10.7%

ACKNOWLEDGMENT

The authors are thankful towards Selim Azzouni for his help with cavity measurements and to Nathalie Franck for her help in proofreading the paper.


Amélie David
email: adavid@ibisc.univ-evry.fr

Deciding ATL * Satisfiability by Tableaux

Keywords: Alternating-time temporal logic, ATL *, Automated theorem prover, Satisfiability, Tableaux

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

Introduction

The logic ATL * is the full version of the Alternating-time Temporal Logic introduced in [START_REF] Alur | Alternating-time temporal logic[END_REF] in order to describe open systems, that is systems that can interact with their environment. Thus ATL and ATL * are the multi-agent versions of the branching-time temporal logics CTL and CTL * . Indeed, in ATL and ATL * the environment is modelled by an extra agent e interfering with the system components (the remaining agents) who need to succeed their task no matter how e responds to their actions. ATL * is an important extension of ATL and ATL + (an intermediate logic between ATL and ATL * ) since it allows one to express useful properties such as fairness constraints. Such properties can be expressed only if nesting of temporal operators is possible, which is not the case in ATL and ATL + . It is worth noting that ATL + only permits Boolean combination of unnested temporal operators.

The problem studied in this paper is about deciding the satisfiability of ATL * formulae. Models for ATL * formulae are directed graphs called concurrent game structures where transitions between two states depend on the chosen action of each agent. In general, there exists two ways for deciding the satisfiability: using automata, as done in [8] or using tableaux; as we do here. In this paper, All proofs of lemmas, propositions and theorems, as well as complete examples can be found in the version with appendices at https://www.ibisc.univ-evry.fr/ ∼ adavid/ fichiers/cade15 tableaux atl star long.pdf.

we propose the first tableau-based decision procedure for ATL * , as well as the first implementation of a decision procedure for ATL * , which is also the first implementation of a tableau-based decision procedure for ATL + . We extend our procedure for ATL + [START_REF] Cerrito | Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic ATL+[END_REF] following the natural basic idea: separate present and future. However, this extension is not trivial since the separation into present and future is more subtle than for ATL + and needs to keep track of path formulae so as to be able to check eventualities. We think that our tableau-based decision procedure for ATL * is easy to understand and therefore also provides a new tableau-based decision procedure for CTL * which is conceptually simple. We prove that our procedure runs in at most 3EXPTIME, which is suboptimal (the optimal worst case complexity has been proved to be 2EXPTIME in [8]). However, we do not know of any specific cases where our procedure runs in 3EXPTIME, which leaves the possibility that it is optimal, after all.

This paper is organized as follows: Sect. 2 gives the syntax and semantics for ATL * . The general structure of the tableau-based decision procedure for ATL * that we propose can be found in Sect. 3 and details of the procedure in Sects. 4, 5 and 6. Theorems about soundness, completeness and complexity are given in Sect. 7 with their sketch of proof. The Sect. 8 is about the implementation of our procedure. The paper ends with some concluding remarks indicating also some possible directions of future research.

2 Syntax and Semantics of ATL * ATL * can be seen as an extension of the computational tree logic (CTL * ) [START_REF] Emerson | Deciding full branching time logic[END_REF] where the path quantifiers E -there exists a path -and A -for all pathsare replaced by A and [[A]] where A is a coalition of agents. Intuitively A Φ means "There exists a strategy for the coalition A such that, no matter which strategy the remaining agents follow, Φ holds". On the other hand, [[A]] Φ means "For all strategies of the coalition A, there exists a strategy of the remaining agents such that Φ holds". Also, whereas transition systems or Kripke structures are used in order to evaluate CTL * formulae, concurrent game models (CGM), whose definition is given in the Sect. 2.2 are used to evaluate ATL* formulae.

Syntax of ATL *

Before giving the syntax of ATL * , we recall that, as for CTL * or LTL, , and U mean "Next", "Always " and "Until " respectively. In this paper, we give the syntax in negation normal form over a fixed set P of atomic propositions and primitive temporal operators "Next", "Always "and U "Until ". The syntax of ATL * in negation normal form is defined as follows:

State formulae: ϕ := l | (ϕ ∨ ϕ) | (ϕ ∧ ϕ) | A Φ | [[ A]] Φ (1)
Path formulae:

Φ := ϕ | Φ | Φ | (Φ UΦ) | (Φ ∨ Φ) | (Φ ∧ Φ) (2)
where l ∈ P ∪{¬p | p ∈ P} is a literal, A is a fixed finite set of agents and

A ⊆ A is a coalition. Note that ⊤ := p ∨¬ p, ⊥ := ¬⊤, ¬ A Φ := [[A]] ¬Φ.
The temporal operator "Sometimes" ♦ can be defined as ♦ϕ := ⊤Uϕ and the temporal operator "Release "a sψ Rϕ := ϕ ∨ ϕ U(ϕ ∧ ψ). When unnecessary, parentheses can be omitted.

In this paper, we use ϕ, ψ, η to denote arbitrary state formulae and Φ, Ψ to denote path formulae. By an ATL * formula we will mean by default a state formula of ATL * .

Concurrent Game Models

As for ATL or ATL + , ATL * formulae are evaluated over concurrent game models. Concurrent games models are transition systems where each transition to a unique successor state results from the combination of actions chosen by all the agents (components and/or environment) of the system. Notation: Given a set X, P(X) denotes the power set of X.

Definition 1 (Concurrent game model and structure). A concurrent game model (in short CGM) is a tuple M =(A, S, {Act a } a∈A , {act a } a∈A , out, P, L) where -A = {1,...,k} is a finite, non-empty set of players (agents), -S is a non-empty set of states, -for each agent a ∈ A, Act a is a non-empty set of actions.

For any coalition A ⊆ A we denote Act A := a∈A Act a and use σ A to denote at u p l ef r o mAct A . In particular, Act A is the set of all possible action vectors in M. -for each agent a ∈ A, act a : S →P (Act a ) \ {∅} defines for each state s the actions available to a at s, -out is a transition function assigning to every state s ∈ S and every action vector σ A = {σ 1 ,...,σ k }∈Act A a state out(s, σ A ) ∈ S that results from s if every agent a ∈ A plays action σ a ,w h e r eσ a ∈ act a (s) for every a ∈ A. -P is a non-empty set of atomic propositions. -L : S →P(P) is a labelling function.

The sub-tuple S =( A, S, {Act a } a∈A , {act a } a∈A , out) is cal led a concurrent game structure (CGS).

Semantics of ATL *

In order to give the semantics of ATL * , we use the following notions. Although they are the same as those in [START_REF] Cerrito | Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic ATL+[END_REF], we recall them here to make the paper selfcontained.

Computations. A play,o rcomputation, is an infinite sequence s 0 s 1 s 2 ••• ∈ S ω of states such that for each i ≥ 0 there exists an action vector σ A = σ 1 ,...,σ k such that out(s i ,σ A )=s i+1 .Ahistory is a finite prefix of a play. We denote by Plays M and Hist M respectively the set of plays and set of histories in M. For a state s ∈ S,w eu s ePlays M (s)a n dHist M (s) as the set of plays and set of histories with initial state s. Given a sequence of states λ, we denote by λ 0 its initial state, by λ i its (i + 1)th state, by λ ≤ i the prefix λ 0 ...λ i of λ and by λ ≥i the suffix λ i λ i+1 ... of λ. When λ = λ 0 ...λ ℓ is finite, we say that it has length ℓ and write |λ| = ℓ. Also, we set last(λ)=λ ℓ .

Strategies. A strategy for an agent a in M is a mapping F a : Hist M → Act a such that for all histories h ∈ Hist M ,w eh a v eF a (h) ∈ act a (last(h)). This kind of strategies is also known as "perfect recall" strategies. We denote by Strat M (a) the set of strategies of agent a. A collective strategy of a coalition A ⊆ A is a tuple (F a ) a∈A of strategies, one for each agent in A. We denote by Strat M (A)t h e set of collective strategies of coalition A.Ap l a yλ ∈ Plays M is consistent with a collective strategy F A ∈ Strat M (A) if for every i ≥ 0 there exists an action vector σ A = σ 1 ,...,σ k such that out(λ i ,σ A )=λ i+1 and σ a = F a (λ ≤i ) for all a ∈ A. The set of plays with initial state s that are consistent with F A is denoted Plays M (s, F A ). For any coalition A ⊆ A and a given state s ∈ S in a given CGM M,a nA -co-action at s in M is a mapping Act c A : Act A → Act A\A that assigns to every collective action of A at the state s a collective action at s for the complementary coalition A \ A. Likewise, an A -co-strategy in M is a mapping F c A : Strat M (A) × Hist M → Act A\A that assigns to every collective strategy of A and every history h a collective action at last(h)f o rA \ A,a n dPlays M (s, F c A )i s the set of plays with initial state s that are consistent with F c A .

Semantics. The semantics of ATL * is the same as the one of CTL * [START_REF] Emerson | Deciding full branching time logic[END_REF] (modulo CGM as intended interpretations) with the exception of the two following items:

-M,s |= A Φ iff there exists an A-strategy F A such that, for all computations λ ∈ Plays M (s,

F A ), M,λ |= Φ -M,s |=[ [ A]] Φ iff there exists an A-co-strategy F c
A such that, for all computations λ ∈ Plays M (s, F c A ), M,λ |= Φ Valid, satisfiable and equivalent formulae in ATL * are defined as usual.

3 Tableau-Based Decision Procedure for ATL * In this section, we give the general description of our tableau-based decision procedure for ATL * formulae. The different steps of the procedure are summarized in this section and Fig. 1 and then detailed in the next three sections.

From an initial formula η, the tableau-based decision procedure for ATL * that we propose attempts to build step-by-step a directed graph from which it i spo s s i b l et oe x t r a c taC G Mf o rη. This attempt will lead to a failure if η is not satisfiable.

Nodes of that graph are labelled by sets of state formulae and are partitioned into two categories: prestates and states. A prestate can be seen as a node where the information contained in its formulae is "implicit". When we decompose all the formulae of a prestate and saturate the prestate, we obtain one or several states as successor nodes. States have the particularity of containing formulae of the form A ϕ or [[A]] ϕ from which it is possible to compute the next steps of the tableau creation. All prestates have states as successors and directed edges between them are of the form =⇒; on the other hand, all states have prestates as successors and directed edges between them are of the form σ A -→ where σ A is an action vector. The procedure is in two phases: the construction phase and the elimination phase. First, we create an initial node, that is a prestate containing the initial formula η, and we construct the graph by expanding prestates into states via a rule called (SR) and by computing prestates from states with a rule called (Next).T h er u l e(SR) decomposes each ATL * formula of a prestate, and then saturates the prestate into new states. Explanation of rules (SR) and (Next) can be found in Sects. 4 and 5, respectively.

The procedure avoids creation of duplicated nodes (a form of loop check), which ensures termination of the procedure. The construction phase ends when no new states can be added to the graph. The graph obtained at the end of the construction phase is called the initial tableau for η, also noted T η 0 .

The second phase of the procedure eliminates via the rule (ER1) all nodes with missing successors, that is prestates with no more successors at all or states with at least one missing action vector on its outcome edges. Also, by means of a rule called (ER2) it eliminates all states with "unrealized eventualities", that is states that cannot ensure that all the objectives it contains will be eventually fulfilled. The graph obtained at the end of the elimination phase of the procedure is called the final tableau for η, also noted T η . Explanation of rules (ER1) and (ER2) can be found in Sect. 6.

Our tableau-based decision procedure for ATL * deals with what [START_REF] Goranko | Tableau-based decision procedures for logics of strategic ability in multiagent systems[END_REF] calls "tight satisfiability": the set A of agents involved in the tableau (and the CGMs it tries to build) is the set of agents present in the input formula.

Construction Phase: Decomposition and Saturation

Decomposition of ATL * Formulae All ATL * formulae can be partitioned into four categories: primitive formulae, α-formulae, β-formulae and γ-formulae. Primitive formulae correspond to the "simplest formulae" in the sense that they cannot be decomposed. These formulae are ⊤, ⊥, the literals and all

ATL * suc- cessor formulae,o ft h ef o r m A ψ or [[A]] ψ where ψ is called the successor component of A ψ or [[A]
] ψ respectively. Every non-primitive formula must be decomposed into primitive formulae. α-formulae are of the form ϕ ∧ ψ where ϕ and ψ are α-components while β-formulae are of the form ϕ ∨ ψ where ϕ and ψ are β-components. Their decomposition is classical. Other formulae, that is of the form A Φ or [[A]] Φ, where Φ = ψ,a r eγ-formulae. This notion firstly introduced in [START_REF] Cerrito | Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic ATL+[END_REF] reveals quite useful also in the more expressive context of ATL * . Decomposition of these formulae is trickier than for α-a n dβ-formulae. Indeed, we will need to extract all possibilities of truth encapsulated in γ-formula ξ, which concretely aims at defining one or several conjunctions of primitive formulae such that their disjunction is equivalent to the γ-formulae ξ (see lemma 1).

Decomposition of γ-Formulae. This subsection contains the heart of the decision procedure for ATL * , indeed the main difference with our decision procedure for ATL + lies in the treatment of γ-formulae. The first difficulty is that quantifiers A or [[A]] cannot distribute over Boolean connectors as seen in [START_REF] Cerrito | Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic ATL+[END_REF]. An additional difficulty specific to ATL * is the fact that it is now necessary to also deal with nesting of temporal operators, resulting in a second level of recurrence when the temporal operators and U are encountered in the decomposition function described below.

In temporal logics, e.g. LTL, the operator U is considered as an eventuality operator, that is an operator that promises to verify a given formula at some instant/state. When we write λ |= ϕ 1 Uϕ 2 , where ϕ 1 and ϕ 2 are state formulae, we mean that there is a state λ i of the computation λ where ϕ 2 holds and ϕ 1 holds for all the states of λ preceding λ i . So, once the property ϕ 2 is verified, we do not need to take care of ϕ 1 , ϕ 2 and ϕ 1 Uϕ 2 any more. We say that ϕ 1 Uϕ 2 is realized. However, if ϕ 1 and ϕ 2 are path formulae, e.g. Φ 1 and Φ 2 respectively, state λ i is such that from it Φ 2 must hold forever -we say that Φ 2 is "initiated" at λ i , in the sense that we start to make Φ 2 true at λ i -, and for every computation λ ≥j , where j<i , Φ 1 must hold. So Φ 1 has to be true forever, that is even after Φ 2 had been initiated. This explains the fact that at a possible state s the path formula ϕ 1 Uϕ 2 may become ϕ 1 Uϕ 2 ∧ ϕ 1 when ϕ 1 is a path formula and we postpone ϕ 2 . Note that ϕ 1 is then also initiated at s.W e now face the problem of memorizing the fact that a path formula Φ is initiated since path formulae cannot be stored directly in a state. That is why, during the decomposition of γ-formulae, we add a new set of path formulae linked to a γ-component and the current state.

The definition and general treatment of eventualities in our procedure are given in Sect. [START_REF] Goranko | Tableau-based decision procedures for logics of strategic ability in multiagent systems[END_REF].

In order to decompose γ-formulae ϕ = A Φ or ϕ =[ [ A]] Φ, we analyse the path formula Φ in terms of present (current state) and future (next states). This analysis is done by a γ-decomposition function dec : ATL * p →P(ATL * s × ATL * p × P(ATL * p )) where ATL * p is the set of ATL * path formulae and ATL * s is the set of ATL * state formulae. Intuitively, the function dec assigns to the path formula Φ, a set of triples ψ, Ψ, S where ψ a state formula true at the current state, Ψ is a path formula expressing what must be true at next states and S is the set of path formulae initiated at the current state during the γ-decomposition This set S will be used during the elimination phase to determine if eventualities are realized or not, see Sect. 6.

We first define two operators ⊗ and ⊕ between two sets S 1 and S 2 of triples.

⋆ S 1 ⊗ S 2 := { ψ i . ∧ ψ j ,Ψ i . ∧ Ψ j ,S i ∪ S j | ψ i ,Ψ i ,S i ∈S 1 , ψ j ,Ψ j ,S j ∈S 2 } ⋆ S 1 ⊕ S 2 := { ψ i . ∧ ψ j ,Ψ i . ∨ Ψ j ,S i ∪ S j | ψ i ,Ψ i ,S i ∈S 1 , ψ j ,Ψ j ,S j ∈S 2 , Ψ i = ⊤,Ψ j = ⊤}
The function dec is defined by induction on the structure of path formula Φ as follows:

⋆ dec(ϕ)={ ϕ, ⊤, ∅ } for any ATL * state formula ϕ ⋆ dec( Φ 1 )={ ⊤,Φ 1 , ∅ } for any path formula Φ 1 ⋆ dec( Φ 1 )={ ⊤, Φ 1 , {Φ 1 } } ⊗ dec(Φ 1 ) ⋆ dec(Φ 1 UΦ 2 )=({ ⊤,Φ 1 UΦ 2 , {Φ 1 } } ⊗ dec(Φ 1 )) ∪ ({ ⊤, ⊤, {Φ 2 } } ⊗ dec(Φ 2 )) ⋆ dec(Φ 1 ∧ Φ 2 )=dec(Φ 1 ) ⊗ dec(Φ 2 ) ⋆ dec(Φ 1 ∨ Φ 2 )=dec(Φ 1 ) ∪ dec(Φ 2 ) ∪ (dec(Φ 1 ) ⊕ dec(Φ 2 ))
Note that the definition of the function dec is based on the fixed-point equivalences of LTL [START_REF] Emerson | Temporal and modal logics[END_REF]: ∨ is to automatically transform resultant formulae in conjunctive normal form without redundancy, and therefore ensures the termination of our tableau-based decision procedure. For instance, when applying the function dec on ♦Φ∧♦Φ we may obtain a path formula ♦Φ ∧ ♦Φ ∧ ♦Φ and applying again the function dec on the so-obtained path formula will return ♦Φ ∧ ♦Φ ∧ ♦Φ ∧ ♦Φ, and so on forever. Also when the formula is complicated with ∧ and ∨ embedded in temporal operators, we may not be able to define which part of a path formula is identical to another one. We avoid these unwanted behaviours with our use of ] Φ be a γ-formula to be decomposed. Each triple ψ, Ψ, S ∈dec(Φ) is then converted to a γ-component γ c (ψ, Ψ, S) as follows:

Ψ ≡ Ψ ∧ Ψ and Φ UΨ ≡ Ψ ∨ (Φ ∧ (Φ UΨ
γ c (ψ, Ψ, S)=ψ if Ψ = ⊤ (3) γ c (ψ, Ψ, S)=ψ ∧ A A Ψ if ζ is of the form A Φ, (4)
γ c (ψ, Ψ, S)=ψ ∧ [[ A]] [[ A]] Ψ if ζ is of the form [[A]] Φ (5)
and a γ-set γ s (ψ, Ψ, S)=S.

The following key lemma claims that every γ-formula is equivalent to the disjunction of its γ-components.

Lemma 1. For any ATL * γ-formula ζ = A Φ or ζ =[ [A]] Φ 1. Φ ≡ {ψ ∧ Ψ | ψ, Ψ, S ∈dec(Φ)} 2. A Φ ≡ { A (ψ ∧ Ψ ) | ψ, Ψ, S ∈dec(Φ)},a n d [[ A]] Φ ≡ {[[ A]] ( ψ ∧ Ψ ) | ψ, Ψ, S ∈dec(Φ)} 3. A Φ ≡ {γ c (ψ, Ψ, S) | ψ, Ψ, S ∈dec(Φ)} Example 1. (Decomposition of θ = 1 (( ♦q∨♦r)∧(♦q∨♦r)))
. First, we apply the decomposition function to the path formula Φ =( ♦q ∨ ♦r) ∧ (♦q ∨ ♦r), see Fig. 2. We recall that ♦ϕ ≡⊤Uϕ. It is worth noting that p and r can be replaced by any state formulae without affecting the basic structure of the computation of the function dec.

Then, for instance, from the triple r, ♦q ∧ ♦q, {r, ♦q} of dec(Φ), we obtain the γ-component γ c (r, ♦q∧♦q, {r, ♦q})=r∧ 1 1 ( ♦q∧♦q) and the γ-set γ s (r, ♦q ∧ ♦q, {r, ♦q})={r, ♦q}; from the triple ⊤, ♦q ∧ ♦q, {♦q} we obtain γ c (⊤, ♦q∧♦q, {♦q})= 1 1 ( ♦q∧♦q)andγ s (⊤, ♦q∧♦q, {♦q})={♦q}.

Closure. The closure cl(ϕ)o fa nATL * state formula ϕ is the least set of ATL * formulae such that ϕ,⊤, ⊥∈cl(ϕ), and cl(ϕ) is closed under taking successor, α-, β-a n dγ-components of ϕ. For any set of state formulae Γ we define

cl(Γ )= {cl(ψ) | ψ ∈ Γ } (6)
We denote by |ψ| the length of ψ and by ||Γ || the cardinality of Γ .

Lemma 2. For any ATL * state formula ϕ, ||cl(ϕ)|| < 2 2 2|ϕ| . Sketch of proof. The double exponent, in the size of the ϕ, of the closure comes from the fact that, during decomposition of γ-formulae, path formulae are put in disjunctive normal form. We recall that this form is necessary to ensure the termination of our procedure.

♦q ∨ ♦r) ∧ (♦q ∨ ♦r))
Full expansions of sets of ATL * formulae. Once we are able to decompose into components every non-primitive ATL * state formulae, it is possible to obtain full expansions of a given set of ATL * state formulae using the following definition:

Definition 2. Let Γ , Δ be sets of ATL * state formulae and Γ ⊆ Δ ⊆ cl(Γ ).

1. Δ is patently inconsistent if it contains ⊥ or a pair of formulae ϕ and ¬ϕ.

Δ is a full expansion of Γ if it is not patently inconsistent and satisfies the following closure conditions:

-i fϕ ∧ ψ ∈ Δ then ϕ ∈ Δ and ψ ∈ Δ; -i fϕ ∨ ψ ∈ Δ then ϕ ∈ Δ or ψ ∈ Δ; -i fϕ ∈ Δ is a γ-formula, then at least one γ-component of ϕ is in Δ and exactly one of these γ-components, say γ c (ψ, Ψ, S),i nΔ, denoted γ l (ϕ, Δ), is designated as the γ-component in Δ linked to the γ-formula ϕ, as explained below. We also denote by γ sl (ϕ, Δ) the set of path formulae γ s (ψ, Ψ, S), which is linked to the γ-component γ l (ϕ, Δ)

The set of all full expansions of Γ is denoted by FE(Γ ).

Proposition 1. For any finite set of ATL * state formulae Γ :

Γ ≡ Δ | Δ ∈ FE(Γ ) .
The proof easily follows from Lemma 1.

The rule (SR) adds to the tableau the set of full expansions of a prestate Γ as successor states of Γ .

Rule (SR).

Given a prestate Γ , do the following:

1. For each full expansion Δ of Γ add to the pretableau a state with label Δ. 2. For each of the added states Δ,ifΔ does not contain any formula of the form A ϕ or [[A]] ϕ, add the formula A ⊤ to it; 3. For each state Δ obtained at steps 1 and 2, link Γ to Δ v i aa= ⇒ edge; 4. If, however, the pretableau already contains a state Δ ′ with label Δ,d on o t create another copy of it but only link Γ to Δ ′ via a =⇒ edge.

Construction Phase: Dynamic Analysis of Successor Formulae

We recall that the considered agents are those explicitly mentioned in the initial formula η.T h er u l e(Next) creates successor prestates to a given state, say Δ, so that the satisfiability of Δ is equivalent to the satisfiability of all the prestates. In our tableau construction procedure, choosing one of the successor formulae contained in Δ is considered as a possible action for every agent. Then each possible action vector is given a set of formulae corresponding to the choice collectively made by every agent. More details about the rationale behind the rule (Next) can be found in [START_REF] Carral | EL-ifying ontologies[END_REF][START_REF] Goranko | Tableau-based decision procedures for logics of strategic ability in multiagent systems[END_REF]. Moreover, it is worthwhile noticing that the rule (Next) is done in such a way so that any created prestate contains at most one formula of the form [[A ′ ]] ψ, where A ′ = A.

Rule (Next). Given a state Δ, do the following, where σ is a shorthand for σ A :

1. List all primitive successor formulae of Δ in such a way that all successor formulae of the form A Φ precede all formulae of the form [[A ′ ]] Φ where A ′ = A, which themselves precede all formulae of the form [[A]] Φ; let the result be the list

L = A 0 ϕ 0 ,..., A m-1 ϕ m-1 , [[ A ′ 0 ]] ψ 0 ,...,[[ A ′ l-1 ]] ψ l-1 , [[ A]] μ 0 ,...,[[ A]] μ n-1
Let r Δ = max{m + l, 1}; we denote by D(Δ) the set {0,...,r Δ -1} |A| . Then, for every σ ∈ D(Δ), denote N (σ): ={i | σ i m}, where σ i is the ith component of the tuple σ, and let co(σ

):=[ i∈N (σ) (σ i -m)] mod l. 2.
For each σ ∈ D(Δ) create a prestate:

Γ σ = {ϕ p | A p ϕ p ∈ Δ and σ a = p for all a ∈ A p } ∪{ψ q | [[ A ′ q ]] ψ q ∈ Δ, co(σ)=q and A -A ′ q ⊆ N (σ)} ∪{μ r | [[ A]] μ r ∈ Δ} If Γ σ is empty, add ⊤ to it. Then connect Δ to Γ σ with σ -→ .
If, however, Γ σ = Γ for some prestate Γ that has already been added to the initial tableau, only connect Δ to Γ with σ -→ .

Example 2. We suppose a state containing the following successor formulae, that we arrange in the following way, where the first line of numbers corresponds to positions among negative successor formulae, and the second line corresponds to positions among successor formulae, with A = A.

L = 0 1 1 ( ♦q ∧ ♦q), 0 1 [[1]] [[1]] ¬q, 1 2 [[2]] [[2]] ♦s, [[ 1 , 2]] ¬q
The application of the rule (Next) on L gives the following results:

σ N (σ) co(σ) Γ (σ) σ N (σ) co(σ) Γ (σ) 0, 0 ∅ 0 1 ( ♦q ∧ ♦q), ¬q 1, 2 {1, 2} 1 [[1]] ¬q, ¬q 0, 1 {2} 0 1 ( ♦q ∧ ♦q), [[2]] ♦s, ¬q 2, 0 {1} 1 [[1]] ¬q, ¬q 0, 2 {2} 1 1 ( ♦q ∧ ♦q), ¬q 2, 1 {1, 2} 1 [[1]] ¬q, ¬q 1, 0 {1} 0 ¬q 2, 2 {1, 2} 0 [[2]] ♦s, ¬q 1, 1 {1, 2} 0 [[2]] ♦s, ¬q 6

Elimination Phase

The elimination phase works step-by-step. In order to go through one step to another we apply by turns two elimination rules, called (ER1) and (ER2), until no more nodes can be eliminated. The rule (ER1) detects and deletes nodes with missing successor, while the rule (ER2) detects and delete states that do not realize all their eventualities. At each step, we obtain a new intermediate tableau, denoted by T η n . We denote by S η n the set of nodes (states and prestates) of the intermediate tableau T η n . At the end of the elimination phase, we obtain the final tableau for η, denoted by T η . It is declared open if the initial node belongs to S η , otherwise closed. The procedure for deciding satisfiability of η returns "No" if T η is closed, "Yes" otherwise.

Remark 1. Contrary to the tableau-based decision procedure for ATL + ,w ed o not eliminate all the prestates at the beginning of the elimination phase. We eliminate them with the rule (ER1) only if necessary. This does not have any effect on the result of the procedure, nor any relevant modification in the soundness and completeness proofs, but it makes implementation quicker and easier.

Rule (ER1). Let Ξ ∈ S η n be a node (prestate or state). -In the case where Ξ is a prestate: if all nodes Δ with Ξ =⇒ Δ have been eliminated at earlier stages, then obtain T η n+1 by eliminating Ξ from T η n . -In the case where Ξ is a state: if, for some σ ∈ D(Ξ), the node Γ with Ξ σ -→ Γ has been eliminated at earlier stage, then obtain T η n+1 by eliminating Ξf r o mT η n . In order to define the rule (ER2), we first need to define what is an eventuality in the context of ATL * and then define how to check whether eventualities are realized or not.

Eventualities. In our context, we consider all γ-formulae as potential eventualities. We recall that a γ-formula is of the form A Φ or [[A]] Φ where Φ = ϕ. When constructing a tableau step-by-step as we do in our procedure, it is possible to postpone forever promises encapsulated in operators such as U as far as we keep promising to satisfy them. We consider that a promise, which is a path formula, is satisfied (or realized) once it is initiated at the current state, which corresponds to an engagement to keep it true if necessary, for any computation starting at that state. So we want to know at a given state and for a given formula whether all promises (or eventualities) are realized. This is the role of the function Realized: ATL * p ×P(ATL * s ) ×P(ATL * p ) → B, where B is the set {true, f alse}. The first argument of the function Realized is the path formula to study, the second argument is a set of state formulae Θ, and the third argument is a set of path formulae on which one is "engaged". This third argument is exactly what is added with respect to ATL + treatment. For our purpose, to know whether a potential eventuality is realized, we use the set Θ to represent the state containing the γ-formula and the set S = γ sl (Φ, Θ) obtained during the decomposition of Φ and the full expansion of Θ. This last set S is computed in Sect. 4 and corresponds to the set of path formulae initiated in the current state Θ. The definition of Realized is given by recursion on the structure of Φ as follows:

-

Realized(ϕ, Θ, S)=true iff ϕ ∈ Θ -Realized(Φ 1 ∧ Φ 2 ,Θ,S)=Realized(Φ 1 ,Θ,S) ∧ Realized(Φ 2 ,Θ,S) -Realized(Φ 1 ∨ Φ 2 ,Θ,S)=Realized(Φ 1 ,Θ,S) ∨ Realized(Φ 2 ,Θ,S) -Realized( Φ 1 ,Θ,S)=true -Realized( Φ 1 ,Θ,S)=true iff Φ 1 ∈ Θ ∪ S -Realized(Φ 2 UΦ 1 ,Θ,S)=true iff Φ 1 ∈ Θ ∪ S Remark 2.
In the two last items, we use the set Θ ∪ S to handle the particular case where Φ 1 is a state formula that is already in the set Θ because of the behaviour of another coalition of agents.

We will see with Definition 4 that if the function Realized declares that an eventuality is not immediately realized at a given state, then we check in the corresponding successor states whether it is realized or not. But, because of the way γ-formulae are decomposed, an eventuality may change its form from one state to another. Therefore, we define the notion of Descendant potential eventuality in order to define a parent/child link between potential eventualities and keep track of not yet realized eventualities, and finally check whether the potential eventualities are realized at a given moment. Δ . The notion of descendant potential eventuality of ξ of degree d,ford>1, is defined inductively as follows:

-any successor eventuality of ξ (w.r.t. some γ-component of ξ) is a descendant eventuality of ξ of degree 1; -any successor eventuality of a descendant eventuality ξ n of ξ of degree n is a descendant eventuality of ξ of degree n +1.

We will also consider ξ to be a descendant eventuality of itself of degree 0.

Realization of Potential Eventualities First, we give some notation:

Notation: Let L = A 0 ϕ 0 ,..., A m-1 ϕ m-1 , [[ A ′ 0 ]] ψ 0 ,...,[[ A ′ l-1 ]] ψ l-1 , [[ A]] μ 0 ,...,[[ A]] μ n-1 be the list of all primitive successor formulae of Δ ∈ S η 0 , induced as part of application of (Next). Succ(Δ, A p ϕ p ):={Γ | Δ σ -→ Γ, σ a = p for every a ∈ A p } Succ(Δ, [[ A ′ q ]] ψ q ):={Γ | Δ σ -→ Γ, co(σ)=q and A -A ′ q ⊆ N (σ)} Succ(Δ, [[ A]] μ r ):={Γ | Δ σ -→ Γ } Definition 4. (Realization of potential eventualities) Let Δ ∈ S η
n be a state and ξ ∈ Δ be a potential eventuality of the form A Φ or

[[ A]] Φ.L e t S = γ sl (ξ, Δ).T h e n : 1. If Realized(Φ, Δ, S)=true then ξ is realized at Δ in T η n . 2. Else, let ξ 1 Δ be the successor potential eventuality of ξ w.r.t. γ l (ξ, Δ).I ff o r every Γ ∈ Succ(Δ, A ξ 1 Δ ) (resp. Γ ∈ Succ(Δ, [[ A]] ξ 1 Δ )), there exists Δ ′ ∈T η n with Γ =⇒ Δ ′ and ξ 1 Δ is realized at Δ ′ in T η n , then ξ is realized at Δ in T η n . Example 3. Let Δ = { 1 (( ♦q ∨ ♦r) ∧ (♦q ∨ ♦r)), [[1]] ¬q, [[2]] ♦s, [[ 1 , 2]] ¬q, ¬q, 1 1 ( ♦q ∧ ♦q), [[1]] [[1]] ¬q, s, [[2]] [[ 2
]] ♦s} be a state. If we consider the potential eventuality ξ = 1 (( ♦q ∨ ♦r) ∧ (♦q ∨ ♦r)) ∈ Δ, Φ =( ♦q ∨ ♦r) ∧ (♦q ∨ ♦r)a n dS = γ sl (ξ, Δ)={♦q}, then we obtain the following result:

Realized(Φ, Δ, S)=Realized( ♦q ∨ ♦r, Δ, S) ∧ Realized(♦q ∨ ♦r, Δ, S) = Realized( ♦q, Δ, S) ∨ Realized(♦r, Δ, S) ∧ Realized(♦q, Δ, S) ∨ Realized(♦r, Δ, S) =(true ∨ false) ∧ (false ∨ false)=false
The call of the function Realized on (Φ, Δ, S) returns false, which means that the potential eventuality ξ is not immediately realized. Therefore, we must check in the future if ξ can be realized or not. Concretely, we must check that the descendant potential eventuality ξ 1 = 1 ( ♦q ∧ ♦q) is realized at the next states corresponding to the collective choices of all agents to satisfy the successor formula 1 ξ 1 , that is states resulting from the transitions (0, 0), (0, 1) and (0, 2), as seen in Example 2.

Rule (ER2). If Δ ∈ S η

n is a state and contains a potential eventuality that is not realized at Δ ∈T η n , then obtain T η n+1 by removing Δ from S η n .

7 Results and Sketches of Proofs Theorem 1. The tableau-based procedure for ATL * is sound with respect to unsatisfiability, that is if a formula is satisfiable then its final tableau is open.

To prove soundness, we first prove that from any satisfiable prestate we obtain at least one satisfiable state, and we prove that from any satisfiable state we obtain only satisfiable prestates. Second, we prove that no satisfiable prestate or state can be eliminated via rule (ER1) or (ER2), and in particular, if the initial prestate is satisfiable, it cannot be removed, which means that the tableau is open.

Theorem 2. The tableau-based procedure for ATL * is complete with respect to unsatisfiability, that is if a tableau for an input formula is open then this formula is satisfiable.

To prove completeness, we construct step-by-step a special structure called Hintikka structure from the open tableau and then we prove that a CGM satisfying the initial formula can be obtained from that Hintikka structure. Theorem 3. The tableau-based procedure for ATL * runs in at most 3EXPTIME.

We first argue that the number of formulae in the closure of the initial formula η is at most double exponential in the size of η (see Lemma 2). Then we have that the number of states is at most exponential in the size of the closure of η. Therefore the procedure runs in at most 3EXPTIME.

Implementation of the Procedure

We propose a prototype implementing our tableau-based decision procedure for ATL * , available on the following web site: http://atila.ibisc.univ-evry.fr/tableau ATL star/. This prototype aims at giving a user-friendly tool to the reader interested in checking satisfiability of ATL* formulae. This is why we provide our prototype as a web application directly ready to be used. The application allows one to enter a formula, or to select one from a predefined list of formulae, and then launch the computation of the corresponding tableau. It returns some statistics about the number of prestates and states generated as well as the initial and final tableaux for the input formula, therefore also an answer on its satisfiability. Explanation on how to use the application is given on the web site.

Our prototype is developed in Ocaml for the computation, and in PHP and JavaScript for the web interface. Binaries of the application can be found on the same web page.

As the main difference between ATL and ATL * comes from path formulae, we mainly focus our test on that point and use the list of tests proposed by Reynolds for CTL * in [START_REF] Reynolds | A faster tableau for CTL[END_REF]. This allows us to check that our application gives the same results in term of satisfiability and that our running times for these examples are satisfactory. Moreover, other tests using formulae with non trivial coalitions have been done. Nevertheless a serious benchmark has still to be done, which is a non trivial work, left for the future. Also, we plan to compare theoretically and experimentally our approach with the automata-decision based procedure of [8].

Conclusion

In this paper, we propose the first sound, complete and terminating tableaubased decision procedure for ATL * : it is easy to understand and conceptually simple. We also provide the first implementation to decide the satisfiability of ATL * formulae, among which ATL + formulae. future works, it would be worthwhile to implement the automata-based decision procedure proposed in [8]a n d be able to make some practical comparisons. Another perspective is to implement model synthesis with a minimal number of states for satisfiable ATL * formulae.

Fig. 1 .

 1 Fig. 1. Overview of the tableau-based decision procedure for ATL *

∨

  correspond respectively to the operators ∧ and ∨ where the associativity, commutativity, idempotence and identity element properties are embedded in the syntax. The aim of both . ∧ and .

∨

  and the transformation of any new path formula in conjunctive normal form without redundancies. Now, let ζ = A Φ or ζ =[ [A]

Fig. 2 .

 2 Fig.2. Function dec applied on the path formula 1 (( ♦q ∨ ♦r) ∧ (♦q ∨ ♦r))

Definition 3 .

 3 (Descendant potential eventualities). Let Δ be a state and let ξ ∈ Δ be a potential eventuality of the formA Φ or [[ A]] Φ. Suppose the γcomponent γ l (ξ, Δ) in Δ linked to ξ is, respectively, of the form ψ ∧ A A Ψ or ψ ∧ [[ A]] [[ A]]Ψ . Then the successor potential eventuality of ξ w.r.t. γ l (ξ, Δ) is the γ-formula A Ψ (resp. [[ A]] Ψ ) and it will be denoted by ξ1

Acknowledgement. I would like to thank Serenella Cerrito and Valentin Goranko for their advices and proofreading. I also thank the anonymous referees for their helpful criticisms.