Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userBehavioural contracts for linear dynamical systems: input assumptions and output guarantees
89
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
We introduce contracts for linear dynamical systems with inputs and outputs. Contracts are used to express formal specifications on the dynamic behaviour of such systems through two aspects: assumptions and guarantees. The assumptions are a linear system that captures the available knowledge about the dynamic behaviour of the environment in which the system is supposed to operate. The guarantees are a linear system that captures the required dynamic behaviour of the system when interconnected with its environment. In addition to contracts, we also define and characterize notions of contract refinement and contract conjunction. Contract refinement allows one to determine if a contract expresses a stricter specifications than another contract. On the other hand, contract conjunction allows one to combine multiple contracts into a single contract that fuses the specifications they express.
rate research
Read More
Motivated by the growing requirements on the operation of complex engineering systems, we present contracts as specifications for continuous-time linear dynamical systems with inputs and outputs. A contract is defined as a pair of assumptions and guarantees, both characterized in a behavioural framework. The assumptions encapsulate the available information about the dynamic behaviour of the environment in which the system is supposed to operate, while the guarantees express the desired dynamic behaviour of the system when interconnected with relevant environments. In addition to defining contracts, we characterize contract implementation, and we find necessary conditions for the existence of an implementation. We also characterize contract refinement, which is used to characterize contract conjunction in two special cases. These concepts are then illustrated by an example of a vehicle following system.
In this paper, we consider the systems with trajectories originating in the nonnegative orthant becoming nonnegative after some finite time transient. First we consider dynamical systems (i.e., fully observable systems with no inputs), which we call eventually positive. We compute forward-invariant cones and Lyapunov functions for these systems. We then extend the notion of eventually positive systems to the input-output system case. Our extension is performed in such a manner, that some valuable properties of classical internally positive input-output systems are preserved. For example, their induced norms can be computed using linear programming and the energy functions have nonnegative derivatives.
We consider the effect of parametric uncertainty on properties of Linear Time Invariant systems. Traditional approaches to this problem determine the worst-case gains of the system over the uncertainty set. Whilst such approaches are computationally tractable, the upper bound obtained is not necessarily informative in terms of assessing the influence of the parameters on the system performance. We present theoretical results that lead to simple, convex algorithms producing parametric bounds on the $mathcal{L}_2$-induced input-to-output and state-to-output gains as a function of the uncertain parameters. These bounds provide quantitative information about how the uncertainty affects the system.
A central question in verification is characterizing when a system has invariants of a certain form, and then synthesizing them. We say a system has a $k$ linear invariant, $k$-LI in short, if it has a conjunction of $k$ linear (non-strict) inequalities -- equivalently, an intersection of $k$ (closed) half spaces -- as an invariant. We present a sufficient condition -- solely in terms of eigenvalues of the $A$-matrix -- for an $n$-dimensional linear dynamical system to have a $k$-LI. Our proof of sufficiency is constructive, and we get a procedure that computes a $k$-LI if the condition holds. We also present a necessary condition, together with many example linear systems where either the sufficient condition, or the necessary is tight, and which show that the gap between the conditions is not easy to overcome. In practice, the gap implies that using our procedure, we synthesize $k$-LI for a larger value of $k$ than what might be necessary. Our result enables analysis of continuous and hybrid systems with linear dynamics in their modes solely using reasoning in the theory of linear arithmetic (polygons), without needing reasoning over nonlinear arithmetic (ellipsoids).
This paper considers the identification of FIR systems, where information about the inputs and outputs of the system undergoes quantization into binary values before transmission to the estimator. In the case where the thresholds of the input and output quantizers can be adapted, but the quantizers have no computation and storage capabilities, we propose identification schemes which are strongly consistent for Gaussian distributed inputs and noises. This is based on exploiting the correlations between the quantized input and output observations to derive nonlinear equations that the true system parameters must satisfy, and then estimating the parameters by solving these equations using stochastic approximation techniques. If, in addition, the input and output quantizers have computational and storage capabilities, strongly consistent identification schemes are proposed which can handle arbitrary input and noise distributions. In this case, some conditional expectation terms are computed at the quantizers, which can then be estimated based on binary data transmitted by the quantizers, subsequently allowing the parameters to be identified by solving a set of linear equations. The algorithms and their properties are illustrated in simulation examples.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
