اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدBehavioural contracts for linear dynamical systems: input assumptions and output guarantees
89
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
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 gua
rantees, 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) inequalit
ies -- 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 out
put 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.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
