# Temporal-Logic Query Checking over Finite Data Streams

arXiv: https://arxiv.org/abs/2006.03751 · HTML: https://mlsanity.com/paper/2006.03751/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Jun 2020.

## Built on by (most cited first, 2 of 2)

- [Interactive Explanations for Reinforcement-Learning Agents](https://mlsanity.com/paper/2504.05393/) (2025)
- [ASQ-IT: Interactive Explanations for Reinforcement-Learning Agents](https://mlsanity.com/paper/2301.09941/) (2023)

## Abstract (arXiv)

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.