# Approximate Analyzing of Labeled Transition Systems

Authors: Qiong Yu; Shihan Yang; Jinzhao Wu
Journal: Mathematical Problems in Engineering
 (2015)

---

## Abstract

As the most important formal semantic model, labeled transition systems are
widely used, which can describe the general concurrent systems or control systems
without disturbance. However, under normal circumstance, transition systems
are complex and difficult to use due to large amount of calculation and the state
space explosion problems. In order to overcome these problems,  approximate
equivalent labeled transition systems are proposed by means of incomplete low-up
matrix decomposition factorization. This technique can reduce the complexity of
computation and calculate under the allowing errors. As for continuous-time linear
systems, we develop a modeling method of approximated transition system based
on the approximate solution of matrix, which provides a facility for approximately
formal semantic modeling for linear systems and to effectively analyze errors.
An example of application in the context of linear systems without disturbances is
studied.


---

## Body

## 1. Introduction

Transition system is an important formal model of concurrent systems, which is widely used in concurrency theory, such as petri nets and process algebras. Petri nets can be used as a graphical tool to simulate the dynamic behavior and concurrent activities of the systems and also can be used as a mathematical tool to establish mathematical model describing the behaviors of the systems. It is a widely transition system and gives a method to describe Petri net using classical transition system [1]. Apart from Petri net theory, there is a process algebra, which is used to describe and study concurrent or distributed system behavior theory by algebraic methods. Thus, many process algebraic systems are proposed. Among them, the first is to propose the following three process algebra systems: CCS (Calculus of Communicating Systems) proposed by Milner [2, 3], CSP (Communicating Sequential Processes) proposed by Hoare [4], and ACP (Algebra of Communicating Processes) proposed by Baeten and Weijland [5]. In recent years, some new process calculus systems have been proposed. For example, probabilistic process algebra [6–12] and stochastic process algebra [13] are proposed to describe possible or random information; real-time process algebra [14–17] is proposed to describe the action time. In the field of process algebra, as the most important semantic model, the transition system is widely used, especially labeled transition system [18], which can describe the general behavior of concurrent systems.Approximation of transition systems has recently been introduced as a powerful tool for the approximation of continuous systems. The notion of simulation is one such formal notion of abstraction that has been used for reducing the complexity of finite state systems such as labeled transition systems. Approximation of purely discrete systems has traditionally been based on language inclusion and equivalence with notions such as simulation or bisimulation relations [19]. These concepts have been useful for simplifying problems such as safety verification or controller synthesis. However, in the cases that the quality requirements of simulation or bisimulation are so exacting sometimes it is so difficult for us to construct finite abstracts with the original system simulation or bisimulation. Although finite abstract with the original system approximate simulation or approximate bisimulation is easy to construct, these methods can only ensure that the system approximately satisfies the given range and is not able to calculate the allowable error of transition between states. To solve this problem, this paper puts forward a design method for transition system—approximate simulation method based on ILU.As a particular class of preconditioners, incomplete factorizations can be thought of as approximating the exactLU factorization of a given matrix (e.g., computed via Gaussian elimination) by disallowing certain filling of this. As opposed to other PDE-based preconditioners such as multigrid and domain decomposition, this class of preconditioners is primarily algebraic in nature and can be applied to any matrices in principle. However, one of the basic methods of preconditioned method is the use of incomplete LU decomposition. The most well known is the incomplete triangular decomposition ILU0 [20] that has nothing more than zero-element filling. Since ILU0 unchanged the structure of sparse matrix, the application of ILU0 is very convenient. However, because of this, it is so rough approximation of the coefficient matrix that the effectiveness of ILU0 is limited. To improve the approximation, filling with nonzero elements is allowed [21, 22]. While the ILU preconditioner works quite well for many problems, it does not perform well for some PDE problems [23]. Then, the generalization of this modified ILU (MILU) preconditioner is proposed by Gustafsson [24]. MILU is to add the fill-ins abandoned by ILU back to the diagonal type, which makes up for inaccuracies caused by discarded. And its accuracy can be calculated. However, mathematically, the transition between states can be described by matrix, and then the allowable error of the approximate transition is needed to be characterized. Furthermore, the allowable error can be defined by the MILU accuracy.In the rest of this paper, Section2 reviews the approximate simulation relations of transition systems. In Section 3, the approximate and incomplete factorizations are recalled. In Section 4, the approximate equivalent of labeled transition systems is proposed in detail. Section 5 proposes the theory of the approximate labeled transition systems. In Section 6, a case is studied. Then Section 7 draws the conclusion.


## 2. Approximation of Transition Systems

### 2.1. Labeled Transition Systems

We know that labeled transition systems allow modeling, in a unified framework, discrete, continuous, and hybrid systems. The main results [25] are reviewed here.Definition 1.
A labeled transition system with observation is a tupleT=(Q,Σ,→,Q0,Π,·) that consists of(i)
a setQ of states,(ii)
a setΣ of labels,(iii)
a transition relation→⊆Q×Σ×Q,(iv)
a setQ0⊆Q of initial states,(v)
a setΠ of observations,(vi)
an observation map·:Q→Π.
A state trajectory ofT is a sequence of transitions, (1)q0⟶σ0q1⟶σ1q2⟶σ2⋯,whereq0∈Q0,qi∈Q,σi-1∈Σ,i=1,2,….
For a given initial state and sequence of labels, there may exist several state trajectories ofT. Thus, the systems we consider are possibly nondeterministic. The associated external trajectory (2)π0⟶σ0π1⟶σ1π2⟶σ2⋯,whereπi=qi,i=0,1,2,…,describes the evolution of the observations under the dynamics of the labeled transition system.
The set of external trajectories of the labeled systemT is called the language of T and is denoted by L(T). The subset of Π reachable by the external trajectories of T is denoted by Reach(T): (3)ReachT=π∈Π∣∃π0⟶σ0π1⟶σ1π2⟶σ2⋯∈LT,∃j∈N,πj=π,where N is the set of positive integers.
An important problem for transition systems is the safety verification problem which consists in checking whether the reachable set Reach(T) intersects a set of observations ΠU associated with unsafe states.


### 2.2. Approximate Simulation Relations

Exact simulation relations between two labeled transition systems require that their observations are (and remain) identical. Approximate simulation relations are less rigid since they only require that the observations of both systems are (and remain) arbitrarily close.LetT1=(Q1,Σ1,→1,Q10,Π1,·1) and T2=(Q2,Σ2,→2,Q20,Π2,·2) be two labeled transition systems with the same set of labels (Σ1=Σ2=Σ) and the same set of observations (Π1=Π2=Π) (i.e., T1 and T2 are elements of T(Σ,Π)). Let us assume that the set of observation Π is a metric space; dΠ denotes the metric of Π.Definition 2.
A metric of a setA is a positive function d:A×A→R∪+∞, where R is the set of real numbers, such that the three following properties hold: for all x,y,z∈A(1)
d(x,y)=0 if and only if x=y,(2)
d(x,y)=d(y,x),(3)
d(x,z)≤d(x,y)+d(y,z).
If the second property is replaced byx=y⇒d(x,y)=0 then d is called a pseudometric. If the third property is dropped, then d is called a directed metric.Definition 3.
A relationSδ⊆Q1×Q2 is a δ-approximate simulation relation of T1 by T2 if for all (q1,q2)∈Sδ(1)
dΠ(q11,q22)≤δ,(2)
∀q1→σ1q1′,∃q2→σ2q2′ such that (q1′,q2′)∈Sδ.
Note that, in there,→1 describes a transition relation of T1, →2 describes a transition relation of T2, q1′ represents the next state of q1, q2′ represents the next state of q2, and σ∈Σ. And that, for δ=0, we have the usual notion of exact simulation relation.Definition 4.
T
2 approximately simulates T1 with the precision δ (noted T1⪯δT2), if there exists Sδ, a δ-approximate simulation relation of T1 by T2 such that, for all q1∈Q10, there exists q2∈Q20 such that (q1,q2)∈Sδ.
IfT2 approximately simulates T1 with the precision δ then the language of T1 is approximated with precision δ by the language of T2.Theorem 5.
IfT1⪯δT2, then for all external trajectories of T1,(4)π10⟶σ0π11⟶σ1π12⟶σ2⋯,there exists an external trajectory of T2 with the same sequence of labels(5)π20⟶σ0π21⟶σ1π22⟶σ2⋯such that, for all i∈N, dΠ(π1i,π2i)≤δ.In Theorem5, if T2 approximately simulates T1 with the precision δ, there must exist a state of T2 approximate simulation the state of T1. But it is very difficult for us to calculate the degree of approximation.


## 2.1. Labeled Transition Systems

We know that labeled transition systems allow modeling, in a unified framework, discrete, continuous, and hybrid systems. The main results [25] are reviewed here.Definition 1.
A labeled transition system with observation is a tupleT=(Q,Σ,→,Q0,Π,·) that consists of(i)
a setQ of states,(ii)
a setΣ of labels,(iii)
a transition relation→⊆Q×Σ×Q,(iv)
a setQ0⊆Q of initial states,(v)
a setΠ of observations,(vi)
an observation map·:Q→Π.
A state trajectory ofT is a sequence of transitions, (1)q0⟶σ0q1⟶σ1q2⟶σ2⋯,whereq0∈Q0,qi∈Q,σi-1∈Σ,i=1,2,….
For a given initial state and sequence of labels, there may exist several state trajectories ofT. Thus, the systems we consider are possibly nondeterministic. The associated external trajectory (2)π0⟶σ0π1⟶σ1π2⟶σ2⋯,whereπi=qi,i=0,1,2,…,describes the evolution of the observations under the dynamics of the labeled transition system.
The set of external trajectories of the labeled systemT is called the language of T and is denoted by L(T). The subset of Π reachable by the external trajectories of T is denoted by Reach(T): (3)ReachT=π∈Π∣∃π0⟶σ0π1⟶σ1π2⟶σ2⋯∈LT,∃j∈N,πj=π,where N is the set of positive integers.
An important problem for transition systems is the safety verification problem which consists in checking whether the reachable set Reach(T) intersects a set of observations ΠU associated with unsafe states.


## 2.2. Approximate Simulation Relations

Exact simulation relations between two labeled transition systems require that their observations are (and remain) identical. Approximate simulation relations are less rigid since they only require that the observations of both systems are (and remain) arbitrarily close.LetT1=(Q1,Σ1,→1,Q10,Π1,·1) and T2=(Q2,Σ2,→2,Q20,Π2,·2) be two labeled transition systems with the same set of labels (Σ1=Σ2=Σ) and the same set of observations (Π1=Π2=Π) (i.e., T1 and T2 are elements of T(Σ,Π)). Let us assume that the set of observation Π is a metric space; dΠ denotes the metric of Π.Definition 2.
A metric of a setA is a positive function d:A×A→R∪+∞, where R is the set of real numbers, such that the three following properties hold: for all x,y,z∈A(1)
d(x,y)=0 if and only if x=y,(2)
d(x,y)=d(y,x),(3)
d(x,z)≤d(x,y)+d(y,z).
If the second property is replaced byx=y⇒d(x,y)=0 then d is called a pseudometric. If the third property is dropped, then d is called a directed metric.Definition 3.
A relationSδ⊆Q1×Q2 is a δ-approximate simulation relation of T1 by T2 if for all (q1,q2)∈Sδ(1)
dΠ(q11,q22)≤δ,(2)
∀q1→σ1q1′,∃q2→σ2q2′ such that (q1′,q2′)∈Sδ.
Note that, in there,→1 describes a transition relation of T1, →2 describes a transition relation of T2, q1′ represents the next state of q1, q2′ represents the next state of q2, and σ∈Σ. And that, for δ=0, we have the usual notion of exact simulation relation.Definition 4.
T
2 approximately simulates T1 with the precision δ (noted T1⪯δT2), if there exists Sδ, a δ-approximate simulation relation of T1 by T2 such that, for all q1∈Q10, there exists q2∈Q20 such that (q1,q2)∈Sδ.
IfT2 approximately simulates T1 with the precision δ then the language of T1 is approximated with precision δ by the language of T2.Theorem 5.
IfT1⪯δT2, then for all external trajectories of T1,(4)π10⟶σ0π11⟶σ1π12⟶σ2⋯,there exists an external trajectory of T2 with the same sequence of labels(5)π20⟶σ0π21⟶σ1π22⟶σ2⋯such that, for all i∈N, dΠ(π1i,π2i)≤δ.In Theorem5, if T2 approximately simulates T1 with the precision δ, there must exist a state of T2 approximate simulation the state of T1. But it is very difficult for us to calculate the degree of approximation.


## 3. Approximate and Incomplete Factorizations

The general problem of finding a preconditioner for a large sparse linear systemAx=b is to find a matrix M (the preconditioner). However, the matrix M should be with the following properties:(i)
M is a nonsingular matrix,(ii)
M is a good approximation to A in some sense,(iii)
the systemMx=b is much easier to solve than the original system Ax=b,(iv)
the construction ofM has some memory and CPU needs protection,(v)
the condition number of theM-1A is much less than that of A, and its minimum singular value becomes larger.That is, we are looking for a nearby problem which is easier to solve than the given one. The idea is to look for a matrixM such that the original linear system Ax=b is transformed into an equivalent linear system M-1Ax=M-1b. Mathematically, we will solve the preconditioned system M-1Ax=M-1b (or the symmetric version (M-1/2AM-1/2)(M1/2x)=M-1/2b when both A and M are symmetric positive definite) by standard iterative methods (such as the conjugate gradient method), in which only the actions of A and M-1 are needed.There are several preconditions: matrix splitting preconditioner, polynomial preconditioners, incomplete factorization preconditioners, approximate inverse preconditioners, and multilevel preconditioners. Here, we mainly focus on incomplete factorization preconditioners, which can be applied to a general purpose. They can be thought of as modifications of Gaussian Elimination, in which some sparse mode is required as the decomposition of matrices, such as making some of the special position of the elements be zero and also abandoning some absolute value in the process of decomposition of minor elements in order to ensure that sparse decomposition.


### 3.1. Incomplete Low-Up Matrix Decomposition (ILU)

The most common type of incomplete factorization is based on taking a setS of matrix positions and keeping all positions outside this set equal to zero during the factorization. The resulting factorization is incomplete in the sense that fill is suppressed.Definition 6.
A matrixA, if A=LU, where L (U) is the lower (upper) triangular sparse matrix, is called a complete decomposition of the matrix A, that is, LU [26].Definition 7.
A matrixA, if A=LU+R, where L (U) is the lower (upper) triangular sparse matrix, is called an incomplete decomposition of the matrix A, that is, ILU. Here R is called error matrix [27].
Let the allowable fill-in positions be given by the index setS; that is,(1)
li,j=0 if j>i or (i,j)∈¯S; ui,j=0 if i>j or (i,j)∈¯S.A commonly used strategy is to defineS by(2)
S=i,j∣ai,j≠0.That is, the only nonzeros allowed in theLU factors are those for which the corresponding entries in A are nonzero. Let the preconditioner M be defined by the product of the resulting LU factors, that is, M=LU. If M becomes a good preconditioner, it must be a good approximation to A in some measure. A typical strategy is to require the entries of M to match those of A on the set S:(3)
mi,j=ai,j if (i,j)∈S.Even though conditions (1) and (3) together are sufficient (for certain classes of matrices) to determine the nonzero entries ofL and U directly, it is more natural and simpler to compute these entries based on a simple modification of the Gaussian elimination algorithm. Matrix A is decomposed into L and U by the incomplete LU. And the corresponding entries of L and U are the same as those obtained by setting those entries of the full LU factors which belong to S. However, the incomplete LU factors of A, respectively, with the lower and upper triangular part of the matrix A, have the same nonzero structure.The constructing process of ILU precondition is in the process of Gaussian elimination by discarding partially filled elements to get sparse triangular matrixesL and U such that M=LU. From the decomposition of ILU we can see that the preconditioners M and A have the same nonzero structure. Therefore, the error matrix R=A-LU=A-M and the main difference from the usual Gaussian elimination lie in how to discard fill-ins in the Gaussian elimination.


### 3.2. Modified Incomplete Low-Up Matrix Decomposition (MILU)

While the ILU preconditioner works quite well for many problems, it does not perform well for some problems. We will next describe the generalization of this modified ILU (MILU) preconditioner to a general matrixA [28].The basic idea is that in condition (3), for ILU, the conditionmi,i=ai,i is removed and a new row sum condition is added. That is, (3) is replaced by(4)
∑j=1nmi,j=∑j=1nai,j∀i and mi,j=ai,j if i≠j and (i,j)∈S.Again, for certain classes of matrices, conditions (4) and (1) are sufficient to determine theLU factors in MILU directly. However, in practice it is easier to compute these LU factors by a modification of the ILU algorithm: instead of dropping the disallowed fill-ins in the ILU algorithm, these terms are added to the diagonal of the same row. Furthermore, the idea of MILU is to make up for inaccuracies caused by discarded by using fill-ins plus backup to cover the diagonal type.Incomplete factorization preconditioners can be portrayed accuracy and stability. Here, accuracy refers to the degree of preconditionerM and matrix A can be measured by the size of M-AF. And stability refers to the degree of preconditioner M and the unit matrix E can be measured by the size of E-M-1AF (for the left preconditioner). Below we give algorithm ILU and algorithm MILU [29].From the analysis of Algorithms1 and 2, the difference between algorithm ILU and MILU is that certain fill-ins given up in algorithm ILU are back to the main diagonal.Algorithm 1:Algorithm ILU.
(1) for  r≔ 1 Step i until  n-1  do
(2)  d≔ 1/ar,r;
(3)  for  i≔  (r+1) Step (1) until  n  do
(4)    if (i,r) ∈ S then;
(5)    e≔dai,r;  ai,r≔e;
(6)    for  j≔ (r+1) Step (1) until  n  do
(7)      if (i,j) ∈ S and (r,j) ∈ S then;
(8)      ai,j≔ai,j-ear,j;
(9)      end if;
(10)    end for  (j-loop);
(11)    end if;
(12)  end for  (i-loop);
(13) end for   (r-loop);Algorithm 2:Algorithm MILU.
(
1) for  r≔1 Step (1) until n-1  do
(2)  d≔1/ar,r;
(3)  for  i≔(r+1) Step (1) until n  do
(4)   if (i,r)∈S then;
(5)   e≔dai,r; ai,r≔e;
(6)   for  j≔(r+1) Step (1) until n  do
(7)    if (r,j)∈S then;
(8)    if (i,j)∈S then;
(9)    ai,j≔ai,j-ear,j;
(10)   else;
(11)    ai,i≔ai,i-ear,j;
(12)   end if;
(13)    end if;
(14)   end for  (j-loop)
(15)   end if;
(16) end for  (i-loop);
(17) end for  (r-loop);


## 3.1. Incomplete Low-Up Matrix Decomposition (ILU)

The most common type of incomplete factorization is based on taking a setS of matrix positions and keeping all positions outside this set equal to zero during the factorization. The resulting factorization is incomplete in the sense that fill is suppressed.Definition 6.
A matrixA, if A=LU, where L (U) is the lower (upper) triangular sparse matrix, is called a complete decomposition of the matrix A, that is, LU [26].Definition 7.
A matrixA, if A=LU+R, where L (U) is the lower (upper) triangular sparse matrix, is called an incomplete decomposition of the matrix A, that is, ILU. Here R is called error matrix [27].
Let the allowable fill-in positions be given by the index setS; that is,(1)
li,j=0 if j>i or (i,j)∈¯S; ui,j=0 if i>j or (i,j)∈¯S.A commonly used strategy is to defineS by(2)
S=i,j∣ai,j≠0.That is, the only nonzeros allowed in theLU factors are those for which the corresponding entries in A are nonzero. Let the preconditioner M be defined by the product of the resulting LU factors, that is, M=LU. If M becomes a good preconditioner, it must be a good approximation to A in some measure. A typical strategy is to require the entries of M to match those of A on the set S:(3)
mi,j=ai,j if (i,j)∈S.Even though conditions (1) and (3) together are sufficient (for certain classes of matrices) to determine the nonzero entries ofL and U directly, it is more natural and simpler to compute these entries based on a simple modification of the Gaussian elimination algorithm. Matrix A is decomposed into L and U by the incomplete LU. And the corresponding entries of L and U are the same as those obtained by setting those entries of the full LU factors which belong to S. However, the incomplete LU factors of A, respectively, with the lower and upper triangular part of the matrix A, have the same nonzero structure.The constructing process of ILU precondition is in the process of Gaussian elimination by discarding partially filled elements to get sparse triangular matrixesL and U such that M=LU. From the decomposition of ILU we can see that the preconditioners M and A have the same nonzero structure. Therefore, the error matrix R=A-LU=A-M and the main difference from the usual Gaussian elimination lie in how to discard fill-ins in the Gaussian elimination.


## 3.2. Modified Incomplete Low-Up Matrix Decomposition (MILU)

While the ILU preconditioner works quite well for many problems, it does not perform well for some problems. We will next describe the generalization of this modified ILU (MILU) preconditioner to a general matrixA [28].The basic idea is that in condition (3), for ILU, the conditionmi,i=ai,i is removed and a new row sum condition is added. That is, (3) is replaced by(4)
∑j=1nmi,j=∑j=1nai,j∀i and mi,j=ai,j if i≠j and (i,j)∈S.Again, for certain classes of matrices, conditions (4) and (1) are sufficient to determine theLU factors in MILU directly. However, in practice it is easier to compute these LU factors by a modification of the ILU algorithm: instead of dropping the disallowed fill-ins in the ILU algorithm, these terms are added to the diagonal of the same row. Furthermore, the idea of MILU is to make up for inaccuracies caused by discarded by using fill-ins plus backup to cover the diagonal type.Incomplete factorization preconditioners can be portrayed accuracy and stability. Here, accuracy refers to the degree of preconditionerM and matrix A can be measured by the size of M-AF. And stability refers to the degree of preconditioner M and the unit matrix E can be measured by the size of E-M-1AF (for the left preconditioner). Below we give algorithm ILU and algorithm MILU [29].From the analysis of Algorithms1 and 2, the difference between algorithm ILU and MILU is that certain fill-ins given up in algorithm ILU are back to the main diagonal.Algorithm 1:Algorithm ILU.
(1) for  r≔ 1 Step i until  n-1  do
(2)  d≔ 1/ar,r;
(3)  for  i≔  (r+1) Step (1) until  n  do
(4)    if (i,r) ∈ S then;
(5)    e≔dai,r;  ai,r≔e;
(6)    for  j≔ (r+1) Step (1) until  n  do
(7)      if (i,j) ∈ S and (r,j) ∈ S then;
(8)      ai,j≔ai,j-ear,j;
(9)      end if;
(10)    end for  (j-loop);
(11)    end if;
(12)  end for  (i-loop);
(13) end for   (r-loop);Algorithm 2:Algorithm MILU.
(
1) for  r≔1 Step (1) until n-1  do
(2)  d≔1/ar,r;
(3)  for  i≔(r+1) Step (1) until n  do
(4)   if (i,r)∈S then;
(5)   e≔dai,r; ai,r≔e;
(6)   for  j≔(r+1) Step (1) until n  do
(7)    if (r,j)∈S then;
(8)    if (i,j)∈S then;
(9)    ai,j≔ai,j-ear,j;
(10)   else;
(11)    ai,i≔ai,i-ear,j;
(12)   end if;
(13)    end if;
(14)   end for  (j-loop)
(15)   end if;
(16) end for  (i-loop);
(17) end for  (r-loop);


## 4. Equivalent Labeled Transition Systems

In labeled transition systems, we can assume thatΣ is a finite set of labels; a label σ∈Σ describes an action. →⊆Q×Σ×Q is a transition relation, where Q is a set of states. Each transition → is a tuple q,σ,q′, where q and q′ represent the pre- and poststates of the transition, respectively. A state trajectory of labeled transition systems is a sequence of transitions: (6)q0⟶σ0q1⟶σ1q2⟶σ2⋯,where q0∈Q0 is the initial state and Q0⊆Q is the initial set of states.For a given initial state and sequence of labels, there may be several state trajectories of labeled transition systems. Thus, the systems we consider are possibly nondeterministic.Here, we mainly consider the setΣ of labels. Let label σ∈Σ has the following form:(7)x˙1=a11tx1+a12tx2+⋯+a1ntxnx˙2=a21tx1+a22tx2+⋯+a2ntxn⋮x˙n=an1tx1+an2tx2+⋯+anntxn.It can be abbreviated asx˙=A(t)x, where x˙=(x˙1x˙2⋯x˙n)T, x=(x1x2⋯xn)T, and(8)At=a11ta12t⋯a1nta21ta22t⋯a2nt⋮⋮⋮⋮an1tan2t⋯annt.We can obtain the preconditionerM(t) of matrix A(t) by means of ILU. We assume the preconditioner M(t) is(9)Mt=b11tb12t⋯b1ntb21tb22t⋯b2nt⋮⋮⋮⋮bn1tbn2t⋯bnnt.According to Section3, we can know that the equivalent equation of x˙=A(t)x is M-1(t)A(t)x=M-1(t)x˙. Let σ′ be symbol of M-1(t)A(t)x=M-1(t)x˙. That is, σ′:M-1(t)A(t)x=M-1(t)x˙. So label σ and label σ′ are equivalent.Definition 8.
Labelσ′:M-1(t)A(t)x=M-1(t)x˙ is the equivalent label of label σ:x˙=A(t)x, where x and x˙ are the pre- and poststate values of the transition, if matrix M(t) is the preconditioner matrix of matrix A(t).
The labeled transition system can only be used for symbolic reasoning. Two labels are equivalent if they have the same form, syntax, and semantics. Here, Definition8 gives the equivalent of two labels. It has the characteristic that labels’ equations are equivalent instead of having the same form, syntax, and semantics.
For all labelsσi∈Σ, i∈N, where N is the set of positive integers, σi:x˙=Ai(t)x; its equivalent label is σi′:Mi-1(t)Ai(t)x=Mi-1(t)x˙, where matrix Mi(t) is the preconditioner matrix of matrix Ai(t). Let Σ′=σi′∣i∈N.Definition 9.
SetΣ={σi∣i∈N} of labels and set Σ′=σi′∣i∈N are equivalent if ∀σi∈Σ; there exists j∈N making σi and σj equivalent.
A labeled transition system with observation is a tupleT=(Q,Σ,→,Q0,Π,·). Let T′=(Q,Σ′,→,Q0,Π,·).Definition 10.
Labeled transition system with observationT and labeled transition system with observation T′ are equivalent if set Σ of labels and set Σ′ of labels are equivalent. One labeled transition system is called equivalent system of another labeled transition system.Here, we only study labels of labeled transition systems.


## 5. Approximate Labeled Transition System

In general, we know that a labeled transition system with observations is used to prescribe control systems. In this section, our goal is to studyx˙=Ax (the transition relationship between states).The purpose of this paper is to characterize approximate similar transition systems that are generated by continuous-time linear systems, which are conceptually similar to the transition systems generated by discrete-time systems. We begin with studying continuous-time linear systems whose dynamics are closer to transition systems due to the existence of an atomic time step [30]. Consider a continuous-time linear system without disturbances(10)C:x˙=Ax,where with time t∈R+, state x(t)∈Rn and matrix A of approximate dimension, given an initial condition x0.Definition 11.
Consider continuous-time systemC given by x˙=Ax and observation set Π=Bp. The transition system TCr+=(Q,Σ,→,Π,·) generated by C and Π consists of(i)
state spaceQ=Rn,(ii)
labelΣ=R+,(iii)
transition relation→⊆Q×R+×Q defined as x→tx′⇔∃u[0,t] with x′=ΦC(t,x,u[0,t]),(iv)
observationΠ=Bp,(v)
observation map·:Q→Π.
Usually, the linear systems are presented by ordinary differential equations, partial differential equations, and difference equations.
Fort∈R+, the transition relation is given by q→tq′ if and only if there exists a function x(·) such that x(0)=q, x(t)=q′, and for almost all s∈[0,t], x˙(s)∈F(x(s)), where F is a valued map.


### 5.1. Approximate Similar States

Consider the following continuous-time linear system of stateq translated to another state q′ without disturbances, where the continuous-time linear system is a nondeterministic continuous system. That is, q→σ1q′:(11)x˙1=a11tx1+a12tx2+⋯+a1ntxnx˙2=a21tx1+a22tx2+⋯+a2ntxn⋮x˙n=an1tx1+an2tx2+⋯+anntxnand state value of the initial state q is x(0)=(b1b2⋯bn), t∈[0,t0].The state is observed through the variableπ1(t)=x1(t) and the transition relation is expressed as →1.We know that the equation is the linear differential equations. We introduce the following mark:(12)At=a11ta12t⋯a1nta21ta22t⋯a2nt⋮⋮⋮⋮an1tan2t⋯annt,where A(t) is an n by n matrix. The above equations can be expressed as(13)x˙=Atx,where x=(x1x2⋯xn)T,   x˙=(x˙1x˙2⋯x˙n)T.However,A(t) is a large sparse matrix for most mathematical models of practical problems in the real world, so it is very difficult for us to obtain the solution of the equation x˙=A(t)x. Then we use ILU to calculate the approximate solution. The preconditioner M=LU, where L is a triangular matrix and U is an upper triangular matrix. Hence, the original linear system x˙=A(t)x is transformed into an equivalent linear system M-1Ax=M-1x˙ (or the symmetric version (M-1/2AM-1/2)(M1/2x)=M-1/2x˙ when both A and M are symmetric positive definite). Because system x˙=A(t)x is a portrait of the transition process from the state q to another state q′, the elements of A(t) present the dynamic changes from state q to another state q′. The preconditioner M is the approximate dynamic changed from the state q to another state q′. Hence, A-M, an error matrix, has the meaning that state q can be translated into another state q′ in the error, and its degree of approximation is M-AF. Then we can define the approximate distance between the two states.Proposition 12.
d
(
x
,
y
)
=
x
-
y
F is the distance between x and y, where x,y∈X and X is a linear space.Proof.
In fact, for the norm axioms,∀x, y, z∈X, d(x,y)=x-yF≥0, and d(x,y)=0 if and only if x-yF=0; that is, x=y.
What is more,(14)dx,y=x-yF=y-xF=dy,x,dx,y=x-yF=x-z+z-yF≤x-zF+z-yF=dx,z+dz,y.Definition 13.
∀
q, q′∈Q, the approximate distance between q and q′ is (15)dQq,q′=M-AF.
Let us assume thatq1,q2,q3 are elements of Q and the state trajectory is(16)q1⟶σ1q2⟶σ2q3.
The mathematical relationship ofq1→σ1q2, q2→σ2q3 is respective x˙=A1(t)x, z˙=A2(t)z. This system is a continuous transition, so a transition from state q1 to state q3 can be expressed as q1→σ2σ1q3. This can be represented by using Figure 1. A line with an arrow indicates state transition, where the end of a line without arrow points to the prestate and the end of a line with arrow points to the poststate, a label marks on the line.Figure 1
Continuous transition of states.CalldQ(q,q′)=M-AF as the degree of approximation of state q translated into state q′. Furthermore, because x(0)=q, x(t0)=q′, the solution y of the equivalent linear system M-1Ax=M-1x˙ is the approximate solution of the original linear system x˙=A(t)x, where t∈[0,t0], y(0)=q, y(t0)=p′. The mathematical relationship of q→σp′ is(17)y˙=Aty,where y=(y1y2⋯yn)T, y˙=(y˙1y˙2⋯y˙n)T, and state value of initial state y(0)=(b1b2⋯bn).The state is observed through the variableπ2(t)=y1(t) and the transition relation is expressed as →2. Therefore, the accuracy between the exact solution x and approximate solution y of the linear systems is δ=M-AF. That is, δ=limt→+∞x-yF=M-AF. And dΠ(π1(t),π2(t))=x1(t)-y1(t)F≤x-yF=δ.Theorem 14.
Lety be the approximate solution of x˙=A(t)x; then y˙=A(t)y simulates approximately x˙=A(t)x with precision limt→+∞A(t)FM-AF.Proof.
(18)
lim
t
→
+
∞
⁡
x
˙
-
y
˙
F
=
lim
t
→
+
∞
⁡
A
t
x
-
A
t
y
F
=
lim
t
→
+
∞
⁡
A
t
x
-
y
F
≤
lim
t
→
+
∞
⁡
A
t
F
x
-
y
F
≤
lim
t
→
+
∞
⁡
A
t
F
lim
t
→
+
∞
⁡
x
-
y
F
=
lim
t
→
+
∞
⁡
A
t
F
M
-
A
F
.
Soy˙=A(t)y simulates approximately x˙=A(t)x. And therefore, we can say the state p′ simulates approximately the state q′.Here, approximate simulation of states is controlled by labels, where labels are special. Furthermore, the degree of approximate similar states can be obtained by the approximate solution of labels’ mathematical models.


### 5.2. Approximate Similar Linear Systems

We have given an approximate simulation method for a state. Now we consider approximate simulation of linear systems.Let the transition system generated byC and Π be expressed as TCr+=(Q,Σ,→,Π,·). Furthermore, for any state in Q we have given its approximate state; that is, ∀qi∈Q, i=1,2,…,qi is approximately simulated by state qi′ by means of ILU, and the equivalent label of label σi:x˙=Ai(t)x is σi′:Mi-1(t)Ai(t)x=Mi-1(t)x˙, where matrix Mi(t) is the preconditioner of matrix Ai(t). Let Q′=qi′∣i=1,2,…, Σ′=σi′∣i=1,2,…, and then T′=(Q′,Σ′,→,Π,·).Definition 15.
T
′ approximately simulates T, if there exists qi′ and σi′, i=1,2,…, where state qi′ is an approximate simulation state of state qi; label σi′ is the equivalent label of label σi. One labeled transition system is called approximate system of another labeled transition system.Theorem 16.
The precision of theT′ approximate simulation T is (19)δ=maxi⁡limt→+∞⁡AitFMi-AiF,i=1,2,….According to Theorem14, we know that a state q′ can simulate approximately the state q with the precision limt→+∞A(t)FM-AF. Thus, for each qi∈Q, ∃qi′∈Q′ simulates approximately state qi with the precision limt→+∞Ai(t)FMi-AiF. This means that each element of set Q has its approximate element with corresponding percision. But the set Q′ generally approximates to the set Q with some other precision. Fortunately, we know that in this situation the precision between the set Q and the set Q′ can be defined by the maximum percision of their elments. So the precision between set Q′ of approximate states and set Q of states is (20)δ=maxi⁡limt→+∞⁡AitFMi-AiF,i=1,2,….But because the precision of the T′ approximate simulation T is caused by set Q′ of approximate state, Theorem 16 is reasonable.


## 5.1. Approximate Similar States

Consider the following continuous-time linear system of stateq translated to another state q′ without disturbances, where the continuous-time linear system is a nondeterministic continuous system. That is, q→σ1q′:(11)x˙1=a11tx1+a12tx2+⋯+a1ntxnx˙2=a21tx1+a22tx2+⋯+a2ntxn⋮x˙n=an1tx1+an2tx2+⋯+anntxnand state value of the initial state q is x(0)=(b1b2⋯bn), t∈[0,t0].The state is observed through the variableπ1(t)=x1(t) and the transition relation is expressed as →1.We know that the equation is the linear differential equations. We introduce the following mark:(12)At=a11ta12t⋯a1nta21ta22t⋯a2nt⋮⋮⋮⋮an1tan2t⋯annt,where A(t) is an n by n matrix. The above equations can be expressed as(13)x˙=Atx,where x=(x1x2⋯xn)T,   x˙=(x˙1x˙2⋯x˙n)T.However,A(t) is a large sparse matrix for most mathematical models of practical problems in the real world, so it is very difficult for us to obtain the solution of the equation x˙=A(t)x. Then we use ILU to calculate the approximate solution. The preconditioner M=LU, where L is a triangular matrix and U is an upper triangular matrix. Hence, the original linear system x˙=A(t)x is transformed into an equivalent linear system M-1Ax=M-1x˙ (or the symmetric version (M-1/2AM-1/2)(M1/2x)=M-1/2x˙ when both A and M are symmetric positive definite). Because system x˙=A(t)x is a portrait of the transition process from the state q to another state q′, the elements of A(t) present the dynamic changes from state q to another state q′. The preconditioner M is the approximate dynamic changed from the state q to another state q′. Hence, A-M, an error matrix, has the meaning that state q can be translated into another state q′ in the error, and its degree of approximation is M-AF. Then we can define the approximate distance between the two states.Proposition 12.
d
(
x
,
y
)
=
x
-
y
F is the distance between x and y, where x,y∈X and X is a linear space.Proof.
In fact, for the norm axioms,∀x, y, z∈X, d(x,y)=x-yF≥0, and d(x,y)=0 if and only if x-yF=0; that is, x=y.
What is more,(14)dx,y=x-yF=y-xF=dy,x,dx,y=x-yF=x-z+z-yF≤x-zF+z-yF=dx,z+dz,y.Definition 13.
∀
q, q′∈Q, the approximate distance between q and q′ is (15)dQq,q′=M-AF.
Let us assume thatq1,q2,q3 are elements of Q and the state trajectory is(16)q1⟶σ1q2⟶σ2q3.
The mathematical relationship ofq1→σ1q2, q2→σ2q3 is respective x˙=A1(t)x, z˙=A2(t)z. This system is a continuous transition, so a transition from state q1 to state q3 can be expressed as q1→σ2σ1q3. This can be represented by using Figure 1. A line with an arrow indicates state transition, where the end of a line without arrow points to the prestate and the end of a line with arrow points to the poststate, a label marks on the line.Figure 1
Continuous transition of states.CalldQ(q,q′)=M-AF as the degree of approximation of state q translated into state q′. Furthermore, because x(0)=q, x(t0)=q′, the solution y of the equivalent linear system M-1Ax=M-1x˙ is the approximate solution of the original linear system x˙=A(t)x, where t∈[0,t0], y(0)=q, y(t0)=p′. The mathematical relationship of q→σp′ is(17)y˙=Aty,where y=(y1y2⋯yn)T, y˙=(y˙1y˙2⋯y˙n)T, and state value of initial state y(0)=(b1b2⋯bn).The state is observed through the variableπ2(t)=y1(t) and the transition relation is expressed as →2. Therefore, the accuracy between the exact solution x and approximate solution y of the linear systems is δ=M-AF. That is, δ=limt→+∞x-yF=M-AF. And dΠ(π1(t),π2(t))=x1(t)-y1(t)F≤x-yF=δ.Theorem 14.
Lety be the approximate solution of x˙=A(t)x; then y˙=A(t)y simulates approximately x˙=A(t)x with precision limt→+∞A(t)FM-AF.Proof.
(18)
lim
t
→
+
∞
⁡
x
˙
-
y
˙
F
=
lim
t
→
+
∞
⁡
A
t
x
-
A
t
y
F
=
lim
t
→
+
∞
⁡
A
t
x
-
y
F
≤
lim
t
→
+
∞
⁡
A
t
F
x
-
y
F
≤
lim
t
→
+
∞
⁡
A
t
F
lim
t
→
+
∞
⁡
x
-
y
F
=
lim
t
→
+
∞
⁡
A
t
F
M
-
A
F
.
Soy˙=A(t)y simulates approximately x˙=A(t)x. And therefore, we can say the state p′ simulates approximately the state q′.Here, approximate simulation of states is controlled by labels, where labels are special. Furthermore, the degree of approximate similar states can be obtained by the approximate solution of labels’ mathematical models.


## 5.2. Approximate Similar Linear Systems

We have given an approximate simulation method for a state. Now we consider approximate simulation of linear systems.Let the transition system generated byC and Π be expressed as TCr+=(Q,Σ,→,Π,·). Furthermore, for any state in Q we have given its approximate state; that is, ∀qi∈Q, i=1,2,…,qi is approximately simulated by state qi′ by means of ILU, and the equivalent label of label σi:x˙=Ai(t)x is σi′:Mi-1(t)Ai(t)x=Mi-1(t)x˙, where matrix Mi(t) is the preconditioner of matrix Ai(t). Let Q′=qi′∣i=1,2,…, Σ′=σi′∣i=1,2,…, and then T′=(Q′,Σ′,→,Π,·).Definition 15.
T
′ approximately simulates T, if there exists qi′ and σi′, i=1,2,…, where state qi′ is an approximate simulation state of state qi; label σi′ is the equivalent label of label σi. One labeled transition system is called approximate system of another labeled transition system.Theorem 16.
The precision of theT′ approximate simulation T is (19)δ=maxi⁡limt→+∞⁡AitFMi-AiF,i=1,2,….According to Theorem14, we know that a state q′ can simulate approximately the state q with the precision limt→+∞A(t)FM-AF. Thus, for each qi∈Q, ∃qi′∈Q′ simulates approximately state qi with the precision limt→+∞Ai(t)FMi-AiF. This means that each element of set Q has its approximate element with corresponding percision. But the set Q′ generally approximates to the set Q with some other precision. Fortunately, we know that in this situation the precision between the set Q and the set Q′ can be defined by the maximum percision of their elments. So the precision between set Q′ of approximate states and set Q of states is (20)δ=maxi⁡limt→+∞⁡AitFMi-AiF,i=1,2,….But because the precision of the T′ approximate simulation T is caused by set Q′ of approximate state, Theorem 16 is reasonable.


## 6. A Case Study

Now let us show the approximate theorem by taking example of some of the computations by considering linear systems without disturbances. Consider the linear systemsx˙=Ax, where(21)x˙1x˙2x˙3=1211-11201x1x2x3and the initial state is x(0)=(100).The linear system is approximately simulated by means of ILU. Firstly, we let(22)A=1211-11201,where A is the matrix of the equations. The LU factors of A are(23)L′=1001102431,U′=1210-3000-1.In terms of Algorithm1, the ILU algorithm gives(24)L=100110201,U=1210-3000-1,which is different from setting the (3, 2) element of the LU factors to zero.Now, we use the method of ILU to solve the problem. The preconditioner(25)M=LU=1001102011210-3000-1=1211-11241.Then, mathematically, the equivalent system of the original linear systemx˙=Ax is the preconditioned system M-1x˙=M-1Ax. That is,(26)1211-11241-1x˙1x˙2x˙3=1211-11241-11211-11201x1x2x3.In the example, we use ILU method to approximate simulation states, and the precise of approximate simulation states can be calculated. That is,(27)M-A=1211-11241-1211-11201=000000040,M-AF=02+02+02+02+02+02+02+42+02=4,AF=12+22+12+12+-12+12+22+02+12=14.So the precision of approximate simulation states isδ=AFM-AF=414≈14.9666, where the precision retains four significant numbers after the decimal point. If we want to use MILU to solve the problem of approximate simulation states, we just deal with A, that is, using Algorithm 2 to decomposition A.


## 7. Conclusions

In this paper, we extend the notion of approximate simulation relations. The semantic analysis of equivalent labeled transition systems is developed by equivalent labels. And an effective characterization of approximate simulation relations of states based on ILU is also developed, where error about the state set approximate is controlled. Furthermore, the technique can be used to approximately simulate labeled transition systems generated by continuous-time system. Finally, a case study of application in the context of linear systems without disturbances is shown.The approximate simulation relation is a key performance consideration of systems. Our future work will focus on these two items in two steps: firstly, developing methods to approximate simulation linear systems with disturbances; secondly, solving the nonlinear systems.



---

*Source: 963597-2015-10-25.xml*