Learning fixed-complexity polyhedral Lyapunov functions from counterexamples

Hybrid linear systems consist of a finite set of modes $Q$, such that for each mode $q\in Q$, there is a closed polyhedral cone $\mathcal{H}_{q}\subseteq\mathbb{R}^{d}$ called the domain, and a flow matrix $A_{q}\in\mathbb{R}^{d\times d}$. Let $\mathcal{F}:\mathbb{R}^{d}\rightrightarrows\mathbb{R}^{d}$ be the set-valued function defined by $\mathcal{F}(x)=\{A_{q}x:q\in Q,\,x\in\mathcal{H}_{q}\}$. For the purpose of our analysis, $\mathcal{F}$ describes completely the dynamics of the system. Therefore, in the following, we will refer to the system as system $\mathcal{F}$. A function $\xi:\mathbb{R}_{\geq 0}\to\mathbb{R}^{d}$ is a trajectory of system $\mathcal{F}$ if $\xi$ is absolutely continuous and satisfies the differential inclusion $\xi^{\prime}(t)\in\mathcal{F}(\xi(t))$ for almost all $t\in\mathbb{R}_{\geq 0}$ [23].

A polyhedral function $V:\mathbb{R}^{d}\to\mathbb{R}$ can be described as the pointwise maximum of a finite set of linear functions, i.e., $V(x)=\max_{i\in[m]}\,c_{i}^{\top}x$ where $m\in\mathbb{N}_{>0}$ and $\{c_{i}\}_{i=1}^{m}\subseteq\mathbb{R}^{d}$.

To be a Lyapunov function for system $\mathcal{F}$, a piecewise smooth function $V:\mathbb{R}^{d}\to\mathbb{R}$ must (i) be positive everywhere except at the origin, and (ii) strictly decrease along all trajectories of the system not starting at the origin [1]. In the case of polyhedral functions, a sufficient condition for being a Lyapunov function and thereby ensuring stability of the system, is as follows [24, Proposition 3]:

In other words, a set a vectors $\{c_{i}\}_{i=1}^{m}$ represents a polyhedral Lyapunov function for system $\mathcal{F}$ if

The condition in (1) is difficult to enforce because (i) it involves an infinite set of constraints, and (ii) each constraint involves a disjunction of $m$ clauses¹¹1$m-1$ clauses come from the “$\exists\,j$” and one clause comes from the condition between brackets “$[\ldots]$”.. In the next section, we describe a tree-based counterexample-guided algorithm to tackle this problem. The idea is to (i) consider only a finite set of constraints, obtained from the counterexamples, and (ii) decompose the disjunction by introducing a branch in the tree for each clause.

We define the $m$-Lyap-Fun-Exists problem as that of checking the existence of a polyhedral function satisfying (1), given a hybrid linear system $\mathcal{F}$ and a number of pieces $m\geq 2$.

To conclude this section, let us introduce an example of hybrid linear systems that we will use throughout the paper to illustrate the approach.

Given a set of constraints $Y\subseteq\mathbb{R}^{d}_{*}\times[m]\times[m]$, we aim to find vectors $(c_{i})_{i=1}^{m}\subseteq\mathbb{R}^{d}$ compatible with $Y$ according to conditions (2)–(3). Therefore, we solve the following feasibility problem:

When $Y$ is finite, (4) is a Linear Program and thus can be solved efficiently [25, 26]. We denote by $S(Y)$ the set of feasible solutions of (5). A set of vectors $(c_{i})_{i=1}^{m}\subseteq\mathbb{R}^{d}$ is thus a candidate solution compatible with $Y$ iff $(c_{i})_{i=1}^{m}\in S(Y)$. Note that $S(Y)$ is a convex set.

We verify whether a candidate solution $(c_{i})_{i=1}^{m}$ computed in the learning phase provides a valid Lyapunov function for system $\mathcal{F}$, by checking whether it satisfies (C1) and (C2) in Proposition 1. If this is not the case, we generates a pair $(x,i)\in\mathbb{R}^{d}\times[m]$, called a counterexample, at which (1) is not satisfied.

First, we verify that (C1) holds for the candidate solution by searching for $x\in\mathbb{R}_{*}^{d}$ such that $V(x)\leq 0$. Without loss of generality, we can set $x$ to be on the boundary of $[-1,1]^{d}$. Therefore, we solve $2d$ Linear Programs, for each facet $F$ of $[-1,1]^{d}$:

If for all facet $F$, (5) is infeasible, then (C1) holds. However, if there is a facet $F$ for which (5) has a feasible solution $x$, then it holds that $x\neq 0$ and $V(x)\leq 0$. We find index $i\in[m]$ with $c_{i}^{\top}x=V(x)$, yielding a counterexample $(x,i)$.

If (C1) is shown to hold, we next verify that (C2) holds too. Therefore, we solve $m\lvert Q\rvert$ LPs, for each $i\in[m]$ and $q\in Q$,

If for all $i,q$, (6) is infeasible, then (C2) holds. However, if there are $i,q$ for which (6) has a feasible solution $x$, then it holds that $x\neq 0$, $c_{i}^{\top}x=V(x)$ and $c_{i}^{\top}v\geq 0$ wherein $v=A_{q}x\in\mathcal{F}(x)$, so that $(x,i)$ is a counterexample.

The algorithm organizes the set of constraints as a tree with the following properties: (a) each node $u$ is associated with a set of constraints $Y(u)$ and thus with a convex set of candidates $S(u)\coloneqq S(Y(u))$; (b) the root of the tree is associated with $Y(\text{root})=\emptyset$; and (c) each node $u$ has $m$ children, $u_{1},\ldots,u_{m}$, with associated sets of constraints $Y(u_{j})=Y(u)\uplus\{(x,i,j)\}$, wherein $(x,i)$ is the counterexample found during the verification of the candidate at node $u$. Each leaf of the tree is marked as unexplored or infeasible.

Each iteration of our algorithm is as follows:

1. 1.

   Choose an unexplored leaf $u$.

2. 2.

   Find a candidate $(c_{i})_{i=1}^{m}\in S(u)$.

3. 3.

   Verify the candidate using (5) and (6).

4. 4.

   If we find a counterexample $(x,i)$, we add $m$ children, $u_{1},\ldots,u_{m}$, to $u$ wherein $u_{j}$ is unexplored and has set of constraints $Y(u_{j})=Y(u)\uplus\{(x,i,j)\}$.

Alg. 1 shows the pseudo-code. We will now establish some properties of Alg. 1. Let $(c_{i})_{i=1}^{m}$ be a candidate chosen for some leaf $u$ (Line 1) and $(x,i)$ be a counterexample that was found for this candidate (Line 1). Consider $S(u_{j})$ for some child $u_{j}$ of $u$ (Line 1).

Let us assume that the underlying system $\mathcal{F}$ has a polyhedral Lyapunov function, given by $(c_{i}^{*})_{i=1}^{m}$, satisfying (1) and without loss of generality assume $\{c_{i}^{*}\}_{i=1}^{m}\subseteq[-1,1]^{d}$.

As a corollary, we get the soundness of the algorithm:

Note that there is no guarantee that Alg. 1 will terminate. To ensure termination, we modify the algorithm by leveraging a central result in convex nonsmooth optimization, known as the cutting-plane argument.

Therefore, assume that at Line 1 of Alg. 1, the candidate $(c_{i})_{i=1}^{m}$ is chosen as the center of the Maximum Volume Ellipsoid (MVE) inscribed in $S(u)$. The MVE center of a polyhedron can be computed efficiently using Semidefinite Programming [26, Proposition 4.9.1]. Remember that the rationale of adding constraints from the counterexample (Line 1) is to exclude the candidate from further consideration at all descendant nodes. The choice of the candidate as the MVE center makes the exclusion stronger by guaranteeing a minimum rate of decrease of the volume of $S(u)$ when going from one node to any of its children. This follows from the cutting-plane argument:

Based on the above, consider the following modification of the algorithm. Fixed $\epsilon>0$ and consider Alg. 1, except that in the learning phase, if $S(u)$ does not contain a ball of radius $\epsilon$, then $u$ is declared infeasible; otherwise, we choose the candidate $(c_{i})_{i=1}^{m}$ as the MVE center of $S(Y)$. See Alg. 2 for a pseudo-code of the modified learning phase. It holds that the modified algorithm terminates in finite time.

The dominant factor in the complexity of Alg. 2 is the depth $D$ of the tree explored during the execution of the algorithm. From the proof of Theorem 7, it holds that

where $r=md$. Alg. 2 explores at most $m^{D+1}$ nodes before termination. We deduce the following complexity bound:

The complexity of Alg. 2 is exponential in $d$ and $m$. The exponential dependence on $d$ is to be expected from Theorem 2 which shows that $m$-Lyap-Fun-Exists is NP-hard, even with $m=2$.

We show that $m$-Lyap-Fun-Exist with $m=2$ is NP-hard by reducing NAE-SAT3 to it. NAE-SAT3 (Not All Equal SATisfiability) is a version of the SAT3 problem that takes as input $L$ clauses $C_{1},\ldots,C_{L}$ over $n$ propositions $p_{1},\ldots,p_{n}$. Each clause $C_{l}$ is a triple of literals: $C_{l}=(s_{l,1},s_{l,2},s_{l,3})$ wherein $s_{l,h}\in\{p_{1},\ldots,p_{n}\}\cup\{\neg p_{1},\ldots,\neg p_{n}\}$.

Given such a tuple $\varphi=(C_{1},\ldots,C_{L})$ of clauses, the NAE-SAT3 problem asks whether there exists an assignment of $\mathit{true}$ or $\mathit{false}$ to each proposition $p_{k}$ such that for each clause $C_{l}$, at least one literal is true and at least one literal is false. Without loss of generality, we assume that for each clause, the three literals involve distinct propositions (otherwise, the clause is trivially “satisfied”). It is well known that NAE-SAT3 is NP-complete [28].

We will now reduce any given NAE-SAT3 instance $\varphi$ with $n$ propositions and $L$ clauses to yield a hybrid linear system, described by $(\{\mathcal{H}_{q}\}_{q\in Q},\{A_{q}\}_{q\in Q})$, that has a $2$-piece polyhedral Lyapunov function iff $\varphi$ has a truth assignment that makes it NAE-SAT3-satisfiable.

Let $d=n+2$. Consider a vector of $d$ variables: $x=(\bar{x}_{1},\ldots,\bar{x}_{n},\hat{x},\tilde{x})$. Also, consider two vectors of $d$ coefficients: $f=(\bar{f}_{1},\ldots,\bar{f}_{n},\hat{f},\tilde{f})$ and $g=(\bar{g}_{1},\ldots,\bar{g}_{n},\hat{g},\tilde{g})$. We look for a $2$-piece polyhedral Lyapunov function, defined by $V(x)=\max\,\{f^{\top}x,g^{\top}x\}$, for the system defined below.

For each $k\in[n]$, let

and consider the dynamics: $\dot{\bar{x}}_{k}=-\bar{x}_{k}$; for all $k^{\prime}\in[n]\setminus\{k\}$, $\dot{\bar{x}}_{k^{\prime}}=0$; $\dot{\hat{x}}=0$; $\dot{\tilde{x}}=\lvert x_{k}\rvert$ (mind the absolute value which can be cast as a piecewise linear dynamics by splitting $\mathcal{H}_{k}$ in two pieces). Condition (1) then becomes

This is equivalent to saying that (i) $\bar{f}_{k}\bar{g}_{k}<0$ (i.e., both are nonzero and have opposite signs), (ii) $\lvert\bar{f}_{k}\rvert>\tilde{f}$, and (iii) $\lvert\bar{g}_{k}\rvert>\tilde{g}$.

If $\bar{f}_{k}<0$ (i.e., $\bar{g}_{k}>0$), we assign the value true to $p_{k}$; otherwise, we assign the value false.

Now, for each $l\in[L]$, let

and consider the dynamics: for all $k\in[n]$, $\dot{\bar{x}}_{k}=\sigma_{l,k}\lvert\hat{x}\rvert$ where

$\dot{\hat{x}}=0$; $\dot{\tilde{x}}=-3\lvert\hat{x}\rvert$. Condition (1) then becomes

This is equivalent to saying that $\hat{f}\hat{g}$, $\sum_{k=1}^{n}\sigma_{l,k}\bar{f}_{k}-3\tilde{f}$ and $\sum_{k=1}^{n}\sigma_{l,k}\bar{g}_{k}-3\tilde{g}$ are negative.

Now, it holds that $\sum_{k=1}^{n}\sigma_{l,k}\bar{f}_{k}-3\tilde{f}<0$ only if there is $k\in[n]$ such that $\sigma_{l,k}\bar{f}_{k}<0$. Similarly, $\sum_{k=1}^{n}\sigma_{l,k}\bar{g}_{k}-3\tilde{g}<0$ only if there is $k\in[n]$ such that $\sigma_{l,k}\bar{g}_{k}<0$. Thus, NAE-SAT3 is satisfied with the assignment described above. On the other hand, if $p_{1},\ldots,p_{n}$ satisfies NAE-SAT3, then the assignment: for all $k\in[n]$, $\bar{f}_{k}=-\bar{g}_{k}=1$ if $\neg p_{k}$ and $\bar{f}_{k}=-\bar{g}_{k}=-1$ if $p_{k}$, $\hat{f}=-\hat{g}=1$, and $\tilde{f}=\tilde{g}=0.9$, provides a $2$-piece polyhedral Lyapunov function for the above system. Thus, the above system admits a $2$-piece polyhedral Lyapunov function iff $\varphi$ is NAE-SAT3-satisfiable.

We prove that system $\mathcal{F}$ in Example 1 does not admit a polynomial Lyapunov function. For the sake of a contradiction, assume that $V$ is a polynomial Lyapunov function for the system. Since $V$ is radially unbounded, it is of nonzero even degree. Fix $r\in\mathbb{R}_{>0}$ and let $x:\mathbb{R}_{\geq 0}\to\mathbb{R}^{d}$ be the trajectory of the system starting from $x(0)=[r,0]^{\top}$. It holds that $x(1)=e^{A_{2}}x(0)=[0,-r]^{\top}$ and $x(2)=e^{A_{3}}x(1)=e^{0.01}[-r,0]^{\top}$. Since $V$ is of nonzero even degree, we have that $V(e^{0.01}[-r,0]^{\top})>V([r,0]^{\top})$ whenever $\lvert r\rvert$ is large enough. Since $r>0$ was arbitrary, this contradicts the property that $V$ decreases along all trajectories of the system.

The proof is by induction on the iterations the algorithm. The property is true at the very beginning since $(c_{i}^{*})_{i=1}^{m}\in S(\text{root})$. Assume it is true after $k$ iterations of the while loop and let $v$ be a leaf satisfying the property at this step. If the algorithm stops at this step, there is nothing to prove. Thus, assume some unexplored leaf $u$ is to be expanded at this step. If $u\neq v$, then the property will be trivially satisfied at the subsequent step. Hence, suppose $u=v$, and let $(x,i)$ be the counterexample found by the verifier. Let $j\in[m]$ be such that $(c_{i}^{*})_{i=1}^{m}\subseteq S(\{(x,i,j)\})$ (which always exists since $(c_{i}^{*})_{i=1}^{m}$ satisfies (1)). Since $(c_{i}^{*})_{i=1}^{m}\subseteq S(Y(u))$, it holds that $(c_{i}^{*})_{i=1}^{m}\subseteq S(Y(u)\cup\{(x,i,j)\})$, so that the child node $u_{j}$ of $u$ satisfies $(c_{i}^{*})_{i=1}^{m}\in S(u_{j})$, concluding the proof.

First, we prove that Alg. 2 always terminates. Let $u$ be the leaf that is expanded and let $v$ be any of its children. Let $r=md$. Since $(c_{i})_{i=1}^{m}$ is the MVE center of $S(u)$, it holds by Lemma 6 that $\mathrm{vol}(S(v))\leq(1-\frac{1}{r})\mathrm{vol}(S(u))$. At the very start of the algorithm, $S(\text{root})\cong[-1,1]^{m\times d}$ which has volume $V_{0}\coloneqq 2^{r}$. Let $v$ be an unexplored leaf at depth $D$ of the tree. By induction, we can show that $\mathrm{vol}(S(v))\leq(1-\frac{1}{r})^{D}V_{0}$. Let $V_{\epsilon}\coloneqq(2\epsilon)^{r}$ be the volume of the $\epsilon$-ball $[-\epsilon,\epsilon]^{m\times d}$. Since we terminate whenever $\mathrm{vol}(S(v))\leq V_{\epsilon}$, it holds that $D\leq\frac{\log(V_{\epsilon})-\log(V_{0})}{\log(1-\frac{1}{r})}$. In other words, the depth of the tree is upper bounded. This proves that Alg. 2 always terminates.

The proof that Alg. 2 is sound is similar to the proof of Theorem 5.