Ce mémoire est dédié à l’étude de la synthèse de l’estimation d’état en temps fini par une approche algébrique (les techniques développées au sein de l’équipe ALIEN) pour les systèmes linéaires à paramètres invariant dans le temps (LTI) sujets à des perturbations extérieures inconnues, les systèmes linéaires à paramètres variant dans le temps (LTV) et les systèmes linéaires à commutation en temps continu (SLC). Pour les systèmes LTI et LTV, une expression formelle de l’état en fonction des intégrales itérées des sorties et de l’entrée a été donnée. Pour les systèmes linéaires à commutation, en combinant les résultats de l’estimation d’état pour les systèmes LTI et de la détection de l’instant de commutation en temps réel présentée dans le chapitre 4, nous donnons la démarche principale de l’estimation en temps réel du mode courant et l’état continu du système. Pour ce faire, on applique certains outils mathématiques : la transformation de Laplace, les outils issus du calcul opérationnel et la théorie des distributions / This PhD thesis is dedicated to the synthesis of the state estimation in a finite time by an algebraic approach (the techniques developed within the ALIEN group) for the linear time-invariant systems (LTI) subject to the external unknown disturbances, the linear time-varying systems (LTV) and the switched linear systems (SLC) in continuous time. For the LTI and LTV systems, a formal expression of state as a function of iterated integrals of the output and the input is obtained. For switched linear systems, combining the results of state estimation for LTI systems and switch instant detection presented in Chapter 4, we give the main approach of current mode estimation and the continuous state estimation in real time. To do this, one applies some mathematical tools: Laplace transforms, the operational calculus and the theory of distribution

Orientador: Pedro Luis Dias Peres / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Elétrica e de Computação / Made available in DSpace on 2018-08-22T18:08:10Z (GMT). No. of bitstreams: 1 Agulhari_CristianoMarcos_D.pdf: 2096468 bytes, checksum: 0e762392c4ee0ab5e249ccd096ab4acf (MD5) Previous issue date: 2013 / Resumo: As principais contribuições desta tese consistem no desenvolvimento de métodos para a síntese de controladores e para a análise de estabilidade de sistemas lineares, variantes ou invariantes no tempo. Com relação aos sistemas invariantes no tempo, o objetivo é a síntese de controladores robustos de ordem reduzida para sistemas a tempo contínuo com parâmetros incertos. O método apresentado para a síntese baseia-se em uma técnica de dois estágios, em que um ganho de realimentação de estados é construído no primeiro estágio e posteriormente utilizado no segundo estágio, que fornece o controlador robusto desejado. Cada etapa consiste na resolução de condições sob a forma de desigualdades matriciais lineares. No caso de sistemas variantes no tempo, em geral, dependendo das informações disponíveis, dois modelos matemáticos podem ser utilizados. Por um lado, para sistemas cujos elementos variantes no tempo são limitados em norma, mas não são completamente conhecidos, é possível utilizar modelos dependentes de parâmetros variantes no tempo, que levam a uma representação politópica. Nesse caso, a técnica de estabilização proposta é baseada no método de dois estágios, para gerar controladores dependentes dos parâmetros. Supõe-se que os parâmetros sejam mensuráveis em tempo real, e os controladores são sintetizados de forma a serem robustos a ruídos nas medições. Por outro lado, se a dinâmica variante no tempo é conhecida, o sistema pode ser tratado diretamente sem que seja utilizado nenhum tipo de parametrização. Duas técnicas de síntese são propostas para esse caso: a construção de ganhos estabilizantes utilizando diretamente a matriz de transição de estados, e uma técnica de síntese projetada a partir de um novo critério para a verificação da estabilidade do sistema. A validade dos métodos propostos é ilustrada por meio de exemplos numéricos, que mostram a qualidade dos resultados que podem ser obtidos / Abstract: The main contributions of this thesis concern the development of methods for the stability analysis and the synthesis of controllers for linear systems, either time varying or time-invariant. Concerning time-invariant systems, the objective is the synthesis of reduced-order robust controllers for continuous-time systems with uncertain parameters. The method presented for the synthesis is based on a two-stage technique, in which a stabilizing state-feedback gain is constructed in the first stage and then applied on the second stage to search for the desired controller. Each stage consists in the resolution of conditions based on linear matrix inequalities. In the case of time-varying systems, depending on the amount of available information, two mathematical models may be used. On one hand, if the time-varying elements of the system are not entirely known, one can model the system as function of time-varying parameters, resulting on a polytopic representation. In this case, the stabilization method proposed is based on the two-stage technique, which yields parameter-dependent controllers. The parameters are supposed to be real-time measurable, and the controllers are robust with respect to noises and uncertainties on the measures. On the other hand, if the time-varying dynamics are known, the system may be directly handled without using any parameterization. Two synthesis techniques are proposed in this case: the construction of stabilizing gains by using the state transition matrix, and a synthesis technique derived from a new stability criterion for time-varying systems. The validity of the proposed methods is illustrated through numerical examples that show the efficiency of the results that can be obtained / Doutorado / Automação / Doutor em Engenharia Elétrica

No description available.

Metamodellierung im Sinne der Meta Object Facility (MOF) stellt eine Methode für die strukturelle Definition der abstrakten Syntax von Modellierungssprachen und Modellen im Softwareentwicklungsprozess dar. Um Modellsimulation und dynamische Analysen für metamodellbasierte Sprachen zu unterstützen, fehlt es an einem Kalkül zur operationalen Semantik. In dieser Arbeit wird ausgehend von MOF die Aktionssemantik MActions entwickelt, die die Definition von operationaler Semantik als Verhalten in Metamodellen ermöglicht. Diese Erweiterung geht einher mit der Beschreibung von Laufzeitmodellen sowie Zuständen und Parallelitätseigenschaften, so dass eine Verifikation von dynamischen Eigenschaften möglich wird. Zu diesem Zweck wird mit der Linear Temporal Object Constraint Language (LT-OCL) exemplarisch eine prädikatenlogische Temporallogik entwickelt, die eine metamodellunabhängige Analyse für ausführbare Modelle erlaubt. Dabei ist die Semantik von temporalen Ausdrücken über Zuständsänderungen von (aufgezeichneten) Ausführungsläufen beschrieben, wobei eine Linearisierung parallele Änderungen zusammenführt. Als weiteren Anwendungsfall der dynamischen Analyse untersuchen wir die Relation zum Verhaltensvergleich im Sinne der Bisimulationstheorie. Metamodelle, Aktionssemantik und Temporallogik werden mittels einer erweiterten Abstract State Machine (ASM) formal beschrieben und kommen in zwei Fallstudien zur Anwendung (Timed Automata und C#). / Object-oriented metamodelling as defined by the Meta Object Facility (MOF) provide a means to describe the structure of models and the abstract syntax of modelling languages at various stages in a software development process. However, MOF lacks concepts for the definition of operational semantics and there is no support for dynamic model analysis based on the semantics and abstract states of a language definition. This thesis investigates on extending the metamodelling framework with an action semantics - the MActions - to support the definition of operational semantics in metamodels and enable simulation as well as verification of dynamic properties. For this purpose, runtime models are incorporated with semantics for states, time, and properties of parallelism that allow a generic analysis solely bound to a certain metamodel definition. Furthermore, we develop the Linear Temporal Object Constraint Language (LT-OCL) to perform a dynamic analysis of execution runs based on the executable models. The semantics of this temporal predicate logic is bound to state changes of (recorded) execution traces that are linearizations of parallel changes of the runtimes model. This establishes the link to the theory of bisimulation as a second application case of dynamic analysis. Abstract State Machines (ASM) have been used to formally define the action language in conjunction with metamodels and the temporal logic. As proof of concept of the whole approach, the framework has been implemented and applied to two languages as case studies (namely Timed Automata and C#).

Title: Testing for linearity in time series Author: Martin Melicherčík Department: Department of Probability and Mathematical Statistics Supervisor: doc. RNDr. Zuzana Prášková, CSc., Department of Probability and Mathematical Statistics Abstract: In the first part of the thesis, a necessary theoretical base from time series analysis is explained, which is consequently used to formulate several tests for linearity. According to variety of approaches the theory includes wide range of knowledge from correlation and spectral analysis and introduces some basic nonlinear models. In the second part, linearity tests are described, classified and compared both theoretically and practically on simulated data from several linear and nonlinear models. At the end, some scripts and hints in R language are introduced that could be used when applying tests to real data. Keywords: linear time series, bispectrum, testing for linearity, nonlinear models

This dissertation focuses on wideband circuit design and implementation issues up to 10GHz based on the direct conversion architecture in the CMOS and SiGe BiCMOS technologies. The dissertation consists of two parts: One, implementation of a RF front-end receiver for an ultra-wideband system and, two, implementation of a local oscillation (LO) signal for a GSM/WCDMA multiband application. For emerging ultra-wideband (UWB) applications, the key active components in the RF front-end receiver were designed and implemented in 0.18um SiGe BiCMOS process. The design of LNA, which is the critical circuit block for both systems, was analyzed in terms of noise, linearity and group delay variation over an extemely wide bandwidth. Measurements are demonstrated for an energy-thrifty UWB receiver based on an MB-OFDM system covering the full FCC-allowed UWB frequency range. For multiband applications such as a GSM/WCDMA dual-band application, the design of wideband VCO and various frequency generation blocks are investigated as alternatives for implementation of direct conversion architecture. In order to reduce DC-offset and LO pulling phenomena that degrade performance in a typical direct conversion scheme, an innovative fractional LO signal generator was implemented in a standard CMOS process. A simple analysis is provided for the loop dynamics and operating range of the design as well as for the measured results of the factional LO signal generator.

Submitted by RAFAEL LOPES PAIXÃO DA SILVA (lopes1313@gmail.com) on 2018-05-02T19:05:38Z No. of bitstreams: 1 0-Thesis.pdf: 4208376 bytes, checksum: e3d171683a2ab6be4462439595e613c3 (MD5) / Approved for entry into archive by Hellen Sayuri Sato null (hellen@ift.unesp.br) on 2018-05-03T18:00:03Z (GMT) No. of bitstreams: 1 silva_rlp_me_ift.pdf: 4208376 bytes, checksum: e3d171683a2ab6be4462439595e613c3 (MD5) / Made available in DSpace on 2018-05-03T18:00:03Z (GMT). No. of bitstreams: 1 silva_rlp_me_ift.pdf: 4208376 bytes, checksum: e3d171683a2ab6be4462439595e613c3 (MD5) Previous issue date: 2018-04-03 / Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) / A modelagem matemática é uma ferramenta presente nos campos da ecologia teórica e da biologia ma- temática. Porém tais modelos que tentam reproduzir parte da dinâmica natural são limitados, o que rapidamente esgota as possibilidades de investigações e exploração dos dados. Visando contornar isso partimos para o contexto da reconstrução de espaços-de-fase, pois queremos obter outras informações sobre aquilo que temos em mãos, a observação da natureza, o dado. De posse dessa nova aplicação da teoria de sistemas dinâmicos, é nos possibilitado uma nova inferência sobre o fenômeno observado, bem como suas causas que, através do modelo estavam ocultas. A técnica do mapeamento cruzado convergente, entre atratores gerados pela reconstrução de espaços-de-fase, através da representação do espaço-de-fase original num espaço euclidiano formado pela série temporal original e seus atrasos, pos- sibilita uma inferência de causalidade mais pragmática e mais efetiva para sistemas que obedeçam uma dinâmica não-linear, o caso para as muitas séries ecológicas e biológicas de interesse. / Mathematical modeling is an almost omnipresent tool in the fields of theoretical ecology and mathe- matical biology. However, such models that try to partially reproduce the natural dynamics are limited, which quickly runs out possibilities for data-driven investigation and exploration. Aiming to circumvent this, we set out to the context of phase-space reconstruction, since we want to obtain other information on what is in hands, an observation of nature, the data. In possession of the new application of the theory of dynamical systems, are enabled to us a new type of inference on the observed phenomenon, and its causes, until now hidden by the models. The technique of convergent-cross mapping, among attractors generated by phase-space reconstruction through the representation of the original phase-space in a Euclidean space formed by the original time series and its delays, enables us a more pragmatic inference of causality and more effective for systems that obey a nonlinear dynamics, the case for many ecological and biological series of interest. / 131659/2016-2.

Passive network reconstruction is the process of learning a structured (networked) representation of a dynamic system through the use of known information about the structure of the system as well as data collected by observing the inputs into a system along with the resultant outputs. This work demonstrates an improvement on an existing network reconstruction algorithm so that the algorithm is capable of consistently and perfectly reconstructing a network when system inputs and outputs are measured without error. This work then extends the improved network reconstruction algorithm so that it functions even in the presence of noise as well as the situation where inputs into the system are unknown. Furthermore, this work demonstrates the capability of the new extended algorithms by reconstructing financial networks from stock market data, and then performing an analysis to understand the vulnerabilities of the reconstructed network to destabilization through localized attacks. The creation of these improved and extended algorithms has opened many theoretical questions, paving the way for future research into network reconstruction.

The controlled rocking heavy timber wall (CRHTW) is a high-performance structural solution that was first developed in New Zealand, mainly considering Laminated Veneer Lumber (LVL), to resist high seismic loads without sustaining structural damage. The wall responds in bending and shear to small lateral loads, and it rocks on its foundation in response to large seismic loads. In previous studies, rocking has been controlled by both energy dissipation elements and post-tensioning, and the latter returns the wall to its original position after a seismic event. The controlled rocking response avoids the need for structural repair after an earthquake, allowing for more rapid return to occupancy than in conventional structures. Whereas controlled rocking walls with supplemental energy dissipation have been studied before using LVL, this thesis proposes an adapted CRHTW in which the design and construction cost and complexity are reduced for low-to-moderate seismic hazard regions by removing supplemental energy dissipation and using cross-laminated timber (CLT) because of its positive economic and environmental potential in the North American market. Moreover, whereas previous research has focussed on direct displacement-based design procedures for CRHTWs, with limited consideration of force-based design parameters, this thesis focusses on force-based design procedures that are more common in practice. A design and analysis process is outlined for the adapted CRHTW, based on a similar methodology for controlled rocking steel braced frames. The design process includes a new proposal to minimize the design forces while still controlling peak drifts, and it also includes a new proposal for predicting the influence of the higher modes by referring to previous research on the capacity design of controlled rocking steel braced frames. Also, a numerical model is outlined, including both a baseline version and a lower-bound model based on comparison to experimental data. The numerical model is used for non-linear time-history analysis of a prototype design, confirming the expected performance of the adapted CRHTW, and the model is also used for incremental dynamic analyses of three-, six-, and nine-storey prototypes, which show a low probability of collapse. / Thesis / Master of Applied Science (MASc) / The controlled rocking heavy timber wall (CRHTW) is a high-performance structural solution that was developed to resist high seismic loads without sustaining structural damage. The wall responds in bending and shear to small lateral loads, and it rocks on its foundation in response to large seismic loads. In previous studies, rocking has been controlled by both energy dissipation elements and post-tensioning; the latter returns the wall to its original position after a seismic event. This controlled rocking behaviour mitigates structural damage and costly repairs. This thesis explores the value of an adapted CRHTW in which the design and construction costs and complexity are reduced for low-to-moderate seismic hazard regions by using post-tensioning but no supplemental energy dissipation. A design and analysis process is outlined; numerical analysis confirms the expected performance of the adapted CRHTW; and the system is shown to have a low probability of collapse.

Society relies on increasingly complex software and hardware systems, hence techniques capable of proving that they behave as expected are of great and growing interest. Formal verification procedures employ mathematically sound reasoning to address this need. This thesis proposes novel techniques for the verification and falsification of expressive specifications on timed and infinite-state systems. An expressive specification language allows the description of the intended behaviour of a system via compact formal statements written at an abstraction level that eases the review process. Falsifying a specification corresponds to identifying an execution of the system that violates the property (i.e. a witness). The capability of identifying witnesses is a key feature in the iterative refinement of the design of a system, since it provides a description of how a certain error can occur. The designer can analyse the witness and take correcting actions by refining either the description of the system or its specification. The contribution of this thesis is twofold. First, we propose a semantics for Metric Temporal Logic that considers four different models of time (discrete, dense, super-discrete and super-dense). We reduce its verification problem to finding an infinite fair execution (witness) for an infinite-state system with discrete time. Second, we define a novel SMT-based algorithm to identify such witnesses. The algorithm employs a general representation of such executions that is both informative to the designer and provides sufficient structure to automate the search of a witness. We apply the proposed techniques to benchmarks taken from software, infinite-state, timed and hybrid systems. The experimental results highlight that the proposed approaches compete and often outperform specific (application tailored) techniques currently used in the state of the art.