Related Experiment Video
Updated: Nov 15, 2025
14:05
One Dimensional Turing-Like Handshake Test for Motor Intelligence
Published on: December 15, 2010
28.2K
Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration
Dario Cattaruzza1, Alessandro Abate1, Peter Schrammel2
1Department of Computer Science, University of Oxford, Oxford, UK.
Journal of Automated Reasoning
|March 8, 2021
Summary
This study introduces counterexample-guided Abstract Acceleration for sound safety verification of infinite-horizon linear time-invariant (LTI) models. The method robustly over-approximates reachability tubes, improving upon existing tools.
Area of Science:
- Control Theory
- Formal Verification
- Computer Science
Background:
- Reachability analysis is crucial for dynamical systems but faces limitations in accuracy and scope.
- Verifying safety properties of unbounded-time systems, especially linear time-invariant (LTI) models, remains challenging.
Purpose of the Study:
- To develop a sound safety verification method for infinite-horizon LTI models with inputs.
- To address limitations in current reachability analysis techniques for complex dynamical systems.
Main Methods:
- Employs counterexample-guided Abstract Acceleration for over-approximating reachability tubes.
- Utilizes abstraction techniques to manage unbounded time horizons and potentially refine results with concrete counterexamples.
Main Results:
- Demonstrates robust performance in safety verification of various LTI models.
- Achieves sound verification for unbounded-time LTI systems, outperforming current state-of-the-art tools in tested scenarios.
Conclusions:
- Counterexample-guided Abstract Acceleration offers a sound and effective approach for LTI system safety verification.
- The proposed method enhances the reliability and applicability of reachability analysis for infinite-horizon dynamical models.
Related Concept Videos
01:23Linear time-invariant Systems
652
A system is linear if it displays the characteristics of homogeneity and additivity, together termed the superposition property. This principle is fundamental in all linear systems. Linear time-invariant (LTI) systems include systems with linear elements and constant parameters.
The input-output behavior of an LTI system can be fully defined by its response to an impulsive excitation at its input. Once this impulse response is known, the system's reaction to any other input can be...
The input-output behavior of an LTI system can be fully defined by its response to an impulsive excitation at its input. Once this impulse response is known, the system's reaction to any other input can be...
652
01:29Evaluating Limits by Direct Substitution
41
In the analysis of functions that represent continuous physical phenomena, it is often necessary to determine the output value as the input approaches a specific point. When a combination of algebraic terms defines the function and exhibits no discontinuities or abrupt changes near the point of interest, the limit of the function can be evaluated directly. This process, known as direct substitution, involves replacing the variable in the expression with the value it approaches.Direct...
41
01:26Constraints and Statical Determinacy
831
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
831
01:24BIBO stability of continuous and discrete -time systems
717
System stability is a fundamental concept in signal processing, often assessed using convolution. For a system to be considered bounded-input bounded-output (BIBO) stable, any bounded input signal must produce a bounded output signal. A bounded input signal is one where the modulus does not exceed a certain constant at any point in time.
To determine the BIBO stability, the convolution integral is utilized when a bounded continuous-time input is applied to a Linear Time-Invariant (LTI) system....
To determine the BIBO stability, the convolution integral is utilized when a bounded continuous-time input is applied to a Linear Time-Invariant (LTI) system....
717
01:21Linear Approximation in Time Domain
197
Nonlinear systems often require sophisticated approaches for accurate modeling and analysis, with state-space representation being particularly effective. This method is especially useful for systems where variables and parameters vary with time or operating conditions, such as in a simple pendulum or a translational mechanical system with nonlinear springs.
For a simple pendulum with a mass evenly distributed along its length and the center of mass located at half the pendulum's length,...
For a simple pendulum with a mass evenly distributed along its length and the center of mass located at half the pendulum's length,...
197
01:28Stability
236
The time response of a linear time-invariant (LTI) system can be divided into transient and steady-state responses. The transient response represents the system's initial reaction to a change in input and diminishes to zero over time. In contrast, the steady-state response is the behavior that persists after the transient effects have faded.
The stability of an LTI system is determined by the roots of its characteristic equation, known as poles. A system is stable if it produces a bounded...
The stability of an LTI system is determined by the roots of its characteristic equation, known as poles. A system is stable if it produces a bounded...
236