Temporal-Logic Query Checking over Finite Data Streams
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.
Cite
@article{arxiv.2006.03751,
title = {Temporal-Logic Query Checking over Finite Data Streams},
author = {Samuel Huang and Rance Cleaveland},
journal= {arXiv preprint arXiv:2006.03751},
year = {2020}
}