2020，没有找到发表在哪个会议上的。。

摘要

由于机器学习组件的复杂性、非线性和参数空间大等特点，给网络物理系统的验证带来了巨大的挑战。
在这项工作中，我们提出了一个新的概率验证框架，为支持学习的CPS，它可以搜索整个(无限)空间的参数，计算出由信号时间逻辑(STL)公式捕获的导致满足或违反规范的事件
我们的技术是基于保形回归( conformal regression,?这个不太明白)，这是一种利用有限样本构造具有边际覆盖保证的预测区间的技术，不需要对分布和回归模型做任何假设。
我们的验证框架，使用正形回归，可以预测系统轨迹在不同参数集上的定量满意度值，并使用这些值来量化系统满足/违反给定STL属性的程度。
我们使用了三个可学习的CPS应用程序的案例研究来证明我们的技术可以成功地应用于参数空间的划分，并提供所需的保证级别。

Introduction

对于那些带有机器学习组件的系统，如高级驾驶辅助系统(ADAS)、自动驾驶控制器和基于神经网络的机器人控制器。由于这些是安全关键的网络物理系统，迫切需要有效和完善的验证算法[7]、[16]、[18]、[33]、[35]、[8]、[15]、[40]。但这种系统存在一些不确定性，如外部输入的环境，初始系统配置，和其他设计参数。我们将这些不确定性的空间称为参数空间，并希望使用验证技术来找到参数的范围，在此范围内，我们可以确保具有学习能力的CPS表现出高度置信度的安全行为。

• 目前的验证方法面临两个困难：1.进行彻底的状态空间搜索会维度爆炸；2.不能保证完全覆盖。
  在这篇文章中,通过开发一个验证框架,可以搜索整个系统的参数空间Θ，来发现满足或违反给定属性的参数集，并提供概率覆盖保证。
• 将能够学习的CPS系统的动力学模型看作一个黑盒，一旦状态空间中的参数(初始状态？系统配置等等)确定了，就能得到一条系统轨迹。
• 系统属性用信号时序逻辑(STL)来定义。这是一种能够在实值连续轨迹上进行规范的形式化方式，已广泛应用于CPS中，用于严格指定需求。STL自带一种量化语义鲁棒性符合值( robust satisfaction value ，RSV)ρ，它是一个函数，能够将属性和轨迹映射成实数 ρ($\varphi$,$\xi$) ，如果这个实数大于0 ，就说明符合属性，负数就不符合，并且如果这个数越大，就越符合属性$\varphi$，反之亦然。
• 然后使用一种用于构造无分布预测集的通用工具–保形回归。**保形回归技术可以构造在有限样本中获得有效覆盖的预测区间，而不需要对分布和潜在的回归算法做出假设。**因此，提出的算法可以利用有限的样本根据它们ρ的预测范围，将初始参数空间分成+，- 和 U，不同的子集。U是保留部分，在达到用户提供的半径阈值前还不知道它属于+ / - 。并且能够保证在+ 的区域里，符合$\varphi$ 属性的概率能够达到 1 - α。
• 为了查看神经网络(NN)或n控制动态系统的精确模型 ，现有技术使用屏障函数、可达性分析、可满足性模块化理论(SMT)的方法或混合整数线性程序(MILP)优化器，以获得安全保证。大多数方法都提供了确定性保证，但是面临可伸缩性问题，并且对它们可以处理的模型类型有额外的限制(例如，必须是ReLU激活函数)。
• 而本文的方法将支持学习的CPS视为黑盒，可以在给定固定参数的情况下生成模拟，因此可以在非常广泛的CPS类上使用。 此外，本文只对参数的联合分布和对应的STL属性的鲁棒值进行了推理。因此，算法的复杂性独立于模型的复杂性(除了从那些模型中获得模拟)，并且可以扩展到复杂的现实世界中支持学习的CPS。
• 基于统计模型检验(Statiscial Model Checking (SMC)的方法能够克服可扩展性、非线性等障碍，提供概率保证。我们在SMC技术和PAC-learning技术方面的工作的主要区别在于，我们的方法可以为任意数量的样本提供所需的概率保证级别。相反，基于SMC和PAC的方法所提供的保证是样本数量的函数。这是因为我们从系统参数到相应STL属性都对相应的鲁棒满意值建立了一个有保证的回归模型。如果回归模型较差，样本较少，那么使用保形回归中的校准步骤，预测的(因此而较差的)区间仍然可以有相同级别的置信度。
  使用保形回归的主要优点是，在回归模型与数据的吻合程度和我们对高可信属性满意度区间的宽度之间进行权衡，而不是在置信程度本身。

预备知识和背景

系统、轨迹和仿真

• 系统的定义：系统被定义为参数化后确定轨迹的集合。也就是说一旦系统的不确定参数都知道了（如输入，初始配置等）那么参数θ的轨迹 $\xi_\theta$ 也就确定了。
• 这里假设 $\theta$ 是一个随机值，并且服从D$_\theta$分布的概率密度函数p($\theta$)，
  
• 这里假设有一个仿真器能够在独立的轨迹上产生样本数据点.
  
• 定义1就是说，定义一个sim函数，输入是一个参数$\theta$和有限的一系列时间节点，然后仿真输出对应的一系列离散系统状态sim($\theta$,t$_i$)，也就是对应的参数空间$\theta$的真实轨迹状态$\xi_\theta$(t$_i$)，一句话就是用离散仿真采样来表示真实连续的轨迹，记为IplSim($\theta$)
• 信号时序逻辑（STL）简单来说就是用一些谓词定义公式来描述、规范系统在连续时间上具有的一些属性。在之前的读文章中也提到过。
  
  
  表示轨迹$\xi$在时间t满足$\varphi$属性，STL的量化语义就能用作我们要的鲁棒性符合值(RSV),它实际上是将一个函数映射为一个属性，将轨迹$\xi$(t)映射为一个值。
  
• inf是下确界，sup上确界。然后举了一个一维的例子来说明：
  下面的曲线都是动力系统的x$_1$(t)的轨迹，红线是不符合属性的，蓝线是符合属性的
  

保形回归

• 保形回归问题是在对联合分布D不做任何假设的情况下，从一个新的特征值Xm+1预测一个新的响应Ym+1。保形回归算法如下：
  
  其中Reg 是回归模型，可以是线性回归，多项式回归，神经网络。计算出回归参数μ和置信区间d，对于一个新来的Xm+1，就可以进行预测：
  
  能够保证Ym+1在预测区间里的概率是大于等于1-α的。

具有概率覆盖保证的参数搜索和分区

• 预备知识讲完了，这一节就来讨论如何搜索和对参数空间Θ进行分区，分出符合或者不符合给定属性 $\varphi$ 的系统行为。准确的说，是将参数空间分成+(符合),-(不符合),U（不确定）三个子集。理想情况下，U应该接近空集的。
• 方法的核心就是，对$\theta$和 ρ($\varphi$,$\xi_\theta$) 建立回归模型，然后使用保形回归来训练和调整这个回归估值，从而得到一个ρ的预测区间，在这里区间里面是能够保证概率覆盖的。
• 如果对于一个参数空间θ，它里面所有的预测区间(上下界)ρ($\varphi$,$\xi_\theta$) 都是正值/负值，那么它就属于$\theta^+$/$\theta^-$。如果有下界<0，上界>0就继续划分，直到完全能够区分开，或者达到用户规定的阈值，不能再区分那么就划入$\theta^U$。

参数与RSV的保形回归

• 已经给出了属性$\varphi$和一些$\theta$，对于每一个IplSim($\theta$) 都可以根据之前的定义2计算出相应的RSV ρ($\varphi$,IplSim($\xi_\theta$)) .
• θ 和 ρ($\varphi$,IplSim($\xi_\theta$)) 是服从联合分布 D$_{θ,ρ}$ 的。我们想要找到一个连续的预测区间[l,u]，使得新的符合D$_{θ,ρ}$ 的样本的RSV，落入[l,u]的概率是有界的。
• 整理一下，输入属性$\varphi$和m个样本以及他们的仿真结果IplSim(θ)，通过保形算法1，我们能够得到回归估值μ，置信区间d。我们使用的算法是Reg，规定的miscoverage级别是α。
• 所以我们可以计算θ里面所有的μ(θ$_i$)，然从中选出最大的v* max和最小的v* min，又因为新输入的第m+1个样本是在D$_{θ,ρ}$ 中取的，所以可以得到 v* min <= μ(θ$_{m+1}$)<=v*min ，因此可以得到，RSV ρ$_{m+1}$ 是属于区间[v *min - d, v *max + d]的。也就是如下引理：
  
  但是因为u(θ)是非凸函数，闭合过近似算法不能计算出真正的最大最小值，所以要使用优化求解器，SMT求解器，或用于神经网络的可达性工具，来得到最优的最大最小值。 优化如下：
  

整体算法

有了以上引理和推论，我们可以进一步得到：

对于不满足以上的情况，可以进一步将区间化小，然后计算。得到如下算法：

个人觉得这个算法有点没说清楚，就是这个继续将区间划小没有说怎么划分，二分吗？还是又均匀分成多少个区间？看后面的图应该是二分吧，还是个单维度的二分emmmm那这样感觉也没有什么让人感觉巧妙的地方。
下面这个定理就是说，对于每个被划分好的区间，里面的概率是可以保证的。

三个案例

前两个案例用带RL控制器的系统，第三个的控制器是非线性自回归移动平均(nonlinear autoregressive moving average， NARMA)神经网络控制器。都是不用Matlab的toolbox实现的。

Mountain Car

• 动力方程如下,x表示位置(单位米)，v表示速度，F是汽车引擎提供的力，μ摩擦系数，u是控制器：
• $\dot{x}$ = v , $\dot{v}$ = -mg cos(3x) + $\frac{F}{m}u$-μ$\dot{x}$
• 绿色的点是RL控制器能够将车开到山顶的初始条件，红色点是不能。
  
  
  后面两个例子甚至都没有可视化展示，只是描述了一下实验参数和结果= =，然后给了一张表展示了一下。