Convex synthesis and veriﬁcation of control-Lyapunov and barrier functions with input constraints Hongkai Dai1and Frank Permenter1

2025-05-06 0 0 706.08KB 8 页 10玖币

侵权投诉

Convex synthesis and veriﬁcation of control-Lyapunov and barrier

functions with input constraints

Hongkai Dai1and Frank Permenter1

Abstract— Control Lyapunov functions (CLFs) and control

barrier functions (CBFs) are widely used tools for synthesizing

controllers subject to stability and safety constraints. Paired

with online optimization, they provide stabilizing control actions

that satisfy input constraints and avoid unsafe regions of

state-space. Designing CLFs and CBFs with rigorous perfor-

mance guarantees is computationally challenging. To certify

existence of control actions, current techniques not only design

a CLF/CBF, but also a nominal controller. This can make

the synthesis task more expensive, and performance estimation

more conservative. In this work, we characterize polynomial

CLFs/CBFs using sum-of-squares conditions, which can be

directly certiﬁed using convex optimization. This yields a

CLF and CBF synthesis technique that does not rely on a

nominal controller. We then present algorithms for iteratively

enlarging estimates of the stabilizable and safe regions. We

demonstrate our algorithms on a 2D toy system, a pendulum

and a quadrotor.

I. INTRODUCTION

When synthesizing controllers for dynamical systems, it

is often paramount to ensure that the closed-loop system

always converges to the desired state and always avoids

unsafe regions. These goals can be met by using control

Lyapunov functions (CLFs) [27] for stability, and control

barrier functions (CBFs) [3] for safety. CLFs and CBFs are

designed such that their online minimization leads to desired

performance goals. Local veriﬁcation amounts to certifying

these minimization problems are feasible on some subset of

state-space, which can be a challenging computational task.

CLFs and CBFs have been used extensively in controller

design for various applications, including legged locomotion

[14], [15], [22], autonomous driving [2], [7], [34], and robot

arm manipulation [21]. Recently, they have been used to

guide learning-based methods [8], [9], [17]. The CLFs/CBFs

are typically synthesized by hand or learned from data

[25], [12] without rigorous veriﬁcation. In this paper, we

provide a new synthesis technique with formal guarantees

that is conceptually simpler than previous formal methods

[16], [19], [1], [32]. In particular, our technique allows

one to verify CLFs and CBFs by solving a single convex

optimization problem, under the assumption the dynamics

are control-afﬁne and the input constraints are polyhedral

(for example, robots subject to torque limits for each motor).

This in turn leads to synthesis algorithms based on sequential

convex optimization.

The basis of our technique is Sum-Of-Squares (SOS)

optimization [6], [23], a widely used tool for controller

1Toyota Research Institute, US hongkai.dai,

frank.permenter@tri.global

Fig. 1: With our certiﬁed CLF, the QP controller can stabilize

the quadrotor from many distant states (including ones that

are 10 meters away or the initial roll angle of 140◦) to the

desired hovering state.

synthesis and veriﬁcation, including CLF and CBF design

[29], [10], [16], [19], [1], [32]. These previous methods

either ignore input constraints [29], [10] or rely on the

joint synthesis of a nominal control law of polynomial form

[16], [19], [1], [32]. Reliance on this polynomial controller

is restrictive if the actual stable/safe control policy is not

polynomial. It also limits scalability, as the size of the SOS

program increases rapidly with the degree of the controller.

In this paper, we derive new necessary and sufﬁcient

conditions for CLFs/CBFs for polynomial dynamical systems

with input constraints. We formulate these conditions as

SOS feasibility problems, and present an iterative algorithm

for enlarging an inner approximation of the stabilizable

and/or safe region via sequential SOS optimization. We

demonstrate our algorithm on different systems, including

a 2D toy example, an inverted pendulum and a quadrotor.

To our best knowledge this is the ﬁrst formal method for

CLF/CBF synthesis that both accounts for input constraints

and explicitly avoids construction of a nominal controller.

II. BACKGROUND

In this section we give a brief introduction to Sum-Of-

Squares (SOS) techniques for certifying polynomial non-

negativity. To begin, a polynomial p(x)is a sum-of-squares

(sos) iff p(x) = Piqi(x)2for some polynomials qi(x).

Clearly p(x)being sos implies that p(x)≥0∀x. If p(x)

has degree 2d, then it is an sos polynomial if and only if

p(x) = m(x)TS m(x), S 0,(1)

where m(x)is a vector consisting of all monomials of degree

at most d. Given p(x)and m(x), existence of Scan be

checked using semideﬁnite programming [23], [6].

arXiv:2210.00629v1 [cs.RO] 2 Oct 2022

Sum-of-squares optimization can also certify polynomial

non-negativity on the feasible set of ﬁnitely-many polyno-

mial inequalities, i.e., on a semialgebraic set Kof the form

{x∈Rn|b1(x)≥0, . . . , bm(x)≥0}. The underlying

certiﬁcates employ the preorder of bi, deﬁned as

preorder(b1(x), . . . , bm(x))

=





l0(x) +

i=1

li(x)bi(x) + X

i6=j

lij (x)bi(x)bj(x)

i6=j6=k

lijk(x)bi(x)bj(x)bk(x)

+. . . |l0(x), li(x), lij (x), lijk(x), . . . are all sos





(2)

For a given polynomial p(x), the Positivstellensatz

[28][18, Section 3.6] states that

p(x)≥0on K

∃q(x), r(x)∈preorder(b1(x), . . . , bm(x)), k ∈N

s.t p(x)q(x) = p(x)2k+r(x).

(3)

In other words, if p(x)is non-negative on K, then there is a

certiﬁcate of this fact deﬁned by polynomials q(x)and r(x)

in the preorder. Further, for ﬁxed k, ﬁnding this certiﬁcate

can be cast as a semideﬁnite program [6].

Unfortunately, a generic element of the preorder is the

summation of 2mdifferent polynomials each scaled by

a different sum-of-squares polynomial. This exponential

complexity motivates simpler (sufﬁcient) conditions for

non-negativity. A common simpliﬁcation—called the S-

procedure [23]—is existence of polynomials ¯ri(x), i =

0, . . . , m satisfying

(1 + ¯r0(x))p(x)−

i=1

¯ri(x)bi(x)is sos (4a)

¯ri(x)is sos, i = 0, . . . , m. (4b)

The equation (4a) implies that p(x)≥0on Kbecause,

by deﬁnition, ¯ri(x)bi(x)≥0on K. Frequently, we simplify

this condition further by taking ¯r0(x)=0.

III. PROBLEM FORMULATION

We consider a control-afﬁne dynamical system of the form

˙x=f(x) + g(x)u, u ∈ U,(5)

where x∈Rnxand u∈Rnudenote the state and

control, f:Rnx→Rnxand g:Rnx→Rnx×nuare

polynomial functions of xand U ⊂ Rnudenotes the set of

admissible inputs, which we assume to be a convex polytope.

Equivalently, we assume existence of a ﬁnite set of points

uisatisfying

U=ConvexHull(u1, . . . , um).(6)

Without loss of generality, we assume that the goal state is

x∗=0. Finally, we note that through a change of variables,

the dynamics of many robotic systems can be written using

polynomials; see, e.g., [24], [26].

A. Control Lyapunov Functions (CLFs)

A polynomial function V(x)is a control Lyapunov func-

tion (CLF) if it satisﬁes the following conditions for some

positive integer α:

V(x)≥(xTx)α∀x(7a)

V(0)=0 (7b)

if V(x)< ρ and x6=0then ∃u∈ U

s.t LfV+LgV u

| {z }

V(x,u)

<−κVV, (7c)

where LfV=∂V

∂x f(x)and LgV=∂V

∂x g(x)denote Lie-

derivatives.

Under these conditions, the sublevel set Ωρ={x∈

Rnx|V(x)< ρ}is an inner approximation of the stabilizable

region, i.e., the backward reachable set of the goal state 0.

This means that for all initial states in Ωρ, there exist control

actions that drive the state to 0. The condition (7a) guarantees

that V(x)is positive deﬁnite and radially unbounded, while

the condition (7c) guarantees that V(x)converges to zero

exponentially with a rate larger than κV>0. Our goal

is to ﬁnd a polynomial CLF V(x)and a scalar ρthat

satisfy (7) and maximize (in some sense) the size of the

Ωρ. In other words, we seek a CLF that yields a large inner

approximation of the stabilizable region. We remark that a

previous technique for outer approximation appears in [20].

B. Control Barrier Functions (CBFs)

Given an unsafe set Xunsafe, a polynomial function h(x)

is a control barrier function with the safe region {x∈

Rnx|h(x)>0}if it satisﬁes

h(x)≤0∀x∈ Xunsafe (8a)

if h(x)> β−then ∃u∈ U

s.t Lfh+Lghu

| {z }

h(x,u)

>−κhh, (8b)

where β−<0and κh>0are given constants. We assume

that the unsafe region is given as the union of semialgebraic

sets, i.e.,

Xunsafe =X1

unsafe ∪. . . ∪ Xnunsafe

unsafe (9a)

unsafe ={x|pi,1(x)≤0, . . . , pi,si(x)≤0},(9b)

where pi,j (x)) is a polynomial. Our goal is to ﬁnd a

polynomial CBF h(x)with a large certiﬁed safe region

{x∈Rnx|h(x)>0}.

Note that the CLF and CBF conditions are related. Speciﬁ-

cally, if V(x)satisﬁes (7c) for a given κ, then h(x) = −V(x)

satisﬁes (8b) with the same κand β−=−ρ. Hence any

approach for synthesizing CLFs can be used to synthesize

CBFs with slight modiﬁcation.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

Convexsynthesisandvericationofcontrol-LyapunovandbarrierfunctionswithinputconstraintsHongkaiDai1andFrankPermenter1AbstractControlLyapunovfunctions(CLFs)andcontrolbarrierfunctions(CBFs)arewidelyusedtoolsforsynthesizingcontrollerssubjecttostabilityandsafetyconstraints.Pairedwithonlineoptimization,th...

展开>> 收起<<

Convex synthesis and veriﬁcation of control-Lyapunov and barrier functions with input constraints Hongkai Dai1and Frank Permenter1.pdf

共8页,预览2页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Convex synthesis and veriﬁcation of control-Lyapunov and barrier functions with input constraints Hongkai Dai1and Frank Permenter1

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: