# Approximate Bisimulation and Optimization of Software Programs Based on Symbolic-Numeric Computation

Authors: Hui Deng; Jinzhao Wu
Journal: Mathematical Problems in Engineering
 (2013)

---

## Abstract

To achieve behavior and structure optimization for a type of software program whose data exchange processes are represented by nonlinear polynomial systems, this paper establishes a novel formal description called a nonlinear polynomial transition system to represent the behavior and structure of the software program. Then, the notion of bisimulation for software programs is proposed based on the equivalence relation of corresponding nonlinear polynomial systems in their nonlinear polynomial transition systems. However, the exact equivalence is too strict in application. To enhance the flexibility of the relation among the different software systems, the notion of approximate bisimulation within a controllable error range and the calculation algorithm of approximate bisimulation based on symbolic-numeric computation are given. In this calculation, an approximate relation is represented as a MAX function that is resolved with the full filled method. At the same time, the actual error is calculable. An example on a multithreading program indicates that the approximate bisimulation relation is feasible and effective in behavior and structure optimization.


---

## Body

## 1. Introduction

With the development of computer software technology and the increase in user requirements for the function of software programs, the structure and behavior of software programs have been growing more and more complex. This change will make the design and property verification processes increasingly difficult. However, if we can achieve a method that can optimize the behavior and structure, then this accomplishment will most likely make a significant difference.In the process of achieving this method, establishing a formal description is a prerequisite of researching the behavior and structure of the software program. The previous formal descriptions of the software programs are discrete concurrent systems, which are composed of abstract behaviors, discrete states, and transitions between states [1–5]. These descriptions are good at calculating and reasoning against programs that are based on ergodic states. Nevertheless, they cannot successfully express the data exchange processes of the software program. The representations of data exchange processes are diverse for example, they can be described by a polynomial algebraic system, a semialgebraic system, a differential algebraic system, and a differential semialgebraic system [6–9]. Among these systems, research on a particular type of software program whose data exchange processes can be described by polynomial algebraic systems can form a basis for researching other types of programs. Thus, we will study this type of software program first. For a polynomial algebraic system, its representation can also be divided into several different types, for example, a homogeneous linear polynomial system, a nonhomogeneous linear polynomial system, or a nonlinear polynomial system, among others. The software programs that have different behavior and structure correspond to different types of polynomial systems and optimization methods. We have already studied the descriptions of one type of software program, whose data exchange processes can be described by linear polynomial systems, and one type of high-level datapath system, whose data exchange processes can be expressed by nonlinear polynomial systems, and these are referred to as a linear polynomial transition system and a polynomial transition system, respectively [10, 11]. These descriptions are a basis for proposing an appropriate description of the type of software programs that are researched in this paper, whose data exchange processes can be expressed by nonlinear polynomial systems.In addition to the above prerequisite, to define and determine the behavior equivalence relation for programs is another precondition to obtain behavior and structure optimization. With equivalence, the equivalent nondeterministic branches are removed, and the complex branch is replaced with a simpler branch. Two software programs are behavior equivalent representations that have the same function. To evaluate equivalence, bisimulation is the best behavior equivalence relation that we can utilize today [12, 13]. If two or more software programs are bisimular, then the solutions of the polynomial systems of their corresponding branches in their transition systems are the same. Based on the nature of bisimulation, researchers have already used it to optimize the design and verification of complex systems, such as hybrid systems and dynamical systems [14, 15]. We have also chosen it to process software programs that are represented by linear polynomial transition systems. For the type of software program researched in this paper, this type of equivalence theory will be established.Exact equivalence can achieve behavior and structure optimization, but this type of equivalence is too strict to be a good solution for programs in which there are errors in the applications. Take a square with side length 1, for example; the length of its diagonal line is2. Because 2 is an irrational number, strictly speaking, we can only make the length of the diagonal line approximately be equal to2. Therefore, there exists an error. For this type of application, exact equivalence is not practical. To strengthen the flexibility of the equivalence relation for different systems, an approximate equivalence within a controllable error range is a good solution. Thus far, approximate bisimulation has been established and applied to optimize the task of property verification for hybrid systems and dynamical systems [16–18]. For software programs that are represented by linear polynomial transition systems, the corresponding approximate relation has been given. Unfortunately, this calculation of an approximate equivalence relation cannot be applied to process the types of software programs that are researched in this paper.For the calculation of approximate equivalence, symbolic-numeric computation can provide us with technical support [19, 20]. The fact that two software programs are approximate means that the solutions of the polynomial systems of the corresponding branches in their transition systems are approximately the same. It also means that the solutions of one system can make another system approximately be equal to zero. This relationship can be expressed as a constrained global optimization, which is called the MAX function in this paper. In the existing literature, there are many different methods that can be used to solve this constrained global optimization. Among these methods, the full filled method proposed by Ge [21–23] is one of the most widely used. Based on this author’s studies, researchers perform some related research and made some improvements [24, 25]. We will use the full filled method in the literature [26] because it has fewer unknown parameters. With this method, the value of the exact error caused by an approximation can be computed.In the next section, we provide a new formal description, called a nonlinear polynomial transition system, which is used to describe the behavior and structure of the type of software program whose data exchange processes are represented by nonlinear polynomial systems. In Section3, we give the notion and algorithm of bisimulation after analyzing the condition of equivalence for these software programs. Based on this relation, the notion and the calculation of the algorithm for approximate bisimulation are described in detail in Section 4. The approximate relation is expressed as a constrained global optimization called the MAX function, which is solved by the full filled method. In Section 5, an example of a multithreading program shows that our approach obtains three useful results, which are listed as follows. The last section presents our conclusions.(i)
The data exchange processes of software programs are described.(ii)
The equivalence and approximate relations are determined for software programs based on symbolic-numeric computation.(iii)
The behavior and structure optimization for the software program are achieved.


## 2. Nonlinear Polynomial Transition System

The definition of a nonlinear polynomial transition system is introduced in this section. This definition is used to describe a type of software program whose data exchange processes can be represented by nonlinear polynomial systems.This nonlinear polynomial transition system is composed of states and transitions, which provide us with a supportive framework to research the behavior and the structure of software programs. A transition that is expressed by a nonlinear polynomial system shows a part of the data exchange process. A function is a transition. The statements between two functions can also be considered to be transitions.First, we must establish a transform rule between a part of the data exchange process and a nonlinear polynomial system, which is established as follows.Algorithm 1.
The transform rule between a part of the data exchange process of a software program and a nonlinear polynomial system.
Input: A part of the data exchange process within a software program.
Output: A nonlinear polynomial system.
Step
1. If there are many assignment statements that assign values to the same variable and that variable does not appear on the right side of the assignment statements, then remove the assignment statements except for the last one.
Step
2. Change the symbols of the variables on the left side of the assignment statements by adding intermediate variables after Step1.
Step
3. If a variable on the right side of the assignment statements is the same as a variable on the left side of the assignment statements before Step2, then change the symbol of the variable on the right side of the assignment statements with the symbol of the variable on the left side of the last assignment statement after Step2.
Step
4. Add the assignment statements into NLPS after being processed by Steps1, 2, and 3.
Step
5. For the conditional statements, if there are variables that were assigned before them, then first change the symbol of these variables with their symbols on the left side of their last assignment statements after Step2, respectively; then, add these conditional statements into NLPS. Otherwise, add the conditional statements into NLPS directly.In NLPS, the variables are temporary variables if they can be eliminated. The remainders are global variables, which play an important role in judging the equivalence relations of the software programs. Based on this transform rule, the notion of a nonlinear polynomial transition system for software programs can be given as follows.Definition 2.
A nonlinear polynomial transition system is a tuple〈V,S,T,Q0,v1〉 that includes(i)
a setV of variables, including temporary variables and global variables;(ii)
a setS of states, which are the values of the variables in V;(iii)
a setT of transitions; each of the transitions is a tuple 〈s1,s2,NLPS,v0〉:
(a)
s1 and s2 are the pre- and postglobal states of a transition;(b)
the transition relationNLPS is a nonlinear polynomial system;(c)
v0 represents the global variables of this transition;(iv)
Q0 is the initial state of this software program;(v)
a setv1 of global variables; the form of v1 can be defined as follows:
(1)v1={vin,vout}={{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:n},kkk{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:n}},where vin is a set of global input variables and vout is a set of global output variables. The layer number of the nonlinear polynomial transition system is n. If we consider every nonlinear polynomial transition system to be a tree, then the layer number is considered to be the depth of the tree. Every bracket represents the set of global input or output variables of one branch in this layer.
Corresponding to the form ofv1, we can give a definition of a set of global states s:
(2)s={s1,s2}={{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:n},kkk{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:n}},
where s1 is a set of global input states and s2 is a set of global output states.
To describe the transform process between a software program and a nonlinear polynomial transition system clearly, an example is given in Figure1. The value of Q0 is given in advance.
With this transform process, we discover that the behavior and structure of a software program are successfully expressed by a nonlinear polynomial transition system, which can also be represented by a transition graph. Compared with the description of a software program language, the forms of a transition system and transition graph are more direct. Moreover, based on the transform process, the behavior equivalence relation between two data exchange processes of software programs can be described by Definition3.Figure 1
Transform process.Definition 3.
The data exchange processes〈s11,s12,NLPS1,v01〉 and 〈s21,s22,NLPS2,v02〉 of a software program are equivalent; if NLPS1 and NLPS2 have solutions in Q, v01 and v02 are the same, then there is(i)
∀x1→NLPS1x2, ∃y1=x1, y1→NLPS2y2, and x2=y2,(ii)
∀y1→NLPS2y2, ∃x1=y1, x1→NLPS1x2, and y2=x2,where x1×x2∈s11×s12, y1×y2∈s21×s22, the variables that correspond to x1and y1are the same, and the variables that correspond to x2 and y2 are the same. Q  is a rational number field.
Within this definition, stating that the solutions of two nonlinear polynomial systems are the same implies that their corresponding data exchange processes in a software program are behavior equivalent.
After determining the relation for two data exchange processes, how to establish the definition of behavior equivalence for the whole software program must also be researched because there could be many layers and many branches in the same layer in a software program.


## 3. Bisimulation for Nonlinear Polynomial Transition Systems

In process algebra, equivalence verification is one of the most important parts and bisimulation is the finest equivalence semantic that can provide the most exact equivalence relation for systems. With equivalence determination, the extra transitions, called nondeterminism, can be removed and a complex branch can be replaced with a simple branch.


### 3.1. The Definition of Bisimulation

Let there be two nonlinear polynomial transition systems:(3)A:〈V1,S1,T1,Q01,v11〉,B:〈V2,S2,T2,Q02,v12〉.
The global state sets of them are
(4)sA={s1A,s2A}={{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:a},kkk{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:a}},sB={s1B,s2B}={{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:b},kkk{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:b}},
where the symbol sijmn represents the nth branch of the mth layer in sij.The sets of nonlinear polynomial systems ofA and B can also be given as follows:
(5)NLPS1={{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:a},NLPS2={{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:b},
where the symbol NPLSimn represents the nth branch of the mth layer in NLPSi.Definition 4.
A binary relationR⊆sA×sB is called bisimulation; if v11and v12 are exactly the same, NLPS1Alm and NLPS2Blg have solutions in Q, and a=b, then, for all (x1×y1)∈R, there are(i)
∀x1→NLPS1Almx2, ∃y1=x1, y1→NLPS2Blgy2, x2Ry2, and x2=y2,(ii)
∀y1→NLPS2Blgy2, ∃x1=y1, x1→NLPS1Almx2, x2Ry2, and x2=y2.
Then,A and B are bisimular, with the notation A=BEB.
Wherex1∈s1Alm, x2∈s2Alm, y1∈s1Blg, y2∈s2Blg, the variables that correspond to x1 and y1 are the same, and the variables that correspond to x2 and y2 are the same.
With this definition, we can determine whether there is a bisimulation relation or not between two software programs. If two software programs are bisimular, then their transition systems are bisimular. This fact also means that if there exists a transition for one, there exists the same transition for another and vice versa. This statement represents that the solutions are the same for the polynomial systems of the corresponding branches in the nonlinear polynomial transition system for the software program as well. Therefore, the bisimulation relation between software programs has the following nature.Theorem 5.
The bisimulation relation for nonlinear polynomial transition systems exists.(i)
Reflexivity:A=BEA, if there is a nonlinear polynomial transition system A.(ii)
Symmetry:B=BEA, if A=BEB.(iii)
Transitivity:A=BEC, if A=BEB and B=BEC.Proof.
(i) For reflexivity: the behavior and structure ofA are the same as itself; thus, A=BEA.
(ii) For symmetry: ifA=BEB, then the corresponding branches of A and B are equivalent, which implies that the corresponding branches of B and A are equivalent; thus, B=BEA.
(iii) For transitivity: ifA=BEB, then the corresponding branches of A and B are equivalent.
IfB=BEC, then the corresponding branches of B and C are equivalent. Therefore, the corresponding branches of A and C are equivalent, which can be expressed with the notation A=BEC.
Thus, the bisimulation relation between the software programs is an equivalence relation.


### 3.2. The Calculation of Bisimulation

After obtaining the definition of behavior equivalence for a software program, we must establish a method for determining whether the solutions of two nonlinear polynomial systems are the same or not. For the type of software programs studied in this paper, Ritt-Wu’s method [27] can be used to determine this solution relation.Theorem 6.
IfCA and CB are the same, then the solutions of A and B are the same, which means that A and B are equivalent.Proof.
BecauseCA and CB are the same, then the initials IAi and IBi are the same, which correspond to CA and CB, respectively. At the same time,
(6)sA=⋃i=1eZero(CAi/IAi),sB=⋃i=1eZero(CBi/IBi).
The irreducible characteristic set of a polynomial system is unique; thus, there is(7)sA=⋃i=1eZero(CAi/IAi)=sB=⋃i=1eZero(CBi/IBi).
Then,A and B are equivalent where A and B are nonlinear polynomial systems. CA=[CA1,…,CAe] and CB=[CB1,…,CBe] are the irreducible characteristic sets of A and B, respectively. Here, sA and sB are the solutions of A and B, respectively.
Therefore, a unique condition that is used to determine the solution relation of the nonlinear polynomial systems is obtained.
This determination in the equivalence relation is based on symbolic computation. From analysis, we discover that numerical computation can also be used in this process, because if the solutions of the two polynomial systems are the same, then the solutions of one system can make another system be equal to zero. In other words, if we change one system into a special formula, the solutions of another system can approximately make the maximum value of this formula be equal to zero. This process can be considered to be a constrained global optimization. Because there are approximate processes while we are addressing this constrained global optimization problem, we will therefore implement this process in the next section.


## 3.1. The Definition of Bisimulation

Let there be two nonlinear polynomial transition systems:(3)A:〈V1,S1,T1,Q01,v11〉,B:〈V2,S2,T2,Q02,v12〉.
The global state sets of them are
(4)sA={s1A,s2A}={{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:a},kkk{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:a}},sB={s1B,s2B}={{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:b},kkk{{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:b}},
where the symbol sijmn represents the nth branch of the mth layer in sij.The sets of nonlinear polynomial systems ofA and B can also be given as follows:
(5)NLPS1={{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:a},NLPS2={{{},…,{}}︸layer:1,…,{{},…,{}}︸layer:b},
where the symbol NPLSimn represents the nth branch of the mth layer in NLPSi.Definition 4.
A binary relationR⊆sA×sB is called bisimulation; if v11and v12 are exactly the same, NLPS1Alm and NLPS2Blg have solutions in Q, and a=b, then, for all (x1×y1)∈R, there are(i)
∀x1→NLPS1Almx2, ∃y1=x1, y1→NLPS2Blgy2, x2Ry2, and x2=y2,(ii)
∀y1→NLPS2Blgy2, ∃x1=y1, x1→NLPS1Almx2, x2Ry2, and x2=y2.
Then,A and B are bisimular, with the notation A=BEB.
Wherex1∈s1Alm, x2∈s2Alm, y1∈s1Blg, y2∈s2Blg, the variables that correspond to x1 and y1 are the same, and the variables that correspond to x2 and y2 are the same.
With this definition, we can determine whether there is a bisimulation relation or not between two software programs. If two software programs are bisimular, then their transition systems are bisimular. This fact also means that if there exists a transition for one, there exists the same transition for another and vice versa. This statement represents that the solutions are the same for the polynomial systems of the corresponding branches in the nonlinear polynomial transition system for the software program as well. Therefore, the bisimulation relation between software programs has the following nature.Theorem 5.
The bisimulation relation for nonlinear polynomial transition systems exists.(i)
Reflexivity:A=BEA, if there is a nonlinear polynomial transition system A.(ii)
Symmetry:B=BEA, if A=BEB.(iii)
Transitivity:A=BEC, if A=BEB and B=BEC.Proof.
(i) For reflexivity: the behavior and structure ofA are the same as itself; thus, A=BEA.
(ii) For symmetry: ifA=BEB, then the corresponding branches of A and B are equivalent, which implies that the corresponding branches of B and A are equivalent; thus, B=BEA.
(iii) For transitivity: ifA=BEB, then the corresponding branches of A and B are equivalent.
IfB=BEC, then the corresponding branches of B and C are equivalent. Therefore, the corresponding branches of A and C are equivalent, which can be expressed with the notation A=BEC.
Thus, the bisimulation relation between the software programs is an equivalence relation.


## 3.2. The Calculation of Bisimulation

After obtaining the definition of behavior equivalence for a software program, we must establish a method for determining whether the solutions of two nonlinear polynomial systems are the same or not. For the type of software programs studied in this paper, Ritt-Wu’s method [27] can be used to determine this solution relation.Theorem 6.
IfCA and CB are the same, then the solutions of A and B are the same, which means that A and B are equivalent.Proof.
BecauseCA and CB are the same, then the initials IAi and IBi are the same, which correspond to CA and CB, respectively. At the same time,
(6)sA=⋃i=1eZero(CAi/IAi),sB=⋃i=1eZero(CBi/IBi).
The irreducible characteristic set of a polynomial system is unique; thus, there is(7)sA=⋃i=1eZero(CAi/IAi)=sB=⋃i=1eZero(CBi/IBi).
Then,A and B are equivalent where A and B are nonlinear polynomial systems. CA=[CA1,…,CAe] and CB=[CB1,…,CBe] are the irreducible characteristic sets of A and B, respectively. Here, sA and sB are the solutions of A and B, respectively.
Therefore, a unique condition that is used to determine the solution relation of the nonlinear polynomial systems is obtained.
This determination in the equivalence relation is based on symbolic computation. From analysis, we discover that numerical computation can also be used in this process, because if the solutions of the two polynomial systems are the same, then the solutions of one system can make another system be equal to zero. In other words, if we change one system into a special formula, the solutions of another system can approximately make the maximum value of this formula be equal to zero. This process can be considered to be a constrained global optimization. Because there are approximate processes while we are addressing this constrained global optimization problem, we will therefore implement this process in the next section.


## 4. Approximate Bisimulation for Nonlinear Polynomial Transition Systems

Exact equivalence requires that the solutions of two polynomial systems must be identical, which appears to be too restrictive and not practical for some software programs. An appropriate approximation within a controllable error range can be a good solution for addressing this issue. By approximation, different software programs might be changed into approximately the same program. Then, the simpler programs can be used to approximately replace the complex programs. Therefore, behavior and structure approximate optimization can be achieved.


### 4.1. The Definition of Approximate Bisimulation

Suppose that there are two nonlinear polynomial transition systems. The descriptions of the variables of these two systems are the same as the descriptions in Section3.1.Definition 7.
The data exchange processes〈s11,s12,NLPS1,v01〉 and 〈s21,s22,NLPS2,v02〉 of a software program are approximate; if NLPS1 and NLPS2 have solutions in Q, v01 and v02 are the same, and ε≤δ, then there is(i)
∀x1→NLPS1x2, ∃y1→NLPS2y2 and ∃x1→NLPS2εx2, then, y1=εx1∪y1, y2=εx2∪y2.(ii)
∀y1→NLPS2y2, ∃x1→NLPS1x2 and ∃y1→NLPS1εy2, then, x1=εx1∪y1, x2=εx2∪y2,where x1×x2∈s11×s12, y1×y2∈s21×s22, the variables that correspond to x1 and y1 are the same, and the variables that correspond to x2 and y2 are the same. Here,
(8)m=εm∪n
represents that we place n into m to form a new m with an error ε. Then,
(9)m→NLPSεn
represents that m and n are the approximate solutions of NLPS with an error ε. Here, ε is the exact error and δ is the precision.
This definition shows that two data exchange processes are approximate if the solutions of their corresponding nonlinear polynomial systems are approximate. Based on this definition, the approximate relation for the entire software program can be given as follows.Definition 8.
A binary relationRε⊆sA×sB is called an approximate bisimulation; if v11 and v12 are the same, NLPS1Alm and NLPS2Blg have solutions in Q, a=b, and ε≤δ, then, for all (x1×y1)∈Rε, there are(i)
∀x1→NLPS1Almx2, ∃y1→NLPS2Blgy2, and ∃x1→NLPS2Blgεl(mg)x2; then, y1=εl(mg)x1∪y1, y2=εl(mg)x2∪y2, and x2Rεy2.(ii)
∀y1→NLPS2Blgy2, ∃x1→NLPS1Almx2, and ∃y1→NLPS1Almεl(mg)y2; then, x1=εl(mg)x1∪y1, x2=εl(mg)x2∪y2, and x2Rεy2.
Then,A and B are approximately bisimular, with the notation A=ABB.
Wherex1∈s1Alm, x2∈s2Alm, y1∈s1Blg, y2∈s2Blg, the variables that correspond to x1 and y1 are the sam, and the variables that correspond to x2 and y2 are the same.
Here,εl(mg) represents the error between NPLS1Alm and NPLS2Blg.
For two different nonlinear polynomial systems, the error between them can be calculated by the function norm. For the nonlinear polynomial transition system researched in this paper, there are always many branches and layers; thus, a measurement rule for the exact error must be given.Step 1.
For different branches in the same layer, compute the errors of every two of them first. Then, choose the largest one as the error in that layer.Step 2.
For the whole nonlinear polynomial transition system, compute the error of every layer with Step1; then, the total error of the system is found by taking the sum.With the previous definition, software programs that are approximately bisimular are those for which the solutions of the polynomial systems of the corresponding branches in their nonlinear polynomial transition systems are approximately the same. In other words, if we change a nonlinear polynomial system into a special formula, the solutions of another system can make the maximum value of this formula approximately be equal to zero. This process can be considered to be a constrained global optimization and its description is given as follows.Given two nonlinear polynomial systems, as follows:(10)p1=0,p2=0;f1=0,f2=0,f3=0.Then, change them into two constrained global optimizations, called MAX functions, as follows(11)maxp12+p22s.t.f1=0f2=0f3=0;maxf12+f22+f32s.t.p1=0p2=0,
which can also be expressed as follows:
(12)max(p12+p22)s.t.f1=0f2=0f3=0;max(f12+f22+f32)s.t.p1=0p2=0.The results of these two constrained global optimizations fall into three categories.(i)
If the two maximum values are equal to zero, then the two nonlinear polynomial systems are equivalent. Thus, the determination of bisimulation between two nonlinear polynomial transition systems in Section3.2 can be solved based on numerical computation.(ii)
If the two maximum values are not more than the precision, then two nonlinear polynomial systems are approximate. Therefore, the determination of approximate bisimulation between two nonlinear polynomial transition systems is achieved.(iii)
If one of the two maximum values is more than the precision, then two nonlinear polynomial systems are not approximate.The maximum value can be achieved by the full filled method. In this process, the maximum number of iterations and the step length of variables must be given in advance.


### 4.2. The Calculation of Approximate Bisimulation

For a software program, we hope to optimize its behavior and structure through approximately optimizing its formal description; this approach is called a nonlinear polynomial transition system with approximate bisimulation.When the variables of the corresponding branches in polynomial transition system are the same, the framework of approximate bisimulation of a software program contains four parts:(i)
change the software program into a nonlinear polynomial transition system;(ii)
group the corresponding branches of the transition system;(iii)
determine the relations of corresponding branches by symbolic-numeric computation;(iv)
achieve the behavior and structure optimization by reducing the equivalent or approximate branches for the given program.The detailed computation algorithm of approximate bisimulation is shown as follows, which is described in Figure2.Figure 2
Approximate bisimulation for the nondeterministic branches of a software program.Algorithm 9.
The calculation algorithm of approximate bisimulation for the nondeterministic branches of a software program based on symbolic-numeric computation.
Input: A software program expressed by a nonlinear polynomial transition system.
Output: An optimized software program for the given software program.
Step
1. Change the software program into a nonlinear polynomial transition system. Let δ be the precision. Group the corresponding branches with bisimulation relations. Suppose that the number of groups is m. We are given a counter i that starts with i=1.
Step
2. Process the ith group. Let the precision δi in this group belong to the following:
(13)(0,δ-∑e=1i-1δe].
Step
3. Choose Ritt-Wu’s method and the MAX function to determine the relation of each of the two branches in this group.
Step
3.1. If irreducible characteristic sets are the same and the errors are equal to zero, then these branches are equivalent. Choose the simplest branch to replace them and go to Step5. Otherwise, go to Step3.2.
Step
3.2. If the errors are not more than δi, then these branches are approximate. Then, choose an appropriate branch to replace them and go to Step5. Otherwise, go to Step3.3.
Step
3.3. Let the number of branches be a, and label them from 1 to a Initiate a counter b at b=1 and go to Step4.
Step
4. Determine the relation between the bth branch and the other branches from the (b+1)th to the ath branch. Let the symbol of the nonlinear polynomial system that corresponds to the jth branch be Jj. Let
(14)εb+1=∥Jb-Jb+1∥,εb+2=∥Jb-Jb+2∥,…,εa=∥Jb-Ja∥.
Select Jj except for Jb to form a set A when the errors are larger than δi. The remainder except for Jb forms a set B; go to Step4.1.
Step
4.1. Let U=A. Choose an appropriate element from B and Jb to replace them. Let the symbol of this element be Jw.
Step
4.2. The merger of U and Jw forms a new group, which is to be considered as the new ith group. Let the number of branches of this new group be a, with b=2. If a>2, then go to Step4; otherwise, go to Step5.
Step
5. Increment i with i++; if i≤m, then go to Step2; otherwise, end. A new polynomial transition system is achieved, which also means that a new optimized software program is got.This algorithm gives a method to optimize the behavior and structure of a software program with approximate bisimulation.If there are several different software programs, then we must know how to implement the determination of an approximate bisimulation for them.The framework of approximate bisimulation of different software programs contains five parts:(i)
optimize software programs by Algorithm9  respectively;(ii)
consider the optimized programs to be the nondeterministic branches of a new program;(iii)
group the corresponding branches of the new program;(iv)
determine the relations of corresponding branches by symbolic-numeric computation;(v)
get the behavior and structure optimizations for the given programs by equivalence.The detailed algorithm is also given as follows and is described by Figure3.Figure 3
Approximate bisimulation for software programs.Algorithm 10.
The calculation algorithm of approximate bisimulation for software programs based on symbolic-numeric computation.
Input: Different software programs that are represented by nonlinear polynomial transition systems.
Output: Optimized software programs for the given software programs.
Step
1. Get the approximately optimized software programs for the given software programs by Algorithm 9. Then, consider these approximately optimized programs as the nondeterministic branches of a new software program.
Step
2. Group the corresponding branches of this new program. Let the number of groups be m and use a counter i that starts with i=1.
Step
3. If there are equivalent branches in the ith group as determined by Ritt-Wu’s method or the MAX function, then go to Step4. Otherwise, go to Step6.
Step
4. Choose the simplest one of them to replace them.
Step
5. Increment i with i++; if i≤m, then go to Step3. Otherwise, go to Step6.
Step
6. End. Achieve the last optimized software programs of the given programs.


## 4.1. The Definition of Approximate Bisimulation

Suppose that there are two nonlinear polynomial transition systems. The descriptions of the variables of these two systems are the same as the descriptions in Section3.1.Definition 7.
The data exchange processes〈s11,s12,NLPS1,v01〉 and 〈s21,s22,NLPS2,v02〉 of a software program are approximate; if NLPS1 and NLPS2 have solutions in Q, v01 and v02 are the same, and ε≤δ, then there is(i)
∀x1→NLPS1x2, ∃y1→NLPS2y2 and ∃x1→NLPS2εx2, then, y1=εx1∪y1, y2=εx2∪y2.(ii)
∀y1→NLPS2y2, ∃x1→NLPS1x2 and ∃y1→NLPS1εy2, then, x1=εx1∪y1, x2=εx2∪y2,where x1×x2∈s11×s12, y1×y2∈s21×s22, the variables that correspond to x1 and y1 are the same, and the variables that correspond to x2 and y2 are the same. Here,
(8)m=εm∪n
represents that we place n into m to form a new m with an error ε. Then,
(9)m→NLPSεn
represents that m and n are the approximate solutions of NLPS with an error ε. Here, ε is the exact error and δ is the precision.
This definition shows that two data exchange processes are approximate if the solutions of their corresponding nonlinear polynomial systems are approximate. Based on this definition, the approximate relation for the entire software program can be given as follows.Definition 8.
A binary relationRε⊆sA×sB is called an approximate bisimulation; if v11 and v12 are the same, NLPS1Alm and NLPS2Blg have solutions in Q, a=b, and ε≤δ, then, for all (x1×y1)∈Rε, there are(i)
∀x1→NLPS1Almx2, ∃y1→NLPS2Blgy2, and ∃x1→NLPS2Blgεl(mg)x2; then, y1=εl(mg)x1∪y1, y2=εl(mg)x2∪y2, and x2Rεy2.(ii)
∀y1→NLPS2Blgy2, ∃x1→NLPS1Almx2, and ∃y1→NLPS1Almεl(mg)y2; then, x1=εl(mg)x1∪y1, x2=εl(mg)x2∪y2, and x2Rεy2.
Then,A and B are approximately bisimular, with the notation A=ABB.
Wherex1∈s1Alm, x2∈s2Alm, y1∈s1Blg, y2∈s2Blg, the variables that correspond to x1 and y1 are the sam, and the variables that correspond to x2 and y2 are the same.
Here,εl(mg) represents the error between NPLS1Alm and NPLS2Blg.
For two different nonlinear polynomial systems, the error between them can be calculated by the function norm. For the nonlinear polynomial transition system researched in this paper, there are always many branches and layers; thus, a measurement rule for the exact error must be given.Step 1.
For different branches in the same layer, compute the errors of every two of them first. Then, choose the largest one as the error in that layer.Step 2.
For the whole nonlinear polynomial transition system, compute the error of every layer with Step1; then, the total error of the system is found by taking the sum.With the previous definition, software programs that are approximately bisimular are those for which the solutions of the polynomial systems of the corresponding branches in their nonlinear polynomial transition systems are approximately the same. In other words, if we change a nonlinear polynomial system into a special formula, the solutions of another system can make the maximum value of this formula approximately be equal to zero. This process can be considered to be a constrained global optimization and its description is given as follows.Given two nonlinear polynomial systems, as follows:(10)p1=0,p2=0;f1=0,f2=0,f3=0.Then, change them into two constrained global optimizations, called MAX functions, as follows(11)maxp12+p22s.t.f1=0f2=0f3=0;maxf12+f22+f32s.t.p1=0p2=0,
which can also be expressed as follows:
(12)max(p12+p22)s.t.f1=0f2=0f3=0;max(f12+f22+f32)s.t.p1=0p2=0.The results of these two constrained global optimizations fall into three categories.(i)
If the two maximum values are equal to zero, then the two nonlinear polynomial systems are equivalent. Thus, the determination of bisimulation between two nonlinear polynomial transition systems in Section3.2 can be solved based on numerical computation.(ii)
If the two maximum values are not more than the precision, then two nonlinear polynomial systems are approximate. Therefore, the determination of approximate bisimulation between two nonlinear polynomial transition systems is achieved.(iii)
If one of the two maximum values is more than the precision, then two nonlinear polynomial systems are not approximate.The maximum value can be achieved by the full filled method. In this process, the maximum number of iterations and the step length of variables must be given in advance.


## 4.2. The Calculation of Approximate Bisimulation

For a software program, we hope to optimize its behavior and structure through approximately optimizing its formal description; this approach is called a nonlinear polynomial transition system with approximate bisimulation.When the variables of the corresponding branches in polynomial transition system are the same, the framework of approximate bisimulation of a software program contains four parts:(i)
change the software program into a nonlinear polynomial transition system;(ii)
group the corresponding branches of the transition system;(iii)
determine the relations of corresponding branches by symbolic-numeric computation;(iv)
achieve the behavior and structure optimization by reducing the equivalent or approximate branches for the given program.The detailed computation algorithm of approximate bisimulation is shown as follows, which is described in Figure2.Figure 2
Approximate bisimulation for the nondeterministic branches of a software program.Algorithm 9.
The calculation algorithm of approximate bisimulation for the nondeterministic branches of a software program based on symbolic-numeric computation.
Input: A software program expressed by a nonlinear polynomial transition system.
Output: An optimized software program for the given software program.
Step
1. Change the software program into a nonlinear polynomial transition system. Let δ be the precision. Group the corresponding branches with bisimulation relations. Suppose that the number of groups is m. We are given a counter i that starts with i=1.
Step
2. Process the ith group. Let the precision δi in this group belong to the following:
(13)(0,δ-∑e=1i-1δe].
Step
3. Choose Ritt-Wu’s method and the MAX function to determine the relation of each of the two branches in this group.
Step
3.1. If irreducible characteristic sets are the same and the errors are equal to zero, then these branches are equivalent. Choose the simplest branch to replace them and go to Step5. Otherwise, go to Step3.2.
Step
3.2. If the errors are not more than δi, then these branches are approximate. Then, choose an appropriate branch to replace them and go to Step5. Otherwise, go to Step3.3.
Step
3.3. Let the number of branches be a, and label them from 1 to a Initiate a counter b at b=1 and go to Step4.
Step
4. Determine the relation between the bth branch and the other branches from the (b+1)th to the ath branch. Let the symbol of the nonlinear polynomial system that corresponds to the jth branch be Jj. Let
(14)εb+1=∥Jb-Jb+1∥,εb+2=∥Jb-Jb+2∥,…,εa=∥Jb-Ja∥.
Select Jj except for Jb to form a set A when the errors are larger than δi. The remainder except for Jb forms a set B; go to Step4.1.
Step
4.1. Let U=A. Choose an appropriate element from B and Jb to replace them. Let the symbol of this element be Jw.
Step
4.2. The merger of U and Jw forms a new group, which is to be considered as the new ith group. Let the number of branches of this new group be a, with b=2. If a>2, then go to Step4; otherwise, go to Step5.
Step
5. Increment i with i++; if i≤m, then go to Step2; otherwise, end. A new polynomial transition system is achieved, which also means that a new optimized software program is got.This algorithm gives a method to optimize the behavior and structure of a software program with approximate bisimulation.If there are several different software programs, then we must know how to implement the determination of an approximate bisimulation for them.The framework of approximate bisimulation of different software programs contains five parts:(i)
optimize software programs by Algorithm9  respectively;(ii)
consider the optimized programs to be the nondeterministic branches of a new program;(iii)
group the corresponding branches of the new program;(iv)
determine the relations of corresponding branches by symbolic-numeric computation;(v)
get the behavior and structure optimizations for the given programs by equivalence.The detailed algorithm is also given as follows and is described by Figure3.Figure 3
Approximate bisimulation for software programs.Algorithm 10.
The calculation algorithm of approximate bisimulation for software programs based on symbolic-numeric computation.
Input: Different software programs that are represented by nonlinear polynomial transition systems.
Output: Optimized software programs for the given software programs.
Step
1. Get the approximately optimized software programs for the given software programs by Algorithm 9. Then, consider these approximately optimized programs as the nondeterministic branches of a new software program.
Step
2. Group the corresponding branches of this new program. Let the number of groups be m and use a counter i that starts with i=1.
Step
3. If there are equivalent branches in the ith group as determined by Ritt-Wu’s method or the MAX function, then go to Step4. Otherwise, go to Step6.
Step
4. Choose the simplest one of them to replace them.
Step
5. Increment i with i++; if i≤m, then go to Step3. Otherwise, go to Step6.
Step
6. End. Achieve the last optimized software programs of the given programs.


## 5. Example Verification and Results

In this section, a multithreading program is used to demonstrate the efficiency of approximate bisimulation in the behavior and structure optimization of software programs.


### 5.1. Example Verification

The multithreading program is represented in Algorithm1.Algorithm 1:Multithreading program.
#include “main.h”
WINMULTITHREAD Branch2Thread5(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->il, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((y1*y1 - (0.01*y2 + 1)*z1) > -APPZERO &&
(y1*y1 - (0.01*y2 + 1)*z1) < APPZERO) &&
((2*y1*y2 - z2 - 0.01) > -APPZERO &&
(2*y1*y2 - z2 - 0.01) < APPZERO)) {
printf(“one solution of HLPS9 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread4(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((y1*y1 - z1) > -APPZERO &&
(y1*y1 - z1) < APPZERO) &&
((2*y1*y2 - z2) > -APPZERO &&
(2*y1*y2 - z2) < APPZERO)) {
printf(“one solution of NLPS8 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread3(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) > -APPZERO &&
(-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) < APPZERO) &&
((-z1 + z2*(y1*y2 + 1)) > -APPZERO &&
(-z1 + z2*(y1*y2 + 1)) < APPZERO)) {
printf(“one solution of NLPS6 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread4(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((-z1 + (y1*y2 + 1)*z2) > -APPZERO &&
(-z1 + (y1*y2 + 1)*z2) < APPZERO) &&
((-(y1*y2 + 1)*(y1*y2 + 1) + 2*z1 + z2*(y1*y2 + 1)) >
-APPZERO &&
(-(y1*y2 + 1)*(y1*y2 + 1) + 2*z1 + z2*(y1*y2 + 1)) <
APPZERO)) {
printf(“one solution of NLPS7 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread2(LPVOID pParam)
{HANDLE hThread13 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg12 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - y1*y1 + y2*y1) > -APPZERO &&
(3*x1 - y1*y1 + y2*y1) < APPZERO) &&
((x2 - y2*y1) > -APPZERO &&
(x2 - y2*y1) < APPZERO)) {
printf(“one solution of NLPS3 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg12.i1 = y1;
tharg12.i2 = y2;
hThread13 = CreateThread(NULL, 0, Branch1Thread3,
(LPVOID)&tharg12, 0, NULL);
WaitForSingleObject(hThread13, INFINITE);
CloseHandle(hThread13);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread3(LPVOID pParam)
{HANDLE hThread25 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg23 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - y1*y1 + x2) > -APPZERO &&
(3*x1 - y1*y1 + x2) < APPZERO) &&
((x2 - y2*y1) > -APPZERO &&
(x2 - y2*y1) < APPZERO)) {
printf(“one solution of NLPS5 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg23.i1 = y1;
tharg23.i2 = y2;
hThread25 = CreateThread(NULL, 0, Branch2Thread5,
(LPVOID)&tharg23, 0, NULL);
WaitForSingleObject(hThread25, INFINITE);
CloseHandle(hThread25);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread2(LPVOID pParam)
{HANDLE hThread24 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg22 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - 0.99*y1*y1 + y2*y1 - 0.01*y2*x1) >
-APPZERO &&
(3*x1 - 0.99*y1*y1 + y2*y1 - 0.01*y2*x1) <
APPZERO) &&
((x2 - y2*y1 + 0.01*y2*x1) > -APPZERO &&
(x2 - y2*y1 + 0.01*y2*x1) < APPZERO)) {
printf(“one solution of NLPS4 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg22.i1 = x1;
tharg22.i2 = x2;
hThread24 = CreateThread(NULL, 0, Branch2Thread4,
(LPVOID)&tharg22, 0, NULL);
WaitForSingleObject(hThread24, INFINITE);
CloseHandle(hThread24);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread1(LPVOID pParam)
{HANDLE hThread22 = NULL, hThread23 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg21 = {0};
double m1 = tharg->i1, m2 = tharg->i2;
double x1 = MINIMUMVALUE, x2 = MINIMUMVALUE;
do {
do {
if (((m2*m2 - x1) > -APPZERO &&
(m2*m2 - x1) < APPZERO) &&
((2*m1*m2 + x2) > -APPZERO &&
(2*m1*m2 + x2) < APPZERO)) {
printf(“one solution of NLPS2 is x1 = %f, x2 = %f∖n”, x1, x2);
tharg21.i1 = x1;
tharg21.i2 = x2;
hThread22 = CreateThread(NULL, 0, Branch2Thread2,
(LPVOID)&tharg21, 0, NULL);
hThread23 = CreateThread(NULL, 0, Branch2Thread3,
(LPVOID)&tharg21, 0, NULL);
WaitForSingleObject(hThread22, INFINITE);
WaitForSingleObject(hThread23, INFINITE);
CloseHandle(hThread22);
CloseHandle(hThread23);
}
x2 += GRANULARITY;
}while (x2 <= MAXIMUMVALUE);
x1 += GRANULARITY;
x2 = MINIMUMVALUE;
} while (x1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread1(LPVOID pParam)
{HANDLE hThread12 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg11 = {0};
double m1 = tharg->i1, m2 = tharg->i2;
double x1 = MINIMUMVALUE, x2 = MINIMUMVALUE;
do {
do {
if (((2*m1*m2 + m2*m2 - x1 + x2) > -APPZERO &&
(2*m1*m2 + m2*m2 - x1 + x2) < APPZERO) &&
((2*m1*m2 - m2*m2 + x1 + x2) > -APPZERO &&
(2*m1*m2 - m2*m2 + x1 + x2) < APPZERO)) {
printf(“one solution of NLPS1 is x1 = %f, x2 = %f∖n”, x1, x2);
tharg11.i1 = x1;
tharg11.i2 = x2;
hThread12 = CreateThread(NULL, 0, Branch1Thread2,
(LPVOID)&tharg11, 0, NULL);
WaitForSingleObject(hThread12, INFINITE);
CloseHandle(hThread12);
}
x2 += GRANULARITY;
}while (x2 <= MAXIMUMVALUE);
x1 += GRANULARITY;
x2 = MINIMUMVALUE;
} while (x1 <= MAXIMUMVALUE);
return 0;
}
int main()
{HANDLE hThread1 = NULL, hThread2 = NULL;
LARGE_INTEGER litc, litStart, litEnd;
ThreadArg iTharg = {0};
printf(“Please enter the value of input m1 = ”);
scanf(“%lf”, &iTharg.i1);
printf(“Please enter the value of input m2 = ”);
scanf(“%lf”, &iTharg.i2);
QueryPerformanceFrequency(&litc);
QueryPerformanceCounter(&litStart);
hThread1 = CreateThread(NULL, 0, Branch1Thread1,
(LPVOID)&iTharg, 0, NULL);
hThread2 = CreateThread(NULL, 0, Branch2Thread1,
(LPVOID)&iTharg, 0, NULL);
WaitForSingleObject(hThread1, INFINITE);
WaitForSingleObject(hThread2, INFINITE);
QueryPerformanceCounter(&litEnd);
printf(“Execution time is %fs∖n”, (double)
(litEnd.QuadPart - litStart.QuadPart)/litc.QuadPart);
return 0;
}Letδ=0.1. The maximum number of iterations is NL=10 and the step length of variables is d=0.5 in the full filled method. The recommended values of the variables are in the range from −1 to 1.Step 1.
With the substitution rules and transform rules, change the multithreading program into a nonlinear polynomial transition system, as shown in Figure4.Figure 4
Transition graph.Step 2.
Because the variables of the corresponding branches are the same, there is a need to determine whether there is an equivalence or approximate relation or not of the corresponding polynomial systems in the multithreading program, which is accomplished as follows:(15){NLPS1,NLPS2};{NLPS3,NLPS4,NLPS5};{NLPS6,NLPS7,NLPS8,NLPS9}.
Step
2.1
. For {NLPS1,NLPS2}: Ritt-Wu’s method is applied to verify the relations. Then, we achieve the irreducible characteristic sets as follows:
(16)C1={m22-x1,2m1m2+x2};C2={m22-x1,2m1m2+x2}.
The irreducible characteristic sets are equivalent. Moreover, the behavior ofNLPS2 is simpler; thus, the branch that corresponds to NLPS2 can be used to replace and merge the two branches that correspond to NLPS2 and NLPS1.
Step
2.2
. For {NLPS3,NLPS4,NLPS5}.
First, Ritt-Wu’s method is applied to determine the relation for{NLPS3,NLPS5}. Then, we can obtain the irreducible characteristic sets:
(17)C3=[C31,C32]=[{y12+3x1+x2,-2y1y2+x2},{x1,x2,y1}];C5=[C51,C52]=[{y12+3x1+x2,-2y1y2+x2},{x1,x2,y1}].
Therefore, they are equivalent. The behavior ofNLPS5 is simpler; thus, the branch that corresponds to NLPS5 is used to replace and merge the two branches that correspond to NLPS5 and NLPS3.
ForNLPS4 and NLPS5, the MAX function is chosen to determine the relation for them.
Step
2.2
.
1
. With the full filled method, calculate
(18)min-(3x1-0.99y12+y2y1-0.01y2x1)2-(x2-y2y1+0.01y2x1)2s.t.3x1-y12+x2=0;x2-y2y1=0.
The results are showed in Table1.
In this process, the solutions of the objective function are the same whenK=3 and K=5. The solutions will be duplicated from K=5; thus, the trend in the objective function will become smooth. Then, the result of
(19)max((3x1-0.99y12+y2y1-0.01y2x1)2+(x2-y2y1+0.01y2x1)2)1/2
is 0.0096.
Step
2.2
.
2
. With the full filled method, calculate
(20)min-(x1-y12+x2)2-(x2-y2y1)2s.t.3x1-0.99y12+y2y1-0.01y2x1=0;x2-y2y1+0.01y2x1=0.
The results are showed in Table2.
In this process, the solutions will be duplicated fromK=1. Thus, the trend in the objective function becomes smooth. The result of
(21)max(x1-y12+x2)2+(x2-y2y1)2
is 0.01.
The above two maxima are less than the precision; therefore,NLPS4 and NLPS5 are approximate. The branch that corresponds to NLPS5 can replace and merge the branches that correspond to NLPS3, NLPS4, and NLPS5.
Step
2.3
. For {NLPS6,NLPS7,NLPS8,NLPS9}.
First, the Ritt-Wu’s method is applied to verify the relation forNLPS6 and NLPS7. Then, we obtain the irreducible characteristic sets as follows:
(22)C6=[C61,C62]=[{y12y22+2y1y2+1-3z1,y1y2-3z2+1},{y1y2+1,z1}{y12y22+2y1y2+1-3z1,y1y2-3z2+1}];C7=[C71,C72]=[{y12y22+2y1y2+1-3z1,y1y2-3z2+1},{y1y2+1,z1}{y12y22+2y1y2+1-3z1,y1y2-3z2+1}].
Therefore,NLPS6 and NLPS7 are equivalent. Because NLPS6 is simpler, the branch that corresponds to NLPS6 is used to replace and merge the two branches that correspond to NLPS7 and NLPS6.
ForNLPS8 and NLPS9, the MAX function is used to determine the relation for them.
Step
2.3
.
1
. With the full filled method, calculate
(23)min-(y12-z1)2-(2y1y2-z2)2s.t.y12-(0.01y1+1)z1=0;2y1y2-z2-0.01=0.
The results are showed in Table3.
The results will be duplicated fromK=2. At this point, the trend in the objective function becomes smooth. Thus, the result of
(24)max(y12-z1)2+(2y1y2-z2)2
is 0.011.
Step
2.3
.
2
. With the full filled method, calculate
(25)min-(y12-(0.01y1+1)z1)2-(2y1y2-z2-0.01)2s.t.y12-z1=0;2y1y2-z2=0.
The results are showed in Table4.
There are duplicate minimums whenK=1 and K=2. Thus, the trend in the objective function becomes smooth. Then, the result of
(26)max(y12-(0.01y1+1)z1)2+(2y1y2-z2-0.01)2
is 0.011.
The precision of this layer is0.7-0.01≈0.69. The achieved two maxima are less than this precision; thus, NLPS8 and NLPS9 are approximate. The branch that corresponds to NLPS8 is used to replace and merge the two branches that correspond to NLPS8 and NLPS9.
Step
2.3
.
3
. For NLPS8 and NLPS6, calculate
(27)min-(-(y1y2+1)2+3z1)2-(z2(y1y2+1)-z1)2s.t.y12-z1=0;2y1y2-z2=0.
The results are showed in Table5.
Therefore, the first maximum of(28)(-(y1y2+1)2+3z1)2+(z2(y1y2+1)-z1)2
is 1.95, which is more than the precision in this layer; thus, NLPS8 and NLPS6 are not approximate.
Step
2.4
. By analysis, the transition graph in Figure 4 is turned into a new transition graph, which is shown in Figure 5, and the optimized multithreading program for the given multithreading program in Algorithm 1 also can be expressed in Algorithm 2.Table 1
Results.
Number of iterations:K
Initial states
Solutions
Minimum
K
=
1
(1, 1, 1, 1)
(0.06, 0.82, 1, 0.82)
-
9.08
e
-
005
K
=
2
(0.04, 0.86, 1, 0.86)
(0.05, 0.86, 1, 0.86)
-
9.17
e
-
005
K
=
3
(0.05, 0.85, 1, 0.85)
(0.05, 0.85, 1, 0.85)
-
9.19
e
-
005
K
=
4
(0.04, 0.84, 1, 0.85)
(0.05, 0.84, 1, 0.85)
-
8.97
e
-
005
K
=
5
(0.04, 0.85, 1, 0.84)
(0.05, 0.85, 1, 0.85)
-
9.13
e
-
005Table 2
Results.
Number of iterations:K
Initial states
Solutions
Minimum
K
=
1
(1, 1, 1, 1)
(0.05, 0.84, 1, 0.84)
-
1.00
e
-
004Table 3
Results.
Number of iterations:K
Initial state
Solution
Minimum
K
=
1
(1, 1, 1, 1)
(0.91, 0.56, 0.82, 1)
-
1.21
e
-
004
K
=
2
(0.9, 0.54, 0.83, 0.98)
(0.91, 0.54, 0.82, 0.98)
-
1.20
e
-
004Table 4
Results.
Number of iterations:K
Initial state
Solution
Minimum
K
=
1
(1, 1, 1, 1)
(0.91, 0.55, 0.82, 1)
-
1.21
e
-
004
K
=
2
(0.92, 0.55, 0.84, 0.99)
(0.92, 0.54, 0.84, 0.99)
-
1.21
e
-
004Table 5
Results.
Number of iterations:K
Initial state
Solution
Minimum
K
=
1
(1, 1, 1, 1)
(0.5, 1, 0.25, 1)
−3.81Algorithm 2:Approximate multithreading program.
#include “main.h”
WINMULTITHREAD Branch1Thread3(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) > -APPZERO &&
(-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) < APPZERO) &&
((-z1 + z2*(y1*y2 + 1)) > -APPZERO &&
(-z1 + z2*(y1*y2 + 1)) < APPZERO)) {
printf(“one solution of NLPS13 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread4(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((y1*y1 - z1) > -APPZERO &&
(y1*y1 - z1) < APPZERO) &&
((2*y1*y2 - z2) > -APPZERO &&
(2*y1*y2 - z2) < APPZERO)) {
printf(“one solution of NLPS14 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread2(LPVOID pParam)
{HANDLE hThread13 = NULL, hThread14 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg12 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - y1*y1 + x2) > -APPZERO &&
(3*x1 - y1*y1 + x2) < APPZERO) &&
((x2 - y2*y1) > -APPZERO &&
(x2 - y2*y1) < APPZERO)) {
printf(“one solution of NLPS12 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg12.i1 = y1;
tharg12.i2 = y2;
hThread13 = CreateThread(NULL, 0, Branch1Thread3,
(LPVOID)&tharg12, 0, NULL);
hThread14 = CreateThread(NULL, 0, Branch1Thread4,
(LPVOID)&tharg12, 0, NULL);
WaitForSingleObject(hThread13, INFINITE);
WaitForSingleObject(hThread14, INFINITE);
CloseHandle(hThread13);
CloseHandle(hThread14);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread1(LPVOID pParam)
{HANDLE hThread12 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg11 = {0};
double m1 = tharg->i1, m2 = tharg->i2;
double x1 = MINIMUMVALUE, x2 = MINIMUMVALUE;
do {
do {
if (((m2*m2 - x1) > -APPZERO &&
(m2*m2 - x1) < APPZERO) &&
((2*m1*m2 + x2) > -APPZERO &&
(2*m1*m2 + x2) < APPZERO)) {
printf(“one solution of NLPS11 is x1 = %f, x2 = %f∖n”, x1, x2);
tharg11.i1 = x1;
tharg11.i2 = x2;
hThread12 = CreateThread(NULL, 0, Branch1Thread2,
(LPVOID)&tharg11, 0, NULL);
WaitForSingleObject(hThread12, INFINITE);
CloseHandle(hThread12);
}
x2 += GRANULARITY;
}while (x2 <= MAXIMUMVALUE);
x1 += GRANULARITY;
x2 = MINIMUMVALUE;
} while (x1 <= MAXIMUMVALUE);
return 0;
}
int main()
{LARGE_INTEGER litc, litStart, litEnd;
HANDLE hThread1 = NULL;
ThreadArg iTharg = {0};
printf(“Please enter the value of input m1 = ”);
scanf(“%lf”, &iTharg.i1);
printf(“Please enter the value of input m2 = ”);
scanf(“%lf”, &iTharg.i2);
QueryPerformanceFrequency(&litc);
QueryPerformanceCounter(&litStart);
hThread1 = CreateThread(NULL, 0, Branch1Thread1,
(LPVOID)&iTharg, 0, NULL);
WaitForSingleObject(hThread1, INFINITE);
QueryPerformanceCounter(&litEnd);
printf(“Execution time is %fs∖n”, (double)
(litEnd.QuadPart - litStart.QuadPart)/litc.QuadPart);
return 0;
}Figure 5
Approximate transition graph.


### 5.2. Results

By the example verification in this section, many advantages of our method are achieved.(i)
Achieve a formal description: software programs are represented by nonlinear polynomial transition systems and transition graphs that contain states and transitions, such as in Figures4 and 5. With these descriptions, all of the data exchange processes, the behavior, and the structure of the software program are described more directly.(ii)
With Ritt-Wu’s method and MAX function, the equivalence and approximate relations are determined for the software program based on symbolic-numeric computation.
(a)
With Ritt-Wu’s method and MAX function, the equivalence and approximate relations are expressed by the “standard forms” and “constrained global optimizations” without calculating the exact values of the states of the software programs. The traditional method must know the exact values of the inputs and outputs to determine the relations for the different software programs. Unfortunately, the exact values of the variables of a software program always exist in a range so that the traditional method will cost too much computing time. Thus, our method is more flexible and effective.(b)
Based on these relations, the behavior and structure optimization of software programs are achieved and are compared, whereby Figure4 is compared with Figure 5 and Algorithm 1 is compared with Algorithm 2. For example, the number of branches in Algorithm 1 is 9 and the number of branches in Algorithm 2 is 4.(c)
Because the states and branches of the software programs are reduced with these relations, the number of feasible paths for the software program is decreased; therefore, the “state explosion” problem can be alleviated in the property verification and the occupancy factor of having a deadlock becomes small.(iii)
The value of the behavior and the structure optimization of the software program is divided into two parts, as follows.
(a)
Behavior optimization: for example, for{NLPS1,NLPS2} in Figure 4, NLPS1 is replaced by NLPS2 in Figure 5. If we allow the inputs of the software programs that correspond to NLPS1 and NLPS2 to be equal to 0.0, and let the step length of variable in this process be equal to 0.00005, then the computing costs are 6.789 s and 4.878 s when calculating the same outputs, respectively. Therefore, the simpler the behavior is, the smaller the computing cost. The solutions of the variables and the computing costs of the software programs are given in Table 6.(b)
Structure optimization: for example, the set{NLPS1,NLPS2,NLPS3,NLPS4,NLPS5} in the  given nonlinear polynomial transition system is reduced to two branches {NLPS11,NLPS12} in the approximate system. If we let the initial inputs of NLPS1 and NLPS11 be equal to 0.01 in the programs that correspond to {NLPS1,NLPS2,NLPS3,NLPS4,NLPS5} and {NLPS11,NLPS12} and let the step length of variable in this process be equal to 0.00005, then the computing costs are 12.041 s and 9.678 s when calculating the approximate outputs of the software programs, respectively. Thus, the fewer the number of branches that are present, the lower the computing cost. The solutions of the variables and the computing costs of the software programs are given in Table 6.(iv)
The approximate bisimulation in this paper can also be used to process the type of software programs whose data exchange processes are expressed by linear polynomial systems [11].
(a)
In the calculation algorithms for approximate bisimulation for linear polynomial transition systems, the entire process is a linear computation that is based on the properties of the matrix in paper [11]. However, the whole process in determining the approximate bisimulation relation of the software programs is a nonlinear computation in this paper because the MAX function is applied to compute the value of the errors caused by the approximation. Therefore, the computing process in [11] requires less time and is more effective than the calculation proposed in this paper for linear polynomial systems.(b)
Unfortunately, the method in [11] cannot be applied to process the nonlinear  polynomial system researched in this paper because the property of the matrix cannot describe the solutions’ relations of the nonlinear polynomial systems.Table 6
Results.
Nonlinear polynomial systems
Solutions
Computing costs
NLPS
1
(0.0001, −0.0002)
6.789s
NLPS
2
(0.0001, −0.0002)
4.878s
{
NLPS
1
,
NLPS
2
,
NLPS
3
,
NLPS
4
,
NLPS
5
}
{(0.0001, −0.0002), (0.0001, −0.0002), {(−0.01, 0.02), (0.01, −0.02)}, {(−0.01005, 0.0199), (0.01005, −0.0199)}, {(−0.01, 0.02), (0.01, −0.02)}}
12.041s
{
NLPS
11
,
NLPS
12
}
{(0.0001, −0.0002), {(−0.01, 0.02), (0.01, −0.02)}}
9.678s


## 5.1. Example Verification

The multithreading program is represented in Algorithm1.Algorithm 1:Multithreading program.
#include “main.h”
WINMULTITHREAD Branch2Thread5(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->il, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((y1*y1 - (0.01*y2 + 1)*z1) > -APPZERO &&
(y1*y1 - (0.01*y2 + 1)*z1) < APPZERO) &&
((2*y1*y2 - z2 - 0.01) > -APPZERO &&
(2*y1*y2 - z2 - 0.01) < APPZERO)) {
printf(“one solution of HLPS9 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread4(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((y1*y1 - z1) > -APPZERO &&
(y1*y1 - z1) < APPZERO) &&
((2*y1*y2 - z2) > -APPZERO &&
(2*y1*y2 - z2) < APPZERO)) {
printf(“one solution of NLPS8 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread3(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) > -APPZERO &&
(-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) < APPZERO) &&
((-z1 + z2*(y1*y2 + 1)) > -APPZERO &&
(-z1 + z2*(y1*y2 + 1)) < APPZERO)) {
printf(“one solution of NLPS6 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread4(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((-z1 + (y1*y2 + 1)*z2) > -APPZERO &&
(-z1 + (y1*y2 + 1)*z2) < APPZERO) &&
((-(y1*y2 + 1)*(y1*y2 + 1) + 2*z1 + z2*(y1*y2 + 1)) >
-APPZERO &&
(-(y1*y2 + 1)*(y1*y2 + 1) + 2*z1 + z2*(y1*y2 + 1)) <
APPZERO)) {
printf(“one solution of NLPS7 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread2(LPVOID pParam)
{HANDLE hThread13 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg12 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - y1*y1 + y2*y1) > -APPZERO &&
(3*x1 - y1*y1 + y2*y1) < APPZERO) &&
((x2 - y2*y1) > -APPZERO &&
(x2 - y2*y1) < APPZERO)) {
printf(“one solution of NLPS3 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg12.i1 = y1;
tharg12.i2 = y2;
hThread13 = CreateThread(NULL, 0, Branch1Thread3,
(LPVOID)&tharg12, 0, NULL);
WaitForSingleObject(hThread13, INFINITE);
CloseHandle(hThread13);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread3(LPVOID pParam)
{HANDLE hThread25 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg23 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - y1*y1 + x2) > -APPZERO &&
(3*x1 - y1*y1 + x2) < APPZERO) &&
((x2 - y2*y1) > -APPZERO &&
(x2 - y2*y1) < APPZERO)) {
printf(“one solution of NLPS5 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg23.i1 = y1;
tharg23.i2 = y2;
hThread25 = CreateThread(NULL, 0, Branch2Thread5,
(LPVOID)&tharg23, 0, NULL);
WaitForSingleObject(hThread25, INFINITE);
CloseHandle(hThread25);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread2(LPVOID pParam)
{HANDLE hThread24 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg22 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - 0.99*y1*y1 + y2*y1 - 0.01*y2*x1) >
-APPZERO &&
(3*x1 - 0.99*y1*y1 + y2*y1 - 0.01*y2*x1) <
APPZERO) &&
((x2 - y2*y1 + 0.01*y2*x1) > -APPZERO &&
(x2 - y2*y1 + 0.01*y2*x1) < APPZERO)) {
printf(“one solution of NLPS4 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg22.i1 = x1;
tharg22.i2 = x2;
hThread24 = CreateThread(NULL, 0, Branch2Thread4,
(LPVOID)&tharg22, 0, NULL);
WaitForSingleObject(hThread24, INFINITE);
CloseHandle(hThread24);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch2Thread1(LPVOID pParam)
{HANDLE hThread22 = NULL, hThread23 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg21 = {0};
double m1 = tharg->i1, m2 = tharg->i2;
double x1 = MINIMUMVALUE, x2 = MINIMUMVALUE;
do {
do {
if (((m2*m2 - x1) > -APPZERO &&
(m2*m2 - x1) < APPZERO) &&
((2*m1*m2 + x2) > -APPZERO &&
(2*m1*m2 + x2) < APPZERO)) {
printf(“one solution of NLPS2 is x1 = %f, x2 = %f∖n”, x1, x2);
tharg21.i1 = x1;
tharg21.i2 = x2;
hThread22 = CreateThread(NULL, 0, Branch2Thread2,
(LPVOID)&tharg21, 0, NULL);
hThread23 = CreateThread(NULL, 0, Branch2Thread3,
(LPVOID)&tharg21, 0, NULL);
WaitForSingleObject(hThread22, INFINITE);
WaitForSingleObject(hThread23, INFINITE);
CloseHandle(hThread22);
CloseHandle(hThread23);
}
x2 += GRANULARITY;
}while (x2 <= MAXIMUMVALUE);
x1 += GRANULARITY;
x2 = MINIMUMVALUE;
} while (x1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread1(LPVOID pParam)
{HANDLE hThread12 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg11 = {0};
double m1 = tharg->i1, m2 = tharg->i2;
double x1 = MINIMUMVALUE, x2 = MINIMUMVALUE;
do {
do {
if (((2*m1*m2 + m2*m2 - x1 + x2) > -APPZERO &&
(2*m1*m2 + m2*m2 - x1 + x2) < APPZERO) &&
((2*m1*m2 - m2*m2 + x1 + x2) > -APPZERO &&
(2*m1*m2 - m2*m2 + x1 + x2) < APPZERO)) {
printf(“one solution of NLPS1 is x1 = %f, x2 = %f∖n”, x1, x2);
tharg11.i1 = x1;
tharg11.i2 = x2;
hThread12 = CreateThread(NULL, 0, Branch1Thread2,
(LPVOID)&tharg11, 0, NULL);
WaitForSingleObject(hThread12, INFINITE);
CloseHandle(hThread12);
}
x2 += GRANULARITY;
}while (x2 <= MAXIMUMVALUE);
x1 += GRANULARITY;
x2 = MINIMUMVALUE;
} while (x1 <= MAXIMUMVALUE);
return 0;
}
int main()
{HANDLE hThread1 = NULL, hThread2 = NULL;
LARGE_INTEGER litc, litStart, litEnd;
ThreadArg iTharg = {0};
printf(“Please enter the value of input m1 = ”);
scanf(“%lf”, &iTharg.i1);
printf(“Please enter the value of input m2 = ”);
scanf(“%lf”, &iTharg.i2);
QueryPerformanceFrequency(&litc);
QueryPerformanceCounter(&litStart);
hThread1 = CreateThread(NULL, 0, Branch1Thread1,
(LPVOID)&iTharg, 0, NULL);
hThread2 = CreateThread(NULL, 0, Branch2Thread1,
(LPVOID)&iTharg, 0, NULL);
WaitForSingleObject(hThread1, INFINITE);
WaitForSingleObject(hThread2, INFINITE);
QueryPerformanceCounter(&litEnd);
printf(“Execution time is %fs∖n”, (double)
(litEnd.QuadPart - litStart.QuadPart)/litc.QuadPart);
return 0;
}Letδ=0.1. The maximum number of iterations is NL=10 and the step length of variables is d=0.5 in the full filled method. The recommended values of the variables are in the range from −1 to 1.Step 1.
With the substitution rules and transform rules, change the multithreading program into a nonlinear polynomial transition system, as shown in Figure4.Figure 4
Transition graph.Step 2.
Because the variables of the corresponding branches are the same, there is a need to determine whether there is an equivalence or approximate relation or not of the corresponding polynomial systems in the multithreading program, which is accomplished as follows:(15){NLPS1,NLPS2};{NLPS3,NLPS4,NLPS5};{NLPS6,NLPS7,NLPS8,NLPS9}.
Step
2.1
. For {NLPS1,NLPS2}: Ritt-Wu’s method is applied to verify the relations. Then, we achieve the irreducible characteristic sets as follows:
(16)C1={m22-x1,2m1m2+x2};C2={m22-x1,2m1m2+x2}.
The irreducible characteristic sets are equivalent. Moreover, the behavior ofNLPS2 is simpler; thus, the branch that corresponds to NLPS2 can be used to replace and merge the two branches that correspond to NLPS2 and NLPS1.
Step
2.2
. For {NLPS3,NLPS4,NLPS5}.
First, Ritt-Wu’s method is applied to determine the relation for{NLPS3,NLPS5}. Then, we can obtain the irreducible characteristic sets:
(17)C3=[C31,C32]=[{y12+3x1+x2,-2y1y2+x2},{x1,x2,y1}];C5=[C51,C52]=[{y12+3x1+x2,-2y1y2+x2},{x1,x2,y1}].
Therefore, they are equivalent. The behavior ofNLPS5 is simpler; thus, the branch that corresponds to NLPS5 is used to replace and merge the two branches that correspond to NLPS5 and NLPS3.
ForNLPS4 and NLPS5, the MAX function is chosen to determine the relation for them.
Step
2.2
.
1
. With the full filled method, calculate
(18)min-(3x1-0.99y12+y2y1-0.01y2x1)2-(x2-y2y1+0.01y2x1)2s.t.3x1-y12+x2=0;x2-y2y1=0.
The results are showed in Table1.
In this process, the solutions of the objective function are the same whenK=3 and K=5. The solutions will be duplicated from K=5; thus, the trend in the objective function will become smooth. Then, the result of
(19)max((3x1-0.99y12+y2y1-0.01y2x1)2+(x2-y2y1+0.01y2x1)2)1/2
is 0.0096.
Step
2.2
.
2
. With the full filled method, calculate
(20)min-(x1-y12+x2)2-(x2-y2y1)2s.t.3x1-0.99y12+y2y1-0.01y2x1=0;x2-y2y1+0.01y2x1=0.
The results are showed in Table2.
In this process, the solutions will be duplicated fromK=1. Thus, the trend in the objective function becomes smooth. The result of
(21)max(x1-y12+x2)2+(x2-y2y1)2
is 0.01.
The above two maxima are less than the precision; therefore,NLPS4 and NLPS5 are approximate. The branch that corresponds to NLPS5 can replace and merge the branches that correspond to NLPS3, NLPS4, and NLPS5.
Step
2.3
. For {NLPS6,NLPS7,NLPS8,NLPS9}.
First, the Ritt-Wu’s method is applied to verify the relation forNLPS6 and NLPS7. Then, we obtain the irreducible characteristic sets as follows:
(22)C6=[C61,C62]=[{y12y22+2y1y2+1-3z1,y1y2-3z2+1},{y1y2+1,z1}{y12y22+2y1y2+1-3z1,y1y2-3z2+1}];C7=[C71,C72]=[{y12y22+2y1y2+1-3z1,y1y2-3z2+1},{y1y2+1,z1}{y12y22+2y1y2+1-3z1,y1y2-3z2+1}].
Therefore,NLPS6 and NLPS7 are equivalent. Because NLPS6 is simpler, the branch that corresponds to NLPS6 is used to replace and merge the two branches that correspond to NLPS7 and NLPS6.
ForNLPS8 and NLPS9, the MAX function is used to determine the relation for them.
Step
2.3
.
1
. With the full filled method, calculate
(23)min-(y12-z1)2-(2y1y2-z2)2s.t.y12-(0.01y1+1)z1=0;2y1y2-z2-0.01=0.
The results are showed in Table3.
The results will be duplicated fromK=2. At this point, the trend in the objective function becomes smooth. Thus, the result of
(24)max(y12-z1)2+(2y1y2-z2)2
is 0.011.
Step
2.3
.
2
. With the full filled method, calculate
(25)min-(y12-(0.01y1+1)z1)2-(2y1y2-z2-0.01)2s.t.y12-z1=0;2y1y2-z2=0.
The results are showed in Table4.
There are duplicate minimums whenK=1 and K=2. Thus, the trend in the objective function becomes smooth. Then, the result of
(26)max(y12-(0.01y1+1)z1)2+(2y1y2-z2-0.01)2
is 0.011.
The precision of this layer is0.7-0.01≈0.69. The achieved two maxima are less than this precision; thus, NLPS8 and NLPS9 are approximate. The branch that corresponds to NLPS8 is used to replace and merge the two branches that correspond to NLPS8 and NLPS9.
Step
2.3
.
3
. For NLPS8 and NLPS6, calculate
(27)min-(-(y1y2+1)2+3z1)2-(z2(y1y2+1)-z1)2s.t.y12-z1=0;2y1y2-z2=0.
The results are showed in Table5.
Therefore, the first maximum of(28)(-(y1y2+1)2+3z1)2+(z2(y1y2+1)-z1)2
is 1.95, which is more than the precision in this layer; thus, NLPS8 and NLPS6 are not approximate.
Step
2.4
. By analysis, the transition graph in Figure 4 is turned into a new transition graph, which is shown in Figure 5, and the optimized multithreading program for the given multithreading program in Algorithm 1 also can be expressed in Algorithm 2.Table 1
Results.
Number of iterations:K
Initial states
Solutions
Minimum
K
=
1
(1, 1, 1, 1)
(0.06, 0.82, 1, 0.82)
-
9.08
e
-
005
K
=
2
(0.04, 0.86, 1, 0.86)
(0.05, 0.86, 1, 0.86)
-
9.17
e
-
005
K
=
3
(0.05, 0.85, 1, 0.85)
(0.05, 0.85, 1, 0.85)
-
9.19
e
-
005
K
=
4
(0.04, 0.84, 1, 0.85)
(0.05, 0.84, 1, 0.85)
-
8.97
e
-
005
K
=
5
(0.04, 0.85, 1, 0.84)
(0.05, 0.85, 1, 0.85)
-
9.13
e
-
005Table 2
Results.
Number of iterations:K
Initial states
Solutions
Minimum
K
=
1
(1, 1, 1, 1)
(0.05, 0.84, 1, 0.84)
-
1.00
e
-
004Table 3
Results.
Number of iterations:K
Initial state
Solution
Minimum
K
=
1
(1, 1, 1, 1)
(0.91, 0.56, 0.82, 1)
-
1.21
e
-
004
K
=
2
(0.9, 0.54, 0.83, 0.98)
(0.91, 0.54, 0.82, 0.98)
-
1.20
e
-
004Table 4
Results.
Number of iterations:K
Initial state
Solution
Minimum
K
=
1
(1, 1, 1, 1)
(0.91, 0.55, 0.82, 1)
-
1.21
e
-
004
K
=
2
(0.92, 0.55, 0.84, 0.99)
(0.92, 0.54, 0.84, 0.99)
-
1.21
e
-
004Table 5
Results.
Number of iterations:K
Initial state
Solution
Minimum
K
=
1
(1, 1, 1, 1)
(0.5, 1, 0.25, 1)
−3.81Algorithm 2:Approximate multithreading program.
#include “main.h”
WINMULTITHREAD Branch1Thread3(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) > -APPZERO &&
(-(y1*y2 + 1)*(y1*y2 + 1) + 3*z1) < APPZERO) &&
((-z1 + z2*(y1*y2 + 1)) > -APPZERO &&
(-z1 + z2*(y1*y2 + 1)) < APPZERO)) {
printf(“one solution of NLPS13 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread4(LPVOID pParam)
{PThreadArg tharg = (PThreadArg)pParam;
double y1 = tharg->i1, y2 = tharg->i2;
double z1 = MINIMUMVALUE, z2 = MINIMUMVALUE;
do {
do {
if (((y1*y1 - z1) > -APPZERO &&
(y1*y1 - z1) < APPZERO) &&
((2*y1*y2 - z2) > -APPZERO &&
(2*y1*y2 - z2) < APPZERO)) {
printf(“one solution of NLPS14 is z1 = %f, z2 = %f∖n”, z1, z2);
}
z2 += GRANULARITY;
}while (z2 <= MAXIMUMVALUE);
z1 += GRANULARITY;
z2 = MINIMUMVALUE;
} while (z1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread2(LPVOID pParam)
{HANDLE hThread13 = NULL, hThread14 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg12 = {0};
double x1 = tharg->i1, x2 = tharg->i2;
double y1 = MINIMUMVALUE, y2 = MINIMUMVALUE;
do {
do {
if (((3*x1 - y1*y1 + x2) > -APPZERO &&
(3*x1 - y1*y1 + x2) < APPZERO) &&
((x2 - y2*y1) > -APPZERO &&
(x2 - y2*y1) < APPZERO)) {
printf(“one solution of NLPS12 is y1 = %f, y2 = %f∖n”, y1, y2);
tharg12.i1 = y1;
tharg12.i2 = y2;
hThread13 = CreateThread(NULL, 0, Branch1Thread3,
(LPVOID)&tharg12, 0, NULL);
hThread14 = CreateThread(NULL, 0, Branch1Thread4,
(LPVOID)&tharg12, 0, NULL);
WaitForSingleObject(hThread13, INFINITE);
WaitForSingleObject(hThread14, INFINITE);
CloseHandle(hThread13);
CloseHandle(hThread14);
}
y2 += GRANULARITY;
}while (y2 <= MAXIMUMVALUE);
y1 += GRANULARITY;
y2 = MINIMUMVALUE;
} while (y1 <= MAXIMUMVALUE);
return 0;
}
WINMULTITHREAD Branch1Thread1(LPVOID pParam)
{HANDLE hThread12 = NULL;
PThreadArg tharg = (PThreadArg)pParam;
ThreadArg tharg11 = {0};
double m1 = tharg->i1, m2 = tharg->i2;
double x1 = MINIMUMVALUE, x2 = MINIMUMVALUE;
do {
do {
if (((m2*m2 - x1) > -APPZERO &&
(m2*m2 - x1) < APPZERO) &&
((2*m1*m2 + x2) > -APPZERO &&
(2*m1*m2 + x2) < APPZERO)) {
printf(“one solution of NLPS11 is x1 = %f, x2 = %f∖n”, x1, x2);
tharg11.i1 = x1;
tharg11.i2 = x2;
hThread12 = CreateThread(NULL, 0, Branch1Thread2,
(LPVOID)&tharg11, 0, NULL);
WaitForSingleObject(hThread12, INFINITE);
CloseHandle(hThread12);
}
x2 += GRANULARITY;
}while (x2 <= MAXIMUMVALUE);
x1 += GRANULARITY;
x2 = MINIMUMVALUE;
} while (x1 <= MAXIMUMVALUE);
return 0;
}
int main()
{LARGE_INTEGER litc, litStart, litEnd;
HANDLE hThread1 = NULL;
ThreadArg iTharg = {0};
printf(“Please enter the value of input m1 = ”);
scanf(“%lf”, &iTharg.i1);
printf(“Please enter the value of input m2 = ”);
scanf(“%lf”, &iTharg.i2);
QueryPerformanceFrequency(&litc);
QueryPerformanceCounter(&litStart);
hThread1 = CreateThread(NULL, 0, Branch1Thread1,
(LPVOID)&iTharg, 0, NULL);
WaitForSingleObject(hThread1, INFINITE);
QueryPerformanceCounter(&litEnd);
printf(“Execution time is %fs∖n”, (double)
(litEnd.QuadPart - litStart.QuadPart)/litc.QuadPart);
return 0;
}Figure 5
Approximate transition graph.


## 5.2. Results

By the example verification in this section, many advantages of our method are achieved.(i)
Achieve a formal description: software programs are represented by nonlinear polynomial transition systems and transition graphs that contain states and transitions, such as in Figures4 and 5. With these descriptions, all of the data exchange processes, the behavior, and the structure of the software program are described more directly.(ii)
With Ritt-Wu’s method and MAX function, the equivalence and approximate relations are determined for the software program based on symbolic-numeric computation.
(a)
With Ritt-Wu’s method and MAX function, the equivalence and approximate relations are expressed by the “standard forms” and “constrained global optimizations” without calculating the exact values of the states of the software programs. The traditional method must know the exact values of the inputs and outputs to determine the relations for the different software programs. Unfortunately, the exact values of the variables of a software program always exist in a range so that the traditional method will cost too much computing time. Thus, our method is more flexible and effective.(b)
Based on these relations, the behavior and structure optimization of software programs are achieved and are compared, whereby Figure4 is compared with Figure 5 and Algorithm 1 is compared with Algorithm 2. For example, the number of branches in Algorithm 1 is 9 and the number of branches in Algorithm 2 is 4.(c)
Because the states and branches of the software programs are reduced with these relations, the number of feasible paths for the software program is decreased; therefore, the “state explosion” problem can be alleviated in the property verification and the occupancy factor of having a deadlock becomes small.(iii)
The value of the behavior and the structure optimization of the software program is divided into two parts, as follows.
(a)
Behavior optimization: for example, for{NLPS1,NLPS2} in Figure 4, NLPS1 is replaced by NLPS2 in Figure 5. If we allow the inputs of the software programs that correspond to NLPS1 and NLPS2 to be equal to 0.0, and let the step length of variable in this process be equal to 0.00005, then the computing costs are 6.789 s and 4.878 s when calculating the same outputs, respectively. Therefore, the simpler the behavior is, the smaller the computing cost. The solutions of the variables and the computing costs of the software programs are given in Table 6.(b)
Structure optimization: for example, the set{NLPS1,NLPS2,NLPS3,NLPS4,NLPS5} in the  given nonlinear polynomial transition system is reduced to two branches {NLPS11,NLPS12} in the approximate system. If we let the initial inputs of NLPS1 and NLPS11 be equal to 0.01 in the programs that correspond to {NLPS1,NLPS2,NLPS3,NLPS4,NLPS5} and {NLPS11,NLPS12} and let the step length of variable in this process be equal to 0.00005, then the computing costs are 12.041 s and 9.678 s when calculating the approximate outputs of the software programs, respectively. Thus, the fewer the number of branches that are present, the lower the computing cost. The solutions of the variables and the computing costs of the software programs are given in Table 6.(iv)
The approximate bisimulation in this paper can also be used to process the type of software programs whose data exchange processes are expressed by linear polynomial systems [11].
(a)
In the calculation algorithms for approximate bisimulation for linear polynomial transition systems, the entire process is a linear computation that is based on the properties of the matrix in paper [11]. However, the whole process in determining the approximate bisimulation relation of the software programs is a nonlinear computation in this paper because the MAX function is applied to compute the value of the errors caused by the approximation. Therefore, the computing process in [11] requires less time and is more effective than the calculation proposed in this paper for linear polynomial systems.(b)
Unfortunately, the method in [11] cannot be applied to process the nonlinear  polynomial system researched in this paper because the property of the matrix cannot describe the solutions’ relations of the nonlinear polynomial systems.Table 6
Results.
Nonlinear polynomial systems
Solutions
Computing costs
NLPS
1
(0.0001, −0.0002)
6.789s
NLPS
2
(0.0001, −0.0002)
4.878s
{
NLPS
1
,
NLPS
2
,
NLPS
3
,
NLPS
4
,
NLPS
5
}
{(0.0001, −0.0002), (0.0001, −0.0002), {(−0.01, 0.02), (0.01, −0.02)}, {(−0.01005, 0.0199), (0.01005, −0.0199)}, {(−0.01, 0.02), (0.01, −0.02)}}
12.041s
{
NLPS
11
,
NLPS
12
}
{(0.0001, −0.0002), {(−0.01, 0.02), (0.01, −0.02)}}
9.678s


## 6. Conclusions

In this paper, we propose a nonlinear polynomial transition system to describe the type of software program whose data exchange processes are expressed by nonlinear polynomial systems. Then, a novel calculation of an approximate bisimulation is provided to achieve the behavior and the structure optimization for the software programs, based on symbolic-numeric computation. The advantages of our approach are verified and listed in Section5.Except for those advantages that are achieved by our approach in this paper, on the one hand, how to improve the efficiency of symbolic-numeric computation is a substantial challenge. This goal will be researched in our future work. On the other hand, the numbers of the states and branches of the software program are reduced due to the behavior and the structure optimization. How to apply these circumstances to optimize the property verification of the software program based on the state, such as safety verification, is also a major direction for our research in the future.



---

*Source: 421926-2013-09-30.xml*