Generating Semi-Algebraic Invariants for Non-Autonomous Polynomial Hybrid Systems  

作　　者：WANG Qiuye LI Yangjia XIA Bican ZHAN Naijun 

机构地区：[1]State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China [2]LMAM&School of Mathematical Sciences,Peking Univcrsity,Beijing 100871,China

出　　处：《Journal of Systems Science & Complexity》2017年第1期234-252,共19页系统科学与复杂性学报（英文版）

基　　金：supported partly by“973 Program”under Grant No.2014CB340701;by the National Natural Science Foundation of China under Grant Nos.61625205,91418204 and 61625206;by CDZ Project CAP(GZ 1023);by the CAS/SAFEA International Partnership Program for Creative Research Teams;supported 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.

关 键 词：Hybrid systems INVARIANTS NON-A utonomous systems polynomial ideals semi-algebraic sets. 

分 类 号：O174.14[理学—数学]