Mining specifications from execution traces presents an automated way of capturing characteristic system behaviors. However, existing approaches are largely restricted to Boolean abstractions of events, limiting their ability to express data-aware properties. In this paper, we extend mining procedures to operate over richer datatypes. We first establish candidate functions in our domain that cover the set of traces by leveraging Syntax Guided Synthesis (SyGuS) techniques. To capture these function applications temporally, we formalize the semantics of TSL$_f$, a finite-prefix interpretation of Temporal Stream Logic (TSL) that extends LTL$_f$ with support for first-order predicates and functional updates. This allows us to unify a corresponding procedure for learning the data transformations and temporal specifications of a system. We demonstrate our approach synthesizing reactive programs from mined specifications on the OpenAI-Gymnasium ToyText environments, finding that our method is more robust and orders of magnitude more sample-efficient than passive learning baselines on generalized problem instances.

翻译：从执行轨迹中挖掘规约为捕获系统特征行为提供了一种自动化方法。然而，现有方法主要局限于事件的布尔抽象，限制了其表达数据感知属性的能力。本文扩展了挖掘过程，使其能够在更丰富的数据类型上操作。我们首先利用语法引导综合（SyGuS）技术，在领域内建立覆盖轨迹集的候选函数。为了在时间维度捕获这些函数应用，我们形式化定义了TSL$_f$的语义——这是一种时序流逻辑（TSL）的有限前缀解释，通过支持一阶谓词和函数更新扩展了LTL$_f$。这使我们能够统一学习系统数据转换与时间规约的对应流程。我们在OpenAI-Gymnasium ToyText环境中演示了从挖掘规约合成反应式程序的方法，发现相较于被动学习基线，我们的方法在泛化问题实例上具有更强鲁棒性，且样本效率高出数个数量级。