Approximate Bisimulation For Polynomial Transition Systems Based On Symbolic-numeric Computation

With the development of computer, the structure and behavior of a program turn to be complex because user's requirements are increasing for the function of program. It becomes more difficult to conduct both design and property verification. Therefore, a method that is able to optimize the behavior and structure of programs need to be researched and achieved.In the research, to establish an appropriate formal description is a prerequisite to study the behavior and structure of a program based on the existing research results. The previous formal descriptions of programs that consist of abstract behaviors, discrete states and the transitions between states are discrete. They are good at calculating and reasoning against programs based upon state ergodicity. Nevertheless, these descriptions cannot express and deal with the data exchange processes of programs, which are the behavior of programs. From the perspective of the behavior and structure of programs by formal method, to research this type of program whose data exchange processes are described by polynomial systems is the basis to study other types of programs. Besides achieving a description, to define and determine the behavior equivalence for the programs is the key to obtain their behavior and structure optimization. Two programs are equivalent represents that they have the same behavior. Bisimulation is the finest equivalence we can utilize for now. With bisimulation, we obtain an optimization for a given program with removing the extra equivalent nondeterministic branches and replacing the complex branches with a simple branch. However, the exact behavior equivalence is too restrictive to be a good solution for a majority of programs in the application. Therefore, to strengthen the flexibility of the relationship between two programs, we relax the restriction of equivalence and propose an approximate relation within a controllable error range, and select appropriate numerical methods to establish an approximate calculation for them.In order to meet the above requirements, this thesis primarily focuses on the behavior and structure optimization for the programs. Three different types of formal descriptions are proposed to partition and describe the kind of program whose data exchange processes can be represented by polynomial systems; then, establish the calculations of bisimulation and approximate bisimulation respectively based upon symbolic-numeric computation. The contributions are as follows. (1) Establish a partition method for the data exchange processes of a program. For the type of program whose data exchange processes are represented by homogeneous linear polynomial systems, a transformation between a data exchange process and a homogeneous linear polynomial system, and a formal description called homogeneous linear polynomial transition system which can be applied to describe the data exchange processes and structure of a program are received. With bisimulation and the nature of the coefficient matrixs of homogeneous linear polynomial systems, the definition and calculation of bisimulation for this kind of program are proposed and considered as the most precise equivalence relation. Besides, to enhance the flexibility of the relation between two programs, the notion and computation of approximate bisimulation are developed within given error and variable ranges. In this process, the error is calculated by matrix norm. Approximate programs are achieved for original programs by singular value decomposition if the actual error is bigger than the given error but it is not more than twice the given error. The experiment indicates that approximate bisimulation achieves behavior and structure optimization for this kind of program.(2) A formal description called non-homogeneous linear polynomial transition system is proposed which shows a type of program whose data exchange processes are represented by non-homogeneous linear polynomial systems. As there exist constant terms in this kind of polynomial system, the calculation of approximation proposed for homogeneous linear polynomial transition system cannot be utilized. To deal with this problem, the definition and calculation of bisimulation and approximate bisimulation of programs are achieved within the given error and extended variable ranges based on the characteristic of augmented matrixs of non-homogeneous linear polynomial systems. The actual error is computed by matrix norm. Approximate programs are able to be achieved for original programs by QR decomposition if the actual error is bigger than the given error but it is not more than twice the given error. The experiment verifies that approximate bisimulation is of great use to optimize the behavior and structure of this type of program. Meanwhile, the process in finding approximate programs with QR decomposition costs less time and space than the same process with singular value decomposition in the homogeneous linear polynomial transition system.(3) Obtain a formal description named nonlinear polynomial transition system. It is used to describe a type of program whose data exchange processes are represented by nonlinear polynomial systems. Based upon this description, a notion of bisimulation for these programs is proposed and two different calculation methods for bisimulation are proposed with the Ritt-Wu's method and Groebner Basis method respectively. Moreover, approximate bisimulation is established within a controlled error range while there is no variable range. In this process, the approximate relation is expressed as a constrained global optimization called Max function that is resolved by the filled function method. The actual error is calculable. An approximate program is proposed by approximately processing the initial sets of the characteristic sets of polynomial systems if the actual error is bigger than the given error but it is not more than twice the given error. The experiment shows that the approximate bisimulation is effective in the behavior and structure optimization for this type of program. Meanwhile, the description and methods proposed for nonlinear polynomial transition system is universal for the all kinds of programs researched in this thesis.To sum up, this thesis pays close attention to behavior and structure optimization of program, and conducts the researches on formal descriptions that can express the data exchange processes of programs, bisimulation and approximate bisimulation. The relative complete theories of equivalence and approximation are established for the kind of program whose data exchange processes are showed by polynomial systems, which provides a formal solution for program optimization.