论文标题
时间逻辑查询对有限数据流进行检查
Temporal-Logic Query Checking over Finite Data Streams
论文作者
论文摘要
本文介绍了一种用于推断有限数据流集的时间逻辑属性的技术。此类数据流在许多域中出现，包括服务器日志，程序测试以及财务和营销数据；集合中所有数据流满足的时间逻辑公式都可以洞悉生成这些流的系统的基本动力学。我们的方法利用了所谓的线性时间逻辑（LTL）查询，该查询是包含缺失子形式的LTL公式，并通过有限的数据流进行解释。求解这样的查询涉及计算可以插入查询中的子形式，以便集合中的所有数据流都满足所得的接地公式。我们描述了一种自动驱动的方法来解决此查询检查问题，并通过试点研究证明了工作实施。
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.
