-
Certified Inductive Synthesis for Online Mixed-Integer Optimization
Authors:
Marco Zamponi,
Emilio Incerto,
Daniele Masti,
Mirco Tribastone
Abstract:
In fields such as autonomous and safety-critical systems, online optimization plays a crucial role in control and decision-making processes, often requiring the integration of continuous and discrete variables. These tasks are frequently modeled as mixed-integer programming (MIP) problems, where feedback data are incorporated as parameters. However, solving MIPs within strict time constraints is c…
▽ More
In fields such as autonomous and safety-critical systems, online optimization plays a crucial role in control and decision-making processes, often requiring the integration of continuous and discrete variables. These tasks are frequently modeled as mixed-integer programming (MIP) problems, where feedback data are incorporated as parameters. However, solving MIPs within strict time constraints is challenging due to their $\mathcal{NP}$-complete nature. A promising solution to this challenge involves leveraging the largely invariant structure of these problems to perform most computations offline, thus enabling efficient online solving even on platforms with limited hardware capabilities. In this paper we present a novel implementation of this strategy that uses counterexample-guided inductive synthesis to split the MIP solution process into two stages. In the offline phase, we construct a mapping that provides feasible assignments for binary variables based on parameter values within a specified range. In the online phase, we solve the remaining continuous part of the problem by fixing the binary variables to the values predicted by this mapping. Our numerical evaluation demonstrates the efficiency and solution quality of this approach compared to standard mixed-integer solvers, highlighting its potential for real-time applications in resource-constrained environments.
△ Less
Submitted 14 March, 2025;
originally announced March 2025.
-
Proper Lumping for Positive Bilinear Control Systems
Authors:
Antonio Jiménez-Pastor,
Daniele Toller,
Mirco Tribastone,
Max Tschaikowski,
Andrea Vandin
Abstract:
Positive systems naturally arise in situations where the model tracks physical quantities. Although the linear case is well understood, analysis and controller design for nonlinear positive systems remain challenging. Model reduction methods can help tame this problem. Here we propose a notion of model reduction for a class of positive bilinear systems with (bounded) matrix and exogenous controls.…
▽ More
Positive systems naturally arise in situations where the model tracks physical quantities. Although the linear case is well understood, analysis and controller design for nonlinear positive systems remain challenging. Model reduction methods can help tame this problem. Here we propose a notion of model reduction for a class of positive bilinear systems with (bounded) matrix and exogenous controls. Our reduction, called proper positive lumping, aggregates the original system such that states of the corresponding reduced model represent non-negative linear combinations of original state variables. We prove a characterization result showing that the reductions by proper positive lumping are exactly those preserving the optimality of a suitable class of value functions. Moreover, we provide an efficient polynomial-time algorithm for the computation of the minimal lumping. We numerically evaluate our approach by applying it to a number of benchmark case studies.
△ Less
Submitted 14 December, 2023;
originally announced December 2023.
-
Certification of the proximal gradient method under fixed-point arithmetic for box-constrained QP problems
Authors:
Pablo Krupa,
Omar Inverso,
Mirco Tribastone,
Alberto Bemporad
Abstract:
In safety-critical applications that rely on the solution of an optimization problem, the certification of the optimization algorithm is of vital importance. Certification and suboptimality results are available for a wide range of optimization algorithms. However, a typical underlying assumption is that the operations performed by the algorithm are exact, i.e., that there is no numerical error du…
▽ More
In safety-critical applications that rely on the solution of an optimization problem, the certification of the optimization algorithm is of vital importance. Certification and suboptimality results are available for a wide range of optimization algorithms. However, a typical underlying assumption is that the operations performed by the algorithm are exact, i.e., that there is no numerical error during the mathematical operations, which is hardly a valid assumption in a real hardware implementation. This is particularly true in the case of fixed-point hardware, where computational inaccuracies are not uncommon. This article presents a certification procedure for the proximal gradient method for box-constrained QP problems implemented in fixed-point arithmetic. The procedure provides a method to select the minimal fractional precision required to obtain a certain suboptimality bound, indicating the maximum number of iterations of the optimization method required to obtain it. The procedure makes use of formal verification methods to provide arbitrarily tight bounds on the suboptimality guarantee. We apply the proposed certification procedure on the implementation of a non-trivial model predictive controller on 32-bit fixed-point hardware.
△ Less
Submitted 5 December, 2023; v1 submitted 29 March, 2023;
originally announced March 2023.
-
Spatial Fluid Limits for Stochastic Mobile Networks
Authors:
Max Tschaikowski,
Mirco Tribastone
Abstract:
We consider Markov models of large-scale networks where nodes are characterized by their local behavior and by a mobility model over a two-dimensional lattice. By assuming random walk, we prove convergence to a system of partial differential equations (PDEs) whose size depends neither on the lattice size nor on the population of nodes. This provides a macroscopic view of the model which approximat…
▽ More
We consider Markov models of large-scale networks where nodes are characterized by their local behavior and by a mobility model over a two-dimensional lattice. By assuming random walk, we prove convergence to a system of partial differential equations (PDEs) whose size depends neither on the lattice size nor on the population of nodes. This provides a macroscopic view of the model which approximates discrete stochastic movements with continuous deterministic diffusions. We illustrate the practical applicability of this result by modeling a network of mobile nodes with on/off behavior performing file transfers with connectivity to 802.11 access points. By means of an empirical validation against discrete-event simulation we show high quality of the PDE approximation even for low populations and coarse lattices. In addition, we confirm the computational advantage in using the PDE limit over a traditional ordinary differential equation limit where the lattice is modeled discretely, yielding speed-ups of up to two orders of magnitude.
△ Less
Submitted 26 April, 2016; v1 submitted 17 July, 2013;
originally announced July 2013.
