基于符号与数值混合计算的多项式变迁系统近似互模拟
|
摘要
计算机飞速发展,促使用户需求单个程序实现更多功能,导致程序行为及结构复杂化,不利于程序设计及性质验证工作。因此,程序行为及结构优化亟待研究及实现。
程序行为及结构优化过程中,创建合理的程序形式化刻画系统是研究程序行为及结构的前提。早期的程序形式化刻画系统大都离散化,由抽象的动作、离散的状态及状态间的转移关系构成,可对程序进行基于状态遍历的计算和推理。遗憾的是,它们无法对程序行为即数据流交换过程进行表示和处理。从形式化的角度出发,数据流交换过程可用多项式系统表示的程序是最基础的一类。在了解程序具体行为及整体结构后,定义及判定程序行为等价是实现行为及结构优化的根本。具有相同行为的程序称为等价。基于最精确的系统等价关系互模拟实现程序等价判定,一方面去掉程序中重复的非确定性分支可实现结构优化,另一方面利用行为简单的分支代替行为复杂的分支可实现行为优化。但是,在大部分程序实际应用中,精确的等价关系显得太过严格,适当的近似不会对程序最终结果产生很大影响。为加强程序间关系的灵活性,可在误差范围内放宽等价限制,提出程序近似互模拟概念,并利用数值计算方法创建带误差且误差可控的近似互模拟计算方法,最终实现程序行为及结构近似优化。
立足以上需求,本文围绕程序行为及结构优化这一主旨展开研究。针对数据流交换过程可以用多项式系统表示的程序,根据行为特征将之细分为三类,然后分别建立可描述其数据流交换过程的形式化刻画系统,并利用符号与数值混合计算创建程序互模拟及近似互模拟计算方法,其主要贡献包括：
(1)构建了程序数据流交换过程划分规则。针对数据流交换过程可用齐次线性多项式系统描述的一类程序,构建了数据流交换过程与齐次线性多项式系统间转换规则。研究得到齐次线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。提出了程序精确行为等价概念,称之为互模拟。基于齐次线性多项式系统系数矩阵的性质,给出了程序互模拟等价计算方法。同时,在给定的变量取值及误差范围内,建立了带误差且误差可控的近似互模拟定义及计算方法,通过矩阵范数实现了近似过程中实际误差的度量。对于实际误差大于给定误差但不大于两倍的给定误差的程序,通过奇异值分解实现了近似程序的求解。实验证明近似互模拟可实现一类程序行为及结构优化。
(2)针对数据流交换过程可用非齐次线性多项式系统描述的一类程序,构建了数据流交换过程与非齐次线性多项式系统间转换规则。研究得到非齐次线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。基于互模拟等价及非齐次线性多项式系统增广矩阵的性质,实现了此类程序互模拟等价判定。在非齐次线性多项式系统中,由于常数项的引入,使得针对齐次线性多项式系统建立的近似方法无法得以沿用。为此,在扩大的变量取值范围及给定误差范围内,为此类程序建立了带误差且误差可控的近似互模拟计算方法,通过矩阵范数实现了实际误差的度量。对于实际误差大于给定误差但不大于两倍给定误差的程序,基于QR分解实现了近似程序的求解。实验表明近似互模拟在优化此类程序行为及结构中可行及有效,且近似程序求解过程比齐次线性多项式变迁系统中相应过程节省时间和空间。
(3)针对数据流交换过程可用非线性多项式系统描述的一类程序,构建了数据流交换过程与非线性多项式系统间转换规则。研究了非线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。针对线性多项式变迁系统互模拟判定方法无法沿用的问题,基于吴特征列和Groebner基方法实现非线性多项式变迁系统互模拟等价判定,对比分析发现吴特征列方法更优。同时,针对线性多项式变迁系统近似互模拟均需约束变量取值范围的问题,通过对非线性多项式变迁系统近似关系的分析,在无需给定变量取值范围的前提下,在给定误差范围内建立了带误差且误差可控的近似互模拟概念及计算方法。在此过程中近似关系被描述为一个全局最优化问题,称为Max函数,通过填充函数法处理此函数,实现实际误差度量。对于实际误差大于给定误差但不大于两倍的给定误差的程序,通过近似调整非线性多项式系统对应特征列系统中的初式集合,得到了求解近似程序的方法构想。实验表明近似互模拟计算方法实现了程序行为及结构优化,且非线性多项式变迁系统的描述规则及近似互模拟计算方法对于本文所研究的所有类型程序均通用。
综上所述,本文以程序行为及结构优化为目标,对可描述程序数据流交换的形式化刻画系统、程序互模拟等价及近似互模拟进行了研究,针对数据流交换过程可用多项式系统表示的程序建立了比较完整的等价及近似理论,为程序行为及结构优化提供了一种形式化的解决思路。
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.
程序行为及结构优化过程中,创建合理的程序形式化刻画系统是研究程序行为及结构的前提。早期的程序形式化刻画系统大都离散化,由抽象的动作、离散的状态及状态间的转移关系构成,可对程序进行基于状态遍历的计算和推理。遗憾的是,它们无法对程序行为即数据流交换过程进行表示和处理。从形式化的角度出发,数据流交换过程可用多项式系统表示的程序是最基础的一类。在了解程序具体行为及整体结构后,定义及判定程序行为等价是实现行为及结构优化的根本。具有相同行为的程序称为等价。基于最精确的系统等价关系互模拟实现程序等价判定,一方面去掉程序中重复的非确定性分支可实现结构优化,另一方面利用行为简单的分支代替行为复杂的分支可实现行为优化。但是,在大部分程序实际应用中,精确的等价关系显得太过严格,适当的近似不会对程序最终结果产生很大影响。为加强程序间关系的灵活性,可在误差范围内放宽等价限制,提出程序近似互模拟概念,并利用数值计算方法创建带误差且误差可控的近似互模拟计算方法,最终实现程序行为及结构近似优化。
立足以上需求,本文围绕程序行为及结构优化这一主旨展开研究。针对数据流交换过程可以用多项式系统表示的程序,根据行为特征将之细分为三类,然后分别建立可描述其数据流交换过程的形式化刻画系统,并利用符号与数值混合计算创建程序互模拟及近似互模拟计算方法,其主要贡献包括：
(1)构建了程序数据流交换过程划分规则。针对数据流交换过程可用齐次线性多项式系统描述的一类程序,构建了数据流交换过程与齐次线性多项式系统间转换规则。研究得到齐次线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。提出了程序精确行为等价概念,称之为互模拟。基于齐次线性多项式系统系数矩阵的性质,给出了程序互模拟等价计算方法。同时,在给定的变量取值及误差范围内,建立了带误差且误差可控的近似互模拟定义及计算方法,通过矩阵范数实现了近似过程中实际误差的度量。对于实际误差大于给定误差但不大于两倍的给定误差的程序,通过奇异值分解实现了近似程序的求解。实验证明近似互模拟可实现一类程序行为及结构优化。
(2)针对数据流交换过程可用非齐次线性多项式系统描述的一类程序,构建了数据流交换过程与非齐次线性多项式系统间转换规则。研究得到非齐次线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。基于互模拟等价及非齐次线性多项式系统增广矩阵的性质,实现了此类程序互模拟等价判定。在非齐次线性多项式系统中,由于常数项的引入,使得针对齐次线性多项式系统建立的近似方法无法得以沿用。为此,在扩大的变量取值范围及给定误差范围内,为此类程序建立了带误差且误差可控的近似互模拟计算方法,通过矩阵范数实现了实际误差的度量。对于实际误差大于给定误差但不大于两倍给定误差的程序,基于QR分解实现了近似程序的求解。实验表明近似互模拟在优化此类程序行为及结构中可行及有效,且近似程序求解过程比齐次线性多项式变迁系统中相应过程节省时间和空间。
(3)针对数据流交换过程可用非线性多项式系统描述的一类程序,构建了数据流交换过程与非线性多项式系统间转换规则。研究了非线性多项式变迁系统,用于描述此类程序数据流交换过程及结构。针对线性多项式变迁系统互模拟判定方法无法沿用的问题,基于吴特征列和Groebner基方法实现非线性多项式变迁系统互模拟等价判定,对比分析发现吴特征列方法更优。同时,针对线性多项式变迁系统近似互模拟均需约束变量取值范围的问题,通过对非线性多项式变迁系统近似关系的分析,在无需给定变量取值范围的前提下,在给定误差范围内建立了带误差且误差可控的近似互模拟概念及计算方法。在此过程中近似关系被描述为一个全局最优化问题,称为Max函数,通过填充函数法处理此函数,实现实际误差度量。对于实际误差大于给定误差但不大于两倍的给定误差的程序,通过近似调整非线性多项式系统对应特征列系统中的初式集合,得到了求解近似程序的方法构想。实验表明近似互模拟计算方法实现了程序行为及结构优化,且非线性多项式变迁系统的描述规则及近似互模拟计算方法对于本文所研究的所有类型程序均通用。
综上所述,本文以程序行为及结构优化为目标,对可描述程序数据流交换的形式化刻画系统、程序互模拟等价及近似互模拟进行了研究,针对数据流交换过程可用多项式系统表示的程序建立了比较完整的等价及近似理论,为程序行为及结构优化提供了一种形式化的解决思路。
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.
引文
[1]Mowery D C. International computer software industry [M]. Oxford University Press,1995.
[2]Wolfram S. Computer Software in Science and Mathematics [J]. Scientific American,1984, 251(3):188-92,194,196-200,203.
[3]Adrion W R, Branstad M A, Cherniavsky J C. Validation, verification, and testing of computer software [J]. ACM Computing Surveys,1982,14(2):159-192.
[4]Jurs P C. Computer software applications in chemistry [M]. John Wiley & Sons,1986.
[5]Lenat D B. Computer Software for Intelligent Systems [J]. Scientific American,1984,251(3): 204-09,211-13.
[6]Wallace D R, Fujii R U. Software verification and validation:an overview [J]. IEEE Software, 1989,6(3):10-17.
[7]Jennings N R. An agent-based approach for building complex software systems [J]. Communications of the ACM,2001,44(4):35-41.
[8]Fenton N E, Ohlsson N. Quantitative analysis of faults and failures in a complex software system [J]. IEEE Transactions on Software Engineering,2000,26(8):797-814.
[9]Leveson N G, Harvey P R. Analyzing software safety [J]. IEEE Transactions on Software Engineering,1983, (5):569-579.
[10]Henzinger T A, Jhala R, Majumdar R, Sutre G. Software verification with BLAST [M]. Model Checking Software. Springer Berlin Heidelberg,2003:235-239.
[11]Leveson NG. Software safety:why, what, and how [J]. ACM Computing Surveys,1986,18(2): 125-163.
[12]Wadleigh K R, Crawford I L. Software Optimization for High-Performance Computers [M]. Prentice Hall Professional,2000.
[13]Ammar R A, Booth T L. Software optimization using user models [J]. IEEE Transactions on Systems, Man and Cybernetics,1988,18(4):552-560.
[14]Peymandoust A, Simunic T, De Micheli G Low power embedded software optimization using symbolic algebra [C]. Design, Automation and Test in Europe Conference and Exhibition, 2002,1052-1058.
[15]Dolan E D, More J J. Benchmarking optimization software with performance profiles [J]. Mathematical programming,2002,91(2):201-213.
[16]Voβ S, Woodruff D L. Optimization software class libraries [M]. Springer US,2003.
[17]Carson Y, Maria A. Simulation optimization:methods and applications [C]. Proceedings of the 29th conference on Winter Simulation.1997,118-126.
[18]Poles S, Vassileva M, Sasaki D. Multiobjective optimization software [M]. Multiobjective Optimization. Springer Berlin Heidelberg,2008,329-348.
[19]Pitchumani V, Stabler E P.A formal method for computer design verification [C]. The 19th Conference on Design Automation,1982,809-814.
[20]Heitmeyer C. On the need for practical formal methods [C]. Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer Berlin Heidelberg,1998,18-26.
[21]Fidge C, Kearney P, Utting M. A formal method for building concurrent real-time software [J]. IEEE Software,1997,14(2):99-106.
[22]Mullin L M R, Thibault S A, Dooling D R, et al. Formal method for scheduling, routing and communication protocol [C]. Proceedings of the 2nd International Symposium on High Performance Distributed Computing,1993,234-242.
[23]Wing J M. A specifier's introduction to formal methods [J]. Computer,1990,23(9):8-22.
[24]Yu H, He X, Deng Y, et al. A formal method for analyzing software architecture models in SAM [C]. The Conference of Computer Software and Applications,2002,645-652.
[25]Shoenfield J R. Mathematical logic [M]. Reading:Addison-Wesley,1967.
[26]Pnueli A. The temporal logic of programs[C]. The 18th Annual Symposium on Foundations of Computer Science,1977,46-57.
[27]Girard J Y. Linear logic [J]. Theoretical computer science,1987,50(1):1-101.
[28]Nerode A. Linear automaton transformations [J]. Proceedings of the American Mathematical Society,1958,9(4):541-544.
[29]Toffoli T. CAM:A high-performance cellular-automaton machine [J]. Physica D:Nonlinear Phenomena,1984,10(1):195-204.
[30]Maraninchi F, Remond Y. Argos:an automaton-based synchronous language [J]. Computer languages,2001,27(1):61-92.
[31]Gunnels J A, Gustavson F G, Henry G M, et al. FLAME:Formal linear algebra methods environment [J]. ACM Transactions on Mathematical Software,2001,27(4):422-455.
[32]Hoare C A R. An overview of some formal methods for program design [J]. Computer,1987, 20(9):85-91.
[33]Hermanns H, Herzog U, Katoen J P. Process algebra for performance evaluation [J]. Theoretical computer science,2002,274(1):43-87.
[34]Christofides N. Graph theory:An algorithmic approach [M]. Academic Press,1975.
[35]Bondy J A, Murty U S R. Graph theory with applications [M]. London:Macmillan,1976.
[36]ERDOS P. Graph theory and probability [J]. Canadian Journal of Mathematics,1959,11(1): 34.
[37]Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications [J]. ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.
[38]Van Glabbeek R, Goltz U. Equivalence notions for concurrent systems and refinement of actions[C]. Mathematical Foundations of Computer Science 1989. Springer Berlin Heidelberg, 1989,237-248..
[39]Winskel G, Nielsen M. Models for concurrency [J]. DAIMI Report Series,1993,22(463).
[40]Henzinger T A. The theory of hybrid automata [M]. Springer Berlin Heidelberg,2000.
[41]Milner R, Sangiorgi D. Barbed bisimulation [M]. Automata, Languages and Programming. Springer Berlin Heidelberg,1992,685-695.
[42]Weyuker E J. Evaluating software complexity measures [J]. IEEE Transactions on Software Engineering,1988,14(9):1357-1365.
[43]Mens T, Tourwe T. A survey of software refactoring [J]. IEEE Transactions on Software Engineering,2004,30(2):126-139.
[44]Horwitz S, Reps T. The use of program dependence graphs in software engineering [C]. Proceedings of the 14th international conference on Software engineering,1992,392-411.
[45]Rosenberg A L. Nondeterminism in Computability Theory [M]. The Pillars of Computation Theory. Springer New York,2010,233-244.
[46]Barbosa L S, Oliveira J N. Transposing partial components-an exercise on coalgebraic refinement [J]. Theoretical Computer Science,2006,365(1):2-22.
[47]Van Glabbeek R J. The linear time-branching time spectrum [M]. Springer Berlin Heidelberg, 1990.
[48]Larsen K G, Skou A. Bisimulation through probabilistic testing [J]. Information and computation,1991,94(1):1-28..
[49]Van Glabbeek R J, Weijland W P. Branching time and abstraction in bisimulation semantics [J]. Journal of the ACM,1996,43(3):555-600.
[50]Desharnais J, Edalat A, Panangaden P. Bisimulation for labelled Markov processes [J]. Information and Computation,2002,179(2):163-193.
[51]Bloom B, Istrail S, Meyer A R. Bisimulation can't be traced [J]. Journal of the ACM,1995, 42(1):232-268.
[52]De Nicola R, Vaandrager F. Three logics for branching bisimulation [J]. Journal of the ACM, 1995,42(2):458-487.
[53]Groote J F, Vaandrager F. Structured operational semantics and bisimulation as a congruence [J]. Information and computation,1992,100(2):202-260.
[54]Smith J, De Micheli G. Polynomial methods for allocating complex components [C]. Proceedings of the conference on Design, automation and test in Europe,1999.
[55]Smith J, De Micheli G. Polynomial circuit models for component matching in high-level synthesis [J]. IEEE Transactions on Very Large Scale Integration Systems,2001,9(6):783-800.
[56]Peymandoust A, De Micheli G. Using symbolic algebra in algorithmic level DSP synthesis [C]. The Conference of Design Automation,2001,277-282.
[57]Zhi Y, Guangsheng M, Shu21 Z. Equivalence Verification of High-Level Datapaths Based on Polynomial Symbolic Algebra [J]. Journal of Computer Research and Development,2009,3: 023.
[58]Buchberger B. A view on the future of symbolic computation [C]. Proceedings of the 2005 international symposium on Symbolic and algebraic computation. ACM,2005,1-1.
[59]Chaochen Z. Program verification through computer algebra [M]. Formal Methods and Software Engineering. Springer Berlin Heidelberg,2006,1-1.
[60]王东明,法学.消去法及其应用[M].科学出版社,2002.
[61]吴文俊.数学机械化[M].科学出版社,2003.
[62]Halstead Jr R H. Multilisp:A language for concurrent symbolic computation [J]. ACM Transactions on Programming Languages and Systems,1985,7(4):501-538.
[63]Lafferriere G, Pappas G J, Yovine S. Symbolic reachability computation for families of linear vector fields [J]. Journal of Symbolic Computation,2001,32(3):231-253.
[64]Touretzky D S. LISP:a gentle introduction to symbolic computation [M]. John Wiley & Sons, Inc.,1984.
[65]王东明.符号计算选讲[M].北京：清华大学出版社.2003.
[66]张军.数值计算[M].北京：清华大学出版社.2008.
[67]Beyn W J. The numerical computation of connecting orbits in dynamical systems [J]. IMA Journal of Numerical Analysis,1990,10(3):379-405.
[68]Higham N J. Numerical Computation:Methods, Software, and Analysis [J]. IEEE Computational Science & Engineering,1998,5(1):79.
[69]Pozrikidis C. Numerical computation in science and engineering [M]. New York:Oxford university press,1998.
[70]支丽红.符号与数值混合计算[J].系统科学与数学.2008.28(8)：1040-1052.
[71]唐焕文.实用最优化方法[M].大连：大连理工大学出版社.2007.33-45.
[72]Stanley P C, Pilkington T C. The combination method:A numerical technique for electrocardiographic calculations [J]. IEEE Transactions on Biomedical Engineering,1989, 36(4):456-461.
[73]Jerard R B, Hussaini S Z, Drysdale R L, et al. Approximate methods for simulation and verification of numerically controlled machining programs [J]. The Visual Computer,1989, 5(6):329-348.
[74]盛骤,谢式千,潘承毅.概率论与数理统计[M].北京：高等教育出版社.2001.25-67.
[75]Yap C K. Towards exact geometric computation [J]. Computational Geometry,1997,7(1): 3-23.
[76]Nolan J P. Numerical calculation of stable densities and distribution functions [J]. Communications in statistics. Stochastic models,1997,13(4):759-774.
[77]Hoare C A R. Communicating sequential processes [J]. Communications of the ACM,1978, 21(8):666-677.
[78]Milner R. A calculus of communicating systems [M]. Springer-Verlag New York,1982.
[79]Bergstra J A, Klop J W. Algebra of communicating processes with abstraction [J]. Theoretical computer science,1985,37:77-121.
[80]Bolognesi T, Brinksma E. Introduction to the ISO specification language LOTOS [J]. Computer Networks and ISDN systems,1987,14(1):25-59.
[81]Pnueli A. The temporal logic of programs [C]. The 18th Annual Symposium on Foundations of Computer Science,1977:46-57.
[82]Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications [J]. ACM Transactions on Programming Languages and Systems (TOPLAS),1986,8(2):244-263.
[83]Emerson E A, Halpern J Y. "Sometimes" and "not never" revisited:on branching versus linear time temporal logic [J]. Journal of the ACM,1986,33(1):151-178.
[84]Petri C A. Nets, time and space [J]. Theoretical computer science,1996,153(1):3-48.
[85]Browne M C, Clarke E M, Grumberg O. Characterizing finite Kripke structures in propositional temporal logic [J]. Theoretical Computer Science,1988,59(1):115-131.
[86]Biere A, Cimatti A, Clarke E, et al. Symbolic model checking without BDDs [M]. Springer Berlin Heidelberg,1999.
[87]Pustejovsky J. The syntax of event structure [J]. Cognition.1991.41(3-1):47-81.
[88]Manna Z, Pnueli A. Temporal verification of reactive systems:safety [M]. USA. Springer. 1995:10-27.
[89]Sankaranarayanan S, Sipma H B, Manna Z. Non-linear loop invariant generation using Grobner bases [J]. ACM SIGPLAN Notices,2004,39(1):318-329.
[90]Chen Y H, Xia B C, Yang L, Zhan N J, Zhou C C. Discovering non-linear ranking functions by solving semi-algebraic systems [J]. Lecture Notes in Computer Science.2007.4711:34-49.
[91]Chen Y H, Xia B C, Yang L, et al. Discovering non-linear ranking functions by solving semi-algebraic systems [M]. Springer Berlin Heidelberg,2007,34-49.
[92]Platzer A. Differential logic for reasoning about hybrid systems[M]. Hybrid Systems: Computation and Control. Springer Berlin Heidelberg,2007,746-749.
[93]Platzer A. Differential dynamic logic for hybrid systems [J]. Journal of Automated Reasoning, 2008,41(2):143-189.
[94]Platzer A. Differential-algebraic dynamic logic for differential-algebraic programs [J]. Journal of Logic and Computation,2010,20(1):309-352.
[95]Engelfriet J. Determinancy→(observation equivalence=trace equivalence) [J]. Theoretical Computer Science.1985.36:21-25.
[96]Van Glabbeek R, Goltz U. Equivalence notions for concurrent systems and refinement of actions [J]. Lecture Notes in Computer Science.1989.379:237-248.
[97]Van Benthem J F A K. Modal correspondence theory [J].1977.
[98]Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems [J]. Theoretical computer science,1995,138(1):3-34.
[99]Pappas G J. Bisimilar linear systems [J]. Automatica,2003,39(12):2035-2047.
[100]Van der Schaft A J. Equivalence of dynamical systems by bisimulation [J]. IEEE Transactions on Automatic Control,2004,49(12):2160-2172.
[101]Girard A, Pappas G J. Approximate bisimulations for nonlinear dynamical systems[C]. The 44th IEEE Conference on Decision and Control,2005:684-689..
[102]Julius A A. Approximate abstraction of stochastic hybrid automata [M]. Hybrid Systems: Computation and Control. Springer Berlin Heidelberg,2006:318-332.
[103]Girard A, Pappas G J. Approximation metrics for discrete and continuous systems [J]. IEEE Transactions on Automatic Control,2007,52(5):782-798.
[104]Girard A, Pappas G J. Approximate bisimulations for constrained linear systems [J]. Automatica.2007,43:1307-1317.
[105]Lafferriere G, Pappas G J. Symbolic reachability computation for families of linear vector fields [J]. Journal of Symbolic Computation.2001,32(3):231-253.
[106]Tsitsiklis J N. An analysis of temporal-difference learning with function approximation [J]. IEEE Transactions on Automatic Control.1997,42(5):674-690.
[107]Triebel H. Interpolation theory, function spaces, differential operators [M]. Heidelberg: Johann Ambrosius Barth,1995.
[108]Grabmeier J, Kaltofen E, Weispfenning V. Computer algebra handbook [M]. Heidelberg. Germany. Springer Verlag Press.2003,10-30.
[109]Stetter H J. Numerical polynomial algebra [M]. The Society for Industrial and Applied Mathematics.2004,30-52.
[110]Emiris I Z, Pan V Y. Improved algorithms for computing determinants and resultants [J]. Journal of Complexity.2005,21(1):43-71.
[Ill]Bates D, Peterson C, Sommese A J. A numerical-symbolic algorithm for computing the multiplicity of a component of an algebraic set [J]. Journal of Complexity.2006,22(4): 475-489.
[112]Kaltofen E, Yang Z F, Zhi L H. Approximate greatest common divisors of several polynomials with linearly constrained coefficients and singular polynomials [C]. Proceedings of the 2006 International Symposium on Symbolic and Algebraic Computation. New York. USA.2006, 169-176.
[113]Kaltofen E, Yang Z F, Zhi L H. Structured low rank approximate of a Sylvester matrix [J]. Trends in Mathematics.2007,69-83.
[114]Hennessy M. Algebraic theory of processes [M]. US:The MIT Press.1988,16-256.
[115]张云凌.求解约束全局最优化问题的填充函数法[D].学位论文.天津：天津大学.2007.
[116]Bergstra J A, Klop J W. Process algebra for synchronous communication [J]. Information and Control.1984,60(1-3):109-137.
[117]Nicola R D, Vaandrager F. Actions versus state based logics for transition systems [J]. Lecture Notes in Computer Science.1990,469:407-419.
[118]Plotkin G. An operational semantics for CSP extended abstract [J]. Lecture Notes in Computer Science.1983,148:250-252.
[119]Keller R M. Formal verification of parallel programs [J]. Communications of the ACM.1976, 19(7):371-384.
[120]Lien Y E. Study of theoretical and practical aspects of transition systems [D]. PhD Disseration. Berkeley. University of California.1972,39-78.
[121]Plotkin G D. A structural approach to operational semantics [J]. Technical Report. Computer Science Department. Aarhus University.1981.
[122]赵锡英.随机进程代数的等价性判定计算[D].学位论文.甘肃：兰州大学.2006,48-136.
[123]Ritt J F. Differential algrbra [M]. USA. American Mathematical Society.1950,40-76.
[124]Buchberger B. Groebner Basis:A short introduction for systems theorists [J]. Lecture Notes in Computer Science.2001,2178:1-19.
[125]Stewart G W. On the early history of the singular value decomposition [J]. SIAM Rev.1993, 35:551-566.
[126]Lathauwer L D, Moor B D, Vandewalle J. A multilinear singular value decomposition [J]. SIAM Journal on Matrix Analysis and Applications.2000,21(4):1253-1278.
[127]Ye J P. A two-stage linear discriminant analysis via QR-decomposition [J]. IEEE Transaction on Pattern Analysis and Machine Intelligence.2005,27(6):929-941.
[128]Ge R P. A filled function method for finding a global minimize of a function of several variables [J]. Mathematical Programming.1990,46(1-3):191-204.
[129]Ge R P. Qin Y F. A class of filled functions of finding global minimizers of a function of several variables [J]. Journal of Optimization Theory and Applications.1987,54(2):241-252.
[130]Ge R P. Qin Y F. The globally convexized filled functions for global optimization [J]. Applied Mathematics and Computation.1990,35(2):131-158.
[131]Liu X. Finding global minima with a computable filled function [J]. Journal of Global Optimization.2001,19(2):151-161.
[132]Zhang L S, Ng C K, Li D, Tian W W. A new filled function method for global optimization [J]. Journal of Global Optimization.2004,28(1):17-43.
[133]Chen Y H, Xia B C, Yang L, Zhan N J. Generating polynomial invariants with DISCOVERER and QEPCAD [J]. Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science.2007,4700:67-82.
[2]Wolfram S. Computer Software in Science and Mathematics [J]. Scientific American,1984, 251(3):188-92,194,196-200,203.
[3]Adrion W R, Branstad M A, Cherniavsky J C. Validation, verification, and testing of computer software [J]. ACM Computing Surveys,1982,14(2):159-192.
[4]Jurs P C. Computer software applications in chemistry [M]. John Wiley & Sons,1986.
[5]Lenat D B. Computer Software for Intelligent Systems [J]. Scientific American,1984,251(3): 204-09,211-13.
[6]Wallace D R, Fujii R U. Software verification and validation:an overview [J]. IEEE Software, 1989,6(3):10-17.
[7]Jennings N R. An agent-based approach for building complex software systems [J]. Communications of the ACM,2001,44(4):35-41.
[8]Fenton N E, Ohlsson N. Quantitative analysis of faults and failures in a complex software system [J]. IEEE Transactions on Software Engineering,2000,26(8):797-814.
[9]Leveson N G, Harvey P R. Analyzing software safety [J]. IEEE Transactions on Software Engineering,1983, (5):569-579.
[10]Henzinger T A, Jhala R, Majumdar R, Sutre G. Software verification with BLAST [M]. Model Checking Software. Springer Berlin Heidelberg,2003:235-239.
[11]Leveson NG. Software safety:why, what, and how [J]. ACM Computing Surveys,1986,18(2): 125-163.
[12]Wadleigh K R, Crawford I L. Software Optimization for High-Performance Computers [M]. Prentice Hall Professional,2000.
[13]Ammar R A, Booth T L. Software optimization using user models [J]. IEEE Transactions on Systems, Man and Cybernetics,1988,18(4):552-560.
[14]Peymandoust A, Simunic T, De Micheli G Low power embedded software optimization using symbolic algebra [C]. Design, Automation and Test in Europe Conference and Exhibition, 2002,1052-1058.
[15]Dolan E D, More J J. Benchmarking optimization software with performance profiles [J]. Mathematical programming,2002,91(2):201-213.
[16]Voβ S, Woodruff D L. Optimization software class libraries [M]. Springer US,2003.
[17]Carson Y, Maria A. Simulation optimization:methods and applications [C]. Proceedings of the 29th conference on Winter Simulation.1997,118-126.
[18]Poles S, Vassileva M, Sasaki D. Multiobjective optimization software [M]. Multiobjective Optimization. Springer Berlin Heidelberg,2008,329-348.
[19]Pitchumani V, Stabler E P.A formal method for computer design verification [C]. The 19th Conference on Design Automation,1982,809-814.
[20]Heitmeyer C. On the need for practical formal methods [C]. Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer Berlin Heidelberg,1998,18-26.
[21]Fidge C, Kearney P, Utting M. A formal method for building concurrent real-time software [J]. IEEE Software,1997,14(2):99-106.
[22]Mullin L M R, Thibault S A, Dooling D R, et al. Formal method for scheduling, routing and communication protocol [C]. Proceedings of the 2nd International Symposium on High Performance Distributed Computing,1993,234-242.
[23]Wing J M. A specifier's introduction to formal methods [J]. Computer,1990,23(9):8-22.
[24]Yu H, He X, Deng Y, et al. A formal method for analyzing software architecture models in SAM [C]. The Conference of Computer Software and Applications,2002,645-652.
[25]Shoenfield J R. Mathematical logic [M]. Reading:Addison-Wesley,1967.
[26]Pnueli A. The temporal logic of programs[C]. The 18th Annual Symposium on Foundations of Computer Science,1977,46-57.
[27]Girard J Y. Linear logic [J]. Theoretical computer science,1987,50(1):1-101.
[28]Nerode A. Linear automaton transformations [J]. Proceedings of the American Mathematical Society,1958,9(4):541-544.
[29]Toffoli T. CAM:A high-performance cellular-automaton machine [J]. Physica D:Nonlinear Phenomena,1984,10(1):195-204.
[30]Maraninchi F, Remond Y. Argos:an automaton-based synchronous language [J]. Computer languages,2001,27(1):61-92.
[31]Gunnels J A, Gustavson F G, Henry G M, et al. FLAME:Formal linear algebra methods environment [J]. ACM Transactions on Mathematical Software,2001,27(4):422-455.
[32]Hoare C A R. An overview of some formal methods for program design [J]. Computer,1987, 20(9):85-91.
[33]Hermanns H, Herzog U, Katoen J P. Process algebra for performance evaluation [J]. Theoretical computer science,2002,274(1):43-87.
[34]Christofides N. Graph theory:An algorithmic approach [M]. Academic Press,1975.
[35]Bondy J A, Murty U S R. Graph theory with applications [M]. London:Macmillan,1976.
[36]ERDOS P. Graph theory and probability [J]. Canadian Journal of Mathematics,1959,11(1): 34.
[37]Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications [J]. ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.
[38]Van Glabbeek R, Goltz U. Equivalence notions for concurrent systems and refinement of actions[C]. Mathematical Foundations of Computer Science 1989. Springer Berlin Heidelberg, 1989,237-248..
[39]Winskel G, Nielsen M. Models for concurrency [J]. DAIMI Report Series,1993,22(463).
[40]Henzinger T A. The theory of hybrid automata [M]. Springer Berlin Heidelberg,2000.
[41]Milner R, Sangiorgi D. Barbed bisimulation [M]. Automata, Languages and Programming. Springer Berlin Heidelberg,1992,685-695.
[42]Weyuker E J. Evaluating software complexity measures [J]. IEEE Transactions on Software Engineering,1988,14(9):1357-1365.
[43]Mens T, Tourwe T. A survey of software refactoring [J]. IEEE Transactions on Software Engineering,2004,30(2):126-139.
[44]Horwitz S, Reps T. The use of program dependence graphs in software engineering [C]. Proceedings of the 14th international conference on Software engineering,1992,392-411.
[45]Rosenberg A L. Nondeterminism in Computability Theory [M]. The Pillars of Computation Theory. Springer New York,2010,233-244.
[46]Barbosa L S, Oliveira J N. Transposing partial components-an exercise on coalgebraic refinement [J]. Theoretical Computer Science,2006,365(1):2-22.
[47]Van Glabbeek R J. The linear time-branching time spectrum [M]. Springer Berlin Heidelberg, 1990.
[48]Larsen K G, Skou A. Bisimulation through probabilistic testing [J]. Information and computation,1991,94(1):1-28..
[49]Van Glabbeek R J, Weijland W P. Branching time and abstraction in bisimulation semantics [J]. Journal of the ACM,1996,43(3):555-600.
[50]Desharnais J, Edalat A, Panangaden P. Bisimulation for labelled Markov processes [J]. Information and Computation,2002,179(2):163-193.
[51]Bloom B, Istrail S, Meyer A R. Bisimulation can't be traced [J]. Journal of the ACM,1995, 42(1):232-268.
[52]De Nicola R, Vaandrager F. Three logics for branching bisimulation [J]. Journal of the ACM, 1995,42(2):458-487.
[53]Groote J F, Vaandrager F. Structured operational semantics and bisimulation as a congruence [J]. Information and computation,1992,100(2):202-260.
[54]Smith J, De Micheli G. Polynomial methods for allocating complex components [C]. Proceedings of the conference on Design, automation and test in Europe,1999.
[55]Smith J, De Micheli G. Polynomial circuit models for component matching in high-level synthesis [J]. IEEE Transactions on Very Large Scale Integration Systems,2001,9(6):783-800.
[56]Peymandoust A, De Micheli G. Using symbolic algebra in algorithmic level DSP synthesis [C]. The Conference of Design Automation,2001,277-282.
[57]Zhi Y, Guangsheng M, Shu21 Z. Equivalence Verification of High-Level Datapaths Based on Polynomial Symbolic Algebra [J]. Journal of Computer Research and Development,2009,3: 023.
[58]Buchberger B. A view on the future of symbolic computation [C]. Proceedings of the 2005 international symposium on Symbolic and algebraic computation. ACM,2005,1-1.
[59]Chaochen Z. Program verification through computer algebra [M]. Formal Methods and Software Engineering. Springer Berlin Heidelberg,2006,1-1.
[60]王东明,法学.消去法及其应用[M].科学出版社,2002.
[61]吴文俊.数学机械化[M].科学出版社,2003.
[62]Halstead Jr R H. Multilisp:A language for concurrent symbolic computation [J]. ACM Transactions on Programming Languages and Systems,1985,7(4):501-538.
[63]Lafferriere G, Pappas G J, Yovine S. Symbolic reachability computation for families of linear vector fields [J]. Journal of Symbolic Computation,2001,32(3):231-253.
[64]Touretzky D S. LISP:a gentle introduction to symbolic computation [M]. John Wiley & Sons, Inc.,1984.
[65]王东明.符号计算选讲[M].北京：清华大学出版社.2003.
[66]张军.数值计算[M].北京：清华大学出版社.2008.
[67]Beyn W J. The numerical computation of connecting orbits in dynamical systems [J]. IMA Journal of Numerical Analysis,1990,10(3):379-405.
[68]Higham N J. Numerical Computation:Methods, Software, and Analysis [J]. IEEE Computational Science & Engineering,1998,5(1):79.
[69]Pozrikidis C. Numerical computation in science and engineering [M]. New York:Oxford university press,1998.
[70]支丽红.符号与数值混合计算[J].系统科学与数学.2008.28(8)：1040-1052.
[71]唐焕文.实用最优化方法[M].大连：大连理工大学出版社.2007.33-45.
[72]Stanley P C, Pilkington T C. The combination method:A numerical technique for electrocardiographic calculations [J]. IEEE Transactions on Biomedical Engineering,1989, 36(4):456-461.
[73]Jerard R B, Hussaini S Z, Drysdale R L, et al. Approximate methods for simulation and verification of numerically controlled machining programs [J]. The Visual Computer,1989, 5(6):329-348.
[74]盛骤,谢式千,潘承毅.概率论与数理统计[M].北京：高等教育出版社.2001.25-67.
[75]Yap C K. Towards exact geometric computation [J]. Computational Geometry,1997,7(1): 3-23.
[76]Nolan J P. Numerical calculation of stable densities and distribution functions [J]. Communications in statistics. Stochastic models,1997,13(4):759-774.
[77]Hoare C A R. Communicating sequential processes [J]. Communications of the ACM,1978, 21(8):666-677.
[78]Milner R. A calculus of communicating systems [M]. Springer-Verlag New York,1982.
[79]Bergstra J A, Klop J W. Algebra of communicating processes with abstraction [J]. Theoretical computer science,1985,37:77-121.
[80]Bolognesi T, Brinksma E. Introduction to the ISO specification language LOTOS [J]. Computer Networks and ISDN systems,1987,14(1):25-59.
[81]Pnueli A. The temporal logic of programs [C]. The 18th Annual Symposium on Foundations of Computer Science,1977:46-57.
[82]Clarke E M, Emerson E A, Sistla A P. Automatic verification of finite-state concurrent systems using temporal logic specifications [J]. ACM Transactions on Programming Languages and Systems (TOPLAS),1986,8(2):244-263.
[83]Emerson E A, Halpern J Y. "Sometimes" and "not never" revisited:on branching versus linear time temporal logic [J]. Journal of the ACM,1986,33(1):151-178.
[84]Petri C A. Nets, time and space [J]. Theoretical computer science,1996,153(1):3-48.
[85]Browne M C, Clarke E M, Grumberg O. Characterizing finite Kripke structures in propositional temporal logic [J]. Theoretical Computer Science,1988,59(1):115-131.
[86]Biere A, Cimatti A, Clarke E, et al. Symbolic model checking without BDDs [M]. Springer Berlin Heidelberg,1999.
[87]Pustejovsky J. The syntax of event structure [J]. Cognition.1991.41(3-1):47-81.
[88]Manna Z, Pnueli A. Temporal verification of reactive systems:safety [M]. USA. Springer. 1995:10-27.
[89]Sankaranarayanan S, Sipma H B, Manna Z. Non-linear loop invariant generation using Grobner bases [J]. ACM SIGPLAN Notices,2004,39(1):318-329.
[90]Chen Y H, Xia B C, Yang L, Zhan N J, Zhou C C. Discovering non-linear ranking functions by solving semi-algebraic systems [J]. Lecture Notes in Computer Science.2007.4711:34-49.
[91]Chen Y H, Xia B C, Yang L, et al. Discovering non-linear ranking functions by solving semi-algebraic systems [M]. Springer Berlin Heidelberg,2007,34-49.
[92]Platzer A. Differential logic for reasoning about hybrid systems[M]. Hybrid Systems: Computation and Control. Springer Berlin Heidelberg,2007,746-749.
[93]Platzer A. Differential dynamic logic for hybrid systems [J]. Journal of Automated Reasoning, 2008,41(2):143-189.
[94]Platzer A. Differential-algebraic dynamic logic for differential-algebraic programs [J]. Journal of Logic and Computation,2010,20(1):309-352.
[95]Engelfriet J. Determinancy→(observation equivalence=trace equivalence) [J]. Theoretical Computer Science.1985.36:21-25.
[96]Van Glabbeek R, Goltz U. Equivalence notions for concurrent systems and refinement of actions [J]. Lecture Notes in Computer Science.1989.379:237-248.
[97]Van Benthem J F A K. Modal correspondence theory [J].1977.
[98]Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems [J]. Theoretical computer science,1995,138(1):3-34.
[99]Pappas G J. Bisimilar linear systems [J]. Automatica,2003,39(12):2035-2047.
[100]Van der Schaft A J. Equivalence of dynamical systems by bisimulation [J]. IEEE Transactions on Automatic Control,2004,49(12):2160-2172.
[101]Girard A, Pappas G J. Approximate bisimulations for nonlinear dynamical systems[C]. The 44th IEEE Conference on Decision and Control,2005:684-689..
[102]Julius A A. Approximate abstraction of stochastic hybrid automata [M]. Hybrid Systems: Computation and Control. Springer Berlin Heidelberg,2006:318-332.
[103]Girard A, Pappas G J. Approximation metrics for discrete and continuous systems [J]. IEEE Transactions on Automatic Control,2007,52(5):782-798.
[104]Girard A, Pappas G J. Approximate bisimulations for constrained linear systems [J]. Automatica.2007,43:1307-1317.
[105]Lafferriere G, Pappas G J. Symbolic reachability computation for families of linear vector fields [J]. Journal of Symbolic Computation.2001,32(3):231-253.
[106]Tsitsiklis J N. An analysis of temporal-difference learning with function approximation [J]. IEEE Transactions on Automatic Control.1997,42(5):674-690.
[107]Triebel H. Interpolation theory, function spaces, differential operators [M]. Heidelberg: Johann Ambrosius Barth,1995.
[108]Grabmeier J, Kaltofen E, Weispfenning V. Computer algebra handbook [M]. Heidelberg. Germany. Springer Verlag Press.2003,10-30.
[109]Stetter H J. Numerical polynomial algebra [M]. The Society for Industrial and Applied Mathematics.2004,30-52.
[110]Emiris I Z, Pan V Y. Improved algorithms for computing determinants and resultants [J]. Journal of Complexity.2005,21(1):43-71.
[Ill]Bates D, Peterson C, Sommese A J. A numerical-symbolic algorithm for computing the multiplicity of a component of an algebraic set [J]. Journal of Complexity.2006,22(4): 475-489.
[112]Kaltofen E, Yang Z F, Zhi L H. Approximate greatest common divisors of several polynomials with linearly constrained coefficients and singular polynomials [C]. Proceedings of the 2006 International Symposium on Symbolic and Algebraic Computation. New York. USA.2006, 169-176.
[113]Kaltofen E, Yang Z F, Zhi L H. Structured low rank approximate of a Sylvester matrix [J]. Trends in Mathematics.2007,69-83.
[114]Hennessy M. Algebraic theory of processes [M]. US:The MIT Press.1988,16-256.
[115]张云凌.求解约束全局最优化问题的填充函数法[D].学位论文.天津：天津大学.2007.
[116]Bergstra J A, Klop J W. Process algebra for synchronous communication [J]. Information and Control.1984,60(1-3):109-137.
[117]Nicola R D, Vaandrager F. Actions versus state based logics for transition systems [J]. Lecture Notes in Computer Science.1990,469:407-419.
[118]Plotkin G. An operational semantics for CSP extended abstract [J]. Lecture Notes in Computer Science.1983,148:250-252.
[119]Keller R M. Formal verification of parallel programs [J]. Communications of the ACM.1976, 19(7):371-384.
[120]Lien Y E. Study of theoretical and practical aspects of transition systems [D]. PhD Disseration. Berkeley. University of California.1972,39-78.
[121]Plotkin G D. A structural approach to operational semantics [J]. Technical Report. Computer Science Department. Aarhus University.1981.
[122]赵锡英.随机进程代数的等价性判定计算[D].学位论文.甘肃：兰州大学.2006,48-136.
[123]Ritt J F. Differential algrbra [M]. USA. American Mathematical Society.1950,40-76.
[124]Buchberger B. Groebner Basis:A short introduction for systems theorists [J]. Lecture Notes in Computer Science.2001,2178:1-19.
[125]Stewart G W. On the early history of the singular value decomposition [J]. SIAM Rev.1993, 35:551-566.
[126]Lathauwer L D, Moor B D, Vandewalle J. A multilinear singular value decomposition [J]. SIAM Journal on Matrix Analysis and Applications.2000,21(4):1253-1278.
[127]Ye J P. A two-stage linear discriminant analysis via QR-decomposition [J]. IEEE Transaction on Pattern Analysis and Machine Intelligence.2005,27(6):929-941.
[128]Ge R P. A filled function method for finding a global minimize of a function of several variables [J]. Mathematical Programming.1990,46(1-3):191-204.
[129]Ge R P. Qin Y F. A class of filled functions of finding global minimizers of a function of several variables [J]. Journal of Optimization Theory and Applications.1987,54(2):241-252.
[130]Ge R P. Qin Y F. The globally convexized filled functions for global optimization [J]. Applied Mathematics and Computation.1990,35(2):131-158.
[131]Liu X. Finding global minima with a computable filled function [J]. Journal of Global Optimization.2001,19(2):151-161.
[132]Zhang L S, Ng C K, Li D, Tian W W. A new filled function method for global optimization [J]. Journal of Global Optimization.2004,28(1):17-43.
[133]Chen Y H, Xia B C, Yang L, Zhan N J. Generating polynomial invariants with DISCOVERER and QEPCAD [J]. Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science.2007,4700:67-82.