kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal safety verification of unknown continuous-time systems: A data-driven approach
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control).ORCID iD: 0000-0002-5452-8850
2021 (English)In: HSCC 2021 - Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control (part of CPS-IoT Week), Association for Computing Machinery (ACM) , 2021Conference paper, Published paper (Refereed)
Abstract [en]

This work studies formal verification of continuous-time continuous-space systems with unknown dynamics against safety specifications. The proposed framework is based on a data-driven construction of barrier certificates using which the safety of unknown systems is verified via a finite set of data collected from trajectories of systems with a priori guaranteed confidence. In the proposed scheme, we first cast the original safety problem as a robust convex program (RCP). Since the unknown model appears in one of the constraints of the proposed RCP, we provide the scenario convex program (SCP) corresponding to the original RCP by collecting finite numbers of data from systems' evolutions. We then establish a probabilistic closeness between the optimal value of SCP and that of RCP. Accordingly, we formally quantify the safety guarantee of unknown systems based on the number of data and the required level of safety confidence. Motivations. In the past few years, formal methods have become a promising approach to analyze dynamical systems against high-level logic properties, e.g., those expressed as linear temporal logic (LTL) formulae, in a reliable way. In this regard, barrier certificates, as a discretization-free approach, have received significant attention as a useful tool for formal analysis of complex dynamical systems. In particular, barrier certificates are Lyapunov-like functions defined over the state space of systems subjected to a set of inequalities on both the function itself and its time derivative along the flow of the system. The existence of such a function provides a formal certificate for the safety of the system [1, 2]. To employ the proposed approaches in the setting of barrier certificates, one needs to know precise models of dynamical systems and, hence, those approaches are not applicable where the model is unknown. Although there are some identification techniques in the relevant literature to first learn the model and then provide the analysis framework (e.g., [3, 4]), acquiring an accurate model for complex systems is always very challenging, time-consuming, and expensive. This crucial challenge motivated us to employ data-driven approaches and directly construct barrier certificates via data collected from trajectories of unknown systems.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM) , 2021.
Keywords [en]
barrier certificates, data-driven optimization, formal safety verification, unknown continuous-time systems
National Category
Control Engineering
Identifiers
URN: urn:nbn:se:kth:diva-309863DOI: 10.1145/3447928.3456661ISI: 000932821700025Scopus ID: 2-s2.0-85105878146OAI: oai:DiVA.org:kth-309863DiVA, id: diva2:1644451
Conference
HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021
Note

QC 20220314

Part of proceedings: ISBN 978-145038339-4

Available from: 2022-03-14 Created: 2022-03-14 Last updated: 2023-09-21Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Jagtap, Pushpak

Search in DiVA

By author/editor
Jagtap, Pushpak
By organisation
Decision and Control Systems (Automatic Control)
Control Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 11 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf