# Interval Number-Based Safety Reasoning Method for Verification of Decentralized Power Systems in High-Speed Trains

Authors: Peng Wu; Ning Xiong; Jiqiang Liu; Liujia Huang; Zhuoya Ju; Yannan Ji; Jinzhao Wu
Journal: Mathematical Problems in Engineering
 (2021)

---

## Abstract

Decentralized power systems are commonly used in high-speed trains. However, many parameters in decentralized power systems are uncertain and inevitably have errors. We present a reasoning method based on the interval numbers for decentralized power systems in high-speed trains. Uncertain parameters and their unavoidable errors are quantitatively described by interval numbers. We also define generalized linear equations with interval numbers (LAIs), which can be used to describe the movement of the train. Furthermore, it is proven that the zero sets of LAIs are convex. Therefore, the inside of the fault-tolerance area can be formed by their vertexes and edges and represented by linear inequalities. Consequently, we can judge whether the system is working properly by verifying that the current system state is in the fault-tolerance area. Finally, a fault-tolerance area is obtained, which can be determined by linear equations with an interval number, and we test the correctness of the fault-tolerance area through large-scale random test cases.


---

## Body

## 1. Introduction

Theorem proving is well established in formal verification [1, 2]. Unlike model checking [3, 4], the deductive reasoning method is used to verify the safety conditions or properties of the system. This method and model checking have complementary strengths and disadvantages [5, 6]. To verify certain properties of the system, labeled transition systems (LTSs) are widely used to describe the system behaviors in the field of system verification, such as communication protocols and hardware logic testing [7, 8], and a similar structure is used. Abstract labels of the labeled transition system (LTS) describe the system states by a set of logical assignments. For instance, the LTS model of a microwave oven, where “close” represents the state that the door of microwave oven is close, “∼close” represents the state of “open door,” “heat” represents the heating state, and “∼heat” represents the nonheating state. Thus, (close, ∼heat) indicates that the oven is closed and not heating. However, it is not completely adequate to describe the state of complex systems. For example, train motion must be described by algebraic equations Naturally, algebraic transition systems can be modeled in the above example, being labeled by polynomial algebraic equations [9, 10]. as the promotion of the logical labeled transition system. In recent years, algebraic polynomial-labeled transition systems or their similar structures are still largely involved with the verification of more complex systems [11]. Especially for verification of hybrid systems characterized by differential polynomial algebraic equations, many theories based on polynomial invariants have been put forward [12–16]. However, to find polynomial invariants, the symbolic calculation theory with high time complexity is involved, such as the Gröbner bases, cylindrical algebraic decomposition, and fixed points. However, in some complex systems, some parameters may be uncertain. For example, in high-speed trains, some model parameters are uncertain, such as the changing weight with the number of passengers [17]. Even if it is assumed that the uncertain parameters change continuously, nonetheless, this may result in the discontinuity of the obtained Gröbner bases. Simply put, the Gröbner bases of two polynomial systems with very close coefficients may be completely different, which limits the application of the above theory to the verification of these systems. In contrast, for the design of systems with uncertain parameters, some scholars have performed system design based on fault-tolerant methods [18, 19]. The fault-tolerant method is mature and has been applied in many aspects [20–22]. The success of the fault-tolerant method in the design of complex systems implies that it may also be effective in the verification of complex systems [23–25]. Nevertheless, verification methods with fault-tolerance are rarely reported.Furthermore, regardless of the uncertain parameters, even measurements cannot be completely accurate. For example, in a real system, it is impossible to accurately measure the temperature just to reach a specified value and often with a certain error. The measurement process is also accompanied by a certain error. Hence, verification with fault tolerance is significant in the industry. In addition, nonlinear problems can be approximated as linear problems in small parts of the system design space [26]. The generalized linear assertion also has a certain theoretical value.In this paper, we present a new reasoning method with fault tolerance between generalized linear algebraic assertions to verify decentralized power systems in high-speed trains, and the method does not involve the methods in numerical calculations. Although the numerical calculation method is much faster than symbolic calculation to solve equations, the accumulation of errors during the reasoning process is inevitable and may lead to incorrect conclusions. In numerical calculations, the iterative algorithm for solving equations is terminated after reaching the termination condition. In fact, we still do not know the exact distance between the numerical solution and the unknown exact solution [27]. On the other hand, some scholars have studied fault detection in power systems, in which machine learning algorithms are involved [28, 29]. Their method is effective on nonlinear problems. However, there are still few reports about their methods in dealing with the system with uncertain parameters.


## 2. Problem Descriptions

Proper decentralized power can reduce the maintenance cost of high-speed trains and avoid unsafe speeds. Safe speed and decentralized power need to be considered.


### 2.1. Safe Speeds

The safe speed defines the safe speed range of high-speed trains. Excessive speed increases the risk of derailment, especially when the train is turning. For example, the derailment of a high-speed railway caused more than 80 deaths in Spain in 2013. When the train turns, excessive or insufficient speed increases the force between the train wheel flanges and the rails, which is a crucial cause of rail scratches. Moreover, rail scratches reduce the tolerance of the rail, which further increases the risk of derailment. Usually, when the train turns, there is an inclination angle in the rail to balance the centripetal force. Ideally, the centripetal force when the train turns is equal to the component of the train’s gravity along the inclination. At this time, the force between the wheel flange and the rail is zero.According to Newtonian mechanics, we have(1)mv2R−gtanθ=fw,where m denotes the mass of a carriage, g is the acceleration due to gravity, fw denotes the combined force of all wheel flanges of the two carriages on their wheels, v denotes the speed of the train, R is the turning radius, and θ is the inclination angle of the rail. During train movement, some of the above parameters have inevitable errors. For example, m varies within a certain range depending on the passengers and their luggage.


### 2.2. Power Distribution

Decentralized power systems are often used in high-speed railways, compared with centralized power systems. High-speed trains usually consist of four or eight carriages. The power-decentralization problem of the two carriages can be considered first because the problem for sixteen carriages can be solved by the recursive 2-carriage problem. Among them, some parameters remain uncertain. For example, when the train is moving at a constant speed, the air resistance changes with the change in air pressure. In addition, the speed of the train cannot be held exactly constant, only within a very small range. The air resistance is proportional to the air pressure and the square of the speed. Hence, changing the air resistance will cause dynamic changes in the net power.In the verification field based on the theorem proof, a reasoning method that fully considers the parameters with errors is necessary to verify the safety conditions and properties of the system.


## 2.1. Safe Speeds

The safe speed defines the safe speed range of high-speed trains. Excessive speed increases the risk of derailment, especially when the train is turning. For example, the derailment of a high-speed railway caused more than 80 deaths in Spain in 2013. When the train turns, excessive or insufficient speed increases the force between the train wheel flanges and the rails, which is a crucial cause of rail scratches. Moreover, rail scratches reduce the tolerance of the rail, which further increases the risk of derailment. Usually, when the train turns, there is an inclination angle in the rail to balance the centripetal force. Ideally, the centripetal force when the train turns is equal to the component of the train’s gravity along the inclination. At this time, the force between the wheel flange and the rail is zero.According to Newtonian mechanics, we have(1)mv2R−gtanθ=fw,where m denotes the mass of a carriage, g is the acceleration due to gravity, fw denotes the combined force of all wheel flanges of the two carriages on their wheels, v denotes the speed of the train, R is the turning radius, and θ is the inclination angle of the rail. During train movement, some of the above parameters have inevitable errors. For example, m varies within a certain range depending on the passengers and their luggage.


## 2.2. Power Distribution

Decentralized power systems are often used in high-speed railways, compared with centralized power systems. High-speed trains usually consist of four or eight carriages. The power-decentralization problem of the two carriages can be considered first because the problem for sixteen carriages can be solved by the recursive 2-carriage problem. Among them, some parameters remain uncertain. For example, when the train is moving at a constant speed, the air resistance changes with the change in air pressure. In addition, the speed of the train cannot be held exactly constant, only within a very small range. The air resistance is proportional to the air pressure and the square of the speed. Hence, changing the air resistance will cause dynamic changes in the net power.In the verification field based on the theorem proof, a reasoning method that fully considers the parameters with errors is necessary to verify the safety conditions and properties of the system.


## 3. Preliminary

In this section, we introduce some of the mathematical concepts that have been established and involved in our approach.Definition 1 (Algebraic transition system).
LetA=<S,F,Ψ,Λ> be an algebraic transition system, whereS is the set of all states in the algebraic transition systemF is the set of transitions between states, F⊆S×SΨ is the set of the algebraic assertionsΛis the set of mapping relationships from F to Ψ and from S to Ψ. Each state or transition can be distributed into algebraic equations based on the mapping relationship
The algebraic transition system describes the system’s transition relationship and the state itself of the system. The setF of an algebraic transition system describes the transition relations between states. Correspondingly, Λ provides each state satisfied algebraic equations or satisfied conditions of transitions between states.
In recent years, the algebraic transition system and its generalized structure have been well established in the field of verification [30, 31].
To establish a reasoning method with fault tolerance, we generalize linear algebraic assertions to quantitatively describe uncertain parameters. A quantitative description of these errors is necessary. Interval numbers have been widely used in the field of error estimation [32, 33]. As a result, we introduce interval numbers to describe the errors. The following is the definition and operation of interval numbers.Definition 2 (Interval number).
An interval number is a set of all real numbers in a closed interval.
LetX¯ be an interval number. Then, X¯=x−,x+, where x−≤x+; x−is the lower bound of X¯ and x+ is the upper bound of X¯. Thus, X¯ can be any value in this closed interval. In particular, when x−=x+, the interval number becomes a normal real number.Definition 3 (Interval number operation).
The interval number operation includes the operations of addition, subtraction, multiplication, and division. Some operations are given as follows.
Leta¯=a−,a+ and b¯=b−,b+, where c is a constant.
Addition:(2)c+a¯=a−+c,a++c,a¯+b¯=a−+b−,a++b+.
Subtraction:(3)a¯−b¯=a−−b+,a+−b−,a¯−c=a−−c,a+−c.
Multiplication:(4)a¯b¯=mina−b−,a−b+,a+b−,a+b+,maxa−b−,a−b+,a+b−,a+b+.
Especially whena¯≥0andb¯≥0,ab=a−b−,a+b+.(5)ifc>0,ca¯=ca−,ca+,ifc<0,ca¯=ca+,ca−,ifc=0,ca¯=0,0=0.
Division:(6)ifc>0,a¯c=a−c,a+c,ifc<0,a¯c=a+c,a−c.
In addition, there are some other definitions of interval number operations [34]. However, we do not elaborate here, as different definitions are irrelevant for the reasoning approach.
Unfortunately, although the errors can be described as any possible values over given intervals, the operation of interval number is not sufficient for reasoning between linear algebra assertions because it may lead to incorrect reasoning. For example, letφ¯=X2¯−X1¯=3,4,X2¯+X1¯=5,6.
According to the interval operation defined above, the linear equations can be solved as follows:(7)X1¯=0,2,X2¯=4,5.
This is not a correct result. The correct result is in the blue diamond area in Figure1.Figure 1
Inclusion relations between zero sets of two LAIs.Definition 4 (Polynomial).
A polynomial is a mathematical expression consisting of a sum of terms, where each term includes one or more variables raised to a power and multiplied by a coefficient.
LetV=x1,…,xn be a set of variables. Let ℝx1,…,xn be a set that comprising all polynomials with real coefficients on V. An example of a polynomial is as follows:(8)f1x1,x2,x3=5x13x2x32+x22+2x3.Definition 5 (Zero set of polynomials).
fx1,…,xn∈ℝx1,…,xn. The zero set of fx1,…,x2 is the set as below, denoted by Zero(f):
Zerof=x1,…,xn∈ℂn|fx1,…,x2=0.Definition 6 (Linear algebraic assertions).
A linear algebraic assertion consists of one or more linear equations.ψ is a linear algebraic assertion that contains the following equations:(9)ψ=f1x1,…,xn=0,f2x1,…,xn=0,…,fnx1,…,xn=0.


## 4. Implication and Equivalence Relations Based on Interval Numbers

In this section, we introduce the judgment rule of implication and equivalence relations based on interval numbers. Implication and equivalence relations are the most basic rules in any reasoning method. We first introduce the reasoning method (Definitions7 and 8) involving implication and equivalence relations. Then, we introduce the definitions (Definitions 9–12).In the classic rules of reasoning, the implication relationship between algebraic assertions can be judged by the inclusion relationship of their zero set.Definition 7 (Implication relations between algebraic assertions).
Letφ1 and φ2 are two algebraic assertions. φ1 implies φ2, denoted as φ1|=φ2, iffZeroφ1⊆Zeroφ2.
For example,x−1=0 implies x2+2x−3=0 because 1⊆1,2.Definition 8 (Equivalence relations between algebraic assertions).
Letφ1 and φ2 be two algebraic assertions. φ1 is equivalent to φ2, denoted as φ1≡φ2, iffZeroφ1=Zeroφ2.Definition 9 (LEI and LAI).
An LEI is a linear algebraic equation whose variables and coefficients can be interval numbers. The LAI consists of one or more LEIs.Definition 10 (Zero set of LEIs).
Letf¯x1,…,xn=a0¯+a1¯x1+a2¯x2+⋯+an¯xn=0 be an LEI. a0¯,a1¯,a2¯,…,an¯ are given some interval numbers, as defined above. The zero set of f¯x1,…,x2 is the set as below and is denoted as Zero (f¯):(10)x1,…,xn|∀a0∈a0¯,∀a1∈a1¯,∀a2∈a2¯,…,∀an∈an¯,a0+a1x1+a2x2+⋯+anxn=0.Definition 11 (Implication relations between LAIs).
Letφ1¯ and φ2¯ be two LAIs that have been defined above. φ1¯ implies φ2¯, denoted as φ1¯|=φ2¯, iffZeroφ1¯⊆Zeroφ2¯.Definition 12 (Equivalence relations between LAIs).
Letφ1¯ and φ2¯ be two LAIs. φ1¯ is equivalent to φ2¯, denoted as φ1¯≡φ2¯, iffZeroφ1¯=Zeroφ2¯.
The implication and equivalence relations are the two main reasoning rules. A simple example is shown in Figure1 for reasoning between LAIs.
Letφ1¯=X2¯−X1¯=3,4,X2¯+X1¯=5,6 and φ2¯=X1¯=0.75,1.25,X2¯=4.25,4.75.
Obviously,Zeroφ2¯⊆Zeroφ1¯ ，and we conclude that φ2¯|=φ1¯.


## 5. Reasoning Method between LAIs and Example

### 5.1. Reasoning Method between LAIs

In this section, we present a reasoning method to judge inclusion relations between zero sets of LAIs. Implication relations between LAIs can be judged by whether their zero set has an inclusion relation just like Definition11 introduced above. The equivalence relations between LAIs can be judged by whether their zero sets have inclusion relations with each other. If the two sets are equal, the two sets contain each other. Before we introduce the reasoning method, we need to introduce the theorems (Lemma 1 and Theorem 1) and two basic mathematical definitions involving our reasoning method.Definition 13 (Convex set).
D⊂ℝn, and let arbitrary x∈Dandy∈D. Dis the convex set, if for, z=λx+1−λy∀λ0≤λ≤1 then z∈D is always true.Definition 14 (Vertex set).
V is a vertex set, if and only if for arbitrary, z∈V , and z∉z′|z′=λx+1−λy,∀x,∀y∈V,∀λ∈0,1.Lemma 1.
The intersection of the zero set of LEI and the first quadrant is a convex set.Proof.
Letf¯x1,…,xn is LEI, and f¯x1,…,xn=a0¯+a1¯x1+a2¯x2+⋯+an¯xn=0, where a0¯=a0−,a0+,a1¯=a1−,a1+,…,an¯=an−,an+.
Let, if arbitraryα∈Zerof¯,β∈Zerof¯,α≠β,(11)α=xα1,xα2,…,xαnT,β=xβ1,xβ2,…,xβnT,then(12)∃aα,∃aβ,aα=aα1,aα2,….,aαnT,aβ=aβ1,aβ2,…,aβnT,aα1∈a1¯,aα2∈a2¯,…,aαn∈an¯,aβ1∈a1¯,aβ2∈a2¯,…,aβn∈an¯.
We have(13)aα0+aα1xα1+⋯+aαnxαn=0,aβ0+aβ1xβ1+⋯+aβnxβn=0.
For arbitraryλ,0≤λ≤1, let λ,1−λ. By multiplying the above two equations, we have(14)λaα0+λaα1xα1+⋯+λaαnxαn=0,1−λaβ0+1−λaβ1xβ1+⋯+1−λaβnxβn=0.
By adding the above two equations, we have(15)λaα0+1−λaβ0+λaα1xα1+1−λaβ1xβ1+⋯+λaαnxαn+1−λaβnxβn=0.
Letλaα0+1−λaβ0=az0.
Apparently,az0=λaα0+1−λaβ0∈minaα0,aβ0,maxaα0,aβ0⊆a0−,a0+.
Letz=λα+1−λβ, following the definition of Zerof¯.
z∈Zerof¯, if and only if(16)∃az1∈a1¯,...,∃azn∈an¯,az0+az1λxα1+1−λxβ1+⋯+aznλxαn+1−λxβn=0.
Let us prove (16).
Takeaz1=λaα1xα1+1−λaβ1xβ1/λxα1+1−λxβ1,…,azn=λaαnxαn+1−λaβnxβn/λxαn+1−λxβn according to (15). Apparently, we have(17)az0+az1λxα1+1−λxβ1+⋯+aznλxαn+1−λxβn=0.
Furthermore, assumingaα1≤aβ1 (the case of aα1>aβ1 is similar), we easily obtain(18)aα1λxα1+1−λxβ1≤λaα1xα1+1−λaβ1xβ1≤aβ1λxα1+1−λxβ1.
Because bothα and β belong to the first quadrant, we have(19)λxα1+1−λxβ1>0.
By dividing (18) by λxα1+1−λxβ1, we obtain(20)aα1≤λaα1xα1+1−λaβ1xβ1λxα1+1−λxβ1≤aβ1,that is,(21)aα1≤az1≤aβ1.
So,az1∈aα1,aβ1⊂a1−,a1+=a1¯.
Similarly,azn∈aαn,aβn⊂an−,an+=an¯.Theorem 1.
the intersection of the zero set of LAI and the first quadrant is a convex set.Proof.
As the definition of LEI, an LAI consists of one LEI or much more LEI.
Letφ¯ be an LAI, (22)φ¯=f1¯x1,…,xn,…,fn¯x1,…,xn,
LetA1 denote the first quadrant area.
Apparently,Zeroφ¯=Zerof1¯∩⋯∩Zerofn¯, and Zerof1¯∩A1,…,Zerofn¯∩A1 are convex sets, following the conclusion of Lemma 1 above.
According to one of the properties of a convex set [35], we find that
Zerof1¯∩A1∩Zerof2¯∩A1∩⋯∩Zerofn¯∩A1 is also a convex set.
That is,A1∩Zerof1¯∩Zerof2¯∩⋯∩Zerofn¯ is also a convex set.
For most engineering problems, only solutions in the first quadrant are meaningful. Although it may be meaningful that the solutions are negative to some problems, it is still possible to make the solution meaningful in the first quadrant through proper coordinate transformation.
For example, ifc represents the temperature value in degrees Celsius, and represents c′ represents the temperature in Kelvin. The coordinate transformation is c′=c+273.15. Apparently, c′ is meaningful only when it is positive. In this article, the zero set of LAIs to which we refer is its intersection with the first quadrant.
Because, ifA and B are both convex sets and p1,p2,…,pn are all vertexes of A, then A⊆Biff∀pi∈B, i=1,2,…,n. Therefore, we can judge whether all of its vertexes are contained by another zero set of LAI to determine whether there is an inclusion relationship between the two sets. We thus obtain the following reasoning method.
Letφ1¯ and φ2¯ be two linear algebraic assertions. Is φ1¯|=φ2¯ correct? A method for judging inclusion relations between the LAI can be given as follows:Step 1. Calculate all vertexes of φ1¯.Step 2. Determine the inequality equations, which are equivalent to the zero set of φ2¯.Step 3. If all vertexes of φ1¯ satisfy the inequalities obtained in Step 2, we have that φ1¯|=φ2¯ is true; otherwise, it is not true.


### 5.2. Reasoning Method Example with LAIs

In this section, we present a case that can be solved by linear algebraic reasoning rules with errors.Let(23)φ1¯=0.9,1X¯+0.8,1Y¯+0.7,1Z¯=0.8,1.2,0.9,1X¯+0.7,1.1Y¯−0.9,1Z¯=0.3,0.4,0.9,1.1X¯−0.7,1.1Y¯+0.9,1Z¯=0.5,0.6,φ2¯=X¯=0.35,0.55,Y¯=0.25,0.4,Z¯=0.2,0.3,We want to know whetherφ2¯|=φ1¯.Proof.
First, we can easily obtain the boundary equations as follows to find all vertexes ofφ1¯:(24)X+Y+Z=0.8,0.9X+0.8Y+0.7Z=1.2,0.9X+0.7Y−Z=0.4,X+1.1Y−0.9Z=0.3,1.1X−0.7Y+Z=0.5,0.9X−1.1Y+0.9Z=0.6.
We obtain three equation systems, each of which contains two equations. An equation is selected arbitrarily from each equation system, so eight groups of equations can be formed. By solving these eight groups of equations, we obtain eight vertexes.
Calculate all vertexes ofφ1¯: p1=9/20,69/340,5/34, p2=549/950,3/50,77/475, p3=9/19,3/50,253/950, p4=81/245,48/245,67/245, p5=284/1253,7971253,872/1253, p7=9/20,1583/2580,1121/2580, and p8=1934/2925,118/325,146/325.
The above eight vertexes ofφ1¯ constitute a hexahedron in 3D space. To mathematically represent the interior region of the hexahedron (including boundary), we need to obtain a group of linear inequalities defining this region. According to the theory of cylindrical algebraic decomposition, all points in a linear closed region isolated by finite points satisfy the same inequalities. To find a point in the interior region of a hexahedron, we need to solve a group of equations, in which the coefficients can take any value within their interval according to Theorem 1, as proven above. If there is no solution or if the solution is not unique for arbitrarily selected coefficients, we can reselect a group of coefficients until the system of equations has a solution.
Find an interior pointPXP,YP,ZP,(25)0.9X+0.9Y+0.9Z=1,X+Y−Z=0.35,X−Y+Z=0.5,⟺PXP,YP,ZP=1740,1136,137360.
PXP,YP,ZP must be in the interior region of the hexahedron (including the boundary), as shown in Figures 2 and 3.
Substituting pointPXP,YP,ZP into formula (24), we obtain three groups of linear inequalities as follows:(26)Xp+Yp+Zp≥0.8,0.9Xp+0.8Yp+0.7Zp≤1.2,0.9Xp+0.7Yp−Zp≤0.4,Xp+1.1Yp−0.9Zp≥0.3,1.1Xp−0.7Yp+Zp≥0.5,0.9Xp−1.1Yp+0.9Zp≤0.6.
Calculate all vertexes ofφ2¯:(27)q1=0.4,0.3,0.3,q2=0.4,0.3,0.4,q3=0.4,0.35,0.3,q4=0.4,0.35,0.4,q5=0.5,0.3,0.3,q6=0.5,0.3,0.4,q7=0.5,0.35,0.3,q8=0.5,0.35,0.4.
According to the properties of convex sets, if all vertexes ofφ2¯ are in the interior region (including the boundary) of the zero set of φ1¯, then Zeroφ2¯⊆Zeroφ1¯.
Take all eight vertexes ofφ2¯ into formula (26) to verify all inequalities in formula (26). We find that only q3 is not satisfied with one inequality of formula (26). For q3, 1.1X−0.7Y+Z≥0.5 does not hold, as 1.1Xq3−0.7Yq3+Zq3=0.495.
So,Zeroφ2¯⊄Zeroφ1¯.
In other words,φ2¯|=φ1¯ does not hold.
If only looking at Figures4 and 5, it seems that all vertexes of φ2¯ are interior regions of the zero set of φ1¯. However, after the above calculations, q3 is almost inside. So it dose not hold.Figure 2
Blue point in the interior.Figure 3
Another angle of Figure2.Figure 4
All vertexes in the area ofφ1¯ and φ2¯.Figure 5
Another angle of Figure4.


## 5.1. Reasoning Method between LAIs

In this section, we present a reasoning method to judge inclusion relations between zero sets of LAIs. Implication relations between LAIs can be judged by whether their zero set has an inclusion relation just like Definition11 introduced above. The equivalence relations between LAIs can be judged by whether their zero sets have inclusion relations with each other. If the two sets are equal, the two sets contain each other. Before we introduce the reasoning method, we need to introduce the theorems (Lemma 1 and Theorem 1) and two basic mathematical definitions involving our reasoning method.Definition 13 (Convex set).
D⊂ℝn, and let arbitrary x∈Dandy∈D. Dis the convex set, if for, z=λx+1−λy∀λ0≤λ≤1 then z∈D is always true.Definition 14 (Vertex set).
V is a vertex set, if and only if for arbitrary, z∈V , and z∉z′|z′=λx+1−λy,∀x,∀y∈V,∀λ∈0,1.Lemma 1.
The intersection of the zero set of LEI and the first quadrant is a convex set.Proof.
Letf¯x1,…,xn is LEI, and f¯x1,…,xn=a0¯+a1¯x1+a2¯x2+⋯+an¯xn=0, where a0¯=a0−,a0+,a1¯=a1−,a1+,…,an¯=an−,an+.
Let, if arbitraryα∈Zerof¯,β∈Zerof¯,α≠β,(11)α=xα1,xα2,…,xαnT,β=xβ1,xβ2,…,xβnT,then(12)∃aα,∃aβ,aα=aα1,aα2,….,aαnT,aβ=aβ1,aβ2,…,aβnT,aα1∈a1¯,aα2∈a2¯,…,aαn∈an¯,aβ1∈a1¯,aβ2∈a2¯,…,aβn∈an¯.
We have(13)aα0+aα1xα1+⋯+aαnxαn=0,aβ0+aβ1xβ1+⋯+aβnxβn=0.
For arbitraryλ,0≤λ≤1, let λ,1−λ. By multiplying the above two equations, we have(14)λaα0+λaα1xα1+⋯+λaαnxαn=0,1−λaβ0+1−λaβ1xβ1+⋯+1−λaβnxβn=0.
By adding the above two equations, we have(15)λaα0+1−λaβ0+λaα1xα1+1−λaβ1xβ1+⋯+λaαnxαn+1−λaβnxβn=0.
Letλaα0+1−λaβ0=az0.
Apparently,az0=λaα0+1−λaβ0∈minaα0,aβ0,maxaα0,aβ0⊆a0−,a0+.
Letz=λα+1−λβ, following the definition of Zerof¯.
z∈Zerof¯, if and only if(16)∃az1∈a1¯,...,∃azn∈an¯,az0+az1λxα1+1−λxβ1+⋯+aznλxαn+1−λxβn=0.
Let us prove (16).
Takeaz1=λaα1xα1+1−λaβ1xβ1/λxα1+1−λxβ1,…,azn=λaαnxαn+1−λaβnxβn/λxαn+1−λxβn according to (15). Apparently, we have(17)az0+az1λxα1+1−λxβ1+⋯+aznλxαn+1−λxβn=0.
Furthermore, assumingaα1≤aβ1 (the case of aα1>aβ1 is similar), we easily obtain(18)aα1λxα1+1−λxβ1≤λaα1xα1+1−λaβ1xβ1≤aβ1λxα1+1−λxβ1.
Because bothα and β belong to the first quadrant, we have(19)λxα1+1−λxβ1>0.
By dividing (18) by λxα1+1−λxβ1, we obtain(20)aα1≤λaα1xα1+1−λaβ1xβ1λxα1+1−λxβ1≤aβ1,that is,(21)aα1≤az1≤aβ1.
So,az1∈aα1,aβ1⊂a1−,a1+=a1¯.
Similarly,azn∈aαn,aβn⊂an−,an+=an¯.Theorem 1.
the intersection of the zero set of LAI and the first quadrant is a convex set.Proof.
As the definition of LEI, an LAI consists of one LEI or much more LEI.
Letφ¯ be an LAI, (22)φ¯=f1¯x1,…,xn,…,fn¯x1,…,xn,
LetA1 denote the first quadrant area.
Apparently,Zeroφ¯=Zerof1¯∩⋯∩Zerofn¯, and Zerof1¯∩A1,…,Zerofn¯∩A1 are convex sets, following the conclusion of Lemma 1 above.
According to one of the properties of a convex set [35], we find that
Zerof1¯∩A1∩Zerof2¯∩A1∩⋯∩Zerofn¯∩A1 is also a convex set.
That is,A1∩Zerof1¯∩Zerof2¯∩⋯∩Zerofn¯ is also a convex set.
For most engineering problems, only solutions in the first quadrant are meaningful. Although it may be meaningful that the solutions are negative to some problems, it is still possible to make the solution meaningful in the first quadrant through proper coordinate transformation.
For example, ifc represents the temperature value in degrees Celsius, and represents c′ represents the temperature in Kelvin. The coordinate transformation is c′=c+273.15. Apparently, c′ is meaningful only when it is positive. In this article, the zero set of LAIs to which we refer is its intersection with the first quadrant.
Because, ifA and B are both convex sets and p1,p2,…,pn are all vertexes of A, then A⊆Biff∀pi∈B, i=1,2,…,n. Therefore, we can judge whether all of its vertexes are contained by another zero set of LAI to determine whether there is an inclusion relationship between the two sets. We thus obtain the following reasoning method.
Letφ1¯ and φ2¯ be two linear algebraic assertions. Is φ1¯|=φ2¯ correct? A method for judging inclusion relations between the LAI can be given as follows:Step 1. Calculate all vertexes of φ1¯.Step 2. Determine the inequality equations, which are equivalent to the zero set of φ2¯.Step 3. If all vertexes of φ1¯ satisfy the inequalities obtained in Step 2, we have that φ1¯|=φ2¯ is true; otherwise, it is not true.


## 5.2. Reasoning Method Example with LAIs

In this section, we present a case that can be solved by linear algebraic reasoning rules with errors.Let(23)φ1¯=0.9,1X¯+0.8,1Y¯+0.7,1Z¯=0.8,1.2,0.9,1X¯+0.7,1.1Y¯−0.9,1Z¯=0.3,0.4,0.9,1.1X¯−0.7,1.1Y¯+0.9,1Z¯=0.5,0.6,φ2¯=X¯=0.35,0.55,Y¯=0.25,0.4,Z¯=0.2,0.3,We want to know whetherφ2¯|=φ1¯.Proof.
First, we can easily obtain the boundary equations as follows to find all vertexes ofφ1¯:(24)X+Y+Z=0.8,0.9X+0.8Y+0.7Z=1.2,0.9X+0.7Y−Z=0.4,X+1.1Y−0.9Z=0.3,1.1X−0.7Y+Z=0.5,0.9X−1.1Y+0.9Z=0.6.
We obtain three equation systems, each of which contains two equations. An equation is selected arbitrarily from each equation system, so eight groups of equations can be formed. By solving these eight groups of equations, we obtain eight vertexes.
Calculate all vertexes ofφ1¯: p1=9/20,69/340,5/34, p2=549/950,3/50,77/475, p3=9/19,3/50,253/950, p4=81/245,48/245,67/245, p5=284/1253,7971253,872/1253, p7=9/20,1583/2580,1121/2580, and p8=1934/2925,118/325,146/325.
The above eight vertexes ofφ1¯ constitute a hexahedron in 3D space. To mathematically represent the interior region of the hexahedron (including boundary), we need to obtain a group of linear inequalities defining this region. According to the theory of cylindrical algebraic decomposition, all points in a linear closed region isolated by finite points satisfy the same inequalities. To find a point in the interior region of a hexahedron, we need to solve a group of equations, in which the coefficients can take any value within their interval according to Theorem 1, as proven above. If there is no solution or if the solution is not unique for arbitrarily selected coefficients, we can reselect a group of coefficients until the system of equations has a solution.
Find an interior pointPXP,YP,ZP,(25)0.9X+0.9Y+0.9Z=1,X+Y−Z=0.35,X−Y+Z=0.5,⟺PXP,YP,ZP=1740,1136,137360.
PXP,YP,ZP must be in the interior region of the hexahedron (including the boundary), as shown in Figures 2 and 3.
Substituting pointPXP,YP,ZP into formula (24), we obtain three groups of linear inequalities as follows:(26)Xp+Yp+Zp≥0.8,0.9Xp+0.8Yp+0.7Zp≤1.2,0.9Xp+0.7Yp−Zp≤0.4,Xp+1.1Yp−0.9Zp≥0.3,1.1Xp−0.7Yp+Zp≥0.5,0.9Xp−1.1Yp+0.9Zp≤0.6.
Calculate all vertexes ofφ2¯:(27)q1=0.4,0.3,0.3,q2=0.4,0.3,0.4,q3=0.4,0.35,0.3,q4=0.4,0.35,0.4,q5=0.5,0.3,0.3,q6=0.5,0.3,0.4,q7=0.5,0.35,0.3,q8=0.5,0.35,0.4.
According to the properties of convex sets, if all vertexes ofφ2¯ are in the interior region (including the boundary) of the zero set of φ1¯, then Zeroφ2¯⊆Zeroφ1¯.
Take all eight vertexes ofφ2¯ into formula (26) to verify all inequalities in formula (26). We find that only q3 is not satisfied with one inequality of formula (26). For q3, 1.1X−0.7Y+Z≥0.5 does not hold, as 1.1Xq3−0.7Yq3+Zq3=0.495.
So,Zeroφ2¯⊄Zeroφ1¯.
In other words,φ2¯|=φ1¯ does not hold.
If only looking at Figures4 and 5, it seems that all vertexes of φ2¯ are interior regions of the zero set of φ1¯. However, after the above calculations, q3 is almost inside. So it dose not hold.Figure 2
Blue point in the interior.Figure 3
Another angle of Figure2.Figure 4
All vertexes in the area ofφ1¯ and φ2¯.Figure 5
Another angle of Figure4.


## 6. Verification of Decentralized Power Systems during Turn

In this section, we present a case that can be solved by the reasoning method mentioned above in this article. The problem in four or eight carriages can be solved by a recursive 2-carriage problem. Hence, we mainly discuss the power decentralization of 2 carriages.A simplified algebraic transition system for the train is shown in Figure6. g1¯ and g2¯ represent the conditions satisfied by corresponding transitions between the states. φ1¯, φ2¯ and φ3¯ are the equations that need to be satisfied in the corresponding states. That is, when the train is in the acceleration state and if φ1¯ is not satisfied, there is a strong possibility that the train is in an abnormal acceleration process, which requires timely troubleshooting.Figure 6
Algebraic transition system of a train.The following case is when a constant-speed train is turning. Decentralized power systems are widely used in high-speed trains. The power source is scattered among the engines of the carriages. The net traction power of each compartment in a train will vary randomly within a small range, caused by the movement of passengers, their luggage, and wind resistance. The role of the wheel flange of the train is to prevent derailment, especially when the train is turning. The force analysis during turning is shown in Figure6.The two self-powered carriages at constant speed are shown in Figure7. Carriage 1 and carriage 2 may be two connected carriages or two groups of carriages. We have the following description: f1 and f2 denote the traction force of carriage 1 and carriage 2, respectively; m denotes the initial mass of each carriage; and Δm denotes the quality change in each carriage due to the variation of passengers and their luggage and is similar to the effect of mass change. When a train passes the inclined plane in turning, a part of the gravity caused by a certain inclination provides the centripetal force for the train to turn, which is also similar to the change in the mass of the train. μ stands for the friction coefficient; f12 denotes the force of carriage 1 on carriage 2; g is the acceleration due to gravity; and fw denotes the combined force of all wheel flanges of the two carriages on their wheels. Wheel flange is a special device to reduce risks when turning. It is shown in Figure 8. When the train turns quickly, fw may exceed the force limit of the wheel flange, which may cause the train to derail. Moreover, a larger fw will increase the friction between the wheel flanges and the rail and cause injures on the wheel flange of both rail flats. Injured rails and wheels further increase the possibility of derailment when turning. Therefore, fw should be within a certain range. ζ is related to the air density and the shape of the train. Among them, the air density may change due to different altitudes. Therefore, ζ is also defined within a certain range.Figure 7
Two self-powered carriages turning.Figure 8
Train turning.It is assumed that the above parameters require the following values according to the design requirements of the train:m=50000kg, Δm=0,0.2m, μ=0.01, f12=0,2000N, θ=10°, g=10m⋅s−2, ζ=1.5,1.6kg⋅m−1, R=3000m, and fw=−10000,10000N.According to mechanics, we have(28)φ¯=f1+f2=2m+Δmgμ+ζv2,−f12+f1=m+Δmgμ+ζv2,m+Δmv2R−gtanθ=fw.From the third equation in (28), we obtain(29)v2R−gtanθ=fwm1,1.2=−0.2,0.2,v2=Rgtanθ−0.2,gtanθ+0.2.LetRgtanθ−0.2=v−2 and Rgtanθ+0.2=v+2.Then,v2=v−2,v+2.That is,(30)φ¯=f1+f2−ζv2=2m1,1.2gμ,f1−ζv2=m1,1.2gμ+f12,v2=v−2,v+2.The boundary equation of each equation inφ¯ can be obtained as follows, which can solve all vertexes of φ¯:(31)f1+f2−1.5v2=10000,f1+f2−1.6v2=12000,f1−1.5v2=5000,f1−1.6v2=8000,v2=v−2=300010tan10°−0.2,v2=v+2=300010tan10°+0.2.We obtain three equation groups, each of which contains two equations. Select an equation arbitrarily from each equation system, so eight equation systems can be formed. Solving these eight equations, we can obtain eight vertexes.Calculate all vertexes ofφ1¯f1,f2,v2:(32)p1=5000+1.5v−2,5000,v−2≈12034.7,5000,4689.8,p2=5000+1.5v+2,5000,v+2≈13834.7,5000,5889.8,p3=8000+1.6v−2,2000−0.1v−2,v−2≈15503.69,1531,4689.8,p4=8000+1.6v+2,2000−0.1v+2,v+2≈17423.69,1411,5889.8,p5=5000+1.5v−2,7000+0.1v−2,v−2≈12034.7,7468.98,4689.8,p6=5000+1.5v+2,7000+0.1v+2,v+2≈13834.7,7588.98,5889.8,p7=8000+1.6v−2,4000,v−2≈15503.69,4000,4689.8,p8=8000+1.6v+2,4000,v+2≈17423.69,4000,5889.8.As before, the above eight vertexes ofφ¯ constitute a hexahedron in 3D space. To mathematically represent the interior region of the hexahedron (including boundary), we need to obtain a group of linear inequalities of this region. According to the theory of cylindrical algebraic decomposition, all points in a linear closed region isolated by finite points satisfy the same inequalities. To find a point in the interior region of a hexahedron, we just need to solve a group of equations, in which coefficients can take any value of their interval according to Theorem 1.An interior pointPf1′,f2′,v2′ can be solved by equations with certain coefficients in the allowable error range. Without losing generality, Pf1′,f2′,v2′ can be solved by the following equations:(33)f1+f2−1.55v2=1.1⋅2mgμ,f1−1.55v2=1.1⋅mgμ+1000,1.1mv2R−gtanθ=0.⟺Pf1′,f2′,v2′≈14699.20,4500,5289.81,By substituting pointPf1′,f2′,v2′ into formula (31), we obtain the following three groups of linear inequalities:(34)f1+f2−1.5v2≥10000,f1+f2−1.6v2≤12000,f1−1.5v2≥5000,f1−1.6v2≤8000,v2≥v−2=300010tan10°−0.2,v2≤v+2=300010tan10°+0.2.The inequality groups in formula (34) represent the fault-tolerance area of the system, which is the area where the system allows controllable errors. The fault-tolerance area is shown in Figures 9 and 10.Figure 9
The fault-tolerance area of the system.Figure 10
Another angle of Figure9.We can verify whetherf1, f2, and v2 satisfy the inequality group in formula (34) to judge whether the decentralized power systems and train speed are working properly. Whenf1, f2, and v2 do not satisfy formula (34), the decentralized power system or train speed is probably working incorrectly and requires timely error detection.In the fault-tolerance area, the interval number ofv2 can be transformed into an interval number of v. The equivalent fault-tolerance area will not be described again:(35)v2≈4689.8,5889.8⇔v≈68.48,76.74m⋅s−1⟺v≈246.52,276.26km⋅h−1.


## 7. Simulation and Comparison

### 7.1. Simulation

In this section, we test the fault-tolerance area in Section6. Δm denotes the quality change; ζ is related to the air density and the shape of the train; fw denotes the combined force of all wheel flanges of the two carriages on their wheels; and f12 denotes the force of carriage 1 on carriage 2. There are four parameters (Δmζfwf12) with errors in (28). The meanings of these four uncertain parameters are the same as those in Section 6. Therefore, it will not be described in detail here. The four interval numbers are as follows:(36)Δm=0,10000,ζ=1.5,1.6,fw=−10000,10000,f12=0,2000.An arbitrary test case refers to randomly assigned values for the four parameters. The N test cases can be described by the following formula:(37)case1=Δm1,ζ1,fw1,f121,…,casen=Δmn,ζn,fwn,f12n.By substituting formula (37) into formula (28), we can obtain the solutions of the corresponding test cases as the following formula:(38)solution1=f11,f21,v12…,solutionn=f1n,f2n,vn2.By substituting formula (38) into formula (28), we can verify the correctness of the fault-tolerance area. After testing, the solutions of all test cases are inside the fault-tolerance area, including its boundary. Figures 11(a) and 11(b) show that the solutions of these 1000 test cases are all inside the fault-tolerance area. Figures 11(c) and 11(d) show that the solutions of these 10,000 and 100,000 test cases.Figure 11
(a) 1000 test cases; (b) another angle of (a); (c) 10,000 test cases; (d) 100,000 test cases.
(a)(b)(c)(d)When the number of test cases is 10,000 and 100,000, the same conclusion is obtained, as shown in Figures11(c) and 11(d), respectively.The sensitivities of these four uncertain parameters are different. The change of mass and air coefficient is the most sensitive to safety conditions. For example, China’s Fuxing high-speed railway has strict limits on the number of passengers.


### 7.2. Comparison

Previous reasoning methods based on algebraic polynomials have mainly concentrated on nonerror systems [9, 12–15], whose coefficients and variables are accurately described. For systems with errors in coefficients and variables, most previous methods are incompetent. However, the method of Reference [16] is very valuable in theory but is only effective for a single variable or coefficient with error not for multiple error variables or coefficients. Among the fault-tolerant methods, there are many similar fault-tolerant error analysis methods [23–25], but formal reasoning methods are rarely reported.


## 7.1. Simulation

In this section, we test the fault-tolerance area in Section6. Δm denotes the quality change; ζ is related to the air density and the shape of the train; fw denotes the combined force of all wheel flanges of the two carriages on their wheels; and f12 denotes the force of carriage 1 on carriage 2. There are four parameters (Δmζfwf12) with errors in (28). The meanings of these four uncertain parameters are the same as those in Section 6. Therefore, it will not be described in detail here. The four interval numbers are as follows:(36)Δm=0,10000,ζ=1.5,1.6,fw=−10000,10000,f12=0,2000.An arbitrary test case refers to randomly assigned values for the four parameters. The N test cases can be described by the following formula:(37)case1=Δm1,ζ1,fw1,f121,…,casen=Δmn,ζn,fwn,f12n.By substituting formula (37) into formula (28), we can obtain the solutions of the corresponding test cases as the following formula:(38)solution1=f11,f21,v12…,solutionn=f1n,f2n,vn2.By substituting formula (38) into formula (28), we can verify the correctness of the fault-tolerance area. After testing, the solutions of all test cases are inside the fault-tolerance area, including its boundary. Figures 11(a) and 11(b) show that the solutions of these 1000 test cases are all inside the fault-tolerance area. Figures 11(c) and 11(d) show that the solutions of these 10,000 and 100,000 test cases.Figure 11
(a) 1000 test cases; (b) another angle of (a); (c) 10,000 test cases; (d) 100,000 test cases.
(a)(b)(c)(d)When the number of test cases is 10,000 and 100,000, the same conclusion is obtained, as shown in Figures11(c) and 11(d), respectively.The sensitivities of these four uncertain parameters are different. The change of mass and air coefficient is the most sensitive to safety conditions. For example, China’s Fuxing high-speed railway has strict limits on the number of passengers.


## 7.2. Comparison

Previous reasoning methods based on algebraic polynomials have mainly concentrated on nonerror systems [9, 12–15], whose coefficients and variables are accurately described. For systems with errors in coefficients and variables, most previous methods are incompetent. However, the method of Reference [16] is very valuable in theory but is only effective for a single variable or coefficient with error not for multiple error variables or coefficients. Among the fault-tolerant methods, there are many similar fault-tolerant error analysis methods [23–25], but formal reasoning methods are rarely reported.


## 8. Conclusion

Our main contribution is to show that the reasoning method is reliable and the error controllable, even though errors exist in the coefficients and variables in the linear assertion. Furthermore, the method proposed in this paper is not limited only to the verification of decentralized power systems, as errors in many systems are common and unavoidable. This method is promising in systems described by linear equations with error parameters. In such systems, our method may remain effective by using linear equations to approximate the nonlinearity within a small time interval. Hence, the method in this study has a wide range of applications.Nevertheless, if not to approximate the nonlinearity of the system by linear equations within a small time interval, our reasoning method may not be applicable to these nonlinear systems with errors. This is also the focus of our work in the future.



---

*Source: 6624528-2021-01-04.xml*