Alexandre Megretski

Mardavij Roozbehani, Alexandre Megretski, Eric Feron

The 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, presence 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-resembling 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.

Mardavij Roozbehani, Alexandre Megretski, Eric Feron

The 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, presence 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-resembling 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.

Wang Zhang, Tsui-Wei Weng, Subhro Das et al. · ibm-research

Deep neural networks (DNN) have shown great capacity of modeling a dynamical system; nevertheless, they usually do not obey physics constraints such as conservation laws. This paper proposes a new learning framework named ConCerNet to improve the trustworthiness of the DNN based dynamics modeling to endow the invariant properties. ConCerNet consists of two steps: (i) a contrastive learning method to automatically capture the system invariants (i.e. conservation properties) along the trajectory observations; (ii) a neural projection layer to guarantee that the learned dynamics models preserve the learned invariants. We theoretically prove the functional relationship between the learned latent representation and the unknown system invariant function. Experiments show that our method consistently outperforms the baseline neural networks in both coordinate error and conservation metrics by a large margin. With neural network based parameterization and no dependence on prior knowledge, our method can be extended to complex and large-scale dynamics by leveraging an autoencoder.

Mark M. Tobenkin, Ian R. Manchester, Alexandre Megretski

This 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.

Omer Tanovic, Alexandre Megretski, Yan Li et al.

We consider baseband equivalent representation of transmission circuits, in the form of a nonlinear dynamical system $\mathbf S$ in discrete time (DT) defined by a series interconnection of a phase-amplitude modulator, a nonlinear dynamical system $\mathbf F$ in continuous time (CT), and an ideal demodulator. We show that when $\mathbf F$ is a CT Volterra series model, the resulting $\mathbf S$ is a series interconnection of a DT Volterra series model of same degree and memory depth, and an LTI system with special properties. The result suggests a new, non-obvious, analytically motivated structure of digital pre-compensation of analog nonlinear distortions such as those caused by power amplifiers in digital communication systems. The baseband model and the corresponding digital compensation structure readily extend to OFDM modulation. MATLAB simulation is used to verify proposed baseband equivalent model and demonstrate effectiveness of the new compensation scheme, as compared to the standard Volterra series approach.

Wang Zhang, Ziwen Ma, Subhro Das et al.

Neural networks are powerful tools in various applications, and quantifying their uncertainty is crucial for reliable decision-making. In the deep learning field, the uncertainties are usually categorized into aleatoric (data) and epistemic (model) uncertainty. In this paper, we point out that the existing popular variance attenuation method highly overestimates aleatoric uncertainty. To address this issue, we propose a new estimation method by actively de-noising the observed data. By conducting a broad range of experiments, we demonstrate that our proposed approach provides a much closer approximation to the actual data uncertainty than the standard method.

Nicholas H. Barbara, Ruigang Wang, Alexandre Megretski et al.

We study parameterizations of stabilizing nonlinear policies for learning-based control. We propose a structure based on a nonlinear version of the Youla-Kucera parameterization combined with robust neural networks such as the recurrent equilibrium network (REN). The resulting parameterizations are unconstrained, and hence can be searched over with first-order optimization methods, while always ensuring closed-loop stability by construction. We study the combination of (a) nonlinear dynamics, (b) partial observation, and (c) incremental closed-loop stability requirements (contraction and Lipschitzness). We find that with any two of these three difficulties, a contracting and Lipschitz Youla parameter always leads to contracting and Lipschitz closed loops. However, if all three hold, then incremental stability can be lost with exogenous disturbances. Instead, a weaker condition is maintained, which we call d-tube contraction and Lipschitzness. We further obtain converse results showing that the proposed parameterization covers all contracting and Lipschitz closed loops for certain classes of nonlinear systems. Numerical experiments illustrate the utility of our parameterization when learning controllers with built-in stability certificates for: (i) "economic" rewards without stabilizing effects; (ii) short training horizons; and (iii) uncertain systems.

Xinyi Chen, Udaya Ghai, Elad Hazan et al.

We study online control of an unknown nonlinear dynamical system that is approximated by a time-invariant linear system with model misspecification. Our study focuses on robustness, a measure of how much deviation from the assumed linear approximation can be tolerated by a controller while maintaining finite $\ell_2$-gain. A basic methodology to analyze robustness is via the small gain theorem. However, as an implication of recent lower bounds on adaptive control, this method can only yield robustness that is exponentially small in the dimension of the system and its parametric uncertainty. The work of Cusumano and Poolla shows that much better robustness can be obtained, but the control algorithm is inefficient, taking exponential time in the worst case. In this paper we investigate whether there exists an efficient algorithm with provable robustness beyond the small gain theorem. We demonstrate that for a fully actuated system, this is indeed attainable. We give an efficient controller that can tolerate robustness that is polynomial in the dimension and independent of the parametric uncertainty; furthermore, the controller obtains an $\ell_2$-gain whose dimension dependence is near optimal.

Mark M. Tobenkin, Ian R. Manchester, Alexandre Megretski

Model instability and poor prediction of long-term behavior are common problems when modeling dynamical systems using nonlinear "black-box" techniques. Direct optimization of the long-term predictions, often called simulation error minimization, leads to optimization problems that are generally non-convex in the model parameters and suffer from multiple local minima. In this work we present methods which address these problems through convex optimization, based on Lagrangian relaxation, dissipation inequalities, contraction theory, and semidefinite programming. We demonstrate the proposed methods with a model order reduction task for electronic circuit design and the identification of a pneumatic actuator from experiment.

Omer Tanovic, Alexandre Megretski, Yan Li et al.

We consider discrete-time (DT) systems S in which a DT input is first tranformed to a continuous-time (CT) format by phase-amplitude modulation, then modified by a non-linear CT dynamical transformation F, and finally converted back to DT output using an ideal de-modulation scheme. Assuming that F belongs to a special class of CT Volterra series models with fixed degree and memory depth, we provide a complete characterization of S as a series connection of a DT Volterra series model of fixed degree and memory depth, and an LTI system with special properties. The result suggests a new, non-obvious, analytically motivated structure of digital compensation of analog nonlinear distortions (for example, those caused by power amplifiers) in digital communication systems. Results from a MATLAB simulation are used to demonstrate effectiveness of the new compensation scheme, as compared to the standard Volterra series approach.