System Simultaneous Stabilization And Safety Verification Via Symbolic Computation

The simultaneous stabilization and safety-verification are fundamental problems of systems science and control theory, it have great theoretical and practical importance. Simultaneous Stabilization problem consider how to design a single controller that can stabilize several plants, that means the closed loop transform functions are stable. There are only some preliminary theoretical results for linear systems in academic community. Especially, even for the case of three plants, there are lots of theoretical problems to be investigated. At the same time, Safety-Verification problems consider whether systems satisfy constraint conditions to meet the practical requirement or avoid some unexpected involution process; sometimes those problems can be transformed to the problems in algebra inequality verification.In this thesis, we consider the linear systems simultaneous stabilization problems and safety verification problem of nonlinear system, the mainly results are list as follows:· We consider the parameter to be determined in the famous "Belgian chocolate prob-lem" in Simultaneous Stabilization for the linear systems. we discuss the transfor-mation in parameter to be determined in Belgian chocolate problem in continuous case and discrete system case, and its intrinsic connection with the famous "Gold-berg constant". By using the method of symbolic computation and the concept of Elliptic Modular Function, more sharper estimate for the length of the hyperbolic homotopy class of closed geodesics on the remain region after the complex plane delete two points, and use this result for the parameter estimate in Belgian chocolate problem, it improved the Hempel and Smith’s result in 1988.· For the determine of numerical lower bound of the Belgian chocolate problem, we discuss the relationship in polynomials roots distribution and the systems parameter in some special case. we figure out that the "new parameter bound(0.976462)"(so called "a new world record") in Belgian chocolate problem Boston claimed in 2012 he obtained is not reliable. The controller he found can not guarantee the closed loop feedback polynomials is stable. We also proposed controller design algorithm by parameter disturbance and verify the Hurwitz stable conditions to compute the solution, the numerical experiments shows that in the lower degree case, the nu-merical lower bound determined by our algorithm dramatically improve the known corresponding degree polynomials.· We research system-verification problem of nonlinear system. Based on symbolic computation tools and differential dynamic system qualitative theory, implement the idea of piece discrimination function and use the of power series solution cut-off skill, this problem can be transformed into a series of algebra inequality verification problem; we verify the safety problem for the benchmark example -Van der Pol system, our method can determine the verification problem efficiently. we can set the provision prior to catch the critical point between the "safety" and the "un-safety". The condition obtained by our method can be deemed as sharp.· We consider the problem of transformation of region, we construct the conformal mapping from the initial region to the outer of the unsafe region, by change the vari-ables from the complex coordinate to the real two dimensional planar coordinate; by doing a transformation to the nonlinear system, the safety verification of the original system transform to new coordinate system. furthermore, we discuss the relationship between the original system and transformed system, some properties such as separability and the transformation of the barrier function.· By using the tools of symbolic computation, for the famous Mordell inequality conjecture, we eliminate the constraint by normalized condition, the problem can be transformed into the unconstraint problem. For the case of n= 3, we verified this inequality by cylindrical algebraic decomposition; meanwhile, for the case of n= 4, we verify the inequality is also valid by using the successive difference substitution method.