Sampling-Based Resolution-Complete Algorithms for Safety Falsification of Linear Systems

DOI10.1007/978-3-540-78929-1_45MaRDI QIDQ3523142zbMATH OpenOpenAlexFDO

Authors Amit Bhatia, Emilio Frazzoli

Publication date 2 September 2008

Published in Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0801.0570

Mathematics Subject Classification ID

Attainable sets, reachability (93B03) Linear systems in control theory (93C05) Discrete-time control/observation systems (93C55)

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.

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

Cited in

(7)

• Extracting counterexamples induced by safety violation in linear hybrid systems
• Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate
• A delta-sampling verification theorem for discrete-time, possibly discontinuous systems
• Sampling-based falsification and verification of controllers for continuous dynamic systems
• Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
• Rigorous constraint satisfaction for sampled linear systems
• Temporally and spatially flexible plan execution for dynamic hybrid systems

Describes a project that uses

Uses Software

• HyTech
• d/dt

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)