Irina Sin
email: irina.sin@mines-paristech.fr

Jérôme Corvisier

Impact of co-injected impurities on hydrodynamics of CO 2 injection. Studying interplayed chromatographic partitioning and density driven flow and fate of the injected mixed gases: numerical and experimental results

Keywords: CO2 storage, impurities, chromatographic partitioning, density-driven flow, numerical modeling, CO2, N2, O2, SO2, Ar, H2S, CH4

This work presented a study on the chromatographic partitioning of CO 2 and impurities present in the injected stream in the CCS context. Laboratory and field observations have already revealed the chromatographic partitioning phenomenon of CO 2 and impurities both in the gas and in the aqueous phases. Series of laboratory experiments are modeled using the reactive transport HYTEC. Numerical results confirm the laboratory observations and show differential breakthrough of injected gases. A series of experiments on CO 2 and H 2 S mixture with different H 2 S concentration is modeled. Numerical results of HYTEC are successfully compared with the results given by CMG-GEM and with experimental data. Another series of dynamic displacement-solubility experiments is modeled to study the chromatographic gas partitioning depending on a type of impurity such as H 2 S, CH 4 , N 2 , SO 2 . O 2 , and Ar. Numerical results show that the physics can be modeled both qualitatively and quantitatively. 1. Solubility of the impurity in the injected stream regarding to that of CO 2 is a key factor. The less soluble the impurity gas is, the earlier and higher breakthrough should be expected. 2. Classification of impurity gases can be proposed. For example, in the decreasing order of their solubility (13.5 MPa, 61°C, 118950 ppm): SO 2 > H 2 S > CO 2 > CH 4 > Ar > O 2 > N 2 . 3. Using accurate models of reactive transport, solubility, phase equilibrium and thermodynamic properties of non-ideal mixtures allows reproducing of the chromatographic partitioning: breakthrough time of gases, gas concentration, and front propagation. Chromatographic partitioning was studied at reservoir scale by modeling two scenarios of impure CO 2 injection over 30 years: 95%CO 2 +4%N 2 +1%O 2 and 95%CO 2 +5%SO 2 . When injecting impurities, the chromatographic partitioning can be observed inside the gas plume and in the aqueous solution. Modeling injection of 95%CO 2 +4%N 2 +1%O 2 demonstrated potential usage of noble gases for monitoring and proved the previous laboratory results. The plume composition strongly depends on a type of the co-injected gas. Moreover, a type of impurity and its concentration change the density of gas current and the density of the formation water with dissolved components. Both densities in the case of 95%CO 2 +5%SO 2 injection are overall higher than those in the 95%CO 2 +4%N 2 +1%O 2 model. This impacts on the buoyancy forces, hence on the distance, velocity and shape of the plume. Since dissolved impurities contribute to the liquid density, it can then accelerate or slow convective dissolution. Heterogeneous gas composition induces density driven motion that can be especially important in case of heavy compounds such as SO 2 .

Introduction

During the capture process, CO 2 should be separated to increase the efficiency of the storage and to respect the environmental and legal aspects. The injection stream can still contain small amounts of impurities such as N 2 , O 2 , Ar, CO, SO x , NO x , CH 4 , H 2 S and H 2 [START_REF] Kather | CO2 quality and other relevant issues[END_REF][START_REF] Ussiri | Carbon Sequestration for Climate Change Mitigation and Adaptation[END_REF]. Composition and concentration of co-contaminant gas vary depending on major CO 2 source, type of industry and capture process. Some of them can negatively affect the integrity of geological site and/or pipelines or reduce the CO 2 storage capacity. Purifying injection stream involves additional power demand. Understanding their impact on CCS is essential to define the allowed maximum concentration of cocontaminant and to optimize the overall cost.

Small amount of impurities of 5% may still remain after gas separation process. Investigation of their impact has been started over the last two decades: studies on a type of impurity, its concentration [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF] and thermodynamic properties, consequences on storage capacity [START_REF] Li | Evaluating cubic equations of state for calculation of vapor-liquid equilibrium of CO2 and CO2-mixtures for CO2 capture and storage processes[END_REF][START_REF] Ziabakhsh-Ganji | Sensitivity of the co 2 storage capacity of underground geological structures to the presence of so 2 and other impurities[END_REF], experimental and numerical models on geochemical reactions [START_REF] Ziabakhsh-Ganji | An equation of state for thermodynamic equilibrium of gas mixtures and brines to allow simulation of the effects of impurities in subsurface co2 storage[END_REF][START_REF] Sterpenich | Role of impurities on co2 injection: ex-perimental and numerical simulations of thermodynamic properties of water-salt-gas mixtures (co2+ co-injected gases) under geological storage conditions[END_REF][START_REF] Corvisier | Impact of co-injected gases on CO2 storage sites: Geochemical modeling of experimental results[END_REF][START_REF] Corvisier | Simulations of the impact of co-injected gases on co2 storage, the sigarrr project: processes and geochemical approaches for gaswater-salt interactions modeling[END_REF], modeling injection of impure CO 2 at large-scale [START_REF] Xu | Numerical modeling of injection and mineral trapping of co2 with h2s and so2 in a sandstone formation[END_REF][START_REF] Xiao | The effects of gas-fluid-rock interactions on CO2 injection and storage: Insights from reactive transport modeling[END_REF][START_REF] Wei | Numerical study on the field-scale aquifer storage of CO2 containing N2[END_REF][START_REF] Sin | Numerical simulation of compressible two-phase flow and reactive transport in porous media[END_REF][START_REF] Todaka | Reactive transport simulation to assess geochemical impact of impurities on co2 injection into siliciclastic reservoir at the otway site, australia[END_REF], field observations of gas migration [START_REF] Wei | Geochemical impact of aquifer storage for impure CO2 containing O2 and N2: Tongliao field experiment[END_REF].

Previous works on experimentally and numerically thermodynamic properties of several CO 2 binary mixtures [START_REF] Li | Evaluating cubic equations of state for calculation of vapor-liquid equilibrium of CO2 and CO2-mixtures for CO2 capture and storage processes[END_REF][START_REF] Ziabakhsh-Ganji | Sensitivity of the co 2 storage capacity of underground geological structures to the presence of so 2 and other impurities[END_REF][START_REF] Ziabakhsh-Ganji | An equation of state for thermodynamic equilibrium of gas mixtures and brines to allow simulation of the effects of impurities in subsurface co2 storage[END_REF][START_REF] Sterpenich | Role of impurities on co2 injection: ex-perimental and numerical simulations of thermodynamic properties of water-salt-gas mixtures (co2+ co-injected gases) under geological storage conditions[END_REF][START_REF] Corvisier | Impact of co-injected gases on CO2 storage sites: Geochemical modeling of experimental results[END_REF][START_REF] Corvisier | Simulations of the impact of co-injected gases on co2 storage, the sigarrr project: processes and geochemical approaches for gaswater-salt interactions modeling[END_REF][START_REF] Al-Siyabi | Effect of impurities on CO2 stream properties[END_REF] highlighted the positive density and solubility effects of SO 2 and the negative impact of CH 4 , Ar, O 2 and N 2 on the volume and solubility storage capacity. However, comparing to low reactive gases as nitrogen, argon or methane such impurities as SO 2 and H 2 S are highly chemically reactive. They can cause an alteration of reservoir and caprock minerals and near wellbore area in particular. For example, even a very small concentration of SO 2 leads to a strong acidification of the brine. Once sulfur dioxide dissolves and pH drops, it then can induce the dissolution of carbonates such as calcite and the precipitation of sulfate minerals such as anhydrite. This was experimentally and numerically demonstrated in [START_REF] Corvisier | Impact of co-injected gases on CO2 storage sites: Geochemical modeling of experimental results[END_REF].

Beside the pure geochemical effects, other physical phenomena have been observed in the presence of impurities. Several field and laboratory observations showed differential breakthrough of injected gases [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF][START_REF] Wei | Geochemical impact of aquifer storage for impure CO2 containing O2 and N2: Tongliao field experiment[END_REF].

• When a mixture of 98% CO 2 and 2% H 2 S was injected, an earlier breakthrough of CO 2 prior to H 2 S was detected at producing wells. • When a CO 2 -rich mixture with N 2 and O 2 was injected, earlier arrivals both of dissolved oxygen and of oxygennitrogen gas mixture were observed.

Chromatographic gas partitioning depending on a type of impurity was studied in [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF]. Behavior of CO 2 binary systems with H 2 S, CH 4 , N 2 , and SO 2 was demonstrated during flow experiments. Laboratory results revealed a key factor of the impurity solubility order regarding to that of CO2.

In this work, these dynamic displacement-solubility experiments have been modeled. Numerical simulations for N 2 , SO 2 , CH 4 , and H 2 S have been performed. The role of differential solubility in chromatographic gas partitioning has been confirmed and the concept has been complemented with O 2 , Ar.

Moreover, the type and concentration of impurities changes gas and liquid densities. This changes the buoyancy forces, hence the distance, velocity and shape of the plume spread. This work presents multiphase multicomponent reactive flow and transport simulations of injection of impure CO2 at reservoir-scale. Dissolved impurities contribute to liquid density and can then accelerate or slow convective dissolution. Heterogeneous gas composition induces density driven motion that can be especially important in case of heavy compounds. When injecting impurities, chromatographic partitioning can be observed inside the gas plume. Plume composition depends on type of co-injected gas.

The numerical simulations presented in this work were performed using the reactive transport code HYTEC [START_REF] Van Der Lee | Module-oriented modeling of reactive transport with HYTEC[END_REF][START_REF] Lagneau | Operator-splitting-based reactive transport models in strong feed-back of porosity change: The contribution of analytical solutions for accuracy validation and estimator improvement[END_REF][START_REF] Sin | Integrating a compressible multicomponent two-phase flow into an existing reactive transport simulator[END_REF] and its geochemical core CHESS [START_REF] Corvisier | Impact of co-injected gases on CO2 storage sites: Geochemical modeling of experimental results[END_REF][START_REF] Corvisier | Simulations of the impact of co-injected gases on co2 storage, the sigarrr project: processes and geochemical approaches for gaswater-salt interactions modeling[END_REF][START_REF] Van Der Lee | Thermodynamic and mathematical concepts of CHESS[END_REF][START_REF] Corvisier | Considering non-ideal gas mixtures in geochemical modeling of gas-water-salt-rock interactions: Application to impure co2 geological storage[END_REF]. Last developments on gas-water-rock interactions allow complex modeling of real gas behavior, solubility in single and mixed brines, thermodynamic properties and coupled multiphase multicomponent flow and reactive transport.

Section 2 briefly describes the mathematical and numerical methods used to perform the multiphase multicomponent reactive flow and transport simulations. Section 3 shows the model of flow experiment and numerical results of chromatographic gas partitioning. Section 4 presents two models of impure CO2 injection at reservoir scale whose numerical results give insights of gas current motion, its heterogeneous composition and density driven dynamics. We make the conclusions in Section 5.

Mathematical and numerical methods

HYTEC is a reactive transport simulator [START_REF] Van Der Lee | Module-oriented modeling of reactive transport with HYTEC[END_REF][START_REF] Lagneau | Operator-splitting-based reactive transport models in strong feed-back of porosity change: The contribution of analytical solutions for accuracy validation and estimator improvement[END_REF][START_REF] Sin | Integrating a compressible multicomponent two-phase flow into an existing reactive transport simulator[END_REF], which was widely evaluated in benchmark studies [START_REF] Carrayrou | Comparison of numerical methods for simulating strongly nonlinear and heterogeneous reactive transport problems -the MoMaS benchmark case[END_REF][START_REF] Lagneau | HYTEC results of the MoMaS reactive transport benchmark[END_REF][START_REF] De Windt | Intercomparison of reactive transport models applied to UO2 oxidative dissolution and uranium migration[END_REF] and applied in various applications such as cement degradation [START_REF] De Windt | Modeling the degradation of Portland cement pastes by biogenic organic acids[END_REF] radioactive waste disposal [START_REF] Debure | HLW glass dissolution in the presence of magnesium carbonate: Diffusion cell experiment and coupled modeling of diffusion and geochemical interactions[END_REF], geological storage of acid gases [START_REF] Corvisier | Impact of co-injected gases on CO2 storage sites: Geochemical modeling of experimental results[END_REF][START_REF] Hajiw | Impact of impurities on co 2 storage in saline aquifers: Modelling of gases solubility in water[END_REF][START_REF] Jacquemet | Armouring of well cement in H2S-CO2 saturated brine by calcite coatingexperiments and numerical modeling[END_REF] and uranium in situ recovery processes [START_REF] Regnault | 3D reactive transport simulations of uranium in situ leaching: Forecast and process optimization[END_REF]. The code is based on a finite-volume method and deals both with structured and with unstructured grids. Its geochemical part CHESS allows modeling interface reactions, precipitation, dissolution, organic compounds, redox reactions and isotopic fractionation. Both reactions at equilibrium and kinetics can be modeled. Morel's method is used to formulate the chemical system, which is then solved by a modified Newton's method. The activity coefficients 𝛾 ! of non-ideal aqueous solutions can be calculated by applying different activity models such as the specific ion theory (SIT) [START_REF] Grenthe | Estimations of medium effects on thermodynamic data[END_REF]. The fugacity-activity (𝜑 -𝛾) approach is used to solve the gas-liquid equilibrium (1):

𝑃𝑦 ! 𝜑 ! ! = 𝐾 ! ! 𝛾 ! 𝑥 ! , ( 1
)
where 𝑃 is the pressure, 𝑦 ! is the gas mole fraction of species 𝑖, 𝐾 ! ! is the corrected Henry's constant of species 𝑖, 𝑥 ! is the mole fraction of species 𝑖 in the liquid phase. 𝐾 ! ! = 𝐾 ! ! (𝑇, 𝑃) comprises the Poynting factor and corrects the reference fugacity with respect to the pressure and the temperature:

𝐾 ! ! 𝑇, 𝑃 = 𝐾 ! ! 𝑇, 𝑃 !"! exp ! ! ! !!! !"# !" (2)
where 𝑃 !"# is the saturation vapor pressure, 𝜐 ! ! is the molar volume of species 𝑖 at infinite dilution. The fugacity coefficients are calculated using an equation of states (EOS). CHESS/HYTEC proposes a wide range of EOS. We chose the Peng-Robinson EOS (PR78) [START_REF] Robinson | The characterization of the heptanes and heavier fractions for the GPA Peng-Robinson programs[END_REF]:

𝑃 = !" !!! ! - ! ! (!) ! !!! ! !! ! (!!! ! ) (3)
where the repulsive and attractive terms are functions of the critical pressure 𝑃 !,! , critical temperature 𝑇 !,! and the acentric factor 𝜔 ! (see details in [START_REF] Robinson | The characterization of the heptanes and heavier fractions for the GPA Peng-Robinson programs[END_REF]). For mixtures, the parameters 𝑎 and 𝑏 are calculated via the combining rule for the cross parameter 𝑎 !" and the quadratic mixing rules for 𝑎 and 𝑏:

𝑎 = 𝑥 ! 𝑥 ! 𝑎 !" ! ! (4) 𝑎 !" = 𝑎 ! 𝑎 ! (1 -𝑘 !" ) (5)
𝑏 = 𝑥 ! 𝑏 ! ! (6)
where 𝑘 !" are the binary interaction parameters. In [START_REF] Jaubert | VLE predictions with the Peng-Robinson equation of state and temperature dependent kij calculated through a group contribution method[END_REF], the predictive PR78 (PPR78) was proposed where the binary interaction parameters can be calculated and depend on the temperature. In [START_REF] Ahlers | Development of an universal group contribution equation of state: I. Prediction of liquid densities for pure compounds with a volume translated Peng-Robinson equation of state[END_REF], a volume translated method (VTPR) was proposed to improve modeling of volumetric properties. The pseudo partial molar volume is then introduced:

𝜐 ! = 𝜐 ! + 𝑐 ! (7)
where 𝑐 ! is the constant translation parameter or the correction of molar volume. Calculation methods of 𝑐 ! can be found in [START_REF] Ahlers | Development of an universal group contribution equation of state: I. Prediction of liquid densities for pure compounds with a volume translated Peng-Robinson equation of state[END_REF]. The approach was applied to model solubility of gas components and binary systems in pure water, salt and complex brine solutions [START_REF] Corvisier | Impact of co-injected gases on CO2 storage sites: Geochemical modeling of experimental results[END_REF][START_REF] Corvisier | Simulations of the impact of co-injected gases on co2 storage, the sigarrr project: processes and geochemical approaches for gaswater-salt interactions modeling[END_REF][START_REF] Hajiw | Impact of impurities on co 2 storage in saline aquifers: Modelling of gases solubility in water[END_REF]. The authors have compared numerical results of the proposed EOS-based method, GC-PR-CPA for Cubic Plus Association using Peng-Robinson EOS and the Group Contribution method [START_REF] Hajiw | Hydrocarbons-water phase equilibria using the cpa equation of state with a group contribution method[END_REF] and experimental data. New numerical results on modeling gas mixture-water-rock experiments are presented in [START_REF] Corvisier | Considering non-ideal gas mixtures in geochemical modeling of gas-water-salt-rock interactions: Application to impure co2 geological storage[END_REF]. Moreover, the approach has been extended to model the volumetric properties of pure compounds and binary mixtures using the PPR78 and VTPR [START_REF] Sin | Numerical simulation of compressible two-phase flow and reactive transport in porous media[END_REF]. Numerical results have been compared with other EOS (PR78, PPR78, T-VTPR, CPA models and GERG-2008 (REFPROP)), experimental and NIST data in [START_REF] Sin | Numerical simulation of compressible two-phase flow and reactive transport in porous media[END_REF]. The approach can be applied to ternary or multicomponent systems, even though their accuracy may be questioned due to lack of required datasets. Nevertheless, the method allows for a detailed investigation of highly coupled hydrodynamic and chemical processes involved in the impure CO2 injection problems at different scales.

HYTEC is based on the operator-splitting approach that integrates not only all functionalities of CHESS but also numerous thermo-hydrodynamic modules (e.g., saturated, unsaturated, two-phase flow, heat and isothermal regimes). A special sequential iterative coupling method [START_REF] Sin | Integrating a compressible multicomponent two-phase flow into an existing reactive transport simulator[END_REF] is applied for modelling compressible two-phase flow and reactive transport. This method ensures flexibility of each module, allows sophisticated modelling of hydrodynamics, thermodynamics and geochemistry. The coupling method was verified on benchmark problems and compared with TOUGH2-ECO2, TOUGH2 (CSIRO), DUNE, GEM and STOMP [START_REF] Sin | Integrating a compressible multicomponent two-phase flow into an existing reactive transport simulator[END_REF].

The presented methods have been used for the numerical models in this work.

Chromatographic partitioning

Chromatographic partitioning of injected gas was investigated experimentally in [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF], in which the authors provided the sensitivity study on the impact of gas impurity concentration (2, 5, 30% of H 2 S), on the impact of pressure, temperature and salinity conditions (61°C and 13.5 MPa; 25°C and 6 MPa; fresh water and 119 ppm of salinity) and of admixture type in the injected stream (H 2 S, N 2 , SO 2 , CH 4 ). In the last stage, the laboratory results revealed a key factor of the impurity solubility order regarding to that of CO 2 . The breakthrough time of the gas compounds and their profiles highly depend on the solubility ratio between gases. The less soluble the admixture gas is, the earlier and higher breakthrough is expected. The impurity gases present in the injection stream after the capture processes can then be classified by the solubility.

A series of experiments with variable H 2 S concentration in the injected gas stream was chosen for modeling. Numerical simulations were performed by CMG-GEM TM and presented in [START_REF] Bachu | Chromatographic partitioning of impurities (H2S) contained in a CO2 stream injected into a deep saline aquifer: Part 2. effects of flow conditions[END_REF]. The laboratory experiments have been modeled by HYTEC. The present section shows our numerical results comparing with the experimental and numerical results obtained in [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF][START_REF] Bachu | Chromatographic partitioning of impurities (H2S) contained in a CO2 stream injected into a deep saline aquifer: Part 2. effects of flow conditions[END_REF]. The dynamic displacement solubility experiments selected for modeling are shortly described in Section 3.1 as well as the model description. Section 3.2 demonstrates the flow evolution and physics of the H 2 S experiments. Section 3.3 shows the extending the numerical model to other types of admixture and confirms the used methods (Section 2) and the laboratory results on chromatographic gas partitioning.

Numerical model of laboratory experiments

The dynamic solubility experiments were carried out at high pressure and temperature conditions in a tube homogeneously packed with silicate rounded frac sand. The length of the tube is 24.38 m; the tube inner diameter is 0.775 cm. The porosity and permeability are 0.37 and 5915 mD, respectively. The gas mixture is injected at a constant rate of 7.5 cm 3 /h in the tube at constant pressure 13.5 MPa, temperature 61°C and brine salinity 118950 ppm. Modeling of viscosities and densities may be different from [START_REF] Bachu | Chromatographic partitioning of impurities (H2S) contained in a CO2 stream injected into a deep saline aquifer: Part 2. effects of flow conditions[END_REF]. The gas and brine viscosities are constant in this study 0.037 and 0.579 mPa•s, respectively. The gas density is modeled according the PR78, which is reliable for the gas mixtures. The McCain model [START_REF] Mccain | Reservoir-fluid property correlations-state of the art[END_REF] was chosen for the brine density. Fitting of relative permeability functions for gas and brine is reported in details in [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF]. Curves were fitted only for H 2 S and CO 2 experiments.

The methods of gas-liquid equilibrium are described in Section 2. The binary interaction parameters 𝑘 !" and the partial molar volume at infinite dilution 𝜐 ! ! used in this study are given in Table 1. In this study, the partial molar volume was globally averaged or locally averaged for several compounds (e.g., Ar, N 2 , CO2, O 2 , SO 2 ). The binary interaction parameters can be found in literature and can be calculated by the PPR78.

Numerical results of H 2 S and CO 2 partitioning

Fig. 1 presents the numerical results for a feed gas of 2% H 2 S and 98% CO 2 . Numerical results are in a good agreement with the laboratory experiments and numerical models reported in [START_REF] Bachu | Chromatographic partitioning of impurities (H2S) contained in a CO2 stream injected into a deep saline aquifer: Part 2. effects of flow conditions[END_REF]. The gas mixture is injected in the saturated tube; the gas front propagates continuously towards the outlet of the tube, Fig. 1a. The numerical results of CMG-GEM and HYTEC are similar. The gas saturation curves have a common shape and evolution. Fig. 2 shows the evolution of gas composition at the outlet of the tube for the cases of 2% H 2 S and 30% H 2 S in the injected stream. The breakthrough of H 2 S is delayed in both cases. Only slight differences between experimental and numerical results can be observed. However, the numerical models give a phenomenological description of the experiment. Since H 2 S is more soluble than CO 2 , the breakthrough gas is CO 2 -rich. The H 2 S breakthrough indeed occurs later but it then rises and reaches its concentration in the feed gas. The composition of CO 2 and H 2 S in the aqueous phase at 0.5 and 1.2 days is shown in Fig. 1b. Retardation of H 2 S front can be observed and its gap with the CO 2 front grows with injection time. This dynamics is explained by a higher solubility of H 2 S with regard to CO 2 . The partitioning of H 2 S and CO 2 both in the gas phase and aqueous solution is observed. The numerical models qualitatively reproduce the laboratory experiment.

Numerical results for SO 2 , H 2 S, CH 4 , Ar, O 2 , and N 2 cases

For the same flow conditions, the authors of [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF] performed a series of experiments with different impurities in the feed gas. The experiments were done with 5% of H 2 S, N 2 , SO 2 and CH 4 in the injected stream. The breakthrough of gases was monitored. The experiments show a key role of differential solubility of gases in the feed gas. In Fig. 3, the mole fraction of the impurity gas H 2 S, N 2 , SO 2 and C1 (methane) are normalized by the relevant initial mole fraction of the injected gas (5% for all four tests) in order to emphasize the scale of the gas partitioning effect due to the different solubility relations. We compare the experimental data and numerical results of HYTEC in Fig. 3a. Despite a small mismatch the numerical model confirms the experimental data. Since the curves of relative permeability were fitted only for H 2 S and CO 2 experiments, that may explain difference between numerical and experimental results. These results confirm that • The solubility of the impurity in the injected stream regarding to that of CO 2 is a key factor. The less soluble the impurity gas is, the earlier and higher breakthrough should be expected.

• Classification of impurity gases can be proposed. For example, in the decreasing order of their solubility (13.5 MPa, 61°C, 118950 ppm):

SO 2 > H 2 S > CO 2 > CH 4 > Ar > O 2 > N 2 .
Hence, the gases on the RHS to CO2 of the inequality (from CH 4 to N 2 ) should evolve the similar profile of the normalized mole fraction with high and early peaks at the edge front of the breakthrough gas, and vice versa, SO 2 and H 2 S yield a lower and later breakthrough. To complete the sequence of experiments, we performed the simulations with 5% Ar and 5% O2 in the 95% CO 2 feed gas. Fg. 3b brings together the six cases of the 5% impurity gas in the injected stream.

Injection of impure CO 2 and convective mixing

Problem description

Modeling of CO 2 injection at reservoir scale allows for analysis of the gas plume evolution and undergoing processes. Supercritical CO 2 is injected through a well in a vertically confined long aquifer with a height of 100 m at a depth of 1100 m, see Fig. 4. The injection rate is constant, 10 kg/s; the well radius is 0.3 m; the injection is performed over the whole area of the well during 30 y. Supposing a homogeneous medium, the 2D axisymmetric problem is set: 0.2 of porosity, 10 -12 m 2 of permeability. The Brooks-Corey models [START_REF] Brooks | Hydraulic properties of porous media[END_REF] are chosen to model the capillary pressure and relative permeability with 𝑝 ! = 10 ! Pa, 𝜆 = 2, 𝑆 !" = 0.15, 𝑆 !" = 0.05. The gas and liquid densities are modeled by the PR78 and the T-VTPR, respectively. The gas and liquid viscosities are considered constant: 2.84×10 !! and 5.49×10 !! Pa•s, respectively. The gas and liquid diffusion coefficients are also constant: 1.95×10 !! and 3.36×10 !! m2/s, respectively. The length of the aquifer is 10 km. Length of cells varies from 2 to 1000 m that allows us to reduce the grid dimension to 33,250 cells.

Considering the observations on chromatographic partitioning given in Section 3, we devise two feed gas scenarios:

• 95% CO 2 , 4% N 2 and 1% O 2 and • 95% CO 2 and 5% SO 2 . Though H 2 O (g) can be neglected, it has been added in the chemical system of the problem. Since N 2 and O 2 are less soluble that CO 2 , they can be expected at the edge of the gas current. The gas mixture with these impurities becomes lighter, the density of current drops. This may promote the plume spreading. An opposite effect leads adding SO 2 in the feed gas. Being more soluble that CO 2 , SO 2 spreading should be delayed comparing to CO 2 propagation. The presence of SO 2 makes both the gas current and the formation water with dissolved species heavier. Therefore, a higher convective mixing can be expected that causes CO 2 dissolution.

Numerical results

Fig. 5 shows a gas front evolution and its composition in mole fraction after 30 y of the CO 2 +N 2 +O 2 injection. Gas current has a conventional plume shape, Fig. 5a. Partitioning of CO 2 , N 2 and O 2 is visible: N 2 and O 2 form a noticeable front at the plume edge, Fig. 5b, c andd. This favorable aspect makes them interesting for monitoring usage. H 2 O (g) can indeed be eliminated from the chemical system, Fig. 5d. Partitioning in the liquid phase is also apparent, Fig. 6. The density of the aqueous solution that contains dissolved species (CO 2 , N 2 and O 2 in this case) is higher than the density of the formation water. This evolves instabilities, which initiate under the plume, create convective motion and moreover, enhances dissolution of gas species. Fig. 6 demonstrates CO 2 , N 2 and O 2 rich fingering. An accurate modeling of non-ideal gaseous mixtures and aqueous solution and their thermodynamic properties is required to replicate an adequate plume propagation, its composition, and a representative rate of convective fluxes.

When injecting CO 2 +SO 2 , there is an opposite gas partitioning, Fig. 7. SO 2 motion is delayed because of its higher solubility. CO 2 spreads further than SO 2 in the aqueous phase as well, Fig. 8. Near-well fingers are of a higher SO 2 concentration. SO 2 has a potentially favorable property: SO 2 mixtures have higher density. Its impact both on the gas density and on the liquid density is significant. The effect can be seen in Figs. 9 and 10, where the gas and liquid densities are mapped for both scenarios. The gas current of the CO 2 +SO 2 case is much heavier, especially near the injection well area. Convective mixing is also more pronounced in the CO 2 +SO 2 case, that evolves a higher dissolution rate. A more detailed analysis of convective fluxes is still needed to evaluate it quantitatively. Also, SO 2 can cause a corrosion of well materials and a strong acidification of the formation water.

Conclusions

This work presented a study on the chromatographic partitioning of CO 2 and impurities present in the injected stream in the CCS context. Laboratory and field observations have revealed the chromatographic partitioning phenomenon of CO 2 and impurities both in the gas and in the aqueous phases [START_REF] Bachu | Chromatographic partitioning of impurities contained in a CO2 stream injected into a deep saline aquifer: Part 1. effects of gas composition and in situ conditions[END_REF][START_REF] Wei | Geochemical impact of aquifer storage for impure CO2 containing O2 and N2: Tongliao field experiment[END_REF][START_REF] Ennis-King | The role of heterogeneity in co2 storage in a depleted gas field: history matching of simulation models to field data for the co2crc otway project, australia[END_REF]. Series of laboratory experiments were modeled using the reactive transport HYTEC. Numerical results confirmed the laboratory observations and showed differential breakthrough of injected gases.

A series of experiments on CO 2 and H 2 S mixture with different H 2 S concentration was modeled. Numerical results of HYTEC are in good agreement both with the results given by CMG-GEM and with experimental data.

Another series of dynamic displacement-solubility experiments was modeled to study the chromatographic gas partitioning depending on a type of impurity. Numerical results show that the physics can be modeled both qualitatively and quantitatively. The experiments were carried out for several impurities: H 2 S, CH 4 , N 2 , and SO 2 . Considering the same flow conditions, numerical models for O 2 , Ar were additionally constructed. Next conclusions can be made:

• Solubility of the impurity in the injected stream regarding to that of CO 2 is a key factor. The less soluble the impurity gas is, the earlier and higher breakthrough should be expected.

• Classification of impurity gases can be proposed, in the decreasing order of their solubility (13.5 MPa, 61°C, 118950 ppm): SO 2 > H 2 S > CO 2 > CH 4 > Ar > O 2 > N 2 . Hence, the gases on the RHS to CO2 of the inequality (from CH 4 to N 2 ) should evolve the similar profile of the normalized mole fraction with high and early peaks at the edge front of the breakthrough gas, and vice versa, SO 2 and H 2 S yield a lower and later breakthrough.

• Using accurate models of reactive transport, solubility, phase equilibrium and thermodynamic properties of nonideal mixtures allows reproducing of the chromatographic partitioning: breakthrough time of gases, gas concentration, and front propagation.

Chromatographic partitioning was studied at reservoir scale by modeling two scenarios of impure CO 2 injection over 30 years: 95%CO 2 +4%N 2 +1%O 2 and 95%CO 2 +5%SO 2 . When injecting impurities, the chromatographic partitioning can be observed inside the gas plume and in the aqueous solution. Modeling injection of 95%CO 2 +4%N 2 +1%O 2 demonstrated potential usage of noble gases for monitoring and proved the previous laboratory results. The plume composition strongly depends on a type of the co-injected gas. Moreover, a type of impurity and its concentration change the density of gas current and the density of the formation water with dissolved components. Both densities in the case of 95%CO 2 +5%SO 2 injection are overall higher than those in the 95%CO 2 +4%N 2 +1%O 2 model. This impacts on the buoyancy forces, hence on the distance, velocity and shape of the plume. Since dissolved impurities contribute to the liquid density, it can then accelerate or slow convective dissolution. Heterogeneous gas composition induces density driven motion that can be especially important in case of heavy compounds such as SO 2 .

Modeling multiphase multicomponent flow and reactive transport and accurate thermodynamic modeling of real behavior of mixtures (such as CO 2 , N 2 , O 2 , Ar, SO 2 , CH 4 , H 2 S, H 2 O, H 2 ) can provide insightful understanding of coupled complex physical processes and build confidence in the sustainability of CO 2 storage sites.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Numerical results of the laboratory experiment [3,35] modeled by CMG-GEM (black lines) and HYTEC (colored lines). Injection of a feed gas of 2% H2S and 98% CO2 in a long sand-packed coil. a) Gas saturation evolution. b) Composition in mole fraction of H2S and CO2 in the aqueous phase at 0.5 and 1.2 days.

Fig. 3 .

 3 Fig. 3. a) Mole fraction of the impurity gases, H2S, N2, SO2, C1 (CH4) at the outlet, normalized by the relevant mole fraction in the initially injected gas (5% for all cases), as a function of the pore volume of the total injection. Comparison of experimental data [3] (black lines) and numerical results of HYTEC (colored lines). b) Mole fraction of the impurity gases at the outlet for H2S, N2, SO2, C1 (CH4) complemented by Ar and O2. Numerical results only.

Fig. 4 .

 4 Fig. 4. Schematic of 2D radial problem.

Fig. 5 .Fig. 6 .

 56 Fig. 5. Injection of 95% CO2, 4% N2, and 1% O2. a) Gas saturation map and gas composition in mole fraction of b) CO2(g), c) N2(g), d) O2(g), and e) H2O(g) after 30 y of injection. Rescaled zone of reservoir [3000 x 100] m.

Fig. 7 .Fig. 8 .Fig. 9 .Fig. 10 .

 78910 Fig. 7. Injection of 95% CO2 and 5% SO2. Gas composition in mole fraction: a) CO2(g) and b) SO2(g) after 30 y of injection. Rescaled zone of reservoir [3000 x 100] m.

Table 1 .

 1 Binary interaction parameters 𝑘 !" and partial molar volume at infinite dilution 𝜐 ! ! .

	Compound	𝑘 !,!!!	𝑘 !,!"!	𝜐 ! ! , cm 3 /mol
	CO2	0.199		28.10
	N2	0.428	-0.007	34.53
	O2	0.606	0.114	39.70
	Ar	0.569	0.163	32.92
	CH4	0.506	0.090	36.20
	H2S	0.143	0.097	38.15
	SO2	0.100	0.046	39.76


Alberto Camacho
email: acamacho@cs.toronto.edu

Meghyn Bienvenu
email: meghyn.bienvenu@labri.fr

Sheila A Mcilraith
email: sheila@cs.toronto.edu

Towards a Unified View of AI Planning and Reactive Synthesis

Automated planning and reactive synthesis are wellestablished techniques for sequential decision making. In this paper we examine a collection of AI planning problems with temporally extended goals, specified in Linear Temporal Logic (LTL). We characterize these so-called LTL planning problems as two-player games and thereby establish their correspondence to reactive synthesis problems. This unifying view furthers our understanding of the relationship between plan and program synthesis, establishing complexity results for LTL planning tasks. Building on this correspondence, we identify restricted fragments of LTL for which plan synthesis can be realized more efficiently.

Introduction

In this work we explore and expose the relationship between AI automated planning and reactive synthesis, a class of program synthesis problems. The two seemingly distinct sequential decision making frameworks share a common past in the seminal work on program and plan synthesis via theorem proving (e.g., [START_REF] Green | Application of theorem proving to problem solving[END_REF][START_REF] Nilsson | A mobile automaton: An application of artificial intelligence techniques[END_REF][START_REF] Waldinger | PROW: A step toward automatic program writing[END_REF][START_REF] Fikes | STRIPS: A new approach to the application of theorem proving to problem solving[END_REF])) but diverged as planning research focused on efficient algorithms for classical planning. With growing interest in non-classical planning problems that include non-deterministic actions and temporally extended goals, we reunite these frameworks through the lens of two-player games. This unified view advances our understanding of the relationship between plan and program synthesis, providing us with complexity results for Linear Temporal Logic (LTL) planning and leading to the identification of fragments of LTL for which plan synthesis is more efficient.

Program synthesis from logical specification follows from the classical synthesis problem originally proposed by [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis[END_REF]. Reactive synthesis is a class of program synthesis problems concerned with synthesizing a reactive module that responds to the environment in accordance with a temporal logic specification. O ur c oncern i n t his p aper is with so-called LTL synthesis -reactive synthesis of specifications expressed in LTL. The problem is commonly characterized as a two-player game and has been shown to be 2EXP-complete [START_REF] Pnueli | On the synthesis of a reactive module[END_REF]. More recently LTL synthesis has been extended to specifications in LTL interpreted over finite traces (aka LTL f ) (e.g., [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF]2015;[START_REF] Zhu | Symbolic LTLf synthesis[END_REF]Camacho et al. 2018a;2018b)), and the model has been extended to handle environment assumptions and quality measures [START_REF] Camacho | Finite LTL synthesis with environment assumptions and quality measures[END_REF].

The popularity of LTL is not restricted to program synthesis. Over the past 20 years there has been growing interest in planning with temporally extended goals and preferences specified in LTL. Initial work focused on planning with deterministic actions and LTL goals (and preferences) interpreted over finite traces (e.g., [START_REF] Bacchus | Using temporal logics to express search control knowledge for planning[END_REF][START_REF] Doherty | TALplanner: A temporal logic-based planner[END_REF]Baier and McIlraith 2006a;2006b;[START_REF] Triantafillou | A unifying framework for planning with ltl and regular expressions[END_REF][START_REF] Torres | Polynomial-time reformulations of LTL temporally extended goals into final-state goals[END_REF]) and subsequently infinite traces (e.g., [START_REF] Albarghouthi | On the use of planning technology for verification[END_REF][START_REF] Patrizi | Computing infinite plans for LTL goals using a classical planner[END_REF]). Other work focused on LTL preferences (e.g., [START_REF] Edelkamp | On the compilation of plan constraints and preferences[END_REF][START_REF] Baier | A heuristic search approach to planning with temporally extended preferences[END_REF][START_REF] Coles | LPRPG-P: relaxed plan heuristics for planning with preferences[END_REF][START_REF] Bienvenu | Specifying and computing preferred plans[END_REF])) some of it in the PDDL3.0 (Planning Domain Definition Language) fragment of LTL [START_REF] Gerevini | Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners[END_REF]). More recent work has examined LTL interpreted over both finite and infinite traces in fully-observable non-deterministic (FOND) planning settings (e.g., (De Giacomo, Patrizi, and Sardiña 2010;[START_REF] Patrizi | Fair LTL synthesis for non-deterministic systems using strong cyclic planners[END_REF][START_REF] Camacho | Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces[END_REF][START_REF] De Giacomo | Automata-theoretic foundations of FOND planning for LTLf and LDLf goals[END_REF][START_REF] D'ippolito | Fully observable non-deterministic planning as assumption-based reactive synthesis[END_REF]). We refer to this broad collection of planning problems loosely as LTL Planning Problems.

We are seeing increasing commonalities between the recent work on LTL synthesis and the work on LTL planning, particularly in the FOND setting. Both exploit automata representations of LTL for synthesizing solutions. Further the non-determinism in the FOND setting is closely related to the non-determinism exhibited by the environment in synthesis settings. Finally, we note the growing interest in using planning algorithms for the realization of LTL f and LTL synthesis (Camacho et al. 2018a;2018c;2018d). The correspondence between planning and synthesis has been previously noted (e.g. [START_REF] D'ippolito | Fully observable non-deterministic planning as assumption-based reactive synthesis[END_REF]Camacho et al. 2018b)), and even hybrid models have been proposed (e.g. [START_REF] De Giacomo | Agent planning programs[END_REF]). Opportunities abound from the cross-fertilization between these research areas, which motivated us to develop a unified view of LTL planning and reactive synthesis.

In Section 2 we review LTL and reactive LTL synthesis, and in Section 3 we outline a collection of LTL planning problems in a manner that is amenable to their formulation in terms of structured games. Next, we introduce game structures, providing a characterization of LTL synthesis in terms of structured games, re-establishing complexity results for LTL synthesis in this context, and highlighting the equivalence of winning strategies for these game and solutions to the corresponding LTL synthesis problems. In Section 5, we provide a clear bidirectional mapping between structured games and LTL FOND and show that LTL f FOND can be reduced to LTL FOND and games. Our reductions allow us to obtain complexity results for LTL/LTL f planning that replicate those for games, utilizing notions of combined complexity as well as domain complexity and goal complexity. While the domain complexity of LTL and LTL f FOND planning is the same as for FOND with reachability goals, the overall complexity jumps to double-exponential time as result of the goal. In Section 6, we identify restricted fragments of LTL and LTL f for which plan synthesis has the same worst-case complexity as FOND with reachability goals but which is richer in terms of its expressiveness. We first explore GR(1), a syntactically restricted fragment of LTL for which synthesis can be done in single exponential time. Then we move to the finite case, and revisit the syntax of PDDL3.0 in the context of LTL f FOND planning. In both cases, we show that these compelling and expressive fragments of LTL can be employed without realizing the double exponential complexity of LTL FOND.

The main contributions of this paper are: (i) a unified view of LTL synthesis and various forms of LTL/LTL f plan synthesis in terms of game structures; (ii) complexity results for various LTL/LTL f plan synthesis tasks that decouple the goal and domain complexity, thereby exposing the barriers to efficient algorithms for LTL/LTL f planning and synthesis; (iii) a structure-preserving correspondence between LTL synthesis and LTL/LTL f planning in FOND settings; (iv) identification of fragments of LTL and LTL f for which plan synthesis can be realized more efficiently, including that FOND planning for PDDL3.0 goals is in the same complexity class as FOND planning with final-state goals.

Our theoretical results open the door to combining the benefits of structured planning models and reactive synthesis to specify and perform controller synthesis. Similarly, existing techniques from one field (e.g. LTL synthesis for GR(1) objectives) may be leveraged for the other (e.g. FOND planning with GR(1) goals, for which no dedicated algorithm exists as of yet).

Preliminaries

LTL and Automata

Linear Temporal Logic (LTL) is a propositional modal logic commonly used to express temporally extended properties of state trajectories [START_REF] Pnueli | The temporal logic of programs[END_REF]. The syntax of LTL is defined over a set of propositional variables p ∈ AP, and includes the standard logical connectives and basic temporal operators next ( ϕ) and until (ϕ 1 Uϕ 2 ).

ϕ p | | ⊥ | ¬ϕ | ϕ 1 ∨ ϕ 2 | ϕ 1 ∧ ϕ 2 | ϕ | ϕ 1 Uϕ 2
Other temporal operators are defined in terms of these basic operators, including eventually (♦ϕ := Uϕ), always ( ϕ := ¬♦¬ϕ), release (ϕ 1 Rϕ 2 := ¬(¬ϕ 1 U¬ϕ 2 ))), and weak until (ϕ 1 Wϕ 2 := ϕ 1 ∨ (ϕ 1 Uϕ 2 )). We denote by |ϕ| the size of ϕ, i.e., its total number of symbols.

LTL formulae are evaluated over infinite traces, i.e., infinite sequences s 1 s 2 . . . where each s i ⊆ AP defines a propositional valuation. Intuitively, formula ϕ states that ϕ holds in the next timestep, while ϕ 1 Uϕ 2 states that ϕ 1 needs to hold until ϕ 2 holds. Formally, we say that an infinite trace

π = s 1 s 2 • • • satisfies an LTL formula ϕ if π, 1 | = ϕ, where π, i | = ϕ (i ≥ 1
) is defined recursively as follows:

• π, i | = p iff p ∈ AP and p ∈ s i , • π, i | = ¬ϕ iff it is not the case that π, i | = ϕ, • π, i | = (ϕ 1 ∧ ϕ 2 ) iff π, i | = ϕ 1 and π, i | = ϕ 2 , • π, i | = ϕ iff π, i + 1 | = ϕ, • π, i | = ϕ 1 Uϕ 2 iff there exists a j ≥ i such that π, j | = ϕ 2
and for every k ∈ {i, . . . , j -1}, π, k | = ϕ 1 . We write π | = ϕ when π satisfies ϕ and call π a model of ϕ.

Every LTL formula can be transformed into an equivalent automaton that accepts all and only the models of the formula. Property 1 formulates this result for deterministic parity word automata (DPW) [START_REF] Piterman | From nondeterministic Büchi and Streett automata to deterministic parity automata[END_REF]. A DPW is a tuple A = Σ, Q, q 0 , δ, α , where Σ is a finite alphabet, Q is a finite set of states, q 0 ∈ Q is the initial state, δ : Q×Σ → Q is the transition function, and α : Q → N is the labeling function. The number of different values (also called colours) that α can take is called the index of the automaton. A run of A on an infinite word w = s 0 s 1 • • • ∈ Σ ω is a sequence q 0 q 1 • • • ∈ Q ω where q i+1 = δ(q i , s i ) for each i ≥ 0. We say that a run ρ = q 0 q 1 • • • is accepting when the highest value that appears infinitely often in α(q 0 )α(q 1 ) • • • is even. Finally, the language L(A) of A is the set of words that have an accepting run on A. LTL formulae can be transformed into DPW over the alphabet Σ 2 AP in double-exponential time. Property 1. Given an LTL formula ϕ, a DPW A ϕ that accepts all and only the models of ϕ can be constructed in worst-case double-exponential time in |ϕ|, with the index of A ϕ being worst-case single-exponential in |ϕ|.

In this work, we also consider LTL f , a variant of LTL in which formulae are interpreted over finite traces π = s 1 • • • s n . LTL f inherits the syntax of LTL. A macro final := ¬ is commonly used to indicate the end of the trace. It is important to notice that in LTL f , ¬ ϕ ¬ϕ, but instead we have ¬ ϕ ≡ final ∨ ¬ϕ (here ≡ denotes equivalence for LTL f semantics, i.e., being satisfied by the same finite traces). LTL f can be transformed into finite-word automata (cf. (Baier and McIlraith 2006b)).

Reactive LTL Synthesis

Reactive synthesis is the problem of automatically constructing a reactive module -a system that reacts to the environment with the objective of realizing a given logical specification [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis[END_REF]. In this paper, we are concerned with LTL synthesis, a form of reactive synthesis where the specification is expressed in LTL [START_REF] Pnueli | On the synthesis of a reactive module[END_REF].

Definition 1. An LTL specification is a tuple X, Y, ϕ , where X and Y are disjoint finite sets of variables, and ϕ is an LTL formula over X ∪ Y.

A strategy for an LTL specification X, Y, ϕ is a function σ : (2 X ) + → 2 Y that maps finite sequences of subsets of X into subsets of Y. For an infinite sequence X = X 1 X 2 • • • ∈ (2 X ) ω , the play induced by strategy σ is the infinite sequence

ρ σ,X = (X 1 ∪ σ(X 1 ))(X 2 ∪ σ(X 1 X 2 )) • • • . A play ρ is winning if ρ | = ϕ,
and a strategy is winning when ρ σ,X | = ϕ for all X ∈ (2 X ) ω . Realizability is the problem of deciding whether an LTL specification has a winning strategy, and synthesis is the problem of computing one. Both problems can be solved in double-exponential time [START_REF] Pnueli | On the synthesis of a reactive module[END_REF]:

Theorem 1. LTL realizability is 2EXP-complete.

Plan Synthesis with LTL Goals

Automated planning provides a framework for sequential decision-making in which the agent can interact with the environment according to a prescribed domain theory, and where the objective is to generate a plan whose execution is guaranteed to satisfy a prescribed goal. Planning problems differ in the assumptions they make about the form of the initial state (complete, partial), the transition system (deterministic, non-deterministic, stochastic), the nature of the goal condition, whether the state is (partially) observable during plan execution, the form of the solution or plan (sequence of actions, conditional plan, policy), and whether the execution of that plan is finite or infinite.

Our concern in this paper is with planning problems whose transition systems are non-deterministic and whose goals are temporally extended and as such take the form of constraints on valid executions of the plan. We specify such temporally extended goals in LTL. Plan executions may be finite or infinite. Unless otherwise noted, initial states are complete and plan execution is fully observable. In the rest of this section we review this class of so-called LTL (resp. LTL f ) Planning Problems using notation that will facilitate subsequent characterization in terms of 2-player games. Planning Domain Following [START_REF] Ghallab | Automated Planning and Acting[END_REF], we represent planning domains compactly using a symbolic representation of states, actions, and transitions: Definition 2. A planning domain is a tuple F , A, δ, Poss , where F is a finite set of fluent symbols, A is a finite set of action symbols, Poss ⊆ 2 F × A, and δ : 2

F × A → 2 2 F . The size of the domain is |F |.
The fluents in F denote state properties; we employ a propositional STRIPS representation to parsimoniously represent states as subsets s ⊆ F ; the set of states is S 2 F . We use the term search space to refer to the set S . An action a is applicable in state s if (s, a) ∈ Poss. The function δ describes state transitions, with s ∈ δ(s, a) indicating that state s is a possible result of applying action a in state s.

A strategy for a planning domain D = F , A, δ, Poss is a function σ : (2 F ) + → A ∪ {end} that maps finite state histories to actions, or to end otherwise. 1 Here end is a special symbol, not contained in D, that denotes the termination of a plan. We require strategies to be well defined, that is, for all n ≥ 0, action σ(s 0 ands n+1 ∈ δ(s n , a n ); and(iii) if n = |π|-1, then a n = end. The execution terminates when a n = end. Terminating executions are finite sequences π = (s 0 , a 0 ) • • • (s n , a n ) where n is the first and only index i such that a i = end. Non-terminating executions are infinite, and we write |π| = ∞ . LTL FOND Planning An LTL fully-observable nondeterministic (FOND) planning problem is a tuple D, ϕ I , ϕ G , where D = F , A, δ, Poss is a planning domain, ϕ I is a propositional formula over F that describes a unique state called the initial state (typically given as a complete conjunction of literals), and ϕ G is an LTL formula over F ∪ A. A strategy σ is a solution to an LTL FOND planning problem D, ϕ I , ϕ G if all executions of σ that commence in s 0 | = ϕ I are infinite and satisfy ϕ G . In other words, the objective is to define a non-terminating process that guarantees achievement of the given temporally extended goal, whose satisfaction may depend on the entire execution, rather than just the final state. LTL f FOND Planning We can define LTL f FOND planning problems in exactly the same manner, except that a strategy σ is deemed a solution if all executions of σ that commence in s 0 | = ϕ I terminate and satisfy ϕ G (note that we use LTL f semantics to evaluate ϕ G over the induced finite trace). Thus, the aim is to generate terminating strategies that guarantee satisfaction of the goal. FOND Planning As a special case of LTL f FOND planning, we have (plain) FOND planning, in which the goal takes the form ϕ G = ♦(θ g ∧ final), with θ g a propositional formula over fluents F (typically, a conjunction of fluents). Solutions to FOND planning are policies (rather than arbitrary strategies), but we observe that this restriction does not affect the existence of solutions (cf. Proposition 1). Proposition 1. Any strategy that solves a LTL f FOND planning problem P with goal ϕ G = ♦(θ g ∧ final) can be transformed into a policy that is a solution to P.

• • • s n ) is applicable in s n . A strategy is history-independent if σ(s 0 • • • s n ) = σ(s n ) for each s 0 • • • s n ∈ (2 F ) + . In this case, we call σ a policy. An execution of σ from s 0 ∈ S is a sequence of state-action pairs π = (s 0 , a 0 )(s 1 , a 1 ) • • • such that, for each n < |π|: (i) a n = σ(s 0 • • • s n ); (ii) if n < |π| -1, then a n ∈ A
Planning with Partially Specified Initial States A benefit of describing the initial state by a formula ϕ I is that it allows us to partially specify the initial state. We extend the definitions of LTL / LTL f FOND to allow for ϕ I to describe a family of states, i.e., those that satisfy ϕ I . Solutions to an LTL / LTL f FOND problem D, ϕ I , ϕ G with partially specified initial state ϕ I are defined in the natural way. A strategy σ is a solution to D, ϕ I , ϕ G if σ is a solution to an LTL / LTL f FOND problem D, ϕ I , ϕ G for any complete formula ϕ I that describes a unique initial state, and such that ϕ I | = ϕ I . Informally, σ solves all problems with initial state that satisfies ϕ I . Deterministic LTL / LTL f Planning The preceding problems can be restricted by only considering actions with deterministic effects, i.e., requiring that |δ(s, a)| = 1 for each pair (s, a) ∈ S × A. We refer to this class of problems as deterministic LTL / LTL f planning problems. Complexity of Planning When speaking about the complexity of planning, we focus on the decision problem of plan existence. There are different possible complexity measures depending on which parts of the problem are considered as fixed or varying. In addition to the standard combined complexity measure (in terms of the size of the whole problem), we will consider domain complexity (in terms of the size of the domain, with the goal formula treated as fixed) and goal complexity (in terms of the size of the goal formula, with the domain treated as fixed).

Game Structures

In the previous section, we presented a variety of LTL (resp. LTL f ) planning problems. In this section we review and elaborate on the notion of game structures which we employ to expose and highlight correspondences between these planning problems and LTL synthesis. [START_REF] Piterman | Synthesis of reactive(1) designs[END_REF] studied the problem of computing winning strategies for so-called game structures (see Definition 3). Intuitively, a game structure is similar to an LTL specification. The difference is that the moves of the players (system and environment) in a game structure are assumed to be constrained by the rules of the game. Solutions are system strategies that guarantee achievement of a winning condition ϕ, under the assumption that both players act as mandated by the rules described by θ e , θ s , ψ e , and ψ s . Definition 3. A game structure is a tuple G = X, Y, θ e , θ s , ψ e , ψ s , ϕ , where:

• X is a finite set of environment variables.

• Y is a finite set of system variables, disjoint with X.

• θ e is a propositional formula over X.

• θ s is a propositional formula over X ∪ Y. • ψ e is a propositional formula over X ∪ Y ∪ X. • ψ s is a propositional formula over X ∪ Y ∪ X ∪ Y. • ϕ is an LTL formula over X ∪ Y (the winning condition) with X = { x | x ∈ X} and Y = { y | y ∈ Y}.
The environment player moves first in each turn, and inputs a subset of the X variables. In response, the system player outputs a subset of Y variables. The moves X n ⊆ X and Y n ⊆ Y in the n-th turn constitute a game configuration, or state s n = X n ∪ Y n . We shall use the term search space to refer to the set of all such states and observe that its size is singly exponential in |X| + |Y|. The structure of the game constrains the players' moves. The LTL formula ψ e relates the values of X n , Y n , and X n+1 and states how the environment is allowed to respond to a state s n . Similarly, the LTL formula ψ s relates the values of X n , Y n , X n+1 , and Y n+1 , and states how the system can react to the environment given the previous state. Formulas θ e and θ s have similar purposes, serving to constrain the players' initial moves.

A play of the game G is a maximal (possibly infinite) sequence of states, ρ = s 0 s 1 • • • , such that: (i) s 0 is an initial state, i.e., s 0 | = θ e ∧ θ s ; and (ii) for each n > 0, s n is a successor of s n-1 , i.e. (s n-1 , s n ) | = ψ e ∧ ψ s . The system player aims to generate a play that satisfies the winning condition ϕ. Formally, a play ρ is winning for the system if either (i) ρ = s 0 • • • s n is finite and there is no s n+1 such that (s n , s n+1 ) | = ψ e (i.e., the environment has no legal move); or (ii) ρ is infinite and ρ | = ϕ.

Game strategies are defined as for LTL synthesis. Namely, a strategy for the system player is a function σ : (2

X ) + → 2 Y . A play ρ = (X 0 ∪ Y 0 )(X 1 ∪ Y 1 ) • • • is σ-compliant if Y n = σ(X 0 • • • X n ) at each n < |ρ|.
We say σ is a winning strategy for the system player if all σ-compliant plays are winning. Winner determination is to decide whether such a winning strategy exists, and by solving the game, we mean the task of producing such a strategy. Game Structures and LTL Synthesis The LTL synthesis and structured game problems are interreducible: structured games can be reduced to LTL synthesis where all the structure is embedded into the LTL objective (Theorem 2); conversely, any LTL specification formula can be converted into an equivalent game with no structural constraints (Proposition 2). We should emphasize that Theorem 2 was originally formulated for syntactically restricted formulae (in the GR(1) fragment, discussed in Section 6.1), but the result naturally extends to arbitrary LTL formulae. The Temporal Logic Synthesis Format (TLSF) is a high-level description format for LTL synthesis [START_REF] Jacobs | A high-level LTL synthesis format: TLSF v1.1[END_REF]. TLSF specifications are described in terms of the components of a structured game. TLSF can be interpreted under two different semantics, so-called strict or alternatively standard semantics. The reduction in Theorem 2 corresponds to the strict semantics. Theorem 2 (adapted2 and extended from [START_REF] Klein | Revisiting synthesis of GR(1) specifications[END_REF][START_REF] Bloem | Synthesis of reactive(1) designs[END_REF])). The system wins the game G = X, Y, θ e , θ s , ψ e , ψ s , ϕ iff X, Y, ϕ G is realizable, where:

ϕ G (θ e → θ s ) ∧ (θ e → (ψ s W¬ψ e )) ∧ (( ψ e ∧ θ e ) → ϕ))
Moreover, the transformation preserves winning strategies.

We now show how LTL synthesis corresponds to a special case of structured games: Proposition 2. A strategy is winning for the LTL synthesis problem X, Y, ϕ iff it is a winning strategy for the corresponding structured game X, Y, , , , , ϕ Solving Structured Games As the reduction from Theorem 2 preserves winning strategies, it provides a way to solve games via reduction to LTL synthesis and to derive the following complexity results: Theorem 3. Structured games can be solved in doubleexponential time, and the winner determination problem for structured games is 2EXP-complete.

In what follows, we present an alternative way to solve games that exploits their structure and allows us to obtain more fine-grained complexity results in terms of the size of the search space and winning condition (Theorem 4). These results extend similar results to games in a restricted fragment of LTL, which we will revisit in Section 6.1.

The classical approach to LTL realizability reduces the specification to a parity game, and constructs a strategy via fixpoint computation (e.g. [START_REF] Pnueli | On the synthesis of a reactive module[END_REF]). This approach can be straightforwardly adapted to solve structured games G = X, Y, θ e , θ s , ψ e , ψ s , ϕ . We revisit here the main steps. The interesting thing to notice is that the procedure decouples the role of the winning condition and the search space within the game complexity.

1. Transform ϕ into a DPW A ϕ 2. Construct a parity game G = A ϕ ||G

Compute a winning strategy for G

The first step computes a DPW A ϕ , in worst-case double exponential time in |ϕ|, that recognizes the models of ϕ. The index d of A ϕ (i.e., number of colors) is, at most, exponential in |ϕ|. In the second step, a product parity game G = A ϕ ||G is constructed that integrates the dynamics of A ϕ and G in parallel. In the context of this paper, a parity game may be viewed as a structured game with a parity winning condition, in place of an LTL formula, to evaluate which infinite plays are winning. Parity games are played on a finite graph whose nodes represent game states. The dynamics of the game alternates between system' and environment' nodes. The nodes associated with the turn of the environment player are labeled with tuples (q, X, Y), where q is a DPW state, X ⊆ X, and Y ⊆ Y. Intuitively, q keeps track of the run of A ϕ on a partial play ρ = s 0 s 1 • • • s n , and X and Y are the components of state s n . Similarly, the nodes associated with the turn of the system player are labeled with tuples (q, X, Y, X ) that keep track of the run of A ϕ on ρ followed by the environment's move X . The colour of a node is the colour of the DBW state in the node's label, and the index of G is the highest colour among all its nodes. The edges of the tree connect nodes in the natural way whenever both players have been following the rules of the structured game. Edges (q, X, Y) X --→ (q, X, Y, X ) reflect an environment's move, X , and edges (q, X, Y, X ) Y -→ (q , X , Y ) reflect a system's move, Y , with q = δ(q, X ∪ Y ). Additional edges are included to handle illegal moves of the structured game G. Environment moves that violate ψ e are captured by edges that point to a dummy node, q . More precisely, (q, X, Y) X --→ q whenever (X ∪Y)(X ) | = ψ e . Similarly, edges to a dummy node q ⊥ handle system moves that violate ψ s , i.e., (q, X, Y, X )

Y -→ q ⊥ whenever (X ∪ Y)(X ∪ Y ) | = ψ s .
We shall assign colour 0 to q , and 1 to q ⊥ . Both q and q ⊥ are sink nodes, meaning that outgoing edges are all self-loops. The root node of the game is labeled with (q 0 , , ), with q 0 being the initial state of the DBW. The root node has no play history associated to it. Its outgoing edges correspond to environment moves X and transition to nodes with labels of the form (q 0 , , , X) whenever X | = θ e , and to q otherwise. Similarly, nodes with labels of the form (q 0 , , , X) transition to nodes with labels of the form (q , X, Y) whenever X ∪Y | = θ s , and to q ⊥ otherwise. This construction preserves winner determination, and a winning strategy for G can be extracted from a winning strategy for G .

In the third step, a winning strategy for G can be computed in O(e • n d ), where e is the number of edges, n is the number of nodes, and d is the index of G [START_REF] Zielonka | Infinite games on finitely coloured graphs with applications to automata on infinite trees[END_REF]). In the parity game G described above, the number of nodes -as well as the number of edges -is polynomial on |X|+|Y|) , and G has the same index of A ϕ , which is exponential in |X| + |Y| (w.l.o.g., we assume A ϕ has index greater than zero). The following result follows:

|A ϕ | • 2 O(
Theorem 4. Structured games can be solved in doubleexponential time in the size of the winning condition, and in polynomial time in the size of the search space.

Plan Synthesis and Structured Games

The correspondence between planning and game structures has been noted in the past. De Giacomo et al. ( 2010) constructed a reduction of FOND planning with final-state goals into game structures. Here, we extend those results to LTL FOND and LTL f FOND planning.

We provide a clear bidirectional mapping between structured games and LTL FOND planning (Sections 5.1 and 5.2), and then show that LTL f FOND planning can be reduced to LTL FOND and games (Section 5.3). Our reductions allow us to obtain complexity results for LTL/LTL f planning that replicate those for games.

Structured Games as LTL FOND Planning

We begin by presenting a reduction of structured games to LTL FOND planning. Intuitively, we model the moves of the system by means of planning actions, and the response of the environment by means of non-deterministic action effects.

Let G = X, Y, θ e , θ s , ψ e , ψ s , ϕ be a game structure. We assume for now that θ e is satisfiable and defines a complete truth assignment to the variables X, returning later to the general case. We construct an LTL FOND planning problem

P G = D, ϕ I , ϕ G with domain D = F , A, δ, Poss and F X ∪ Y ∪ X ∪ x init , x end , x end , a end A {A | A ⊆ Y} ∪ a end ϕ I x init ∧ ¬x end ∧ ¬x end ∧ ¬a end ∧ θ e ϕ G ♦x end ∨ ϕ
Note that we use V {v | v ∈ V} to denote a set of primed variables (and similarly, use θ e for θ e with all variables now primed). Planning states keep track of the last game state. Intuitively, primed variables serve to indicate the moves performed by each player in the current turn, whereas unprimed variables indicate the last game state.

The set Poss ⊆ 2 F × A consists of all pairs (X

1 ∪ A 1 ∪ X 2 , A 2 ) such that X 1 ⊆ X ∪ {x init , x end }, X 2 ⊆ X ∪ {x end }, A 1 , A 2 ⊆ Y ∪ {a end }, and • X 1 | = x init ∧ ¬x end and (X 2 ∪ A 2 ) | = θ s , or • X 1 , X 2 ⊆ X, A 1 , A 2 ⊆ Y, and (X 1 ∪ A 1 )(X 2 ∪ A 2 ) | = ψ s , or • X 2 | = x end and A 2 = {a end }
The initial state ϕ I simulates the initial move of the environment, determined by the (unique, by assumption) interpretation of X variables that make θ e true. We now define how δ simulates the moves of the environment in response to the moves of the system. Intuitively, the non-determinism in δ allows the environment to make a legal move, or otherwise transition to {x end }. Formally, if X 1 , X 2 ⊆ X, and A 1 , A 2 ⊆ Y, then δ is defined by:

δ(X 1 ∪ A 1 ∪ X 2 , A 2 ) X 2 ∪ A 2 ∪ X 3 | X 3 = {x end } ∪ X 2 ∪ A 2 ∪ X 3 | X 3 ⊆ X and (X 2 ∪ A 2 )(X 3 ) | = ψ e
We simulate that the environment makes an illegal move by assigning X 3 = {x end }, and force the dynamics to enter a loop in which only action a end can be applied:

δ(X 1 ∪ A 1 ∪ {x end }, {a end })
{{x end , a end , x end }}. Those simulated executions satisfy ♦x end . Note that executions that satisfy ϕ are in correspondence with plays that satisfy the winning condition, ϕ. The one-timestep offset in ϕ is needed because ϕ is evaluated over unprimed variables, and those are delayed by one timestep in the construction of the problem.

In the general case, with generic θ e , our reduction can be extended with a dummy action, only applicable in a new dummy initial state, that transitions non-deterministically into one of the states that satisfy x init ∧ ¬x end ∧ ¬x end ∧ ¬a end ∧θ e , or x end . The new goal becomes ϕ G ♦x end ∨ ϕ, with the additional next operator being introduced to reflect the extra initial timestep. The reduction is polynomial, as it transforms a game G into an LTL FOND problem P G with a polynomial increase in the size of the search space. Winning strategies to G can be extracted directly from solutions to the reduced LTL FOND problem.

Theorem 5. A structured game with winning condition ϕ can be reduced to an LTL FOND planning problem with goal ϕ G ♦x end ∨ ϕ, with a polynomial increase in the size of the search space.

LTL FOND Planning as Structured Games

To complete the bidirectional mapping, we provide a reduction from LTL FOND planning into structured games. For an LTL FOND planning problem P = D, ϕ I , ϕ G with domain D = F , A, δ, Poss we construct a game G P = X, Y, θ e , θ s , ψ e , ψ s , ϕ G , where X F , Y A, and:

θ e ϕ I ψ e s∈2 F a∈A s ∈δ(s,a) (τ(s) ∧ a ∧ (τ(s ))) θ s         ϕ one A ∧ (s,a)∈Poss τ(s) ∧ a         ψ s         ϕ one A ∧ (s,a)∈Poss τ(s) ∧ a        
Consistent with our notation for planning, we use s for subsets of F and A for subsets of A. We let τ(s) f ∈s f ∧ f ∈F \s ¬ f and set ϕ one A a∈A a ∧ a,a ∈A,a a ¬(a ∧ a ). Note that in ψ e and ψ s , we use in front of arbitrary propositional formulas, but by pushing down to the fluents and actions, we obtain formulae of the required form.

The components of G P mimic the dynamics of P, according to the semantics discussed in Section 4. In the game G P , the environment controls the fluents (X F ), and the system controls the actions (Y A). The formulas ψ e and ψ s reproduce the state transition model in D. Formula ψ e checks whether state s in a sequence (s ∪ A)(s ∪ A ) of two consecutive game states is a legal move of the environment player, relative to s and A -assuming that previous moves of each player respected the dynamics of the game. This occurs when s ∈ δ(s, a). Formula ψ s checks whether A ⊆ A is a legal move of the system player, relative to s, A, and sassuming that previous moves of each player respected the dynamics of the game. This occurs when (i) A contains a single action; and (ii) action a ∈ A is applicable in s . Finally, formulas θ e and θ s are assertions over X and X ∪ Y, respectively, and check that the initial move of the environment and system players is legal -that is, the environment sets the initial state to ϕ I , and the system responds with an action that is applicable in the initial state. The auxiliary formula ϕ one

A ensures that exactly one action symbol holds in each game position, making it possible to translate winning game strategies into solutions. Note that our reduction does not require ϕ I to define a unique state. Theorem 6. Plan existence of an LTL FOND planning problem P can be reduced to winner determination of the game structure G P and, by extension, to LTL realizability of ϕ P

(θ e → θ s ) ∧ (θ e → (ψ s W¬ψ e )) ∧ (( ψ e ∧ θ e ) → ϕ G )) Furthermore, the reduction is such that solutions can be directly extracted from winning strategies.

Encoding STRIPS Models When we represent planning problems with propositional STRIPS-like models, formulas ψ e and ψ s can be written more compactly, as follows:

ψ eff a a → e∈Eff a         f ∈Adde f ∧ f ∈Dele ¬ f ∧ f ∈F\Adde∪Dele f ↔ f         ψ e a∈A ψ eff a θ s         ϕ one A ∧ a∈A         ¬a ∨ p∈Prea p                 ψ s θ s
Observe that ψ eff a captures both the positive and negative effects of non-deterministic action a, as well as frame assumptions -that the truth value of every other fluent, not affected by the action a, stays the same. In particular, formulae f ∈F\Add e ∪Del e f ↔ f capture the frame axioms for effect e ∈ Eff a . We can write these as successor state axioms to realize a more parsimonious solution to the frame problem [START_REF] Reiter | Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems[END_REF]. Complexity Analysis Our reduction of LTL FOND planning into structured games conveniently decouples the domain from the goal formula. This allows us to characterize the complexity of LTL FOND planning in terms of these two components and obtain analogous results to those in game structures (cf. Theorem 4), The same complexity results have been independently obtained very recently (available on arXiv, [START_REF] Aminof | Planning and synthesis under assumptions[END_REF])) with a different approach. Theorem 7. Plan existence in LTL FOND planning is EXPcomplete in domain complexity, and 2EXP-complete for goal and combined complexity. Proof sketch. Membership follows from the reduction to games in Theorem 6 and results in Theorem 4. Hardness is obtained by reducing LTL f FOND into LTL FOND (see Lemma 1), and then applying the hardness results for LTL f FOND from (De Giacomo and Rubin 2018).

Remark 1. The results in Theorems 6 and 7 also apply to LTL FOND planning with partially specified initial states.

LTL f FOND Planning as Structured Games

It is also possible to reduce LTL f FOND planning to structured games. We show this by reducing LTL f FOND to LTL FOND, from which Theorem 6 can be applied. The reduction of an LTL f FOND problem P = D, ϕ I , ϕ fin with domain D = F , A, δ, Poss is an LTL FOND problem D , ϕ I , ϕ inf whose domain, D F , A , δ , Poss , has symbols F F ∪ {alive} and A A ∪ {a end }. The dynamics of D simulate plan executions in D. Symbol a end indicates that the simulated plan execution has terminated, and symbol alive indicates the opposite. Formally:

Poss {(s ∪ {alive} , a) | (s, a) ∈ Poss} ∪ (s, a end ) | s ∈ 2 F δ (s, a) {s ∪ {alive}} s ∈δ(s\{alive},a) if a a end and s | = alive {∅} otherwise
The new initial state is given by ϕ I ϕ I ∧ (alive). Finally, LTL goal formula ϕ inf tr(ϕ fin ) ∧ ♦¬(alive) is obtained by applying the following polynomial transformation to ϕ fin :

tr(p) = p tr(¬ϕ) = ¬tr(ϕ) tr(ϕ 1 ∧ ϕ 2 ) = tr(ϕ 1 ) ∧ tr(ϕ 2 ) tr( ϕ) = (alive ∧ tr(ϕ)) tr(ϕ 1 Uϕ 2 ) = tr(ϕ 1 )U(alive ∧ tr(ϕ 2 ))
Intuitively, an infinite trace π satisfies ϕ inf iff alive is false at some point, and the finite prefix π in which alive is true simulates a finite trace that satisfies ϕ fin . The preceding transformation is based on the transformations found in [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF][START_REF] Camacho | Finite LTL synthesis with environment assumptions and quality measures[END_REF], but fixes some minor mistakes and makes some simplifications by leveraging the dynamics induced by a end .

The transformation preserves plan existence (Lemma 1). Moreover, solutions σ fin to the LTL f FOND planning problem can be easily defined from solutions σ inf to the LTL FOND planning reduction as σ fin (s 0

• • • s n ) σ inf (s 0 • • • s n ),
where primed states are augmented with predicate alive, and execution terminates (end) whenever σ inf outputs a end .

Lemma 1. Plan existence of an LTL f FOND planning problem D, ϕ I , ϕ fin can be polynomially reduced to plan existence of an LTL FOND planning problem D , ϕ I , ϕ inf .

Combining Lemma 1 and Theorem 6 yields: Theorem 8. Plan existence of an LTL f FOND planning problem P can be reduced to winner determination of a game structure and, by extension, to LTL realizability.

Encoding STRIPS Models With a propositional STRIPSlike representation of the planning problems, the translation of a domain D with symbols F , A produces a new domain, D , with symbols F F ∪ {alive} and A A ∪ {a end }. Action a end has preconditions Pre a end {alive} and a deterministic effect, Eff a end = { ∅, F }, that deletes all fluents. Actions in A are updated to incorporate symbol alive in their preconditions.

Remark 2. The results in Lemma 1 and Theorem 8 apply to LTL f FOND planning with partially specified initial states.

Complexity Analysis Complexity results for LTL f FOND planning (with unique initial state) were recently published by De Giacomo and Rubin (2018). Membership can be easily deduced from our reductions. We extend their result to LTL f FOND planning with partially specified initial states. Interestingly, the complexity of LTL f FOND replicates that of LTL FOND. The same phenomenon occurs in LTL and LTL f synthesis, both being 2EXP-complete problems [START_REF] Pnueli | On the synthesis of a reactive module[END_REF][START_REF] De Giacomo | Synthesis for LTL and LDL on finite traces[END_REF]. Theorem 9. Plan existence for LTL f FOND with partially specified initial states is EXP-complete in domain complexity, and 2EXP-complete in goal and combined complexity. Proof sketch. Hardness results follow from (De Giacomo and Rubin 2018). Membership follows from our reductions (cf. Lemma 1, Theorem 7, and Remarks 1 and 2).

6 More Efficient LTL/LTL f Plan Synthesis

In the previous sections, we formalized the connection between LTL synthesis, game structures, and various forms of planning. By doing so, we derived complexity results for planning that mimic those in LTL synthesis and games. While the domain complexity of LTL and LTL f FOND planning is the same as for FOND with reachability goals, the overall complexity jumps to double-exponential time.

The aim of this section is to identify restricted fragments of LTL and LTL f for which plan synthesis has the same worstcase complexity as FOND with reachability goals but which is richer in terms of its expressiveness. We first explore GR(1), a syntactically restricted fragment of LTL for which synthesis can be done in single-exponential time. Then we move to the finite case, and revisit the syntax of PDDL3.0 in the context of LTL f FOND planning.

GR(1) Synthesis and Game Structures

Generalized Reactivity (1) (GR(1) for short) is a fragment of LTL that has been studied in the context of synthesis and games for its computational advantages. Inconsistent use of terminology in the literature has created some confusion regarding what the GR(1) fragment is, how GR(1) synthesis differs from GR(1) games, and the complexity of these tasks. We provide a brief historical overview, with the aim of clarifying each of these concepts as we understand them.

The GR(1) fragment of LTL was originally introduced by Piterman, [START_REF] Piterman | Synthesis of reactive(1) designs[END_REF], and comprised the fragment of LTL formulae in the syntactic form

i∈I ♦α i → j∈J ♦β j
where α i and β j are propositional formulae. GR(1) synthesis can be done with exponentially lower worst-case complexity than general LTL synthesis (Theorem 10). Theorem 10 ( [START_REF] Piterman | Synthesis of reactive(1) designs[END_REF]. Synthesis of specifications X, Y, ϕ with GR(1) formula ϕ can be done in exponential time on the number of variables in ϕ.

Piterman et al. studied the problem of computing winning strategies for so-called GR(1) games, that is, game structures with GR(1) winning condition. They provided a first reduction from GR(1) games into standard assume-guarantee LTL synthesis. That reduction contained a fundamental flaw that produced false unrealizable specifications. The flaw was detected and corrected by [START_REF] Klein | Revisiting synthesis of GR(1) specifications[END_REF], and subsequently included in [START_REF] Bloem | Synthesis of reactive(1) designs[END_REF] in the form given in Theorem 2, namely:

(θ e → θ s ) ∧ (θ e → (ψ s W¬ψ e )) ∧ (( ψ e ∧ θ e ) → ϕ))

Similar to GR(1) synthesis, GR(1) games can be solved with exponentially lower hardness bounds than for general LTL winning conditions. Perhaps better known than Theorem 11 is the tractability result for GR(1) games in Corollary 1. It is worth noting that the polynomial time bounds are only valid when the size of the game search space is fixed. Theorem 11. [START_REF] Bloem | Synthesis of reactive(1) designs[END_REF]] GR(1) games with winning condition ϕ can be solved in polynomial time on the size of the search space, and exponential time in the number of variables in ϕ. Corollary 1. For a fixed search space, GR(1) games can be solved in polynomial time.

Despite the fact that GR(1) is a syntactically restricted fragment of LTL, many non-GR(1) properties can be captured by GR(1) games by adding extra control variables. [START_REF] Maoz | GR(1) synthesis for LTL specification patterns[END_REF] gave a method to reduce LTL realizability into winner determination for a GR(1) game. The approach works for any LTL formula that can be transformed into deterministic Büchi word automata (DBW). This is the case for 54 out of the 56 industrial patterns listed in [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF], highlighting the strong appeal of the GR(1) fragment for practical applications. The construction first takes an LTL description of the pattern and transforms it into a DBW. In a second step, an LTL formula is constructed with extra controllable variables -one per automaton state -that capture the Büchi acceptance condition. The syntactic form of the formula makes it possible to apply existing methods that reduce LTL realizability to winner determination of a GR(1) game.

Planning with GR(1) Goals

The advantageous computational properties of the GR(1) fragment for game structures also manifest in LTL FOND planning (Theorem 13). This is because there exists a bidirectional mapping between game structures and LTL planning when the goal and winning condition is a GR(1) formula: GR(1) games can be reduced to LTL planning with GR(1) goals and, conversely, LTL planning with GR(1) goals can be reduced to GR(1) LTL planning. Theorem 12. GR(1) games can be polynomially reduced to LTL FOND planning with GR(1) goals, and vice versa. Proof sketch. For the first direction, we employ the reduction from Theorem 5. Observe that ϕ G ♦x end ∨ ϕ is equivalent to ϕ G ♦x end ∨ ϕ when ϕ = i∈I ♦α i → j∈J ♦β j is a GR(1) formula. Further observe that, for the constructed planning problem, an execution satisfies ♦x end iff it satisfies ¬ ♦¬x end . This is because x end cannot be made false once it has been made true. By means of syntactic manipulation, we can further show that an execution satisfies ϕ G iff it satisfies the GR(1) formula ♦¬x end ∧ i∈I ♦α i → j∈J ♦β j . For the second statement, we can reuse the reduction underlying Theorem 6, as it does not modify goal formulae.

Theorem 13. Plan existence for LTL FOND planning problems with GR(1) goals is EXP-complete in domain and combined complexity, and in PTIME w.r.t. goal complexity (i.e., when the domain is fixed).

Proof sketch. Membership results are obtained by combining Theorems 11, 12, and Corollary 1. The EXP lower bound follows from the EXP-hardness of FOND and the fact that reachability goals can encoded using GR(1) formulae.

The results in Theorem 13 can be extended to the finite case: plan synthesis of FOND problems with LTL f goal in GR(1) syntactic form can be done in exponential time. Unfortunately, this result is not very interesting because LTL f FOND planning with GR(1) goals is equivalent to FOND planning with final-state goals.

Property 2. The GR(1) syntactic fragment of LTL f is equally expressive as the syntactic fragment of formulas of the form ♦(θ ∧ final) for some propositional formula θ.

Proof. Satisfaction of GR(1) LTL f formula i∈I ♦α i → j∈J ♦β j is equivalent to satisfaction of LTL f formula ♦(θ ∧ final) with θ = i∈I α i → j∈J β j . Conversely, sat- isfaction of LTL f formula ♦(θ ∧ final) is equivalent to satis- faction of GR(1) LTL f formula ♦ → ♦θ.

Request-Response Planning

We propose here the class of request-response formulas: a syntactic class that appear to be a reasonable counterpart to GR(1) in the finite case, as it captures similar patterns. Request-response formulas take the form (α → ♦β), for some propositional formulas α and β. Request-response LTL formulas can be transformed into GR(1) LTL formulas that capture the same patterns, possibly with introduction of two extra variables using [START_REF] Maoz | GR(1) synthesis for LTL specification patterns[END_REF]'s technique. Therefore, LTL games, synthesis, and planning for request-response LTL formulas can be polynomially reduced into their GR(1) counterparts. In contrast to GR(1), requestresponse LTL f formulas are more expressive than final-state goals when interpreted over finite traces.

We omit the proof of Theorem 14, as it can be obtained from the more general Theorem 15.

Theorem 14. Plan existence for LTL f FOND with requestresponse goal formulas is EXP-complete for domain and combined complexity, and in PTIME for goal complexity.

Planning with PDDL3.0 Goals

The Planning Domain Definition Language (PDDL) is a globally accepted language used to describe planning problems. Different variants of PDDL exist that allow for e.g. durative actions and conditional effects. PDDL3.0 [START_REF] Gerevini | Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners[END_REF]), which we abbreviate to PDDL3, extends the language of PDDL with the modal temporal operators listed in Table 1, to be interpreted over finite traces. We included equivalent LTL f formulae, as shown in [START_REF] Gerevini | Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners[END_REF][START_REF] De Giacomo | Reasoning on LTL on finite traces: Insensitivity to infiniteness[END_REF]. We provided corrected versions for the operators hold-during and hold-after. We also simplified the formula for sometime-before and at-most-once. The syntax of PDDL3 does not allow nesting of modal operators, and is limited to conjunctions of modal operators and literals. Despite its restricted syntax, PDDL3 temporal operators subsume GR(1) and request-response formulas. In this paper, all PDDL3 formulae apply PDDL3 modal operators to propositional formulae, but note that PDDL3 also allows for a lifted syntax.

modal operator equivalent LTL f size of DFA (at-end θ) ♦(θ ∧ final) 2 (always θ) θ 3 (sometime θ) ♦θ 3 (sometime-after θ 1 θ 2 ) (θ 1 → ♦θ 2 ) 3 (sometime-before θ 1 θ 2 ) θ 2 R¬θ 1 4 (at-most-once θ) (¬θ)W(θW( ¬θ)) 5 (within n θ) 0≤i≤n i θ n + 3 (always-within n θ 1 θ 2 ) (θ 1 → 0≤i≤n i θ 2 ) n +
Relation with Request-Response formulas Requestresponse formulas (p → ♦q) correspond to PDDL3 operator (sometime-after p q). Relation with GR(1) formulas When interpreted over finite traces, GR(1) formulas i ♦α i → j ♦β j are equivalent to PDDL3 operator (at-end θ), with θ = i α i → j β j .

Relation with FOND planning FOND planning with finalstate goals is a special case of FOND planning with PDDL 3 goals in the form (at-end θ). Solutions in the form of a policy can be constructed from strategies (cf. Proposition 1).

Reduction to Structured Games FOND planning with PDDL3 goals can be reduced to LTL f FOND by rewriting PDDL3 operators in LTL f , as indicated in Table 1.

Complexity Analysis

The following theorem clarifies the complexity of FOND planning with PDDL3 goals, which to the best of our knowledge has not yet been considered in the literature. The formulation is a bit more involved than earlier results due to the use of numeric values in some of the PDDL3 temporal operators.

Theorem 15. Assuming a unary encoding of numbers in PDDL3 modal operators, plan existence for FOND planning with PDDL3 goals is EXP-complete for domain and goal complexity, and the goal complexity is in PTIME provided that there is a bound on the number of conjuncts in the goal that use numeric temporal operators.

Proof sketch. FOND planning with PDDL3 goals can be reduced to LTL f FOND (cf. Table 1). LTL f FOND planning can be reduced to solving a DFA game3 following a similar technique as in Section 5.2. The game DFA is the product of (i) a DFA encoding the transition system (which is exponential, (ii) multiple DFA, one per PDDL3 operator in the goal formula. The former DFA is of exponential size in the domain, and each of the latter DFAs is of polynomial size (see third column of Table 1), assuming a unary representation of numeric values. The product DFA is thus of exponential size, and if the domain is fixed, the restriction on the number of numeric conjuncts suffices to obtain a polynomial-size DFA. We conclude by recalling that DFA games can be solved in polynomial time in the size of the DFA (see e.g. [START_REF] Camacho | Finite LTL synthesis with environment assumptions and quality measures[END_REF]).

Summary and Discussion

Synthesizing strategies for software agents is a central problem in artificial intelligence. In this work, we made a step towards reconciling two different perspectives that address this problem: AI planning and LTL synthesis.

Our work contributes with principled, bidirectional mappings between so-called LTL FOND planning, two-player games, and reactive LTL synthesis. By means of these mappings, we were able to revisit well-known complexity results in LTL and LTL f FOND planning, and derive new ones.

A further contribution was the identification of restricted forms of LTL and LTL f FOND planning for which plan synthesis can be realized more efficiently than in the general case. For LTL FOND planning, we derived results for GR(1) goals that are analogous to so-called GR(1) games. For the finite-trace setting, we provided novel complexity results for LTL f FOND planning with PDDL3.0 goals and observed that, over finite traces, its expressivity subsumes other fragments including GR(1). These results show that LTL FOND and LTL f FOND plan synthesis can be performed with the same computational complexity as traditional FOND planning with final-state goals, but utilizing a richer class of temporally extended goal formulae.

Table 1 :

 1 PDDL3 modal temporal operators, equivalent LTL f formulae, and size of the corresponding minimal DFA. Nested operators are abbreviated with a superindex. Operator weak-next ( ) is defined as ϕ final ∨ ϕ. We provide corrected LTL f formulae for operators tagged with * .

	3

History-dependent strategies are often represented compactly in form of finite-state controllers (cf.(Patrizi, Lipovetzky, and Geffner

2013;[START_REF] Camacho | Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces[END_REF]).

The formula in[START_REF] Bloem | Synthesis of reactive(1) designs[END_REF]) makes uses future and past temporal operators. Here, we use an equivalent formula with only future temporal operators (cf.[START_REF] Jacobs | A high-level LTL synthesis format: TLSF v1.1[END_REF]).

In the context of this paper, DFA games can be seen as structured games where the winning condition is given by the acceptance of DFA.

Acknowledgements

We gratefully acknowledge funding from the Natural Sciences and Engineering Research Council of Canada (NSERC) and Microsoft Research.