Keywords

AMS Subject Classifications

1 Introduction

Air Traffic Control (ATC) is an important factor for the airliner operations, guiding the aircraft on the air and on the ground. ATC is responsible for organizing the air traffic flow in an efficient way, while ensuring the safety.

The separation of aircraft is the concept of keeping a minimum distance between aircraft to avoid collisions and possible accidents caused by wake turbulence. The lift that the aircraft’s wing is designed to produce directly affects the intensity and lifespan of the generated vortex. Therefore, the separation minima is based upon wake vortex categories of the preceding and the following aircraft which, in turn, are derived from the maximum takeoff weight (MTOW) or the maximum takeoff mass (MTOM) [8, 10, 13, 14].

Due to the increasing traffic and congested airports, regulation changes are currently being planned, with the aim of increasing airport capacity [6, 12, 14, 17]. The first step is the wider adaptation of RECAT, which recategorizes aircraft and sets new standards for wake turbulence separation minima. Therefore, the wingspan is used as an additional to MTOW/MTOM parameter. As a result, aircraft are placed into six wake vortex categories, common for departure and arrival separation, which enhance both safety and efficiency [8, 11, 14]. The second step is a static separation matrix of distance and time for both arrivals and departures for the common commercial aircraft, called RECAT-2 [7]. The third step, RECAT-3, will provide dynamic pair-wise spacing that will vary with atmospheric conditions and aircraft performance [7]. However, if in the future the concepts of Free Flight and Self-Separation are employed, the management of air traffic will be revolutionized. They consist of decentralized methods of ATC, using computer communication to reserve parts of the airspace dynamically and automatically in a distributed way [20].

The above mentioned changes mandate the modernization of the current infrastructure, as their application necessitates the operation of relevant computer systems. For example, a specialized tool will be required to apply RECAT-2, because of the size of the separation matrix. Besides, after the realization of Free Flight and Self-Separation concepts, conflict avoidance will be totally automated, relying only on computer systems and computer communication between aircraft.

Our research project aspires to support the evolution of ATC. We propose a rule-based approach to model ATC regulations in the terminal airspace. Our approach allows the validation and verification of its formal properties [15], without compromising the compliance with the regulations. We have used the reference Naf Hornlog implementation of RuleML rule language, OO jDREW, taking advantage of its suitable built-in predicates and functions, and its vast multi-agent and distributed systems compatible API. Furthermore, our approach can serve as a tool for the application of both current and future regulations on the field.

Our main contributions are as follows: (i) we developed rules, derived from the regulations, for the definition of wake vortex categories; (ii) we developed rules concerning the separation minima during the landing phases; (iii) a large database of more than 200 types of aircraft was developed, containing the characteristics required to compute the above. Additionally, we developed a reference airport database, containing characteristics of airports in Greece; (iv) we developed the mathematical background within the rule base, capable of handling the heading of aircraft as well as angles and angle comparison, as a base for future work; (v) we developed rules and a methodology of handling not fully established future regulations, covering different orientations that may follow.

The rest of the paper is organized as follows. Section 20.2 presents related work, while Sect. 20.3 introduces RuleML. Section 20.4, the main part of our paper, presents the design of the rule-base. Finally, Sect. 20.5 concludes the paper and proposes future work.

2 Related Work

To the best of our knowledge, no strict rule-based approach for ATC in the airport area exists. However, a convergence point can be found in other lines of research concerning decision support tools, landing scheduling, and Free Flight. Below, the most related previous work is discussed.

Prototype decision support tools for terminal area and controllers, such as FAST [5], have been developed and evaluated in operation with live air traffic. More complete systems have been developed and tested, such as [17]. An overview of a method for formal requirements capture and validation, in the domain of oceanic ATC is presented in [16]. The obtained model focuses on conflict prediction, while being compliant to the regulations governing aircraft separation in oceanic airspace. The design approach, the specification structure, and some examples of the rules and axioms of the formal specification are provided. Those examples, expressed in Many-Sorted First Order Logic or in the Prolog notation, include rules about conflict prediction and aircraft separation. Supplementary, the model was validated by automated processes, formal reasoning and domain experts.

The objective of landing scheduling is to position all arriving aircraft to a runway and to a specific time window, while respecting separation constraints and minimizing delays [2, 5, 6, 18, 19, 21]. Different algorithms and heuristics are used, the simplest one being first-come first-served (FCFS). Aircraft separation is used as a scheduling constraint. However, it has to be underlined that the regulations requirements are not strictly followed, but constant values or simplified forms are used.

Research in the field of Free Flight concept focuses on model principles and different algorithms for conflict detection and avoidance. In [20], a general platform (NAMA), which is oriented towards agent-based Free Flight implementations, was presented. In the same work, a conflict detection and resolution, based on utility functions without any negotiations between agents, was proposed. However, the separation constraints were not explained. In [12], the authors focused on airport airspace. They developed a multi-agent architecture, and a software prototype. The latter implements an ATC system with distributed policy of conflict resolution, predictive analysis and P2P interaction-based autonomous coordination of aircraft’s motions. Nevertheless, aircraft classes serve only for the estimation of airspeed range and not for the differences in separation between classes.

3 RuleML Basics

RuleML is a markup language, designed to express both top–down and bottom–up rules in XML schema; a shorthand is POSL, that follows a Prolog-like syntax. More specifically, we used OO jDREW, a RuleML implementation that follows Horn Clauses in implication form, supports negation as failure, and is written in the Java programming language.

A Horn Clause in implication form is written as \(h \leftarrow p\wedge q\wedge \ldots \wedge r\), where h, p, q, r are atoms. An atom is of the form \(r(t_1,\ldots ,t_n)\), where r is a predicate of arity n, and \(t_i\) are terms.

In POSL, a clause has the general form:

h :- p,q,...,r.

The head of the clause is h and the body is \(p,q, \ldots ,r\). A clause is called a fact if the body is empty. Neither disjunction nor negation is supported on the body [3]. In this paper, we take advantage of OO jDREW’s built-in equality and inequality predicates, as well as of math functions. The English sentence: “A customer is premium if their spending has been min 5000 euro in the previous year”, part of the classic RuleML example which can be found in [4], can be written in POSL form, using inequality predicates, as follows:

premium(?customer) :-

\(\texttt { spending(?customer, ?amount,"previous year"),}\)

The relation atoms are premium and spending, ?customer and ?amount are variables representing customer’s name and amount spent, respectively, while "previous year" and 5000 are constants and is the type. The built-in predicate greaterThanOrEqual is satisfied iff the first argument is equal to or greater than the second argument. By asserting e.g., the following fact in the Knowledge Base:

the query premium(?x) binds Peter to the variable ?customer, as shown in Fig. 20.1.

Fig. 20.1
figure 1

The query execution tab of OO JDREW

Full size image

The notation used in this paper is: (i) variables are denoted by \(x_k\), (ii) constants and bindings are lower or upper case alphanumericals, (iii) atoms, predicates and functions can be either in the form \(R_k^n(t_1,\ldots t_n)\), or in the simplified form —e.g. \((t_1 < t_2)\)— for equality and inequality predicates.

4 The Rule Base

In this section we present the design of our approach. We express in terms of rules, ATC regulations concerning aircraft separation standards in the airport vicinity under instrument flight rules (IFR). We follow weight classes and the separation of aircraft of different classes according to International Civil Aviation Organization (ICAO) and Federal Aviation Administration (FAA) regulations. Additionally, we decscribe rules regarding airport layout, heading and turns, and weather conditions in order to cover future regulations or complex cases.

The design of the rule base aims to (i) implement ATC regulations adhering to ICAO and FAA standards. (ii) study complex cases (iii) be easily integrated with any existing or future framework (iv) be flexibly adapted to each framework’s requirements.

Handling intersection departures, intersecting runways, intersecting flight path operations and parallel approaches is presented as example of how our proposed rule base efficiently solves complex cases.

4.1 Database

The database, written in RuleML/POSL, contains more than 200 types of aircraft defined by ICAO aircraft designation (a three- or four-character alphanumeric code designating aircraft), with the characteristics needed to compute the separation minima. The data were obtained from [9]. Each entry has a general form of an atom of arity 4 as follows:

$$\begin{aligned} { aircraftChar}(x_{type},\ x_{kg},\ x_{ft},\ x_{kt}) \end{aligned}$$
(20.1)

where \(x_{type}\) denotes the type of the aircraft as defined by ICAO aircraft designation, \(x_{kg}\) denotes the MTOM in kilograms, \(x_{ft}\) the wingspan of the aircraft measured in feet, and \(x_{kt}\) is the approach speed, measured in knots. The corresponding code, for the Airbus A321 (ICAO aircraft designation code: A321), in RuleML/POSL, is as follows:

For each characteristic an individual atom of arity 1 is obtained by the following Horn Clauses, written in an implication form:

$$\begin{aligned} mtom(x_{kg}) \leftarrow aircraftChar(x_{type},\ x_{kg},\ x_{ft},\ x_{kt})\wedge aircraft(x_{type})\nonumber \\ \end{aligned}$$
(20.2)
$$\begin{aligned} wingspan(x_{ft}) \leftarrow aircraftChar(x_{type},\ x_{kg},\ x_{ft},\ x_{kt})\wedge aircraft(x_{type})\nonumber \\ \end{aligned}$$
(20.3)
$$\begin{aligned} appSpeed(x_{kt}) \leftarrow aircraftChar(x_{type},\ x_{kg},\ x_{ft},\ x_{kt})\wedge aircraft(x_{type})\nonumber \\ \end{aligned}$$
(20.4)

where \(aircraft(x_{type})\) must be defined —e.g. aircraft(A321) for the Airbus A321— in the knowledge base as a fact.

Similar atoms are defined for the preceding aircraft:

$$\begin{aligned}&mtomPreceding(x_{kg}) \leftarrow \\&\qquad \qquad \quad aircraftChar(x_{type},\ x_{kg},\ x_{ft},\ x_{kt})\wedge precedingAircraft(x_{type}) \nonumber \end{aligned}$$
(20.5)
$$\begin{aligned}&wingspanPreceding(x_{ft}) \leftarrow \\&\qquad \qquad \quad aircraftChar(x_{type},\ x_{kg},\ x_{ft},\ x_{kt})\wedge precedingAircraft(x_{type}) \nonumber \end{aligned}$$
(20.6)

where \(precedingAircraft(x_{type})\) must be defined as a fact.

Furthermore, the database contains a reference implementation of airports. Each entry in the database is of the form:

$$\begin{aligned} airportChar(x_{code}, x_{or_1}, x_{or_2}, x_{or_3}, x_{or_4}, x_{name_1}, x_{name_2}, x_{name_3}, x_{name_4},\\ x_d, x_{rules}) \nonumber \end{aligned}$$
(20.7)

where \(x_{code}\) is representing the ICAO airport code (a four-character alphanumeric code designating airports), \(x_{or_1}\), \(x_{or_2}\), \(x_{or_3}\) and \(x_{or_4}\) are representing the the exact heading of each runway in degrees in ascending order respectively, \(x_{name_1}\), \(x_{name_2}\), \(x_{name_3}\), and \(x_{name_4}\) are the variables representing the runway designation, \(x_d\) is the distance between the two runways and, the regulations applicable to each airport are denoted by \(x_{rules}\).

Those characteristics are needed to compute the airport layout, the heading during landing, and the initial heading after take-off. Currently, the rule base supports up to two runways in both directions.

As above, atoms of arity 1 are obtained for each characteristic, by the following Horn Clauses, written in an implication form:

$$\begin{aligned} runwayOneOr(x_{or_1}) \leftarrow&airportChar(x_{code}, x_{or_1}, \dots ) \wedge airportName(x_{code})\nonumber \\ \\&\vdots&\nonumber \end{aligned}$$
(20.8)
$$\begin{aligned} runwayOneName&(x_{name_1})\leftarrow \\&\,\ airpor tChar(x_{code},\dots ,x_{name_1},\dots ) \wedge airportName(x_{code}) \nonumber \\&\qquad \qquad \vdots \nonumber \end{aligned}$$
(20.9)
$$\begin{aligned} distanceBtwnRunw(x_d)\leftarrow airportChar(x_{code},..,x_{d},..) \wedge airportName(x_{code})\nonumber \\ \end{aligned}$$
(20.10)

where \(airportName(x_{code})\) must be defined as a fact in the knowledge base, e.g. aiportName(LGTS) for the Thessaloniki Airport “Macedonia” (ICAO airport code: LGTS), an airport with two intersecting runways (10/28 and 16/34). The corresponding entry in the database, in RuleML/POSL, is

Weather information can be useful for simultaneous operations on different runways, or for future expansion to support RECAT-3, Weather Dependent Separations (WDS), and Time-Based Separation (TBS) in strong headwind conditions [7]. The form of the atoms in the database concerning weather information is as follows:

$$\begin{aligned} weather(x_{code},x_{kt},x_{dir}) \end{aligned}$$
(20.11)

where \(x_{code}\) is representing the ICAO airport code, \(x_{kt}\) denotes the wind speed, measured in knots, and \(x_{dir}\) denotes the wind direction.

The following is an example according to METAR information of March, \(21^{st}\), 18:20 UTC, for LGTS:

$$\begin{aligned} weather(LGTS,\ 3, \ variable). \end{aligned}$$
(20.12)

As above, atoms of arity 1 can be obtained by the following Horn Clauses, written in an implication form:

$$\begin{aligned} windSpeed(x_{kt})\leftarrow weather(x_{code},x_{kt},x_{dir})\wedge airportName(x_{code})\nonumber \\\end{aligned}$$
(20.13)
$$\begin{aligned} windDirection(x_{dir})\leftarrow weather(x_{code},x_{kt},x_{dir})\wedge airportName(x_{code})\nonumber \\ \end{aligned}$$
(20.14)

4.2 ICAO Regulations

Current regulations of ICAO categorize aircraft as follows [13, 14]:

 

Light :

MTOM of 7000 kg or less.

Medium :

MTOM of greater than 7000 kg, but less than 136000 kg.

Heavy :

MTOM of 136000 kg or greater.

Super :

- A separate designation that currently only refers to the Airbus A380 (MTOM 575000 kg, ICAO designation A388).

  The categorization can be specified using the following Horn Clauses, (for Light and Medium categories):

$$\begin{aligned} icaoCategory(light)\leftarrow & {} mtom(x_{kg})\wedge (x_{kg}\le 7000) \end{aligned}$$
(20.15)
$$\begin{aligned} icaoCategory(medium)\leftarrow & {} mtom(x_{kg})\wedge (x_{kg}>7000)\wedge (x_{kg}<136000)\nonumber \\ \end{aligned}$$
(20.16)

Airbus A380 would normally belong to Heavy category. Consequently, the definition of Heavy and Super classes is additionally using the aircraft type.

$$\begin{aligned} icaoCategory(heavy)\leftarrow mtom(x_{kg})\wedge (x_{kg}\ge 136000)&\wedge&\\ aircraft(x_{type})&\wedge&(x_{type} \ne A380) \nonumber \end{aligned}$$
(20.17)
$$\begin{aligned} icaoCategory(super) \leftarrow aircraft(A380) \end{aligned}$$
(20.18)

Inequality predicates are built-ins of OO jDREW. The computation of aircraft’s category can be made by defining the type of an aircraft, which must be present at the database as a fact —e.g. aircraft(A321)— and executing the query icaoCategory(?x). Similar rules exist for the preceding aircraft, defining the atom \(icaoCategoryPreceding(x_{class})\).

ICAO separation standards for flights on instrument flight rules (IFR) are presented at Table 20.1.

Table 20.1 Current ICAO weight categories and associated separation minima [14]
Full size table

Those separations standards can be represented by Horn Clauses. For instance, the derived Horn Clauses for the categories heavy, medium are as follows:

$$\begin{aligned} icaoSeparation(mrs) \leftarrow icaoCategory(heavy) \wedge icaoCategoryPreceding(medium) \end{aligned}$$
(20.19)
$$\begin{aligned} icaoSeparation(5) \leftarrow icaoCategory(medium) \wedge icaoCategoryPreceding(heavy) \end{aligned}$$
(20.20)
$$\begin{aligned} icaoSeparation(mrs) \leftarrow icaoCategory(medium) \wedge icaoCategoryPreceding(medium) \end{aligned}$$
(20.21)
$$\begin{aligned} icaoSeparation(4) \leftarrow icaoCategory(heavy) \wedge icaoCategoryPreceding(heavy) \end{aligned}$$
(20.22)

By defining the type of the preceding and following aircraft, the needed separation can be obtained by executing the query icaoSeparation(?x).

4.3 FAA Regulations

The methodology for constructing the rules concerning aircraft classes and separation according to FAA regulations is similar. The FAA is using the following classes [10]:  

Small :

- Aircraft of 41000 pounds (19000 kg) or less MTOW.

Large :

- Aircraft of more than 41000 pounds (19000 kg) MTOW, up to, but not including, 300000 pounds (140000 kg).

Heavy :

- Aircraft capable of takeoff weights of 300000 pounds (140000 kg) or more.

Super :

- A separate designation that currently only refers to the Airbus A380 and the Antonov An-225

B757 :

- Different separation standards are applied for the Boeing 757.

 

The Horn Clauses defining the above regulations, after conversion of pounds to kilograms has been applied, are:

$$\begin{aligned} faaCategory(small) \leftarrow mtom(x_{kg})\wedge (x_{kg}\le 19000) \end{aligned}$$
(20.23)

Boeing 757 would normally belong to Large class, while Airbus A380 and Antonov A225 would belong to Heavy class. Therefore, similar to ICAO categorization, the definition of those classes additionally needs the aircraft type:

$$\begin{aligned} faaCategory(large) \leftarrow aircraft(x_{type})\wedge (x_{type}\ne B757)&\wedge&\\ mtom(x_{kg})\wedge (x_{kg}>7000)&\wedge&(x_{kg}<136000) \nonumber \end{aligned}$$
(20.24)
$$\begin{aligned} faaCategory(heavy)\leftarrow mtom(x_{kg})\wedge (x_{kg}\ge 136000)&\wedge&\\ aircraft(x_{type})\wedge (x_{type}\ne A380)&\wedge&(x_{type} \ne A225)\nonumber \end{aligned}$$
(20.25)
$$\begin{aligned} faaCategory(super) \leftarrow aircraft(A380) \vee aircraft(A225) \end{aligned}$$
(20.26)
$$\begin{aligned} faaCategory(B757)\leftarrow aircraft(B757) \end{aligned}$$
(20.27)

The lack of disjunction in the head of Horn Clauses and in RuleML/POSL, mandates two rules for B757 and Super classes, one for each ICAO aircraft code designation (B752, B753 for Boeing 757, A225 for Antonov An-225). Executing the query faaCategory(?x), answers the class of the aircraft. Similar rules exist for the preceding aircraft, defining the atom \(faaCategoryPreceding(x_{class})\).

The separation standards at the runway threshold for flights under IFR are defined by the Table 20.2.

The derived Horn Clauses for e.g. the categories heavy, B757, are as follows:

$$\begin{aligned} faaSeparation(5) \leftarrow faaCategory(B757) \wedge faaCategoryPreceeding(heavy) \end{aligned}$$
(20.28)
$$\begin{aligned} faaSeparation(4) \leftarrow faaCategory(heavy) \wedge faaCategoryPreceeding(B757) \end{aligned}$$
(20.29)
$$\begin{aligned} faaSeparation(4) \leftarrow faaCategory(heavy) \wedge faaCategoryPreceeding(heavy) \end{aligned}$$
(20.30)
$$\begin{aligned} faaSeparation(4) \leftarrow faaCategory(B757) \wedge faaCategoryPreceeding(B757) \end{aligned}$$
(20.31)
Table 20.2 FAA wake separation standards (nautical miles, at the threshold) [8]
Full size table

4.4 RECAT Regulations

For the purposes of wake turbulence separation minima, aircraft are categorized as Category A through Category F. Each aircraft is assigned a category based on wingspan, and maximum takeoff weight (MTOW) [8, 11]:

 

Category A.:

Aircraft capable of MTOW of 300,000 pounds or more and wingspan greater than 245 feet.

Category B.:

Aircraft capable of MTOW of 300,000 pounds or more and wingspan greater than 175 feet and less than or equal to 245 feet.

Category C.:

Aircraft capable of MTOW of 300,000 pounds or more and wingspan greater than 125 feet and less than or equal to 175 feet.

Category D.:

Aircraft capable of MTOW of less than 300,000 pounds and wingspan greater than 125 feet and less than or equal to 175 feet; or aircraft with wingspan greater than 90 feet and less than or equal to 125 feet.

Category E.:

Aircraft capable of MTOW greater than 41,000 pounds with wingspan greater than 65 feet and less than or equal to 90 feet.

Category F.:

Aircraft capable of MTOW of less than 41,000 pounds and wingspan less than or equal to 125 feet, or aircraft capable of MTOW less than 15,500 pounds regardless of wingspan, or a powered sailplane.

  The derived definite clauses in implication form, after conversion of pounds to kilograms are as follows:

$$\begin{aligned} recat(A)\leftarrow mtom(x_{kg})\wedge (x_{kg} \ge 136000)\wedge wingspan(x_{ft})\wedge (x_{ft} > 245) \end{aligned}$$
(20.32)
$$\begin{aligned} recat(B) \leftarrow mtom(x_{kg}) \wedge (x_{kg} \ge 136000)&\wedge&\\ wingspan(x_{ft})&\wedge&(x_{ft} \le 245) \wedge (x_{ft}>175) \nonumber \quad \quad \end{aligned}$$
(20.33)
$$\begin{aligned} recat(C) \leftarrow mtom(x_{kg}) \wedge (x_{kg} \ge 136000)&\wedge&\\ wingspan(x_{ft})&\wedge&(x_{ft} \le 175) \wedge (x_{ft}>125) \nonumber \end{aligned}$$
(20.34)
$$\begin{aligned} recat(D) \leftarrow (wingspan(x_{ft}) \wedge (x_{ft} \le 125) \wedge (x_{ft}>90))&\vee&\\ (mtom(x_{kg})\wedge (x_{kg}<136000)&\wedge&\nonumber \\ wingspan(x_{ft}) \wedge (x_{ft} \le 175)&\wedge&(x_{ft}>125)) \nonumber \end{aligned}$$
(20.35)
$$\begin{aligned} recat(E) \leftarrow mtom(x_{kg}) \wedge (x_{kg}> 18000)&\wedge&\\ wingspan(x_{ft})&\wedge&(x_{ft} \le 90)\wedge (x_{ft}>65) \nonumber \end{aligned}$$
(20.36)
$$\begin{aligned} recat(F) \leftarrow (mtom(x_{kg}) \wedge (x_{kg}<7000))&\vee&\\ (mtom(x_{kg}) \wedge (x_{kg} \le 18000)&\wedge&wingspan(x_{ft})\wedge (x_{ft} \le 125)) \nonumber \end{aligned}$$
(20.37)

The lack of disjunction in the body of Horn Clauses and in RuleML/POSL, mandates two rules for categories D and F. Executing the query recatCategory(?x) answers about aircraft’s category. Similar rules exist for the preceding aircraft, defining the atom \(recatPreceding(x_{class})\).

RECAT separation standards for IFR flights are presented in Table 20.3. For instance, the separation values for the pair B, C are captured from the following Horn Clauses:

$$\begin{aligned} recatSeparation(mrs) \leftarrow recat(B) \wedge recatPreceding(C)\end{aligned}$$
(20.38)
$$\begin{aligned} recatSeparation(4) \leftarrow recat(C) \wedge recatPreceding(B) \end{aligned}$$
(20.39)
Table 20.3 RECAT wake separation standards (nautical miles) [8, 11]
Full size table

4.5 Airport Layout

ICAO and FAA rules are covering cases such as intersecting runway/intersecting flight path separation, intersection departures, parallel approaches, etc. Furthermore, different separation standards may exist when aircraft operate in different runways separated by at least 2500 ft or 760 m [10, 13]. Finally, the rule base must cover situations where a runway is closed for maintenance of for emergency reasons. In order to implement the above, it is necessary to define rules concerning the airport layout.

Reasoning on airport layout is realized by using information about airport characteristics described in Sect. 20.4.1, combined with additional rules. Currently, the rule base supports up to two runways, used both ways. In accordance with ICAO and FAA regulations, the basic layouts supported are: (i) single runway, (ii) two intersecting runways, (iii) two close parallel runways, less than 2500 feet (760 m for ICAO regulations) apart, (iv) parallel runways more than or equal to 2500 feet, and (v) non parallel and non intersecting runways, denoted as npni.

$$\begin{aligned} layout(closeparallel)\leftarrow & {} (R_1(x_1)\wedge R_2(x_2) \wedge (x_1=x_2)) \wedge R_d(x_3 < 2500) \nonumber \\ \end{aligned}$$
(20.40)
$$\begin{aligned} layout(farparallel)\leftarrow & {} (R_1(x_1)\wedge R_2(x_2) \wedge (x_1=x_2)) \wedge R_d(x_3 \ge 2500)\nonumber \\ \end{aligned}$$
(20.41)
$$\begin{aligned} layout(npni)\leftarrow & {} (R_1(x_1)\wedge R_2(x_2) \wedge (x_1 \ne x_2)) \wedge R_d(x_3 \ne 0)\nonumber \\ \end{aligned}$$
(20.42)

where \(R_{layout}\) is defined by layout, \(R_1\) is the heading of the first runway, defined as runwayOneOr, \(R_2\) is the heading of the second runway, defined as runwayTwoOr and \(R_d\) is the distance between runways, defined by the atom distanceBtwnRunw. Equality predicate is built-in of OO jDREW. The query layout(?x) is shown in Fig. 20.2.

Fig. 20.2
figure 2

Executing the query about airport layout, for the Thessaloniki Airport “Macedonia”

Full size image

4.6 Angles and Heading

Solving complex cases, as mentioned in Sect. 20.4.5, require reasoning over heading and turns, as well as weather information. Representing spatial information for the purpose of an ATC rule base mandates the use of quantitative terms for angle and heading, since qualitative spatial terms cannot be used for precise arithmetic calculations. Previous work (e.g. [1]), can be useful only in cases of fuzzy terms, as wind heading variations as expressed by METAR information.

During landing phase, aircraft’s heading is derived from the orientation of the runway on which the aircraft operates (denoted by the atom \(onRunway(x_2)\)). Four rules are needed to match runway name with the corresponding heading.

$$\begin{aligned} heading(x_{deg}) \leftarrow runwayOneOr(x_{deg})&\wedge&\\ runwayOneName(x_1)&\wedge&onRunway(x_2) \wedge (x_1=x_2) \nonumber \end{aligned}$$
(20.43)

Heading and angle changes require two Horn Clauses for each computation, due to the possible, greater than \(360^{\circ }\) result. Angle subtraction also requires additional rules, covering cases from \(0^{\circ }\) to \(180^{\circ }\) and from \(180^{\circ }\) to \(360^{\circ }\). Negative values have been taken in to consideration, using the built-in function \(abs(x_{abs},x_1)\), where, given that the first argument is a variable then it will be bound to the absolute value of the second argument.

4.7 Future Regulations

The final form of the pair-wise separation matrix of RECAT-2 is not yet known; therefore it was not possible to include those regulations in the rule base. However, a \(120 \times 120\) matrix was implemented for testing purposes. The computational time was sufficient for use in real-time environments, or at large simulations (\({\sim }5\) ms per query on a laptop with AMD A6-6310 APU, 8GB RAM).

Other planned regulation changes as WDS or TBS can be handled by the rule base and the database, according to known information. One advantage of the current rule base is the inclusion of approach speed for each type of aircraft which makes the precise computation of the time-based separation needed possible, in contrast with [12, 17, 21].

5 Conclusions and Future Work

A rule base for ATC regulations has been developed for the vicinity of the airport. This rule base, equipped with a large database consisting of characteristics of aircraft and airports, can compute the separation minima during landing phases, as mandated from current and future ATC regulations concerning operations under IFR.

The rule base is derived from interpretation of ATC regulations as Horn Clauses, which allows validation and verification of formal properties. The reasoner used, OO jDREW, provides adequate built-in predicates and functions for the implementation of the subset of ATC regulations studied.

This approach is suitable for building a database of aircraft and airports, containing their characteristics. Furthermore, it is possible to develop rules for categorization of aircraft using only characteristics which are present in the database, according to current ICAO, FAA and RECAT regulations, and subsequently, the implementation of separation tables defined by the above.

Other aspects of regulations and existing models were investigated, leading to the preliminary implementation of a mathematical background capable of handling angles and angle comparison, headings of aircraft, turns, airspeed, airport layout and future regulations.

In the future, we plan to extend the rule base to include a more complete set of regulations, such as cases of separation minima reduction, incident management, and transition zones. Further extensions may include lateral and vertical separation, and 4-D rules, which, given the position, heading, airspeed and time, will generate advisories to avoid possible conflicts. Finally, a collision avoidance method, external or embedded in the rule base, will be necessary to utilize the rule base in Free Flight concepts.