# A New Algebraic Approach to Decision Making in a Railway Interlocking System Based on Preprocess

Authors: Antonio Hernando; Roberto Maestre; Eugenio Roanes-Lozano
Journal: Mathematical Problems in Engineering
 (2018)

---

## Abstract

The safety of railway networks is a very important issue. Roughly speaking, it can be split into safety along lines and safety of railway facilities such as stations, junctions, yards, etc. In modern networks the safety along lines is controlled byautomatic block systems that do not give clearance to trains to enter a section (block) until the latter is detected to be unoccupied. Meanwhile, the safety within railway facilities is supervised byrailway interlocking systems. Decision making in a railway interlocking is a very important issue which is considered to be very labour-intensive. Decision-making in both automatic block systems and railway interlocking systems, unlike road traffic light systems, is not based on time (they are not scheduling problems) but in space. Basically, two different trains should never be allowed to access the same section (whatever time has passed). There are many different approaches to automate decision-making in railway interlocking systems. The classic approaches are offline: only certain routes are allowed and their compatibility is decided in advance. Meanwhile, modern approaches make decisions in real time and are independent from the topology of the railway network, but can be applied only to small or medium size railway networks. Nevertheless, these last approaches have the following drawbacks: the performances are very dependent on the number of trains in the railway network; and are unsuitable to large networks since they take long time to be run. On the other hand, algebraic approaches based on computer algebra concepts have been used in artificial intelligence for implementing expert systems. In this paper we present a completely new algebraic model, based on these concepts of computer algebra that overcomes these drawbacks: the performance of our approach is independent of the number of trains in the railway network and also is suitable for large railway networks.


---

## Body

## 1. Introduction

The safety of railway networks is a very important issue. Roughly speaking, it can be split in safety along lines and safety of railway facilities such as stations, junctions, yards, etc.In modern networks the safety along lines is controlled by automatic block systems, that do not give clearance to trains to enter a section (block) until the latter is detected to be unoccupied.Meanwhile, the safety within railway facilities is supervised by railway interlocking systems. Decision making in a railway interlocking is a very important issue which is considered very labour-intensive.Railway interlocking systems are conceived so that different trains can be placed on different sections. Semaphores (mechanical devices) or light signals and turnouts must be stated so that two trains cannot collide when moving, if obeying the signalling. A railway interlocking system has the purpose of not allowing unsafe situations in the railway network. In fact the most sophisticated railway interlocking systems also forbid the switches under the train to be changed before the train has left that section, an issue that is not addressed in this article.Let us underline that decision making in both automatic block systems and railway interlocking systems, unlike road traffic light systems, are not based on time (that is, they are not scheduling problems) but in space: basically, two different trains should never be allowed to access the same section (whatever time has passed since the first one entered the section). The reason is that trains need long distances to break and a train can be unexpectedly found stopped at a certain place due, for instance, to a breakdown. This approach has allowed to introduce semiautomatic train operation and even driverless train operation in some subways and airport shuttle services much earlier than autonomous cars were developed, although that is not the topic of this article.The first railway interlocking systems were mechanical and were installed in the second half of the nineteenth century (Figure1). In the mid twentieth century the control was relays-based (Figure 2). From the 1980s, most of the new railway interlocking systems are computer-controlled (electronic interlocking systems) [1–4]. Many of the interlocking systems are specifically designed for a particular railway network and they are not topology-independent. For instance, the first topology-independent railway interlocking system in Spain was installed only in 1993 [5]. Detecting if the situation of trains in a railway network is dangerous is an eye-catching problem. Traditionally, an offline approach is followed: only certain routes are considered and what is allowed by the interlocking is established in advance, usually by hand [6].Figure 1
A mechanical railway interlocking system still in use at a junction in 2009. On the left a general view of the system is shown. The levers operated the semaphores (mechanical devices) and the switches of the turnouts. On the right a top view is shown. In the latter the bars that detect if a given lever conflicts with that controlled by another lever are clearly visible (it was common that the mechanical railway interlocking had glass tops so that the internal system could be appreciated).Figure 2
One of the corridors full of relays of the relay interlocking system of a big railway station in the ‘90s.Modern approaches use algorithms for checking in real time the safety of a railway network: any proposed change in the position of switches and the signals aspects is analyzed in real time before being authorized. Clearly, an exhaustive analysis of all the possible movements allowed to all trains according to the proposal has to be performed. Obviously, the performance of the algorithm is a crucial issue of these approaches. It is surprising that, in real railway interlocking systems, unacceptable errors can be found (this happened, for instance, in the railway interlocking system of a tiny subway station [7]).There are many different papers regarding computer applications to railway interlocking systems in general [8] and decision making in particular. These latter works either create a formal specification for an existing railway system (in order to verify it or to create a new decision making tool) or describe a completely new model for railway interlocking systems. Some of these approaches depend strongly on the number of trains in the railway network and are not suitable for large railway networks.This paper deals with a new algebraic method for detecting the safety in a railway network that overcomes these previous drawbacks. It uses computer algebra concepts (like Boolean polynomials, ideals, Groebner bases, or normal forms) to solve the problem of decision making in a railway interlocking system.The paper is structured in the following way. In Section2, we will discuss techniques related to ours. In Section 3, we will define formally concepts related to railway networks. In Section 4, we will describe our method (as a black box) for determining the safety of a railway network. In Section 5, we will explain the basis of our algebraic approach based on the calculations of Groebner bases and normal forms. In Section 6, we will show the advantages of our model. As said above in this section, there are very many different approaches to decision making in a railway interlocking (see, e.g., the survey [8]), but usually the code is not available. That is why different approaches are described in Section 6 but the new system proposed is just compared with four (but very different) approaches, for which the complete implementation was available. Finally, in Section 8, we will set our conclusions.


## 2. Related Works

### 2.1. An Overview of Different Approaches

In this section, we will analyze different approaches for the problem of detecting the safety of a certain situation in a railway network.In the classic approach, admissible train routes are predefined. Aroute denotes a path along the topology of the station or junction (for instance a path from an entrance of the station to a certain track where the train will stop). Establishing a route implies adequately setting the switches of the turnouts and light signals along the train route. Once an engine driver has been given a proceed signal concerning a route, the route is locked (that is, it cannot be changed before the train has completely cleared it). The standard approach to railway interlocking systems design is to predefine the admissible train routes and to manually study in advance their compatibility.Many works have been proposed for railway interlocking systems (see, for instance, the survey [8]). These works either are specifically designed for an existing railway system or develop a generic new model. The Ph.D. thesis [9] uses a theorem prover implemented in higher-order logic to detect the safety of a certain situation in a railway interlocking. This work is revisited using an annotated logic program with temporal reasoning in [10]. The work [6] uses ordered binary decision diagrams to model railway interlocking systems. The work [11] uses Z notation for an example in the Slovak National Railways. In [12], a VDM model is presented for a case in the Danish State Railways. In [13–15] statecharts are used instead.An early topology-independent formal model is [16]. It uses different layers of abstraction (called domains). Petri nets are used for the dynamic domains and double point graphs as well as logic invariants for the static domains. It is implemented inObjective-C andPROLOG. Let us underline that it does not follow the standard approach to railway interlocking systems; the concept of routes has been replaced with a context-free check of the permissibility for each controlling command.A generic tool for verifying and validating railway interlocking systems is detailed in [17]. The track interlocking tables corresponding to an existing tramway network is represented using a domain-specific language (DSL) as illustration, and they are automatically transformed into an executable control system model expressed in SystemC.In [18] DSL is also used to represent and analyze the track layout diagrams, interlocking tables, and circuit diagrams of existing relay interlockings of the DSB (Danish state Railways).In [19] the size of the layouts that can be addressed using formal methods for checking interlocking tables described with control tables is explored. The symbolic model checker NuSMV and the verification system SPIN are used and the conclusion is that these methods cannot be used to address large layouts.The model checker NuSMV is also used in [20], where a formal model is built from a high-level (logic) description. The interlocking system is interpreted as an Abstract State Machine (ASM). The approach is applied to certain railway interlocking systems of Queensland Rails (QR) network.Duration calculus, a specific technique for real-time systems [21], has also been applied to decision making in a railway interlocking [22].


### 2.2. Some Approaches with Available Code

The following topologically independent approaches do not consider the direction of the trains (allowing to directly deal with special situations like reversing loops and reversing triangles).Model Based on Graphs. In [23] the problem is translated into graph theory language and treated using a matrices-based approach. This approach cannot be used for large railways networks because the matrices involved are square and sparse but N
×
N (where N is the number of sections of the network).Algebraic Model. In [24], the problem is directly translated into an algebraic problem. According to this model, the safety of a railway network may be detected by calculating the Groebner basis [25–27] of a polynomial ideal. This approach is not suitable for large stations since the calculation of the Groebner bases of these polynomial ideals usually take a long time. These Groebner bases depend not only on the position of the switches of the turnouts and the color of the light signals, but also on the position of the trains. Curiously, computing times decrease in this model when the number of trains increases, as variables (representing sections) are substituted by numbers (representing trains).Model Based on Boolean Propositional Logic. In [28], the problem is directly translated into many SAT problems which can be solved using an algorithm based on the DPLL technique [29]. Indeed, the safety of a railway network may be detected by solving N SAT problems where N is the number of sections of the railway network. These SAT problems depend on the position of the switches of the turnouts and the color of the light signals, as well as on the position of the trains. Like the previous approaches, this approach is not suitable for large stations, since many SAT problems need to be solved for a particular configuration of the railway network.Logic-Algebraic Model. According to the model [30], the safety of the railway network may be detected by calculating a Groebner basis of an ideal of Boolean polynomials, G (which usually takes considerable time), and the normal forms of N polynomials modulo G (which is usually very fast computed). Like in [24], only a Groebner bases calculation is required for a particular state of the railway network. However, this model is much faster than [24], since the Groebner basis of this model (unlike the model [24]) is calculated on Boolean polynomials. This model is also faster than the previous one [28]. Nevertheless, this approach depends on the position of the trains and the performing time for calculations strongly depends on the number of trains.ASP Model. According to [31], the problem to check the safety of the railway network is directly translated in the answer set programming (ASP) paradigm, defining relations and derived relations and solving the problem with logic techniques from ASP. This approach is much faster and efficient than previous approaches and thus can be applied to larger railway stations. From an operational point of view, the response time of this model depends on the number of trains in the station; i.e., more trains means more time to check the safety.However, all of the previous approaches (except ASP) are not suitable for very large railway networks with many trains, since they involve long time to detect dangerous situation. In this paper, we will propose a completely new approach based on the calculation of a Groebner basis. In this new algebraic approach, unlike the algebraic approach in [24], we deal with Boolean polynomials and we use specialized algorithms for calculating Groebner bases over Boolean polynomials [32]. The approach here presented is completely different from [30]. Indeed, the set of polynomials for which we calculate the Groebner basis does not depend on the trains in the railway network (unlike [30]). As we will see in Section 6, once a precomputation has been performed, our approach is much faster than the previous ones (see Section 6) and is suitable for very large stations.


## 2.1. An Overview of Different Approaches

In this section, we will analyze different approaches for the problem of detecting the safety of a certain situation in a railway network.In the classic approach, admissible train routes are predefined. Aroute denotes a path along the topology of the station or junction (for instance a path from an entrance of the station to a certain track where the train will stop). Establishing a route implies adequately setting the switches of the turnouts and light signals along the train route. Once an engine driver has been given a proceed signal concerning a route, the route is locked (that is, it cannot be changed before the train has completely cleared it). The standard approach to railway interlocking systems design is to predefine the admissible train routes and to manually study in advance their compatibility.Many works have been proposed for railway interlocking systems (see, for instance, the survey [8]). These works either are specifically designed for an existing railway system or develop a generic new model. The Ph.D. thesis [9] uses a theorem prover implemented in higher-order logic to detect the safety of a certain situation in a railway interlocking. This work is revisited using an annotated logic program with temporal reasoning in [10]. The work [6] uses ordered binary decision diagrams to model railway interlocking systems. The work [11] uses Z notation for an example in the Slovak National Railways. In [12], a VDM model is presented for a case in the Danish State Railways. In [13–15] statecharts are used instead.An early topology-independent formal model is [16]. It uses different layers of abstraction (called domains). Petri nets are used for the dynamic domains and double point graphs as well as logic invariants for the static domains. It is implemented inObjective-C andPROLOG. Let us underline that it does not follow the standard approach to railway interlocking systems; the concept of routes has been replaced with a context-free check of the permissibility for each controlling command.A generic tool for verifying and validating railway interlocking systems is detailed in [17]. The track interlocking tables corresponding to an existing tramway network is represented using a domain-specific language (DSL) as illustration, and they are automatically transformed into an executable control system model expressed in SystemC.In [18] DSL is also used to represent and analyze the track layout diagrams, interlocking tables, and circuit diagrams of existing relay interlockings of the DSB (Danish state Railways).In [19] the size of the layouts that can be addressed using formal methods for checking interlocking tables described with control tables is explored. The symbolic model checker NuSMV and the verification system SPIN are used and the conclusion is that these methods cannot be used to address large layouts.The model checker NuSMV is also used in [20], where a formal model is built from a high-level (logic) description. The interlocking system is interpreted as an Abstract State Machine (ASM). The approach is applied to certain railway interlocking systems of Queensland Rails (QR) network.Duration calculus, a specific technique for real-time systems [21], has also been applied to decision making in a railway interlocking [22].


## 2.2. Some Approaches with Available Code

The following topologically independent approaches do not consider the direction of the trains (allowing to directly deal with special situations like reversing loops and reversing triangles).Model Based on Graphs. In [23] the problem is translated into graph theory language and treated using a matrices-based approach. This approach cannot be used for large railways networks because the matrices involved are square and sparse but N
×
N (where N is the number of sections of the network).Algebraic Model. In [24], the problem is directly translated into an algebraic problem. According to this model, the safety of a railway network may be detected by calculating the Groebner basis [25–27] of a polynomial ideal. This approach is not suitable for large stations since the calculation of the Groebner bases of these polynomial ideals usually take a long time. These Groebner bases depend not only on the position of the switches of the turnouts and the color of the light signals, but also on the position of the trains. Curiously, computing times decrease in this model when the number of trains increases, as variables (representing sections) are substituted by numbers (representing trains).Model Based on Boolean Propositional Logic. In [28], the problem is directly translated into many SAT problems which can be solved using an algorithm based on the DPLL technique [29]. Indeed, the safety of a railway network may be detected by solving N SAT problems where N is the number of sections of the railway network. These SAT problems depend on the position of the switches of the turnouts and the color of the light signals, as well as on the position of the trains. Like the previous approaches, this approach is not suitable for large stations, since many SAT problems need to be solved for a particular configuration of the railway network.Logic-Algebraic Model. According to the model [30], the safety of the railway network may be detected by calculating a Groebner basis of an ideal of Boolean polynomials, G (which usually takes considerable time), and the normal forms of N polynomials modulo G (which is usually very fast computed). Like in [24], only a Groebner bases calculation is required for a particular state of the railway network. However, this model is much faster than [24], since the Groebner basis of this model (unlike the model [24]) is calculated on Boolean polynomials. This model is also faster than the previous one [28]. Nevertheless, this approach depends on the position of the trains and the performing time for calculations strongly depends on the number of trains.ASP Model. According to [31], the problem to check the safety of the railway network is directly translated in the answer set programming (ASP) paradigm, defining relations and derived relations and solving the problem with logic techniques from ASP. This approach is much faster and efficient than previous approaches and thus can be applied to larger railway stations. From an operational point of view, the response time of this model depends on the number of trains in the station; i.e., more trains means more time to check the safety.However, all of the previous approaches (except ASP) are not suitable for very large railway networks with many trains, since they involve long time to detect dangerous situation. In this paper, we will propose a completely new approach based on the calculation of a Groebner basis. In this new algebraic approach, unlike the algebraic approach in [24], we deal with Boolean polynomials and we use specialized algorithms for calculating Groebner bases over Boolean polynomials [32]. The approach here presented is completely different from [30]. Indeed, the set of polynomials for which we calculate the Groebner basis does not depend on the trains in the railway network (unlike [30]). As we will see in Section 6, once a precomputation has been performed, our approach is much faster than the previous ones (see Section 6) and is suitable for very large stations.


## 3. Basic Concepts regarding a Railway Interlocking System

Let us consider the tiny station in Figure3(Notice that the turnouts represented in the figures are really punctual elements that do not represent section themselves, they only represent the connectivity between sections.). As may be seen, the railway network represented is divided into sections, denoted in this case S
1
,
…
,
S
11 (there is a light signal between sections S
1 and S
2, a turnout D
1 connecting sections S
2
,
S
3 and S
9, and another light signal between sections S
10 and S
9, and so on).Figure 3
A very simple station.TakingD
1 on Figure 3 as example, the position of the switches can hold two states:(i)
Direct track position: the switch of turnoutT
1 connects sections S
2 and S
3.
(ii)
Diverted track position: the switch ofD
1 connects sections S
2 and S
9.The position of the switches of the turnouts in Figure3 is as follows: D
1 is in the direct track position (connecting S
2 and S
3) and D
2 in the diverted track position (connecting S
11 and S
6). Note the symbols under the turnouts.In this paper only nontrailable turnouts will be considered. However, it will be easy to extend this approach in order to model trailable turnouts just adding more polynomials. Let us underline that a trailable turnout is a turnout that allows to be passed even when the switch is not in the correct position.A light signal can hold two states:(i)
Proceed, represented by or  in the figures. For instance, in Figure 3,  indicates “proceed", thus it is possible to pass from S
1 to S
2,
(ii)
Stop, represented by or  in the figures. For instance, in Figure 3,  indicates “stop", thus it is not possible to pass from S
4 to S
5.If, for instance, three trains are placed onS
1
,
S
10, and S
8 (respectively), and the switch of D
1 is in the direct track position, and the switch of D
2 is in the diverted track position; , ,  indicate “proceed" and , , ,  indicate “stop" (see Figure 4); the proposed situation is dangerous because section S
7 and S
8 are reachable by the trains placed in S
10 and S
8.Figure 4
Example of dangerous situation.If, for instance, two trains are placed onS
1 and S
10 (respectively), and the switch of D
1 is in the direct track position, and the switch of D
2 is in the diverted track position; , ,  indicate “proceed" and , , ,  indicate “stop" (see Figure 5); the proposed situation is safe.Figure 5
Example of safe situation.More formally, let us consider a railway network withM sections and N trains placed in it. Asection is a connected (single piece) part of the network, separated from the adjacent (neighbour) sections by a light signal or a turnout.It is possible to pass from sectionS
i to the adjacent section S
j if and only if(i)
there is a turnout between sectionsS
i and section S
j, and its switch directs trains from S
i to section S
j and conversely (like S
2 and S
3 in Figure 3),
(ii)
there is a light signal controlling the pass fromS
i to S
j, and it indicates “proceed” (for instance, the light signal  controlling the movement from S
1 to S
2 in Figure 3, indicates “proceed”),
(iii)
there is no light signal controlling the pass fromS
i to S
j, and they are not connected by a turnout, but there is a light signal controlling the pass from S
j to S
i (like S
2 and S
1 in Figure 3).We provide afterwards a recursive definition illustrating the idea that a train may reach a given section.Definition 1.
The notion “a traint
i can reach section S
j” is recursively defined as (i)
if traint
i is in section S
j then it can reach section S
j,
(ii)
if traint
i is in section S
l and it can reach section S
k and it is possible to pass from section S
k to section S
j according to the position of the switches and the color of the light signals, then train t
i can reach section S
j.Definition 2.
LetM be a positive integer, M
≤
N, and let {
w
1
,
w
2
,
…
,
w
M
}
⊆
{
1,2
,
…
,
N
}. The position of M trains in sections S
w
1
,
…
,
S
w
M (one in each section) is dangerous if and only if there is a section S
i reachable from two sections S
j and S
k (j
≠
k) where two different trains are placed.


## 4. Overview of Our Approach

### 4.1. Description

In this section we will describe the approach proposed for determining the safety of a railway network composed ofN sections, denoted as S
1
,
…
,
S
N.Our approach is based on defining a set of Boolean polynomials (that is to say, polynomials whose coefficients are in{
0,1
}) in variables s
1
,
…
,
s
N
,
t
1
,
…
,
t
N. A variable s
i and a variable t
i are considered for each section S
i in the railway network. More precisely,(i)
a polynomial variable,s
i, is assigned to each section S
i;
(ii)
another polynomial variable,t
i, is considered for each section S
i. Let us underline that variables t
i represent neither a section nor a train. The polynomial variables t
i will be used to introduce both the allowed connectivity between sections (see the paragraphs immediately below and Section 5) and the sections occupancy (through the membership of some of these polynomial variables to a certain polynomial monomial that introduces the positions of the trains).For a configuration of the railway network (defining the position of the switch of each turnout and the color of each light signal), we will consider the following steps.Step 1.
Obtain a setK of polynomials according to the connectivity of the railway network: if it is possible to pass from section S
i to section S
j, we will consider the polynomial t
i
+
s
i
t
j. That is to say, we have that (1)
K
=
t
i
+
s
i
t
j
∣
i
t
i
s
p
o
s
s
i
b
l
e
t
o
p
a
s
s
from
s
e
c
t
i
o
n
S
i
t
o
s
e
c
t
i
o
n
S
jStep 2.
Calculate the Groebner basis,G, of the following ideal: (2)
I
=
K
+
s
1
2
+
s
1
,
…
,
s
N
2
+
s
N
,
t
1
2
+
t
1
,
…
,
t
N
2
+
t
N
(with respect to a certain order for the monomials and a certain order for the polynomial variables). Although Groebner bases [25–27] is a complicated concept of algebra to be completely detailed here, in Section 5.1, we will describe those properties of this concept which are relevant for our purpose.Once these two steps are calculated, we can determine whether the position of a set of trains is dangerous or not. In this approach, a train only can be placed in one section at the same time, however, as we will see later in Section7, we can extend the proposed model to take into account when a train occupies several sections at the same time.Step 3.
LetM be a positive integer, M
≤
N, and let {
w
1
,
w
2
,
…
,
w
M
}
⊆
{
1,2
,
…
,
N
}. For determining if the position of M trains in sections S
w
1
,
S
w
2
,
…
,
S
w
M (one in each section) is dangerous, we calculate the normal form of the monomial t
w
1
t
w
2
…
t
w
M modulo I (I can be given through the Groebner basis G previously calculated): (3)
N
F
t
w
1
t
w
2
…
t
w
M
,
I
Like Groebner bases, the concept of normal form is also enough complicated to be completely described here. Nevertheless, in Section5.1, we will describe those properties relevant for our purpose.
In this step we can detect if the position of the trains is dangerous. Indeed, as we will see in Theorem9, we have that the position of the trains is dangerous if and only if N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
) contains a number of t
α variables lower than M.As we will see, Step 1 and Step 2 are only needed to be performed again if the configuration of the railway network changes. Only Step 3 must be performed (which is very fast done, around 0.0001 seconds) for different placement of the trains. As we have previously stated, this is an important advantage of the present approach over the previous approaches, which require to completely run the algorithm for different positions of the trains.


### 4.2. Example of the Approach

Let us consider the example of the railway network depicted in Figure3. Since this railway network contains 11 sections, we will make use of polynomials in variables s
1
,
…
,
s
11
,
t
1
,
…
,
t
11.Step 1.
We calculate the setK of t
i
+
s
i
t
j polynomials related to the connectivity of the railway network (defined in Step 1 of Section 4.1):(4)
K
=
t
1
+
s
1
t
2
,
t
2
+
s
2
t
1
,
t
2
+
s
2
t
3
,
t
3
+
s
3
t
2
,
t
3
+
s
3
t
4
,
t
5
+
s
5
t
4
,
t
9
+
s
9
t
10
,
t
10
+
s
10
t
11
,
t
11
+
s
11
t
10
,
t
6
+
s
6
t
11
,
t
6
+
s
6
t
7
,
t
7
+
s
7
t
8
,
t
8
+
s
8
t
7
(for instance,t
1
+
s
1
t
2 is included in K because it is possible to pass from section S
1 to section S
2). Observe that trailing through a switch set against is not allowed. Then it is as if the turnout was guarded by (possibly) nonexistent light signals. For instance, it is considered that moving from s
9 to s
2 and from s
5 to s
6 is forbidden.Step 2.
We calculate the Groebner basis of the ideal:(5)
I
=
K
+
s
1
2
+
s
1
,
…
,
s
11
2
+
s
11
,
t
1
2
+
t
1
,
…
,
t
11
2
+
t
11
:and(6)
G
=
t
1
+
s
1
t
2
,
t
2
+
s
2
t
1
,
t
2
+
s
2
t
3
,
t
3
+
s
3
t
2
,
t
3
+
s
3
t
4
,
t
5
+
s
5
t
4
,
t
9
+
s
9
t
10
,
t
10
+
s
10
t
11
,
t
11
+
s
11
t
10
,
t
6
+
s
6
t
11
,
t
6
+
s
6
t
7
,
t
7
+
s
7
t
8
,
t
8
+
s
8
t
7is obtained.Step 3.
Once the Groebner basis is calculated, we can immediately determine if the position of a set of trains is dangerous for this configuration of the railway network.(i)
As example, if there are three trains respectively placed in sectionsS
1
S
10
S
8, in order to determine if the position of the trains is dangerous, we just simply need to calculate: (7)
N
F
t
1
t
10
t
8
,
I
=
t
4
t
11
As may be seen, there are only two variablest
α in N
F
(
t
1
t
10
t
8
,
I
)
=
t
4
t
11, which is lower than the number of trains. Therefore, we determine that the position of the trains in {
S
1
,
S
10
,
S
8
} is dangerous (as may be seen, section S
7 is reachable from sections S
8 and section S
11, where trains are placed).(ii)
As example, if there are now two trains respectively placed in sectionsS
1
,
S
10, in order to determine if the the position of the trains is dangerous we just simply need to calculate: (8)
N
F
t
1
t
10
,
G
=
t
1
t
11
As may be seen, there are two variablest
α in N
F
(
t
1
t
10
,
I
)
=
t
1
t
10, which is equal to the number of trains in the railway network. Therefore, we determine that the position of the trains in {
S
1
,
S
10
} is not dangerous.


## 4.1. Description

In this section we will describe the approach proposed for determining the safety of a railway network composed ofN sections, denoted as S
1
,
…
,
S
N.Our approach is based on defining a set of Boolean polynomials (that is to say, polynomials whose coefficients are in{
0,1
}) in variables s
1
,
…
,
s
N
,
t
1
,
…
,
t
N. A variable s
i and a variable t
i are considered for each section S
i in the railway network. More precisely,(i)
a polynomial variable,s
i, is assigned to each section S
i;
(ii)
another polynomial variable,t
i, is considered for each section S
i. Let us underline that variables t
i represent neither a section nor a train. The polynomial variables t
i will be used to introduce both the allowed connectivity between sections (see the paragraphs immediately below and Section 5) and the sections occupancy (through the membership of some of these polynomial variables to a certain polynomial monomial that introduces the positions of the trains).For a configuration of the railway network (defining the position of the switch of each turnout and the color of each light signal), we will consider the following steps.Step 1.
Obtain a setK of polynomials according to the connectivity of the railway network: if it is possible to pass from section S
i to section S
j, we will consider the polynomial t
i
+
s
i
t
j. That is to say, we have that (1)
K
=
t
i
+
s
i
t
j
∣
i
t
i
s
p
o
s
s
i
b
l
e
t
o
p
a
s
s
from
s
e
c
t
i
o
n
S
i
t
o
s
e
c
t
i
o
n
S
jStep 2.
Calculate the Groebner basis,G, of the following ideal: (2)
I
=
K
+
s
1
2
+
s
1
,
…
,
s
N
2
+
s
N
,
t
1
2
+
t
1
,
…
,
t
N
2
+
t
N
(with respect to a certain order for the monomials and a certain order for the polynomial variables). Although Groebner bases [25–27] is a complicated concept of algebra to be completely detailed here, in Section 5.1, we will describe those properties of this concept which are relevant for our purpose.Once these two steps are calculated, we can determine whether the position of a set of trains is dangerous or not. In this approach, a train only can be placed in one section at the same time, however, as we will see later in Section7, we can extend the proposed model to take into account when a train occupies several sections at the same time.Step 3.
LetM be a positive integer, M
≤
N, and let {
w
1
,
w
2
,
…
,
w
M
}
⊆
{
1,2
,
…
,
N
}. For determining if the position of M trains in sections S
w
1
,
S
w
2
,
…
,
S
w
M (one in each section) is dangerous, we calculate the normal form of the monomial t
w
1
t
w
2
…
t
w
M modulo I (I can be given through the Groebner basis G previously calculated): (3)
N
F
t
w
1
t
w
2
…
t
w
M
,
I
Like Groebner bases, the concept of normal form is also enough complicated to be completely described here. Nevertheless, in Section5.1, we will describe those properties relevant for our purpose.
In this step we can detect if the position of the trains is dangerous. Indeed, as we will see in Theorem9, we have that the position of the trains is dangerous if and only if N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
) contains a number of t
α variables lower than M.As we will see, Step 1 and Step 2 are only needed to be performed again if the configuration of the railway network changes. Only Step 3 must be performed (which is very fast done, around 0.0001 seconds) for different placement of the trains. As we have previously stated, this is an important advantage of the present approach over the previous approaches, which require to completely run the algorithm for different positions of the trains.


## 4.2. Example of the Approach

Let us consider the example of the railway network depicted in Figure3. Since this railway network contains 11 sections, we will make use of polynomials in variables s
1
,
…
,
s
11
,
t
1
,
…
,
t
11.Step 1.
We calculate the setK of t
i
+
s
i
t
j polynomials related to the connectivity of the railway network (defined in Step 1 of Section 4.1):(4)
K
=
t
1
+
s
1
t
2
,
t
2
+
s
2
t
1
,
t
2
+
s
2
t
3
,
t
3
+
s
3
t
2
,
t
3
+
s
3
t
4
,
t
5
+
s
5
t
4
,
t
9
+
s
9
t
10
,
t
10
+
s
10
t
11
,
t
11
+
s
11
t
10
,
t
6
+
s
6
t
11
,
t
6
+
s
6
t
7
,
t
7
+
s
7
t
8
,
t
8
+
s
8
t
7
(for instance,t
1
+
s
1
t
2 is included in K because it is possible to pass from section S
1 to section S
2). Observe that trailing through a switch set against is not allowed. Then it is as if the turnout was guarded by (possibly) nonexistent light signals. For instance, it is considered that moving from s
9 to s
2 and from s
5 to s
6 is forbidden.Step 2.
We calculate the Groebner basis of the ideal:(5)
I
=
K
+
s
1
2
+
s
1
,
…
,
s
11
2
+
s
11
,
t
1
2
+
t
1
,
…
,
t
11
2
+
t
11
:and(6)
G
=
t
1
+
s
1
t
2
,
t
2
+
s
2
t
1
,
t
2
+
s
2
t
3
,
t
3
+
s
3
t
2
,
t
3
+
s
3
t
4
,
t
5
+
s
5
t
4
,
t
9
+
s
9
t
10
,
t
10
+
s
10
t
11
,
t
11
+
s
11
t
10
,
t
6
+
s
6
t
11
,
t
6
+
s
6
t
7
,
t
7
+
s
7
t
8
,
t
8
+
s
8
t
7is obtained.Step 3.
Once the Groebner basis is calculated, we can immediately determine if the position of a set of trains is dangerous for this configuration of the railway network.(i)
As example, if there are three trains respectively placed in sectionsS
1
S
10
S
8, in order to determine if the position of the trains is dangerous, we just simply need to calculate: (7)
N
F
t
1
t
10
t
8
,
I
=
t
4
t
11
As may be seen, there are only two variablest
α in N
F
(
t
1
t
10
t
8
,
I
)
=
t
4
t
11, which is lower than the number of trains. Therefore, we determine that the position of the trains in {
S
1
,
S
10
,
S
8
} is dangerous (as may be seen, section S
7 is reachable from sections S
8 and section S
11, where trains are placed).(ii)
As example, if there are now two trains respectively placed in sectionsS
1
,
S
10, in order to determine if the the position of the trains is dangerous we just simply need to calculate: (8)
N
F
t
1
t
10
,
G
=
t
1
t
11
As may be seen, there are two variablest
α in N
F
(
t
1
t
10
,
I
)
=
t
1
t
10, which is equal to the number of trains in the railway network. Therefore, we determine that the position of the trains in {
S
1
,
S
10
} is not dangerous.


## 5. Theoretical Foundations of Our Approach

In this section we will detail the theoretical foundations of our algebraic approach for the problem of detecting dangerous situation in a railway network. In Section5.1, we will give some outlines about concepts of computer algebra (like Boolean polynomials, ideals, Groebner bases, normal forms) which are relevant for this paper. In Section 5.2 we will describe the problem of detecting dangerous situation in an interlocking system by means of states and transformation of the states by means of operations. As we will see in Section 5.3, these states may be represented in algebraic terms (by means of Boolean monomials) which will allow us to determine whether the position of the trains is dangerous or not.


### 5.1. Some Introductory Notes about Boolean Polynomials and Ideals

In this section we will describe some outlines about Boolean polynomial. A polynomialp
∈
Z
2
[
x
1
,
…
,
x
N
] is a polynomial in the variables x
1
,
…
,
x
N whose coefficients lie in the field Z
2
=
{
0,1
}. An example of this kind of polynomials is (9)
p
=
x
1
x
2
7
+
x
3
+
x
2
x
3
x
4We must take into account the fact that the coefficients lie inZ
2, and therefore, we have that (since 1+1=0 in Z
2), for example, (10)
x
1
x
2
+
x
3
x
4
+
x
3
x
4
=
x
1
x
2
+
1
+
1
x
3
x
4
=
x
1
x
2As we have previously seen, the concept of ideal will play an important role in our approach. An ideal is a special kind of subset of a ring: it is also a ring and has the curious property that the product of an element of the subring by an element of the ring (and vice versa, if the ring is not a commutative one) always belongs to the subring. For instance, the set of even numbers is an ideal of the integers. In our case, the idealJ, generated by p
1
,
…
,
p
m, denoted J
=
〈
p
1
,
…
,
p
m
〉, turns out to be the set of polynomials of the following form: (11)
β
1
p
1
+
…
+
β
m
p
mwhere β
1
,
…
,
β
N are polynomials in Z
2
[
x
1
,
…
,
x
N
], that is, J is the set of algebraic combinations of p
1
,
…
,
p
m.Given a polynomialp, we define p
+
J as the set of polynomials of the form p
+
q where q
∈
J. It is possible that p
+
J
=
q
+
J although p
≠
q.Example 3.
Let us consider the idealJ
=
x
1
+
x
2
x
3
,
x
2
+
x
3
x
4 and the polynomial p
=
x
1
x
4
+
x
2. We have that (12)
p
+
J
=
x
1
x
4
+
x
2
+
J
=
x
2
x
3
x
4
+
x
2
+
J
x
1
=
x
2
x
3
b
e
c
a
u
s
e
x
1
+
x
2
x
3
∈
J
=
x
3
2
x
4
2
+
x
2
+
J
1
s
t
o
c
u
r
r
e
n
c
e
of
x
2
=
x
3
x
4
b
e
c
a
u
s
e
x
2
+
x
3
x
4
∈
J
=
x
3
2
x
4
2
+
x
3
x
4
+
J
2
n
d
o
c
u
r
r
e
n
c
e
of
x
2
=
x
3
x
4
b
e
c
a
u
s
e
x
2
+
x
3
x
4
∈
JIn this paper, we will consider polynomials inZ
2
[
s
1
,
…
,
s
N
,
t
1
,
…
,
t
N
]. The ideal I defined in Section 4 is generated by the following polynomials:(i)
The polynomialss
i
2
+
s
i, t
i
2
+
t
i
∈
I
,
i
=
1
,
…
n,. This involves that, for every polynomial p, we can get a polynomial q such that p
+
I
=
q
+
I and the exponents of all the variables in q is 1.Example 4.
Let us consider, for example, the idealI and the polynomial p
=
s
1
2
t
2
3
+
s
1
t
2
+
s
1
3. We have that (13)
p
+
I
=
s
1
2
t
2
3
+
s
1
t
2
+
s
1
3
+
I
=
s
1
t
2
2
t
2
+
s
1
t
2
+
s
1
2
s
1
+
I
s
1
2
=
s
1
,
t
2
3
=
t
2
2
t
2
a
n
d
s
1
3
=
s
1
2
s
1
=
s
1
t
2
t
2
+
s
1
t
2
+
s
1
s
1
+
I
t
2
2
=
t
2
a
n
d
s
1
2
=
s
1
=
s
1
t
2
2
+
s
1
t
2
+
s
1
2
+
I
t
2
t
2
=
t
2
a
n
d
s
1
s
1
=
s
1
2
=
s
1
t
2
+
s
1
t
2
+
s
1
+
I
t
2
2
=
t
2
a
n
d
s
1
2
=
s
1
=
s
1
+
I
2
s
1
t
2
=
0Remember that (as we have seen before)(14)
K
=
t
i
+
s
i
t
j
∣
i
t
i
s
p
o
s
s
i
b
l
e
t
o
p
a
s
s
from
s
e
c
t
i
o
n
S
i
t
o
s
e
c
t
i
o
n
S
jand (15)
I
=
K
+
s
1
2
+
s
1
,
…
,
s
N
2
+
s
N
,
t
1
2
+
t
1
,
…
,
t
N
2
+
t
N
(ii)
The polynomialt
i
+
s
i
t
j
∈
I if it is possible to pass from section S
i to section S
j. This involves that for every monomial t
1
·
…
·
t
n we can obtain other monomials in variables t and s.Example 5.
In the example of the railway network described in Figure3, we have that p
=
t
1
t
10
t
8: (16)
p
+
I
=
t
1
t
10
t
8
+
I
=
t
1
t
10
s
8
t
7
+
I
t
8
=
s
8
t
7
b
e
c
a
u
s
e
t
8
+
s
8
t
7
∈
I
=
t
1
s
10
t
11
s
8
t
7
+
I
t
10
=
s
10
t
11
b
e
c
a
u
s
e
t
10
+
s
10
t
11
∈
I
=
t
1
s
10
s
11
t
6
s
8
t
7
+
I
t
11
=
s
11
t
6
b
e
c
a
u
s
e
t
11
+
s
11
t
6
∈
I
=
t
1
s
10
s
11
s
6
t
7
s
8
t
7
+
I
t
6
=
s
6
t
7
b
e
c
a
u
s
e
t
6
+
s
6
t
7
∈
I
=
t
1
s
10
s
11
s
6
t
7
2
s
8
+
I
t
7
t
7
=
t
7
2
=
t
1
s
10
s
11
s
6
t
7
s
8
+
I
t
7
2
=
t
7
=
t
1
s
10
s
11
s
6
t
8
+
I
s
8
t
7
=
t
8
b
e
c
a
u
s
e
t
8
+
s
8
t
7
∈
IBy means of these substitutions induced by the idealI, we can obtain, for every monomial p, another monomial q whose variables are to power 1 and such that p
+
I
=
q
+
I.An important solved issue in computer algebra is to find the “simplest” monomialq such that q
+
I
=
p
+
I. In a formal way, we pose the problem of finding the minimal polynomial q (where a total order between monomials, ⪯, must be defined) such that p
+
I
=
q
+
I. This polynomial q is what is called normal form of p modulo the ideal I (under the order ⪯), N
F
(
p
,
I
), which can be calculated by performing pseudodivisions of the polynomial p by a Groebner basis of the ideal I (which are required to be previously calculated). In this way, the concept of normal form requires defining a monomial order.For the purpose of this paper, we will define the following order between monomials:(i)
Ifp contains a lower number of t
α variables than q, we have that p
⪯
q.
(ii)
Ifp contains exactly the same number of t
α variables as q, we have that p
⪯
q
⇔
p
⪯
L
e
x
q, where ⪯
L
e
x is the typical lexicographical order used in computer algebra.By means of this order⪯, the normal form of p modulo I, N
F
(
p
,
I
), returns the monomial q with minimal number of variables in t such that p
+
I
=
q
+
I. Next equations are examples of ⪯ order used in this approach: (17)
s
3
⪯
t
1
=
T
r
u
e
t
1
⪯
s
3
=
F
a
l
s
e
t
2
⪯
t
1
=
T
r
u
e
t
1
⪯
t
2
=
F
a
l
s
e
s
1
⪯
s
2
=
F
a
l
s
e


### 5.2. An Approach to the Railway Interlocking Problem Based on States

Here we will see how the interlocking problem can be described by means of states which are transformed by means of operations. On the one hand a state describes the sections where the trains are presently placed in the railway network at a given moment; on the other one, past states describe the sections where the trains were placed in the railway network in the past. Operations of the states (i.e., transitions between states) represent possible movements of the trains in the railway network.For our purpose, each state is described by a subset of variabless
1
,
…
,
s
N, t
1
,
…
,
t
N.The following are examples of possible states of the railway network in Figure3: E
0
=
t
1
t
10
t
8
,
E
1
=
t
1
t
10
s
8
t
7
,
E
2
=
t
1
s
10
t
11
s
8
t
7,E
3
=
{
t
1
s
10
s
11
t
6
s
8
t
7
}
,
E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
t
7
}
,
E
5
=
{
t
1
s
10
s
11
s
6
t
8
}.We can transform a stateE
i into another one E
j by means of one of these operations (we will denote E
i
→
E
j):(i)
When it is possible, substitute allt
i in E
i by the monomial s
i
t
j
∈
I if it is possible to pass from S
i to S
j. For example, we have that E
0
→
E
1 (E
0
=
{
t
1
t
10
t
8
} and E
1
=
{
t
1
t
10
s
8
t
7
}) by substituting t
8 by s
8
t
7, because t
8
+
s
8
t
7
∈
I.
(ii)
When it is possible, substitute alls
i
t
j in E
i by the variable t
i
∈
I if it is possible to pass from S
i to S
j. For example, we have that E
4
→
E
5 (E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
t
7
} and E
5
=
{
t
1
s
10
s
11
s
6
t
8
}) by substituting s
8
t
7 by t
8, because t
8
+
s
8
t
7
∈
I.Variablest and s in these states inform about possible movements of the trains. Variables t indicate the present position of the trains, and variables s the sections through which these trains have gone. Indeed,(i)
the stateE
0
=
{
t
1
t
10
t
8
} represents that there are trains in the sections S
1
,
S
10, S
8 (variables t
1
,
t
10
,
t
8 appear in E
0);
(ii)
the stateE
1
=
{
t
1
t
10
s
8
t
7
} represents that there are trains in the sections S
1
,
S
7
,
S
10 (variables t
1
,
t
7
,
t
10 appear in E
1) and that (at least) one of these trains has passed through the section S
8 (variable s
8 appears in E
1);
(iii)
the stateE
2
=
{
t
1
s
10
t
11
s
8
t
7
} represents that there are trains in the sections S
1
,
S
7
,
S
11 (variables t
1
,
t
7
,
t
11 appear in E
2) and that (at least) one of these trains has passed through the sections S
8
,
S
10 (variables s
10
,
s
8 appear in E
2);
(iv)
the stateE
3
=
{
t
1
s
10
s
11
t
6
s
8
t
7
} represents that there are trains in the sections S
1
,
S
6
,
S
7 (variables t
1
,
t
6
,
t
7 appear in E
3) and that (at least) one of these trains has passed through the sections S
8
,
S
10
,
S
11 (variables s
8
,
s
10
,
s
11 appear in E
3).As may be seen, statesE
0
,
E
1
,
E
2, E
3 contain the same number of variables t representing the position of the trains in different times. However, we can transform the state E
3
=
{
t
1
s
10
s
11
t
6
s
8
t
7
} into the state E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
t
7
}
=
{
t
1
s
10
s
11
s
6
t
7
s
8
} by substituting t
6 with s
6
t
7 (the train which was in section S
6 moves to section S
7). In this case, the number of “t” variables is lower than the cardinal of E
3, since the variable t
7 (that we add with the operation) indeed belongs to the previous state E
3. The operation means that the train which was in section S
6 moves to section S
7, and, since section S
7 was occupied by another train, a possible collision may happen.Following this reasoning, we have the following.Proposition 6.
LetM be a positive integer, M
≤
N, and let {
w
1
,
w
2
,
…
,
w
M
}
⊆
{
1,2
,
…
,
N
}. The position of M trains in sections S
w
1
,
S
w
2
,
…
,
S
w
M (one in each section) is dangerous ⇔ the state E
0
=
{
t
1
…
t
M
} can be transformed into a state E
z with a number of t
α variables lower than M.In the previous example we had{
t
1
t
10
t
8
}
=
E
0
→
E
1
→
E
3
→
E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
}. According to the previous proposition, the position of the trains in sections S
1, S
10, S
8 (related to the state E
0
=
{
t
1
t
10
t
8
}) is dangerous in the railway network (as we saw in Section 3).


### 5.3. Interpretation of States in Algebraic Terms

In this section, we will represent each of the states described in the previous section by means of a Boolean monomial. As we will see, this representation will be useful for determining whether the position of the trains is dangerous or not.We represent each stateE, a set consisting in one monomial, by means of precisely such monomial, so φ
(
E
)
∈
Z
2
[
s
1
…
,
s
N
,
t
1
…
,
t
N
], and can be expressed as follows: (18)
φ
E
=
∏
i
∈
S
^
s
i
∏
j
∈
T
^
t
jwhere S
^
,
T
^
⊆
{
1
,
…
,
N
}
∧
T
^
≠
∅. In this way, we have the following:(i)
φ
(
E
0
)
=
φ
(
{
t
1
t
10
t
8
}
)
=
t
1
t
10
t
8
(ii)
φ
(
E
1
)
=
φ
(
{
t
1
t
10
s
8
t
7
}
)
=
t
1
t
10
s
8
t
7
(iii)
φ
(
E
2
)
=
φ
(
{
t
1
s
10
t
11
s
8
t
7
}
)
=
t
1
s
10
t
11
s
8
t
7
(iv)
φ
(
E
3
)
=
φ
(
{
t
1
s
10
s
11
t
6
s
8
t
7
}
)
=
t
1
s
10
s
11
t
6
s
8
t
7
(v)
φ
(
E
4
)
=
φ
(
{
t
1
s
10
s
11
s
6
t
7
s
8
}
)
=
t
1
s
10
s
11
s
6
t
7
s
8As we saw in Section5.1, the operations previously defined for transforming a state E
1 into E
2 are completely related to the fact that φ
(
E
1
)
+
I
=
φ
(
E
2
)
+
I. Therefore, we have the following.Proposition 7.
LetE
a
,
E
b be two states. We have that (19)
E
a
→
E
b
⇔
φ
E
a
+
I
=
φ
E
b
+
ILet us clarify this proposition with the example of Figure6. In this case we have that K
=
{
t
1
+
s
1
t
2
} because the light signal represented by  indicates “proceed", thus I
=
K
+
{
t
1
+
t
1
2
,
t
2
+
t
2
2
,
s
1
+
s
1
2
}.Figure 6
Two sections connected.We can define as possible statesE
a
,
E
b
,
E
c where (20)
φ
E
a
=
t
1
+
I
t
r
a
i
n
t
1
i
s
p
l
a
c
e
d
i
n
s
1
φ
E
b
=
t
2
+
I
t
r
a
i
n
t
2
i
s
p
l
a
c
e
d
i
n
s
2
φ
E
c
=
s
1
t
2
+
I
t
1
=
s
1
t
2
b
e
c
a
u
s
e
t
1
+
s
1
t
2
∈
IState E
c is equivalent to state E
a and different from state E
b (E
a
→
E
c and E
c
→
E
a). Calculating N
F
(
φ
(
E
a
)
·
φ
(
E
b
)
) that represents two trains placed in sections s
1 and s
2 respectively, we have that (21)
N
F
φ
E
a
·
φ
E
b
=
t
1
t
2
+
I
=
s
1
t
2
t
2
+
I
t
1
=
s
1
+
t
2
b
e
c
a
u
s
e
t
1
+
s
1
t
2
∈
I
=
s
1
t
2
+
I
t
2
2
=
t
2Consequently, Proposition6 can be stated in the following way.Proposition 8.
Let us consider a railway network composed ofN sections, let M be a positive integer, M
≤
N and let {
w
1
,
w
2
,
…
,
w
M
}
⊆
{
1,2
,
…
,
N
}. The position of M trains in sections S
w
1
,
S
w
2
,
…
,
S
w
M (one in each section) is dangerous ⇔ there is a monomial p with a number of t
α variables lower than M, such that p
+
I
=
t
w
1
t
w
2
…
t
w
M
+
I.In order to find this polynomialp, we make use of N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
), the normal form of the monomial modulo the ideal I. According to Section 5.1, N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
), returns the monomial p with minimal number of t
α variables such that p
+
I
=
t
w
1
t
w
2
…
t
w
M
+
I. Consequently, we have the following result.Theorem 9.
Let us consider a railway network composed ofN sections and let M be a positive integer, M
≤
N. The position of M trains located in sections S
w
1
,
S
w
2
,
…
,
S
w
M is dangerous ⇔
N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
) contains a number of t
α variables lower than M.


## 5.1. Some Introductory Notes about Boolean Polynomials and Ideals

In this section we will describe some outlines about Boolean polynomial. A polynomialp
∈
Z
2
[
x
1
,
…
,
x
N
] is a polynomial in the variables x
1
,
…
,
x
N whose coefficients lie in the field Z
2
=
{
0,1
}. An example of this kind of polynomials is (9)
p
=
x
1
x
2
7
+
x
3
+
x
2
x
3
x
4We must take into account the fact that the coefficients lie inZ
2, and therefore, we have that (since 1+1=0 in Z
2), for example, (10)
x
1
x
2
+
x
3
x
4
+
x
3
x
4
=
x
1
x
2
+
1
+
1
x
3
x
4
=
x
1
x
2As we have previously seen, the concept of ideal will play an important role in our approach. An ideal is a special kind of subset of a ring: it is also a ring and has the curious property that the product of an element of the subring by an element of the ring (and vice versa, if the ring is not a commutative one) always belongs to the subring. For instance, the set of even numbers is an ideal of the integers. In our case, the idealJ, generated by p
1
,
…
,
p
m, denoted J
=
〈
p
1
,
…
,
p
m
〉, turns out to be the set of polynomials of the following form: (11)
β
1
p
1
+
…
+
β
m
p
mwhere β
1
,
…
,
β
N are polynomials in Z
2
[
x
1
,
…
,
x
N
], that is, J is the set of algebraic combinations of p
1
,
…
,
p
m.Given a polynomialp, we define p
+
J as the set of polynomials of the form p
+
q where q
∈
J. It is possible that p
+
J
=
q
+
J although p
≠
q.Example 3.
Let us consider the idealJ
=
x
1
+
x
2
x
3
,
x
2
+
x
3
x
4 and the polynomial p
=
x
1
x
4
+
x
2. We have that (12)
p
+
J
=
x
1
x
4
+
x
2
+
J
=
x
2
x
3
x
4
+
x
2
+
J
x
1
=
x
2
x
3
b
e
c
a
u
s
e
x
1
+
x
2
x
3
∈
J
=
x
3
2
x
4
2
+
x
2
+
J
1
s
t
o
c
u
r
r
e
n
c
e
of
x
2
=
x
3
x
4
b
e
c
a
u
s
e
x
2
+
x
3
x
4
∈
J
=
x
3
2
x
4
2
+
x
3
x
4
+
J
2
n
d
o
c
u
r
r
e
n
c
e
of
x
2
=
x
3
x
4
b
e
c
a
u
s
e
x
2
+
x
3
x
4
∈
JIn this paper, we will consider polynomials inZ
2
[
s
1
,
…
,
s
N
,
t
1
,
…
,
t
N
]. The ideal I defined in Section 4 is generated by the following polynomials:(i)
The polynomialss
i
2
+
s
i, t
i
2
+
t
i
∈
I
,
i
=
1
,
…
n,. This involves that, for every polynomial p, we can get a polynomial q such that p
+
I
=
q
+
I and the exponents of all the variables in q is 1.Example 4.
Let us consider, for example, the idealI and the polynomial p
=
s
1
2
t
2
3
+
s
1
t
2
+
s
1
3. We have that (13)
p
+
I
=
s
1
2
t
2
3
+
s
1
t
2
+
s
1
3
+
I
=
s
1
t
2
2
t
2
+
s
1
t
2
+
s
1
2
s
1
+
I
s
1
2
=
s
1
,
t
2
3
=
t
2
2
t
2
a
n
d
s
1
3
=
s
1
2
s
1
=
s
1
t
2
t
2
+
s
1
t
2
+
s
1
s
1
+
I
t
2
2
=
t
2
a
n
d
s
1
2
=
s
1
=
s
1
t
2
2
+
s
1
t
2
+
s
1
2
+
I
t
2
t
2
=
t
2
a
n
d
s
1
s
1
=
s
1
2
=
s
1
t
2
+
s
1
t
2
+
s
1
+
I
t
2
2
=
t
2
a
n
d
s
1
2
=
s
1
=
s
1
+
I
2
s
1
t
2
=
0Remember that (as we have seen before)(14)
K
=
t
i
+
s
i
t
j
∣
i
t
i
s
p
o
s
s
i
b
l
e
t
o
p
a
s
s
from
s
e
c
t
i
o
n
S
i
t
o
s
e
c
t
i
o
n
S
jand (15)
I
=
K
+
s
1
2
+
s
1
,
…
,
s
N
2
+
s
N
,
t
1
2
+
t
1
,
…
,
t
N
2
+
t
N
(ii)
The polynomialt
i
+
s
i
t
j
∈
I if it is possible to pass from section S
i to section S
j. This involves that for every monomial t
1
·
…
·
t
n we can obtain other monomials in variables t and s.Example 5.
In the example of the railway network described in Figure3, we have that p
=
t
1
t
10
t
8: (16)
p
+
I
=
t
1
t
10
t
8
+
I
=
t
1
t
10
s
8
t
7
+
I
t
8
=
s
8
t
7
b
e
c
a
u
s
e
t
8
+
s
8
t
7
∈
I
=
t
1
s
10
t
11
s
8
t
7
+
I
t
10
=
s
10
t
11
b
e
c
a
u
s
e
t
10
+
s
10
t
11
∈
I
=
t
1
s
10
s
11
t
6
s
8
t
7
+
I
t
11
=
s
11
t
6
b
e
c
a
u
s
e
t
11
+
s
11
t
6
∈
I
=
t
1
s
10
s
11
s
6
t
7
s
8
t
7
+
I
t
6
=
s
6
t
7
b
e
c
a
u
s
e
t
6
+
s
6
t
7
∈
I
=
t
1
s
10
s
11
s
6
t
7
2
s
8
+
I
t
7
t
7
=
t
7
2
=
t
1
s
10
s
11
s
6
t
7
s
8
+
I
t
7
2
=
t
7
=
t
1
s
10
s
11
s
6
t
8
+
I
s
8
t
7
=
t
8
b
e
c
a
u
s
e
t
8
+
s
8
t
7
∈
IBy means of these substitutions induced by the idealI, we can obtain, for every monomial p, another monomial q whose variables are to power 1 and such that p
+
I
=
q
+
I.An important solved issue in computer algebra is to find the “simplest” monomialq such that q
+
I
=
p
+
I. In a formal way, we pose the problem of finding the minimal polynomial q (where a total order between monomials, ⪯, must be defined) such that p
+
I
=
q
+
I. This polynomial q is what is called normal form of p modulo the ideal I (under the order ⪯), N
F
(
p
,
I
), which can be calculated by performing pseudodivisions of the polynomial p by a Groebner basis of the ideal I (which are required to be previously calculated). In this way, the concept of normal form requires defining a monomial order.For the purpose of this paper, we will define the following order between monomials:(i)
Ifp contains a lower number of t
α variables than q, we have that p
⪯
q.
(ii)
Ifp contains exactly the same number of t
α variables as q, we have that p
⪯
q
⇔
p
⪯
L
e
x
q, where ⪯
L
e
x is the typical lexicographical order used in computer algebra.By means of this order⪯, the normal form of p modulo I, N
F
(
p
,
I
), returns the monomial q with minimal number of variables in t such that p
+
I
=
q
+
I. Next equations are examples of ⪯ order used in this approach: (17)
s
3
⪯
t
1
=
T
r
u
e
t
1
⪯
s
3
=
F
a
l
s
e
t
2
⪯
t
1
=
T
r
u
e
t
1
⪯
t
2
=
F
a
l
s
e
s
1
⪯
s
2
=
F
a
l
s
e


## 5.2. An Approach to the Railway Interlocking Problem Based on States

Here we will see how the interlocking problem can be described by means of states which are transformed by means of operations. On the one hand a state describes the sections where the trains are presently placed in the railway network at a given moment; on the other one, past states describe the sections where the trains were placed in the railway network in the past. Operations of the states (i.e., transitions between states) represent possible movements of the trains in the railway network.For our purpose, each state is described by a subset of variabless
1
,
…
,
s
N, t
1
,
…
,
t
N.The following are examples of possible states of the railway network in Figure3: E
0
=
t
1
t
10
t
8
,
E
1
=
t
1
t
10
s
8
t
7
,
E
2
=
t
1
s
10
t
11
s
8
t
7,E
3
=
{
t
1
s
10
s
11
t
6
s
8
t
7
}
,
E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
t
7
}
,
E
5
=
{
t
1
s
10
s
11
s
6
t
8
}.We can transform a stateE
i into another one E
j by means of one of these operations (we will denote E
i
→
E
j):(i)
When it is possible, substitute allt
i in E
i by the monomial s
i
t
j
∈
I if it is possible to pass from S
i to S
j. For example, we have that E
0
→
E
1 (E
0
=
{
t
1
t
10
t
8
} and E
1
=
{
t
1
t
10
s
8
t
7
}) by substituting t
8 by s
8
t
7, because t
8
+
s
8
t
7
∈
I.
(ii)
When it is possible, substitute alls
i
t
j in E
i by the variable t
i
∈
I if it is possible to pass from S
i to S
j. For example, we have that E
4
→
E
5 (E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
t
7
} and E
5
=
{
t
1
s
10
s
11
s
6
t
8
}) by substituting s
8
t
7 by t
8, because t
8
+
s
8
t
7
∈
I.Variablest and s in these states inform about possible movements of the trains. Variables t indicate the present position of the trains, and variables s the sections through which these trains have gone. Indeed,(i)
the stateE
0
=
{
t
1
t
10
t
8
} represents that there are trains in the sections S
1
,
S
10, S
8 (variables t
1
,
t
10
,
t
8 appear in E
0);
(ii)
the stateE
1
=
{
t
1
t
10
s
8
t
7
} represents that there are trains in the sections S
1
,
S
7
,
S
10 (variables t
1
,
t
7
,
t
10 appear in E
1) and that (at least) one of these trains has passed through the section S
8 (variable s
8 appears in E
1);
(iii)
the stateE
2
=
{
t
1
s
10
t
11
s
8
t
7
} represents that there are trains in the sections S
1
,
S
7
,
S
11 (variables t
1
,
t
7
,
t
11 appear in E
2) and that (at least) one of these trains has passed through the sections S
8
,
S
10 (variables s
10
,
s
8 appear in E
2);
(iv)
the stateE
3
=
{
t
1
s
10
s
11
t
6
s
8
t
7
} represents that there are trains in the sections S
1
,
S
6
,
S
7 (variables t
1
,
t
6
,
t
7 appear in E
3) and that (at least) one of these trains has passed through the sections S
8
,
S
10
,
S
11 (variables s
8
,
s
10
,
s
11 appear in E
3).As may be seen, statesE
0
,
E
1
,
E
2, E
3 contain the same number of variables t representing the position of the trains in different times. However, we can transform the state E
3
=
{
t
1
s
10
s
11
t
6
s
8
t
7
} into the state E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
t
7
}
=
{
t
1
s
10
s
11
s
6
t
7
s
8
} by substituting t
6 with s
6
t
7 (the train which was in section S
6 moves to section S
7). In this case, the number of “t” variables is lower than the cardinal of E
3, since the variable t
7 (that we add with the operation) indeed belongs to the previous state E
3. The operation means that the train which was in section S
6 moves to section S
7, and, since section S
7 was occupied by another train, a possible collision may happen.Following this reasoning, we have the following.Proposition 6.
LetM be a positive integer, M
≤
N, and let {
w
1
,
w
2
,
…
,
w
M
}
⊆
{
1,2
,
…
,
N
}. The position of M trains in sections S
w
1
,
S
w
2
,
…
,
S
w
M (one in each section) is dangerous ⇔ the state E
0
=
{
t
1
…
t
M
} can be transformed into a state E
z with a number of t
α variables lower than M.In the previous example we had{
t
1
t
10
t
8
}
=
E
0
→
E
1
→
E
3
→
E
4
=
{
t
1
s
10
s
11
s
6
t
7
s
8
}. According to the previous proposition, the position of the trains in sections S
1, S
10, S
8 (related to the state E
0
=
{
t
1
t
10
t
8
}) is dangerous in the railway network (as we saw in Section 3).


## 5.3. Interpretation of States in Algebraic Terms

In this section, we will represent each of the states described in the previous section by means of a Boolean monomial. As we will see, this representation will be useful for determining whether the position of the trains is dangerous or not.We represent each stateE, a set consisting in one monomial, by means of precisely such monomial, so φ
(
E
)
∈
Z
2
[
s
1
…
,
s
N
,
t
1
…
,
t
N
], and can be expressed as follows: (18)
φ
E
=
∏
i
∈
S
^
s
i
∏
j
∈
T
^
t
jwhere S
^
,
T
^
⊆
{
1
,
…
,
N
}
∧
T
^
≠
∅. In this way, we have the following:(i)
φ
(
E
0
)
=
φ
(
{
t
1
t
10
t
8
}
)
=
t
1
t
10
t
8
(ii)
φ
(
E
1
)
=
φ
(
{
t
1
t
10
s
8
t
7
}
)
=
t
1
t
10
s
8
t
7
(iii)
φ
(
E
2
)
=
φ
(
{
t
1
s
10
t
11
s
8
t
7
}
)
=
t
1
s
10
t
11
s
8
t
7
(iv)
φ
(
E
3
)
=
φ
(
{
t
1
s
10
s
11
t
6
s
8
t
7
}
)
=
t
1
s
10
s
11
t
6
s
8
t
7
(v)
φ
(
E
4
)
=
φ
(
{
t
1
s
10
s
11
s
6
t
7
s
8
}
)
=
t
1
s
10
s
11
s
6
t
7
s
8As we saw in Section5.1, the operations previously defined for transforming a state E
1 into E
2 are completely related to the fact that φ
(
E
1
)
+
I
=
φ
(
E
2
)
+
I. Therefore, we have the following.Proposition 7.
LetE
a
,
E
b be two states. We have that (19)
E
a
→
E
b
⇔
φ
E
a
+
I
=
φ
E
b
+
ILet us clarify this proposition with the example of Figure6. In this case we have that K
=
{
t
1
+
s
1
t
2
} because the light signal represented by  indicates “proceed", thus I
=
K
+
{
t
1
+
t
1
2
,
t
2
+
t
2
2
,
s
1
+
s
1
2
}.Figure 6
Two sections connected.We can define as possible statesE
a
,
E
b
,
E
c where (20)
φ
E
a
=
t
1
+
I
t
r
a
i
n
t
1
i
s
p
l
a
c
e
d
i
n
s
1
φ
E
b
=
t
2
+
I
t
r
a
i
n
t
2
i
s
p
l
a
c
e
d
i
n
s
2
φ
E
c
=
s
1
t
2
+
I
t
1
=
s
1
t
2
b
e
c
a
u
s
e
t
1
+
s
1
t
2
∈
IState E
c is equivalent to state E
a and different from state E
b (E
a
→
E
c and E
c
→
E
a). Calculating N
F
(
φ
(
E
a
)
·
φ
(
E
b
)
) that represents two trains placed in sections s
1 and s
2 respectively, we have that (21)
N
F
φ
E
a
·
φ
E
b
=
t
1
t
2
+
I
=
s
1
t
2
t
2
+
I
t
1
=
s
1
+
t
2
b
e
c
a
u
s
e
t
1
+
s
1
t
2
∈
I
=
s
1
t
2
+
I
t
2
2
=
t
2Consequently, Proposition6 can be stated in the following way.Proposition 8.
Let us consider a railway network composed ofN sections, let M be a positive integer, M
≤
N and let {
w
1
,
w
2
,
…
,
w
M
}
⊆
{
1,2
,
…
,
N
}. The position of M trains in sections S
w
1
,
S
w
2
,
…
,
S
w
M (one in each section) is dangerous ⇔ there is a monomial p with a number of t
α variables lower than M, such that p
+
I
=
t
w
1
t
w
2
…
t
w
M
+
I.In order to find this polynomialp, we make use of N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
), the normal form of the monomial modulo the ideal I. According to Section 5.1, N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
), returns the monomial p with minimal number of t
α variables such that p
+
I
=
t
w
1
t
w
2
…
t
w
M
+
I. Consequently, we have the following result.Theorem 9.
Let us consider a railway network composed ofN sections and let M be a positive integer, M
≤
N. The position of M trains located in sections S
w
1
,
S
w
2
,
…
,
S
w
M is dangerous ⇔
N
F
(
t
w
1
t
w
2
…
t
w
M
,
I
) contains a number of t
α variables lower than M.


## 6. Evaluation and Discussion

In this section, we will analyze the performance of the approach presented here, comparing it with other techniques with available implementations. Indeed, we have made a comparison between the times required to calculate the safety of the railway network with differentN sections and M trains. All experiments have been carried out on the same computer.


### 6.1. Comparing the Performances of the Logic, Algebraic, and Logic-Algebraic Models

In Table1, a comparison between the times required to calculate the safety of certain railway networks in different situations using different models is shown. The Logic [28], Algebraic [24], and Logic-Algebraic [30] models were implemented in the computer algebra systemMaple.Table 1
Time comparative of methods implemented in for detecting the safety in a railway interlocking system withN sections and M trains.
M
=
15
N
=
32
M
=
15
N
=
64
M
=
45
N
=
93
M
=
60
N
=
127
M
=
65
N
=
160
M
=
105
N
=
224
Logic
10.23 s
250.250 s
>
1 h
>
1
h
>
1h
>
1h
Algebraic
15.356 s
380.368 s
>
1 h
>
1
h
>
1h
>
1h
Logic-Algebraic
0.005 s
0.060 s
1.1 s
3.348 s
10.323 s
38.392 sWe can state that these three models are strongly dependent on the number of sections and trains. From the experiments carried out (and as can be seen in the first two columns of Table 1), we can affirm that timings grow very quickly with the number of sections. The timings obtained make it clear that these models are not appropriate for middle size or large size railway networks.Regarding the influence of the number of trains on timings, they grow quickly both in the Logic and Logic-Algebraic models. In the Algebraic Model, the polynomial variable corresponding to the section is substituted by an integer number when a train is declared to be in a certain section. Therefore more trains mean less variables in the Groebner basis. So, curiously, if the number of sections is fixed, timings decrease if the number of trains increases. In the degenerated case of one different train in each section, we would have time to be equal to 0 in the Groebner basis computation, as there is no variable left.


### 6.2. Comparing the Performances of the ASP and the New Model

Meanwhile, the ASP model [31] and the new proposed model can be applied to large railway networks. We have used as example for the benchmarks Madrid Chamartin station in its state prior to the transformation of some of its tracks into international gauge [33], with 300 sections and more than 200 turnouts and light signals.The ASP model was implemented inSmodels. Finally, the model introduced in this article has been implemented inPolyBoRi [32], an specialized software to calculate Groebner bases and normal forms on Boolean rings. Table 2 shows the times obtained considering different numbers of trains (Times inSmodels are calculated taking into account thelparse andsmodels executions. We apply the same rule inPolyBoRi.).Table 2
Time comparative between the ASP model and the new model, with300 sections and M
=
5,15,30 trains.
M
=
5
N
=
300
M
=
15
N
=
300
M
=
30
N
=
300
ASP
0.646s
0.716s
0.799s
New model (GB preprocess)
2.3s
2.3s
2.3s
New model (NF)
0.0001s
0.00039s
0.0054sThe main results from Table2 are, one the one hand, that the efficiency of our method is always high superior to the other approaches tested when the GB is previously calculated; on the other hand, the time to calculate the GB is reasonably fast (e.g., ~
2.3
s for Chamartin Station), providing very competitive times for large networks. Moreover, the Groebner bases computed in the preprocess step can be stored and used in case the same situation is proposed again. Let us observe that our two steps method connects somehow with the traditional methods that check the compatible routes in advance.In our approach, computation timings for the Groebner bases preprocess grow when the number of sections increases (as happens in all the other models).But, unlike the other approaches, ours does not need to perform all the calculations for the different positions of the trains for a given specific particular state of the turnouts and light signals. Indeed, we only need to calculate the normal form of one monomial (once the Groebner basis is calculated for this particular state of turnouts and light signals), as detailed in Theorem9. The time for calculating this normal form grows with the number of trains, as can be seen in Table 2. Nevertheless, these timings of this second step have always been negligible (lower than 0.01s in all the experiments carried out, regardless of the size of the railway network or the number of trains).On the contrary, the other approaches require to recalculate all the computations.


### 6.3. Comparison: Final Remarks

The approach presented in this paper only focuses on the safeness of the proposed situation; meanwhile other approaches like [23, 34] also consider other properties such as reachability of sections or the situation of the switches of the turnouts under a train (that shouldn’t be changed under any circumstance to avoid derailments due to a premature change of the switch during the transit of the train). Another issue not treated in our model is the confirmation that the switches of the turnouts and the light signals have really been set to the ordered situation (something considered, for instance, in [34]; this latter approach uses a real-time system, a flexible approach with a wide variety of applications [21]).On the other hand, our new approach can handle really big layouts (like the one in the example of Table1, with, as said above, 300 sections and more than 200 turnouts and light signals, what is a far bigger layout than any one that we have found treated in real time). For instance, the authors of [34] mention that “our study is unique in the fact that modeling and verification of mid to large size railway yard is being undertaken in UPPAAL model checker (…)” and the example presented (Rawalpindi Cantt station) has 25 semaphores and 27 mechanically operated points.


## 6.1. Comparing the Performances of the Logic, Algebraic, and Logic-Algebraic Models

In Table1, a comparison between the times required to calculate the safety of certain railway networks in different situations using different models is shown. The Logic [28], Algebraic [24], and Logic-Algebraic [30] models were implemented in the computer algebra systemMaple.Table 1
Time comparative of methods implemented in for detecting the safety in a railway interlocking system withN sections and M trains.
M
=
15
N
=
32
M
=
15
N
=
64
M
=
45
N
=
93
M
=
60
N
=
127
M
=
65
N
=
160
M
=
105
N
=
224
Logic
10.23 s
250.250 s
>
1 h
>
1
h
>
1h
>
1h
Algebraic
15.356 s
380.368 s
>
1 h
>
1
h
>
1h
>
1h
Logic-Algebraic
0.005 s
0.060 s
1.1 s
3.348 s
10.323 s
38.392 sWe can state that these three models are strongly dependent on the number of sections and trains. From the experiments carried out (and as can be seen in the first two columns of Table 1), we can affirm that timings grow very quickly with the number of sections. The timings obtained make it clear that these models are not appropriate for middle size or large size railway networks.Regarding the influence of the number of trains on timings, they grow quickly both in the Logic and Logic-Algebraic models. In the Algebraic Model, the polynomial variable corresponding to the section is substituted by an integer number when a train is declared to be in a certain section. Therefore more trains mean less variables in the Groebner basis. So, curiously, if the number of sections is fixed, timings decrease if the number of trains increases. In the degenerated case of one different train in each section, we would have time to be equal to 0 in the Groebner basis computation, as there is no variable left.


## 6.2. Comparing the Performances of the ASP and the New Model

Meanwhile, the ASP model [31] and the new proposed model can be applied to large railway networks. We have used as example for the benchmarks Madrid Chamartin station in its state prior to the transformation of some of its tracks into international gauge [33], with 300 sections and more than 200 turnouts and light signals.The ASP model was implemented inSmodels. Finally, the model introduced in this article has been implemented inPolyBoRi [32], an specialized software to calculate Groebner bases and normal forms on Boolean rings. Table 2 shows the times obtained considering different numbers of trains (Times inSmodels are calculated taking into account thelparse andsmodels executions. We apply the same rule inPolyBoRi.).Table 2
Time comparative between the ASP model and the new model, with300 sections and M
=
5,15,30 trains.
M
=
5
N
=
300
M
=
15
N
=
300
M
=
30
N
=
300
ASP
0.646s
0.716s
0.799s
New model (GB preprocess)
2.3s
2.3s
2.3s
New model (NF)
0.0001s
0.00039s
0.0054sThe main results from Table2 are, one the one hand, that the efficiency of our method is always high superior to the other approaches tested when the GB is previously calculated; on the other hand, the time to calculate the GB is reasonably fast (e.g., ~
2.3
s for Chamartin Station), providing very competitive times for large networks. Moreover, the Groebner bases computed in the preprocess step can be stored and used in case the same situation is proposed again. Let us observe that our two steps method connects somehow with the traditional methods that check the compatible routes in advance.In our approach, computation timings for the Groebner bases preprocess grow when the number of sections increases (as happens in all the other models).But, unlike the other approaches, ours does not need to perform all the calculations for the different positions of the trains for a given specific particular state of the turnouts and light signals. Indeed, we only need to calculate the normal form of one monomial (once the Groebner basis is calculated for this particular state of turnouts and light signals), as detailed in Theorem9. The time for calculating this normal form grows with the number of trains, as can be seen in Table 2. Nevertheless, these timings of this second step have always been negligible (lower than 0.01s in all the experiments carried out, regardless of the size of the railway network or the number of trains).On the contrary, the other approaches require to recalculate all the computations.


## 6.3. Comparison: Final Remarks

The approach presented in this paper only focuses on the safeness of the proposed situation; meanwhile other approaches like [23, 34] also consider other properties such as reachability of sections or the situation of the switches of the turnouts under a train (that shouldn’t be changed under any circumstance to avoid derailments due to a premature change of the switch during the transit of the train). Another issue not treated in our model is the confirmation that the switches of the turnouts and the light signals have really been set to the ordered situation (something considered, for instance, in [34]; this latter approach uses a real-time system, a flexible approach with a wide variety of applications [21]).On the other hand, our new approach can handle really big layouts (like the one in the example of Table1, with, as said above, 300 sections and more than 200 turnouts and light signals, what is a far bigger layout than any one that we have found treated in real time). For instance, the authors of [34] mention that “our study is unique in the fact that modeling and verification of mid to large size railway yard is being undertaken in UPPAAL model checker (…)” and the example presented (Rawalpindi Cantt station) has 25 semaphores and 27 mechanically operated points.


## 7. Model Extension for Trains Occupying Several Sections at the Same Time

Two trains are represented in Figure7, one placed on section S
10 and another one placed on sections S
1
,
S
2 at the same time. It is common to find these situations in a real railway when several trains can occupied several sections at the same time.Figure 7
Possible situation of trains occupy several sections at the same time. The situation is safe.In order to check the safety of a railway network withM trains that can occupy several sections at the same time, we will redefine Step 3 of Section 4 as follows.Step 3.1. As long as E represents the sections occupied by a given train T, we calculate N
F
(
φ
(
E
)
,
I
)
=
E
′. E
′ is a reduced initial state representing the sections occupied by a train.Step 3.2. Once M initial states E
1
′
,
…
,
E
M
′ have been calculated, we calculate the joint state E
′
′ which φ
(
E
′
′
)
=
N
F
(
φ
(
E
1
′
)
·
…
·
φ
(
E
M
′
)
,
I
) of all initial states.Step 3.3. For determining if the position of M trains with initial states E
1
′
,
…
,
E
M
′ is dangerous, we need to check if (22)
∑
i
=
1
M
η
E
i
′
>
η
E
′
′whereη
(
E
)
→
N is a function that returns the number of t
α variables in the monomial φ
(
E
).Example 10.
As example, the safety of the railway network on Figure7 will be checked.
Step 3.1. The first train is represented by E
1
=
{
t
1
t
2
} and the second one is represented by E
2
=
{
t
11
}. Therefore, the initial train states will be (23)
E
1
′
=
N
F
t
1
t
2
,
I
=
t
4
s
3
E
2
′
=
N
F
t
10
,
I
=
t
11
Step 3.2. Joint calculations of all initial states are (24)
E
′
′
=
N
F
φ
E
1
′
·
φ
E
2
′
,
I
=
t
4
t
11
Step 3.3. Check the number of variables t in both monomials: (25)
η
E
1
′
+
η
E
2
′
=
η
E
′
′
=
2so we have that the proposed situation of the trains on Figure 7 is safe.Example 11.
Let us propose another example where the situation in the railway network is dangerous. Figure8 represents two trains, one located in S
10 and another one located on S
6
,
S
7
,
S
8. In order to check if exists a dangerous situation, we will calculate the following.
Step 3.1. The first train is represented by E
1
=
{
t
10
} and the second one is represented by E
2
=
{
t
6
t
7
t
8
}. Therefore, the initial train states will be as follows: (26)
E
1
′
=
N
F
t
10
,
I
=
t
11
E
2
′
=
N
F
t
6
t
7
t
8
,
I
=
t
11
Step 3.2. Joint calculations of all initial states are(27)
E
′
′
=
N
F
φ
E
1
′
·
φ
E
2
′
,
I
=
t
11
,
Step 3.3. Check the number of variables t in both monomials: (28)
η
E
1
′
+
η
E
2
′
>
η
E
′
′So we have that the proposed situation of the trains on Figure 8 is dangerous.Figure 8
Possible situation of trains occupying several sections at the same time. The situation is dangerous.


## 8. Conclusions

In this paper we have presented a new algebraic model for railway interlocking systems. According to this new model, the position of the trains in a railway network is dangerous if and only if the normal form of a certain monomial (representing the present position of the trains) contains a lower number oft
α variables than the number of trains in the railway network. We have implemented this model on the computer algebra systemPolyBoRi resulting in a very short program code. Moreover, we have compared the execution times with other very fast models implemented previously.



---

*Source: 4982974-2018-10-01.xml*