اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدPolyAR: A Highly Parallelizable Solver For Polynomial Inequality Constraints Using Convex Abstraction Refinement
93
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Numerical tools for constraints solving are a cornerstone to control verification problems. This is evident by the plethora of research that uses tools like linear and convex programming for the design of control systems. Nevertheless, the capability of linear and convex programming is limited and is not adequate to reason about general nonlinear polynomials constraints that arise naturally in the design of nonlinear systems. This limitation calls for new solvers that are capable of utilizing the power of linear and convex programming to reason about general multivariate polynomials. In this paper, we propose PolyAR, a highly parallelizable solver for polynomial inequality constraints. PolyAR provides several key contributions. First, it uses convex relaxations of the problem to accelerate the process of finding a solution to the set of the non-convex multivariate polynomials. Second, it utilizes an iterative convex abstraction refinement process which aims to prune the search space and identify regions for which the convex relaxation fails to solve the problem. Third, it allows for a highly parallelizable usage of off-the-shelf solvers to analyze the regions in which the convex relaxation failed to provide solutions. We compared the scalability of PolyAR against Z3 8.9 and Yices 2.6 on control designing problems. Finally, we demonstrate the performance of PolyAR on designing switching signals for continuous-time linear switching systems.
قيم البحث
اقرأ أيضاً
Motivated by the need for decentralized learning, this paper aims at designing a distributed algorithm for solving nonconvex problems with general linear constraints over a multi-agent network. In the considered problem, each agent owns some local in
formation and a local variable for jointly minimizing a cost function, but local variables are coupled by linear constraints. Most of the existing methods for such problems are only applicable for convex problems or problems with specific linear constraints. There still lacks a distributed algorithm for such problems with general linear constraints and under nonconvex setting. In this paper, to tackle this problem, we propose a new algorithm, called proximal dual consensus (PDC) algorithm, which combines a proximal technique and a dual consensus method. We build the theoretical convergence conditions and show that the proposed PDC algorithm can converge to an $epsilon$-Karush-Kuhn-Tucker solution within $mathcal{O}(1/epsilon)$ iterations. For computation reduction, the PDC algorithm can choose to perform cheap gradient descent per iteration while preserving the same order of $mathcal{O}(1/epsilon)$ iteration complexity. Numerical results are presented to demonstrate the good performance of the proposed algorithms for solving a regression problem and a classification problem over a network where agents have only partial observations of data features.
In this paper, we propose an incremental abstraction method for dynamically over-approximating nonlinear systems in a bounded domain by solving a sequence of linear programs, resulting in a sequence of affine upper and lower hyperplanes with expandin
g operating regions. Although the affine abstraction problem can be solved offline using a single linear program, existing approaches suffer from a computation space complexity that grows exponentially with the state dimension. Hence, the motivation for incremental abstraction is to reduce the space complexity for high-dimensional systems, but at the cost of yielding potentially worse abstractions/overapproximations. Specifically, we start with an operating region that is a subregion of the state space and compute two affine hyperplanes that bracket the nonlinear function locally. Then, by incrementally expanding the operating region, we dynamically update the two affine hyperplanes such that we eventually yield hyperplanes that are guaranteed to over-approximate the nonlinear system over the entire domain. Finally, the effectiveness of the proposed approach is demonstrated using numerical examples of high-dimensional nonlinear systems.
Partially Observable Markov Decision Process (POMDP) is widely used to model probabilistic behavior for complex systems. Compared with MDPs, POMDP models a system more accurate but solving a POMDP generally takes exponential time in the size of its s
tate space. This makes the formal verification and synthesis problems much more challenging for POMDPs, especially when multiple system components are involved. As a promising technique to reduce the verification complexity, the abstraction method tries to find an abstract system with a smaller state space but preserves enough properties for the verification purpose. While abstraction based verification has been explored extensively for MDPs, in this paper, we present the first result of POMDP abstraction and its refinement techniques. The main idea follows the counterexample-guided abstraction refinement (CEGAR) framework. Starting with a coarse guess for the POMDP abstraction, we iteratively use counterexamples from formal verification to refine the abstraction until the abstract system can be used to infer the verification result for the original POMDP. Our main contributions have two folds: 1) we propose a novel abstract system model for POMDP and a new simulation relation to capture the partial observability then prove the preservation on a fragment of Probabilistic Computation Tree Logic (PCTL); 2) to find a proper abstract system that can prove or disprove the satisfaction relation on the concrete POMDP, we develop a novel refinement algorithm. Our work leads to a sound and complete CEGAR framework for POMDP.
This paper presents a sparse solver based on the alternating direction method of multipliers algorithm for a linear model predictive control (MPC) formulation in which the terminal state is constrained to a given ellipsoid. The motivation behind this
solver is to substitute the typical polyhedral invariant set used as a terminal constraint in many nominal and robust linear MPC formulations with an invariant set in the form of an ellipsoid, which is (typically) much easier to compute and results in an optimization problem with significantly fewer constraints, even for average-sized systems. However, this optimization problem is no longer the quadratic programming problem found in most linear MPC approaches, thus meriting the development of a tailored solver. The proposed solver is suitable for its use in embedded systems, since it is sparse, has a small memory footprint and requires no external libraries. We show the results of its implementation in an embedded system to control a simulated multivariable plant, comparing it against other alternatives.
Optimized Pulse Patterns (OPPs) are gaining increasing popularity in the power electronics community over the well-studied pulse width modulation due to their inherent ability to provide the switching instances that optimize current harmonic distorti
ons. In particular, the OPP problem minimizes current harmonic distortions under a cardinality constraint on the number of switching instances per fundamental wave period. The OPP problem is, however, non-convex involving both polynomials and trigonometric functions. In the existing literature, the OPP problem is solved using off-the-shelf solvers with local convergence guarantees. To obtain guarantees of global optimality, we employ and extend techniques from polynomial optimization literature and provide a solution with a global convergence guarantee. Specifically, we propose a polynomial approximation to the OPP problem to then utilize well-studied globally convergent convex relaxation hierarchies, namely, semi-definite programming and relative entropy relaxations. The resulting hierarchy is proven to converge to the global optimal solution. Our method exhibits a strong performance for OPP problems up to 50 switching instances per quarter wave.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
