Falsification using reachability of surrogate Koopman models

DOI10.1145/3641513.3650141MaRDI QIDQ6993484zbMATH OpenFDO

Authors Stanley Bak, Sergiy Bogomolov, Abdelrahman Hekal, Niklas Kochdumper, Andrew Mata, Amir Rahmati

Publication date 25 April 2025

Full work available at URL https://doi.org/10.1145/3641513.3650141

zbMATH Keywords

cyber-physical systemsfalsificationKoopman operator linearizationreachability analysissignal temporal logic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Cites work

• A data-driven approximation of the koopman operator: extending dynamic mode decomposition
• Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness
• Falsification of cyber-physical systems with robustness-guided black-box checking
• Falsification of hybrid systems using symbolic reachability and trajectory splicing
• Falsification of temporal properties of hybrid systems using the cross-entropy method
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Hamiltonian Systems and Transformation in Hilbert Space
• scientific article; zbMATH DE number 6678650 (Why is no real title available?)
• scientific article; zbMATH DE number 44386 (Why is no real title available?)
• scientific article; zbMATH DE number 1916891 (Why is no real title available?)
• Linear predictors for nonlinear dynamical systems: Koopman operator meets model predictive control
• Linearization of discrete-time systems
• Logical foundations of cyber-physical systems
• Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems
• Nonlinear set‐membership state estimation based on the Koopman operator
• Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
• Robustness of temporal logic specifications for continuous-time signals
• S-TaLiRo: a tool for temporal logic falsification for hybrid systems
• Scalable extended dynamic mode decomposition using random kernel approximation
• Simulation-equivalent reachability of large linear systems with inputs
• Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis
• Stochastic local search for falsification of hybrid systems
• Utilizing dependencies to obtain subsets of reachable sets

Cited in

(1)

• Exploring behaviors of hybrid systems via the Voronoi bias over output signals

This page was built for publication: Falsification using reachability of surrogate Koopman models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6993484)