LTLf

深度分析

結合 LTLf 與 SMT 的可預期資料感知時序監測框架

面對黑盒且異質的動態系統，傳統設計時驗證難以適用。本文改寫的研究提出一個可預期（anticipatory）的監測框架，針對以理論豐富的 LTLf 模組化 SMT（LTL_M_T_f）為規格的屬性進行監控。方法結合自動機處理時間邏輯與 SMT 求解器處理第一階資料約束，並以保守擴展的模型延伸（embeddings）處理追蹤連續性。