Decision making in railway interlocking systems based on calculating the remainder of dividing a polynomial by a set of polynomials

1.   Introduction

Rail transportation is an important mode of transportation around the world. It is a reliable and efficient way to transport goods and people over long distances. According to a literature review on resilience in railway transport systems, rail transportation is a critical infrastructure that plays a vital role in the economy and society^[1,2].

Railway interlocking is a safety-critical system that ensures trains do not collide on the tracks. It is a complex problem that has been studied extensively in the literature. One source that provides an overview of railway signalling principles is Pachl ^[3]. Recent research has explored the use of artificial intelligence to detect faults in railway signal interlocking systems ^[4]. Other researchers have compared different methods for verifying the safety of railway interlockings ^[5]. There has also been work on developing formal model-based methodologies to support railway engineers in specifying and verifying interlocking systems ^[6]. Overall, the railway interlocking problem is an important and active area of research with many different approaches being explored.

Ensuring the compatibility of switch positions and signal indications at a railway station is crucial for safety. Interlocking is a safety measure that prevents improper changes to traffic signals and turnout switches. A railway station consists of sections connected by traffic signals and turnouts, which define the possible movement of trains. A route is a sequence of connected sections that a train can travel along partitioned into several blocks. To prevent collisions and dangerous situations, two trains may never be in the same block of a route. Two intersection routes (or the relevant blocks thereof) must be allocated to trains at the same time, to prevent collisions. Once a route is set and a train receives the signal to proceed, all switches and signals along the route are locked until the train has passed through.

A possible classification of computer-based railway interlocking systems could be as follows:

● Route-table based: For every route request, an algorithm checks its feasibility using a "control table". The software consists of a single algorithm, independent of the topology.

● Geographical: The interlocking program is made up of instances of software objects that mimic the behavior of physical objects. The configuration of this program depends on the topology. Within this category, we can distinguish between:

– Route-based: Routes are defined a priori, and their definitions constitute data shared by the instantiated objects.

– On-demand route definition: There is no a priori definition of routes. Instead, a train's request to the interlocking system is given only as the final destination that the train must reach. Instantiated software objects are responsible for exploring possible routes to the destination and choosing one of them. Our approach lies in this category.

Classical railway interlocking systems are route-based and the compatibility of routes is decided (usually by human experts) in advance ^[7] (although unacceptable errors have been found in real railway interlocking systems ^[8]).

Some modern railway interlocking systems can make decisions on the fly. This makes them more flexible as routes are not predetermined. However, before authorizing any changes to signals or switch positions, it is necessary to check if two trains would travel on intersecting routes (including the same route) and potentially collide. If this is the case, changes are not made and it may be necessary to wait for a train to leave the station.

The first railway interlocking systems were developed in the nineteenth century (they were complex mechanical devices with levers and interacting bars). Typical railway interlocking systems of the mid twentieth century were based on the use of electric relays and needed complicated electric circuits translating the connectivity of the railway station. In the 1980's, the first computer-controlled railway interlocking systems are installed ^[9,10,11,12]. The first geographical railway interlocking system installed in Spain is dated on 1993 ^[13].

All modern railway interlocking systems are computer based (either geographical or route-based). Naive implementations of geographical algorithms may run into exponential complexity problems concerning the running time needed for finding safe routes through the railway network. Efficient data validation for geographical interlocking systems has also been studied ^[14]. Another approach to verifying geographically distributed interlocking systems is through model checking using UMC ^[15]. The approach presented here describes the configuration of the railway station through a single algebraic structure in which safety can be checked by a single algebraic operation. The main goal of our work is mainly theoretical. Nevertheless, it has the limitation that it cannot be certified and applied in practice. However we think that our approach can also be used for simulations that do not require certification credit and it is interesting from a theoretical point of view. Indeed, our approach represents a step on our research on proposing algorithms to solve railway interlocking problems for any railway station using an algebraic model similar to those used in Artificial Intelligence for implementing expert systems based on polynomials, ideals, and Groebner basis ^[16]. Our proposal offers significant advantages over previous approaches. The motivation for our work is as follows:

● Our approach relates two seemingly different fields: computational algebra and interlocking problems. Indeed the model we propose here proves that an interlocking problem can be solved by applying a division algorithm. This relation is not only interesting and inspiring from a theoretical point of view, but also has certain practical benefits: a possible proposal for improvement in the division algorithm in the field of computational algebra directly results in faster performance in solving interlocking problems.

● By expressing the interlocking problem as an algebraic system similar to those used in expert systems, we can address problems related to expert systems in railway stations. We believe that once the problem is described in algebraic terms, it will be possible to develop expert systems based on these algebraic systems to solve more complex problems in the future. For example, such systems could detect which signals and switches cannot change the state due to safety concerns and provide recommendations for changing the configuration of switches and signals to allow trains to move safely to specific locations.

● Unlike our previously proposed models that used algebraic systems ^[17,18,19], the model we propose now has great advantages over the others:

– It eliminates the need for calculating Groebner bases, a task that is known to be very slow due to its exponential complexity. Indeed, in contrast to our previous approaches, the present model guarantees a linear complexity.

– As a result, our new model is much faster than our previous models and has been shown to have linear complexity.

– In contrast to our previous approaches, we use different polynomials to represent the static and dynamic topology of the railway station. The static topology is represented by a set of polynomials while the dynamic topology is represented by a monomial. Another monomial is used to represent the position of trains. This allows for immediate updates to the polynomials representing the problem when there are changes in train positions or the configuration of the railway station.

The paper is structured as follows. In Section 2 we discuss other approaches related to the one proposed here. In Section 3 we propose a possible formalisation of the concepts related to a railway interlocking system. In Section 4 we describe our method (as a black box) for determining the safety of a proposed situation in a railway interlocking system. In Section 5 the worst case complexity of the new model in calculated. In Section 6 the extension of the model to trains occupying more than one section of the layout is detailed. In Section 7 we show that the new model is much faster than previous ones. Finally, in Section 8 we set our conclusions.

2.   Related works

An overview of different existing approaches to decision making in a railway interlocking system is given afterwards.

The paths (lists of consecutive sections) along the railway station are called routes. An example can be a route from an entrance of a station to a given track beside a certain platform. Establishing a route requires setting the turnouts and colour light signals along the route appropriately.

Many approaches have been applied to decision making in a railway interlocking system. Although out of date, ^[20] includes an interesting annotated bibliography.

In the classic approaches, the routes of the railway interlocking system are predefined. Moreover, the compatibility of routes is determined in advance (traditionally by human experts). They are usually denoted tabular railway interlocking systems.

The railway interlocking system is usually denoted geographical if the problem is translated into computational notation and decisions are made on the fly.

Geographical approaches do not depend on the track layout of the railway station. An inference engine extracts knowledge in a rule-based expert system and is independent of the given rules and facts stated as true. Similarly, a geographical railway interlocking system can decide upon the safety of any proposed situation in any given railway station.

The ^[21] uses a theorem prover implemented in a higher-order logic to decide on the safety of a situation. This work is revisited using an annotated logic program with temporal reasoning in ^[22].

Meanwhile, ^[7] uses ordered binary decision diagrams to model railway interlocking systems.

A specific work for the Slovak National Railways is ^[23], that uses Z notation.

Another specific work, in this case for the Danish State Railways is ^[24], that uses the Vienna Development Method (VDM).

The ^[25] presents an early but sophisticated formal model that can deal with complex topologies including reversing loops and reversing triangles. It uses Petri nets and graphs and is implemented in Objective-C and PROLOG.

Another model (component-based) is used in the interesting approach ^[26,27,28]. The railway station is abstracted as a set of connected components.

Another example is ^[29], where CAD, RailML, and logic programming are used. It is applied to a Norwegian railways station.

A very interesting approach that also uses RailML to describe the topology of the railway station and UML class diagrams and is applied to a Dutch station is ^[30].

We will describe afterwards some models for decision making in railway interlocking systems designed and implemented by the authors. All these models are topologically-independent and do not have restrictions on the direction of the trains.

● Model based on the use of graphs ^[31]: Our approach is based on graph theory and Boolean matrices (adjacency matrices). This approach is slow and can only be applied to small railways stations because, although the matrices are sparse, their number of rows and columns is the number of sections of the network.

● Algebraic model ^[17,32]: Here, our approach is based on algebraic terms which requires calculating a Groebner basis ^[33,34] of a polynomial ideal. Since the algorithm for calculating this Groebner basis involves a long time, this approach is not suitable for large stations.

● Model based on Boolean propositional logic ^[35]: This approach is based on propositional logic: sections are represented by Boolean propositional variables and connectivity between sections are represented by a Boolean propositional formula. The safety of a railway station is detected by solving a SAT problem for each section in the railway station. All techniques, like DPLL ^[36], to solve a SAT problem involve exponential complexity. However, the high number of SAT problems required in this approach makes it impossible for large stations.

● Logic-algebraic model ^[18]: The advantage with respect to the algebraic model mentioned above is that in this case, the polynomial ring where computations take place is Boolean and consequently, Groebner bases and normal forms calculations required are much faster. In fact, this model is much faster than the three previous ones. However, the algorithm for calculating a Groebner basis involves high complexity computations and therefore, this approach is not suitable for large stations.

● ASP model ^[37]: This approach is based on the answer set programming (ASP) paradigm. Connectivity and safety relations are defined by relations and derived relations through logic programming. This approach is further more efficient than previous ones and may be suitable for larger railway stations. However, this is not a polynomial complexity approach and consequently, it is not scalable.

● Model based on preprocess and Boolean Polynomials: An algebraic approach that represents the proposed configuration of the railway station and the position of the trains using Boolean polynomials and Groebner bases is detailed in ^[19]. The set of polynomials for which the Groebner basis is computed does not depend on the position of the trains. A new Groebner basis has to be computed if any changes in the aspect of the colour light signals or the position switches take place. Although faster than previous approaches, it can still be slow if the railway station is really large.

As may be seen, many of these approaches are based on translating the topology of the railway station into polynomials with several variables and require calculating Groebner bases since they are usually required to solve many algebraic problems involving polynomials with several variables. Unfortunately, calculating a Groebner basis requires a very long time, and consequently, all these approaches are not suitable for very large railway stations with many trains since they need a long time to make a decision upon the safety of the proposed situation.

In this paper, we propose a completely new algebraic approach that does not require computing Groebner bases and is much faster than our previous ones. In our approach, the computational complexity of deciding upon the safety of a proposed situation is linear with respect to the number of sections and trains in the railway station (see Section 5). Therefore, it is completely suitable for very large railway stations (even if there are many trains involved).

3.   A formalisation of the safety of a proposed situation in a railway station

In this section we will define some formal concepts that allow us to prove the validity of our approach.

A railway station is a set of sections $\{S_1\ldots S_N\}$ and a binary relation defining the connection between sections by means of colour light signals and turnouts. There may be trains placed in the sections of a railway station. In this paper, we will initially consider that each train is placed in just one section. Nevertheless, we will generalize our results for the general case that a train can be placed in different sections in Section 6.

A colour light signal is defined as $(S_i, S_j)$, a pair of connected sections. If the indication of the colour light signal is proceed, then a train may pass from section $S_i$ to section $S_j$. If the indication of the colour light signal is stop, then trains are not allowed to pass from section $S_i$ to section $S_j$.

A turnout is defined as $(S_i, S_j, S_k)$, an array of three connected sections. If the switch of the turnout is in the direct track position, then a train may pass from section $S_i$ to section $S_j$ (and conversely). If the switch of the turnout is in the diverted track position, then a train may pass from section $S_i$ to $S_k$ (and conversely).

The potential connectivity of a railway station derives from the situation of the colour light signals and the situation of the turnouts (that is, from the so called topology of the station). We define the relation $E$ for describing the potential connectivity between sections. Formally, $E$ is a set of pair of sections $(i, j)$ indicating that the section $S_i$ is connected to section $S_j$ (by means of a colour light signal and/or a turnout).

Definition 3.1. We define the set $E\subset \mathbb{Z}\times\mathbb{Z}$ as:

Consequently, the relation $E$ is symmetric.

Remark 3.1. In the case that there are a series of n turnouts, we assume the presence of intermediate sections between them. Consequently, in a railway station, each section is connected to a maximum of three other sections on each extreme through a turnout. This means that each section can be connected to a maximum of six other sections. Therefore, the size of $E$ is less than or equal to $6\cdot N$ where $N$ is the number of sections. As a result, the number of elements in $E$, is $O(N)$.

The indications of the colour light signals and the position of the switches of the turnouts (that is, the configuration of the railway station) define if a section is reachable from another. A configuration of the railway station is defined by a subset $P\subseteq E$. $(S_i, S_j) \in P$ if and only if it is possible to pass from the section $S_i$ to the section $S_j$ according to the indications of the colour light signals and the position of the switches of the turnouts (obviously a necessary condition is that section $S_i$ is connected to section $S_j$).

Remark 3.2. In this model of railway interlocking systems we assume that if the switch of the turnout $(S_i, S_j, S_k)$ is in the direct track position, a train is not allowed to pass from $S_k$ to $S_i$. Similarly, if the switch of the turnout $(S_i, S_j, S_k)$ is in the diverted track position, a train should not try to pass from $S_j$ to $S_i$. We will consider that turnouts are always properly protected by colour light signals.

Remark 3.3. Two sections are connected by means of either a colour light signal or a turnout, but not both. If the latter was the case, we introduce a section in between (like $S_9$ between $S_{10}$ and $(S_2, S_3, S_9)$ in Figure 3.2). Similarly, we include sections between two semaphores or turnouts.

Remark 3.4. Note that, despite the fact that turnouts can be long apparatuses, they are not considered sections in this model, but connections between sections.

The set $P$ determines the possible paths of the railway station. A path is a list of sections $[u_1\ldots u_n]$ such that for every $i$ $(u_i, u_{i+1})\in P$. The set $P$ fulfills the following important property: For every pair of sections $i$ and $j$, there is at most one path in $P$ from section $i$ to section $j$.

Remark 3.5. For the property in the previous paragraph to hold we are considering paths defined by $P$ (not by $E$). Besides, we are considering in this model only "usual" railway terminus stations or railway overtaking stations (unlike toy trains where one side of the overtaking station is connected to the other side). In these "usual" stations, we have that for every pair of sections $i$ and $j$, there is at most one path in $P$ from section $i$ to section $j$.

Example 3.1. Let us consider the railway station of Figure 3.1.

As may be seen, the railway station is divided into sections $S_1\ldots S_{11}$ and there are seven colour light signals (for example, there is a colour light signal between sections $S_1$ and $S_2$) and two turnouts (for example, a turnout connecting sections $S_2$, $S_3$ and $S_9$). Note that signalling is on the right hand side of the track.

According to Definition 3.1, the set $E$ is:

Note that the set $E$ is defined independently from the specific configuration of the elements of the railway station (from the indications of the colour light signals and the positions of the switches of the turnouts).

Let us consider the configuration depicted in Figure 3.2. The position of the switches of the turnouts is represented by:

● a small segment, if the switch is in the direct track position (see for instance the turnout between sections $S_2$ and $S_3, S_9$ in Figure 3.2), or

● a small angle, if the switch is in the diverted track position (see for instance the turnout between sections $S_6$ and $S_5, S_{11}$ in Figure 3.2).

In view that the figures are printed in black and white, the aspect of the colour light signals will be represented by a black circle (indication stop) or white circle (indication proceed).

Now, we will determine the subset $P\subseteq E$ given by the indications of the colour light signals and the position of the switches of the turnouts in Figure 3.2:

As may be seen, $(10, 9)\not \in P$ because the indication of the colour light signal connecting sections $S_{10}$ and $S_9$ is stop. In the same way, $(2, 9)\not \in P$ because the switch of the turnout $(S_2, S_3, S_9)$ is in direct track position.

We would like to emphasize here that remark 3.5 holds in Figure 3.2. Although it is apparent that there are sections connected by more than one path, there are no loops once $P$ is defined. That is to say, for every sections $i$ and $j$ there is at most one path in $P$ from $i$ to $j$.

Let us formally define the set $P$.

Definition 3.2. We define the subset $P\subseteq E$ as the set of $(i, j)\in E$ such that exactly one of these conditions holds (with the conditions imposed in this model the conditions are mutually exclusive):

● It is always possible to pass from section $S_i$ to section $S_j$ (regardless of the configuration of the railway station).

For example, $(2, 1)\in P$ in the configuration of Figure 3.2 since it is always possible to pass from section $S_2$ to section $S_1$.

● There is a colour light signal $(S_i, S_j)$ and its indication is proceed.

For example, $(1, 2)\in P$ in the configuration of Figure 3.2 since the indication of the colour light signal $(S_1, S_2)$ (controlling the pass from section $S_1$ to section $S_2$) is proceed.

● There is a turnout $(S_i, S_j, S_k)$ or a turnout $(S_j, S_i, S_k)$ and its switch is in the direct track position.

For example, $(2, 3)\in P$ and $(3, 2)\in P$ in the configuration of Figure 3.2 since the switch of the turnout $(S_2, S_3, S_9)$ is in the direct track position.

● There is a turnout $(S_i, S_k, S_j)$ or a turnout $(S_j, S_k, S_i)$ and its switch is in the diverted track position.

For example, $(6, 11)\in P$ and $(11, 6)\in P$ in the configuration of Figure 3.2 since the switch of the turnout $(S_6, S_5, S_{11})$ is in the diverted track position.

Definition 3.3. We define the multiset $Q$ as the set of sections in which a train is placed: the number of times that element $i$ appears in $Q$ represents the number of trains located in section $S_i$.

We will consider that $Q$ is a multiset instead of a set, since $Q$ will have repeated elements in case that two different trains are placed in the same section (which is dangerous).

Definition 3.4. Let us consider a railway station and let the relation $E$ describe its potential connectivity (see Definition 3.1). A railway interlocking problem is an ordered pair $(P, Q)$, where $P$ is the set of Definition 3.2, describing a certain configuration of the elements of the railway station (indications of the colour light signals and positions of the switches of the turnouts) and $Q$ is the multiset of Definition 3.3, describing the positions of the trains.

Definition 3.5. We will say that the railway interlocking problem $(P, Q)$ is in a dangerous situation if and only if there are two lists of integers $[u_1, \ldots u_n]$ and $[v_1, \ldots v_m]$ such that all the following conditions hold:

(1) For all $0 < i < n$, we have that $(u_i, u_{i+1})\in P$. That is to say, consecutive sections in the list $[u_1, \ldots u_n]$ must be connected.

(2) For all $0 < j < m$, we have that $(v_j, v_{j+1})\in P$. That is to say, consecutive sections in the list $[v_1, \ldots v_m]$ must be connected.

(3) $\{u_1, v_1\}\subseteq Q$. That is to say, there must be a train in $u_1$ and $v_1$.

(4) $u_n = v_m$. That is to say, both paths reach the same section (there is a possible collision).

(5) For all $1 < i < n$ $u_i\not \in Q$ and for all $1 < j < m$ $v_j\not \in Q$. That is to say, intermediate sections in the list must be free of trains so that trains from from section $u_1$ and section $v_1$ may reach section $u_n = v_m$.

(6) For all $1 < i < n$ and for all $1 < j < m$ we have $u_i\neq v_j$. That is to say, the possible collision happens at the end of the paths.

(7) For all $i\neq j$ we have $u_i\neq u_j$. That is to say, the path $[u_1, \ldots u_n]$ does not contain cycles.

(8) For all $i\neq j$ we have $v_i\neq v_j$. That is to say, the path $[v_1, \ldots v_m]$ does not contain cycles.

We will say that the railway interlocking problem $(P, Q)$ is in a safe situation if and only if $(P, Q)$ is not in a dangerous situation.

Example 3.2. Let us recall the railway station of Figure 3.1 and its possible configuration shown in Figure 3.2. Figure 3.3 depicts the placement of one train in section $S_1$ and another train in section $S_{10}$. Therefore, in this case: $Q = \{1, 10\}$

Clearly, this situation is safe:

● the train located in section $S_1$ could stay in section $S_1$ or move to sections $S_1, S_2, S_3, S_4$,

● the train located in section $S_{10}$ could stay in section $S_{10}$ or move to sections $S_{11}, S_6, S_7, S_8$.

Example 3.3. However, if a new train were allocated in section $S_8$, that is to say $Q = \{1, 8, 10\}$ (Figure 3.4), the situation would turn into a dangerous one: the trains situated in sections $S_{10}$ and $S_8$ could collide in sections $S_7$ and $S_8$. Following the formalization of Definition 3.5:

● lists ^[10,11,6,7] and ^[8,7] fulfil the conditions Definition 3.5 (representing a possible collision in section $S_7$),

● lists ^{[10,11,6,7,8]} and ^[8] fulfil the conditions Definition 3.5 (representing a possible collision in section $S_8$).

Example 3.4. In case the aspect of the colour light signal between section $S_{10}$ and section $S_{11}$ were changed, now indicating stop, the situation would be safe again (Figure 3.5).

4.   Overview of the new approach

In this section we will extensively describe our algebraic approach based on the use of polynomials. As we will see, the potential connectivity of a railway station is represented by a set of polynomials with coefficients in the field $\mathbb{Z}_2$. A specific configuration of the railway station is represented by a polynomial with coefficients in the same field. The same happens with a specific placement of trains in the railway station. In order to detect whether a proposed situation is dangerous or not, we only need to check if the remainder of dividing a polynomial by a set of polynomials is zero or not.

4.1.   The algebraic model

Our approach is based on defining a set of polynomials in the variables $t_i, l_{ij}$ and $m_{ij}$, where:

● $t_i$: a variable $t_i$ is considered for each section $S_i$ in the railway station.

● $l_{ij}, m_{ij}$: two variables, $l_{ij}$ and $m_{ij}$, are considered for each pair of sections $S_i$ and $S_j$ when $(i, j)\in E$. That is to say, we consider the variables $l_{ij}$ and $m_{ij}$ if the topology of the station allows to pass from section $S_i$ to section $S_j$ (in some configuration of the railway station).

We will work hereinafter in the polynomial ring

and we will use the lexicographical order given by $l_{ij} > m_{ij} > t_i$. The set of polynomials representing the potential connectivity of the railway station, the polynomial describing the specific configuration of the railway station and the polynomial describing the specific placement of trains in the railway station are constructed as follows.

The list of polynomials $\mathcal{E}$ representing the railway station. Through the set $E$ (see Definition 3.1, the set of ordered pairs of integer numbers describing the potential connectivity of a railway station, we will define $\mathcal{E}$ as the list of polynomials of $\mathcal{A}$ formed by:

● $\forall(i, j)\in E$, the two polynomials:

● For each variable $t_i$:

As may be seen, the list of polynomials $\mathcal{E}$ depends only on $E$ and, therefore, it is defined independently from the specific configuration of the elements of the railway station (from indications of the colour light signals and the position of the switches of the turnouts).

The polynomial $p$ representing a given configuration of the railway station. For each set of ordered pairs of integers $P\subseteq E$ representing a given configuration of the railway station (see Definition 3.2), we will consider the monomial $p \in \mathcal{A}$:

As may be seen, this monomial is defined according to the configuration of the railway station in the following way (note that the symbol $|$ represents the relation is a divisor of or divides, for example, $xz|xyz$ because $xz$ divides $xyz$):

● If it is always possible to pass from section $S_i$ to section $S_j$ (regardless of the configuration of the railway station), then $l_{ij} | p$.

● If there is a colour light signal between section $S_i$ and section $S_j$, then:

– if the indication of the colour light signal is proceed, then $l_{ij} | p$.

– if the indication of the colour light signal is stop, then $m_{ij} | p$.

● If there is a turnout connecting section $S_i$ to either section $S_j$ or section $S_k$ then:

– if the switch is in the straight track position, then $l_{ij}l_{ji}m_{ik}m_{ki} | p$.

– if the switch is in the diverted track position, then $l_{ik}l_{ki}m_{ij}m_{ji} | p$.

As may be seen, a variable $l_{ij}$ in $p$ represents that it is possible to pass from section $S_i$ to section $S_j$. In the same way, a variable $m_{ij}$ in $p$ represents that it is not possible to pass from section $S_i$ to section $S_j$

The polynomial $q$ representing the placement of the trains. Let us consider that there are trains placed in sections $S_{i_1}, \ldots, S_{i_m}$. We define the monomial $q \in \mathcal{A}$:

As may be seen, a variable $t_i$ in $q$ represents that there is a train in section $S_i$.

4.2.   Decision making in the algebraic model

Here we will summarize the steps required to solve a railway interlocking problem.

Step 1. Given a railway station by the set describing its potential connectivity, $E$, we obtain the list $\mathcal{E}$.

We would like to emphasize that this list $\mathcal{E}$ is calculated only once for every railway interlocking problem associated to $E$. We do not need to recalculate this set if there are movements of trains or if there are changes in the configuration of the railway station. Besides, this set only contains $2K+N$ polynomials (where $K$ is the size of $E$ and $N$ is the number of sections).

Step 2. Given a configuration of the railway station, $P$, we calculate the monomial $p$.

As may be seen, for every change of the configuration in the railway station, we need to calculate $p$, but this monomial contains $K$ variables where $K$ is $O(N)$.

Step 3. Given a placement of the trains, $Q$, we need to calculate the monomial $q$.

As may be seen, for every change of the placement of the trains, we need to calculate $q$, but this monomial contains at most $N$ variables.

Step 4. In order to solve the $(P, Q)$ railway interlocking problem we need to compute:

where ${\rm{NR}}$ represents the remainder of the monomial $pq$ respect to the list $\mathcal{E}$. If this value is 0, the railway interlocking problem is in a dangerous situation, otherwise it is in a safe situation (see Theorem A.11). This may be calculated with any Computer Algebra System (CAS). In this paper we will use the CAS CoCoA 5.2 ^[38,39].

As we will see in Section 7, all these steps can be completed in less than 1 s for very large railway stations using a conventional computer.

4.3.   Examples of application of the algebraic method proposed

We will use the CAS CoCoA in order to show how to solve some railway interlocking problems for the railway station of Example 3.1 (depicted in Figure 3.1) using the algebraic approach proposed in this paper.

Example 4.1. Let us recall the potential connectivity of the railway station of Example 3.1. Let us remember that in this case:

The process starts as follows:

Step 1. We define the polynomial ring and the list $\mathcal{E}$ corresponding to the topology of this railway station as described in Section 4.1. The variables of the polynomial ring are:

● variables: $t_1\ldots t_{11}$ (since this railway station contains 11 sections)

and

● variables: $l_{1, 2}, l_{2, 9}, l_{ 9, 10}, l_{10, 11}, l_{11, 6}, l_{2, 3}$,$l_{3, 4}, l_{4, 5}, l_{5, 6}, l_{6, 7}, l_{7, 8},$

$l_{2, 1}, l_{9, 2}, l_{10, 9}, l_{11, 10}, l_{6, 11}$,$l_{3, 2}, l_{4, 3}, l_{5, 4}, l_{6, 5}, l_{7, 6}, l_{8, 7},$

$m_{1, 2}, m_{2, 9}, m_{ 9, 10}, m_{10, 11}, m_{11, 6}$,$m_{2, 3}, m_{3, 4}, m_{4, 5}, m_{5, 6}, m_{6, 7}, m_{7, 8},$

$m_{2, 1}, m_{9, 2}, m_{10, 9}, m_{11, 10}$,$m_{6, 11}, m_{3, 2}, m_{4, 3}, m_{5, 4}, m_{6, 5}, m_{7, 6}, m_{8, 7}$

In CoCoA syntax:

The polynomials in the list $\mathcal{E}$ are defined as described in Section 4.2.

● $l_{1, 2}l_{2, 1}t_1+m_{1, 2}m_{2, 1}t_1t_2$ (because $(1, 2)\in E$),

● $l_{1, 2}m_{2, 1}t_1+m_{1, 2}m_{2, 1}t_1t_2$ (because $(1, 2)\in E$),

● $\ldots$

In CoCoA syntax:

Step 2. Let us now consider the configuration of Example 3.1 (Figure 3.2). In this configuration:

so we define the monomial $p$ as follows:

As may be seen, the variable $m_{29}$ appears in the monomial $p$ since it is not possible to pass from section $S_2$ to section $S_9$. Similarly, the variable $l_{12}$ appears in $p$ since it is possible to pass from section $S_1$ to section $S_2$.

In CoCoA syntax:

Example 4.2. Let us now consider the placement of trains of Example 3.2 (Figure 3.3): there are two trains located in sections $1$ and $10$, respectively.

Step 3. In this case: $Q = \{1, 10\}$. Therefore, we define the monomial

In CoCoA syntax:

Step 4. In order to solve the railway interlocking problem $(P, Q)$ we need to check whether ${\rm{NR}}(pq, \mathcal{E}) = 0$ or not. In CoCoA syntax:

As the output of CoCoA is "false", the proposed situation is safe.

Example 4.3. Let us now consider the placement of trains of Example 3.3 (Figure 3.4) instead: a new train is placed in section $S_8$. We only need to perform Steps 3 and 4.

Step 3. We need to recalculate the polynomial $q$. Now: $Q = \{1, 10, 8\}$, and, therefore, we define the monomial

In CoCoA syntax:

Step 4. Again, we need to check whether ${\rm{NR}}(pq, \mathcal{E}) = 0$ or not. In CoCoA syntax:

The output of CoCoA is "true" in this case. Consequently, the proposed situation is dangerous.

Example 4.4. If the aspect of the colour light signal between section $S_{10}$ and section $S_{11}$ were changed, now indicating stop (see Figure 3.5 in Example 3.4), we would only need to recompute Steps 2 and 4.

Step 2. We need to recalculate the polynomial $p$. Now we have:

and therefore:

($l_{10, 11}$ has been substituted by $m_{10, 11}$). In CoCoA syntax:

Step 4. We need to check if the situation is dangerous. In CoCoA syntax:

returns "false". Consequently, the proposed situation is safe.

4.4.   Intuition of our approach

In this section, we will provide the intuition behind the choice of polynomials and the reason why the division algorithm provides the solution for detecting whether an interlocking problem is in a dangerous situation or not.

As may be seen in the previous section, in order to detect if an interlocking problem $(P, Q)$ is in a dangerous situation we need to check if ${\rm{NR}}(pq, \mathcal{E}) = 0$. Although the definition ${\rm{NR}}$ is not simple and requires many technical details, we provide the intuition behind the value ${\rm{NR}}(pq, \mathcal{E})$: the remainder of the polynomial, $pq$ by a list of polynomials $\mathcal{E}$.

In the same way as ordinary division (for polynomials with one variable and natural numbers), the division of a polynomial $p$ (with several variables) by a list of polynomials $G = [f_1\ldots f_m]$ is $p = \alpha_1 f_1 + \ldots \alpha_m f_m + r$. The value ${\rm{NR}}(p, G)$ just denotes $r$, the remainder of the division.

The algorithm for calculating ${\rm{NR}}(p, G)$, in the same way as ordinary division, involves calculating intermediate dividends: it sets $r_0 = pq$ and for each step $i$, it choose a polynomial $f\in G$ and obtain a new intermediate dividend $r_{i+1}$, fulfilling

where $z_{i+1}$ is another polynomial. The new intermediate dividend $r_{i+1}$ is a polynomial 'simpler'^* than $r_i$. The last intermediate dividend $r_n$ is one such that it not possible to obtain a polynomial $r_{n+1}$ simpler than $r_n$. By definition, the value ${\rm{NR}}(pq, \mathcal{E})$ is the last intermediate dividend $r_n$. That is to say, ${\rm{NR}}(p, G) = r_n$. In Definition A.6 in Appendix A we give more details of this operator.

^* Obviously, in order to provide a formal definition, it is required to consider many mathematical issues: define when $r_{i+1}$ is simpler than $r_i$ (this is done by means of leading terms of the polynomial); analyze if the output takes into account the election of $f$ when several choices are possible. All these mathematical questions are deeply considered in ^[34]. We will briefly describe them in Section A.

In our approach, we calculate ${\rm{NR}}(pq, \mathcal{E})$ where $pq$ represents the interlocking problem $(P, Q)$. As we will see in Appendix A, each intermediate dividend $r_i$ is a polynomial with the form $p_iq_i$ such that $r_i$ represents an interlocking problem $(P_i, Q_i)$. This interlocking problem $(P_i, Q_i)$ is strongly related to $(P, Q)$. Indeed, $(P_i, Q_i)$ is in a dangerous situation if and only if $(P, Q)$ is in a dangerous situation. By means of this property, we can, consequently, detect if $(P, Q)$ is in a dangerous situation by checking if $(P_n, Q_n)$ (the interlocking problem associated to $r_n = {\rm{NR}}(pq, \mathcal{E})$) is in a dangerous situation. Besides, we will prove in Appendix A another important property: the interlocking problem $(P_n, Q_n)$ is in a dangerous situation if and only if $r_n = 0$. By means of these two properties we conclude that $(P, Q)$ is in a dangerous situation if and only if ${\rm{NR}}(pq, \mathcal{E}) = 0$. We will prove all these previous results in Appendix A.

We will illustrate all these ideas by means of an example. We will consider the intermediate dividends of ${\rm{NR}}(pq, \mathcal{E})$ for the interlocking problem in Figure 3.4 and the interlocking problems associated to them in Figure 4.1.

● The interlocking problem A in Figure 4.1 is the same as the interlocking problem in Figure 3.4. The monomial $p_A$ and $q_A$ are the following:

– $p_A = l_{1, 2}m_{2, 9}l_{9, 10}l_{10, 11}l_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}l_{6, 7}$l_7,8$l_{2, 1}m_{9, 2}m_{10, 9}l_{11, 10}l_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}l_{8, 7}$

– $q_A = t_1t_{10}t_8$

● In the interlocking problem A in Figure 4.1 there is a train located in section $s_{10}$ that can pass from $s_{10}$ to $s_{11}$. We can use the polynomial $g_{10, 11} = l_{10, 11}l_{11, 10}t_{10}+m_{10, 11}m_{11, 10}t_{10}t_{11} \in \mathcal{E}$ in the algorithm of division and we have that:

where:

– $z_1 = l_{1, 2}m_{2, 9}l_{9, 10}l_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}l_{6, 7} l_{7, 8}l_{2, 1}$m_9,2$m_{10, 9}l_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}l_{8, 7}t_1t_8$. The monomial $z_B$ is irrelevant for our purpose.

– $r_1 = p_Bq_B$ is the first intermediate dividend, where $p_B$ and $q_B$ are monomials describing the interlocking problem B in Figure 4.1:

* $p_B = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}l_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}l_{6, 7} l_{7, 8}l_{2, 1}$m_9,2$m_{10, 9}m_{11, 10}l_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}l_{8, 7}$

* $q_B = t_1t_{10}t_8t_{11}$

The interlocking problems A and B are closely related: A is in a dangerous situation if and only if B is in dangerous situation.

● In the interlocking problem B in Figure 4.1 there is a train located in section $s_8$ that can pass from $s_8$ to $s_7$. We can use the polynomial $g_{8, 7} = l_{8, 7}l_{7, 8}t_{8}+m_{8, 7}m_{7, 8}t_{8}t_{7} \in \mathcal{E}$ in the algorithm of division and we have that:

where:

– $z_2 = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}l_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}l_{6, 7} l_{2, 1}m_{9, 2}$m_10,9$m_{11, 10}l_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}t_1t_{10}t_{11}$. The monomial $z_C$ is irrelevant for our purpose.

– $r_2 = p_Cq_C$ is the second intermediate dividend, where $p_C$ and $q_C$ are monomials describing the interlocking problem C in Figure 4.1:

* $p_C = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}l_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}l_{6, 7} m_{7, 8}l_{2, 1}$m_9,2$m_{10, 9}m_{11, 10}l_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}m_{8, 7}$

* $q_C = t_1t_{10}t_8t_{11}t_7$

In the same way, the interlocking problems B and C are closely related: B is in a dangerous situation if and only if C is in dangerous situation.

● In the interlocking problem C in Figure 4.1 there is a train located in section $s_{11}$ that can pass from $s_{11}$ to $s_6$. We can use the polynomial $g_{11, 6} = l_{11, 6}l_{6, 11}t_{11}+m_{11, 6}m_{6, 11}t_{11}t_6 \in \mathcal{E}$ in the algorithm of division and we have that:

where:

– $z_3 = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}l_{6, 7} m_{7, 8}l_{2, 1}m_{9, 2}$m_10,9$m_{11, 10}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}m_{8, 7}t_1t_{10}t_1t_{10}t_8t_7$. The monomial $z_D$ is irrelevant for our purpose.

– $r_3 = p_Dq_D$ is the third intermediate dividend, where $p_D$ and $q_D$ are monomials describing the interlocking problem D in Figure 4.1:

* $p_D = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}m_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}l_{6, 7} m_{7, 8}l_{2, 1}$m_9,2$m_{10, 9}m_{11, 10}m_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}m_{8, 7}$

* $q_D = t_1t_{10}t_8t_{11}t_7t_6$

In the same way, the interlocking problems C and D are closely related: C is in a dangerous situation if and only if D is in dangerous situation.

● In the interlocking problem D in Figure 4.1 there is a train located in section $s_7$ that can pass from $s_7$ to $s_6$. We can use the polynomial $g'_{6, 7} = l_{6, 7}m_{7, 6}t_6+m_{6, 7}m_{7, 6}t_7t_6 \in \mathcal{E}$ in the algorithm of division and we have that:

where:

– $z_4 = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}m_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}m_{7, 8}l_{2, 1}m_{9, 2}$m_10,9$m_{11, 10}m_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{8, 7}t_1t_{10}t_8t_{11}t_7$. The monomial $z_E$ is irrelevant for our purpose.

– $r_4 = p_Eq_E$ is the fourth intermediate dividend, where $p_E$ and $q_E$ are monomials describing the interlocking problem E in Figure 4.1:

* $p_E = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}m_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}m_{6, 7} m_{7, 8}l_{2, 1}$m_9,2$m_{10, 9}m_{11, 10}m_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}m_{8, 7}$

* $q_E = t_1t_{10}t_8t_{11}t_7t_6^2$

● In the interlocking problem E in Figure 4.1 there are two trains located in section $s_6$ (we will say that it as a trivial interlocking problem), and, therefore, the interlocking problem E is in a dangerous situation. Consequently, our original interlocking problem A is also in a dangerous situation. We can use the polynomial $t_6^2 \in \mathcal{E}$ in the algorithm of division and we have that:

where

– $z_5 = l_{1, 2}m_{2, 9}l_{9, 10}m_{10, 11}m_{11, 6}l_{2, 3}l_{3, 4}m_{4, 5}m_{5, 6}m_{6, 7} m_{7, 8}l_{2, 1}$m_9,2$m_{10, 9}m_{11, 10}m_{6, 11}l_{3, 2}m_{4, 3}l_{5, 4}m_{6, 5}m_{7, 6}$m_8,7$t_1t_{10}t_8t_{11}t_7$. The monomial $z_E$ is irrelevant for our purpose.

– $r_5 = 0$.

We have that $r_5$ is the last intermediate dividend. Therefore, ${\rm{NR}}(p_Aq_A, \mathcal{E}) = r_5 = 0$.

5.   Worst case computational complexity

In this section we will discuss that the complexity of every step of our approach is linear. We will consider that $N$ is the number of sections in the railway station and $K$ is the size of the set $E$ (see Definition 3.1).

Step 1. Obtaining $\mathcal{E}$. The number of variables of the polynomial ring is $N+3K$. Since $K$ is $O(N)$, we have that the number of variables is $O(N)$. The number of polynomials in $\mathcal{E}'$ is $N+2K$. Since $K$ is $O(N)$ (see Remark 3.1), we have that the number of polynomials is $O(N)$. Each polynomials is the sum of two monomials at most. Consequently, the time complexity of this step is $O(N)$.

Step 2. Calculating the polynomial $p$. Since the number of variables in the polynomial ring is $O(N)$, we have that the time complexity of this step is $O(N)$.

Step 3. Calculating the polynomial $q$. Since the number of variables in the polynomial ring is $O(N)$, we have that the time complexity of this step is $O(N)$.

Step 4. Checking ${\rm{NR}}(pq, \mathcal{E}) = 0$. The complexity of generic algorithms for calculating the normal remainder of a polynomial $pq$ with respect to a list of polynomials like $\mathcal{E}$ strongly depends on the structure used for representing the polynomials and the kind of polynomials in the list ($\mathcal{E}$ in our case). The polynomials in $\mathcal{E}$ are just sum of two monomials with a constant number of variables and $pq$ is a monomial with a high number of variables. In Appendix B we describe an algorithm with complexity O($N$) for calculating this task when $pq$ and the polynomials in $E$ fulfill these characteristics.

6.   Model extension for trains occupying more than one section at the same time

Till now, we have analysed the case where trains are placed just in one section. Here we will see that the railway interlocking problems for trains placed in more than one section can be reduced to railway interlocking problems for trains placed in one section.

Let us consider a railway interlocking problem $(P, Q)$. Lets us suppose that a train is placed in sections $\{S_{v_1}, \ldots, S_{v_m}\}$, where $(v_i, v_{i+1})\in E$, $i\in\{1\ldots m-1\}$. Clearly, the proposed railway interlocking problem is equivalent to consider that the train is just in $S_{v_1}$ and that it is possible to pass from section $S_{v_i}$ to $S_{v_{i+1}}$ and from section $S_{v_{i+1}}$ to $S_{v_i}$ for every $i\in\{1\ldots m-1\}$. In other words, if there are colour light signals along the train occupying more than one section, it is considered that the indication of them all is proceed, whichever their real indications are. This can be achieved by considering the railway interlocking problem $(P', Q)$ where:

instead of $(P, Q)$.

Consequently, we can reduce the general case to the specific one in which every train is placed in just one section.

Example 6.1. We will illustrate this in the example of the railway station with the specific configuration depicted in Figure 3.2 (Example 3.1, Section 3). There we have:

In Figure 6.1, we have a situation in which some trains are placed in more than one section: there is a train placed in sections $[S_1, S_2]$ and there is a train placed in sections $[S_3, S_4, S_5]$.

The general railway interlocking problem of Figure 6.1 is equivalent to the railway interlocking problem $(P', Q')$ depicted in Figure 6.2, in which all trains are placed in just one section, and where:

7.   Experimental evaluation

In this section we analyse the performance of the approach presented in this paper, comparing it with other previous algebraic approaches. Indeed, we have made a comparison between the times required to decide upon the safety of a proposed situation in very large stations, with different numbers of sections ($N$) and trains ($M$). As may be seen, the new method proposed is always much more efficient than the other approaches proposed by the authors. This is possible because the present approach has worst case linear complexity (see Section 5).

In Table 1, we show the times required to decide upon the safety of different proposed situations (we have not included model in ^[31] because its performance is very poor bad for large stations). These times refer to the average performance of ten different configurations (both safe and unsafe) of a railway station with $N$ sections and $M$ trains involved.

Indeed, our new approach takes always less than 1 second to decide upon the safety of the proposed situation, even when the number of sections is huge, while the other approaches are much slower. In this case the first column corresponds to the track layout of a former Spanish railway station. The next columns correspond to concatenating that station with itself several times (we have observed that there are no significant changes in the performance of our approach if we add these stations in parallel by means of turnouts).

Time of our approach include the four steps in Section 4.2: it includes the calculation of the polynomials of the polynomials for the topology, configuration and trains.

Madrid-Chamartín-Clara Campoamor is the biggest railway station in Spain. Now it has 21 passing tracks of two gauges (15 of the Iberian gauge, traditionally used in Spain and Portugal, and 6 of the standard gauge, used in the Spanish high-speed lines) ^[40]. The railway station is under renovation and it will have in the next future 25 passing tracks (13 of Iberian gauge and 12 of standard gauge) ^[41]. We have considered in Table 2 the track layout of this railway station when all its tracks were of Iberian gauge (in order to consider a real world example as big as possible). This stations contains 250 sections, 81 semaphores, 100 turnouts.

8.   Conclusions

In this paper we have presented a new algebraic model for detecting dangerous situation in a railway station. According to this model, the position of trains in a railway station configuration is considered unsafe if and only if the remainder of a certain monomial (representing the configuration and the current position of the trains) divided by a list of polynomials vanishes. This connects two seemingly different fields: computer algebra and interlocking problems. Not only is this interesting from a theoretical perspective, but it also offers practical advantages. We have implemented this in CoCoA, resulting in very short program code. In this way, any improvement in the implementation of division algorithms immediately results in faster performance in our program. We have compared execution times with other fast models previously implemented by the authors and found that our approach eliminates the need to calculate a Groebner basis. Besides, our approach can be used as 'accelerated-time simulations', allowing for the analysis of different modifications in a railway network without the need to physically implement them with the enormous cost that it would require ^{[42,43,44,45]}.

However, our approach has a significant limitation. While it is mathematically interesting, Computer Algebra Systems have not been certified for use in safety-critical implementations^[46]. Obtaining ad hoc certification is much more costly than certifying a search engine over a table. As a result, our approach currently has no chance of being implemented in real-world systems. Nevertheless, we believe that our approach has value from a mathematical perspective and can be extended in several directions:

● Develop a library that allows for easy definition of the list $E$ for any topology; that defines switch changes and semaphore colors through functions and train movements. Updates to the polynomials $p$ and $q$ through multiplication and division of variables.

● Develop a graphical environment that allows for the visual design of a station and obtains the polynomials in E, p, and q in a computer algebra system like CoCoA.

● Extend our model. Although usual stations do not contain cycles and for each pair of sections there is only one path, it would be interesting from a theoretical point of view to extend the model so that this restriction is not necessary.

● Study alternatives for general graphs, not just those derived from railway stations.

● Extend the interlocking problem to include other problems related to expert systems in railway stations, such as automatically detecting which semaphores and switches cannot be changed because they would imply a dangerous situation. Since our approach expresses the interlocking problem as an algebraic system similar to those used for implementing expert systems ^[16], we believe that our model can be easily integrated into these expert systems.

Use of AI tools declaration

The authors declare they have not used Artificial Intelligence (AI) tools in the creation of this article.

Acknowledgments

This work was partially supported by the research project PID2021-122905NB-C21 (Government of Spain).

This paper is dedicated to the memory of Eugenio Roanes-Lozano. Eugenio passed away suddenly just days after submitting this paper. He was an exceptional researcher in various fields, one of which was his extraordinary passion for trains, with numerous publications on the subject. This paper represents the culmination of his research in this area. Eugenio was a significant figure to us in many ways: as a researcher, teacher, colleague, and most importantly, as a friend. We would like to highlight his immense humanity. Eugenio, it was not yet time for you to take your last train. You will be deeply missed.

Conflict of interest

The authors declare there are no conflicts of interest.

A.   Proof of our approach

In this section, we will formally prove that the new algebraic approach works.

Distinguishing different kinds of railway interlocking problems

Given the details of a railway station through its potential connectivity, $E$ (see Definition 3.1), we will study the relation between different possible railway interlocking problems for this railway station.

We will start defining when railway interlocking problem is trivial.

Definition A.1. Given the potential connectivity of railway station, $E$, a configuration in it, $P$, and a placement of trains, $Q$, we say that the railway interlocking problem $(P, Q)$ is trivial if and only if $Q$ contains two repeated elements.

Obviously, a trivial railway interlocking problem is always in a dangerous situation (because there is more than one train at a certain section).

We will define a transitive relation between railway interlocking problems (see Definition A.2). To illustrate the intuition behind this definition, consider Figure A.1. On the right side of the figure, there is a railway interlocking problem $A$ where a train is in Section $S_i$ (i.e., $i\in Q$), and can move from section $S_i$ to section $S_j$. From this interlocking problem $A$, we can derive another railway interlocking problem, $B$, illustrated on the left side of the figure. In this interlocking problem, $B$, there is another train in section $S_j$ but sections $S_i$ and $S_j$ are now separated: it is no longer possible to move from Section $S_i$ to section $S_j$ or vice versa. We say that the interlocking problem $B$ is derived from $A$. Problems $B$ and $A$ are closely related. According to Proposition A.1 we can detect if $A$ is in a dangerous situation by analyzing $B$. That is to say, $A$ is in a dangerous situation if and only if $B$ is in a dangerous situation. As may be seen, the first and the third items of the formal definition (see Definition A.2) extend this idea so that this relation is reflective and transitive. The relation "is derived from" records possible train movements ($Q_2$ contains both old and new train positions) while changing the configuration of the possible movements in the railway network ($P_2$ does not correspond to the configuration resulting from the train movement from $i$ to $j$).

Definition A.2. Let $(P_1, Q_1)$ and $(P_2, Q_2)$ be two possible railway interlocking problems in a railway station detailed by $E$. We will say that $(P_2, Q_2)$ is immediately derived from $(P_1, Q_1)$ if and only if $\exists (i, j)\in P_1$ such that:

● $i\in Q_1$

and

● $P_2 = P_1-\{(i, j), (j, i)\}$

and

● $Q_2 = Q_1\cup \{j\}$

We define the relation "derived from" as the transitive and reflexive closure of the "immediately derived from'" relation. That is to say: $(P_2, Q_2)$ is derived from $(P_1, Q_1)$ if and only if

● $P_1 = P_2$ and $Q_1 = Q_2$

● $(P_1, Q_1)$ is immediately derived from $(P_2, Q_2)$

● there is a railway interlocking problem $(P_3, Q_3)$ of $E$ such that $(P_2, Q_2)$ is derived from $(P_3, Q_3)$ and $(P_3, Q_3)$ is derived from $(P_1, Q_1)$.

(The key idea underlying the second condition is that if there is a train in a section $S_i$ and $(i, j)\in P$, we can consider instead that such train can reach $S_j$, adding that section to $Q_2$ and to erase $(i, j)$ and $(j, i)$ from $P2$ –if they belong to $P2$.)

In Figure 4.1 there are more examples of this relation: the interlocking problem B is derived from A, C is derived from B, D is derived from C, E is derived from D.

Proposition A.1. Let $(P_1, Q_1)$ and $(P_2, Q_2)$ be two railway interlocking problems in a railway station detailed by $E$ such that $(P_2, Q_2)$ is derived from $(P_1, Q_1)$. We have that:

Proof. As $(P_2, Q_2)$ is derived from $(P_1, Q_1)$, from Definition A.2 it follows that we can suppose that $(i, j)\in P_1$, $i\in Q_1$, $P_2 = P_1-\{(i, j), (j, i)\}$ and $Q_2 = Q_1\cup\{j\}$.

$\boldsymbol{\Rightarrow)}$ $(P_1, Q_1)$ is in a dangerous situation. Let $[u_1, \ldots u_n]$ and $[v_1\ldots v_m]$ be two paths fulfilling Definition 3.5 for $(P_1, Q_1)$.

We will consider the following cases:

Case $\exists k < n$ such that $u_k = j$ and $u_{k +1} = i$. By (7) in Definition 3.5, we have that for every $1\leq k'\leq k$ $u_{k'}\neq i$ and, therefore, $(u_{k'}, u_{k'+1})\notin\{(i, j), (j, i)\}$. Therefore, $[u_1\ldots u_k]$ and $[j]$ fulfil all conditions in Definition 3.5 for $(P_2, Q_2)$.

Case $\exists k' < m$ such that $v_{k'} = j$ and $v_{k' +1} = i$. It is analogous to the previous case.

Case $\exists k < n$ such that $u_k = i$ and $u_{k +1} = j$. Since $i\in Q_1$, by (5) in Definition 3.5, we have that $u_1 = i$.

We will consider the following subcases:

$v_1 = i$. Then $[u_1]$ and $[v_1]$ fulfil all conditions in Definition 3.5 for $(P_2, Q_2)$.

$v_1\neq i$. Since $u_1 = i$, by (6) in Definition 3.5, we have that for every $1\leq k' < m$, $v_{k'}\neq i$. Besides, we have that $v_m\neq i$ since $v_m = u_n\neq u_1 = i$, by (4) and (7) in Definition 3.5 (since we are considering that $n > 1$ in this case). Therefore, $(v_{k'}, v_{k'+1})\notin \{(i, j), (j, i)\}$.

Since $u_1 = i$, by (7) in Definition 3.5 we have that for every $2\leq k\leq n$ $u_k\neq i$, and therefore, $(u_k, u_{k+1})\notin \{(i, j), (j, i)\}$.

Consequently, $[u_2, \ldots u_n]$ and $[v_1\ldots v_m]$ fulfil all conditions in Definition 3.5 for $(P_2, Q_2)$.

Case $\exists k'$ such that $v_{k'} = i$ and $v_{k' +1} = j$. It is analogous to the previous case.

Case for every $1\leq k < n$ $(u_k, u_{k+1}) \notin \{(i, j), (j, i)\}$ and for every $1\leq k' < m$ $(v_{k'}, v_{k'+1}) \notin \{(i, j), (j, i)\}$. It is immediate to prove that $[u_1, \ldots u_n]$ and $[v_1\ldots v_m]$ fulfil all conditions in Definition 3.5 for $(P_2, Q_2)$.

$\boldsymbol{\Leftarrow)}$ Let $[u_1\ldots u_n]$ and $[v_1\ldots v_m]$ be paths fulfilling Definition 3.5 for the railway interlocking problem $(P_2, Q_2)$. Since $P_2\subset P_1$, we have that for every $1\leq k < n$ $(u_k, u_{k+1})\in P_1$ and that for every $1\leq k' < m$ $(v_{k'}, v_{k'+1})\in P_1$. We will consider the following cases:

Case 1. $u_1 = j = v_1$. We have that $[i, j]$ and $[j]$ are paths fulfilling Definition 3.5 for $(P_1, Q_1)$.

Case 2. $u_1\neq j\neq v_1$. We have that $[u_1\ldots u_n]$ and $[v_1\ldots v_m]$ are paths fulfilling Definition 3.5 for $(P_1, Q_1)$.

Case 3. $u_1 = j\neq v_1$. We have that $v_1\neq i$. Otherwise, we would have that $[v_1, u_1\ldots, u_n]$ and $[v_1\ldots v_m]$ would be two different paths from $v_1$ to $v_m = u_n$ for $(P_1, Q_1)$ and this is excluded (see Remark 3.5). Consequently, $[i, u_1\ldots u_n]$ and $[v_1\ldots v_m]$ are paths fulfilling Definition 3.5 for $(P_1, Q_1)$ because:

● $(i, u_1) = (i, j)\in P_1$.

● $\{v_1, i\}\subseteq Q_1$ because $i\in Q_1$, $v_1\neq i$, and, since $v_1\neq j$ $v_1 \in Q_1$.

Case 4. $v_1 = j\neq u_1$. It is analogous to the previous case.

Although every trivial railway interlocking problem is in a dangerous situation, not all railway interlocking problems in a dangerous situations are trivial ones. However, a trivial railway interlocking problem can be derived from any railway interlocking problem in a dangerous situation (Theorem A.1).

Theorem A.1. A railway interlocking problem $(P, Q)$ is in a dangerous situation if and only if a trivial railway interlocking problem is derived from $(P, Q)$.

Proof. $\boldsymbol{\Rightarrow)}$ Let us suppose that $(P, Q)$ is in a dangerous situation.

Let $[u_1, \ldots, u_n]$ and $[v_1, \ldots, v_m]$ be paths fulfilling Definition 3.5. That is to say, we have that $u_n = v_m$, $(u_i, u_{i+1})\in P$, $(v_i, v_{i+1})\in P$, $u_1\in Q$ and $v_1 \in Q$.

We'll proceed by induction on the sum of the lengths of the two paths, $n+m$.

Case n = m = 1: The paths are $[u_1]$ and $[v_1]$. Since $u_1 = v_1$ we have that this is a trivial railway interlocking problem.

Case $n>1$ or $m>1$. Let us suppose that $n > 1$ (the case $m > 1$ is identical). Since $(u_1, u_2)\in P$ and $u_1\in Q$, we have that $(P_2, Q_2) = (P-\{(u_1, u_2), (u_2, u_1)\}, Q\cup \{u_2\})$ is derived from $(P, Q)$. Then $(P_2, Q_2)$ is in a dangerous situation because the paths $[u_2, \ldots, u_n]$ and $[v_1, \ldots, v_m]$ fulfil the conditions in Definition 3.5. By induction hypothesis, a trivial railway interlocking problem is derived from $(P_2, Q_2)$, and therefore, this trivial railway interlocking problem is derived from $(P, Q)$.

$\boldsymbol{\Leftarrow})$ Let us suppose that a trivial railway interlocking problem is derived from the railway interlocking problem $(P, Q)$. As a consequence of Definition A.1, a trivial railway interlocking problem is always in a dangerous situation, and therefore, by Proposition A.1, we have that $(P, Q)$ is in a dangerous situation too.

Algebraic Preliminaries. Some introductory notes about polynomial rings

In this section we will briefly describe some results about polynomial rings that we will need to prove the validity of our approach (see, for instance, ^[34], for a detailed introduction to the topic).

Definition A.3. A monomial in $x_1, \ldots, x_N$ is a product of the form $x_1^{\alpha_1}\cdot x_2^{\alpha_2}\cdot \dots x_N^{\alpha_N}$. An element in the polynomial ring $\mathbb{K}[x_1, \ldots, x_N]$ is a polynomial in the variables $x_1, \ldots, x_N$ whose coefficients lie in the field $\mathbb{K}$, that is, a finite linear combination of monomials with coefficients in $\mathbb{K}$:

where $a_{(\alpha_1, \alpha_2, ..., \alpha_N)} \in \mathbb{K}$ and $\alpha_1, \alpha_2, ..., \alpha_N \in \mathbb{Z}_{\geq 0}$, written sometimes, for the sake of brevity

If $a_{(\alpha_1, \alpha_2, ..., \alpha_N)} \neq 0$ then $a_{(\alpha_1, \alpha_2, ..., \alpha_N)} x^{\alpha_1}x^{\alpha_2}\dots x^{\alpha_N}$ is called a term. If $\mathbb{K} = \mathbb{Q}$, an example of polynomial in $\mathbb{Q}[x_1, x_2, x_3]$ is $p = 2x_1^2+7x_1x_2x_3-x_3+\frac{1}{2}x_2x_3$.

Later in this paper we will focus on the case $\mathbb{K} = \mathbb{Z}_2$. An element in the polynomial ring $\mathcal{A} = \mathbb{Z}_2[x_1, \ldots, x_N]$ is a polynomial in the variables $x_1, \ldots, x_N$ whose coefficients lie in the field $\mathbb{Z}_2 = \{0, 1\}$. An example of this kind of polynomials is $p = x_1x_2+x_3+x_2x_3$. We must take into account that the coefficients lie in $\mathbb{Z}_2$, and therefore, we have that, for instance, (since 1+1 = 0 in $\mathbb{Z}_2$):

The algebraic structure ideal is key in our approach.

Definition A.4. An ideal of a commutative ring is a subring that verifies that the product of any element of the ring by any element of the subring belongs to the subring.

Example A.1. For instance, the set of even numbers is an ideal of $\mathbb{Z}$. For example, the set of polynomials in $\mathbb{Z}[x]$ with a trailing coefficient equal to $0$ (i.e., the multiples of $x$) form an ideal of $\mathbb{Z}[x]$.

Proposition A.2. Given a set of polynomials $G = \{f_1, \ldots, f_m\} \subseteq \mathbb{K}[x_1, \ldots, x_N]$, the smallest ideal containing $G$, denoted $\langle f_1, \ldots, f_m\rangle$, turns out to be:

Notation A.1. For the sake of simplicity, if $G$ is a list of polynomials, we will denote $\langle G \rangle$ the ideal generated by the polynomials in $G$.

Once an order for the variables is given, for instance $x_1 > x_2 > \ldots > x_m$, a total order for the monomials can be defined (see ^[34], pp. 52–57). Although there are many monomial orderings, we will use the pure lexicographical order in this paper. Simplifying it, if we have, for instance, $x < y$ and the monomials $x^2y = xxy$ and $x^3 = xxx$, think of them as if they were words to be ordered in a dictionary: $xxx < xxy$.

Definition A.5. The leading monomial of a polynomial $p\in\mathbb{K}[x_1, \ldots, x_N]$, denoted ${\rm{LM}}(p)$, is its greatest monomial with respect to the chosen monomial ordering. The corresponding term is its leading term, and is denoted ${\rm{LT}}(p)$.

Example A.2. For example, in $\mathbb{R}[x_1, x_2, x_3]$ with $x_1 > x_2 > x_3$ and the lexicographic monomial order:

and

Remark A.1. In this paper we will focus on the case $\mathbb{K} = \mathbb{Z}_2$, and, obviously, in these polynomial rings: $LT(p) = LM(p)$.

Theorem A.2. Once the monomial ordering is defined in $\mathbb{K}[x_1, \ldots, x_N]$, the division of a polynomial $p$ by an ordered $m$- list of polynomials $G = (f_1, \ldots, f_m)$ can be defined. This division outputs:

where $\alpha_1, \ldots, \alpha_m, r\in\mathbb{K}[x_1, \ldots, x_N]$ and either $r = 0$ or $r$ is a linear combination of monomials, none of which is divisible by any of ${\rm{LT}}(f_1) \dots {\rm{LT}}(f_m)$.

A proof can be found in (see ^[34], pp. 62–64).

Notation A.2. The polynomial $r$, remainder of $p$ on division by $G$, will be denoted ${\rm{NR}}(p, G)$ or $\overline{p}^G$.

The proof in ^[34] (pp. 62–64) provides an algorithm to find the polynomials $\alpha_1, \ldots \alpha_m, r\in \mathbb{K}[x_1, \ldots, x_N]$ in Theorem A.2. In each step of this algorithm we obtain an intermediate-dividend. We will require only some of the first intermediate-dividends of this algorithm.

Definition A.6. Given $p\in\mathbb{K}[x_1, \ldots, x_N]$ and an ordered $m$- list of polynomials $G = (f_1, \ldots, f_m)\subseteq\mathbb{K}[x_1, \ldots, x_N]$, we recursively define the first-intermediate-dividends of $p$ on division by $G$, $r_0, \ldots, r_n\in\mathbb{K}[x_1, \ldots, x_N]$, as follows:

● $r_0 = p$,

● if $i > 0$ then

– if $\exists j\in\{1, \ldots, m\}$ such that ${\rm{LT}}(f_j)|{\rm{LT}}(r_i)$ then

where $k$ is the minimum $j$ such that ${\rm{LT}}(f_j)|{\rm{LT}}(r_i)$,

– if $\forall j\in\{1, \ldots, m\}, {\rm{LT}}(f_j)\!\!\not|{\rm{LT}}(r_i)$ then $r_n = r_i$.

According to the proof ^[34] (pp. 62–64), we have:

Proposition A.3. Let $p\in\mathbb{K}[x_1, \ldots, x_N]$ and let $G = (f_1, \ldots, f_m)\subseteq\mathbb{K}[x_1, \ldots, x_N]$ be an ordered $m$- list of polynomials. Let $r_0, \ldots r_n\in\mathbb{K}[x_1, \ldots, x_N]$ be the first-intermediate-dividends of $p$ on division by $G$. We have that:

Groebner bases are very special ideal bases: among other nice properties, they allow to decide whether a polynomial belongs to the ideal or not (see Theorem A.3). As we wil see, Grobener bases will play an important role in the proof in our main result, Theorem A.11.

Theorem A.3. Let $p$ be a polynomial in $\mathbb{K}[x_1, \ldots, x_N]$ and let $G$ be a Groebner basis for an ideal $I \subset \mathbb{K}[x_1, \ldots, x_N]$. Then we have that:

A proof can be found in ^[34] (Proposition 1 and Corollary 2, pp. 79–80).

Notation A.3. Let $p_1, p_2 \in \mathbb{K}[x_1, \ldots, x_N]$. ${\rm{LCM}}(p_1, p_2)$ denotes least common multiple of $p_1$ and $p_2$.

Definition A.7. Let $p_1, p_2 \in \mathbb{K}[x_1, \ldots, x_N]$. The S-polynomial of $p_1$ and $p_2$ is:

Remark A.2. Obviously, in case the polynomial ring considered is $\mathcal{A} = \mathbb{Z}_2[x_1, \ldots, x_N]$, the $-$ in Definition A.7 can be substituted by a $+$.

Remark A.3. In case the polynomial ring considered is $\mathcal{A} = \mathbb{Z}_2[x_1, \ldots, x_N]$, if $p \in \mathcal{A}$, $p \neq 0$, then ${\rm{LM}}(p) = {\rm{LT}}(p)$.

The following theorem allows to verify if $G$ is a Groebner basis:

Theorem A.4. Let $I$ be a polynomial ideal in $\mathbb{K}[x_1, \ldots, x_N]$ and let $G = \{f_1, \ldots, f_m\}$ be a basis of $I$. Then:

(where $G^*$ is an an ordered $m$- list of the polynomials in $G$, ordered in some way).

A proof can be found in ^[34] (Theorem 6, pp. 82–85).

The railway interlocking problem in algebraic terms

Given a railway station and the description, $E$, of its potential connectivity between sections (see Definition 3.1), we will define the list $\mathcal{E}'$ from the list $\mathcal{E}$ (see Section 4.1) as follows:

Lemma A.5. Let $E$ be the description of the potential connectivity between sections of a railway station. Then:

Proof. It is enough to prove that $\forall f_1, f_2 \in \mathcal{E}'$, $\overline {S(f_1, f_2)}^{\mathcal{E}'} = 0$. But the elements of $\mathcal{E}'$ are of the form $g_{ij}$ or $g'_{ij}$ or $t_i^2$ or $m_{ij}^2$, and, although tedious, it can be easily checked by hand or using a CAS, that in the $4^2$ possible combinations, the S-polynomial vanishes.

Hereinafter, $p$ and $q$ are the polynomials representing the given configuration of the railway station, $P$, and the placement of the trains, $Q$, respectively (see Section 4.1).

Lemma A.6. Let $(P, Q)$ be a railway interlocking problem for a railway station whose connectivity is described by $E$. Let $r_0, r_1\ldots r_n$ be the first-intermediate-dividends of $pq$ on division by any chosen ordering of the elements $\mathcal{E}'$. Then:

i) $\forall i\in\{0, \ldots, n-1\}$ there is a railway interlocking problem $(P_i, Q_i)$ derived from $(P, Q)$ such that $r_i = p_iq_i$.

ii) If ${\rm{NR}}(pq, \mathcal{E}') = 0$ the railway interlocking problem $(P, Q)$ is in a dangerous situation.

Proof.

${\rm{i)}}$ For $i = 0$, we have that $r_0 = pq$ and, therefore, $(P_0, Q_0) = (P, Q)$ is a railway interlocking problem derived from $(P, Q)$.

Suppose that $0 < i < n$, $r_{i-1} = p_{i-1}q_{i-1}$ and $(P_{i-1}, Q_{i-1})$ is a railway interlocking problem derived from $(P, Q)$. We will prove that $r_i$ represents a railway interlocking problem, $(P_i, Q_i)$, derived from $(P, Q)$. According to Definition A.6, we have that:

where $f_k$ is a polynomial in $\mathcal{E}'$ such that ${\rm{LT}}(f_k)|{\rm{LT}}(r_{i-1})$. We have also that ${\rm{LT}}(r_{i-1}) = {\rm{LT}}(p_{i-1}q_{i-1}) = p_{i-1}q_{i-1}$, where $p_{i-1}$ is a monomial that contains only variables of the kind $l_{xy}$ and $m_{xy}$, and $q_{i-1}$ is a monomial that contains only variables of the kind $t_x$ (see Section 4.1).

We have that $f_{k}\neq t_k^2$. Otherwise, we would have that $r_i = 0$, and therefore, $i = n$ (but we have supposed that $i < n$).

We have that $f_{k}\neq m_{xy}^2$ because $pq$ is a monomial where the exponent of the $m_{xy}$ variables is at most $1$.

Consequently, there are two cases left:

Case $f_k = g_{xy}$. We have that $g_{xy}$ is of the form:

$g_{xy} = l_{xy}l_{yx}t_x + m_{xy}m_{yx}t_xt_y$.

Since ${\rm{LT}}(f_k)|{\rm{LT}}(r_{i-1})$ we have that ${\rm{LT}}(g_{x, y}) = l_{xy}l_{yx}t_x | p_{i-1}q_{i-1}$. Thus, we have that $l_{xy}l_{yx}|p_i$ and $t_x|q_i$ (remember that $p_{i-1}$ is a monomial that contains only variables of the kind $l_{xy}$ and $m_{xy}$, and $q_{i-1}$ is a monomial that contains only variables of the kind $t_x$). Consequently:

– $p_{i-1}$ is of the form $p_{i-1} = p'\cdot l_{xy}l_{yx}$ where $p'$ is a monomial.

– $q_{i-1}$ is of the form $q_{i-1} = q'\cdot t_x$ where $q'$ is a monomial.

Therefore, we have that

We define:

– $p_i = p'\cdot m_{xy}m_{yx}$

– $q_i = q'\cdot t_xt_y$

Just observe that $p_i$ is a monomial that contains the same variables as $p_{i-1}$ except that $l_{x, y}$ and $l_{y, x}$ in $p_{i-1}$ have respectively turned to be $m_{x, y}$ and $m_{y, x}$. In the same way, $q_i$ is a monomial that contains all the variables in $q_{i-1}$ and also the variable $t_y$. Consequently, we have that $r_i = p_iq_i$ are polynomials representing the railway interlocking problem $(P_i, Q_i)$ where $P_i = P_{i-1}- \{(x, y), (y, x)\}$ and $Q_i = Q_{i-1}\cup \{y\}$.

Case $f_k = g'_{x, y}$. We have that $g'_{xy}$ is of the form:

$g'_{xy} = l_{xy}m_{yx}t_x + m_{xy}m_{yx}t_xt_y$.

Since ${\rm{LT}}(f_k)|{\rm{LT}}(r_{i-1})$ we have that ${\rm{LT}}(g'_{x, y}) = l_{xy}m_{yx}t_x | p_{i-1}q_{i-1}$. Thus, we have that $l_{xy}m_{yx}|p_i$ and $t_x|q_i$ (remember that $p_{i-1}$ is a monomial that contains only variables of the kind $l_{xy}$ and $m_{xy}$, and $q_{i-1}$ is a monomial that contains only variables of the kind $t_x$). Consequently:

– $p_{i-1}$ is of the form $p_{i-1} = p'\cdot l_{xy}m_{yx}$ where $p'$ is a monomial

– $q_{i-1}$ is of the form $q_{i-1} = q'\cdot t_x$ where $q'$ is a monomial

Therefore, we have that:

We define:

– $p_i = p'\cdot m_{xy}m_{yx}$

– $q_i = q'\cdot t_xt_y$

Just observe that $p_i$ is a monomial that contains the same variables as $p_{i-1}$ except that $l_{x, y}$ in $p_{i-1}$ has turned to be $m_{x, y}$. In the same way, $q_i$ is a monomial that contains all the variables in $q_{i-1}$ and also the variable $t_y$. Consequently, we have that $r_i = p_iq_i$ is a monomial representing the railway interlocking problem $(P_i, Q_i)$ where $P_i = P_{i-1} -\{(x, y)\} = P_{i-1}- \{(x, y), (y, x)\}$ (just observe that $(y, x)\not \in P_{i-1}$) and $Q_i = Q_{i-1}\cup \{y\}$.

Consequently, we have that $r_i = p_iq_i$ represents that the interlocking problem $(P_i, Q_i)$ is derived from $(P_{i-1}, Q_{i-1})$. By the transitivity property of the derived relation between railway interlocking problems (see Definition A.2), we have that $(P_i, Q_i)$ is also derived from $(P, Q)$.

ⅱ) According to Proposition A.3, we have that $r_n = {\rm{NR}}(pq, \mathcal{E}') = 0$. Consequently,

That is to say, $p_{n-1} q_{n-1} = \frac{p_{n-1} q_{n-1}}{{\rm{LT}}(f_k)}f_k$

Since $p_{n-1} q_{n-1}$ is a monomial, we have that $f_k$ must be also a monomial. Consequently, $f_k$ cannot be either of the form $g_{ij}$ or the form $g'_{ij}$. Besides, $f_k$ cannot be either of the form $m_i^2$ since $pq$ is a monomial where the exponent of the $m_{ij}$ variables is at most $1$. Therefore, we have that $f_k = t_x^2$.

Since ${\rm{LT}}(f_k)|{\rm{LT}}(r_{n-1})$, we have that $t_x^2|p_{n-1}q_{n-1}$, and consequently, the interlocking problem $(P_{n-1}, Q_{n-1})$ is a trivial railway interlocking because $Q_{n-1}$ contains a repeated element $x$. Therefore, $(P_{n-1}, Q_{n-1})$ is in a dangerous situation.

By ⅰ) we have that $(P_{n-1}, Q_{n-1})$ is derived from $(P, Q)$. Since $(P_{n-1}, Q_{n-1})$ is in a dangerous situation, by Theorem A.1, we have that $(P, Q)$ is also in a dangerous situation.

Lemma A.7. Let $(P, Q)$ be a railway interlocking problem for a railway station described by $E$. We have that:

Proof. Since the algorithm for calculating ${\rm{NR}}(pq, \mathcal{E}')$ in Lemma A.6 discards the case $f_{k} = m_{ij}^2$, we have that ${\rm{NR}}(pq, \mathcal{E}) = {\rm{NR}}(pq, \mathcal{E}')$.

According to previous results (see ii in Lemmas A.6 and A.7), we have a sufficient condition to detect if an interlocking problem $(P, Q)$ is in a dangerous situation: if ${\rm{NR}}(pq, \mathcal{E}) = 0$ then the interlocking problem $(P, Q)$ is in a dangerous situation. Now, we will prove that this is also a necessary condition: if the interlocking problem $(P, Q)$ is in a dangerous situation, then ${\rm{NR}}(pq, \mathcal{E}) = 0$. This proof is more complicated and requires translating the problem in terms of a ideal membership problem. An important result for the proof will be that $\mathcal{E}'$ is a Groebner basis.

Lemma A.8. Let $(P_0, Q_0)$ be a trivial railway interlocking problem for a railway station described by $E$. We have that:

Proof. According to Definition A.1, $i$ must appear more than once in $Q_0$. Let $k$ be the number of times $i$ appears in $Q_0$. Since $k\geq 2$, we have that $k = m+2$ where $m\geq 0$. Therefore, we have that $q_0$ is of the form $q_0 = q'\cdot t_i^k = q'\cdot t_i^{m+2} = q'\cdot t_i^m\cdot t_i^2$ where $q'$ is a monomial. Consequently, $p_0q_0 = p_0\cdot q'\cdot t_i^m\cdot t_i^2\in\langle\mathcal{E}' \rangle$ since $t_i^2\in \mathcal{E}'$.

Lemma A.9. Let $(P_1, Q_1)$ and $(P_2, Q_2)$ be two railway interlocking problems for a railway station described by $E$ such that $(P_2, Q_2)$ is derived from $(P_1, Q_1)$. We have that:

Proof. Let $(i, j)\in P_1$ be such that $i\in Q_1$

and $P_2 = P_1 - \{(i, j), (j, i)\}$

and $Q_2 = Q_1 \cup\{j\}.$

Since $i\in Q_1$ and $Q_2 = Q_1\cup\{j\}$, we have that $q_1$ and $q_2$ are of the form (for a certain monomial $q$):

$q_1 = q\cdot t_i$

$q_2 = q\cdot t_it_j$

Since $(i, j)\in P_1$ we have that $l_i | p_1$.

We will consider two cases:

Case $(j, i)\in P_1$. We have that $l_{ji} | p_1$. Since $P_2 = P_1\cup\{(i, j)(j, i)\}$, we have that $p_1$ and $p_2$ are of the form (for a certain monomial $p$):

$p_1 = p\cdot l_{ij}l_{ji}$

$p_2 = p\cdot m_{ij}m_{ji}$

Besides, we have that $g_{ij} = l_{ij}l_{ji}t_i + m_{ij}m_{ji}t_it_j \in \mathcal{E}'$. Therefore, we have that:

$pq\cdot g_{ij} = pq \cdot l_{ij}l_{ji}t_i + pq\cdot m_{ij}m_{ji}t_it_j = p_1q_1 + p_2q_2$

Consequently,

Case $(j, i)\not \in P_1$. We have that $m_{ji} | p_1$. Since $P_2 = P_1\cup\{(i, j), (j, i)\}$, we have that the monomials $p_1, p_2$ are of the form (where $p$ is a certain monomials):

$p_1 = p\cdot l_{ij}m_{ji}$

$p_2 = p\cdot m_{ij}m_{ji}$

Besides, we have that $g'_{ij} = l_{ij}m_{ji}t_i + m_{ij}m_{ji}t_it_j \in \mathcal{E}'$. Therefore, we have that:

$pq\cdot g'_{ij} = pq \cdot l_{ij}m_{ji}t_i + pq\cdot m_{ij}m_{ji}t_it_j = p_1q_1 + p_2q_2$

Consequently,

We have the following theorem:

Theorem A.10. Let $(P, Q)$ be a railway interlocking problem for a railway station described by $E$.

Proof. $\boldsymbol{\Rightarrow)}$ Let $(P, Q)$ be a railway interlocking problem in a dangerous situation. According to Theorem A.1, we have that a trivial railway interlocking problem is derived from $(P, Q)$. According to Lemmas A.8 and A.9, we have that $pq\in\langle \mathcal{E}'\rangle$.

$\boldsymbol{\Leftarrow})$ Suppose that $pq\in\langle\mathcal{E}'\rangle$. Since $\mathcal{E}'$ is a Groebner basis (see Lemma A.5), we have, by Theorem A.3, that ${\rm{NR}}(pq, \mathcal{E}') = 0$. Consequently, by Lemma A.6, we have that $(P, Q)$ is in a dangerous situation.

Since the list $\mathcal{E}'$ is indeed a Groebner basis (see Lemma A.5), the ideal membership problem of the previous theorem can be easily solved (see Theorem A.11).

Theorem A.11. Let $(P, Q)$ be a railway interlocking problem for a railway station described by $E$. We have that:

Proof. This is a immediate consequence of Theorem A.3, Lemma A.5, Theorem A.10 and Lemma A.7.

B.   A linear algorithm for calculating $NR$ for our algebraic approach

Here we will propose an efficient algorithm for calculating ${\rm{NR}}(p, \mathcal{E})$ for the specific case that:

● The coefficients of polynomials lie in $\mathbb{Z}_2$.

● $p$ is a monomial.

● $\mathcal{E} = \{g_i\}$ is a list of polynomials such that each $g_i$ is the sum of two monomials $p_i$ and $q_i$. That is to say, $g_i = p_i+q_i$ where $p_i > q_i$. We will use the notation ${\rm{LT}}(g_i) = p_i$ and $M(g_i) = q_i$.

In this specific case, the general algorithm for calculating ${\rm{NR}}$ can be simplified since all intermediate dividends are monomials and the algorithm can run in O($N$) if we use appropriate data structures:

● In order to represent $p = \prod_j {x_j}^{v_j}$ we use the array $[v_1\ldots v_N]$. An empty array $[]$ will represent the monomial $p = 0$. We will use this data structure to represent the intermediate dividends of the algorithm. For example, we represent the monomial $p = x_1x_2^3$ by means of the array $p: [1, 3, 0, \ldots, 0]$.

● In order to represent the monomials $p_i$ and $q_i$ in $g_i = p_i+q_i$ we use a list with the form $\{(x_i, v_i)\}$. In this case a list $\{(x_j, v_j)\}$ will represent the monomial $q_i = \prod_j {x_j}^{v_j}$. For example, we represent the monomial $q_i = x_1x_2^3$ by means of the list $\{(x_1, 1), (x_2, 3)\}$.

● In order to represent the polynomial $g_i = p_i+q_i$, we use two lists: one for representing $p_i$, another for representing $q_i$. For example, for $\mathcal{E} = \{g_1, g_2, g_3\}$ where $g_1 = x_1x_2+x_2x_3; g_2 = x_2^2 + x_5x_6; g_3 = x_3 + x_5$ we represent each polynomial $g_i$ in the following way:

– $g_1 = x_1x_2+x_2x_3$ is represented by these two lists: ${\rm{LT}}(g_1) = \{(1, 1), (2, 1)\}; M(g_1) = \{(2, 1), (3, 1)\}$.

– $g_2 = x_2^2 + x_5x_6$ is represented by these two lists: ${\rm{LT}}(g_2) = \{(2, 2)\}; M(g_2) = \{(5, 1), (6, 1)\}$.

– $g_3 = x_3 + x_5$ is represented by these two lists: ${\rm{LT}}(g_3) = \{(3, 1)\}; M(g_3) = \{(5, 1)\}$.

● For each variable $x_j$ we consider $F_{x_j}$, the list of the polynomials $g_i\in\mathcal{E}$ such that the variables are in ${\rm{LT}}(g)$: that is to say, there is some natural $e$ such that $(x_j, e)\in {\rm{LT}}(g)$. For example, in case that $\mathcal{E} = [g_1, g_2, g_3] = [x_1x_2+x_2x_3, x_2^2 + x_5x_6, x_3 + x_5]$, we have that:

– $F_{x_1} = \{g_1\}$ because $x_1$ appears in the monomial ${\rm{LT}}(g_1)$.

– $F_{x_2} = \{g_1, g_2\}$ because $x_2$ appears in the monomials ${\rm{LT}}(g_1)$ and ${\rm{LT}}(g_2)$.

– $F_{x_3} = \{g_3\}$ because $x_2$ appears in the monomial ${\rm{LT}}(g_3)$.

– $F_{x_4} = F_{x_5} = F_{x_6} = \emptyset$ because $x_4, x_5, x_6$ do not appear in ${\rm{LT}}(g_i)$ for any $g_i$.

● For each polynomial $g_i$, we consider $V_{g_i}$, the set of the variables that are in $M(g_i)$. For example, in case that $\mathcal{E} = [g_1, g_2, g_3] = [x_1x_2+x_2x_3, x_2^2 + x_5x_6, x_3 + x_5]$, we have that:

– $V_{g_1} = \{2, 3\}$ because $x_2$ and $x_3$ appears in $M(g_1)$.

– $V_{g_2} = \{5, 6\}$ because $x_5$ and $x_6$ appears in $M(g_2)$.

– $V_{g_3} = \{5\}$ because $x_5$ appears in $M(g_3)$.

The algorithm for calculating the remainder of a monomial $p$ with respect to a list of polynomials $\mathcal{E}$ is the following:

The algorithm $\mathtt{CanBeUsedToReduce(g, p)}$ outputs $\mathtt{true}$ if ${\rm{LT}}(g)\|p$ (that is to say, if the polynomial $g$ can be used to reduce the monomial $p$). This algorithm is very simple and checks for every $(a, b)\in {\rm{LT}}(g)$ if $\mathtt{p[a]> b}$. Since the size of ${\rm{LT}}(g)$ is constant in our algebraic model, this algorithm runs in O(1).

The algorithm $\mathtt{Reduce(g, p)}$ calculates a new intermediate dividend (that is to say, reduces the monomial $p$ with respect to the polynomial $g$). This algorithm is also very simple due to the data structures used. For every $(a, b)\in {\rm{LT}}(g)$ and $(a, c)\in M(g)$, we update $\mathtt{p[a]}$ with the value $\mathtt{p[a]-b+c}$. Since the size of the sets ${\rm{LT}}(g)$ and $M(g)$ are constant in our algebraic model, this algorithm runs in O(1).

The algorithm uses a stack, $\mathtt{check}$, in which the algorithm stores the polynomials $g_i$ that may be used to reduce the monomial p. The algorithm ${\rm{NR}}$ runs in O($N$) since the step $\mathtt{Reduce}$ can only be applied $N$ times at most and every time the monomial is reduced, the number of polynomials added to $\mathtt{check}$ is constant.