An interlocking system determining the configuration of rail traffic control elements to ensure safety

1.   Introduction

Rail transport serves as a key component in global transportation networks, offering a dependable and effective means for the movement of both commodities and passengers across extensive distances. Insights from research on the robustness of rail transport systems highlight its significance as an essential infrastructure, underpinning both economic and societal functions. 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 Systems are a crucial component of railway signalling. These systems consist of a set of signalling devices that prevent conflicting movements among trains. They ensure that trains are only granted authority to proceed when the routes have been set, locked, and detected to be clear of other trains. This intricate system plays a vital role in maintaining the safety and efficiency of rail traffic.

These systems are designed with the foremost goal of minimizing human mistakes and guaranteeing a 'fail-safe' condition in case of malfunctions, thereby averting any potential hazards. This objective is accomplished via an intricate array of signals and switches that collectively manage the locomotion of trains. The signals serve to inform whether a track is available or in use, and the switches determine the trajectory of the train.

Pachl's work offers a comprehensive guide to the principles of railway signaling ^[3]. Traditional interlocking systems in railways, which are established based on predetermined routes, often rely on human expertise for route compatibility decisions ^[4]. Despite this, historical instances have revealed significant flaws within these systems ^[5]. In contrast, contemporary interlocking systems boast the capability to adapt dynamically, enhancing flexibility as they are not confined to fixed routes. Nonetheless, it is imperative to verify that any alterations to signals or switch positions do not result in intersecting paths for trains, which could lead to collisions. Absent this assurance, modifications are withheld, potentially necessitating a delay until a train departs the station. The genesis of railway interlocking can be traced back to the 19th century, characterized by intricate mechanical constructs composed of levers and bars. By the mid-20th century, the advent of electric relays necessitated complex electrical circuitry to mirror the station's layout. The 1980s marked the debut of computerized control in railway interlocking systems ^[6,7,8,9], with Spain pioneering its first geographical railway interlocking system in 1993 ^[10].

The intricate nature and critical significance of Railway Interlocking Systems render them an intriguing area for ongoing research and enhancement. Progress in technological capabilities has seen these systems transition from mechanical to electrical, and presently to computer-operated frameworks. Each stage of this evolution has contributed to heightened efficiency, dependability, and safety standards. Nonetheless, such progress is not without its hurdles. The assimilation of novel technologies demands meticulous attention to ensure they mesh seamlessly with the pre-existing structures. Moreover, the escalating complexity of these systems inherently raises the risk of malfunctions. Consequently, persistent research and development are imperative to perpetuate the advancement of safety and operational efficiency in Railway Interlocking Systems.

Contemporary railway interlocking systems universally employ computerization, whether they are geographically oriented or route-based. Simple versions of geographical algorithms can encounter issues with exponential complexity, significantly impacting the time required to identify secure routes within the rail network. Studies have explored efficient data validation techniques for these systems ^[11]. Model checking, particularly with UMC, offers another method for validating geographically dispersed interlocking systems ^[12]. Diverse strategies have been utilized in the decision-making processes of railway interlocking, including, albeit somewhat outdated, a comprehensive annotated bibliography by Bjorner ^[13]. The complexity of this issue has spurred extensive research, with recent investigations focusing on artificial intelligence for fault detection ^[14] and comparing various safety verification techniques ^[15]. There have also been developments in formal model-based methods to aid engineers in defining and confirming the specifications of interlocking systems ^[16]. Morley's research employs a theorem prover based on higher-order logic for safety assessments ^[17], while Nakamatsu revisits this using temporal logic in annotated logic programs ^[18]. Winter's work utilizes ordered binary decision diagrams for modeling interlocking systems ^[4]. Notably, Janota's study for the Slovak National Railways employs Z notation^[19], and Hansen's for the Danish State Railways uses the Vienna Development Method^[20]. Montigel introduces an advanced early model capable of handling complex railway topologies, implemented using Petri nets, graphs, Objective-C, and PROLOG ^[21]. Yulin's component-based model represents the station as interconnected components ^[22,23,24]. Luteberget integrates CAD, RailML, and logic programming for application in Norwegian railway stations ^[25], and a Dutch station's topology is articulated using RailML alongside UML class diagrams in another notable study ^[26].

Over the years, authors have developed various models to study this problem ^{[27,28,29,30,31,32]}. Some of these models are based on polynomials, ideals, and Groebner bases ^[33], similar to those used in Artificial Intelligence for implementing expert systems ^[34]. This approach bridges computational algebra and interlocking problems, suggesting that computer algebra systems can be used to implement interlocking systems.

Recently, a groundbreaking algebraic model was unveiled ^[35] that improves the implementation of interlocking systems. This model provides a linear algorithm that significantly outperforms previous models and is suitable for large-scale railway stations. However this model determines only whether a situation is dangerous or not, in case that the situation is dangerous, this model does not provide any guide on how to configure certain rail traffic control elements to ensure safety. In this paper, we will extend this model to include this capacity.

The paper is structured as follows. In Section 2, we outline the contributions of the present model in comparison to the one presented in ^[35]. In Section 3, we outline the approach of this paper. In Section 4, we present formal concepts of the interlocking systems and the problem we will focus on. In Section 5.1, we translate previous concepts into an algebraic model. In Section 6, we demonstrate how an interlocking system based on our model can be implemented by means of a Computer Algebra System. In Section 7, we provide our conclusions.

2.   Contribution of our model

Let us examine a case study involving interlocking systems to underscore the significance of our paper and demonstrate the advantages of our proposed model.

Consider the railway station depicted in Figure 1, comprising eight sections (S1 to S8), two turnouts (D1 and D2), and eight traffic light signals (L1 to L8). This station is equipped with an interlocking system designed to detect the dangerous situation: the possibility of two trains colliding within the station's confines. In our prior research, detailed in ^[35], we introduced an algebraic model adept at swiftly identifying potential dangerous scenarios, proving especially effective for larger stations. The implementation of such systems is vital for maintaining safety within the railway station.

For illustration, let us consider the scenario presented in the railway station shown in Figure 2. Here, two trains are positioned—one in section S1 and the other in section S10. The traffic light signals, labelled as $\texttt{L2}$ and $\texttt{L4}$, are set to red, while the rest display green. Moreover, the turnout switch $\texttt{D1}$ is adjusted to the diverging track setting, and the switch for turnout $\texttt{D2}$ is in the straight track position. The pressing concern is the potential collision between the train in section S1 and the one in S10. Specifically, the train in S1 could traverse from S1 to S10 via sections S2 and S9. Consequently, this scenario poses a hazard, necessitating modifications to the railway traffic control components—we must alter either the signal colors or the turnout positions.

However, when faced with a dangerous situation like this, it falls upon an expert to configure certain control elements to ensure safety. The model proposed in ^[35] does not explicitly identify which control elements need adjustment. While we can simulate the situation to assess its danger level after making changes, this process can become cumbersome for large stations. In this paper, we aim to streamline this manual and tedious task by introducing a new algebraic model. Unlike previous models ^{[27,28,29,30,31,32,35]}, our approach not only detects dangerous situations but also provides specific information on which rail traffic control elements must be modified to restore safety.

To achieve this, we need to create a new model that addresses the problem. Although the model presented in this manuscript significantly differs from a previous one, we will build upon the groundwork laid by the earlier model described in ^[35]. Leveraging many of the results demonstrated in the previous paper, we will extend our new model to determine precisely which control elements must be modified to ensure a safe situation.

The model presented in this paper shares several key points with the previous work described in ^[35]:

● Both models are algebraic, representing the situation in the railway station using polynomials.

● Both models allow us to determine whether a situation is safe by calculating the remainder of polynomial division against a list of polynomials.

● The fact that this model represents the railway station and train positions similarly to the approach in ^[35] enables us to leverage many of the results from that previous model for the current one.

Although the current model builds upon the previous one and shares some characteristics, it represents a substantial departure from its predecessor, particularly from a mathematical perspective:

● In the previous model, there was no explicit representation of control elements. Polynomials were not associated with turnouts or traffic signals. This limitation prevented the model from determining which control elements needed adjustment.

● The current model allows us to determine the configuration of control elements to ensure safety, whereas the previous model did not provide this capability.

● While the previous model calculated the remainder of dividing a monomial by a list of polynomials, the current model requires dividing a polynomial (with multiple monomials) by that same list of polynomials.

● The representation of the railway station's configuration differs from the approach described in ^[35]. Here, we explicitly consider control element configurations using polynomials, whereas the previous model represented them through a monomial, losing information about potential control element configurations.

In the current version of the paper, there are no sections duplicated from the work cited as ^[35]. We have retained its framework, but every theorem and proposition presented here is original to this paper and was not stated in ^[35].

3.   Overview

The methodology we present here provides a mathematical framework for assessing whether a situation at a railway station is dangerous, and if so, offers guidance on how to configure certain rail traffic control elements to ensure safety. Our approach is based on the following steps:

(1). Representation of the Railway Station in algebraic terms: we define a polynomial ring is several variables, denoted as $\mathcal{A}'$, and a list $\mathcal{E}$ of polynomials in this ring $\mathcal{A}$'.

(2). Representation of a situation in the railway station in algebraic terms: for each situation at the railway station, we will define a monomial $q \in \mathcal{A}'$ that represents the placement of the trains within the railway station, and a polynomial $p_f\in\mathcal{A}'$ that represents the configuration of the rail traffic control elements at the station.

(3). Identification of dangerous situations: we can verify if a situation is dangerous by checking if ${\rm{NR}}(p_fq, \mathcal{E})$ is zero, where ${\rm{NR}}$ is the remainder of dividing a polynomial over a set of polynomials.

(4). Safety assurance through the configuration of some traffic control elements. If a situation is identified as dangerous, our system provides guidance on how to adjust certain control elements to ensure safety. This is done by updating the polynomial $p_f$, which encodes the control elements that we allow to change. We then recalculate the polynomial ${\rm{NR}}(p_fq, \mathcal{E})$ and analyze its monomials, as they encode all the possible configurations that can ensure safety.

4.   Mathematical framework

4.1.   Determined configurations

A railway station is characterized by a finite set of sections $\{S_1\ldots S_n\}$ and a set of rail traffic control elements (traffic lights and turnouts) that physically connect these sections. These connections enable us to define a binary relation $E$, defined in ^[35]:

Definition 4.1. Given a railway station, we define the set $E\subset \mathbb{Z}\times\mathbb{Z}$ as follows:

This relation indicates whether there is a physical connection between two sections. Figure 1 provides an illustration of a railway station with $11$ sections, where the set $E$ is defined as follows:

As observed, $(1, 2)\in E$ signifies that $S_1$ is connected to $S_2$. However, it is crucial to note that the presence $(1, 2)\in E$ does not necessarily imply that a train can always transition from section $S_1$ to section $S_2$, as it depends on the indication of the color light signal L1.

Railway stations incorporate rail traffic control elements to determine whether one section is accessible from another. These control elements fall into two categories: Color light signals which regulate train movements, and turnouts, which faciliate the switching of trains from one track to another. As can be seen, the railway station depicted in Figure 1 is equipped with eight color light signals and two turnouts. The following definition formalizes the concept of rail traffic control elements and their states within a railway station.

Definition 4.2. A rail traffic control element within a railway station can be categorized into two types

● A color light signal $L$, represented as a pair of sections $(S_i, S_j)$.

● A turnout $D$, represented as a triple $(S_i, S_j, S_k)$.

The set of these rail traffic control elements is symbolized by $\mathcal{X}$.

Each control element possesses two states, denoted by 1 or 2. Specifically,

● For a color light signal, the color green is represented by 1, while the color red is represented by 2.

● For a turnout, the straight track position of the switch is represented by 1, and the diverted track position of the switch is represented by 2.

In Figure 1, the rail traffic control elements are:

The state of the rail traffic control elements determines a configuration of the railway station. Formally, a determined configuration is defined as a function $g:\mathcal{X} \to \{1, 2\}$.

Definition 4.3. A determined configuration of the railway station is defined as a function:

The determined configuration $g$ for the situation depicted in Figure 2 is:

$g(\text{L1}) = g(\text{L5}) = g(\text{L6}) = g(\text{L7}) = g(\text{L8}) = 1$

$g(\text{L2}) = g(\text{L3}) = g(\text{L4}) = 2$

$g(\text{D1}) = 2$

$g(\text{D2}) = 1$

Given $g$, a determined configuration of the railway station, we define the relation $P_g$ for this configuration $g$. This relation indicates whether a train can transition from one section to another connected to it.

Definition 4.4. Given a determined configuration, $g$, we define the set $P_g\subset E$ as:

Figure 2 depicts a possible configuration of the railway station. As can be observed, since the switch of the turnout connecting sections $S_2$, $S_3$ and $S_9$ is in the diverted track position, it follows that $(2, 3)\not \in P_g$ and $(2, 9) \in P_g$.

There are certain pairs of sections $(S_i, S_j)$ that belong to $P_g$ for all determined configurations. For instance in Figure 2, a train can always transition from section $S_2$ to section $S_1$. We define the set of these pairs as:

Definition 4.5.

In the situation depicted in Figure 1, we have that:

By definition, $P_F\subseteq P_g$ for any determined configuration $g$ of the railway station. The remaining elements in $P_g$ are dictated by the state of the turnouts and the color light signals in the determined configuration $g$. We can formally express this as follows:

Definition 4.6. Given a rail traffic control element $x$ and a determined configuration $g:\mathcal{X}\to\{1, 2\}$, we have that:

● if $x = (S_i, S_j)$ is a color light signal and $g(x) = 1$ (the color is green), then:

● if $x = (S_i, S_j)$ is a color light signal and $g(x) = 2$ (the color is red), then:

● if $x = (S_i, S_j, S_k)$ is a turnout and $g(x) = 1$ (the switch is in the straight track position), then:

● if $x = (S_i, S_j, S_k)$ is a turnout and $g(x) = 2$ (the switch is in the diverted track position), then:

In Proposition 4.1, we introduce a proposition that allows for the explicit computation of the set $P_g$ given the configuration $g$.

Proposition 4.1. Let $g$ be a determined configuration. We have that:

Proof. This is an immediate consequence of Definition 4.4, Definition 4.5 and Definition 4.6. □

In the situation depicted in Figure 2, we have that:

Trains may be positioned in various sections of the railway station. As multiple trains may occupy the same section, we will utilize a multiset $Q$ to represent the information regarding the placement of the trains within the station.

Definition 4.7. 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$.

In the scenario depicted in Figure 2, we have $\{1, 10\}$ because one train is in section $S_1$ and another in section $S_{10}$.

Given a set $P_g$ and a multiset $Q$, we can formulate the problem of determining whether the situation is dangerous or not^*. In other words, we can assess if there is a possibility of two trains in the railway station colliding given the determined configuration $g$.

*The pair $(P_g, Q)$ is referred to as an Interlocking Problem, which is resolved algebraically using a linear algorithm ^[35].

4.2.   Undefined configurations

In this paper, we will focus on the broader issue of determining the state of a subset of rail traffic control elements to ensure safety. Specifically, we will set the state of some rail traffic control elements, while exploring the possibility of discovering the state of others. In the previous section we defined a determined configuration as a situation where the state of every rail traffic control element is fixed. For our purposes, we will employ an undefined configuration to represent scenarios where some of the rail traffic control elements' states need to be discovered.

Definition 4.8. An undefined configuration is a function:

Figure 3 depicts the concept under discussion: the states of traffic lights L1 and L4 are not determined, and our objective is to ascertain their states to ensure safety. The undefined configuration corresponding to this figure is as follows:

$f(\text{L1}) = f(\text{L4}) = 0$

$f(\text{L5}) = f(\text{L6}) = f(\text{L7}) = f(\text{L8}) = 1$; $f(\text{L2}) = f(\text{L3}) = 2$; $f(\text{D1}) = 2$; $f(\text{D2}) = 1$

Given an undefined configuration, $f$ we can identify those rail traffic control elements whose states we aim to ascertain for safety, as they are mapped to 0 by $f$. Formally, we define the set $U_f$ as follows:

Definition 4.9. Given an undefined configuration $f:\mathcal{X}\to \{0, 1, 2\}$, we define the set $U_f$, as:

In Figure 3 we find that $U_f = \{\text{L1, L4}\}$.

Given $f$, an undefined configuration, a determined configuration $g$ is derived from it by setting the states of the rail traffic control elements in $U_f$. We define a potential configuration of $f$ as follows:

Definition 4.10. Given an undefined configuration $f:\mathcal{X}\to\{0, 1, 2\}$, a potential configuration of $f$ is is a determined configuration $g:\mathcal{X} \to \{1, 2\}$ such that for every $x\in\mathcal{X}$ where $f(x)\in\{1, 2\}$ it holds that $g(x) = f(x)$.

We denote $\mathcal{P}_f$ as the set of potential configurations of $f$. Among all potential configurations, our goal is to identify those that are safe. We denote $\mathcal{S}_f$ as the set of potential configurations of $f$ that are safe.

Given an undefined configuration $f$, and a multiset $Q$ that denotes the placement of trains, our aim of this paper is to identify the set $\mathcal{S}_f$. As we will explore in Section 5.3 we will compute a polynomial whose monomials encode all the elements in the set $\mathcal{S}_f$ (refer to Theorem 5.1)

In the case illustrated in Figure 3, it is clear that if L1 and L4 are red, the situation is safe. Consequently, a safe potential configuration, $g$, is:

$g(\text{L1}) = g(\text{L4}) = 2$

$g(\text{L5}) = g(\text{L6}) = g(\text{L7}) = g(\text{L8}) = 1$; $g(\text{L2}) = g(\text{L3}) = 2$; $g(\text{D1}) = 2$; $g(\text{D2}) = 1$

Figure 4 presents another undefined configuration in which we also aim to ascertain the state of the switch of the turnout D1.

In this case, the undefined configuration, $f$, is as follows:

$f(\text{L1}) = f(\text{L4}) = f(\text{D1}) = 0$

$f(\text{L5}) = f(\text{L6}) = f(\text{L7}) = f(\text{L8}) = 1$; $f(\text{L2}) = f(\text{L3}) = 2$; $f(\text{D2}) = 1$

There are several potential configurations of $f$ that are safe (indeed, there are exactly five possibilities as we will see in Section 6). Two of these are:

L1 and L4 are set to green and D1 is set to the straight track position. That is to say,

$g_1(\text{L1}) = g_1(\text{L4}) = 1; g_1(\text{D1}) = 1;$

$g_1(\text{L5}) = g_1(\text{L6}) = g_1(\text{L7}) = g_1(\text{L8}) = 1; g_1(\text{L2}) = g_1(\text{L3}) = 2$; $g_1(\text{D2}) = 1$

L1 is set to green, L4 is set to red and D1 is set to the straight track position. That is to say,

$g_2(\text{L1}) = 1; g_2(\text{L4}) = 2; g_2(\text{D1}) = 1;$

$g_2(\text{L5}) = g_2(\text{L6}) = g_2(\text{L7}) = g_2(\text{L8}) = 1$; $g_2(\text{L2}) = g_2(\text{L3}) = 2$; $g_2(\text{D2}) = 1$

5.   Algebraic representation

In this section, we will express the problem of determining $\mathcal{S}_f$ for any undefined configuration $f$ and any multiset $Q$ in algebraic terms. Specifically, we will represent the railway station using a list of polynomials in a ring $\mathcal{A}'$ (refer to Section 5.1). In Section 5.2 we will represent a specific situation within this railway station using a monomial $q$ (see Definition 4.7) and a polynomial $p_f$ (see Definition 4.5). Finally, in Section 5.3, we will present our main theorem 5.1, which states that the set $\mathcal{S}_f$ is encoded in the monomials of the polynomial obtained by the expression ${\rm{NR}}(p_fq, \mathcal{E}$).

5.1.   Representing the railway station

Let us consider a railway station characterized by the set of sections $\{S_1\ldots S_n\}$, a set of rail traffic control elements $X = \{x_1\ldots x_k\}$ and the relation $E$ representing the potential connectivity of the railway station. We will depict the railway station using a list of polynomials with the following variables:

● $t_i$. For each section $S_i$ in the railway station, we consider a variable $t_i$.

● $l_{ij}, m_{ij}$. For each pair of sections $S_i$ and $S_j$ where $(i, j)\in E$, we w consider two variables $l_{ij}$ and $m_{ij}$. In other words, we consider the variables $l_{ij}$ and $m_{ij}$ if the station's topology allows passage from section $S_i$ to section $S_j$ under configuration of the railway station.

● $z_{x, 1}, z_{x, 2}$: For each rail traffic control element, $x$, we consider two variables $z_{x, 1}$ and $z_{x, 2}$.

In ^[35] we considered the polynomial ring:

with the lexicographical order given by $l_{ij} > m_{ij} > t_i$. Here we will extend the aforementioned polynomial ring to:

with the lexicographical order given by $z_{x, 1} > z_{x, 2} > l_{ij} > m_{ij} > t_i$. Next, we will define a list $\mathcal{E}$ of polynomials representing the potential connectivity of the railway station. These polynomials are the same as the ones defined in the model proposed in ^[35], which serves as our starting point. Their application and underlying intuition necessitate comprehensive explanations that are beyond the scope of this paper, and we direct readers to that paper for an in-depth mathematical understanding of their role in $\mathcal{E}$, which is essential for the model's functionality:

Definition 5.1. Given $E$ (see Definition 4.1), the list of polynomials $\mathcal{E}$ representing the railway station is composed of polynomials in $\mathcal{A}'$ as follows:

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

● For each variable $t_i$:

In the railway station depicted in Figure 1, we have that:

5.2.   Representing situations within the railway station

Like in ^[35], we will depict a situation with the railway station using a monomial $q\in\mathcal{A}'$ to represent the multiset $Q$ and a polynomial $p_f\in\mathcal{A}'$ to represent any undefined configuration $f$.

For the multiset $Q$, we have {( like in ^[35])}:

Definition 5.2. Given $Q$ (see Definition 4.7), we define the monomial $q$ as:

The definition of the set $P_g$ is more intricate: initially, we will assign a monomial to each rail traffic control element (see Definition 5.3); subsequently, we will utilize the monomial of each control element to assign a monomial to any undefined configuration of the railway station (see Definition 5.5).

Definition 5.3. Given $x\in \mathcal{X}$, we define $p_x:\{0, 1, 2\}\to \mathcal{A}$':

The monomial $p_F$ is allocated to the set $P_F$ (see Definition 4.5).

Definition 5.4. We define the monomial $p_F$ as:

Definition 5.5. Given an undefined configuration $f:\mathcal{X}\to\{0, 1, 2\}$, we define:

In the special case where the undefined configuration $f$ is a determined configuration, we can readily define $p_f$ via the set $P_f$ (see Definition 4.4).

Proposition 5.1. Let $g$ be a determined configuration. Let $P_g$ be the set defined according to Definition 4.4. We have that $p_g$ is:

Proof. This is an immediate consequence of Proposition 4.1, Definition 5.3, Definition 5.4 and Definition 5.5. □

For a general undefined configuration $f$, we can compute $p_f$ in terms of the monomials $p_g$ associated with the potential configurations $g$ of $f$ (see Proposition 5.2). However, before we present this proposition, we require a preceding definition, which will play a crucial role in our paper:

Definition 5.6. Let $g:\mathcal{X}\to\{1, 2\}$ be a potential configuration of an undefined configuration $f$. We define the following monomial:

Proposition 5.2. Let $f$ be an undefined configuration. We have the following:

Proof. We have the following:

$p_f = p_F\prod_{x\in\mathcal{X}} p_x(f(x)) = p_F\prod_{x\not\in U_f} p_x(f(x))\prod_{x\in U_f} p_x(f(x)) = \\ = p_F\prod_{x\not\in U_f} p_x(f(x))\prod_{x\in U_f}(z_{x, 1}p_x(1)+z_{x, 1}p_x(2)) = \\ = p_F\prod_{x\not\in U_f} p_x(f(x))\sum_{g\in \mathcal{P}_f}\prod_{x\in U_f}(z_{x, g(x)}p_x(g(x)) = \\ = p_F\prod_{x\not\in U_f} p_x(f(x))\sum_{g\in \mathcal{P}_f}r_{f, g} \prod_{x\in U_f}p_x(g(x)) = \\ = \sum_{g\in \mathcal{P}_f}p_F r_{f, g} \prod_{x\not\in U_f} p_x(f(x)) \prod_{x\in U_f}p_x(g(x)) = \\ = \sum_{g\in \mathcal{P}_f}p_F r_{f, g} \prod_{x\not\in U_f} p_x(g(x)) \prod_{x\in U_f}p_x(g(x)) = \\ = \sum_{g\in \mathcal{P}_f}p_F r_{f, g} \prod_{x\in \mathcal{X}} p_x(g(x)) = \sum_{g\in \mathcal{P}_f}r_{f, g} p_F \prod_{x\in \mathcal{X}} p_x(g(x)) = \sum_{g\in \mathcal{P}_f}r_{f, g} p_{g}$

□

According to the following proposition, the monomial $r_{f, g}$ identifies the potential configuration $g$ of the undefined configuration $f$.

Proposition 5.3. Let $f$ be an undefined configuration. Let $r_{f, g}$ be the monomial associated to the potential configuration $g$ of $f$ (see Definition 5.6), we can obtain $g$ through $f$ and $r_{f, g}$ by the following expression:

Proof. We will consider the following cases:

Case $z_{x, 1} | r_{f, g}$. By Definition 5.6, we have that $g(x) = 1$ and $x\in U_f$.

Case $z_{x, 2} | r_{f, g}$. By Definition 5.6, we have that $g(x) = 2$ and $x\in U_f$.

Case $z_{x, 1} \not | r_{f, g}$ and $z_{x, 2} \not | r_{f, g}$. Since $g\in\{1, 2\}$, we have that (see Definition 5.6) $x\not \in U_f$. Consequently $g(x) = f(x)$.

□

In the railway station depicted in Figure 1, we have:

In the scenario depicted in Figure 3, we have:

In the scenario depicted in Figure 4, we have:

5.3.   Calculating the set $\mathcal{S}_f$

In this section, we will unveil the primary result of our paper. Given a multiset $Q$ that represents the placement of the trains within the railway station and an undefined configuration $f$, the monomials of the polynomial derived by the expression ${\rm{NR}}(p_f q, \mathcal{E})$ encode all the safe potential configurations of $f$. In other words, we can derive the set $\mathcal{S}_f$.

We introduce a preliminary lemma:

Lemma 5.1. let $g:\mathcal{X}\to\{1, 2\}$ be a potential configuration of $f$.

i) We have that ${\rm{NR}}(p_{g} q, \mathcal{E})$ is either 0 or a monomial without variables of type $z$.

- ${\rm{NR}}(p_{g} q, \mathcal{E})$ is a monomial without variables of type $z$

- ${\rm{NR}}(p_{g} q, \mathcal{E}) = 0 \Leftrightarrow g\not \in \mathcal{S}_f$

ii) We have that ${\rm{NR}}(r_{f, g} p_{g}q, \mathcal{E})$ is a monomial. Besides,

iii) Given $G\subseteq\mathcal{P}_f$, we have that

Proof.

i) This is the main result in ^[35].

ii) This is a immediate consequence of the fact that the polynomials in $\mathcal{E}$ does not contain variables of type $z$.

iii) We have that:

${\rm{NR}}(\sum_{g\in G} r_{f, g} p_{g}q, \mathcal{E}) = {\rm{NF}}(\sum_{g\in G} r_{f, g} p_{g}q, \mathcal{E}') = \sum_{g\in G} {\rm{NF}}(r_{f, g} p_{g}q, \mathcal{E}') = \sum_{g\in G} {\rm{NR}}(r_{f, g} p_{g}q, \mathcal{E}) = \\ \sum_{g\in G} r_{f, g} {\rm{NR}}(p_{g}q, \mathcal{E})$

□

Theorem 5.2. Let $f:\mathcal{X}\to\{0, 1, 2\}$ be an undefined configuration of a railway station. Let $Q$ be the multiset of the position of trains in the railway station. We have that:

● If $U_f = \emptyset$ we have that:

● If $U_f\neq \emptyset$, then the polynomial ${\rm{NR}}(p_fq, \mathcal{E})$ includes exactly $|\mathcal{S}_f|$ distinct monomials, each of which represents a safe potential configuration of $f$. Specifically, we have:

where $u_{g}$ is a monomial in $\mathcal{A}$.

In the case that $\mathcal{S}_f = \emptyset$ (the situation is dangerous regardless of the state of the traffic rail control elements in $U_f$), we have that:

Proof.

● Suppose that $U_f = \emptyset$.

We have that $f$ is also a potential configuration of $f$ (see Definition 4.10). We have that $f\in \mathcal{S}_f$ if and only if ${\rm{NR}}(p_fq, \mathcal{E})\neq 0$. By definition, we have that $f \in \mathcal{S}_f$ if and only if the situation is safe. Consequently, we have that the situation is dangerous if and only if ${\rm{NR}}(p_fq, \mathcal{E}) = 0$

● Suppose that $U_f\neq\emptyset$.

${\rm{NR}}(p_f q, \mathcal{E}) = \text{(By Proposition 5.2)}\\ = {\rm{NR}}(\sum_{g\in \mathcal{P}_f} r_{f, g} p_{g} q, \mathcal{E}) = \text{(by iii in Lemma 5.1)} \\ = \sum_{g\in \mathcal{P}_f}r_{f, g} {\rm{NR}}(p_{g} q, \mathcal{E}) = \text{(by i in Lemma 5.1)}\\ = \sum_{g\in \mathcal{S}_f} r_{f, g} {\rm{NR}}(p_{g} q, \mathcal{E}) = \sum_{g\in \mathcal{S}_f} r_{f, g} \cdot u_{g}$

where $u_{g} = {\rm{NR}}(p_gq, \mathcal {E})$

According to Proposition 5.3 all the terms $r_{f, g} \cdot u_{g}$ in the summand are monomials, they are different each other, and each one identifies each potential configuration $g$ that is safe. Consequently, the size of $\mathcal{S}_f$ is given by the number of monomials of $p_f$. □

In the scenario depicted in Figure 3, we have:

${\rm{NR}}(p_f q, \mathcal{E}) = z_{1, 2}z_{4, 2}\cdot l_{2, 1}l_{2, 9}l_{3, 4}l_{5, 4}l_{5, 6}l_{6, 5}l_{6, 7}l_{7, 6} l_{7, 8}l_{8, 7}l_{9, 2}l_{9, 10}m_{1, 2}m_{2, 3}m_{3, 2}m_{4, 3}m_{4, 5}m_{6, 11}m_{10, 9}m_{10, 11}m_{11, 6}\\ m_{11, 10}t_{1}t_{10}t_{11}$

As observed, the polynomial ${\rm{NR}}(p_f q, \mathcal{E})$ is simply one monomial. Therefore, according to Theorem 5.2, there is only one safe potential configuration, $g_1$. This implies that $\mathcal{S}_f = \{g_1\}$. Given that $r_{f, g_1} = z_{1, 2}z_{4, 2}$, it follows that $g_1(\text{L1}) = g_1(\text{L4}) = 2$. In other words, the color of the lights signals L1 and L4 must be set to red to ensure safety.

In the situation depicted in Figure 4, we have:

${\rm{NR}}(p_f q, \mathcal{E}) = z_{1, 1}z_{4, 1}z_{9, 1}\cdot l_{5, 4}l_{5, 6}l_{6, 5}l_{6, 7}l_{7, 6}l_{7, 8}l_{8, 7}m_{1, 2} m_{2, 1}m_{2, 3}m_{2, 9}m_{3, 2}m_{3, 4}m_{4, 3}m_{4, 5}m_{6, 11}m_{9, 2}m_{9, 10} \\ m_{10, 9}m_{10, 11}m_{11, 6}m_{11, 10}t_{1}t_{2}t_{3}t_{4}t_{9}t_{10}t_{11} +\\ + z_{1, 1}z_{4, 2}z_{9, 1} \cdot l_{5, 4}l_{5, 6}l_{6, 5}l_{6, 7}l_{7, 6}l_{7, 8}l_{8, 7}l_{9, 10} m_{1, 2}m_{2, 1}m_{2, 3}m_{2, 9}m_{3, 2}m_{3, 4}m_{4, 3}m_{4, 5}m_{6, 11}m_{9, 2} m_{10, 9}m_{10, 11}\\ m_{11, 6}m_{11, 10}t_{1}t_{2}t_{3}t_{4}t_{10}t_{11} +\\ + z_{1, 2}z_{4, 1}z_{9, 1} \cdot l_{2, 1}l_{2, 3}l_{3, 2}l_{3, 4}l_{5, 4}l_{5, 6}l_{6, 5}l_{6, 7} l_{7, 6}l_{7, 8}l_{8, 7}m_{1, 2}m_{2, 9}m_{4, 3}m_{4, 5}m_{6, 11}m_{9, 2}m_{9, 10} m_{10, 9}m_{10, 11}\\ m_{11, 6}m_{11, 10}t_{1}t_{9}t_{10}t_{11} + \\ + z_{1, 2}z_{4, 2}z_{9, 1}\cdot l_{2, 1}l_{2, 3}l_{3, 2}l_{3, 4}l_{5, 4}l_{5, 6}l_{6, 5}l_{6, 7} l_{7, 6}l_{7, 8}l_{8, 7}l_{9, 10}m_{1, 2}m_{2, 9}m_{4, 3}m_{4, 5}m_{6, 11}m_{9, 2} m_{10, 9}m_{10, 11}m_{11, 6}m_{11, 10}t_{1}t_{10}t_{11} + \\ + z_{1, 2}z_{4, 2}z_{9, 2}\cdot l_{2, 1}l_{2, 9}l_{3, 4}l_{5, 4}l_{5, 6}l_{6, 5}l_{6, 7}l_{7, 6} l_{7, 8}l_{8, 7}l_{9, 2}l_{9, 10}m_{1, 2}m_{2, 3}m_{3, 2}m_{4, 3}m_{4, 5}m_{6, 11} m_{10, 9}m_{10, 11}m_{11, 6}m_{11, 10}t_{1}t_{10}t_{11}$

As observed, ${\rm{NR}}(p_f q, \mathcal{E})$ is the sum of five monomial. Consequently, according to Theorem 5.2, there are five possibilities to ensure safety (the size of $\mathcal{S}_f$ is 5). Each monomial $r_{f, g}$ of $p_f$ identifies each potential configuration $\mathcal{S}_f = \{g_1, g_2, g_3, g_4, g_5\}$ (see Proposition 5.3). These are:

● $r_{f, g_1} = z_{1, 1}z_{4, 1}z_{9, 1}$: The color light signals L1 and L4 are set to green and the switch of the turnout D1 is set to the straight track position. That is to say, we have that:

$g_1(\text{L1}) = g_1(\text{L4}) = g_1(\text{D1}) = 1$.

● $r_{f, g_2} = z_{1, 1}z_{4, 2}z_{9, 1}$: The color light signal L1 is set to green, the color light signal L4 is set to red and the switch of the turnout D1 is set to the straight track position. That is to say, we have that:

$g_2(\text{L1}) = 1; g_2(\text{L4}) = 2; g_2(\text{D1}) = 1$.

● $r_{f, g_3} = z_{1, 2}z_{4, 1}z_{9, 1}$: The color light signal L1 is set to red, the color light signal L4 is set to green and the switch of the turnout D1 is set to the straight track position. That is to say, we have that:

$g_3(\text{L1}) = 2; g_3(\text{L4}) = 1; g_3(\text{D1}) = 1$.

● $r_{f, g_4} = z_{1, 2}z_{4, 2}z_{9, 1}$: The color light signals L1 and L4 are set to red and the switch of the turnout D1 is set to the straight track position. That is to say, we have that:

$g_4(\text{L1}) = 1; g_4(\text{L4}) = 2; g_4(\text{D1}) = 1$.

● $r_{f, g_5} = z_{1, 2}z_{4, 2}z_{9, 2}$: The color light signals L1 and L4 are set to red and the switch of the turnout D1 is set to the diverted track position. That is to say, we have that:

$g_5(\text{L2}) = g_5(\text{L4}) = 2; g_5(\text{D1}) = 2$.

6.   Implementation in CoCoA

In this section, we will implement an interlocking system using CoCoA ^[36], a Computer Algebra System. The system will not only determine if a given situation poses a danger, but it will also identify the states of the turnouts and color light signals for undefined configurations to ensure safety. For illustrative purposes, we will delve into a specific railway station depicted in Figure 1. However, the principles and methods discussed can be seamlessly applied to any railway system.

6.1.   Instructions related to the design of the railway station

In this section, we will provide the instructions in CoCoA related to a railway station. Specifically, we will define the ring which polynomials and monomials lie, define the list $\mathcal{E}$, declare the rail traffic control elements, and implement the function that assigns a polynomial to an undefined configuration in the railway station.

We define the ring $\mathcal{A}'$ for the railway station depicted in Figure 1.

$\texttt{use ZZ/(2)[z[1..10, 1..2], l[1..11, 1..11], m[1..11, 1..11], t[1..11]], lex; }$

Next, we define the list $\mathcal{E}$ for this railway station, in accordance with Definition 5.1.

$\texttt{E: = [l[1,2]*l[2,1]*t[1]+m[1,2]*m[2,1]*t[1]*t[2], } \\ \texttt{ l[1,2]*m[2,1]*t[1]+m[1,2]*m[2,1]*t[1]*t[2], } \\ \texttt{ l[2,9]*l[9,2]*t[2]+m[2,9]*m[9,2]*t[2]*t[9], } \\ \texttt{ l[2,9]*m[9,2]*t[2]+m[2,9]*m[9,2]*t[2]*t[9], } \\ \texttt{ l[9,10]*l[10,9]*t[9]+m[9,10]*m[10,9]*t[9]*t[10], } \\ \texttt{ l[9,10]*m[10,9]*t[9]+m[9,10]*m[10,9]*t[9]*t[10], } \\ \texttt{ l[10,11]*l[11,10]*t[10]+m[10,11]*m[11,10]*t[10]*t[11], } \\ \texttt{ l[10,11]*m[11,10]*t[10]+m[10,11]*m[11,10]*t[10]*t[11], } \\ \texttt{ l[11,6]*l[6,11]*t[11]+m[11,6]*m[6,11]*t[11]*t[6], } \\ \texttt{ l[11,6]*m[6,11]*t[11]+m[11,6]*m[6,11]*t[11]*t[6], } \\ \texttt{ l[2,3]*l[3,2]*t[2]+m[2,3]*m[3,2]*t[2]*t[3], } \\ \texttt{ l[2,3]*m[3,2]*t[2]+m[2,3]*m[3,2]*t[2]*t[3], } \\ \texttt{ l[3,4]*l[4,3]*t[3]+m[3,4]*m[4,3]*t[3]*t[4], } \\ \texttt{ l[3,4]*m[4,3]*t[3]+m[3,4]*m[4,3]*t[3]*t[4], } \\ \texttt{ l[4,5]*l[5,4]*t[4]+m[4,5]*m[5,4]*t[4]*t[5], } \\ \texttt{ l[4,5]*m[5,4]*t[4]+m[4,5]*m[5,4]*t[4]*t[5], } \\ \texttt{ l[5,6]*l[6,5]*t[5]+m[5,6]*m[6,5]*t[5]*t[6], } \\ \texttt{ l[5,6]*m[6,5]*t[5]+m[5,6]*m[6,5]*t[5]*t[6], } \\ \texttt{ l[6,7]*l[7,6]*t[6]+m[6,7]*m[7,6]*t[6]*t[7], } \\ \texttt{ l[6,7]*m[7,6]*t[6]+m[6,7]*m[7,6]*t[6]*t[7], } \\ \texttt{ l[7,8]*l[8,7]*t[7]+m[7,8]*m[8,7]*t[7]*t[8], } \\ \texttt{ l[7,8]*m[8,7]*t[7]+m[7,8]*m[8,7]*t[7]*t[8], } \\ \texttt{ l[2,1]*l[1,2]*t[2]+m[2,1]*m[1,2]*t[2]*t[1], } \\ \texttt{ l[2,1]*m[1,2]*t[2]+m[2,1]*m[1,2]*t[2]*t[1], } \\ \texttt{ l[9,2]*l[2,9]*t[9]+m[9,2]*m[2,9]*t[9]*t[2], } \\ \texttt{ l[9,2]*m[2,9]*t[9]+m[9,2]*m[2,9]*t[9]*t[2], } \\ \texttt{ l[10,9]*l[9,10]*t[10]+m[10,9]*m[9,10]*t[10]*t[9], } \\ \texttt{ l[10,9]*m[9,10]*t[10]+m[10,9]*m[9,10]*t[10]*t[9], } \\ \texttt{ l[11,10]*l[10,11]*t[11]+m[11,10]*m[10,11]*t[11]*t[10], } \\ \texttt{ l[11,10]*m[10,11]*t[11]+m[11,10]*m[10,11]*t[11]*t[10], } \\ \texttt{ l[6,11]*l[11,6]*t[6]+m[6,11]*m[11,6]*t[6]*t[11], } \\ \texttt{ l[6,11]*m[11,6]*t[6]+m[6,11]*m[11,6]*t[6]*t[11], } \\ \texttt{ l[3,2]*l[2,3]*t[3]+m[3,2]*m[2,3]*t[3]*t[2], } \\ \texttt{ l[3,2]*m[2,3]*t[3]+m[3,2]*m[2,3]*t[3]*t[2], } \\ \texttt{ l[4,3]*l[3,4]*t[4]+m[4,3]*m[3,4]*t[4]*t[3], } \\ \texttt{ l[4,3]*m[3,4]*t[4]+m[4,3]*m[3,4]*t[4]*t[3], } \\ \texttt{ l[5,4]*l[4,5]*t[5]+m[5,4]*m[4,5]*t[5]*t[4], } \\ \texttt{ l[5,4]*m[4,5]*t[5]+m[5,4]*m[4,5]*t[5]*t[4], } \\ \texttt{ l[6,5]*l[5,6]*t[6]+m[6,5]*m[5,6]*t[6]*t[5], } \\ \texttt{ l[6,5]*m[5,6]*t[6]+m[6,5]*m[5,6]*t[6]*t[5], } \\ \texttt{ l[7,6]*l[6,7]*t[7]+m[7,6]*m[6,7]*t[7]*t[6], } \\ \texttt{ l[7,6]*m[6,7]*t[7]+m[7,6]*m[6,7]*t[7]*t[6], } \\ \texttt{ l[8,7]*l[7,8]*t[8]+m[8,7]*m[7,8]*t[8]*t[7], } \\ \texttt{ l[8,7]*m[7,8]*t[8]+m[8,7]*m[7,8]*t[8]*t[7], } \\ \texttt{ t[1]^2, t[2]^2, t[3]^2, t[4]^2, t[5]^2, t[6]^2, } \\ \texttt{ t[7]^2, t[8]^2, t[9]^2, t[10]^2, t[11]^2];}$

Finally, we define the set of the rail traffic control elements, $\mathcal{X}$, in accordance with Definition 4.2. This set includes eight color light signals, $\texttt{L1}$, $\ldots$, $\texttt{L8}$, and two turnouts, $\texttt{D1}$ and $\texttt{D2}$.

$\texttt{L1: = [1,2]; } \\ \texttt{ L2: = [4,3];} \\ \texttt{ L3: = [4,5]; } \\ \texttt{ L4: = [10,9]; } \\ \texttt{ L5: = [10,11];} \\ \texttt{ L6: = [11,10]; } \\ \texttt{ L7: = [6,7];} \\ \texttt{ L8: = [8,7]; } \\ \texttt{ D1: = [2,3,9];} \\ \texttt{ D2: = [6,5,11];}$

$\texttt{ X: = [L1, L2, L3, L4, L5, L6, L7, L8, D1, D2]; } \\ \texttt{ NUM_LIGHTS: = 8; } \\ \texttt{ Green: = 1; Red: = 2; } \\ \texttt{ Straight: = 1; Diverted: = 2; }$

Now, we define the monomial $p_F$, the polynomial assigned to each rail traffic control element and the polynomial assigned to an undefined configuration.

● According to Definition 5.4, the polynomial $p_F$ is:

$\texttt{ pF: = l[2,1]*l[3,4]*l[5,4]*l[7,6]*l[7,8]*l[9,10];}$

● According to Definition 5.3, we implement the function $p_x:\{0, 1, 2\}\to \mathcal{A}'$ for each control element $x$.

However, here we consider two arguments for the implementation of this function $\texttt{p_x}$:

- $\texttt{i}$ referring to the $i$-th control element in $\texttt{X}$.

- $\texttt{v}$ referring to the independent variable $v$ in the function $p_x$ (see Definition 5.3).

$\texttt{ Define p_x(i, v) } \\ ~~~~ \texttt{ TopLevel X; } \\ ~~~~ \texttt{ TopLevel l; } \\ ~~~~ \texttt{ TopLevel m; } \\ ~~~~ \texttt{ TopLevel z; } \\ ~~~~ \texttt{ if v = 0 then return z[i, 1]*p_x(i, 1) + z[i, 2]*p_x(i, 2); endif; } \\ ~~~~ \texttt{ x: = X[i]; } \\ ~~~~~~ \texttt{ if len(x) = 2 then } \\ ~~~~~~~~ \texttt{ if v = 1 then } \\ ~~~~~~~~ \texttt{ return l[x[1], x[2]]; } \\ ~~~~~~ \texttt{ else } \\ ~~~~~~~~ \texttt{ return m[x[1], x[2]]; } \\ ~~~~~~ \texttt{ endif; } \\ ~~~~ \texttt{ Elif len(x) = 3 then } \\ ~~~~~~~~ \texttt{ if v = 1 then } \\ ~~~~~~~~~~ \texttt{ return l[x[1], x[2]]*l[x[2], x[1]]*m[x[1], x[3]]*m[x[3], x[1]]; } \\ ~~~~~~~~ \texttt{ else } \\ ~~~~~~~~~~ \texttt{return m[x[1], x[2]]*m[x[2], x[1]]*l[x[1], x[3]]*l[x[3], x[1]]; } \\ ~~~~~~~~ \texttt{ endif; } \\ ~~~~~~ \texttt{ endif; } \\ ~~~~ \texttt{ EndDefine; }$

• According to Definition 5.5, we define the polynomial $p_f$ associated with an undefined configuration of the railway station:

$\texttt{ Define p_f(f)} \\ ~~~~ \texttt{ TopLevel pF; } \\ ~~~~ \texttt{ TopLevel X; } \\ ~~~~ \texttt{ p: = pF; } \\ ~~~~ \texttt{ for i: = 1 to len(X) do } \\ ~~~~~~~~ \texttt{ p: = p*p_x(i, f[i]); } \\ ~~~~ \texttt{ endfor; } \\ ~~~~ \texttt{ return p; } \\ \texttt{ EndDefine;}$

6.2.   Instructions related to analyze a situation in the railway station

In this section, we will provide the instructions in CoCoA related to analyze situations in the railway station.

We will consider the scenario depicted in Figure 2: there are two trains (one in section S1 and another in section S10); the color light signals $\texttt{L2}$ and $\texttt{L4}$ are displaying red, while the rest are displaying green; the switch of the turnout $\texttt{D1}$ is set to the diverted track position, and the switch of the turnout $\texttt{D2}$ is set to the straight track position. We define $q$ and the determined configuration $f$:

$\texttt{f: = [Green, Red, Red, Red, Green, Green, Green, Green, Diverted, Straight];} \\ \texttt{ q: = t[1]*t[10]; }$

According to part i) of Theorem 5.2 we can determine whether the situation is safe or dangerous by calculating ${\rm{NR}}(p_f(f)q, \mathcal{E})$. The Computer Algebra System $\texttt{CoCoA}$ includes the internal function $\texttt{NR}$ to calculate this function ${\rm{NR}}$.

$\texttt{ NR(p_f(f)*q, E); }$

Since the output in CoCoA is $\texttt{0}$, the situation dangerous. Consequently, we need to change the state of some control elements in the railway station to make it safe. We will consider changing the state of the color light signals $\texttt{L1}$ and $\texttt{L4}$ as depicted in Figure 3.

$\texttt{ f[1]: = 0; } \\ \texttt{ f[4]: = 0;} \\ \texttt{ NR(p_f(f)*q, E);}$

The output is:

$\texttt{ z[1,2]*z[4,2]*l[2,1]*l[2,9]*l[3,4]*l[5,4]*l[5,6]*l[6,5]*l[6,7]*l[7,6]* }\\ \texttt{ l[7,8]*l[8,7]*l[9,2]*l[9,10]*m[1,2]*m[2,3]*m[3,2]*m[4,3]*m[4,5]* }\\ \texttt{m[6,11]*m[10,9]*m[10,11]*m[11,6]*m[11,10]*t[1]*t[10]*t[11] }$

According to part ii) of Theorem 5.2, since the variables $\texttt{z[1,2]}$ and $\texttt{z[4,2]}$ are present in the output, we can conclude that the situation will be safe if both L1 and L4 are set to red. Indeed, since the output polynomial contains only one monomial, this is the only possibility to make the situation safe.

Now, we will consider that we could also change the state of the turnout $\texttt{D1}$ as depicted in Figure 4.

$\texttt{ f[1]: = 0; }\\ \texttt{ f[4]: = 0; }\\ \texttt{ f[1 + NUM_LIGHTS]: = 0; }\\ \texttt{ NR(p_f(f)*q, E);}$

The output is:

$\texttt{z[1,1]*z[4,1]*z[9,1]*l[5,4]*l[5,6]*l[6,5]*l[6,7]*l[7,6]*l[7,8]*l[8,7]*m[1,2]* }\\ \texttt{m[2,1]*m[2,3]*m[2,9]*m[3,2]*m[3,4]*m[4,3]*m[4,5]*m[6,11]*m[9,2]*m[9,10]* }\\ \texttt{m[10,9]*m[10,11]*m[11,6]*m[11,10]*t[1]*t[2]*t[3]*t[4]*t[9]*t[10]*t[11] +}\\ \texttt{ + z[1,1]*z[4,2]*z[9,1]*l[5,4]*l[5,6]*l[6,5]*l[6,7]*l[7,6]*l[7,8]*l[8,7]*l[9,10]* }\\ \texttt{m[1,2]*m[2,1]*m[2,3]*m[2,9]*m[3,2]*m[3,4]*m[4,3]*m[4,5]*m[6,11]*m[9,2]*}\\ \texttt{ m[10,9]*m[10,11]*m[11,6]*m[11,10]*t[1]*t[2]*t[3]*t[4]*t[10]*t[11] + }\\ \texttt{+ z[1,2]*z[4,1]*z[9,1]*l[2,1]*l[2,3]*l[3,2]*l[3,4]*l[5,4]*l[5,6]*l[6,5]*l[6,7]* }\\ \texttt{l[7,6]*l[7,8]*l[8,7]*m[1,2]*m[2,9]*m[4,3]*m[4,5]*m[6,11]*m[9,2]*m[9,10]* }\\ \texttt{m[10,9]*m[10,11]*m[11,6]*m[11,10]*t[1]*t[9]*t[10]*t[11] +}\\ \texttt{ + z[1,2]*z[4,2]*z[9,1]*l[2,1]*l[2,3]*l[3,2]*l[3,4]*l[5,4]*l[5,6]*l[6,5]*l[6,7]* }\\ \texttt{l[7,6]*l[7,8]*l[8,7]*l[9,10]*m[1,2]*m[2,9]*m[4,3]*m[4,5]*m[6,11]*m[9,2]* }\\ \texttt{m[10,9]*m[10,11]*m[11,6]*m[11,10]*t[1]*t[10]*t[11] +}\\ \texttt{ + z[1,2]*z[4,2]*z[9,2]*l[2,1]*l[2,9]*l[3,4]*l[5,4]*l[5,6]*l[6,5]*l[6,7]*l[7,6]* }\\ \texttt{l[7,8]*l[8,7]*l[9,2]*l[9,10]*m[1,2]*m[2,3]*m[3,2]*m[4,3]*m[4,5]*m[6,11]* }\\ \texttt{m[10,9]*m[10,11]*m[11,6]*m[11,10]*t[1]*t[10]*t[11] }$

According to part ii) of Theorem 5.2, since the output polynomial contains five monomials, there are five possibilities to make the situation safe.

6.3.   Instructions related to interpret $p_f$

The polynomial ${\rm{NR}}(p_f(f)q, \mathcal{E})$ might indeed be difficult to interpret because it contains monomials with many variables of a type other than $z$. In this section, we will provide an implementation in CoCoA of a function, $\texttt{PrintAllPotentialConfigurations}$ that outputs a string describing the potential configurations of $f$.

We need to first implement some auxiliary functions:

$\texttt{ Define PrintDescriptionName(v) } \\ ~~~~ \texttt{ TopLevel NUM_LIGHTS; } \\ ~~~~~~ \texttt{num: = IndetSubscripts(v); } \\ ~~~~ ~~ \texttt{if num[1] < = NUM_LIGHTS then } \\ ~~~~~~~~ \texttt{ print "L[", num[1], "]:"; } \\ ~~~~~~~~\texttt{ if num[2] = 1 then print "Green"; else print "Red "; endif; } \\ ~~~~ \texttt{ else } \\ ~~~~~~ \texttt{ print "D[", num[1]-NUM_LIGHTS, "]:"; } \\ ~~~~~~ \texttt{ if num[2] = 1 then print "Straight"; else print "Diverted"; endif; } \\ ~~~~ \texttt{ endif; } \\ \texttt{ EndDefine;}$

$\texttt{Define PrintOnePotentialConfiguration(m, f) } \\ ~~~~ \texttt{ TopLevel z; } \\ ~~~~ \texttt{ for i: = 1 to len(f) do } \\ ~~~~~~ \texttt{ if f[i] = 0 then } \\ ~~~~~~~~~~~~ \texttt{ r: = z[i, 1]; } \\ ~~~~~~~~~~~~ \texttt{ if IsDivisible(m, r) then } \\ ~~~~~~~~~~ \texttt{ PrintDescriptionName(r); print " "; } \\ ~~~~~~~~ \texttt{ else } \\ ~~~~~~~~~~ \texttt{ r: = z[i, 2]; } \\ ~~~~~~~~~~ \texttt{ PrintDescriptionName(r); print " "; } \\ ~~~~~~~~~~~~ \texttt{ endif; } \\ ~~~~~~~~~~ \texttt{ endif; } \\ ~~~~~~~~ \texttt{ endfor; } \\ ~~~~~~~~ \texttt{ println; } \\ \texttt{ EndDefine; }$

As may be seen, the implementation of the function $\texttt{PrintOnePotentialConfiguration}$ requires $\texttt{IsDivisible}$, an internal function of $\texttt{CoCoA}$ (implemented in any computer algebra system) which determines whether a polynomial $\texttt{m}$ is divisible by $\texttt{r}$.

The implementation of $\texttt{PrintAllPotentialConfigurations}$ is as follows:

$\texttt{Define PrintAllPotentialConfigurations(f, q)}\\ ~~~~ \texttt{ TopLevel E;}\\ ~~~~ ~~ \texttt{ r: = NR(p_f(f)*q, E);}\\ ~~~~ ~~ \texttt{ if r = 0 then println "The situation is dangerous"; else println "The situation is safe for these cases:"; endif; }\\ ~~~~ ~~ \texttt{while r <>0 do }\\ ~~~~ ~~ ~~\texttt{m: = LT(r); }\\ ~~~~ ~~ ~~\texttt{PrintOnePotentialConfiguration(m, f); }\\ ~~~~ ~~ ~~ \texttt{r: = m+r;}\\ ~~~~ ~~ \texttt{ EndWhile;}\\ \texttt{ EndDefine; }$

Now, we can easily identify the possibilities to make the situation safe. For the scenario depicted in Figure 4, we simply need to input the following into CoCoA:

$\texttt{ PrintAllPotentialConfigurations(f, q); }$

And CoCoA will output the results:

$\texttt{The situation is safe for these cases: }\\ \texttt{ L[1]:Green L[4]:Green D[1]:Straight}\\ \texttt{ L[1]:Green L[4]:Red D[1]:Straight }\\ \texttt{L[1]:Red L[4]:Green D[1]:Straight}\\ \texttt{ L[1]:Red L[4]:Red D[1]:Straight }\\ \texttt{L[1]:Red L[4]:Red D[1]:Diverted }$

These are the five possibilites to turn the situation safe. For example, we can set the color of traffic lights $\texttt{L1}$ and $\texttt{L4}$ to $\texttt{Green}$ and set the switch of the turnout $\texttt{D1}$ in straight track position to turn the situation safe.

7.   Conclusions

We present an algebraic model for railway interlocking systems, which are crucial safety components in rail transportation. These systems regulate the transitions between sections of a railway station using rail traffic control elements and prevent train collisions. The model introduced in this paper enhances the capabilities of these systems by not only indicating whether a situation is dangerous but also providing guidance on how to configure certain rail traffic control elements to ensure safety if a dangerous situation is detected.

The model represents the railway station and its situations algebraically through polynomials. It transforms the task of identifying dangerous situations into calculating the residue polynomial of a monomial division over a set of polynomials. The monomials contained in this residue polynomial encode all possible configurations that would render the situation safe.

We extend a previous groundbreaking algebraic model that improved the implementation of interlocking systems by providing a linear algorithm suitable for large-scale railway stations. However, the previous model determined only whether a situation was dangerous or not and did not provide any guide on how to configure certain control elements to ensure safety in case of danger. We fill that gap by extending the model to include this capacity.

In conclusion, this paper contributes significantly to the field of railway interlocking systems by introducing an enhanced algebraic model that not only identifies dangerous situations but also provides guidance on how to ensure safety in such situations. This work paves the way for more efficient and safer rail transportation.

Author contributions

Antonio Hernando, Gabriel Aguilera-Venegas, José Luis Galán-García, Sheida Nazary: conceptualization, investigation, methodology, validation, formal analysis; Antonio Hernando: supervision, writing-original draft preparation; Gabriel Aguilera-Venegas, José Luis Galán-García: Software; Sheida Nazary: writing-review and editing.

All authors have read and approved the final version of the manuscript for publication.

Use of AI tools declaration

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

Conflict of interest

Prof. José Luis Galán-García is the special issue editor for AIMS Mathematics and was not involved in the editorial review or the decision to publish this article. All authors declare that there are no competing interests.