核心概念
本文提出了離線離散時間監測算法,包含加速啟發式,用於布爾監測和定量健壯性監測。加速啟發式在子公式成立的時間區間上操作,而非原始軌跡的採樣點。這是第一個實現具有嵌套凍結變量的STL*公式監測算法的工作。
摘要
本文介紹了值凍結信號時間邏輯(STL*)及其監測問題。STL*通過引入值凍結運算子,增強了信號時間邏輯(STL)的表達能力,可以描述工程中常見的性質,如振蕩性質。
作者提出了離線離散時間監測算法,包括布爾監測和定量健壯性監測。算法使用加速啟發式,在子公式成立的時間區間上操作,而非原始軌跡的採樣點。這樣可以顯著減少計算量。
具體來說,對於包含|V|個凍結變量的公式φ,檢查軌跡π是否滿足φ,需要考慮|π||V|種可能的凍結變量綁定。作者提出,無需遍歷所有時間點,而是可以遍歷這些子公式成立的時間區間,這些區間數量遠小於時間點數量。這樣可以將複雜度從|π||V|+1降低到|π||V|·max(log(|π|), |φ|·|intvl(φ)|)。
對於定量健壯性監測,直接使用區間的想法不可行,因為從一個凍結綁定到下一個,健壯性值會發生變化。但作者提出使用二分搜索計算健壯性值的下界和上界,並使用這個範圍來解決健壯性決策問題。
作者實現了這些算法,並進行了實驗驗證。結果表明,對於包含兩個嵌套凍結變量的公式,布爾監測在10k軌跡上耗時約3分鐘,健壯性值計算在17分鐘內完成(最終結果在2%誤差範圍內)。對於三個嵌套凍結變量,在500軌跡上耗時約2.5分鐘,1k軌跡上耗時約22分鐘。這是首次實現對具有嵌套凍結變量的STL*公式進行監測的工作。
統計資料
以下是一些重要數據:
對於10k軌跡,包含兩個嵌套凍結變量的公式的布爾監測耗時約3分鐘
對於10k軌跡,包含兩個嵌套凍結變量的公式的健壯性值計算耗時約17分鐘,最終結果在2%誤差範圍內
對於500軌跡,包含三個嵌套凍結變量的公式的布爾監測耗時約2.5分鐘
對於1k軌跡,包含三個嵌套凍結變量的公式的布爾監測耗時約22分鐘
引述
"本文提出的加速啟發式在子公式成立的時間區間上操作,而非原始軌跡的採樣點,這樣可以顯著減少計算量。"
"這是首次實現對具有嵌套凍結變量的STL*公式進行監測的工作。"