Thierry Authié

Mickael Dall'orso

Sébastien Trilles

H Choi

H Kim

J Lee

E Lee

G Nam

Performances Monitoring and Analysis for KASS

The Korea Augmentation Satellite System (KASS) is the future SBAS of the Republic of Korea. It is developed by the Korea Aerospace research Institute (KARI) for the government of the Republic of Korea, and Thales Alenia Space is the industry prime contractor of this development. The function of the KASS is to decompose all possible range error sources and to distribute corrections and/or alerts to its users by means of geostationary satellites.

The KASS Processing Station (KPS) is the component of KASS in charge of computing the orbit, clock and ionosphere correction and alert information (below 'Navigation Overlay Frame', NOF) using data from a set of reference stations. The KPS is composed of two independent elements: the Processing Set (PS) and the Check Set (CS). The first element is responsible of computing the complete navigation context for the GNSS constellation (orbits and clock) and the ionosphere model, then to prepare and send the NOF to be broadcast to the users. The second element acts as a super user by applying the NOF to the GPS messages checking that this is consistent with an independent set of measurement to control and insure the integrity.

The KPS-PS component plays a key role in the KASS performance achievement where the APV-1 service level is required. To feed the KPS, the KASS has specific KASS Reference Station (KRS) located on the Rep. of Korea land masses. Compared to other SBAS, this leads to a very concentrated station network. This particularity makes a specific algorithm adaptation of the KPS-PS necessary, as compared to the EGNOS solution, to provide the desired APV-1 performance. These adaptations regard both orbit determination and all the more ionosphere corrections due to the very low number of Ionosphere Grid Points (IPG) that need be modeled and monitored.

To cope with these KASS specificities, Thales Alenia Space has designed, developed and qualified a new complete real time navigation algorithm chain that provides MOPS-compliant NOF messages. The ionosphere model is different from the EGNOS one that favors a local analysis counter to a global approach as the TRIN model [2] used in EGNOS.

This new algorithm chain provides the specified APV-1 performance, particularly in the case of strong ionosphere activity, with a very good level of integrity margin. This paper presents the overall KASS system architecture as well as the results obtained using this new algorithm chain under different ionosphere contexts. The APV-1 service availability level is presented and the maximum of safety index on each monitored IGP and satellite is discussed.

INTRODUCTION

The KASS is the planned Satellite-Based Augmentation System (SBAS) in Korea. An SBAS is a Global Navigation Satellite System (GNSS) augmentation system standardized in Annex 10, Volume 1, to the International Convention on Civil Aviation published and maintained by the International Civil Aviation Organization (ICAO). The KASS is a system that will provide safety-critical services for the Civil aviation as well as an Open service, usable by other forms of transportation and possibly other position, navigation and timing (PNT) applications.

The KASS will provide improved GNSS navigation services for suitably equipped users in the agreed service areas of the Republic of Korea by broadcasting an augmentation signal to the US Global Positioning System (GPS) Standard Positioning Service (SPS). The augmentation signal provides corrections to ranging measurements from GPS satellites clock & orbits and integrity bounds on the residual ranging errors, as well as corrections and integrity bounds for ionosphere delays. The augmentation signal will be broadcast by two Geostationary Earth Orbiting (GEO) satellites and will be used by GPS/SBAS user equipment to compute a navigation solution.

The KASS is a project of the Korean Ministry of Land, Infrastructure and Transport (MOLIT). The KASS procurement is being managed by a KASS Program Office (KPO) within the Korea Aerospace Research Institute (KARI). The KARI is the primary entity of the Republic of Korea in the sphere of space exploration. The KARI is a developer, manufacturer and operator of various types of spacecraft and mission. Once commissioned for operational use, the KASS will be maintained and operated by the MOLIT. Thales Alenia Space in France is the industry prime contractor of the KASS development.

The KASS is designed to be a system-of-systems including hardware and software to fulfill the following functions.

-Collect GPS and GEO satellite data at various locations in the Republic of Korea (and possibly in other States in the future), -Transmit these data to redundant KASS Processing Stations (KPSs) where the contents of the augmentation signal are generated, and redundant KASS Control Stations (KCSs) where operators monitor and control the system, -Compute corrections and associated integrity bounds for ranging measurements from GPS and possibly GEO satellites in view of the KASS, -Format messages compliant with the SBAS user interface standardized in ICAO SARPS Annex 10 and the RTCA MOPS 229-D change 1 [START_REF]Minimum operational performance standards for Global positioning system / wide area augmentation system airborne equipment[END_REF], -Uplink a signal carrying these messages to navigation payloads on the KASS GEOs, and -Broadcast the signal to the users after frequency-conversion to the L1 band.

The Navigation services provided to the aviation community by the KASS support the implementation of Performance-Based Navigation (PBN) in the Republic of Korea by providing navigation services for the following phases of flight:. En route (oceanic and domestic), terminal area, non-precision approach (also called LNAV, lateral navigation), approach with vertical guidance type I (APV-I), departure, and Required Navigation Performance (RNP) operations. The KASS may also be used to support Automatic Dependent Surveillance -Broadcast (ADS-B) applications.

The KASS ensures the integrity of the broadcast corrections in case of possible failures of the GPS constellation, of some of its hardware components or possible latent faults of some of its software components, and promptly alerts the users whenever the integrity of the broadcast corrections cannot be assured.

The global overview of the system is given in the Figure 1. The ground segment will comprise the following subsystems .

-The network of KRSs (KASS Reference Stations), with two independent receivers at each KRS site; -The redundant KPSs (KASS Processing Sets) and KCSs (KASS Control Stations), and the KUSs (KASS Uplink Stations); and -The communication network between all system components distributed across Korea (WAN).

The space segment will include the GEOs satellites and the navigation payloads onboard these GEOs.

Using measurements from the KRS spread over the KASS coverage area, the KPS derives the information necessary to support the generation of the KASS broadcast messages. Each message is transmitted to the KUS to uplink them to the KASS GEO satellites for onwards transmission to the users.

To achieve the required overall KASS availability and continuity performance, it is necessary to have several redundant KPS which are collocated with the KCS to share communication lines. The KPSs at all sites will all be active (i.e. simultaneously operational). The selection of the KPS channel to be used as the user data message provider will be made at the KUS, using status validation data from each KPSs check functions as well as control information from the KCS.

The KPS computation processing set (KPS-PS) determines the user data information (corrections, confidence intervals, etc.) using measurements from one of the receivers of each KRS site. The integrity of the derived information is then assessed by the KPS check set (KPS-CS) using data from at least one other group of independent receiver from each KRS site. The status information generated from the integrity assessment is transmitted to the KUS for use in selecting the KPS to be used as the user data provider. A KPS channel is made of one Processing Set and one Check Set.

The KPS Processing Set is responsible for computing the necessary GNSS corrections and integrity data to be broadcast to the user (Messages Types 2-6, 25, for the satellites and 26 for the ionosphere), and for selecting and formatting the most appropriate sequence of messages in which this information must be sent. Additionally, the KPS Processing Set must incorporate some means of verifying the correctness of its performance.

The Integrity data are formed by User Differential Range Error (UDRE) and Grid Ionospheric Vertical Error (GIVE) for each satellite and Ionosphere Grid Point (IGP) respectively. The UDRE bounds the non-modelled orbit and clock error once applied the satellite KASS corrections. The GIVE bounds the vertical ionospheric delay error the Grid Ionosphere Vertical Delay (GIVD) once has been applied. According the MOPS [START_REF]Minimum operational performance standards for Global positioning system / wide area augmentation system airborne equipment[END_REF], the UDRE and GIVE values are linked to the standard deviation of a normal distribution that overbound the residual errors at the desired confidence level, after application of SBAS corrections:

- = 3.29 • ⋅
, where value is defined in Message Type 27, and -= 3.29 • .

The functional description of the processing set is divided in several sub-sets. They include the pre-processing of the data, the computation of the main corrections, i.e. ephemeris, clocks and ionosphere, the computation of the UDRE, the GIVE and the selection and formatting of the messages. This set is also responsible to establish the KASS Network Time (KNT) that represent the internal reference time scale on which all clocks are synchronized (stations and satellites). The KNT is steered towards the GPS time scale by the KPS Processing Set design. The steering shall be closer than 50ns by requirement, but in practice the gap between the two time references is below 3ns (see [START_REF] Labe | New Orbit Determination and Clock synchronisation modules for EGNOS[END_REF]). The message the KPS Processing Set sends is the NOF Up Link (UP).

The KPS Check Set is responsible for verifying the integrity of the NOF coming from the Signal In Space (SIS). There are five KPS cycles between the NOF-UP emission event and the NOF-SIS reception event. For each monitored satellite defined in the PRN mask (Message Type 1), the KPS Check Set computes the Satellite Residual Error at the Worst user location (SREW) and compares it to the broadcast UDRE in the NOF-SIS. For each monitored IGP defined in the IGP mask (Message Type 18) the KPS Check Set computes the GIVD error and compares it to the broadcast GIVE in the NOF-SIS. The KPS Check Set send a 'do not use' alarm to the KPS Processing Set for injection inside the very next NOF-UP in case an anomaly is detected.

The Figure 2 provides details on the data flows exchanged between Subsystems and between KPS sets. The proposed KRS network for KASS are located on the Rep. of Korea land masses. The specificity of this stations network is the geographic colocalisation. This led to important KPS algorithms adaptations regarding on orbit determination and ionosphere corrections for KPS-PS and integrity assessment for KPS-CS. Although the final location of the KRS is not finalized and depend on site survey the positions that are used from now are depicted below.

KRS ID Location

Latitude Longitude Altitude The performance of a satellite navigation system is expressed in four Criteria: Accuracy, Integrity, Continuity and Availability.

(deg) (Min) (Sec) (deg) (Min) (Sec) (m)
The Accuracy feature is the difference between the computed value and the actual value of the user position, speed and time.

The Integrity feature refers to the notion of trust that the user may have in the computed position. Integrity includes the ability of a system to provide confidence thresholds as well as Alarms within a known time-to-alert (TTA) in case of anomaly.

The Continuity feature defines the ability of a system to perform its function without interruption during the operation planned by the user (for example landing phase of an aircraft). It is evaluated as the probability that from the moment when the criteria of precision and integrity are completed at the beginning of an operation, they remain so for the duration of the operation.

Finally the Availability feature is the percentage of time when, over a certain geographical area, the criteria of accuracy, integrity and continuity are met.

The System time to alert is defined as the time starting when an alarm condition occurs to the time that the alarm is displayed in the cockpit. The KASS is designed in such a way the TTA is always under 6 seconds as EGNOS. The performance features that are presented in this paper are the level of targeted APV-1 performance levels associated with integrity characteristics as Safety Index (SFI) on satellites and IGP. Because the KASS project is currently under preliminary design these performances features are assessed only on the base of synthetic scenarios at the date of the paper no real data coming from KRS are available.

However the synthetic data shall be representative of the ionosphere behaviour above the South Korea in nominal conditions but almost in case of strong ionosphere dynamic to warranty the integrity of the system. The accuracy, availability and continuity commitments are based on the nominal scenario. The integrity commitment is assessed whatever the environment situation thus in nominal and degraded ionosphere conditions. On degraded scenario the commitment is only to maintain integrity.

The synthetic scenario have to catch the real ionosphere and then then have been built based on a real data collection coming from a set of Korea stations and neighboured IGS stations. Having these datasets a dedicated methodology shall be developed to inject these ionosphere information in the synthetic scenarios. The description of this methodology is the scope of the following section.

IONOSPHERE MODELLING APPROACH FOR SYNTHETIC SCENARIO

The processing of the ionosphere is critical to the KASS system performance. In order to test the performance of the KASS system, and especially the capability for maintaining integrity during solar storm conditions, synthetic scenarios were produced. The scenarios were derived from actual observations of GPS receivers located in the Republic of Korea. The 3D distribution of electron density was created by deriving grid values of the ionosphere parameters, foF2 and M(3000)F2, from observed data and by applying the NeQuick model to this grid ([4], [START_REF] Nava | A new version of the NeQuick ionosphere electron density model[END_REF]).

The NeQuick model (see [START_REF] Giovanni | An analytical model of the electron density profile in the ionosphere[END_REF] and [START_REF] Nava | A new version of the NeQuick ionosphere electron density model[END_REF]) is adapted to real ionospheric conditions by means of using the Az parameter. This will be the concept used to derive the scenarios by computing a grid of Az values.

The ionosphere conditions representative of the Korea environment have been simulated from actual observations of GPS receivers located in the Republic of Korea, complemented by some IGS stations located in neighbouring. IGS datasets are provided daily at a 30s sampling rate.

The first step is to assess the quality of the data of every receiver. In order to prevent any ionosphere mismodelling, the receiver measurements shall not contain any abnormal level of multipath or of IFB behaviour. Each receiver with such an anomaly has been discarded from the set of receivers used to elaborate the ionosphere model.

Then, the measurements of the remaining receivers have been pre-processed in order to separate the Slant Total Electron Content (STEC) from other sources of error. This algorithm chain implements filters that aim at mitigating the multipath error in the geometry-free L1/L2 combination and also estimates the satellite and receiver IFB. At the end of this process, the STEC values are obtained.

Once the STEC values have been computed, Vertical TEC (VTEC) values have been estimated over a thin layer grid of 1 degree latitude/longitude resolution. The approach consists in performing a local approximation of the vertical TEC variable in the vicinity of a given grid point of the thin layer considering a large set of Ionosphere Pierce Points. Around each grid point, the ionosphere has been modelled by a polynomial fit.

Finally, some NeQuick models have been calibrated in order to be able to reproduce an ionosphere environment consistent with the observed ionosphere delays from the measurements. For each grid point and each epoch the Az value has been computed. The methodology to compute the Az maps is based on minimizing, the error between the observed VTEC and the one computed by the NeQuick, using the Brent method. Hence, an Az map is obtained with the same sample as the input VTEC grid. These Az maps are finally used as input of engineering tools in order to generate an ionosphere scenario.

The Figure 5 presents the different steps of the methodology: The last day of the scenario (November 10 th , 2004) shows local ionosphere events. Figure 11 shows a map of the vertical delay on the last day of the degraded scenario at the time the ionosphere gradients are the higher.

INTEGRITY PERFORMANCE ASSESSMENT METHODOLOGY

The alarm limit is the maximum allowable error in the user position solution before an alarm is to be raised within the specific TTA. The Horizontal Alarm Limit (HAL) and Vertical Alarm Limit (VAL) define the alarm box (see Figure 12) .

Figure 12: Alarm Limit box

This alarm limit is dependent on the flight phase (see Table ).

The definition of the integrity risk is the probability during the period of operation that an error, whatever is the source, might result in a computed position error, where and note its horizontal and vertical components, exceeding the Alarm Limit, and the user be not informed within the specific TTA.

The integrity is maintained while

! ∧ !$ % 1 ' ()
Where () = 2 * 10 ,-150 s ⁄ for APV-1 service level for instance.

In case the previous inequation does not hold at a time 1, an alarm shall be received by the user before 1 2 33 . In case the alarm in not received under TTA a non-integer situation occurs.

The Horizontal and Vertical Protection Level (HPL and VPL) are the values computed by the user receiver which estimates the bound on the actual Navigation System Error using data transmitted by the SBAS signal (UDRE, GIVE) and pre-determined bounds. The HPL and VPL shall bound the positioning error with a probability equal to 0.9999999.

The HPL and VPL are calculated on the basis of the integrity data provided by the SBAS and standardized assumption on the budget of local errors.

The integrity assessment is apportioned in two parts.

-The nominal condition i.e. without failure named the Fault Free condition, -The degraded condition corresponding to an exposition to Feared Event.

The total budget is equally allocated between this two features, the nominal and degraded conditions. Under nominal or Fault Free (FF) condition the KPS design shall guaranty that

44 = % ! ∨ % !$ 1 2 ()
The integrity is insured by design: the and time series are computed in such a way the non-modeled residual error are bounded up to 5.33 or 5.33 corresponding to the required confidence level (10 ,-for SL3 service level). For APV1 service level the budget of 2 * 10 ,-/150 s is allocated to the whole KASS system: it must be declined to the subsystems. The KPS Processing Set and the Check Set are two filters that can stop an integrity event, and they are supposed independent. Indeed, they don't process the same measurements, and their algorithms are different; even their HW and SW are independent.

The integrity is verified at pseudorange level by measuring at each sample time the safety index on both satellite (SV) and IGP defined as: where ∆GIVE is the additional GIVE contribution allocated for the Hatch filter user smoothing and computed with the specified MOPS ionosphere gradient of 10 mm/s. This contribution shall be removed from because it is assumed that it is completely consumed by the user so it cannot be considered as a protection against ionosphere errors i.e. GIVD error ( S ).

While 78 9 5.33 and 78 @ 5.33 the pseudorange integrity is warranty and then the integrity at user level is warranty.

On a nominal system condition without failure (Fault Free) integrity is verified by tests and checking that the maximum safety index are always inferior to 5.33.

Under degraded condition the KPS design shall guaranty that, for the set of all Feared Event (FE), then

4 1 2 ()
The probability of non-integrity is case of feared event is the sum of each integrity risk in front of each feared event 8 T . The probability 4 U is a conditional probability of impact that, under the 8 T has occurred, a missed detection has an impact at user level. The system failure modes associated with feared events are defined with a certain probability of occurrence SVV . Taking into account this probability of occurrence the integrity risk associated at the degraded condition is:

4 = W SVV 8 T $ • 4 U T
The general equation used to evaluate the integrity risk is given by the previous probability figures weighted by the time exposure time, namely the probability of occurrence to be either in nominal or degraded condition :

X = SVV 88$ • 44 2 4 ()
where SVV 88$ is the exposure probability (closed to 1) to the nominal condition regime and X is the total budget of Non-Integrity that has to be below the requirement given in Table .

In the following only the integrity performance 44 figure in nominal condition is mentioned because the integrity risk in case of feared event is currently under assessment.

RESULTS AND DISCUSSION

This section presents the first preliminary results of the KASS performance on accuracy, integrity and availability. The Horizontal NSE is below 13.7m, to be compared with the 3.7km requirement, for En Route, 740m for Terminal and 220m for NPA services level over the FIR of Incheon.

C. Integrity performance

As mentioned in section 11 this section presents the safety index (SFI) maps for both satellites and IGP. The safety index is defined as the maximum over the scenario of ratio of the observed error to the 1-sigma bound value. These maps are focused on days 3 of the nominal and degraded scenario, that are representative of the overall days of each.

For the nominal scenario, Figure 19 presents the maximum of the SFI per monitored IGP. The maximum that is obtained is 1.33 (to be compared to the 5.33 requirement) and is reached at two IGP of 30 deg North of latitude and 125 deg, 130 deg of longitude. These IGPs are monitored 100% of time, whereas it is not the case for the IGPs located further South. Indeed the less an IGP is monitored, the lower the integrity risk is. For the degraded scenario, the figures below shows the maximum Safety Index per IGP on the degraded scenario for a few days. Overall, the maximum SFI on the whole scenario is 3.2, which leaves a good integrity margin, despite the very degraded ionospheric conditions. These conditions are reflected through the evolution of the maximum SFI over time, which is shown below: The maximum Safety Index shows variations due to the rapid evolution of the ionospheric conditions over Korea for this scenario. However, the ionospheric corrections calculated allow to always bound the error with a good margin.

The maximum Safety Index for the satellites shows, just like the nominal scenario, a large integrity margin, the maximum value for day 3 being 1.1. The results for the other days of the scenario are very similar. Like the nominal scenario, the satellite maximum SFI remains very stable over time: The KASS design and the KPS algorithms design prototype allows reaching a very good level of accuracy, integrity and availability performance features. The summary of our results is given in Table 2.

Phase

Figure 1 :

 1 Figure 1: KASS architecture overview

Figure 2 :

 2 Figure 2: KPS data flows The interface between the KPS Processing Set and KPS Check Set consists in the following: -Internal and operational NOF computed by the Processing Set and sent to the Check Set for independent verifications, -Transition information sent by the Processing Set to the Check Set in order to recover from SV/IGP NM/DU periods through the NOF-SIS, -NM/DU flags requested by the Check Set for inclusion in the NOF-UP to be send by the Processing Set to the KUS -Communication test performed during the initialization phase of the KPS

Figure 3 :

 3 Figure 3: KRS proposed network for KASS

Figure 4 :

 4 Figure 4: KASS service area

Figure 5 :Figure 6 :Figure 7 :Figure 8 :Figure 10 :

 567810 Figure 5: Injection methodology of real ionosphere data in synthetic scenarios At the end of this activity, the objective is to have two available scenarios, representative of the Korea ionosphere environment. -One scenario representative of nominal conditions -One scenario representative of degraded conditions

Figure 11 :

 11 Figure 11: DAY7 (07/09/2002): Representative of the 10/11/2004

  ABBCB D; EFG? H ,∆JKLM H

Figure 18 :

 18 Figure 18: HNSE for NPA, Terminal, En-Route service level

Figure 19 : 3 Figure 20

 19320 Figure 19: SFI max per IGP, nominal scenario, day 3 Figure 20 shows the IGP SFI max time series that highlight a very good integrity margin as well a very stable behavior along time.

Figure 20 : 3 Figure 21

 20321 Figure 20: IGP SFI max time series, nominal condition, day 3 Figure 21 presents the maximum of SFI per monitored satellite. The figures are homogenous for each satellite and the integrity margin is very good. The maximum of SFI reached is 1.2 (to be compared to the 5.33 requirement) by PRN 28.

Figure 21 : 3 Figure 22

 21322 Figure 21: SFI max per satellite, nominal condition, day 3Figure22shows the satellites SFI max time series and highlights a very good behavior stability. Some geometric pattern may be noted due to the GPS orbital period (i.e. twice a day).

Figure 22 :

 22 Figure 22: Satellite SFI max time series, nominal condition, day 3

Figure 23 : 3 Figure 24 : 4 Figure 25 :

 23324425 Figure 23: SFI max per IGP, degraded scenario, day 3

Figure 26 : 3 Figure 27 : 4 Figure 28 :

 26327428 Figure 26: IGP SFI max time series, degraded condition, day 3

Figure 29 :

 29 Figure 29: SFI max per satellite, degraded condition, day 3

Figure 30 :

 30 Figure 30: Satellite SFI max time series, degraded condition, day 3

Table 1 : KASS performance service levels

 1 Table below provides the various service levels and the associated performance requirement for KASS GPS L1 legacy.

	Phase	Service coverage Availability Continuity TTA	Accuracy HNE VNE HAL	Integrity VAL Risk P HMI
	En Route	FIRs of Incheon	99.0%	10 -5 /hour 5 mn 3.7 km N/A 3.7 km N/A	10 -7 /h
	Terminal	FIRs of Incheon	99.0%	10 -5 /hour 15 s 740 m	NA 1.85 km N/A	10 -7 /h
	NPA	FIRs of Incheon	99.0%	10 -5 /hour 10 s 220 m	NA	556 m	N/A	10 -7 /h
	APV-I	Land-masses Korea + Jeju	99.0%	8x10 -6 /15 s 10 s 16.0 m 20.0 m 40.0 m 50.0 m	2x10 -7 /150 s

Table 2 : Performance budget summary assessment

 2

		Service coverage	Availability	TTA	Accuracy HNE VNE	Integrity Risk P HMI
			100% in Fault Free +				Good margin in Fault Free
	En Route	FIRs of Incheon	GPS failures System Failures not	6 s	13.7 m	N/A	Feared Event budget currently
			included yet				under assessment
			100% in Fault Free +				Good margin in Fault Free
	Terminal	FIRs of Incheon	GPS failures System Failures not	6 s	13.7 m	NA	Feared Event budget currently
			included yet				under assessment
			100% in Fault Free +				Good margin in Fault Free
	NPA	FIRs of Incheon	GPS failures System Failures not	6 s	13.7 m	NA	Feared Event budget currently
			included yet				under assessment
	APV-I	Land-masses Korea + Jeju Island	99.83% in Fault Free + GPS failures System Failures not included yet	6 s	1.6 m	2.4 m	Good margin in Fault Free Feared Event budget currently under assessment

ACKNOWLEDGMENTS

The authors would like to thanks Mathias Van Den Bossche and Celine Benassy-Foch from Thales Alenia Space for their paper proofreading and benefit discussions.

Heonho Choi is a researcher at the Korea Aerospace Research Institute. He received his Ph.D. degree from the Department of Heesung Kim is a researcher at Korea Aerospace Research Institute. He received his Ph.D. degree from the School of Electronics and Telecommunication of the Korea Aerospace University (Rep. of Korea) in 2014. He currently works for the development of the Korea Augmentation Satellite System. Jae-Eun Lee is a researcher at Korea Aerospace Research Institute SBAS R&D head office. She received her M.S. degree from the Department of Astronomy of the Yonsei University (Rep. of Korea) in 2007. Eunsung Lee is a principal researcher at Korea Aerospace Research Institute. He received his Ph.D. degree in Aerospace Engineering from the Konkuk University, (Rep. of Korea) in 2005. Gi-Wook Nam is the Executive Director of Korea Aerospace Research Institute SBAS R&D head office. He received his M.S. in Aeronautical Engineering from the Korea Aerospace University (Rep. of Korea) in 1988.

A. Availability performances

The availability performance map that are presented are built as an average on the five days of the nominal scenario considering the extended 27 SPS08 GPS constellation with a probability of failures.

For APVI, the colored area of Figure 13 shows the users for which the availability is above 99%.

The Figure 14 shows the availability performance for the other services level. The coverage over the FIRs of Incheon is 100% everywhere.

B. Accuracy performance

In our simulation conditions, the accuracy is estimated using the Navigation System Error (NSE). The NSE is the 95 th percentile of the the position error distribution at a specific . The following Figure 15 and Figure 16 present the 95 th percentile of the five days of the nominal scenario for both horizontal and vertical accuracy for APV-1 service level.

Figure 15: Horizontal NSE for APV1 service level

The Horizontal NSE is below 1.60m, to be compared to the requirement of 16m over the Republic of Korea land masses. The following map shows the vertical accuracy performance.

Figure 16: VNSE for APV1 service level

The vertical NSE is below 2.40m to be compared with the 20m requirement over the Korea land masses.

The accuracy of the ionosphere correction is given in Figure 17 for the day three of the nominal scenario. The Figure 18 shows the Horizontal NSE for the 5 days of the nominal scenario for En Route, Terminal and NPA services level (i.e. without using the ionosphere corrections).


Christian Doczkal
email: christian.doczkal@ens-lyon.fr

Joachim Bard

Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq

come

Introduction

Propositional Dynamic Logic (PDL) [START_REF] Michael | Propositional Dynamic Logic of Regular Programs[END_REF][START_REF] Harel | Dynamic Logic[END_REF] is a modal logic developed for reasoning about programs with applications for instance in knowledge representation [START_REF] Baader | Description Logic[END_REF]. The modalities of PDL are given by regular programs (i.e., regular expressions with tests) describing binary relations on states. The formula [α]φ is satisfied by some state if all α-reachable states satisfy φ. The language of programs includes a reflexive transitive closure operation (α * ) causing PDL to be non-compact. Converse PDL (CPDL), also defined in [START_REF] Michael | Propositional Dynamic Logic of Regular Programs[END_REF], extends PDL with a converse operation on programs. Both PDL and CPDL have the small-model property [START_REF] Michael | Propositional Dynamic Logic of Regular Programs[END_REF] and are EXPTIME-complete [START_REF] Michael | Propositional Dynamic Logic of Regular Programs[END_REF][START_REF] Vaughan | Models of Program Logics[END_REF]. Axiomatizations of PDL and CPDL were first given by Segerberg [START_REF] Segerberg | A Completeness Theorem in the Modal Logic of Programs[END_REF] and shown complete independently by Gabbay [START_REF] Gabbay | Axiomatization of Logic Programs[END_REF] and Parikh [START_REF] Parikh | The Completeness of Propositional Dynamic Logic[END_REF].

Our main result is a machine-checked constructive proof that for every PDL or CPDL formula φ one can either construct a proof of ¬φ from the respective axioms or a model of bounded size satisfying the formula. Completeness and the small-model property as well as decidability of satisfiability, validity and provability then follow as corollaries. The form of constructive completeness result established here is more informative than a classical completeness result in the sense that it provides an algorithm constructing proofs for valid formulas rather than merely showing the existence of such proofs.

The completeness proofs for (C)PDL in the literature either use non-standard canonical models and filtration [START_REF] Harel | Dynamic Logic[END_REF][START_REF] Parikh | The Completeness of Propositional Dynamic Logic[END_REF] or construct "canonical" models inside a finite syntactic universe [START_REF] Kozen | An Elementary Proof of the Completness of PDL[END_REF]. Both techniques are non-constructive in the sense that they assume (at least) logical decidability of provability (i.e., ⊢ φ ∨ ̸ ⊢ φ for all φ). While logical decidability follows from (computational) decidability, the easiest way to show decidability of provability is via completeness.

In order to obtain a constructive completeness result, we base the completeness proof on a decision method for satisfiability. We employ a variant of pruning [START_REF] Kaminski | Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics[END_REF][START_REF] Vaughan | Models of Program Logics[END_REF] extended to provide refutations for unsatisfiable formulas in addition to constructing models for satisfiable formulas. Translating these pruning refutations to proofs in the Hilbert system then yields the desired completeness result. The use of pruning as decision procedure underlying the completeness result naturally leads to a factorization of the proof into an algorithmic part for the decision method, a semantic argument for the model construction, and a syntactic translation from pruning refutations to Hilbert refutations. We believe that the constructive nature of the proof and the clear separation of concerns makes the proof particularly easy to follow.

The pruning-based approach is inspired by completeness proofs for the branching time logics UB ("unified branching") [START_REF] Ben-Ari | The Temporal Logic of Branching Time[END_REF] and Computation Tree Logic (CTL) [START_REF] Emerson | Decision Procedures and Expressiveness in the Temporal Logic of Branching Time[END_REF] and was employed by the first author to obtain formal and constructive completeness proofs of Hilbert and sequent systems for CTL [START_REF] Doczkal | A Machine-Checked Constructive Metatheory of Computation Tree Logic[END_REF][START_REF] Doczkal | Completeness and Decidability Results for CTL in Constructive Type Theory[END_REF]. For the construction of models using pruning, we follow the presentation of pruning in [START_REF] Kaminski | Incremental Decision Procedures for Modal Logics with Nominals and Eventualities[END_REF]. The translation from pruning refutations to Hilbert proofs builds on ideas in [START_REF] Kozen | An Elementary Proof of the Completness of PDL[END_REF]. For CPDL, we show that the Hilbert system validates the conversion of formulas to converse normal form and then use pruning for converse normal formulas. This isolates the treatment of converse to a few select places in the proof. We are not aware of any other completeness proof treating converse this way.

The mathematical proofs described in this paper are constructive and designed with the formalization in mind. The accompanying Coq development [START_REF] Doczkal | Coq development accompanying this paper[END_REF] follows the proofs outlined in the paper and provides the details elided in the paper. The development is carried out using the Ssreflect [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF] proof language and the Mathematical Component Libraries [START_REF]The Mathematical Components team[END_REF]. Our development builds upon the formal and constructive completeness proof for test-free PDL presented in [START_REF] Bard | A Formal Completeness Proof for Test-free PDL[END_REF].

The rest of the paper is organized as follows. Section 2 recalls the syntax, semantics, and Hilbert system of PDL and describes their representation in Coq. Sections 3 to 6 describe the constructive completeness result for PDL. Section 7 describes the changes required to extend our results to CPDL. Section 8 provides a high-level overview of the accompanying Coq development [START_REF] Doczkal | Coq development accompanying this paper[END_REF].

Propositional Dynamic Logic

We fix a countably infinite type of atomic programs A and a countably infinite type of atomic propositions P. The letter a ranges over atomic programs and the letter p ranges over atomic propositions. We consider Propositional Dynamic Logic (PDL) with the following syntax for programs (denoted α, β, . . . ) and formulas (denoted φ,ψ , . . .).

α, β a | α + β | α β | α * | φ? (a : A) φ,ψ p | ⊥ | φ → ψ | [α]φ (p : P)
We define the remaining logical operations in terms of this syntax (i.e., ¬φ φ → ⊥, φ ∧ ψ ¬(φ → ¬ψ ), ⟨α⟩φ ¬[α]¬φ, . . . ). 1 We write |φ| and |α | for the sizes of formulas and programs (i.e., the size of the syntax tree).

Formulas are interpreted over transition systems where the states are labeled with atomic propositions and the transitions are labeled with atomic programs. A transition system M hence consists of • A (possibly infinite) type |M | whose elements are called states

• A transition relation a ⇒ M : |M | → |M | → Prop for every a : A • A labeling L M : P → |M | → Prop.
In the following, we write M for transitions systems as well as their underlying type of states.

Let M be a transition system. We define a satisfaction relation between states w of M and formulas φ, written w |= φ, and an interpretation of programs α as binary relations on M, written α ⇒ (with M implicit), by mutual recursion on formulas and programs (cf. fig. 1). Note that we use the same symbols (e.g. →) both for the logical operators of PDL and for those of the type theory. This does not lead to ambiguity. 1 While φ → ψ could be defined as [φ?]ψ , we include it in the syntax since this allows us to define the Hilbert system with minimal reliance on defined logical operations.

w |= p L M p w w |= ⊥ ⊥ w |= φ → ψ w |= φ → w |= ψ w |= [α]φ ∀v.w α ⇒ v → v |= φ w a ⇒ v w a ⇒ M v w α +β ⇒ v w α ⇒ v ∨ w β ⇒ v w α β ⇒ v ∃u.w α ⇒ u ∧ u β ⇒ v w α * ⇒ v w ( α ⇒) * v w φ? ⇒ v w = v ∧ w |= φ Figure 1.

Semantics of formulas and programs

Our goal is to show soundness and completeness of the Hilbert system for PDL presented in fig. 2. The Hilbert system employed here is a variant of Segerberg's axiomatization as presented in [START_REF] Harel | Dynamic Logic[END_REF]. We replace the original induction axiom

(i.e., [α * ](φ → [α]φ) → φ → [α * ]φ) with a rule (Ind) and omit ⊢ φ → [α][α * ]φ → [α * ]
φ, which is derivable by induction. We prefer the system from fig. 2 because, a priori, it appears weaker. Nevertheless, it is straightforward to show that the two systems are equivalent (see [START_REF] Doczkal | Coq development accompanying this paper[END_REF] for the details). Hence, all our results apply to both systems.

The satisfaction relation essentially constitutes a shallow2 embedding of the classical object logic PDL into the constructive type theory of Coq. In order to ensure that the object logic is interpreted classically we restrict our attention to those transition systems for which the satisfaction relation is stable under double negation. Definition 2.1. A (classical) model is a transition system M for which |= is stable under double negation, i.e., a transition system satisfying

∀w : M ∀φ.¬¬(w |= φ) → w |= φ (*)
Classical models can be understood in several ways. The condition (*) localizes the classical assumptions required for soundness into the definition of models. In fact, classical models are the largest class of models for which one can constructively show soundness of the Hilbert system for PDL given in fig. 2. Theorem 2.2 (Soundness). Let M be a transition system. Then ⊢ is sound for M (i.e., ⊢ φ implies w |= φ for all φ and all w : M) if and only if M is a classical model.

⊢ φ → ψ → φ (1) ⊢ (θ → φ → ψ ) → (θ → φ) → θ → ψ (2) ⊢ ¬¬φ → φ (3) ⊢ [α](φ → ψ ) → [α]φ → [α]t (4) ⊢ [α]φ → [β]φ → [α + β]φ (5) ⊢ [α + β]φ → [α]φ (6) ⊢ [α + β]φ → [β]φ (7) ⊢ [α β]φ → [α][β]φ (8) ⊢ [α][β]φ → [α β]φ (9)
⊢ [α * ]φ → φ (10) ⊢ [α * ]φ → [α][α * ]φ (11) ⊢ [φ?]ψ ↔ (φ → ψ ) ( 12
) MP ⊢ φ → ψ ⊢ φ ⊢ ψ Nec ⊢ φ ⊢ [α]φ Ind ⊢ φ → [α]φ ⊢ φ → [α * ]φ Figure 2.
Hilbert system for PDL Note that every transition system is a classical model if one assumes excluded middle. Moreover, one can show constructively that all finite transition systems (with boolean transition relations and labeling) are classical models. This amounts to proving decidability of the model-checking problem -which in the case of PDL is straightforward. Since PDL has the small-model property, we only need to construct finite models to show completeness.

For the rest of the paper, the word model always means classical model. We say that a formula φ is satisfiable if w |= φ for some state w of some model and valid if w |= φ for every state w of every model.

The main result of this paper is a constructive proof that for every formula φ, one can either construct a finite model certifying the satisfiability of φ or a proof of ¬φ from the axioms in fig. 2 (certifying the unsatisfiability of φ). Completeness of the Hilbert system (i.e., ⊢ φ whenever φ is valid) as well as decidability of satisfiability, validity and provability then follow as corollaries.

The central notions in the completeness proof are the notions of demo, subformula universe, and pruning. Demos are a class of finite syntactic models designed such that for every subformula universe U , there exists a largest demo over U satisfying all satisfiable formulas in U . We construct this largest demo using pruning in such a way that we obtain proofs of ¬φ for all unsatisfiable formulas φ in U .

Subformula Universes

We now define the notion of subformula universe. A subformula universe for a formula φ is a finite set of signed formulas [START_REF] Smullyan | A Unifying Principal in Quantification Theory[END_REF] containing all formulas that play a role in deciding satisfiability of φ. Definition 3.1. We call a finite set F of formulas subformula closed if it satisfies the following closure properties:

S1. If φ → ψ ∈ F , then {φ,ψ } ⊆ F . S2. If [a]φ ∈ F , then φ ∈ F . S3. If [α + β]φ ∈ F , then {[α]φ, [β]φ, φ} ⊆ F . S4. If [α β]φ ∈ F , then {[α][β]φ, [β]φ, φ} ⊆ F . S5. If [α * ]φ ∈ F , then {[α][α * ]φ, φ} ⊆ F . S6. If [ψ ?]φ ∈ F , then {ψ , φ} ⊆ F .
Note that subformula closedness requires the presence of more than just the subformulas of every formula (e.g.,

[α][α * ]φ when [α * ]φ ∈ F ).
It is a standard result about PDL that every formula is included in a subformula closed set of size linear in |φ| called the Fisher-Ladner closure [START_REF] Michael | Propositional Dynamic Logic of Regular Programs[END_REF][START_REF] Harel | Dynamic Logic[END_REF] of φ. This closure be computed using two mutually recursive functions FL and FL □ as follows:

FL(p) {p} FL(⊥) {⊥} FL(φ → ψ ) {φ → ψ } ∪ FL(φ) ∪ FL(ψ ) FL([α]φ) FL □ (α, φ) ∪ FL(φ) FL □ (p, φ) {[p]φ} FL □ (α + β, φ) {[α + β]φ} ∪ FL □ (α, φ) ∪ FL □ (β, φ) FL □ (α β, φ) {[α β]φ} ∪ FL □ (α, [β]φ) ∪ FL □ (β, φ) FL □ (α * , φ) {[α * ]φ} ∪ FL □ (α, [α * ]φ) FL □ (ψ ?, φ) {[ψ ?]φ} ∪ FL(ψ )
In order to show that FL(φ) is subformula closed, we first establish the following transitivity property. The proof follows the presentation in [START_REF] Harel | Dynamic Logic[END_REF]. Proof. By mutual induction on φ and α. □

Lemma 3.2. 1. φ ∈ FL(φ) and [α]φ ∈ FL □ (α, φ). 2. If ψ ∈ FL(φ), then FL(ψ ) ⊆ FL(φ). 3. If ψ ∈ FL □ (α, φ), then FL(ψ ) ⊆ FL □ (α, φ) ∪ FL(φ). Proof. Claim (1) is trivial. Claims (2) and
For the definition of subformula universes, we employ signed formulas. A signed formula has the form φ σ where φ is a formula and σ ∈ {-, +} is its sign. Signs never occur within a formula and bind weaker than formula constructors, e.g, [α]φ + is to be read as ([α]φ) + . Semantically, negative signs correspond to top-level negations. That is, w |= φ -is to be read as w ̸ |= φ and w |= φ + as w |= φ. In particular, we have:

w |= [α]φ -⇔ ∃v.w α ⇒ v ∧ w |= φ -⇔ w |= ⟨α⟩¬φ
Definition 3.5 (Subformula Universe). Let F be a subformula closed set. We refer to the set { φ σ | φ ∈ F , σ ∈ {+, -} } as the subformula universe over F . For formulas φ, we write U (φ) for the subformula universe over FL(φ).

Signed formulas are a technical device allowing us to describe demos and pruning, which are usually described using negation-normal formulas, in terms of our minimal syntax for PDL.

Demos

A clause is a finite set of signed formulas. Demos [START_REF] Kaminski | Incremental Decision Procedures for Modal Logics with Nominals and Eventualities[END_REF][START_REF] Kaminski | Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics[END_REF] are certain sets of clauses that can be seen as models in such a way that every state satisfies all signed formulas it contains.

The first requirement on demos is that all states are Hintikka sets. H1. ⊥ + H . H2. There is no formula φ such that {φ

+ , φ -} ⊆ H . H3. If (φ → ψ ) + ∈ H , then φ -∈ H or ψ + ∈ H . H4. If (φ → ψ ) -∈ H , then φ + ∈ H and ψ -∈ H . H5. If [α β]φ σ ∈ H , then [α][β]φ σ ∈ H . H6. If [α + β]φ + ∈ H , then [α]φ + ∈ H and [β]φ + ∈ H . H7. If [α + β]φ -∈ H , then [α]φ -∈ H or [β]φ -∈ H H8. If [α * ]φ + ∈ H , then φ + ∈ H and [α][α * ]φ + ∈ H . H9. If [α * ]φ -∈ H , then φ -∈ H or [α][α * ]φ -∈ H . H10. If [φ?]ψ + ∈ H , then φ -∈ H or ψ + ∈ H . H11. If [φ?]ψ -∈ H , then φ + ∈ H and ψ -∈ H .
Intuitively, Hintikka sets are clauses that are consistent with respect to state-local reasoning. Note that if φ σ ∈ U for some subformula universe U , then all formulas mentioned in the Hintikka condition for φ σ are also in U . The use of signs avoids the need to close subformula universes under adding/removing top-level negations (as is, for instance, done in [START_REF] Emerson | Decision Procedures and Expressiveness in the Temporal Logic of Branching Time[END_REF]) thus simplifying the reasoning about the closure properties of the subformula universes.

Every finite set of clauses S, can be seen as a model M(S) in the following way:

|M(S)| S H a ⇒ M(S ) H ′ { φ | [a]φ ∈ H } ⊆ H ′ L M(S ) p H p + ∈ H
Even for sets of Hintikka sets, the states of M(S) will generally not satisfy all the formulas they contain. To see this, recall that [a]p -corresponds to the diamond formula ⟨a⟩¬p, and consider the case where S {{[a]p -, p + }}. Then the only state of M(S) lacks the a-successor satisfying p - required by [a]p -. Definition 4.2. Let S be a finite set of clauses. We interpret programs as relations on S in the following way:

C a ⇝ S D { φ + | [a]φ + ∈ C } ⊆ D C α +β ⇝ S D C α ⇝ S D ∨ C β ⇝ S D C α β ⇝ S D ∃E ∈ S.C α ⇝ S E ∧ E β ⇝ S D C α * ⇝ S D C ( α ⇝ S ) * D C φ? ⇝ S D C = D ∧ φ ∈ C Remark 1.
The set library employed in the formalization only allows us to write down sets that are finite by construction. However, finiteness of the unrestricted comprehension

{ φ + | [a]φ + ∈ C }
(D) If [α]φ -∈ C ∈ D, then C α ⇝ D D and φ -∈ D for some D ∈ D.
We now show that for demos D, every state of M(D) satisfies all formulas it contains. We fix some demo D for the rest of this section. The proof follows [START_REF] Kaminski | Incremental Decision Procedures for Modal Logics with Nominals and Eventualities[END_REF].

Pruning

Pruning [START_REF] Kaminski | Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics[END_REF][START_REF] Vaughan | Models of Program Logics[END_REF] starts from a given set of Hintikka sets and removes clauses violating the demo condition until a demo is reached. We will show that when starting from the set of all maximal Hintikka sets over some subformula universe U , this process terminates with a demo satisfying all satisfiable formulas from U . Moreover, we will obtain pruning refutations for all removed clauses. We fix some subformula closed set F and write U for the subformula universe over F .

Definition 5.1. A Hintikka set C ⊆ U is called maximal if for all φ ∈ F either φ + ∈ C or φ -∈ C.
The pruning function is defined recursively as follows:

prune S        prune(S \ {C}) ∃[α]φ -∈ C.¬∃D ∈ S. C α ⇝ S D ∧ φ -∈ D S
S is a demo Remark 2. The definition above does not specify which Hintikka set is to be removed if several violate the demo condition.

In the Coq development, we use a choice operator for finite sets to deterministically pick a clause to remove.

We now define a demo over U as follows:

S 0 { C ⊆ U | C maximal and hintikka } D prune S 0 Lemma 5.2. D is a demo contained in S 0 .
We say that a set of clauses S supports a clause C, written S ▷ C, if there exists some Hintikka set D ∈ S such that C ⊆ D. We have already established that a formula φ ∈ F is satisfiable whenever D ▷ {φ + } (theorem 4.6). In order to obtain completeness, it remains to show ⊢ ¬φ whenever D ̸ ▷ {φ + }. To prove this, we need to generalize from single formulas to clauses, i.e., prove ⊢ ¬C whenever D ̸ ▷ C. When a clause C appears in the place of a formula, as in ⊢ ¬C above, it is to be read as the sign respecting conjunction of the formulas it contains, i.e., C is to be read as φ σ ∈C ⌊φ σ ⌋ where ⌊φ -⌋ ¬φ and ⌊φ + ⌋ φ. If ⊢ ¬C, we call C (Hilbert) refutable.

We will show that all clauses over U that are not supported by S 0 are refutable. Moreover, we will show that this is an invariant that is preserved during pruning. That is, when a Hintikka clause is removed from S 0 and therefore some clause C ⊆ U is no longer supported by the remaining clauses, we can prove ⊢ ¬C, possibly using proofs constructed at an earlier stage.

To abstract from the algorithmic details of pruning, we give an inductive characterization of the clauses over U that are not supported by D and then translate derivations of this inductive definition to proofs in the Hilbert system. The rules are given in fig. 3. If pref C, we say that C is pruning refutable and if pcoref S for some S ⊆ S 0 , say that S is pruning corefutable. In both rules, the set S corresponds to some intermediate stage of pruning and the premise pcoref S captures the intuition that we have already established pref C for all preciously removed Hintikka clauses. The rule P1 then

P1 pcoref S C ⊆ U S ̸ ▷ C pref C P2 S ⊆ S 0 pcoref S [α]φ -∈ C ¬∃D ∈ S.C α ⇝ S D ∧ φ -∈ D pref C pcoref S ∀C ∈ S 0 \ S.

Hilbert Refutations

We now establish completeness of the Hilbert system by showing that pruning refutable clauses are also Hilbert refutable. The proof is compositional in the sense that we show the rules for pruning refutations admissible for the Hilbert system.

For sets of clauses A, we abbreviate C ∈A C as A. We continue to work with the subformula universe U from the previous section. We say that a set S ⊆ S 0 is (Hilbert) corefutable if ⊢ ¬C for all clauses in S 0 \ S. Lemma 6.1. Let C ⊆ U be maximal but not a Hintikka set. Then ⊢ ¬C.

Proof. By case analysis on the Hintikka condition being violated using propositional reasoning and axioms [START_REF] Ben-Ari | The Temporal Logic of Branching Time[END_REF][START_REF] Brünnler | Cut-free sequent systems for temporal logic[END_REF][START_REF] Cohen | A finset and finmap DRAFT library[END_REF][START_REF] Doczkal | A Machine-Checked Constructive Metatheory of Computation Tree Logic[END_REF][START_REF] Doczkal | Coq development accompanying this paper[END_REF][START_REF] Doczkal | Completeness and Decidability Results for CTL in Constructive Type Theory[END_REF][START_REF] Emerson | Decision Procedures and Expressiveness in the Temporal Logic of Branching Time[END_REF][START_REF] Michael | Propositional Dynamic Logic of Regular Programs[END_REF]. □

We remark that lemma 6.1 encapsulates most of the satelocal reasoning required to prove completeness. Otherwise, the claim is trivial. □

In addition to the lemmas above, we also make use of the following facts. Lemma 6.6.

1. If ⊢ φ → ψ , then ⊢ [α]φ → [α]ψ and ⟨α⟩φ → ⟨α⟩ψ . 2. ⊢ ¬⟨α⟩⊥ 3. ⊢ ⟨α⟩φ → [α]ψ → ⟨α⟩(φ ∧ ψ ) 4. ⊢ ¬[α]φ ↔ ⟨α⟩¬φ 5. ⊢ [α]φ → [α]ψ → [α](φ ∧ ψ ) 6. ⊢ ⟨α⟩(φ ∨ ψ ) → ⟨α⟩φ ∨ ⟨α⟩ψ 7. If ⊢ ψ → φ and ⊢ ⟨α⟩ψ → ψ , then ⊢ ⟨α * ⟩ψ → φ
Note that lemma 6.6(1) justifies rewriting with implications underneath of modalities, and we will do so without explicit mention.

In the following we present Hilbert proofs in "backward style" where each line is obtained from the previous line by rewriting with some lemma or by propositional reasoning (usually the introduction or elimination of some big conjunction or disjunction). We chose this presentation, rather than the traditional forward chaining, because it closely matches the way the proofs are obtained in Coq.

The next lemma is the core of the completeness proof. In particular, this is the place where the induction rule for α * is used. Case α = βγ : We reason as follows:

⊢ C → [βγ ]¬D ⇐ ⊢ C → [β][γ ]¬D axiom (9) ⇐ ⊢ C → ⟨β⟩⟨γ ⟩D → ⊥ lemma 6.6(4)
⇐ ⊢ C → ⟨β⟩(( S) ∧ ⟨γ ⟩D) → ⊥ lemma 6.5(1)

⇐ ⊢ C → ⟨β⟩( E ∈S (E ∧ ⟨γ ⟩D)) → ⊥ ⇐ ⊢ C → E ∈S (⟨β⟩(E ∧ ⟨γ ⟩D)) → ⊥ lemma 6.6(6) ⇐ ⊢ C → ⟨β⟩(E ∧ ⟨γ ⟩D) → ⊥ (for E ∈ S)
By assumption, we have

C β ̸ ⇝ S E or E γ ̸ ⇝ S D. By induction hypothesis, we obtain either ⊢ C → [β]¬E or ⊢ E → [γ ]¬D.
The claim then follows with lemma 6.6(3) and lemma 6.6(2). Case: α = β * : We want to apply the induction rule with a suitable invariant. We define

I { E ∈ S | C β *
⇝ S E }. We clearly have C ∈ I and therefore ⊢ C → I . By assumption, D I and therefore ⊢ I → ¬D since for every E ∈ I we have E D and therefore ⊢ E → ¬D (lemma 6.4). Using the induction rule with ψ set to I , it suffices to show ( I ) → [β]( I ). We reason as follows:

⊢ ( I ) → [β]( I ) ⇐ ⊢ E → [β]( I ) E ∈ I ⇐ ⊢ E → ⟨β⟩(¬ I ) → ⊥ lemma 6.6(4)
⇐ ⊢ E → ⟨β⟩( S \ I ) → ⊥ lemma 6.5(2)

⇐ ⊢ E → ( F ∈S \I ⟨β⟩F ) → ⊥ lemma 6.6(6) ⇐ ⊢ E → ⟨β⟩F → ⊥ F ∈ S \ I ⇐ ⊢ E → [β]¬F lemma 6.6(4) Since E β ̸ ⇝ S F
by the definition of I , the last claim follows by induction hypothesis. □ Remark 3. The previous lemma can be seen as a generalization of the contrapositive of [18, Lemma 1] from the collection of maximally consistent clauses (over a given universe) to arbitrary corefutable collections of maximal Hintikka sets (i.e., all possible intermediate states of pruning). We need the generalization in order to incrementally construct Hilbert derivations and the contrapositive since at the current point in the development there is no easy way to show that provability of formulas is decidable. Decidability of provability does follow once we have established decidability of satisfiability and completeness (cf. corollary 6.12). Lemma 6.8 (Admissibility of P2). Let S ⊆ S 0 be corefutable and let

C ∈ S with [α]φ -∈ C such that ¬∃D ∈ S.C α ⇝ S D ∧ φ -∈ D. Then ⊢ ¬C. Proof. Let X { D ∈ S | φ -∈ D }.
In order to prove ¬C, we show that C implies both [α]( D ∈X ¬D) and ⟨α⟩ X and that that these two consequences are contradictory. For the first implication we reason as follows:

⊢ C → [α]( D ∈X ¬D) ⇐ ⊢ C → D ∈X [α]¬D lemma 6.6(5) ⇐ ⊢ C → [α]¬D D ∈ X
The last claim follows with lemma 6.7 since C α ̸ ⇝ S D by assumption. For the second implication we have:

⊢ C → ⟨α⟩ X ⇐ ⊢ ¬[α]φ → ⟨α⟩ X ¬[α]φ ∈ C ⇐ ⊢ ⟨α⟩¬φ → ⟨α⟩ X lemma 6.6(4) ⇐ ⊢ {φ -} → X lemma 6.6(1)
This time, the last claim follows with lemma 6.2. Now it suffices to show

⊢ [α]( D ∈X ¬D) → ⟨α⟩( X ) → ⊥ ⇐ ⊢ ⟨α⟩(( D ∈X ¬D) ∧ X ) → ⊥ lemma 6.6(3) ⇐ ⊢ ¬(( D ∈X ¬D) ∧ X ) lemma 6.6(2)
The last claim follows with propositional reasoning. Thus we obtain ⊢ ¬C. □ Lemma 6.9. ⊢ ¬C whenever C is pruning refutable.

Proof. By induction on pref C using lemmas 6.3 and 6.8. □

We are now in the position to prove our main result for PDL. We say a predicate P : X → Prop is decidable if there is a function p : X → B such that Px ↔ (p x = true) for all x : X (i.e., p decides P). With respect to this (shallow) notion of decidability, we also obtain: Corollary 6.12 (Decidability). Satisfiability, validity and provability of formulas are decidable.

Proof. Immediate with soundness and completeness. □ Corollary 6.13 (Small-Model Property). Let φ be satisfiable. Then φ is satisfied by a model with at most 2 2|φ | states.

Proof. Immediate with soundness. □ Note that we prove the small-model property (smp) using a decision procedure rather than proving decidability using the smp as is often done in classical arguments.

Converse

We now extend the informative completeness result from PDL to CPDL. The proofs remain largely the same as for PDL. Therefore we only describe the parts that need to be changed. The formalization accompanying this paper [START_REF] Doczkal | Coq development accompanying this paper[END_REF] includes separate developments for the two logics.

We extend the syntax with a new program construct α ⌣ . The satisfaction relation for CPDL is defined as for PDL with the interpretation of α ⌣ defined as:

w α ⌣ ⇒ v v α ⇒ w
Following [START_REF] Harel | Dynamic Logic[END_REF], the Hilbert system for CPDL extends the Hilbert system from fig. 2 with two axioms:

⊢ φ → [α]⟨α ⌣ ⟩φ (13)
⊢ φ → [α ⌣ ]⟨α⟩φ (14)
By duality we obtain:

Lemma 7.1. ⊢ ⟨α⟩[α ⌣ ]φ → φ and ⊢ ⟨α ⌣ ⟩[α]φ → φ.
The main problem in extending the proof to CPDL is to adapt the proof of lemma 4.4. It turns out that the Hintikka conditions (definition 4.1) are insufficient to handle the case for converse appearing on top of other programs. We resolve this by showing that the Hilbert system validates a conversion to converse normal form (i.e., formulas where converse is only applied to atomic programs) and then restricting to converse normal formulas.

We start by computing converse normal forms. We want to exhaustively apply the following transformations to programs.

(α + β) ⌣ → α ⌣ + β ⌣ α * ⌣ → α ⌣ * (α β) ⌣ → β ⌣ α ⌣ α ⌣⌣ → α
As with the computation of the Fisher-Ladner closure, we define two functions cnf : formula → formula cnp : bool → program → program by mutual recursion on formulas and programs as shown in fig. 4. The boolean argument for cnp serves as a flag signaling whether we are currently pushing down a converse Lemma 7.2.

cnf p p cnf (φ → ψ ) cnf φ → cnf ψ cnf ⊥ ⊥ cnf ([α]φ) [cnp false α](cnf φ) cnp false a a cnp true a a ⌣ cnp false (α β) (cnp false α)(cnp false β) cnp true (α β) (cnp true β)(cnp true α) cnp b (α + β) cnp b α + cnp b β cnp b (α * ) (cnp b α) * cnp b (φ?) (cnf φ)? cnp b (α ⌣ ) cnp (¬b) α
1. ⊢ φ ↔ cnf φ 2. ⊢ [cnp true α]ψ ↔ [α ⌣ ]ψ 3. ⊢ [cnp false α]ψ ↔ [α]ψ
Proof. We show claim (1) and the conjunction of ( 2) and ( 3) by mutual induction on φ and α. Most cases follow immediately with the respective induction hypotheses. It remains to show

⊢ [α]φ ↔ [β]φ whenever α → β. We show one direction of the case for α * ⌣ → α ⌣ * . ⊢ [α ⌣ * ]φ → [α * ⌣ ]φ ⇐ ⊢ [α * ⌣ ]⟨α * ⟩[α ⌣ * ]φ → [α * ⌣ ]φ axiom (14)
⇐ ⊢ ⟨α * ⟩[α ⌣ * ]φ → φ lemma 6.6(1)

⇐ ⊢ ⟨α * ⟩[α ⌣ * ]φ → [α ⌣ * ]φ axiom (10) ⇐ ⊢ ⟨α⟩[α ⌣ * ]φ → [α ⌣ * ]φ lemma 6.6 (7)
(and ⊢ [α ⌣ * ]φ → [α ⌣ * ]φ) ⇐ ⊢ ⟨α⟩[α ⌣ ][α ⌣ * ]φ → [α ⌣ * ]φ axiom (11)
The last claim follows with lemma 7.1. □ Note that in the proof above, we need to generalize the claim using axiom (10) before applying the induction lemma (lemma 6.6 [START_REF] Cohen | A finset and finmap DRAFT library[END_REF]).

We extend the definition of FL □ with an additional clause for converse

FL □ (α ⌣ , φ) {[α ⌣ ]φ} ∪ FL □ (α, φ) Lemma 7.3. If φ is converse normal, then all ψ ∈ FL(φ) are converse normal.
The only place in the proof where we need to exploit the fact that we can restrict to converse normal formulas is when adapting the proof of lemma 4.4. We adapt the transition relation on sets of clauses by changing the case for atomic programs to respect converses of atomic programs

C a ⇝ S D { φ + | [a]φ + ∈ C } ⊆ D ∧ { φ + | [a ⌣ ]φ + ∈ D } ⊆ C
and adapt the definition of M(S) accordingly. Proof. By induction on α. The case for a ⌣ is symmetric to the case for a. All other cases are essentially the same as in the proof of lemma 4.4.

□

The translation to Hilbert refutations requires the addition of two new cases to the proof of lemma 6.7. Firstly, C a ⇝ S D can now also fail because φ + C for some formula [a ⌣ ]φ ∈ D. Secondly, we need to handle the case where C α ⌣ ̸ ⇝ S D. Both cases are straightforward.

Theorem 7.5. For every CPDL formula φ, one can either construct a proof of ¬φ or a model with at most 2 4|φ | states satisfying φ.

Proof. Let φ be some formula. Then ⊢ φ ↔ cnfφ (lemma 7.2) and |U (φ)| ≤ 4|φ| since |cnf φ| ≤ 2|φ|. The claim then follows analogously to the proof of theorem 6.10. □

The corollaries from the previous section carry over to CPDL as expected.

We remark that, since CPDL has both more syntactic constructs and a Hilbert system with more axioms, the completeness result for CPDL does not subsume the completeness result for PDL.

Remarks on the Formalization

The Coq development accompanying this paper [START_REF] Doczkal | Coq development accompanying this paper[END_REF] follows the mathematical development fairly closely and provides the details elided in the paper. The development consists of about 1300 lines for CPDL and 1000 lines for PDL split roughly halfand-half between specifications and proofs. This conciseness is achieved by relying on the mathematical component libraries [START_REF]The Mathematical Components team[END_REF] as well as two libraries developed in [START_REF] Doczkal | A Machine-Checked Constructive Metatheory of Computation Tree Logic[END_REF]. The latter two account for another 2000 lines.

The first library is for reasoning about finite sets over countable base types (e.g., formulas) and used to define the Fisher-Ladner closure, clauses, demos, and pruning. While the mathematical component libraries do contain a library for extensional finite sets, this library only provides sets over finite types, which is too restrictive for our purposes. While we use finite sets as data structure underlying the pruning method for deciding PDL satisfiability, the purpose is to allow for a constructive proof rather than actually running the procedure. Consequently, we implement finite sets without regard for computational costs. We obtain an extensional representation by representing each set using some canonical duplicate free list. In addition to the usual operations (e.g., separation, replacement, and powerset), the library also features a number of constructions not needed here (e.g., fixpoint operators for bounded monotone functions) and comes with rudimentary automation based on a tableau calculus implemented in Ltac [START_REF] Anisimov | Proof Automation for Finite Sets[END_REF]. We remark that there is another library for finite sets over countable types [START_REF] Cohen | A finset and finmap DRAFT library[END_REF], currently being developed with the aim of integrating it into the mathematical component libraries, incorporating some of the design decisions underlying our finite set library.

The second library underlying the development is a library for constructing Hilbert derivations. It is folklore that reasoning inside deeply embedded proof systems (i.e., where the proof system is represented using an inductive definition) is cumbersome in Coq. This is particularly true for reasoning inside a bare Hilbert system due to the lack of assumption management. The libraries developed in [START_REF] Doczkal | A Machine-Checked Constructive Metatheory of Computation Tree Logic[END_REF] provide tactics for assumption management for any Hilbert system extending classical propositional logic. Further, it provides the instances to enable (setoid) rewriting [START_REF] Sozeau | A New Look at Generalized Rewriting in Type Theory[END_REF] with the preorder φ ≺ ψ ⊢ φ → ψ . The facilities for assumption management are mainly used when proving basic, often propositional, facts. For the more high-level lemmas (e.g., lemma 6.7) rewriting with ≺ is the main source of automation. We remark that rewriting with equivalences alone would be too restrictive for our purposes since many important facts (e.g., axioms ( 13) and ( 14)) are only implications.

Morally, we see proofs as computational objects that can be inspected and manipulated. However, the need for setoid rewriting described above forces us to formalize the Hilbert systems as predicates (i.e., ⊢ : formula → Prop) rather than as families of types (i.e., ⊢ : formula → Type). While the introduction of universe polymorphism in recent versions of Coq allows, in principle, to use setoid rewriting also for type families, we ran into technical problems that we were, so far, unable to resolve when trying to turn the Hilbert systems into type families.

From the engineering point of view, it is also unfortunate that we were forced to create two separate developments for PDL and CPDL even though there is a considerable overlap between the two proofs. We could have obtained a limited amount of sharing by proving basic facts about the Hilbert systems (e.g., lemma 6.6) for a structure hiding the inductive nature of the Hilbert system (i.e., the fact that there are no other axioms) and then instantiating this structure with the Hilbert systems for both PDL and CPDL. This approach was used in [START_REF] Doczkal | A Machine-Checked Constructive Metatheory of Computation Tree Logic[END_REF] to build a hierarchy of Hilbert systems including propositional logic, K, K * , and CTL. However, given the large number of syntactic constructs for PDL and the fact that we only need about a dozen of these basic facts, the gains would be marginal at best. One option to merge the two developments might have been the introduction of a boolean flag, along the lines of the formalization underlying [START_REF] Pous | Kleene Algebra with Tests and Coq Tools for while Programs[END_REF], signaling the presence or absence of converse in definitions and lemma statements. This could provide for significant sharing, at the cost of some technical overhead and slightly less natural definitions and lemma statements.

Conclusion

We have given formal and constructive completeness proofs for PDL and CPDL by combining ideas and techniques from a variety of sources [START_REF] Harel | Dynamic Logic[END_REF][START_REF] Kaminski | Incremental Decision Procedures for Modal Logics with Nominals and Eventualities[END_REF][START_REF] Kozen | An Elementary Proof of the Completness of PDL[END_REF]. We consider the constructive argument given here more informative than a classical completeness proof in the sense that it provides an algorithm constructing both finite models for satisfiable formulas and proofs for valid formulas. 3 In addition to basing the proof on an algorithm, we also prove the correctness of this algorithm without classical assumptions. The reason for this is twofold. First, classical assumptions (besides those localized to classical models) are simply not necessary. Moreover, working without axioms allows us to appeal to the normalization property of the logic of Coq. This, for instance, yields that the shallow notion of decidability used in corollary 6.12 entails computational decidability in the usual sense.

The completeness proof is designed to be constructive while reusing ideas from the literature wherever possible. The desire to work constructively essentially rules out the approach in [START_REF] Harel | Dynamic Logic[END_REF], where completeness is established by using filtration on an infinite non-standard canonical model. In fact, even the construction of a finite "canonical" model for a given subformula universe in [START_REF] Kozen | An Elementary Proof of the Completness of PDL[END_REF] is non-constructive in the sense that it requires decidability of Hilbert provability in order to determine which formulas are contained in which state. Of course, Hilbert provability is decidable (corollary 6.12) However, since the Hilbert system is not analytic, the easiest way to establish this is via completeness. This motivates basing the proof on a decision method. We use pruning since the maximal demo it constructs corresponds closely to the model employed in [START_REF] Kozen | An Elementary Proof of the Completness of PDL[END_REF]. This allows us to obtain one of the key lemmas in the translation from pruning refutations to Hilbert refutations by adapting the corresponding lemma in [START_REF] Kozen | An Elementary Proof of the Completness of PDL[END_REF]. Altogether, we obtain a natural factorization of the proof into an algorithmic part for the decision method, a semantic argument for the model construction, and a syntactic translation from pruning refutations to Hilbert refutations.

By using converse normalization, we were able to adapt the proofs for PDL to CPDL with only a few local changes. We remark that proving the commutation properties underlying the correctness of converse normalization (lemma 7.2) turned out to be surprisingly tricky, in particular as it comes to ⊢ [α * ⌣ ]φ ↔ [α ⌣ * ]φ where both directions require a generalization of the statement before the induction rule is applied. Our attempts to find the relevant arguments in the literature were unsuccessful. The Coq development [START_REF] Doczkal | Coq development accompanying this paper[END_REF] contains all arguments in their entirety.

There are a number of methodical differences between the proofs presented here and the constructive completeness proofs for CTL in [START_REF] Doczkal | A Machine-Checked Constructive Metatheory of Computation Tree Logic[END_REF][START_REF] Doczkal | Completeness and Decidability Results for CTL in Constructive Type Theory[END_REF]. The most fundamental one is the use of the more traditional Hintikka sets in favor of literal clauses and support. Here, literal clauses are clauses containing only formulas of the form [a]φ σ and p σ and the support relation is a recursively-defined decidable predicate corresponding to the Hintikka conditions, e.g.,

C ▷ (φ → ψ ) + C ▷ φ -∨ C ▷ ψ +
That is, the support relation is defined such that a literal clause supports all its possible Hintikka extensions. In [START_REF] Doczkal | A Machine-Checked Constructive Metatheory of Computation Tree Logic[END_REF], where pruning refutations are also translated to derivations of the sequent system for CTL presented in [START_REF] Brünnler | Cut-free sequent systems for temporal logic[END_REF], the support relation provides a natural fit for the destructive reading of the sequent rules (i.e., the reading where the active formula is removed when applying a rule and next state rules are applied to literal clauses only). We would have preferred to extend the methodology employed for CTL also to PDL. However, as observed in [START_REF] Abate | An On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability[END_REF][START_REF] Kaminski | Incremental Decision Procedures for Modal Logics with Nominals and Eventualities[END_REF], a naive recursive definition of support for PDL, employing

C ▷ [α * ]φ + C ▷ φ + ∧ C ▷ [α][α * ]φ
to handle transitive closure, does not terminate on [a * * ]p + . This is sometimes called the nested star problem. While a notion of support can be defined for PDL [START_REF] Kaminski | Incremental Decision Procedures for Modal Logics with Nominals and Eventualities[END_REF], it is not clear whether the Hilbert system is expressive enough for constructing derivations based on this definition. When moving from literals and support to Hintikka sets, the recursive definition of the support relation is replaced with the checking of closure properties for Hintikka sets, thus avoiding the nested star problem.

Brünnler and Lange [START_REF] Brünnler | Cut-free sequent systems for temporal logic[END_REF] suggest that, following the same methodology as for CTL, it should be possible to obtain an analytic sequent system for PDL. To the best of our knowledge, the details have not been worked out yet. It would be interesting to see if such an analytic sequent system can indeed be derived for PDL and whether a pruning based argument can be used to show its completeness.

( 3 )

 3 follow by mutual induction on φ for (2) and α for (3). □ Lemma 3.3. FL(φ) is subformula closed. Proof. Immediate with lemma 3.2(1) and lemma 3.2(2). □ Lemma 3.4. |FL(φ)| ≤ |φ| and |FL □ (α,ψ )| ≤ |α |.

Definition 4 . 1 .

 41 A clause H is called a Hintikka set if satisfies the following closure conditions.

Lemma 4 . 4 .

 44 Let [α]φ + ∈ C such that C α ⇒ M(D) D and for all E ∈ S and all ψ with |ψ | < |α | we have that t -∈ E implies E ̸ |= ψ . Then φ + ∈ D. Proof. By induction on α. The assumption on formulas smaller than α is required to handle the case for tests. □ Lemma 4.5. Let {C, D} ⊆ D such that C α ⇝ D D and assume that ψ + ∈ E implies E |= ψ for all E ∈ D and all ψ such that |ψ | < |α |. Then C α ⇒ M(D) D.

Theorem 4 . 6 (

 46 Demo Theorem). Let φ σ ∈ C ∈ M(D). Then C |= φ σ .Proof. By complete induction on |φ|. The case for φ = [α]ψ + follows with lemma 4.4 using the induction hypothesis to establish the condition on formulas smaller than |α |. Similarly, the case for φ = [α]ψ -follows with the demo condition and lemma 4.5. All other cases follow by induction using the Hintikka properties of C. □

Lemma 6 . 2 (

 62 Extension). Let S ⊆ S 0 be corefutable and letC ⊆ U be a clause. Then ⊢ C → { D ∈ S | C ⊆ D }. Proof. Since S is corefutable, it suffices to show ⊢ C → { D ∈ S 0 | C ⊆ D }. The claim follows by induction on |U | -|C |. If C is maximal, then either C ∈ S 0 or ⊢ ¬C (lemma 6.1). Both cases are trivial. If C is not maximal then ⊢ C → C ∪ {φ + } ∨ C ∪ {φ -} for some φ ∈ F such that {φ + , φ -} ∩ C = ∅and the claim follow by induction hypothesis. □ Lemma 6.3 (Admissibility of P1). Let S be corefutable and let C ⊆ U such that S ̸ ▷ C. Then ⊢ ¬C. Proof. Immediate with lemma 6.2. □ Before we can translate the rule P2, we need a few more auxiliary lemmas. Lemma 6.4. Let C, D ⊆ U be maximal. Then ⊢ C → ¬D whenever C D. Lemma 6.5. Let S ⊆ S 0 be corefutable. Then 1. ⊢ S. 2. ⊢ ¬( A) → (S \ A) for all A ⊆ S. Proof. Claim (1) follows immediately with lemma 6.2. For (2) it suffices to show ⊢ C → ¬( A) → (S \ A) for C ∈ S (Claim (1)). If C ∈ A we obtain a contradiction with ¬ A.

Lemma 6 . 7 .

 67 Let S ⊆ S 0 be corefutable and let C, D ∈ S. Then ⊢ C → [α]¬D whenever C α ̸ ⇝ S D. Proof. By induction on α. Case α = a: By assumption, there exists some [a]φ + ∈ C such that φ + D. Hence φ -∈ D since D is maximal. To show ⊢ C → [a]¬D it therefore suffices to show ⊢ [a]φ → [a]¬¬φ which follows with lemma 6.6(1). Case: α = ψ ?: By axiom (12), it suffices to show ⊢ C → ψ → ¬D. Since C ψ ? ̸ ⇝ S D, we either have C D and the claim follows with lemma 6.4 or C = D and ψ + C. But then, ψ -∈ C since C is maximal. Therefore ⊢ C → ¬ψ and the claim follows with propositional reasoning. Case α = β + γ : By induction hypothesis we have both ⊢ C → [β]¬D and ⊢ C → [γ ]¬D. The claim then follows with axiom (5).

Theorem 6 . 10 (

 610 Informative Completeness). For every PDL formula φ, one can either construct a proof of ¬φ or a model with at most 2 2|φ | states satisfying φ. Proof. Fix some formula φ. By theorem 5.4, we either obtain a model for φ of size 2 |U (φ) | and the claim follows with lemma 3.4 or we have pref C and the claim follows with lemma 6.9. □ In Coq, theorem 6.10 takes the form of a function having the (dependent) type ∀φ. (ΣM (x : M). |M | < 2 2|φ | ∧ w |= φ) + (⊢ ¬φ) Corollary 6.11 (Completeness). ⊢ φ whenever φ is valid.

Figure 4 .

 4 Figure 4. Converse Normalization

Lemma 7 . 4 .

 74 Let D be a demo containing only converse normal formulas and let [α]φ + ∈ C such that C α ⇒ M(D) D and for all E ∈ S and all ψ with |ψ | < |α | we have that t -∈ E implies E ̸ |= ψ . Then φ + ∈ D.

  depends on the injectivity of the box constructor. In Coq, we instead use replacement and separation (i.e., { body φ | φ ∈ { ψ ∈ C | isBoxψ } }, where isBox tests for the shape [α]φ + and body strips away the outer box) yielding a set that is finite by construction.

	Note that

α ⇝ S , does not mention the satisfaction relation. This allows us to use α ⇝ S to phrase the condition ensuring that α ⇒ and |= behave as required.

Definition 4.3 (Demo). A finite set D of Hintikka sets is called a demo if it satisfies the following condition:

  pref C Figure 3. Pruning Refutations expresses the fact a clause cannot be supported by D if all clauses that could possibly support it have already been removed and the rule P2 corresponds to the pruning condition.

Lemma 5.3. D is pruning corefutable. Theorem 5.4 (Pruning Completeness). Let C ⊆ U , then C is either pruning refutable or satisfied by a model with at most 2 |U | states. Proof. By case analysis on D ▷ C using theorem 4.6 and lemmas 5.2 and 5.3. □

Here, shallow refers to the fact that w |= φ is just a proposition talking about some relations over an arbitrary type.

More precisely, it provides an algorithm that is, while still impractical, more informative than blindly enumerating proofs.

* This author has been funded by the European Research Council (ERC) under the European Union's Horizon 2020 programme (CoVeCe, grant agreement No 678157). This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR). CPP 2018, January 8 -9, 2018, of the work. It is posted here for


Aicha Bakki
email: aicha.bakki@univ-lemans.fr

Lahcen Oubahssi
email: lahcen.oubahssi@univ-lemans.fr

Chihab Cherkaoui
email: ccherkaoui@yahoo.fr

Sebastien George
email: sebastien.george@univ-lemans.fr

Motivation and Engagement in MOOCs: How to Increase Learning Motivation by Adapting Pedagogical Scenarios?

Keywords: MOOC, Motivation, dropout, personalization, adaptivity, pedagogical scenario, engagement, learning model, learning design

With the MOOC movement, education stakeholders are taking part of a pedagogical renewal. These dynamics present different advantages such as: massiveness, openness, accessibility, etc. However, it raises particular issues related to the dropout. To remedy to this issue, a promising lead resides in supporting learners' motivation and engagement. To reach this goal, innovative pedagogic strategies and / or sophisticated Instructional design, personalization or even adaptability are needed. The purpose of this paper is to examine the point of view of literature, the dropout issue and possible solutions to motivate learners.

Introduction

MOOCs are distinguished from E-Learning platforms by different characteristics such as the massiveness, openness, accessibility, certification, the nature and programming of content, assessment modalities, etc. All of these characteristics offer added value to education in general and to major stakeholders involved in online learning process (teachers, learners and tutors). For teachers for example, it is a question to think about the learning activity by formalizing pedagogical scenarios and implementing them through new technologies and modalities. This allow us experimenting although different educational approaches and content, but also promoting sharing and reusing content and best practices. For the learner, many benefits can be distinguished namely: flexibility, accessibility, openness, collaboration, autonomy, etc.

The aim of our work is to conceive and develop various tools that consider complementary and plural aspects of online learning, through individual and/or adaptive, collaborative, fun and massive dimensions. We consider particularly the dropout issue and we propose a synthesis of approaches to reduce the dropout rate. Therefore, the perspective of our work is to refine these approaches to provide models, tools and techniques enhancing MOOCs centric scenarios by trying to capture the issues of motivation and adaptation.

The main purpose of this communication is to not examine the contribution of MOOCs in achieving the guidelines traced at the beginning, but to discuss new issues raised, especially dropout rates. Indeed, for reference, most authors point out a success rate that not exceed 10% [START_REF] Liyanagunawardena | MOOCs: A systematic study of the published literature 2008-2012[END_REF]. In a deeper analysis of this issue, several authors link this dropout to a lack of learners' motivation, or a lack of learners' engagement [START_REF] Anderson | Promise and/or Peril: MOOCs and Open and Distance Education. Commonwealth of Learning[END_REF][3] [START_REF] Kizilcec | Deconstructing disengagement: analyzing learner subpopulations in massive open online courses[END_REF]. These dropout rates are also associated with an insufficiency of tools and methods that allow personalization and/or adaptation of learning activities, in order to motivate learners in these environments [START_REF] Kizilcec | Deconstructing disengagement: analyzing learner subpopulations in massive open online courses[END_REF].

Dropout issue in MOOCs

Many researchers have examined the dropout issue in MOOCs. Clow [START_REF] Clow | MOOCs and the funnel of participation[END_REF] explain the dropout rate by the demotivation of learners. Anderson [START_REF] Anderson | Promise and/or Peril: MOOCs and Open and Distance Education. Commonwealth of Learning[END_REF] emphasized that several participants "enroll" just to satisfy their curiosity without any intention to complete the course. Other researches are around the engagement of learners in a MOOC, we cite in particular: the work of Kizilcec et al. [START_REF] Kizilcec | Deconstructing disengagement: analyzing learner subpopulations in massive open online courses[END_REF]. They explore an empirical study about the lack of engagement of learners and its causes in MOOCs; but also the lack of interaction between participants in MOOC. In the same sense, the fact participants' isolation is considered by many authors as one of the main reasons behind the weak engagement of the participants [START_REF] Cisel | Etudier les interactions dans les MOOCs[END_REF].

To study the dropout issue in MOOCs, we examined the work related to learner's profiles in MOOCs. In this sense, we note the work of Kizilcec et al. [START_REF] Kizilcec | Deconstructing disengagement: analyzing learner subpopulations in massive open online courses[END_REF] and Hill [START_REF] Hill | Some validation of MOOC student patterns graphic[END_REF]. They introduce classifications of learners that interacting with the platform. For illustration, we summarize Hill's work [START_REF] Hill | Some validation of MOOC student patterns graphic[END_REF]. He proposed a classification of participants in a MOOC according to their degree of involvement in five categories: Active, passive, Drop-ins, Observers & No-shows.

Some possible solutions to minimize dropout

Based on a literature review, we can distinguish four different approaches to minimize the dropout rate: Pedagogical strategies approach. It is a number of theoretical strategies validated by empirical studies. Among the pedagogical strategies discussed in the literature, we highlight the work of Williams [START_REF] Williams | Applying Cognitive Science to Online Learning[END_REF] of adding motivational messages to students when they solve mathematics problems [START_REF]Khan Academy platform[END_REF].

Personalization and/or adptivity approach. Several researches focus on the importance of personalization to avoid dropout. In this context, we can mention PERSUA2MOOC project [START_REF] Clerc | Mise en Place de la Personnalisation Dans le Cadre des MOOCs[END_REF]. This project provides a system for personalization of learning outcomes in MOOCs. PERSUA2MOOC is a project that aims to "adapt" the learning activities considering the individualities and teachers educational activities. Gamification approach. Integrating games into the learning process is a solution to capture a larger audience. Indeed, the coupling of learning, virtual reality and video games allow to consider the integration of serious games in the online learning process. We can mention the work of [10][11].

Technological approach. Finally, we note that in addition to video, MOOCs also follow technological ascent implementing other tools web2.0, namely, social networks, wikis, forums, etc.

Discussion

First observations in MOOCs: a revolutionary platform, a new educational reform and a very high dropout rates. A learner-centered approach reveals several difficulties. In the first place, defining the learners' profiles that enroll in MOOC and their initial motivations. Second, massiveness, which constitutes a major issue when we talk about monitoring, mentoring or coaching: how to handle a huge number of learners? Especially as the MOOCs do not offer proximity between teachers and learners. We also highlight the importance of considering two fundamental aspects MOOC: massiveness and openness in the process of elaboration of pedagogical scenarios. We speak more and more about personalization and adaptivity to reduce dropout rates. Moreover, many researches have been specified in this sense. Research works in TEL, in this context, have allowed the development of different approaches and methods; that have been recovered under the MOOCs. We have specified, the project PERSUA2MOOC [START_REF] Clerc | Mise en Place de la Personnalisation Dans le Cadre des MOOCs[END_REF] which presents a personalization in MOOC according to Learners' profiles.

Our work focuses on supporting learners' motivation through instructional scenario building, by implementing tools and models specific to the field of TEL but also cognitive science and educational sciences. Indeed, the elaboration of our work spread over several layers. The principal layer includes different TEL platforms and tools. It integrates also different works specified in: instructional scenario building, learners' profiles and different motivation theories.

However, we must consider the different types of MOOCs. We distinguish two principal types: xMOOCs and cMOOCs, each having their own technological and pedagogical characteristics. They represent two pedagogical models that consider the video as primary course support, but disjoining in instructional scenario building models that they offer. So many other types are emerging nowadays, to prevent some dysfunctions in MOOCs, but the purposes of this paper will be limited to xMOOCs and cMOOCs. xMOOC is most of the time comprising traditional approaches of teaching and learning, it places the teacher as the main leader in the pedagogical scenario process, whereas cMOOC is more collaborative. It integrates the learner in a dynamic multi-actors process of instructional scenario building. According to this, we believe that cMOOCs are adapted to our research vision and approach.

Our approach consists to study instructional scenario building process, in cMOOCs, according to three points of view: massiveness, openness and motivation. Our research problematic can be summarized in three questions:

Which pedagogical context model to comply with learning rhythm in a massive environment? Our objective is to be able to manage and adapt the pedagogical activities in MOOCs in order to create a favorable environment for learning and personal development.

Which model or approach of the motivational theory should be used? Our goal is to identify and adapt the various existing motivation approaches, models and theories to reduce dropout rates.

Which model to adopt to organize and sequence teaching activities? Our goal is to manage and adapt pedagogical scenario in MOOCs in order to respect the aspects of opening (a specificity of MOOCs).

Conclusion

Following the various issues presented, we posed a first draft of the current problems related to the issue of dropout in MOOCs. The synthesis of the literature highlights our views on the approach of dropout along three dimensions: possible causes of dropout, research related to the types of participants and solutions to minimize the dropout rate. All points are complementary. The objective of our work is to propose an approach, models, methods and techniques to users of MOOCs, to take into account motivation concept in the design and / or adaptation of their pedagogical scenarios.