A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. (January 2017)

• Record Type: Journal Article
• Authors: Ghorbal, Khalil; Sogokon, Andrew; Platzer, André
• Is Part Of: Computer languages, systems & structures. Volume 47:Part 1(2017)
• Page Start: 19
• Page End: 43
• Publication Date: 2017-01
• Subjects: Formal verification -- Polynomial differential equations -- Positive invariance -- Deductive power -- Dynamical systems; Programming languages (Electronic computers) -- Periodicals; Computer networks -- Periodicals; Computer architecture -- Periodicals; Computer systems -- Periodicals; Langage de programmation; Réseau d'ordinateurs; Architecture d'ordinateur; Périodique électronique (Descripteur de forme); Ressource Internet (Descripteur de forme); 005.13
• DOI: 10.1016/j.cl.2015.11.003
• Languages: English
• ISSNs: 1477-8424

Abstract

Abstract: This paper studies sound proof rules for checking positive invariance of algebraic and semi-algebraic sets, that is, sets satisfying polynomial equalities and those satisfying finite boolean combinations of polynomial equalities and inequalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting. Abstract : Highlights: 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.