Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Interpolation-Inspired Closure Certificates

Mohammed Adib Oumer, Vishnu Murali, Majid Zamani

TL;DR

An SOS programming approach is presented to search for sets of functions which jointly over-approximate a transition invariant by first considering one-step transitions, then two, and repeat until a transition invariant is obtained.

Abstract

Barrier certificates, a form of state invariants, provide an automated approach to the verification of the safety of dynamical systems. Similarly to barrier certificates, recent works explore the notion of closure certificates, a form of transition invariants, to verify dynamical systems against $ω$-regular properties including safety. A closure certificate, defined over state pairs of a dynamical system, is a real-valued function whose zero superlevel set characterizes an inductive transition invariant of the system. The search for such a certificate can be effectively automated by assuming it to be within a specific template class, e.g. a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, one may not be able to find such a certificate for a fixed template. In such a case, one must change the template, e.g. increase the degree of the polynomial. In this paper, we consider a notion of multiple closure certificates dubbed interpolation-inspired closure certificates. An interpolation-inspired closure certificate consists of a set of functions which jointly over-approximate a transition invariant by first considering one-step transitions, then two, and so on until a transition invariant is obtained. The advantage of interpolation-inspired closure certificates is that they allow us to prove properties even when a single function for a fixed template cannot be found using standard approaches. We present SOS programming and a scenario program to find these sets of functions and demonstrate the effectiveness of our proposed method to verify persistence and general $ω$-regular specifications in some case studies.

Interpolation-Inspired Closure Certificates

TL;DR

An SOS programming approach is presented to search for sets of functions which jointly over-approximate a transition invariant by first considering one-step transitions, then two, and repeat until a transition invariant is obtained.

Abstract

Barrier certificates, a form of state invariants, provide an automated approach to the verification of the safety of dynamical systems. Similarly to barrier certificates, recent works explore the notion of closure certificates, a form of transition invariants, to verify dynamical systems against -regular properties including safety. A closure certificate, defined over state pairs of a dynamical system, is a real-valued function whose zero superlevel set characterizes an inductive transition invariant of the system. The search for such a certificate can be effectively automated by assuming it to be within a specific template class, e.g. a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, one may not be able to find such a certificate for a fixed template. In such a case, one must change the template, e.g. increase the degree of the polynomial. In this paper, we consider a notion of multiple closure certificates dubbed interpolation-inspired closure certificates. An interpolation-inspired closure certificate consists of a set of functions which jointly over-approximate a transition invariant by first considering one-step transitions, then two, and so on until a transition invariant is obtained. The advantage of interpolation-inspired closure certificates is that they allow us to prove properties even when a single function for a fixed template cannot be found using standard approaches. We present SOS programming and a scenario program to find these sets of functions and demonstrate the effectiveness of our proposed method to verify persistence and general -regular specifications in some case studies.
Paper Structure (22 sections, 10 theorems, 19 equations, 2 figures)

This paper contains 22 sections, 10 theorems, 19 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Notation
  4. Discrete-time Dynamical System
  5. Formal Specifications and Verification Results
  6. Safety
  7. Persistence
  8. Linear Temporal Logic (LTL)
  9. Interpolation-Inspired Closure Certificates
  10. ICCs for Safety
  11. ICCs for Persistence
  12. ICCs for LTL Specifications
  13. Computation of ICCs
  14. Safety
  15. Persistence
  16. ...and 7 more sections

Key Result

Theorem 1

For a system $\mathcal{S}$ with unsafe states $\mathcal{X}_u$, the existence of a barrier certificate $\mathcal{B}$ satisfying conditions eq:bc_1-eq:bc_3 implies its safety.

Figures (2)

  • Figure 1: Sample state trajectories of Lotka-Volterra dynamic model. Set $\mathcal{X}_{VF}$ is only visited finitely often.
  • Figure 2: An NBA $\mathcal{A}$ for the two-room temperature case study from Section \ref{['subsec:ltl_casestudy']}. The automata represents the LTL formula $\neg( a\ \mathsf{U}\ \mathsf{G} c)$. $\top$ indicates any letter in the alphabet.

Theorems & Definitions (24)

  • Definition 2.1
  • Definition 2.2: BC
  • Theorem 1: BCs imply safety prajna2004safety
  • Definition 2.3: IBC
  • Theorem 2: IBCs imply safety oumer2024ibc
  • Definition 2.4: CC for Safety
  • Theorem 3: CCs imply safety murali2024closure
  • Definition 2.5: CC for Persistence
  • Theorem 4: CCs imply Persistence murali2024closure
  • Definition 2.6: CC for LTL
  • ...and 14 more