arXiv subjects

Sofie Haesaert

Publications and source records attributed to Sofie Haesaert.

50 records · Page 3Linked to original sources

arXiv2022

Convex Incremental Dissipativity Analysis of Nonlinear Systems - Extended version

Efficiently computable stability and performance analysis of nonlinear systems becomes increasingly more important in practical applications. Dissipativity can express stability and performance jointly, but existing results are limited to the regions around the equilibrium points of these nonlinear systems. The incremental framework, based on the convergence of the system trajectories, removes this limitation. We investigate how stability and performance characterizations of nonlinear systems in the incremental framework are linked to dissipativity, and how general performance characterization beyond the $\mathcal{L}_2$-gain concept can be understood in this framework. This paper presents a matrix inequalities-based convex incremental dissipativity analysis for nonlinear systems via quadratic storage and supply functions. The proposed dissipativity analysis links the notions of incremental, differential, and general dissipativity. We show that through differential dissipativity, incremental and general dissipativity of the nonlinear system can be guaranteed. These results also lead to the incremental extensions of the $\mathcal{L}_2$-gain, the generalized $\mathcal{H}_2$-norm, the $\mathcal{L}_\infty$-gain, and passivity of nonlinear systems.

eess.SY↗

arXiv2022

Deep-Learning-Based Identification of LPV Models for Nonlinear Systems

The Linear Parameter-Varying (LPV) framework provides a modeling and control design toolchain to address nonlinear (NL) system behavior via linear surrogate models. Despite major research effort on LPV data-driven modeling, a key shortcoming of the current identification theory is that often the scheduling variable is assumed to be a given measured signal in the data set. In case of identifying an LPV model of a NL system, the selection of the scheduling map, which describes the relation to the measurable scheduling signal, is put on the users' shoulder, with only limited supporting tools available. This choice however greatly affects the usability and complexity of the resulting LPV model. This paper presents a deep-learning-based approach to provide joint estimation of a scheduling map and an LPV state-space model of a NL system from input-output data, and has consistency guarantees under general innovation-type noise conditions. Its efficiency is demonstrated on a realistic identification problem.

eess.SY↗

arXiv2022

Correct-by-Design Control of Parametric Stochastic Systems

This paper addresses the problem of computing controllers that are correct by design for safety-critical systems and can provably satisfy (complex) functional requirements. We develop new methods for models of systems subject to both stochastic and parametric uncertainties. We provide for the first time novel simulation relations for enabling correct-by-design control refinement, that are founded on coupling uncertainties of stochastic systems via sub-probability measures. Such new relations are essential for constructing abstract models that are related to not only one model but to a set of parameterized models. We provide theoretical results for establishing this new class of relations and the associated closeness guarantees for both linear and nonlinear parametric systems with additive Gaussian uncertainty. The results are demonstrated on a linear model and the nonlinear model of the Van der Pol Oscillator.

eess.SY↗

arXiv2022

Cautious Planning with Incremental Symbolic Perception: Designing Verified Reactive Driving Maneuvers

This work presents a step towards utilizing incrementally-improving symbolic perception knowledge of the robot's surroundings for provably correct reactive control synthesis applied to an autonomous driving problem. Combining abstract models of motion control and information gathering, we show that assume-guarantee specifications (a subclass of Linear Temporal Logic) can be used to define and resolve traffic rules for cautious planning. We propose a novel representation called symbolic refinement tree for perception that captures the incremental knowledge about the environment and embodies the relationships between various symbolic perception inputs. The incremental knowledge is leveraged for synthesizing verified reactive plans for the robot. The case studies demonstrate the efficacy of the proposed approach in synthesizing control inputs even in case of partially occluded environments.

cs.RO↗

arXiv2022

Data-Driven Predictive Control for Linear Parameter-Varying Systems

Based on the extension of the behavioral theory and the Fundamental Lemma for Linear Parameter-Varying (LPV) systems, this paper introduces a Data-driven Predictive Control (DPC) scheme capable to ensure reference tracking and satisfaction of Input-Output (IO) constraints for an unknown system under the conditions that (i) the system can be represented in an LPV form and (ii) an informative data-set containing measured IO and scheduling trajectories of the system is available. It is shown that if the data set satisfies a persistence of excitation condition, then a data-driven LPV predictor of future trajectories of the system can be constructed from the IO data set and online measured data. The approach represents the first step towards a DPC solution for nonlinear and time-varying systems due to the potential of the LPV framework to represent them. Two illustrative examples, including reference tracking control of a nonlinear system, are provided to demonstrate that the data-based LPV-DPC scheme, achieves similar performance as LPV model-based predictive control.

eess.SY↗

arXiv2022

Fundamental Lemma for Data-Driven Analysis of Linear Parameter-Varying Systems

Based on the Fundamental Lemma by Willems et al., the entire behaviour of a Linear Time-Invariant (LTI) system can be characterised by a single data sequence of the system as long the input is persistently exciting. This is an essential result for data-driven analysis and control. In this work, we aim to generalise this LTI result to Linear Parameter-Varying (LPV) systems. Based on the behavioural framework for LPV systems, we prove that one can obtain a result similar to Willems'. Based on an LPV representation, i.e., embedding, of nonlinear systems, this allows the application of the Fundamental Lemma for systems beyond the linear class.

eess.SY↗

arXiv2020

Where to Map? Iterative Rover-Copter Path Planning for Mars Exploration

In addition to conventional ground rovers, the Mars 2020 mission will send a helicopter to Mars. The copter's high-resolution data helps the rover to identify small hazards such as steps and pointy rocks, as well as providing rich textual information useful to predict perception performance. In this paper, we consider a three-agent system composed of a Mars rover, copter, and orbiter. The objective is to provide good localization to the rover by selecting an optimal path that minimizes the localization uncertainty accumulation during the rover's traverse. To achieve this goal, we quantify the localizability as a goodness measure associated with the map, and conduct a joint-space search over rover's path and copter's perceptual actions given prior information from the orbiter. We jointly address where to map by the copter and where to drive by the rover using the proposed iterative copter-rover path planner. We conducted numerical simulations using the map of Mars 2020 landing site to demonstrate the effectiveness of the proposed planner.

cs.RO↗

arXiv2018

Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems

Discrete-time stochastic systems are an essential modelling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis of control strategies are computationally hard and generally rely on the use of approximate abstractions. Building on approximate abstractions, we compute control strategies with lower- and upper-bounds for satisfying unbounded temporal logic specifications. Firstly, robust dynamic programming mappings over the abstract system are introduced to solve the control synthesis and verification problem. These mappings yield a control strategy and a unique lower bound on the satisfaction probability for temporal logic specifications that is robust to the incurred approximation errors. Secondly, upper-bounds on the satisfaction probability are quantified, and properties of the mappings are analysed and discussed. Finally, we show the implications of these results for linear stochastic dynamic systems with a continuous state space. This abstraction-based synthesis framework is shown to be able to handle infinite-horizon properties. Approximation errors expressed as deviations in the outputs of the models and as deviations in the probabilistic transitions are allowed and are quantified using approximate stochastic simulation relations.

cs.SY↗

arXiv2018

Temporal logic control of general Markov decision processes by approximate policy refinement

The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between the original model and its abstraction. We newly work with a robust satisfaction for the construction and verification of control strategies, which allows for both deviations in the outputs of the gMDPs and in the probabilistic transitions. The computation is done over the reduced or abstracted models, such that when a property is robustly satisfied on the abstract model, it is also satisfied on the original model with respect to a refined control strategy.

eess.SY↗

arXiv2017

Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes

We present a new method for statistical verification of quantitative properties over a partially unknown system with actions, utilising a parameterised model (in this work, a parametric Markov decision process) and data collected from experiments performed on the underlying system. We obtain the confidence that the underlying system satisfies a given property, and show that the method uses data efficiently and thus is robust to the amount of data available. These characteristics are achieved by firstly exploiting parameter synthesis to establish a feasible set of parameters for which the underlying system will satisfy the property; secondly, by actively synthesising experiments to increase amount of information in the collected data that is relevant to the property; and finally propagating this information over the model parameters, obtaining a confidence that reflects our belief whether or not the system parameters lie in the feasible set, thereby solving the verification problem.

cs.LG↗

arXiv2017

Control refinement for discrete-time descriptor systems: a behavioural approach via simulation relations

The analysis of industrial processes, modelled as descriptor systems, is often computationally hard due to the presence of both algebraic couplings and difference equations of high order. In this paper, we introduce a control refinement notion for these descriptor systems that enables analysis and control design over related reduced-order systems. Utilising the behavioural framework, we extend upon the standard hierarchical control refinement for ordinary systems and allow for algebraic couplings inherent to descriptor systems.

eess.SY↗

arXiv2015

Observer-based correct-by-design controller synthesis

Current state-of-the-art correct-by-design controllers are designed for full-state measurable systems. This work first extends the applicability of correct-by-design controllers to partially observable LTI systems. Leveraging 2nd order bounds we give a design method that has a quantifiable robustness to probabilistic disturbances on state transitions and on output measurements. In a case study from smart buildings we evaluate the new output-based correct-by-design controller on a physical system with limited sensor information.

eess.SY↗

arXiv2015

Data-driven and Model-based Verification: a Bayesian Identification Approach

This work develops a measurement-driven and model-based formal verification approach, applicable to systems with partly unknown dynamics. We provide a principled method, grounded on reachability analysis and on Bayesian inference, to compute the confidence that a physical system driven by external inputs and accessed under noisy measurements, verifies a temporal logic property. A case study is discussed, where we investigate the bounded- and unbounded-time safety of a partly unknown linear time invariant system.

eess.SY↗

arXiv2015

Sampling-based Approximations with Quantitative Performance for the Probabilistic Reach-Avoid Problem over General Markov Processes

This article deals with stochastic processes endowed with the Markov (memoryless) property and evolving over general (uncountable) state spaces. The models further depend on a non-deterministic quantity in the form of a control input, which can be selected to affect the probabilistic dynamics. We address the computation of maximal reach-avoid specifications, together with the synthesis of the corresponding optimal controllers. The reach-avoid specification deals with assessing the likelihood that any finite-horizon trajectory of the model enters a given goal set, while avoiding a given set of undesired states. This article newly provides an approximate computational scheme for the reach-avoid specification based on the Fitted Value Iteration algorithm, which hinges on random sample extractions, and gives a-priori computable formal probabilistic bounds on the error made by the approximation algorithm: as such, the output of the numerical scheme is quantitatively assessed and thus meaningful for safety-critical applications. Furthermore, we provide tighter probabilistic error bounds that are sample-based. The overall computational scheme is put in relationship with alternative approximation algorithms in the literature, and finally its performance is practically assessed over a benchmark case study.

eess.SY↗