Temporal-Logic Query Checking over Finite Data Streams

Abstract

This paper describes a technique for solving temporal-logic queries over finite sets of finite-length data streams. Such data streams arise in many domains, including server logs, program testing, and financial and marketing data; temporal-logic formulas that are satisfied by all data streams in a set can provide insight into the underlying dynamics of the system generating the streams. Our approach to finding such formulas involves queries, or formulas that include an unknown, given in a variant of Linear Temporal Logic (LTL). Solving such a query involves computing all propositional formulas that, when substituted for the unknown in the query, yield an LTL formula satisfied by all data streams in the set. We give an automaton-based approach to solving these queries and demonstrate a working implementation via a pilot study.