从执行轨迹中自动挖掘数据敏感的时序规范，提升系统行为建模能力。
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
- 利用语法引导合成技术生成覆盖轨迹的数据函数
- 提出TSL$_f$逻辑，支持一阶谓词与函数更新的时序表达
- 在强化学习环境上实现高效且鲁棒的程序合成
从执行轨迹中挖掘规范是一种自动化捕捉系统特征行为的方法。然而，现有方法大多局限于事件的布尔抽象，难以表达依赖数据的性质。本文将挖掘过程扩展至更丰富的数据类型：首先利用语法引导合成（SyGuS）技术构建覆盖所有轨迹的候选函数；为捕获函数的时序应用，形式化定义了TSL$_f$——一种有限前缀的时序流逻辑，其在LTL$_f$基础上支持一阶谓词和函数更新。该框架统一了数据变换与时序规范的学习流程。我们在OpenAI-Gymnasium ToyText环境中验证了该方法，通过挖掘规范合成反应式程序，结果表明，该方法在泛化问题实例上比被动学习基线更鲁棒，且样本效率高出数个数量级。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。