FM2018 Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
（International Symposium on Formal Methods）

摘要

摘要
Introduction
Related work
基础定义
具体算法
评估方法
具体实验
- 汽车模型
其他影响实验的因素
- log-sum-exp 的参数α
- 关于执行时间
总结

摘要

随着软件和分布式计算的迅速发展，信息物理系统（CPS）被广泛应用于许多领域，如智能电网，自动驾驶汽车等。由于软件和物理系统的复杂性，检测CPS模型中的缺陷是困难的，传统的系统验证技术，如模型检验或定理证明，由于物理部件具有无穷多个状态，很难应用于CPS。为了有效地发现CPS模型中的缺陷，引入了以鲁棒性为导向CPS模型性质falsification方法。现有方法使用全局优化技术来生成违反了CPS模型性质的反例。然而，这些方法可能需要大量的模拟运行才能找到反例，往往超出了实际可行性。本文探索最先进的深度强化学习（DRL）技术，以减少查找此类反例所需的模拟运行次数，并讨论了具体方法和初步评估结果。
个人理解就是，如果做图片和文本的对抗样本的话，只需要很直观的添加扰动就可以了，但是做系统的话，需要仿真出一系列的轨迹，就很麻烦，如果用RL的话，可以很自动化的仿真出这样一条轨迹，并且这个轨迹还是能够检测系统缺陷的。

Introduction

传统的用于保证CPS模型正确性的测试方法很难保证测试的高覆盖率，因为状态空间是无限的。可以用测试软件系统的形式化方法诸如模型检测和理论证明来缜密的验证这个系统，但model check是不确定的，因为CPS的状态空间是无限的；而理论证明又非常困难。因此，引入了鲁棒引导证伪[2]、[3]方法来有效地检测CPS中的缺陷。
使用Metric Temporal Logic(MTL)和它的 Signal Temporal Logic (STL)常被用于表示CPS模型应该满足的（鲁棒性）性质，从而数字化度量一个CPS模型的鲁棒性程度，然后通过在CPS模型的状态空间中探索，确定鲁棒性最小的系统参数作为测试的输入参数。通过这种方式，鲁棒性引导的证伪有助于生成缺陷引导系统参数（即反例），从而能够更高效、更自动地检测缺陷。尽管稳健性引导证伪的不终止并不意味着没有反例，这在一定程度上说明了CPS模型的正确性。
现有随机全局优化方法如模拟退火、交叉熵的方法来最小化时序逻辑公式的值。（loss函数？）为了测试CPS，我们需要生成一系列能够使这些系统失败的输入。现有的鲁棒性指导的证伪通常被表示为参数生成问题。输入分为几个控制点，在这些点的输入被视为系统参数。但是这些输入和系统响应之间的时序关系是被丢掉了的，并且代表输入的控制点形成高维空间，在高维空间中进行优化是非常困难的。
在DRL在无功非线性系统（如游戏）上的成功应用的启发下，本文提出将伪造问题作为一个强化学习问题并进行解释，利用DRL的交互学习能力寻找反例。我们关注的是reactive的CPS，即实时从环境中获取输入的CPS。我们采用了两种最先进的强化学习(D RL)技术，即Asynchronous Advanced Actor Critic(A3C)和Double Deep-Q Network(D DQN)，来解决CPS上的鲁棒性引导伪造问题。
本文的主要贡献有：
（1）展示了怎样将找到违反CPS模型鲁棒性性质的行为序列的问题转化为深度强化学习（DRL）问题；
（2）实现提出的方法并进行初步评估，结果证明利用DRL技术可以减少寻找CPS模型致错输入需要的模拟运行次数，进而减少模拟运行的总时间。
（3）提出基于强化学习技术的CPS模型鲁棒性性质falsification问题的测试框架，为进一步探索该问题提供了保障。

Related work

鲁棒性指导的方法分为黑盒方法和灰盒方法。黑盒方法可以进一步分为将鲁棒性伪造问题转化为全局优化问题的方法和基于统计建模的方法。采用全局优化技术的方法包括采用模拟退火的方法、采用遗传算法的方法、Tabu search（禁忌搜索）、梯度下降等。基于统计建模的方法包括交叉熵法、高斯回归。
在控制器合成领域也有采用强化学习(RL)来满足MTL性质的方法。这项任务的挑战之一是如何从给定的公式设计RL中的奖励。一种策略是探索基于自动机的奖励塑造[31]、[32]、[33]。这些方法将MTL公式转换为相应的自动机，并根据自动机的当前状态决定奖励。另一种方法使用MTL的健壮性。控制器生成方法是要将系统一直保持在安全的状态中，但证伪方法是找出系统的漏洞，不同的目的对应了不同的奖励函数设置。

基础定义

我们关注的是能够实时输入并且输出的系统，并且假设输入和输出是发生在一瞬间的离散的时刻。连续的系统可以通过采样来适应离散的系统。这个系统就是一个函数f ：X* -> Y X*是输入的集合，Y是输出。f(x1_11, . . . , xi_ii) = yi+1_{i+1}i+1 ，意思是连续输入i次，输出的结果记为yi+1_{i+1}i+1 。
定义 Dist(x, D) 是输入集合X中的一个点x 到 X的闭合子集D的距离。inf是指下确界。相当于min，但是不是min，最简单的情况如果z是一个开区间的话，可能没有最大最小值，但是是可以有上确界sup和下确界inf的。如果x属于D的话，那么他的下确界是离开这个区域的最短距离，是个正值；如果x不属于D那么他的下确界是到D这个区域的最小距离，但是这里取了负值，表示不在这个区域。（也就是说出了安全区域，就很差了，鲁棒性就为负值。即使在安全区域里面，他离出安全区域越近他的鲁棒性就越低）
然后。定义了鲁棒性数值的衡量 degree[[φ]] (y,t) 表示输出信号y在时间t对φ的鲁棒性
φ是一个MTL-formula，他的规则如下所示，直观的说就是，yn_nn这个状态满足p这个属性。当然还可以进行一些与、或等逻辑判别。定义1：y是系统的输出，n是表示经历了n个x的输入，如tn_nn,表示的这个时间瞬间。t = t0_00…tn_nn…表示的是这个系统状态的无限采样的时间序列。 y=y0_00，y1_11，…，yn_nn，…分别为时间瞬间的系统状态。y, n |= φ 表示yn_nn满足φ这个属性。
同时还引用其他文章中未来可到达 fr§ 的定义，表示未来确定p这个属性是真值所需要的最小时间。如果fr§=0的话就表示，这属性是"单纯的过去依赖"属性，意思就是过去的状态已经能够满足这个属性了。他这里举的例子的意思是，如果p已经确定为真，fr§=0，要确定在之后的0~3秒里面p都是真，要第三秒才能知道；要确定从当前时间之前的-3秒到0秒里面p是真在第0秒就能知道了(因为他fr§=0了嘛表示当前已经满足了，所以最晚也是第0秒就能知道)
紧接着我们需要定义一个monitoring formula。因为我们希望关心的安全属性不是一个单纯的过去依赖，也就是说，不是一个只满足某个瞬间的状态，而是一定时间内能满足的，这个monitoring formual φ0_00相当于属性φ的一个近似，而文中为了简化问题，将φ0_00定义为单纯的过去依赖的，也就是可以立即判别的。

具体算法

文章使用了两种强化学习算法 Asynchronous Advantage Actor-Critic (A3C) 和Double Deep Q Network (DDQN)。A3C主要就是将原本的DQN分成了两部分，Actor学习动作和Critic学习值函数估值，两个互相独立的神经网络，但是Critic会影响Actor。DDQN主要是为了解决DQN的过估计问题，弄了两个一模一样的网络，在学习估值的时候用max来做评估，在选择输出动作的时候用另一个没有做过max 评估的权重集合来做动作，一定程度上降低了过估计的可能性，对动作选择和动作估值进行解耦，收敛更平滑。（文章只做了简要介绍，没有具体展开，感觉需要再写一篇来专门学习这几个算法才能彻底弄懂，因为本身也是原始DQN的优化算法，所以暂时就默认他们作为DL的作用）
给定安全属性φ，以及它的monitoring formual φ0_00，系统和主体，我们的目的是输出一个x集合，使得执行完x里面的动作后，系统的输出是不符合安全属性的。每次对系统进行L步的仿真，如果最后结果里面有状态是不安全的，那么就把这组输入保存下来作为一个对抗样本，否则就在保留主体记忆的情况下又从头开始仿真学习。其中，仿真的步数L和进行的轮数N是可以自主设定的参数。
reward的定义如下，直观的讲就是对当前输出进行评价，如果鲁棒性越小，reward就越大。

评估方法

一共做了三个实验的对比实验（随机均匀采样）uniform random sampling (RAND), （交叉熵）Cross Entropy (CE) and （模拟退火)Simulated Annealing (SA)。将随机采样作为本次实验的目标基准线，所有的实验结果和它进行比较之后的结果作为不同方法好坏的判断标准。后面两种方法不太了解emmmm应该还需要继续学习才能明白。
此外计算200轮中成功找到对抗样本的比例和找到对抗样本轮数的中位数。使用中位数而不是平均数的原因是，伪造所需轮数的分布高度不正常，因此平均没有意义。
但以上两种方法不足以反应结果的分布差异还采用了一个“相对效应大小”度量方法，有两个随机数X和Y，为了比较他们两个谁的范围更大，就求X小于Y的概率：p如果小于0.5，说明X<Y小的概率很小，那么X大部分情况比Y大。
而我们这里想知道，在比较方法A和B的时候，A比B表现更好的频率有多高，而平均值和中位数，只是在强有力的假设下间接的说明这个问题，是不够直观的。

具体实验

作者们做了三个实验，每个实验工作量一个比一个庞大= =，这里只以第一个相对简单的实验介绍一下

汽车模型

如上图所示，这个模型输入是Throttle (节气门？)向量和 Brake（制动器）值。输出五个参数包括速度等。然后根据属性的复杂性定义了如下几个等级的属性（eg,φ4_44表示了系统续航力，φ5_55体现了系统的反应能力等）：
对于两个强化学习算法的实验，还分别作了黑盒和白盒的测试，这里文章只提了一句话说，白盒是能观察到完整的输出y1~ y5，黑盒只能观察到鲁棒性结果。后面解释了= =是指的强化学习算法中，每次仿真完系统，白盒会得到y1~y5的作为yi_ii进行学习即整个系统的状态，但黑盒是使用的yi_ii的鲁棒性数值不能观察到系统的整个状态。下图表示的是成功找到对抗样本的比例：
下面这张是模型成功次数的中位数及其可视化。TABLE4和TABLE5是之前提到的“相对效应大小”来比较两种方法谁有更高的概率性能更优。表中的值越小，就说明列方法比行方法更小，更集中->也就是说伪造成功的次数越低。（其实可视化的图已经很直观了= =）

其他影响实验的因素

log-sum-exp 的参数α

通过实验得出，整体而言阿尔法不会对结果造成很大影响。

关于执行时间

因为还要考虑不同方法使用的语言差异，环境差异等这里使用仿真次数作为单位来衡量执行时间，因为执行一步主要时间其实是在仿真上面的，迭代次数越少，总执行时间就会越少。同时也评估了Δ\DeltaΔT执行时间的影响，如果有影响的话小的Δ\DeltaΔT就会使学习的迭代次数增加那么，就也会更慢，但实验证明并没有大影响（除了φ\varphiφ5_55，文章解释说应该是因为这个属性只需要非常少的模拟次数，所以初始化开销占了大部分执行时间。没太懂，感觉这里的意思是执行时间还是真实的时间，只是计量单位用的仿真次数）。这样也是为了尽量避免因为执行环境和选取的编程语言带来的差异。

总结

提出了一种生成信息物理系统（CPS）对抗样本的强化学习方法
并且展示了如何将一个CPS对抗样本生成问题转化成强化学习问题
进行了实验对比了多种不同方法和RL方法的差异，并且使用“相对影响大小”的方法来进行分析。并且找到了影响RL结果两个因素：是否能观察的整个系统的结果以及输入结构，另一个因素是伪造输入中存在可学习的结构。

【阅读笔记】Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning相关推荐

Deep Reinforcement Learning for Sepsis Treatment文献阅读记录
Deep Reinforcement Learning for Sepsis Treatment 1 Introduction 本文所提出的是一种基于深度强化学习的脓毒症治疗方法. 使用强化学习而非有 ...
论文阅读：DRN: A Deep Reinforcement Learning Framework for News Recommendation
文章目录摘要一.Introduction 1.引入原因 2.结构框架二.相关工作 1.新闻推荐算法 2.推荐中的强化学习 3.问题定义三.实现原理 1.模型框架 2.特征构造 3.深度强化推荐 ...
AutoML论文笔记（十四）Automatic Data Augmentation via Deep Reinforcement Learning for Effective Kidney Tumor
文章题目:Automatic Data Augmentation via Deep Reinforcement Learning for Effective Kidney Tumor Segmenta ...
论文笔记之：Action-Decision Networks for Visual Tracking with Deep Reinforcement Learning
论文笔记之:Action-Decision Networks for Visual Tracking with Deep Reinforcement Learning 2017-06-06 21: ...
算法笔记：Playing Atari with Deep Reinforcement Learning
Playing Atari with Deep Reinforcement Learning 比较尴尬,上篇文章不是DQN的来源,这篇才是.上篇Nature文章对于DQN做出的改进上次没读明白,查看其 ...
论文笔记（十六）：Learning to Walk in Minutes Using Massively Parallel Deep Reinforcement Learning
Learning to Walk in Minutes Using Massively Parallel Deep Reinforcement Learning 文章概括摘要 1 介绍 2 大规模并 ...
【论】A Deep Reinforcement Learning Framework for Rebalancing Dockless Bike Sharing Systems
A Deep Reinforcement Learning Framework for Rebalancing Dockless Bike Sharing Systems 摘要自行车共享为旅行提供了 ...
【论文阅读】DouZero: Mastering DouDizhu with Self-Play Deep Reinforcement Learning
[论文阅读]DouZero: Mastering DouDizhu with Self-Play Deep Reinforcement Learning 1 本文解决了什么问题? 斗地主是一个非常具有 ...
Deep Reinforcement Learning for Task Offloading in Mobile Edge Computing Systems
Deep Reinforcement Learning for Task Offloading in Mobile Edge Computing Systems 移动边缘计算系统中任务卸载的深度强化学 ...

【阅读笔记】Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning

摘要

摘要