arXiv subjects

Iury Bessa

Publications and source records attributed to Iury Bessa.

15 recordsLinked to original sources

arXiv2026

Dynamic Event-Triggered Control of Discrete-Time Nonlinear Systems based on Difference-Algebraic Representations

This paper addresses the dynamic event-triggered control for a class of discrete-time nonlinear systems described by a difference-algebraic representation (DAR), using a gain-scheduled controller. An outstanding aspect of the proposed method is the incorporation of information about the system's nonlinearities into the control law and the trigger function. The proposed event-triggered mechanism also incorporates information on the asynchronous terms induced by the event-based sampling. All these ingredients enable the derivation of a less conservative co-design condition for the simultaneous design of the gain-scheduled control law and the dynamic triggering mechanism to ensure the asymptotic stability of the closed-loop system. An estimate of the region of attraction of the origin of the closed-loop system is obtained to guarantee the closed-loop system's operation within the domain of validity of the DAR. Then, an optimization problem is formulated to reduce the number of events and enlarge the estimated region of attraction. Finally, the effectiveness of the proposed condition is illustrated by a numerical example.

eess.SY↗

arXiv2025

Unit-Vector Control Design under Saturating Actuators

This paper deals with unit vector control design for multivariable polytopic uncertain systems under saturating actuators. For that purpose, we propose LMI-based conditions to design the unit vector control gain such that the origin of the closed-loop system is finite-time stable. Moreover, an optimization problem is provided to obtain an enlarged estimate of the region of attraction of the equilibrium point for the closed-loop system, where the convergence of trajectories is ensured even in the presence of saturation functions. Numerical simulations illustrate the effectiveness of the proposed approach.

math.OC↗

arXiv2024

A Systematic LMI Approach to Design Multivariable Sliding Mode Controllers

This paper deals with sliding mode control for multivariable polytopic uncertain systems. We provide systematic procedures to design variable structure controllers (VSCs) and unit-vector controllers (UVCs). Based on suitable representations for the closed-loop system, we derive sufficient conditions in the form of linear matrix inequalities (LMIs) to design the robust sliding mode controllers such that the origin of the closed-loop system is globally stable in finite time. Moreover, by noticing that the reaching time depends on the initial condition and the decay rate, we provide convex optimization problems to design robust controllers by considering the minimization of the reaching time associated with a given set of initial conditions. Two examples illustrate the effectiveness of the proposed approaches.

math.OC↗

arXiv2023

Towards Global Neural Network Abstractions with Locally-Exact Reconstruction

Neural networks are a powerful class of non-linear functions. However, their black-box nature makes it difficult to explain their behaviour and certify their safety. Abstraction techniques address this challenge by transforming the neural network into a simpler, over-approximated function. Unfortunately, existing abstraction techniques are slack, which limits their applicability to small local regions of the input domain. In this paper, we propose Global Interval Neural Network Abstractions with Center-Exact Reconstruction (GINNACER). Our novel abstraction technique produces sound over-approximation bounds over the whole input domain while guaranteeing exact reconstructions for any given local input. Our experiments show that GINNACER is several orders of magnitude tighter than state-of-the-art global abstraction techniques, while being competitive with local ones.

cs.LG↗

arXiv2022

CEG4N: Counter-Example Guided Neural Network Quantization Refinement

Neural networks are essential components of learning-based software systems. However, their high compute, memory, and power requirements make using them in low resources domains challenging. For this reason, neural networks are often quantized before deployment. Existing quantization techniques tend to degrade the network accuracy. We propose Counter-Example Guided Neural Network Quantization Refinement (CEG4N). This technique combines search-based quantization and equivalence verification: the former minimizes the computational requirements, while the latter guarantees that the network's output does not change after quantization. We evaluate CEG4N~on a diverse set of benchmarks, including large and small networks. Our technique successfully quantizes the networks in our evaluation while producing models with up to 72% better accuracy than state-of-the-art techniques.

cs.LG↗

arXiv2021

QNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking

QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achieved by employing state-of-the-art software model checking (SMC) techniques. It translates the implementation of neural networks to a decidable fragment of first-order logic based on satisfiability modulo theories (SMT). The effects of fixed- and floating-point operations are represented through direct implementations given a hardware-determined precision. Furthermore, QNNVerifier allows to specify bespoke safety properties and verify the resulting model with different verification strategies (incremental and k-induction) and SMT solvers. Finally, QNNVerifier is the first tool that combines invariant inference via interval analysis and discretization of non-linear activation functions to speed up the verification of neural networks by orders of magnitude. A video presentation of QNNVerifier is available at https://youtu.be/7jMgOL41zTY

cs.AI↗

arXiv2021

Verifying Quantized Neural Networks using SMT-Based Model Checking

Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis. However, concerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks. These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of mathematical operations and thus introduce additional quantization errors. Here, we develop and evaluate a novel symbolic verification framework using software model checking (SMC) and satisfiability modulo theories (SMT) to check for vulnerabilities in ANNs. More specifically, we propose several ANN-related optimizations for SMC, including invariant inference via interval analysis, slicing, expression simplifications, and discretization of non-linear activation functions. With this verification framework, we can provide formal guarantees on the safe behavior of ANNs implemented both in floating- and fixed-point arithmetic. In this regard, our verification approach was able to verify and produce adversarial examples for $52$ test cases spanning image classification and general machine learning applications. Furthermore, for small- to medium-sized ANN, our approach completes most of its verification runs in minutes. Moreover, in contrast to most state-of-the-art methods, our approach is not restricted to specific choices regarding activation functions and non-quantized representations. Our experiments show that our approach can analyze larger ANN implementations and substantially reduce the verification time compared to state-of-the-art techniques that use SMT solving.

cs.LG↗

arXiv2021

Incremental Learning and State-Space Evolving Fuzzy Control of Nonlinear Time-Varying Systems with Unknown Model

We present a method for incremental modeling and time-varying control of unknown nonlinear systems. The method combines elements of evolving intelligence, granular machine learning, and multi-variable control. We propose a State-Space Fuzzy-set-Based evolving Modeling (SS-FBeM) approach. The resulting fuzzy model is structurally and parametrically developed from a data stream with focus on memory and data coverage. The fuzzy controller also evolves, based on the data instances and fuzzy model parameters. Its local gains are redesigned in real-time -- whenever the corresponding local fuzzy models change -- from the solution of a linear matrix inequality problem derived from a fuzzy Lyapunov function and bounded input conditions. We have shown one-step prediction and asymptotic stabilization of the Henon chaos.

eess.SY↗

arXiv2021

Evolving Fuzzy System Applied to Battery Charge Capacity Prediction for Fault Prognostics

This paper addresses the use of data-driven evolving techniques applied to fault prognostics. In such problems, accurate predictions of multiple steps ahead are essential for the Remaining Useful Life (RUL) estimation of a given asset. The fault prognostics' solutions must be able to model the typical nonlinear behavior of the degradation processes of these assets, and be adaptable to each unit's particularities. In this context, the Evolving Fuzzy Systems (EFSs) are models capable of representing such behaviors, in addition of being able to deal with non-stationary behavior, also present in these problems. Moreover, a methodology to recursively track the model's estimation error is presented as a way to quantify uncertainties that are propagated in the long-term predictions. The well-established NASA's Li-ion batteries data set is used to evaluate the models. The experiments indicate that generic EFSs can take advantage of both historical and stream data to estimate the RUL and its uncertainty.

eess.SY↗

arXiv2020

Incremental Verification of Fixed-Point Implementations of Neural Networks

Implementations of artificial neural networks (ANNs) might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are barely interpretable. Here, we develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference, to obtain adversarial cases and validate coverage methods in a multi-layer perceptron (MLP). We exploit incremental BMC based on interval analysis to compute boundaries from a neuron's input. Then, the latter are propagated to effectively find a neuron's output since it is the input of the next one. This paper describes the first bit-precise symbolic verification framework to reason over actual implementations of ANNs in CUDA, based on invariant inference, therefore providing further guarantees about finite-precision arithmetic and its rounding errors, which are routinely ignored in the existing literature. We have implemented the proposed approach on top of the efficient SMT-based bounded model checker (ESBMC), and its experimental results show that it can successfully verify safety properties, in actual implementations of ANNs, and generate real adversarial cases in MLPs. Our approach was able to verify and produce adversarial examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods. Although our verification time is higher than existing approaches, our methodology can consider fixed-point implementation aspects that are disregarded by the state-of-the-art verification methodologies.

cs.LO↗

arXiv2017

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems (Tool Demonstration)

An automated counterexample reproducibility tool based on MATLAB is presented, called DSValidator, with the goal of reproducing counterexamples that refute specific properties related to digital systems. We exploit counterexamples generated by the Digital System Verifier (DSVerifier), which is a model checking tool based on satisfiability modulo theories for digital systems. DSValidator reproduces the execution of a digital system, relating its input with the counterexample, in order to establish trust in a verification result. We show that DSValidator can validate a set of intricate counterexamples for digital controllers used in a real quadrotor attitude system within seconds and also expose incorrect verification results in DSVerifier. The resulting toolbox leverages the potential of combining different verification tools for validating digital systems via an exchangeable counterexample format.

eess.SY↗

arXiv2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants

We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitalization of signals by the controller. Our approach has two stages, leveraging counterexample guided inductive synthesis (CEGIS) and reachability analysis. CEGIS synthesizes a static feedback controller that stabilizes the system under restrictions given by the safety of the reach space. Safety is verified either via BMC or abstract acceleration; if the verification step fails, we refine the controller by generalizing the counterexample. We synthesize stable and safe controllers for intricate physical plant models from the digital control literature.

eess.SY↗

arXiv2017

Verifying Digital Systems with MATLAB

A MATLAB toolbox is presented, with the goal of checking occurrences of design errors typically found in fixed-point digital systems, considering finite word-length effects. In particular, the present toolbox works as a front-end to a recently introduced verification tool, known as Digital-System Verifier, and checks overflow, limit cycle, quantization, stability, and minimum phase errors, in digital systems represented by transfer-function and state-space equations. It provides a command-line version, with simplified access to specific functions, and a graphical-user interface, which was developed as a MATLAB application. The resulting toolbox is important for the verification community, since it shows the applicability of verification to real-world systems.

eess.SY↗

arXiv2017

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counter-example guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes.

eess.SY↗

arXiv2014

SMT-Based Bounded Model Checking of Fixed-Point Digital Controllers

Digital controllers have several advantages with respect to their flexibility and design's simplicity. However, they are subject to problems that are not faced by analog controllers. In particular, these problems are related to the finite word-length implementation that might lead to overflows, limit cycles, and time constraints in fixed-point processors. This paper proposes a new method to detect design's errors in digital controllers using a state-of-the art bounded model checker based on satisfiability modulo theories. The experiments with digital controllers for a ball and beam plant demonstrate that the proposed method can be very effective in finding errors in digital controllers than other existing approaches based on traditional simulations tools.

eess.SY↗