Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions

Author(s):  
Joachim Bard ◽  
Heiko Becker ◽  
Eva Darulova
Keyword(s):  
Author(s):  
Иннокентий Васильевич Семушин ◽  
Юлия Владимировна Цыганова ◽  
Андрей Владимирович Цыганов

Предложен новый метод автоматического контроля оптимальности дискретного фильтра Калмана, основанный на равенстве нулю градиента вспомогательного функционала качества (ВФК) по параметрам адаптивного дискретного фильтра. Для вычисления градиента ВФК применяется численно устойчивый к ошибкам машинного округления алгоритм модифицированной взвешенной ортогонализации Грама-Шмидта (MWGS-ортогонализации). Алгоритм реализован на языке Matlab. Результаты проведенных численных экспериментов подтверждают эффективность предложенного метода The paper proposes a new method for automatic control of the nominal operating mode of a dynamic stochastic system, based on a combination of two previously developed methods: the auxiliary performance index (API) method and the LD modification of an adaptive filter numerically robust to roundoff errors. The API method was previously developed to solve the problems of identification, adaptation, and control of stochastic systems with control and filtering. We suggest using the API not only as a tool for identifying the parameters of the stochastic system model from the measurement data but also for automatically monitoring the optimality of the adaptive filter, namely, the condition that the API gradient is close to zero should be satisfied (with the necessity and sufficiency) at the point corresponding to the optimal value of the vector parameter in the adaptive Kalman filter. The main result is the new eLD-KF-AC algorithm (extended LD Kalman-like adaptive filtering algorithm with automatic optimality control). The advantages of the obtained solution are as follows: 1) the choice of the adaptive filter structure in the form of an extended LD algorithm can significantly reduce the effect of machine roundoff errors on the calculation results when supplemented by the ability to calculate the sensitivity functions by the system vector parameter of the adaptive filter; 2) the application of the API method allows controlling the optimality of the adaptive filter by the condition that the API gradient is zero at the minimum point, which corresponds to the optimal value of the parameter in the adaptive filter; 3) the calculation of the API gradient in the adaptive extended LD filter does not require significant computational costs and such a control method can be carried out in real-time. The results of the work will be applied to solving problems of joint control and identification of parameters in the class of discrete-time linear stochastic systems represented by equations in the state-space form.


1988 ◽  
Vol 42 (5) ◽  
pp. 715-721 ◽  
Author(s):  
Francis R. Verdun ◽  
Carlo Giancaspro ◽  
Alan G. Marshall

A frequency-domain Lorentzian spectrum can be derived from the Fourier transform of a time-domain exponentially damped sinusoid of infinite duration. Remarkably, it has been shown that even when such a noiseless time-domain signal is truncated to zero amplitude after a finite observation period, one can determine the correct frequency of its corresponding magnitude-mode spectral peak maximum by fitting as few as three spectral data points to a magnitude-mode Lorentzian spectrum. In this paper, we show how the accuracy of such a procedure depends upon the ratio of time-domain acquisition period to exponential damping time constant, number of time-domain data points, computer word length, and number of time-domain zero-fillings. In particular, we show that extended zero-filling (e.g., a “zoom” transform) actually reduces the accuracy with which the spectral peak position can be determined. We also examine the effects of frequency-domain random noise and roundoff errors in the fast Fourier transformation (FFT) of time-domain data of limited discrete data word length (e.g., 20 bit/word at single and double precision). Our main conclusions are: (1) even in the presence of noise, a three-point fit of a magnitude-mode spectrum to a magnitude-mode Lorentzian line shape can offer an accurate estimate of peak position in Fourier transform spectroscopy; (2) the results can be more accurate (by a factor of up to 10) when the FFT processor operates with floating-point (preferably double-precision) rather than fixed-point arithmetic; and (3) FFT roundoff errors can be made negligible by use of sufficiently large (> 16 K) data sets.


Sign in / Sign up

Export Citation Format

Share Document