球友会qy

天基综合信息系统全国重点实验室2025年度鲁班论坛第7期

时 间：2025年5月28日 15:00 – 16:00

地 点：中国科研实验室软件园区5号楼4层第三会议室

主讲人：Khalil Ghorbal, 研究员, INRIA / 法国国家信息与自动化研究所

报告主题：Deductive Safety Verification of Continuous and Cyber-Physical System:The Problem of Checking Positively Invariant Sets

报告摘要：

Checking inductive invariance of sets is of fundamental importance in deductive safety verification of continuous and cyber-physical systems. In this talk, we present two characterizations of positive invariance of sets under the flow of systems of ordinary differential equations. The first characterization uses inward sets which intuitively collect those points from which the flow evolves within the set for a short period of time, whereas the second characterization uses the notion of exit sets, which intuitively collect those points from which the flow immediately leaves the set.

Our proofs emphasize the use of the real induction principle as a generic and unifying proof technique that captures the essence of the formal reasoning justifying our results and provides cleaner alternative proofs of known results. The two characterizations presented in this article, while essentially equivalent, lead to two rather different decision procedures (termed respectively LZZ and ESE) for checking whether a given semi-algebraic set is positively invariant under the flow of a system of polynomial ordinary differential equations. The procedure LZZ improves upon the original work by Liu, Zhan and Zhao (Liu et al., 2011). The procedure ESE is novel and works by splitting the problem, in a principled way, into simpler sub-problems that are easier to check, and is shown to exhibit substantially better performance compared to LZZ on problems featuring semi-algebraic sets described by formulas with non-trivial Boolean structure. We will briefly focus on the special case in which all polynomials are affine to show a number of interesting computational properties that afford considerable improvements to the efficiency of invariant checking.

报告人介绍：

Khalil Ghorbal is a researcher at INRIA, France. He primarily works on differential algebra with a particular interest in differential ideals, their characterization and effective computation. He has previously worked on interactive theorem provers and still actively involved in devising novel techniques to improve the scalability of the formal verification of dynamical and hybrid systems.