Temporal-Logic Query Checking over Finite Data Streams

TL;DR

This paper presents a novel automaton-based method for inferring and checking temporal-logic properties over finite data streams, aiding understanding of complex system behaviors in various domains.

Contribution

It introduces a new approach for inferring temporal-logic properties using LTL queries with missing subformulas over finite data streams, with an implementation demonstrating its feasibility.

Findings

Automaton-driven approach effectively solves query-checking problems.

Implementation successfully infers properties from real data streams.

Method applicable to diverse domains like server logs and financial data.

Abstract

This paper describes a technique for inferring temporal-logic properties for sets of finite 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 these streams. Our approach makes use of so-called Linear Temporal Logic (LTL) queries, which are LTL formulas containing a missing subformula and interpreted over finite data streams. Solving such a query involves computing a subformula that can be inserted into the query so that the resulting grounded formula is satisfied by all data streams in the set. We describe an automaton-driven approach to solving this query-checking problem and demonstrate a working implementation via a pilot study.