佘志坤

姓     名

佘志坤(博导)

职     称    

教授

所属系别    

信息与计算科学系

学科专业    

混成系统自动验证、微分方程和动力系统、符号-数值计算

办公地点    

图书馆西配楼518房间  

办公电话    

电子邮件    

zhikun.she@buaa.edu.cn

教育背景

19959月到1999年7月,就读于北京大学数学科学学院,获理学学士学位;

19999月到20056月,就读于北京大学数学科学学院,获理学博士学位。

工作简历

20041月到200612月,工作于德国马普计算机科学研究所;

2006年12月迄今,工作于北京航空航天大学数学与系统科学学院(于2009年被破格聘为博士生导师)。

科研项目


1)主持国家自然基金项目“混成系统稳定性分析的代数化与机械化及应用”(2014.01-2017.12,50万);
2)主持国家自然基金项目“基于代数分析与符号计算的混成系统自动验证”(
2011.01-2013.1220万);
3)主持国家军口
863项目“XXXXXXXXXXXXXX可靠性研究2010.07-2011.0630万);
4)主持国家军口
863项目“XXXXXXXXXXXXXXXX关键技术研究”(2008.07-2010.0670)
5)主持
2008年度北京市科技新星计划项目“混杂系统自动验证及其在软件可靠性中的应用”(2009.01-2011.1225)
6)主持
2007年度北京市优秀人才资助项目“混杂系统自动验证和分析”(2007.01-2008.12,2.5万);

发表论文

   

在ACM Transactions on Embedded Computing Systems、SIAM Journal on Control and Optimization、IEEE Transactions on Automatic Control、IEEE Transactions on Circuits and Systems、Journal of Symbolic Computation、Celestial Mechanics and Dynamical Astronomy等领域国际顶级刊物和AAAI、CAV、ISSAC、HSCC、CDC等领域国际顶级会议上发表学术论文60余篇。研究成果被来自于Massachusetts Institute of Technology、Stanford University、University of California at Berkeley、University of Cambridge、University of Oxford、ETH Zurich、Carnegie Mellon University、RWTH Aachen、日本早稻田大学、新加坡国立大学、清华大学、CNRS、INRIA、MPII、中国科学院软件所等国内外著名机构的学者他引400余次,单篇最高他引100余次。其中,2007年图灵奖获得者Edmund M. Clarke(2008年自动推理杰出贡献奖Herbrand奖获得者、美国工程院院士Alberto L. Sangiovanni-Vincentelli、美国工程院院士、美国科学院院士、欧洲科学院院士Moshe Y. Vardi哥德尔奖获得者)、英国皇家学会院士Prof. Lawrence PaulsonIsabelle创始人、2017年自动推理杰出贡献奖Herbrand奖获得者)、清华大学孙家广院士、斯坦福大学资深教授、ACM会士Prof. Zohre Manna2016年自动推理杰出贡献奖Herbrand奖获得者)、国际自动控制联合会主席Prof. Janan Zaytoon德国科学与工程院院士Werner Damm、欧洲科学院院士、IEEE会士Bernd Becker、欧洲科学院院士、ACM会士Marta Kwiatkowska、欧洲科学院院士Joost-Pieter Katoen、欧洲科学院院士Holger HermannsIEEE会士Prof. John A. StankovicIEEE会士Prof. Bruce KroghIEEE会士Prof. Bud MishraIEEE会士Prof. Insup LeeIEEE会士Prof. John LygerosIEEE会士Prof.George PappasIEEE会士Prof. Boudewijn R. HaverkortIEEE会士Prof. Calin BeltIEEE会士Prof. Weixing Zheng等给予了诸如“改进了传统方法”、“显著的”、“最早工具”、“明显优势”、“对于推动复杂系统验证是有价值的”、“灵感之源”、“更经得起检验”等等的正面评价。特别地,由图灵奖获得者Edmund M. Clarke等编著并于2018年出版的《Handbook of Model Checking》在第30章“Verification of Hybrid Systems”的第七节“Verification Tools”介绍了HSolver(共介绍了六个),指出“Even though HSolver is based on fast machine-precision floating point arithmetic, it uses sound rounding, and hence the correctness of its results cannot be hampered by round-off errors. HSolver not only verifies (unbounded horizon) reachability properties of hybrid systems, but—in addition—it also computes abstractions of the input system.”

   

1)   Bai Xue, Zhikun She and Arvind Easwaran. Under-Approximating Backward Reachable Sets by Polytopes.In Proceedings of the 28nd International Conference on Computer Aided Verification, Part I, Lecture Notes in Computer Science, Vol. 9779, pp. 457-476, Springer, 2016.CAV为计算机科学“Programming Languages and Software Engineering”领域的国际顶级会议,NUS评价为Rank 1AUS评价为A+。)

2)   Meilun Li, Zhikun She, Andrea Turrini and Lijun Zhang. Preference Planning for Markov Decision Processes. In Proceedings of the 29th AAAI Conference on Artificial Intelligence,3313-3319, 2015.AAAI为计算机科学“Artificial Intelligence”领域的国际顶级会议,NUS评价为Rank 1AUS评价为A+。欧洲科学院院士、牛津大学Prof. Marta Kwiatkowska引用了该文。)

3)  Zhikun She and Bai Xue. Algebraic Analysis on Asymptotic Stability of Switched Hybrid Systems. In Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, pp. 187-196, 2012.HSCC为“混成系统”领域的国际领先会议)28regular papers中唯一一篇来自亚洲的论文,且其中有一篇论文的署名作者是图灵奖得主Edmund M. Clarke、一篇论文的署名作者是欧洲科学院院士Prof. Marta Kwiatkowska,还有至少6篇论文的署名作者是ACM Fellow/IEEE Fellow,例如IEEE Transactions on Automatic Control主编Prof. Panos J. AntsaklisIEEE Transactions on Control Systems Technology创刊主编Prof. Bruce H. Krogh等。)

4)   Zhikun She, Bai Xue and Zhiming Zheng. Algebraic Analysis on Asymptotic Stability of Continuous Dynamical Systems. In Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation, pp. 313-320, 2011.ISSAC为计算机科学“Algorithms and Theory”领域的国际顶级会议,NUS评价为Rank 1AUS评价为A+(德国卡塞尔大学Prof. Werner M. Seiler在《美国数学评论》上针对该文发表了评论,指出“they avoid the computationally demanding use of generic quantifier elimination techniques”。)

5)   Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns and Ernst M. Hahn. Safety Verification for Probabilistic Hybrid Systems. In Proceedings of the 22nd International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 6174, pp. 196-211, Springer, 2010.CAV为计算机科学“Programming Languages and Software Engineering”领域的国际顶级会议,NUS评价为Rank 1AUS评价为A+)Scholar google搜索结果,40余次引用)(34regular papers中有一篇论文的署名作者是是图灵奖得主Edmund M. Clarke,另有三篇论文的署名作者是欧洲科学院院士Thomas A. Henzinger17tool papers中有一篇论文的署名作者是图灵奖得主Amir Pnueli。特别地,欧洲科学院院士、牛津大学Prof. Marta KwiatkowskaIEEE会士、ETH自动控制实验室主任Prof. John Lygeros等引用了该文。)

6)   Felix Klaedtke, Stefan Ratschan and Zhikun She. Language-based abstraction refinement for hybrid system verification. In Proceedings of the 8th International Conference on Verification, Model Checking and Abstraction Interpretation. Lecture Notes in Computer Science, Vol. 4349, pp. 151-166, Springer, 2007.VMCAI2007共接受21篇学术论文,其中有一篇论文的署名作者是图灵奖得主Amir Pnueli,另有一篇论文的署名作者是欧洲科学院院士Thomas A. Henzinger。

7)   Stefan Ratschan and Zhikun She. Safety Verification of Hybrid System by Constraint Propagation Based Abstraction Refinement. In M. Morari and L. Thiele (Eds.): HSCC 2005, Lecture Notes in Computer Science, Vol. 3414, pp. 573-589, Springer-Verlag, 2005.HSCC为“混成系统”领域的国际领先会议)(HSCC2005共接受40regular papers,其中有一篇论文的署名作者是图灵奖得主Edmund M. Clarke、有一篇论文的署名作者是美国工程院院士Shankar Sastry、有两篇论文的署名作者是美国工程院院士Alberto L. Sangiovanni-Vincentelli)(Scholar google搜索结果,100余次引用。特别地,由美国工程院院士Alberto L. Sangiovanni-Vincentelli发表的、详细介绍国际上混成系统研究方面最新进展的综述性学术论文《Languages and Tools for Hybrid Systems Design》(Foundations and Trends in Electronic Design Automation. Vol. 1, No 1/2 (2006), 1-193)在134140页利用一整节的篇幅详细介绍了此工作,指出“HSolver improves this traditional method by implementing a pruning algorithm that removes uninteresting parts of the state space before reducing the grid size. Consequently, the refinement of the over-approximation can be obtained even without increasing the number of grid locations, one of the causes of exponential blowout in the verification algorithms for hybrid systems”、The language for describing hybrid systems is very easy to understand. There are no limitations in describing a single automaton and the limited number of statements in the language makes it simple to use”。)

8)   Junjie Lu, Zhikun She, Weijie Feng and Shuzhi Sam Ge. Stabilisability of Time-varying Switched Systems Based on Piecewise Continuous Scalar Functions. IEEE Transactions on Automatic Control, 2019. DOI: 10.1109/TAC.2018.2867933.

9)   Xiuliang Zheng, Zhikun She, Junjie Lu and Meilun Li. Computing multiple Lyapunov-like functions for inner estimates of domains of attraction of switched hybrid systems. International Journal of Robust and Nonlinear Control, 2018. DOI: 10.1002/rnc.4280.

10) Quanyi Liang and Zhikun She. Constraint consensus of heterogeneous multi-agent systems. International Journal of Modern Physics C, Vol. 29, No. 5, Article ID 1840005, 9 pages, 2018. DOI: 10.1142/S0129183118400053.

11) Tianrong Weng, Lei Wang, Zhikun She and Quanyi Liang. Distributed Optimization with Closed Convex Set for Multi-Agent Networks Over Directed Graphs. Journal of The Franklin Institute, 2018. DOI: 10.1016/j.jfranklin.2017.12.010.

12) Quanyi Liang, Lei Wang, Qiqi Hao and Zhikun She. Synchronization of heterogeneous linear networks with distinct inner coupling matrices. ISA Transactions, 75: 127-136, 2018. DOI: 10.1016/j.isatra.2018.01.31.

13) Xiuliang Zheng, Zhikun She, Quanyi Liang and Meilun Li. Inner approximations of domains of attraction for a class of switched systems by computing Lyapunov-like functions. International Journal of Robust and Nonlinear Control, 28(6): 2191-2208, 2018. DOI: 10.1002/rnc.4010.

14) Quanyi Liang, Kairong Liu, Gang Meng and Zhikun She. Minimization of the Lowest Eigenvalue for a Vibrating Beam. Discrete and Continuous Dynamical Systems (Series A), 38(4):2079-2092, 2018. DOI:10.3934/dcds.2018085.

15) Junjie Lu, Zhikun She, Shuzhi Sam Ge and Xin Jiang. Stability Analysis of Discrete-time Switched Nonlinear Systems via Multi-step Multiple Lyapunov Functions. Nonlinear Analysis: Hybrid Systems, 27: 44-61, 2018.

16) Xin Jiang, Zhikun She, Zhaosheng Feng and Xiuliang Zheng. Bifurcation Analysis of a Predator-Prey System with Ratio-Dependent Functional Response. International Journal of Bifurcation and Chaos, Vol. 27, No. 14, Article ID 1750222, 21 pages, 2017.

17) Quanyi Liang, Zhikun She, Lei Wang, Michael Chen and Qing-Guo Wang. Characterizations and Criteria for Synchronization of Heterogeneous Networks to Linear Subspaces. SIAM Journal on Control and Optimization, 55(6): 4048-4071, 2017. DOI. 10.1137/16M1086509.

18) Bai Xue, Zhikun She and Arvind Easwaran. Underapproximating Backward Reachable Sets by Semialgebraic Sets. IEEE Transactions on Automatic Control, 62(10): 5185--5197, 2017. DOI: 10.1109/TAC.2017.2694351. (Full Paper)

19) Quanyi Liang, Zhikun She, Lei Wang and Housheng Su. General Lyapunov Functions for Consensus of Nonlinear Multiagent Systems. IEEE Transactions on Circuits and Systems II: Express Briefs, 64(10): 1232-1236, 2017. DOI: 10.1109/TCSII.2017.2647744.

20) Zhikun She, Junjie Lu, Quanyi Liang, Shuzhi Sam Ge. Dwell Time Based Stabilizability Criteria for Discrete-time Switched Systems. International Journal of Systems Science, 48(14): 3087-3097, 2017. DOI: 10.1080/00207721.2017.1367430.

21) Xin Jiang, Gang Meng and Zhikun She. Existence of periodic solutions in a nonautonomous food web with Beddington-DeAngelis functional response. Applied Mathematics Letters, Vol. 71, pp. 59-66, 2017.

22) Xuhua Cheng and Zhikun She. Study on Chaotic behavior of the Restricted Four-body Problem with an Equilateral Triangle Configuration. International Journal of Bifurcation and Chaos, Vol. 27, No. 2, Article ID 1750026, 12 pages, 2017.

23) Xin Jiang, Kairong LiuGang Meng and Zhikun She. Continuity of the Eigenvalues for a Vibrating Beam. Applied Mathematics Letters, Vol. 67, pp. 60-66, 2017.

24) Junjie Lu and Zhikun She. Sufficient and necessary conditions for discrete-time nonlinear switched systems with uniform local exponential stability. International Journal of Systems Science, 47(15): 3561-3572, 2016.

25) Haiyin Li, Gang Meng and Zhikun She. Stability and Hopf Bifurcation of a Delayed Density-Dependent Predator-Prey System with Beddington-DeAngelis Functional Response. International Journal of Bifurcation and Chaos, Vol. 26, No. 10, Article ID 1650165, 17 pages, 2016.

26) Xin Jiang, Zhikun She and Zhaosheng Feng. Stability analysis and Hopf bifurcation in a density-dependent predator-prey system with Beddington-DeAngelis functional response. Electronic Journal of Differential Equations, Vol. 2016, No. 255, pp. 1-20, 2016.

27) Haiyin Li and Zhikun She. Dynamics of a Non-autonomous Density-Dependent Predator-Prey Model with Beddington-DeAngelis Type. International Journal of Biomathematics, Vol. 9, No. 4, Article ID 1650050, 25 pages, 2016.

28) Haiyin Li and Zhikun She. Uniqueness of Periodic Solutions of a Nonautonomous Density-Dependent Predator-Prey System. Journal of Mathematical Analysis and Applications, 422(2): 886-905, Elsevier, 2015.

29) Xuhua Cheng and Zhikun She. A Note on the Existence of a Smale Horseshoe in the Planar Circular Restricted Three-Body Problem. Abstract and Applied Analysis, Volume 2015, Article ID 965829, 8 pages, 2015.

30) Zhikun She and Bai Xue. Discovering Multiple Lyapunov Functions for Switched Hybrid Systems. SIAM Journal on Control and Optimization, 52(5): 3312-3340, 2014.

31) Haiyin Li and Zhikun She. A DENSITY-DEPENDENT PREDATOR-PREY MODEL WITH BEDDINGTON-DEANGELIS TYPE. Electronic Journal of Differential Equations, Vol. 2014, No. 192, pp. 1-15, 2014.

32) Zhikun She and Xuhua Cheng. The Existence of a Smale Horseshoe in a Planar Circular Restricted Four-Body Problem. Celestial Mechanics and Dynamical Astronomy, 118(2): 115-127, 2014.

33) Zhikun She, Haoyang Li, Bai Xue, Zhiming Zheng and Bican Xia. Discovering Polynomial Lyapunov Functions for Continuous Dynamical Systems. Journal of Symbolic Computation, 58: 41-63, Elsevier, 2013.

34) Zhikun She and Bai Xue. Computing an invariance kernel with target by computing Lyapunov-like functions. IET Control Theory and Applications, 7(15): 1932-1940, 2013.

35) Zhikun She and Haiyin Li. Dynamics of a Density-Dependent Stage-Structured Predator-Prey System with Beddington-DeAngelis Functional Response. Journal of Mathematical Analysis and Applications, 406(1): 188-202, Elsevier, 2013.

36) Zhikun She, Xuhua Cheng and Cuiping Li. The Existence of Transversal Homoclinic Orbits in a Planar Circular Restricted Four-Body Problem. Celestial Mechanics and Dynamical Astronomy, 115(3): 299-309, Springer, 2013.

37) Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns and Ernst M. Hahn. Safety Verification for Probabilistic Hybrid Systems. European Journal of Control, 18(6): 572-587, 2012.(图灵奖得主Edmund M. Clarke在综述性学术论文《32 Years of Model CheckingLecture Notes in Computer ScienceVolume 8974, pp 26-402015)首先指出“Results related to the analysis and verification of SHSs are still limited. For instance, analysis approaches for GSHSs are often based on Monte-Carlo simulation. Considering the hardness of dealing with the general class, efforts have been mainly placed on different subclasses For a more expressive class of models - probabilistic hybrid automata (PHAs), Zhang et al. abstracted the original PHA to a probabilistic automaton (PA), and then used the established Model Checking methods for the abstracting model,然后在第3.2节“Abstraction-based Methods”中利用大部分篇幅重点描述了我们的“abstraction-based method”,并进一步通过Figure 1中的例子直观地解释我们的整个抽象流程;美国Vanderbilt大学Prof . X. Koutsoukos对该文专门写了DiscussionDiscussion on: Safety Verification for Probabilistic Hybrid Systems”,European Journal of Control, 18(6): 588-590, 2012),一开头就指出“The work extends formal verification methods of (nonprobabilistic) hybrid systems based on discrete abstractions”。)

38) Zhikun She, Bican Xia and Zhiming Zheng. Condition number based complexity estimate for solving polynomial systems. Journal of Computational and Applied Mathematics, 235(8): 2670-2678, Elsevier, 2011.