In this paper,the notion of rational univariate representations with variables is introduced.Consequently,the ideals,created by given rational univariate representations with variables,are defined.One merit of these c...In this paper,the notion of rational univariate representations with variables is introduced.Consequently,the ideals,created by given rational univariate representations with variables,are defined.One merit of these created ideals is that some of their algebraic properties can be easily decided.With the aid of the theory of valuations,some related results are established.Based on these results,a new approach is presented for decomposing the radical of a polynomial ideal into an intersection of prime ideals.展开更多
Hybrid systems are dynamical systems with interacting discrete computation and continuous physical processes, which have become more common, more indispensable, and more complicated in our modern life. Particularly, m...Hybrid systems are dynamical systems with interacting discrete computation and continuous physical processes, which have become more common, more indispensable, and more complicated in our modern life. Particularly, many of them are safety-critical, and therefore are required to meet a critical safety standard. Invariant generation plays a central role in the verification and synthesis of hybrid systems. In the previous work, the fourth author and his coauthors gave a necessary and sufficient condition for a semi-algebraic set being an invariant of a polynomial autonomous dynamical system, which gave a confirmative answer to the open problem. In addition, based on which a complete algorithm for generating all semi-algebraic invariants of a given polynomial autonomous hybrid system with the given shape was proposed. This paper considers how to extend their work to non-autonomous dynamical and hybrid systems. Non-autonomous dynamical and hybrid systems are with inputs, which are very common in practice; in contrast, autonomous ones are without inputs. Furthermore, the authors present a sound and complete algorithm to verify semi-algebraic invariants for non-autonomous polynomial hybrid systems. Based on which, the authors propose a sound and complete algorithm to generate all invariants with a pre-defined template.展开更多
This paper investigates the termination problems of multi-path polynomial programs (MPPs) with equational loop guards. To establish sufficient conditions for termination and nontermination simultaneously, the author...This paper investigates the termination problems of multi-path polynomial programs (MPPs) with equational loop guards. To establish sufficient conditions for termination and nontermination simultaneously, the authors propose the notion of strong/weak non-termination which under/over- approximates non-termination. Based on polynomial ideal theory, the authors show that the set of all strong non-terminating inputs (SNTI) and weak non-terminating inputs (WNTI) both correspond to tile real varieties of certain polynomial ideals. Furthermore, the authors prove that the variety of SNTI is computable, and under some sufficient conditions the variety of WNTI is also computable. Then by checking the computed SNTI and WNTI varieties in parallel, termination properties of a consid- ered MPP can be asserted. As a consequence, the authors establish a new framework for termination analysis of MPPs.展开更多
We define the second discriminant D_(2)of a univariate polynomial f of degree greater than 2 as the product of the linear forms 2r_(k)-r_(i)-r_(j)for all triples of roots r_(i),r_(k),r_(j)of f with i<j and j≠k,k≠...We define the second discriminant D_(2)of a univariate polynomial f of degree greater than 2 as the product of the linear forms 2r_(k)-r_(i)-r_(j)for all triples of roots r_(i),r_(k),r_(j)of f with i<j and j≠k,k≠i.D_(2)vanishes if and only if f has at least one root which is equal to the average of two other roots.We show that D_(2)can be expressed as the resultant of f and a determinant formed with the derivatives of f,establishing a new relation between the roots and the coefficients of f.We prove several notable properties and present an application of D_(2).展开更多
Pan and Wang presented a method for computing uniform GrSbner bases for certain ide- als generated by polynomials with parametric exponents in 2006, and two criteria were proposed to determine if a uniform GrSbner bas...Pan and Wang presented a method for computing uniform GrSbner bases for certain ide- als generated by polynomials with parametric exponents in 2006, and two criteria were proposed to determine if a uniform GrSbner basis can be obtained. This paper gives a new algorithmic approach for computing tile uniform GrSbner basis such that Pan and Wang's method could be concluded as a special case. The authors use the method of reduced term order under ring homomorphisnl to get the reduced uniform GrSbner basis. Also the authors point and correct a mistake in Pan and Wang's method. The result is a generalization of approach of Pan and Wang and one could compute the uniform GrSbner basis more efficiently by the new approach.展开更多
A linear system arising from a polynomial problem in the approximation theory is studied, and the necessary and sufficient conditions for existence and uniqueness of its solutions are presented. Together with a class ...A linear system arising from a polynomial problem in the approximation theory is studied, and the necessary and sufficient conditions for existence and uniqueness of its solutions are presented. Together with a class of determinant identities, the resulting theory is used to determine the unique solution to the polynomial problem. Some homogeneous polynomial identities as well as results on the structure of related polynomial ideals are just by-products.展开更多
In this paper,the so-called invertibility is introduced for rational univariate representations,and a characterization of the invertibility is given.It is shown that the rational univariate representations,obtained by...In this paper,the so-called invertibility is introduced for rational univariate representations,and a characterization of the invertibility is given.It is shown that the rational univariate representations,obtained by both Rouillier’s approach and Wu’s method,are invertible.Moreover,the ideal created by a given rational univariate representation is defined.Some results on invertible rational univariate representations and created ideals are established.Based on these results,a new approach is presented for decomposing the radical of a zero-dimensional polynomial ideal into an intersection of maximal ideals.展开更多
基金supported by the National Natural Science Foundation of China under Grant No.12161057。
文摘In this paper,the notion of rational univariate representations with variables is introduced.Consequently,the ideals,created by given rational univariate representations with variables,are defined.One merit of these created ideals is that some of their algebraic properties can be easily decided.With the aid of the theory of valuations,some related results are established.Based on these results,a new approach is presented for decomposing the radical of a polynomial ideal into an intersection of prime ideals.
基金supported partly by“973 Program”under Grant No.2014CB340701by the National Natural Science Foundation of China under Grant Nos.61625205,91418204 and 61625206+2 种基金by CDZ Project CAP(GZ 1023)by the CAS/SAFEA International Partnership Program for Creative Research Teamssupported partly by the National Natural Science Foundation of China under Grant Nos.11290141,11271034 and 61532019
文摘Hybrid systems are dynamical systems with interacting discrete computation and continuous physical processes, which have become more common, more indispensable, and more complicated in our modern life. Particularly, many of them are safety-critical, and therefore are required to meet a critical safety standard. Invariant generation plays a central role in the verification and synthesis of hybrid systems. In the previous work, the fourth author and his coauthors gave a necessary and sufficient condition for a semi-algebraic set being an invariant of a polynomial autonomous dynamical system, which gave a confirmative answer to the open problem. In addition, based on which a complete algorithm for generating all semi-algebraic invariants of a given polynomial autonomous hybrid system with the given shape was proposed. This paper considers how to extend their work to non-autonomous dynamical and hybrid systems. Non-autonomous dynamical and hybrid systems are with inputs, which are very common in practice; in contrast, autonomous ones are without inputs. Furthermore, the authors present a sound and complete algorithm to verify semi-algebraic invariants for non-autonomous polynomial hybrid systems. Based on which, the authors propose a sound and complete algorithm to generate all invariants with a pre-defined template.
基金supported by the National Basic Research Program of China under Grant No.2014CB340700the National Science and Technology Major Project of China under Grant No.2012ZX01039-004+3 种基金the National Natural Science Foundation of China under Grant Nos.91118007,11071273,61202131,11401218,cstc2012ggB40004,cstc2013jjys40001SRFDP under Grant No.20130076120010the Open Project of Shanghai Key Laboratory of Trustworthy Computing under Grant No.07dz22304201307West Light Foundation of Chinese Academy of Sciences
文摘This paper investigates the termination problems of multi-path polynomial programs (MPPs) with equational loop guards. To establish sufficient conditions for termination and nontermination simultaneously, the authors propose the notion of strong/weak non-termination which under/over- approximates non-termination. Based on polynomial ideal theory, the authors show that the set of all strong non-terminating inputs (SNTI) and weak non-terminating inputs (WNTI) both correspond to tile real varieties of certain polynomial ideals. Furthermore, the authors prove that the variety of SNTI is computable, and under some sufficient conditions the variety of WNTI is also computable. Then by checking the computed SNTI and WNTI varieties in parallel, termination properties of a consid- ered MPP can be asserted. As a consequence, the authors establish a new framework for termination analysis of MPPs.
基金supported by National Natural Science Foundation of China(Grant Nos.61702025 and 11801101)the Special Fund for Guangxi Bagui Scholar Project+1 种基金Guangxi Science and Technology Program(Grant No.2017AD23056)the Startup Foundation for Advanced Talents in Guangxi University for Nationalities(Grant No.2015MDQD018)。
文摘We define the second discriminant D_(2)of a univariate polynomial f of degree greater than 2 as the product of the linear forms 2r_(k)-r_(i)-r_(j)for all triples of roots r_(i),r_(k),r_(j)of f with i<j and j≠k,k≠i.D_(2)vanishes if and only if f has at least one root which is equal to the average of two other roots.We show that D_(2)can be expressed as the resultant of f and a determinant formed with the derivatives of f,establishing a new relation between the roots and the coefficients of f.We prove several notable properties and present an application of D_(2).
基金supported by the National Natural Science Foundation of China under Grant No.11271040Science and Technology Foundation of Gui Zhou Province LKM[2013]16
文摘Pan and Wang presented a method for computing uniform GrSbner bases for certain ide- als generated by polynomials with parametric exponents in 2006, and two criteria were proposed to determine if a uniform GrSbner basis can be obtained. This paper gives a new algorithmic approach for computing tile uniform GrSbner basis such that Pan and Wang's method could be concluded as a special case. The authors use the method of reduced term order under ring homomorphisnl to get the reduced uniform GrSbner basis. Also the authors point and correct a mistake in Pan and Wang's method. The result is a generalization of approach of Pan and Wang and one could compute the uniform GrSbner basis more efficiently by the new approach.
文摘A linear system arising from a polynomial problem in the approximation theory is studied, and the necessary and sufficient conditions for existence and uniqueness of its solutions are presented. Together with a class of determinant identities, the resulting theory is used to determine the unique solution to the polynomial problem. Some homogeneous polynomial identities as well as results on the structure of related polynomial ideals are just by-products.
基金the National Natural Science Foundation of China under Grant No.12161057。
文摘In this paper,the so-called invertibility is introduced for rational univariate representations,and a characterization of the invertibility is given.It is shown that the rational univariate representations,obtained by both Rouillier’s approach and Wu’s method,are invertible.Moreover,the ideal created by a given rational univariate representation is defined.Some results on invertible rational univariate representations and created ideals are established.Based on these results,a new approach is presented for decomposing the radical of a zero-dimensional polynomial ideal into an intersection of maximal ideals.