Searcharxiv⌕ Search

arXiv subjects

Assalé Adjé

Publications and source records attributed to Assalé Adjé.

17 recordsLinked to original sources
arXiv2026

Extensions of $\mathcal{KL}$ and Lyapunov Functions for Discrete-time Dynamical System Peaks Analysis

In this paper, we extend two classes of functions involved in asymptotic stability analyses. The goal of this extension is to study a maximization problem on the reachable values of a discrete-time dynamical system. This specific maximization problem is called a peak computation problem. The problem consists in finding a pair composed of an initial state and a time that maximizes a given function over states. The paper focuses on the time component of the optimal solution, which is an integer as the time is discrete. We apply a method developed in previous papers to compute an upper bound of the greatest index maximizer of a real sequence. The method uses a formula based on a pair of a strictly increasing and continuous function on [0,1] and a convergent geometric sequence that provides an upper bound of the analyzed sequence. This pair is proven to exist. However, in practice, the computation cannot be done in a general setting. In this paper, we developed two alternative methods. The first uses discontinuous and non-strictly increasing/decreasing KL-like functions. We prove that the existence of a KL-like upper bound is equivalent to the existence of a pair of a strictly increasing and continuous function on [0,1] and a convergent geometric sequence. The construction of a strictly increasing continuous function from a KL-like function requires an extension of the famous Sontag's lemma. Finally, we construct a new type of Lyapunov function that is well designed for our peak computation problem. These Lyapunov-like functions are suitable as we establish an equivalence theorem between the existence of a Lyapunov-like function and that of a pair of a strictly increasing and continuous function on [0,1] and a convergent geometric sequence. The construction of a Lyapunov-like function is inspired by the Yoshizawa construction of Lyapunov functions.

math.OC↗
arXiv2026

On the Maximization of Real Sequences

In this paper, we study a maximization problem on real sequences. More precisely, for a given sequence, we are interested in computing the supremum of the sequence and an index for which the associated term is maximal. We propose a general methodology to solve this maximization problem. The method is based on upper approximations constructed from pairs of eventually decreasing sequences of strictly increasing continuous functions on $[0,1]$ and scalars in $(0,1)$. Then, we can associate integers with these pairs using the inverse of the functions on $[0,1]$. We prove that such pairs always exist, and one provides the index maximizer. In general, such pairs provide an upper bound for the greatest maximizer of the sequence. Finally, we apply the methodology to concrete examples, including famous sequences such as the logistic, Fibonacci, and Syracuse sequences. We also apply our techniques to norm-based peak computation problems on discrete-time linear systems.

math.OC↗
arXiv2025

$\mathcal{KL}$ and Lyapunov Approaches for Discrete-time Peak Computation Problems

In this paper, we propose a method to solve discrete-time peak computation problems (DPCPs for short). DPCPs are optimization problems that consist of maximizing a function over the reachable values set of a discrete-time dynamical system. The optimal value of a DPCP can be rewritten as the supremum of the sequence of optimal values. Previous results provide general techniques for computing the supremum of a real sequence from a well-chosen pair of a strictly increasing continuous function on [0,1] and a positive scalar in (0,1). In this paper, we exploit the specific structure of the optimal value of the DPCP to construct such a pair from classical tools from stability theory: $\mathcal{KL}$ certificate and Lyapunov functions.

math.OC↗
arXiv2024

A Parametric Optimization Point-Of-View of Comparison Functions

In this paper, we obtain results about the positive definiteness, the continuity and the level-boundedness of two optimal value functions of specific parametric optimization problems. Those two optimization problems are generalizations of special functions called comparison functions which arise in dynamical systems stability theory.

math.OC↗
arXiv2023

Quadratic Maximization of Reachable Values of Stable Discrete-Time Affine Systems

In this paper, we solve a maximization problem where the objective function is quadratic and the constraints set is the reachable values set of a stable discrete-time affine system. This problem is equivalent to solve an infinite number of linearly constrained quadratic maximization programs. To solve exactly and in finite time this problem, we have to safely extract a finite number of them. Safely means that we must guarantee that the optimal solution can be found within this extracted family. This family has to be the smallest possible. Therefore, we construct an integer-valued function defined on the solutions of the discrete Lyapunov equation. Those integers represent overapproximations of the number of quadratic programs to solve to obtain an optimal solution of our specific maximization problem. The integer-valued function is minimized in order to get the smallest possible overapproximation. The method proposed in the paper is first illustrated on a class of nondiagonalizable systems of dimension two and finally experimented on randomly generated instances of the problem.

math.OC↗
arXiv2023

Set-based value operators for non-stationary Markovian environments

This paper analyzes finite state Markov Decision Processes (MDPs) with uncertain parameters in compact sets and re-examines results from robust MDP via set-based fixed point theory. To this end, we generalize the Bellman and policy evaluation operators to contracting operators on the value function space and denote them as \emph{value operators}. We lift these value operators to act on \emph{sets} of value functions and denote them as \emph{set-based value operators}. We prove that the set-based value operators are \emph{contractions} in the space of compact value function sets. Leveraging insights from set theory, we generalize the rectangularity condition in classic robust MDP literature to a containment condition for all value operators, which is weaker and can be applied to a larger set of parameter-uncertain MDPs and contracting operators in dynamic programming. We prove that both the rectangularity condition and the containment condition sufficiently ensure that the set-based value operator's fixed point set contains its own extrema elements. For convex and compact sets of uncertain MDP parameters, we show equivalence between the classic robust value function and the supremum of the fixed point set of the set-based Bellman operator. Under dynamically changing MDP parameters in compact sets, we prove a set convergence result for value iteration, which otherwise may not converge to a single value function. Finally, we derive novel guarantees for probabilistic path-planning problems in planet exploration and stratospheric station-keeping.

cs.LG↗
arXiv2021

Fast and Efficient Bit-Level Precision Tuning

In this article, we introduce a new technique for precision tuning. This problem consists of finding the least data types for numerical values such that the result of the computation satisfies some accuracy requirement. State of the art techniques for precision tuning use a try and fail approach. They change the data types of some variables of the program and evaluate the accuracy of the result. Depending on what is obtained, they change more or less data types and repeat the process. Our technique is radically different. Based on semantic equations, we generate an Integer Linear Problem (ILP) from the program source code. Basically, this is done by reasoning on the most significant bit and the number of significant bits of the values which are integer quantities. The integer solution to this problem, computed in polynomial time by a (real) linear programming solver, gives the optimal data types at the bit level. A finer set of semantic equations is also proposed which does not reduce directly to an ILP problem. So we use policy iteration to find the solution. Both techniques have been implemented and we show that our results encompass the results of state of the art tools.

cs.PL↗
arXiv2020

Quadratic Maximization over the Reachable Values Set of a Convergent Discrete-time Affine System : The diagonalizable case

In this paper, we solve a maximization problem where the objective function is quadratic and convex or concave and the constraints set is the reachable value set of a convergent discrete-time affine system. Moreover, we assume that the matrix defining the system is diagonalizable. The difficulty of the problem lies in the infinite sequence to handle in the constraint set. Equivalently, the problem requires to solve an infinite number of quadratic programs. Therefore, the main idea is to extract a finite of them and to guarantee that the resolution of the extracted problems provides the optimal value and a maximizer for the initial problem. The number of quadratic programs to solve has to be the smallest possible. Actually, we construct a family of integers that over-approximate the exact number of quadratic programs to solve using basic ideas of linear algebra. This family of integers is used in the final algorithm. A new computation of an integer of the family within the algorithm ensures a reduction of the number of loop iterations. The method proposed in the paper is illustrated on small academic examples. Finally, the algorithm is experimented on randomly generated instances of the problem.

math.OC↗
arXiv2020

Fixed Points of the Set-Based Bellman Operator

Motivated by uncertain parameters encountered in Markov decision processes (MDPs), we study the effect of parameter uncertainty on Bellman operator-based methods. Specifically, we consider a family of MDPs where the cost parameters are from a given compact set. We then define a Bellman operator acting on an input set of value functions to produce a new set of value functions as the output under all possible variations in the cost parameters. Finally we prove the existence of a fixed point of this set-based Bellman operator by showing that it is a contractive operator on a complete metric space.

math.OC↗
arXiv2016

A Sums-of-Squares Extension of Policy Iterations

In order to address the imprecision often introduced by widening operators in static analysis, policy iteration based on min-computations amounts to considering the characterization of reachable value set of a program as an iterative computation of policies, starting from a post-fixpoint. Computing each policy and the associated invariant relies on a sequence of numerical optimizations. While the early research efforts relied on linear programming (LP) to address linear properties of linear programs, the current state of the art is still limited to the analysis of linear programs with at most quadratic invariants, relying on semidefinite programming (SDP) solvers to compute policies, and LP solvers to refine invariants. We propose here to extend the class of programs considered through the use of Sums-of-Squares (SOS) based optimization. Our approach enables the precise analysis of switched systems with polynomial updates and guards. The analysis presented has been implemented in Matlab and applied on existing programs coming from the system control literature, improving both the range of analyzable systems and the precision of previously handled ones.

cs.LO↗
arXiv2016

Overapproximating the Reachable Values Set of Piecewise Affine Systems Coupling Policy Iterations with Piecewise Quadratic Lyapunov Functions

We have recently constructed a piecewise quadratic Lyapunov function to prove the boundedness of the reachable values set of piecewise affine discrete-time systems. The method developed also provided an overapproximation of the reachable values set. In this paper, we refine the latter overapproximation extending previous works combining policy iterations with quadratic Lyapunov functions.

math.OC↗
arXiv2015

Quadratic Zonotopes:An extension of Zonotopes to Quadratic Arithmetics

Affine forms are a common way to represent convex sets of $\mathbb{R}$ using a base of error terms $ε\in [-1, 1]^m$. Quadratic forms are an extension of affine forms enabling the use of quadratic error terms $ε_i ε_j$. In static analysis, the zonotope domain, a relational abstract domain based on affine forms has been used in a wide set of settings, e.g. set-based simulation for hybrid systems, or floating point analysis, providing relational abstraction of functions with a cost linear in the number of errors terms. In this paper, we propose a quadratic version of zonotopes. We also present a new algorithm based on semi-definite programming to project a quadratic zonotope, and therefore quadratic forms, to intervals. All presented material has been implemented and applied on representative examples.

cs.LO↗
arXiv2015

Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization

While abstract interpretation is not theoretically restricted to specific kinds of properties, it is, in practice, mainly developed to compute linear over-approximations of reachable sets, aka. the collecting semantics of the program. The verification of user-provided properties is not easily compatible with the usual forward fixpoint computation using numerical abstract domains. We propose here to rely on sums-of-squares programming to characterize a property-driven polynomial invariant. This invariant generation can be guided by either boundedness, or in contrary, a given zone of the state space to avoid. While the target property is not necessarily inductive with respect to the program semantics, our method identifies a stronger inductive polynomial invariant using numerical optimization. Our method applies to a wide set of programs: a main while loop composed of a disjunction (if-then-else) of polynomial updates e.g. piecewise polynomial controllers. It has been evaluated on various programs.

cs.LO↗
arXiv2014

Polynomial Template Generation using Sum-of-Squares Programming

Template abstract domains allow to express more interesting properties than classical abstract domains. However, template generation is a challenging problem when one uses template abstract domains for program analysis. In this paper, we relate template generation with the program properties that we want to prove. We focus on one-loop programs with nested conditional branches. We formally define the notion of well-representative template basis with respect to such programs and a given property. The definition relies on the fact that template abstract domains produce inductive invariants. We show that these invariants can be obtained by solving certain systems of functional inequalities. Then, such systems can be strengthened using a hierarchy of sum-of-squares (SOS) problems when we consider programs written in polynomial arithmetic. Each step of the SOS hierarchy can possibly provide a solution which in turn yields an invariant together with a certificate that the desired property holds. The interest of this approach is illustrated on nontrivial program examples in polynomial arithmetic.

cs.LO↗
arXiv2013

Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs

The problem of computing the smallest fixed point of an order-preserving map arises in the study of zero-sum positive stochastic games. It also arises in static analysis of programs by abstract interpretation. In this context, the discount rate may be negative. We characterize the minimality of a fixed point in terms of the nonlinear spectral radius of a certain semidifferential. We apply this characterization to design a policy iteration algorithm, which applies to the case of finite state and action spaces. The algorithm returns a locally minimal fixed point, which turns out to be globally minimal when the discount rate is nonnegative.

math.OC↗
arXiv2012

Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis

We introduce a new domain for finding precise numerical invariants of programs by abstract interpretation. This domain, which consists of level sets of non-linear functions, generalizes the domain of linear "templates" introduced by Manna, Sankaranarayanan, and Sipma. In the case of quadratic templates, we use Shor's semi-definite relaxation to derive computable yet precise abstractions of semantic functionals, and we show that the abstract fixpoint equation can be solved accurately by coupling policy iteration and semi-definite programming. We demonstrate the interest of our approach on a series of examples (filters, integration schemes) including a degenerate one (symplectic scheme).

cs.LO↗