1,721,004 research outputs found
Optimization of Lyapunov Invariants in Verification of Software Systems
Full text linkThe paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance specifications. These include but are not limited to absence of overflow, absence of division-by-zero, termination in finite time, absence of dead-code, and certain user-specified assertions. Central to this framework are Lyapunov invariants. These are properly constructed functions of the program variables, and satisfy certain properties-analogous to those of Lyapunov functions-along the execution trace. The search for the invariants can be formulated as a convex optimization problem. If the associated optimization problem is feasible, the result is a certificate for the specification.National Science Foundation (U.S.) (Grant CNS-1135955)National Science Foundation (U.S.) (Grant CPS-1135843)United States. Army Research Office. Multidisciplinary University Research Initiative (Award W911NF-11-1-0046)United States. National Aeronautics and Space Administration (Grant/Cooperative Agreement NNX12AM52A
Input classes for identifiability of bilinear systems
No full textThis paper asks what classes of input signals are sufficient in order to completely identify the input/output behavior of generic bilinear systems. The main results are that step inputs are not sufficient, nor are single pulses, but the family of all pulses (of a fixed amplitude but varying widths) do suffice for identification.National Science Foundation (U.S.) (DMS-0504557)National Science Foundation (U.S.) (DMS-0614371)National Science Foundation (U.S.) (DMS-0614371)National Natural Science Foundation of China (Grant No. 60228003
Stability analysis of uncertain systems: Integral quadratic constraints approach
Full text linkThis work describes a practical implementation of a unified approach to robustness analysis with respect to nonlinearities, time-variations and uncertain parameters called Intergral Quadratic Constraints (IQC) methodology. It can be used as an introduction to a specific technique developed by Alexandre Megretski and Anders Ranzer and as a manual to the software package for stability analysis of uncertain system.
There are basically three parts of the script. After introduction to the methodology in Chapter 1 we present the main theoretical results by A. Megretski and A. Ranzer which are the basis of the whole IQC approach. Then we discuss the practical issues arised in applying this technique to application problems and the way they have been implemented in the IQC toolbox by the author. The last chapter shows how powerful is the tool developed for the application to stabilizing of F-16 aircraft model
Stable nonlinear identification from noisy repeated experiments via convex optimization
Full text linkThis paper introduces new techniques for using convex optimization to fit input-output data to a class of stable nonlinear dynamical models. We present an algorithm that guarantees consistent estimates of models in this class when a small set of repeated experiments with suitably independent measurement noise is available. Stability of the estimated models is guaranteed without any assumptions on the input-output data. We first present a convex optimization scheme for identifying stable state-space models from empirical moments. Next, we provide a method for using repeated experiments to remove the effect of noise on these moment and model estimates. The technique is demonstrated on a simple simulated example
Explicit Solutions for Root Optimization of a Polynomial Family with One Affine Constraint
Full text linkGiven a family of real or complex monic polynomials of fixed degree with one affine constraint on their coefficients, consider the problem of minimizing the root radius (largest modulus of the roots) or root abscissa (largest real part of the roots). We give constructive methods for efficiently computing the globally optimal value as well as an optimal polynomial when the optimal value is attained and an approximation when it is not. An optimal polynomial can always be chosen to have at most two distinct roots in the real case and just one distinct root in the complex case. Examples are presented illustrating the results, including several fixed-order controller optimal design problems
Distributed lyapunov functions in analysis of graph models of software
No full textIn previous works, the authors introduced a framework for software analysis, which is based on optimization of Lyapunov invariants. These invariants prove critical software properties such as absence of overflow and termination in finite time. In this paper, graph models of software are introduced and the software analysis framework is further developed and extended on graph models. A distributed Lyapunov function is assigned to the software by assigning a Lyapunov function to every node on its graph model. The global decremental condition is then enforced by requiring that the Lyapunov functions on each node decrease as transitions take place along the arcs. The concept of graph reduction and optimality of graphs for Lyapunov analysis is briefly discussed.National Science Foundation (U.S.) (NSF-0715025
Lower bounds on the performance of Analog to Digital Converters
Full text linkThis paper deals with the task of finding certified lower bounds for the performance of Analog to Digital Converters (ADCs). A general ADC is modeled as a causal, discrete-time dynamical system with outputs taking values in a finite set. We define the performance of an ADC as the worst-case average intensity of the filtered input matching error. The input matching error is the difference between the input and output of the ADC. This error signal is filtered using a shaping filter, the passband of which determines the frequency region of interest for minimizing the error. The problem of finding a lower bound for the performance of an ADC is formulated as a dynamic game problem in which the input signal to the ADC plays against the output of the ADC. Furthermore, the performance measure must be optimized in the presence of quantized disturbances (output of the ADC) that can exceed the control variable (input of the ADC) in magnitude. We characterize the optimal solution in terms of a Bellman-type inequality. A numerical approach is presented to compute the value function in parallel with the feedback law for generating the worst case input signal. The specific structure of the problem is used to prove certain properties of the value function that allow for iterative computation of a certified solution to the Bellman inequality. The solution provides a certified lower bound on the performance of any ADC with respect to the selected performance criteria.United States. Army Research Office. Efficient Linearized All-Silicon Transmitter IC
Optimality and performance limitations of analog to digital converters
No full textThe paper deals with the task of optimal design of Analog to Digital Converters (ADCs). A general ADC is modeled as a causal, discrete-time dynamical system with outputs taking values in a finite set. Its performance is defined as the worst-case average intensity of the filtered input matching error. The design task can be viewed as that of optimal quantized decision making with the objective of optimizing the performance measure. An algorithm based on principles of optimal control is presented for designing general m-dimensional ADCs. The design process involves numerical computation of the candidate value function of the underlying dynamic program, which is computed iteratively, in parallel with the quantization law. A procedure is presented for certifying the numerical solution and providing an upper bound for performance of the designed ADC. Furthermore, an exact analytical solution to the optimal one-dimensional ADC is presented. It is shown that the designed one-dimensional optimal ADC is identical to the classical Delta-Sigma Modulator (DSM) with uniform quantization spacing.National Science Foundation (U.S.). (Grant number 0835947)Los Alamos National Laboratory. Information Science and Technology Institut
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
