An Extension of LTL with Rules and its Application to Runtime Verification

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 of propositional LTL, which promote the expressive power to that of Büchi automata, have therefore been proposed; however, none of which was, by and large, adopted for RV. We present an extension of propositional LTL with rules that is as expressive as these extensions, for which preforming RV follows a simple adaptation of classical algorithms. Furthermore, in many practical cases, there is a need in RV to monitor events that carry data, and for which the propositional temporal logic is not sufficient. This problem has been addressed by numerous authors, and in previous work we provided an algorithm for first-order LTL that uses BDDs to represent relations over data elements. We show deficiencies in expressiveness also of first-order LTL and suggest an extension of first-order LTL with rules to address these limitations. We show how to adapt the RV algorithm to allow this extension. We describe how the D EJAV U RV tool is modified to encapsulate the extended algorithm and provide experimental results.