Automata-based monitoring for LTL-FO~+

摘要

We present an automata-based runtime verification procedure for LTL-FO+ properties. LTL-FO+ is an extension of LTL that includes first-order quantification over bounded variables, thus greatly increasing the expressivity of the language. We show how to construct an automata representation of an LTL-FO+ property which allows runtime verification using a breadth-first search throughout the automata, and we prove the correctness of the construction. Finally, we introduce Pelota, an automata-based monitor for LTL-FO+, and show empirical results of its use on sample properties. Compared with an existing monitor for LTL-FO+, Pelota exhibits better time and space consumption, especially on memory-intensive properties.