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(x${}_1$, . . . , x${}_i$) = y${}_{i+1}$ ，意思是連續輸入i次，輸出的結果記為y${}_{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，他的規則如下所示，直觀的說就是，y${}_n$這個狀態滿足p這個屬性。當然還可以進行一些與、或等邏輯判別。定義1：y是系統的輸出，n是表示經歷了n個x的輸入，如t${}_n$,表示的這個時間瞬間。t = t${}_0$…t${}_n$…表示的是這個系統狀態的無限采樣的時間序列。 y=y${}_0$，y${}_1$，…，y${}_n$，…分別為時間瞬間的系統狀態。y, n |= φ 表示y${}_n$滿足φ這個屬性。
  
• 同時還引用其他文章中 未來可到達 fr§ 的定義，表示未來確定p這個屬性是真值所需要的最小時間。如果fr§=0的話就表示，這屬性是"單純的過去依賴"屬性，意思就是過去的狀態已經能夠滿足這個屬性了。他這里舉的例子的意思是，如果p已經確定為真，fr§=0，要確定在之后的0~3秒里面p都是真，要第三秒才能知道；要確定從當前時間之前的-3秒到0秒里面p是真在第0秒就能知道了(因為他fr§=0了嘛表示當前已經滿足了，所以最晚也是第0秒就能知道)
  
• 緊接著我們需要定義一個monitoring formula。因為我們希望關心的安全屬性不是一個單純的過去依賴，也就是說，不是一個只滿足某個瞬間的狀態，而是一定時間內能滿足的， 這個monitoring formual φ${}_0$相當于屬性φ的一個近似，而文中為了簡化問題，將φ${}_0$定義為 單純的過去依賴的，也就是可以立即判別的。

具體算法

• 文章使用了兩種強化學習算法 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$， 系統和主體，我們的目的是輸出一個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$表示了系統續航力，φ${}_5$體現了系統的反應能力等）：
  
• 對于兩個強化學習算法的實驗，還分別作了黑盒和白盒的測試，這里文章只提了一句話說，白盒是能觀察到完整的輸出y1~ y5，黑盒只能觀察到魯棒性結果。后面解釋了= =是指的強化學習算法中，每次仿真完系統，白盒會得到y1~y5的作為y${}_i$進行學習即整個系統的狀態，但黑盒是使用的y${}_i$的魯棒性數值不能觀察到系統的整個狀態。下圖表示的是成功找到對抗樣本的比例：
  
• 下面這張是模型成功次數的中位數及其可視化。TABLE4和TABLE5是之前提到的“相對效應大小”來比較兩種方法誰有更高的概率性能更優。表中的值越小，就說明列方法比行方法更小，更集中->也就是說偽造成功的次數越低。（其實可視化的圖已經很直觀了= =）
  
  

其他影響實驗的因素

log-sum-exp 的參數α

通過實驗得出，整體而言阿爾法不會對結果造成很大影響。

關于執行時間

• 因為還要考慮不同方法使用的語言差異，環境差異等這里使用仿真次數作為單位來衡量執行時間，因為執行一步主要時間其實是在仿真上面的，迭代次數越少，總執行時間就會越少。同時也評估了$\Delta$T執行時間的影響，如果有影響的話小的$\Delta$T就會使學習的迭代次數增加那么，就也會更慢，但實驗證明并沒有大影響（除了$\phi$${}_5$，文章解釋說應該是因為這個屬性只需要非常少的模擬次數，所以初始化開銷占了大部分執行時間。沒太懂，感覺這里的意思是執行時間還是真實的時間，只是計量單位用的仿真次數）。這樣也是為了盡量避免因為執行環境和選取的編程語言帶來的差異。

總結

• 提出了一種生成信息物理系統（CPS）對抗樣本的強化學習方法
• 并且展示了如何將一個CPS對抗樣本生成問題轉化成強化學習問題
• 進行了實驗對比了多種不同方法和RL方法的差異，并且使用“相對影響大小”的方法來進行分析。并且找到了影響RL結果兩個因素：是否能觀察的整個系統的結果以及輸入結構，另一個因素是偽造輸入中存在可學習的結構。

總結

以上是生活随笔為你收集整理的【阅读笔记】Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。