An Extension Of Ltl With Rules And Its Application To Runtime Verification
RUNTIME VERIFICATION, RV 2019(2019)
摘要
Runtime Verification (RV) consists of analyzing execution traces using formal techniques, e.g., monitoring executions against Linear Temporal Logic (LTL) properties. Propositional LTL is, however, limited in expressiveness, as first shown by Wolper [32]. Several extensions to propositional LTL, which promote the expressive power to that of regular expressions, have therefore been proposed; however, none of which was, by and large, adopted for RV. In addition, for many practical cases, there is a need in RV to monitor properties that carry data. This problem has been addressed by numerous authors, and in previous work we addressed this by providing an algorithm that uses BDDs to represent relations over data elements. We show expressiveness deficiencies of first-order LTL and suggest an extension of (propositional as well as first-order) LTL with rules to address these limitations. We describe how the DEJAVU tool is correspondingly extended and provide some experimental results.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络