A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

详细信息    查看全文

• 作者：Khalil Ghorbal^a ; ^{kghorbal@cs.cmu.edu} ; Andrew Sogokon^c ; ^{a.sogokon@sms.ed.ac.uk} ; André ; Platzer^b ; ^{aplatzer@cs.cmu.edu}
• 关键词：Formal verification ; Polynomial differential equations ; Positive invariance ; Deductive power ; Dynamical systems
• 刊名：Computer Languages, Systems & Structures
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：47
• 期：part_P1
• 页码：19-43
• 全文大小：2311 K
• 卷排序：47

文摘

We investigate proof rules to check positive invariance of semialgebraic sets. We introduce a sufficient condition we term nonsmooth Strict Barrier Certificate. We explore the effect of square-free decomposition. We assess the practical proof rule performance on a set of benchmarks.