Sampling-Based Resolution-Complete Algorithms for Safety Falsification of Linear Systems
From MaRDI portal
Publication:3523142
DOI10.1007/978-3-540-78929-1_45zbMATH Open1144.93309arXiv0801.0570OpenAlexW1613235480MaRDI QIDQ3523142FDOQ3523142
Authors: Amit Bhatia, Emilio Frazzoli 
Publication date: 2 September 2008
Published in: Hybrid Systems: Computation and Control (Search for Journal in Brave)
Abstract: In this paper, we describe a novel approach for checking safety specifications of a dynamical system with exogenous inputs over infinite time horizon that is guaranteed to terminate in finite time with a conclusive answer. We introduce the notion of resolution completeness for analysis of safety falsification algorithms and propose sampling-based resolution-complete algorithms for safety falsification of linear time-invariant discrete time systems over infinite time horizon. The algorithms are based on deterministic incremental search procedures, exploring the reachable set for feasible counter examples to safety at increasing resolution levels of the input. Given a target resolution of inputs, the algorithms are guaranteed to terminate either with a reachable state that violates the safety specification, or prove that no input exists at the given resolution that violates the specification.
Full work available at URL: https://arxiv.org/abs/0801.0570
Recommendations
- Sampling-based falsification and verification of controllers for continuous dynamic systems
- Falsification of LTL Safety Properties in Hybrid Systems
- Reachability analysis of linear systems with stepwise constant inputs
- Falsification of hybrid systems with symbolic reachability analysis and trajectory splicing
- Parsimonious, Simulation Based Verification of Linear Systems
Attainable sets, reachability (93B03) Linear systems in control theory (93C05) Discrete-time control/observation systems (93C55)
Cited In (7)
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Sampling-based falsification and verification of controllers for continuous dynamic systems
- Rigorous constraint satisfaction for sampled linear systems
- Extracting counterexamples induced by safety violation in linear hybrid systems
- Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate
- Temporally and spatially flexible plan execution for dynamic hybrid systems
- A delta-sampling verification theorem for discrete-time, possibly discontinuous systems
Uses Software
This page was built for publication: Sampling-Based Resolution-Complete Algorithms for Safety Falsification of Linear Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3523142)
