分段随机障碍函数

《Automatica》：Piecewise Stochastic Barrier Functions

　　雷扬·马祖兹（Rayan Mazouz）、弗雷德里克·贝姆勒·马蒂森（Frederik Baymler Mathiesen）、卢卡·劳伦蒂（Luca Laurenti）、莫尔特扎·拉希贾尼安（Morteza Lahijanian）
美国科罗拉多大学博尔德分校航空航天工程科学系

**摘要**
随机屏障函数（Stochastic Barrier Functions, SBFs）是一种类似李雅普诺夫（Lyapunov）的函数，可用于随机系统的安全性分析。然而，找到一个有效的SBF是具有挑战性的，因为这需要解决一个复杂的函数优化问题。现有的凸优化方法通常仅适用于具有简单（多项式）动态特性的低维系统，而非凸方法则缺乏完整性保证。为了解决这些问题，本文提出了一种基于分段函数（Piecewise Functions, PWs）的新型SBF合成框架。首先，我们概述了PW-SBFs的一般公式。然后，我们重点讨论了PW-Constant（PWC）SBFs，并展示了它们的简单性如何为一般随机系统带来计算优势。具体来说，我们证明了PWC-SBFs的合成可以归结为最小最大优化问题。接下来，我们介绍了三种高效的算法来解决这个问题，每种算法都有其独特的权衡，并且都保证了完整性。第一种算法基于对偶线性规划（Dual Linear Programming, LP），可以精确求解最小最大优化问题；第二种算法基于反例引导的归纳合成（Counter-Example Guided Inductive Synthesis, LP-CEGIS），涉及解决两个较小的LP问题；第三种算法使用梯度下降（Gradient Descent, GD）求解最小最大问题，具有更好的可扩展性。我们在包括神经网络动态模型、非线性切换系统和高维线性系统在内的多种案例研究中对这些方法进行了广泛评估。我们的实验表明，PWC-SBFs的性能优于现有的最先进方法（如平方和函数和神经屏障函数），并且能够扩展到八维系统。

**引言**
在安全关键领域部署的自主系统需要彻底的验证以确保可靠性。这类系统的例子包括在人类共享环境中的自动驾驶车辆（Shalev-Shwartz等人，2017年）、航空航天系统（从空中运输Lee等人，2016年到太空探索Maluf等人，2005年）以及外科手术机器人（Guiochet等人，2017年）。然而，这种验证过程面临着由系统动态复杂性以及物理或随机算法不确定性引起的重大挑战。随机屏障函数（SBFs）（Kushner, 1967年；Prajna等人，2007年；Santoyo等人，2021年）是一种广泛采用的方法，用于提供必要的安全性保证。SBFs为安全性概率提供了一个下界，从而可以用于安全性认证。尽管对SBFs有大量研究，但现有方法要么缺乏完整性（在非凸方法的情况下），要么主要限于简单的情况（在凸方法的情况下），即多项式动态特性和低维系统。本研究旨在通过开发适用于复杂系统的一系列理论和计算框架来解决这些限制。

SBFs的合成类似于李雅普诺夫函数，归结为一个函数优化问题：目标是最小化函数沿系统轨迹的增长率（在期望意义上），以及在初始状态下的函数值，同时确保函数在不安全状态下始终高于某个阈值。文献中提出了两种主要的SBFs合成方法：平方和优化（Sum-of-Squares, SOS）（Mazouz等人，2022年；Santoyo等人，2021年）和神经屏障函数（Neural Barrier Functions, NBF）（Dawson等人，2022年；Mathiesen等人，2022年）。SOS优化依赖于预定义的SOS多项式模板，并通过凸优化来确定其系数。虽然这种方法很强大，但在系统维度较大或安全集是非凸的情况下效果不佳（Ahmadi & Majumdar, 2014年）。另一方面，NBF使用神经网络（NNs）作为屏障函数，解决了SOS在非凸环境中的保守性问题。然而，NBF存在可扩展性问题，因为需要验证NN是否符合SBF条件，这对于高维系统来说是一个挑战。

为了说明这些挑战，考虑图1中所示的具有加性高斯噪声的二维线性系统。图1(a)展示了初始集合和安全集合。注意，安全集合是非凸的。图1(b)和(c)分别展示了使用Mazouz等人（2022年）和Mathiesen等人（2022年）提出的最先进技术合成的30阶SOS SBF和NBF。通常，SBF的值越高（特别是在初始集合上），系统的安全性概率下限就越低。对于SOS SBF，10个时间步内保持在安全集合中的概率下限为0.075，而NBF的概率下限为0.93，相应的计算时间分别为197秒和3600秒。显然，NBF在安全性概率方面优于SOS，但计算时间增加了近10倍。实际上，对于高维系统，确保训练有素的NN是SBF所需的计算时间会迅速增加。

在本文中，我们提出了一种基于分段函数（PWs）的SBF框架。首先，我们概述了PW-SBFs的一般公式。然后，我们重点讨论了PW-Constant（PWC）SBFs，其简单性使其适用于一般随机系统。我们的关键发现是，通过使用常数函数，可以显著减轻SBFs所需的期望值计算和函数组合等复杂操作，从而实现简单性和可扩展性。基于这一发现，我们证明了PWC-SBF合成问题可以归结为最小最大优化问题，并为此引入了三种高效且完整的计算方法。首先，我们展示了即使对于非线性随机系统，最小最大优化问题也可以通过对偶公式转化为线性规划（LP）。其次，为了实现可扩展性，我们引入了一种迭代算法，该算法基于反例引导的归纳合成（LP-CEGIS）原理，需要解决两个较小的LP问题。然而，LP-CEGIS方法可能消耗较多内存。第三种方法使用梯度下降（GD）算法求解最小最大问题，具有更好的可扩展性，并解决了LP-CEGIS的内存问题，但在设计收敛标准方面存在挑战。图1(d)展示了PWC-SBFs的优势：使用相同的0.93安全性概率下限，计算时间仅为69秒，比NBF快了一个数量级（50倍）。我们的广泛评估证明了所提出方法的有效性，它们优于现有方法，并且能够扩展到八维系统。

**总结**
本研究的主要贡献包括：
1. 提出了一种针对PW-SBFs的一般公式，特别关注PWC-SBFs，为一般随机系统的安全性验证提供了简单的公式。
2. 将PWC-SBF合成问题归结为最小最大凸优化问题。
3. 三种高效且可扩展的PWC-SBF合成计算方法：
- 基于对偶线性规划的方法，并证明了零对偶间隙，即可以获得最小最大问题的精确解；
- LP-CEGIS算法，在有限时间内收敛到最优解；
- 使用梯度下降（GD）算法，显著减少了计算时间。
4. 通过广泛的案例研究证明了所提出方法相对于SOS和NBF等现有方法的优越性，并对其进行了分析。

总体而言，这项工作在安全关键系统的SBF合成方面取得了重大进展，提供了理论见解和计算方法，增强了复杂环境中的可扩展性。

**结论**
屏障函数（也称为屏障证书（Barrier Certificates，Ames等人，2014年；Ames等人，2016年；Prajna和Jadbabaie，2004年）为动态系统的安全性提供了正式方法，特别是对于非线性和混合模型（Prajna，2006年；Prajna和Jadbabaie，2004年）。屏障函数既适用于确定性系统（Ames等人，2019年；Prajna和Rantzer，2005年），也适用于随机系统（Kushner，1967年；Prajna等人，2007年）。Kushner（1967年）首次使用SBFs验证离散时间系统，基于鞅理论建立了一个函数成为SBF的条件。Prajna等人（2007年）首次将SBFs应用于具有离散跳跃的连续时间混合系统。

寻找给定系统的SBF是一个最近受到更多关注的问题，包括SOS优化（Mazouz等人，2022年；Santoyo等人，2021年）、神经网络（Mathiesen等人，2022年）和CEGIS（Ding等人，2022年；Jagtap等人，2020年；Peruffo等人，2021年）等方法。基于SOS优化的方法通常面临可扩展性和非凸安全集表示方面的挑战，且通常仅适用于多项式动态和低维系统。Mazouz等人（2022年）的工作扩展了SOS方法，利用Zhang等人（2018年）的技术构建了动态的仿射界。然而，可扩展性仍然是一个重大挑战。

为了解决SOS方法的局限性，最近提出了神经屏障函数（NBF）（Dawson等人，2022年；Mathiesen等人，2022年）。NBF利用神经网络（NNs）的表示能力训练出合适的SBF候选者，然后需要验证其是否为有效的证书。?ikeli?等人（2023年）的工作将NBF与强化学习结合，基于一种新的达到-避免鞅（Reach-Avoid Martingales）公式训练深度策略。这些方法的主要局限性在于它们依赖于NN验证，这也存在可扩展性问题。Jagtap等人（2020年）提出了一种基于CEGIS（Alur等人，2013年）的替代（非凸）SBF合成方法。具体来说，Jagtap等人使用（单项式）基函数参数化SBF，并从状态空间的有限样本中合成参数。所得函数作为候选SBF，然后需要在整个状态空间中验证是否符合SBF条件。验证通过寻找违反条件的反例来完成，通常使用SMT求解器或非线性优化方法。然而，这些方法不完整，非线性求解器容易陷入局部最小值。此外，这些（非凸）CEGIS方法还存在可扩展性问题（Barbosa等人，2019年）。

本文旨在解决SOS、NBF和非凸CEGIS方法在保守性和可扩展性方面的局限性。我们的工作主要基于Laurenti和Lahijanian（2023年）的结果，建立了SBFs与动态规划之间的联系。基于这一见解，我们提出了一种基于分段函数（PWs）的新型SBF合成方法。与Laurenti和Lahijanian（2023年）的方法不同，本文引入了新的PW-SBF类别及其定制的合成方法，并与现有的SBF合成方法进行了详细比较。此外，与Jagtap等人（2020年）的非凸CEGIS方法不同，本文提出的所有方法都是凸的，因此是完整且高效的，包括我们的LP-CEGIS方法。

其他相关工作包括（Anand等人，2022年；Edwards等人，2024年；Nejati和Zamani，2023年；Prajna和Jadbabaie，2004年）。具体来说，Nejati和Zamani（2023年）提出了一种基于多种控制屏障证书的驱动方法来合成安全控制器。然而，这些方法假设系统的动态是确定性的。在Prajna和Jadbabaie（2004年）中，提出了一种用于（非）确定性混合系统安全验证的SBF方法，其中每个函数对应系统的某一离散模式。Edwards等人（2024年）提出了一种用于确定性离散和时间系统正式验证和控制的工具。在Anand等人（2022年）中，提出了一种基于小增益理论的互连随机系统验证方法。然而，这些工作都没有解决我们在本文中提出的针对一般离散时间随机系统的PW-SBF合成问题。

我们在文中使用的基本符号如下：自然数、实数和非负实数分别用N、R和R≥0表示。随机变量用粗体符号表示，例如x∈Rn表示取值于n维欧几里得空间的随机变量，而x∈Rn表示该空间中的一个点。Pr表示概率测度，Ps表示安全性概率。从紧凑集合Xi?Rn到紧凑（可测量）集合Xj?Rn的概率转移用pij∈[0,1]表示，其下界和上界分别用p?ij和pˉij∈[0,1]表示，即0≤p?ij≤pij≤pˉij≤1。对于K∈N个紧凑集合X1,X2,…,XK?Rn，从Xi到Xj的可行转移概率分布用pi=(pi1,…,piK)表示，满足pij∈[p?ij,pˉij]对所有j∈{1,…,K}且∑j=1Kpij=1。所有从Xi出发的可行转移概率的集合用Pi表示。问题构建我们考虑一个由以下随机差分方程描述的随机过程：xk+1=f(xk,vk)，其中状态xk取值于Rn，噪声vk是一个独立同分布的随机变量，其取值范围在Rv内，并具有相应的概率分布pv。此外，f:Rn×Rv→Rn是表示系统(1)一步动态的向量场。我们假设f在几乎所有地方都是连续的。直观地说，xk是具有可能性的随机过程的一个通用模型。随机屏障函数在本节中，我们提供了随机屏障函数的概述。考虑系统(1)，其中安全集Xs?Rn，初始集合X0?Xs，不安全集Xu=Rn?Xs。那么，如果存在标量η、β≥0，使得B(x)≥0?x∈Rn，B(x)≥1?x∈Xu，B(x)≤η?x∈X0，E[B(f(x,v))|x]≤B(x)+β?x∈Xs，并且v∈Rn是一个具有密度pv的随机变量，那么函数B:Rn→R就是一个随机屏障函数（SBF）。给定一个SBF B，可以根据以下内容获得系统(1)的安全概率的下限。分段随机屏障函数在本文中，我们引入了分段SBF（PW-SBF）的概念。考虑将紧凑的安全集Xs划分为K个紧凑集合X1，…，XK，即?i=1KXi=Xs且Xi∩Xj=0?对于所有i≠j∈{1，…，K}，使得向量场f在每个区域Xi内是连续的，并且我们进一步假设每个Xi的边界相对于T(?∣x)的测度为零，对于任何x∈Xs。此外，设Bi:Xi→R是每个i∈{1，…，K}的一个实值连续函数。我们定义PW函数B(x)=Bi(x)如果x∈Xi，否则...分段常数SBF合成在本节中，我们首先正式提出了一个用于合成PWC-SBF的优化问题。然后，我们介绍了三种有效的计算方法来解决这个优化问题，即基于线性规划（LP）对偶的方法、基于LP反例引导的归纳合成（LP-CEGIS）程序和基于梯度下降（GD）的方法。评估为了展示PWC-SBF的能力以及我们提出的合成方法的有效性，我们研究了一组七个基准问题的性能，这些问题包括具有线性和非线性动态的随机系统，并且维度从2D到8D不等。我们还将PWC-SBF的性能与最先进的连续SBF技术（即SOS和NBF）进行了比较。除了NBF之外，我们实现的所有方法，包括三种提出的PWC-SBF合成方法，都是在Julia中实现的。结论在这项工作中，我们提出了分段（PW）随机屏障函数（SBF）的公式。我们讨论了它们所提供的灵活性以及由此带来的计算成本的增加。为了奠定基础，我们专注于它们最简单的形式，即PW常数（PWC）函数。我们展示了最优PWC SBF的合成可以简化为一个包含双线性项的约束极小优化问题。我们进一步展示了PWC SBF可以获得相同甚至更高的概率安全性。Rayan Mazouz在代尔夫特工业大学获得了航空航天工程的学士学位和硕士学位。目前，他正在科罗拉多大学博尔德分校攻读博士学位。他的研究主要集中在随机动态系统的形式验证和控制合成方面。