FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Vector Barrier Certificates and Comparison Systems

Authors: Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan and André Platzer

Paper Information

Title:Vector Barrier Certificates and Comparison Systems
Authors:Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan and André Platzer
Proceedings:FM FMComplete
Editors: Jan Peleska, Klaus Havelund and Bill Roscoe
Keywords:barrier certificates, safety verification, continuous systems, ordinary differential equations, comparison systems, vector Lyapunov functions
Abstract:

ABSTRACT. Vector Lyapunov functions are a multi-dimensional extension of the more familiar (scalar) Lyapunov functions, commonly used to prove stability properties in systems described by non-linear ordinary differential equations (ODEs). This paper explores an analogous vector extension for so-called barrier certificates used in safety verification. As with vector Lyapunov functions, the approach hinges on constructing appropriate comparison systems, i.e., related differential equation systems from which properties of the original system may be inferred. The paper presents an accessible development of the approach, demonstrates that most previous notions of barrier certificate are special cases of comparison systems, and discusses the potential applications of vector barrier certificates in safety verification and invariant synthesis.

Pages:19
Talk:Jul 16 17:00 (Session 115C)
Paper: