A Scenario Approach for Synthesizing k-Inductive Barrier Certificates

Murali, Vishnu; Trivedi, Ashutosh und Zamani, Majid (2022): A Scenario Approach for Synthesizing k-Inductive Barrier Certificates. In: IEEE Control Systems Letters (L-Css), Bd. 6: S. 3247-3252

Abstract

The notion of k-inductive barrier certificates generalize the idea of k-induction to verification of discrete-time continuous-state dynamical systems by requiring restrictions over k-grams (sequence of k-states in evolution) of the system transitions. The promise of k-inductive barrier certificates is in the simplicity of the form of barrier certificates (lower-degree of polynomials) at the cost of more complex non-convex constraints involving logical implications. Recent breakthroughs in convex robust programming via the scenario approach deliver a sampling-based randomized algorithm for the computation of barrier certificates. In the absence of system dynamics (a.k.a. black box models), extending scenario approach to k-inductive barrier certificates faces challenges due to the resulting lack of convexity. This letter overcomes non-convexity challenges by providing a sound approach for data-driven computation of k-inductive barrier certificates. We present computational methods to solve the resulting scenario programs for k-inductive barrier certificates, provide out-of-sample performance guarantees, and experimentally demonstrate the effectiveness of the proposed results.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 2475-1456
• Sprache: Englisch