Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

Sam Nicholas Kouteili, William Fishell, Christian Scaff, Mark Santolucito, Ruzica Piskac

TL;DR

The semantics of TSL$_f$ is formalized, a finite-prefix interpretation of Temporal Stream Logic that extends LTL$_f$ with support for first-order predicates and functional updates that allows for synthesizing reactive programs from mined specifications on OpenAI-Gymnasium ToyText environments.

Abstract

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.

Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

TL;DR

The semantics of TSL is formalized, a finite-prefix interpretation of Temporal Stream Logic that extends LTL with support for first-order predicates and functional updates that allows for synthesizing reactive programs from mined specifications on OpenAI-Gymnasium ToyText environments.

Abstract

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, a finite-prefix interpretation of Temporal Stream Logic (TSL) that extends LTL 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.
Paper Structure (22 sections, 1 theorem, 8 equations, 6 figures, 9 tables, 4 algorithms)

This paper contains 22 sections, 1 theorem, 8 equations, 6 figures, 9 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Formalisms
  4. Syntax
  5. Semantics
  6. Realizability
  7. Mining Procedure
  8. Function Discovery
  9. Lifting Well-Formed Traces
  10. Learning Specifications
  11. Evaluation
  12. Related Works
  13. Conclusion
  14. Thm.1 proof. TSL$_f$ is strictly less expressive than TSL.
  15. Trace Generation
  16. ...and 7 more sections

Key Result

theorem 1

TSL$_f$ is strictly less expressive than TSL

Figures (6)

  • Figure 1: FrozenLakeopenai2016gym. Two positive (green) and two negative (red) traces.
  • Figure 2: OpenAI-Gymnasium FrozenLake game trace. Each line represents a timestep and encodes environment state. x and y refer to player coordinates, gX and gY to the goal coordinates, and h*X and h*Y to obstacle coordinates.
  • Figure 3: Function discovery procedure. After choosing input-output pairs, the SyGuS solver determines unique functions for each constraint. Constraints are merged by their synthesized functions, at which point smaller constraint sets attempt to merge into larger ones, eliminating spurious functions.
  • Figure 4: Constructing well-formed TSL$_f$ traces. Having learned the functions of our system, we model a valid interpretation of system behavior. For the trace to be well-formed, each variable must only have one update (until the last timestep).
  • Figure 5: Full OpenAI-Gym ToyText openai2016gym suite. We evaluate on generalized instances. Left to right: FrozenLake, CliffWalking, Taxi, and Blackjack.
  • ...and 1 more figures

Theorems & Definitions (2)

  • theorem 1
  • proof