Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

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

cs.LOMar 5, 2026

Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

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

Organizations: Yale University · Columbia University · Barnard College, Columbia University

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.

Figures & tables

Panel of Figure 1 — Figure 1: FrozenLake [ 11 ] . Two positive (green) and two negative (red) traces.

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 [ 11 ] suite. We evaluate on generalized instances. Left to right: FrozenLake , CliffWalking , Taxi , and Blackjack .

Figure 6: FrozenLake varied configuration results. Specification mining is more sample-efficient and generalizes better than imitation learning baselines.

Method	Train	Test	4	8	12	16	20	50	100	500	1000
SpecMining(TSL f )	fixed	var_conf	24	42	50	50	50	-	-	-	-
	var_conf	var_conf	45	50	50	50	50	-	-	-	-
	fixed	var_size	24	50	50	50	50	-	-	-	-
	var_size	var_size	42	50	50	50	50	-	-	-	-
Alergia(SMM)	fixed	var_conf	24	23	21	22	21	22	24	24	21
	var_conf	var_conf	20	22	14	25	29	26	33	34	42

Table 1: FrozenLake win rates (out of 50 test instances). var_conf : fixed

4\times 4

board with varied hole/goal positions. var_size :

3\times 3

5\times 5

boards with varied positions. Columns show number of training samples.

Method	Liveness	Safety
TSL f	$\mathbf{F}\,((\texttt{eq}\,x\,\texttt{goalx})\land(\texttt{eq}\,y\,\texttt{goaly}))$	$\mathbf{G}\,\neg((\texttt{eq}\,x\,\texttt{hole1x})\land(\texttt{eq}\,y\,\texttt{hole1y}))$
		$\mathbf{G}\,(((\texttt{eq}\,x\,\texttt{hole0x})\land(\texttt{eq}\,y\,\texttt{hole0y}))\leftrightarrow(((\texttt{eq}\,x\,\texttt{hole1x})\land(\texttt{eq}\,y\,\texttt{hole1y}))))$
		$\mathbf{G}\,(((\texttt{eq}\,x\,\texttt{hole2x})\land(\texttt{eq}\,y\,\texttt{hole2y}))\leftrightarrow(((\texttt{eq}\,x\,\texttt{hole0x})\land(\texttt{eq}\,y\,\texttt{hole0y}))\lor((\texttt{eq}\,x\,\texttt{hole1x})\land(\texttt{eq}\,y\,\texttt{hole1y}))))$
LTL-BB	$\mathbf{F}\,(\texttt{x\_b1})$	$\mathbf{G}\,((\mathbf{X}\,\texttt{goalX\_b2})\to(\texttt{x\_b1}))$
	$\mathbf{F}\,((\texttt{y\_b0})\land(\mathbf{X}\,\texttt{x\_b1}))$	$\mathbf{G}\,((\texttt{y\_b0})\to((\texttt{y\_b1})\leftrightarrow(\mathbf{X}\,\texttt{y\_b0})))$
	$\mathbf{F}\,(\mathbf{G}\,((\texttt{y\_b0})\land(\texttt{y\_b1})))$	$\mathbf{G}\,((\mathbf{X}\,\texttt{goalX\_b2})\to((\texttt{y\_b0})\land(\texttt{y\_b1})))$

Table 2: Unique specifications found by TSL f and LTL-BB on FrozenLake .

Method	Train	Test	4	8	12	16	20	50	100	200	500	1000
SpecMining(TSL f )	fixed	var_size	17	17	17	17	17	-	-	-	-	-
	var_size	var_size	50	50	50	50	50	-	-	-	-	-
	var_mov_fixed	var_size	17	17	17	17	17	-	-	-	-	-
	var_mov_size	var_size	0	50	50	50	50	-	-	-	-	-
Alergia(SMM)	fixed	var_size	19	21	22	22	21	20	18	19	20	20
	var_size	var_size	50	50	50	50	50	50	50	50	50	50

Table 3: CliffWalking win counts from training over fixed boards and varied board configurations. Test on 50 var_size instances (cliff height

h\in[1,3]

, board width

w\in[3,12]

, board length

l\in[4,6]

Method	Liveness	Safety
TSL f	$\mathbf{F}\,((\texttt{eq}\,x\,\texttt{goalx})\land(\texttt{eq}\,y\,\texttt{goaly}))$	$\mathbf{G}\,((\texttt{eq}\,x\,\texttt{goaly})\lor((\texttt{eq}\,y\,\texttt{goaly})\to(\texttt{eq}\,x\,\texttt{goalx})))$
		$\mathbf{G}\,((\texttt{eq}\,x\,\texttt{goalx})\lor((\texttt{lt}\,y\,\texttt{cliffHeight})\to(\texttt{eq}\,x\,\texttt{goalx})))$
LTL-BB	$\mathbf{F}\,(\mathbin{\mathbf{G}}((\texttt{x\_b0})\land(\texttt{x\_b1})))$	$\mathbf{G}\,((\mathbf{X}\,\texttt{cliffHeight\_b1})\to((\texttt{x\_b0})\land(\texttt{x\_b1})))$
	$\mathbf{F}\,(\mathbin{\mathbf{G}}((\texttt{x\_b0})\land(\texttt{x\_b3})))$	$\mathbf{G}\,((\mathbf{X}\,\texttt{cliffHeight\_b1})\to((\texttt{x\_b0})\land(\texttt{x\_b3})))$
	$\mathbf{F}\,(\neg((\mathbf{X}\,\texttt{x\_b3})\to(\texttt{y\_b1})))$	$\mathbf{G}\,((\mathbf{X}\,\texttt{cliffHeight\_b2})\to(\texttt{x\_b3}))$

Table 4: Unique specifications found by TSL f and LTL-BB on CliffWalking .

Method	Train	Test	4	8	12	16	20	50	100	200	500	1000
SpecMining(TSL f )	fixed	var_pos	2	31	50	50	50	-	-	-	-	-
SpecMining(TSL f )	var_pos	var_pos	2	50	50	50	50	-	-	-	-	-
Alergia(SMM)	fixed	var_pos	14	19	5	14	17	14	17	17	23	19
Alergia(SMM)	var_pos	var_pos	27	27	23	18	23	29	32	28	30	31
BehavClon(NN)	fixed	var_pos	0	0	0	1	0	0	2	1	0	0
BehavClon(NN)	var_pos	var_pos	2	4	3	12	0	9	9	14	17	14

Table 5: Taxi win counts from training over fixed boards and varied board configurations. Test on 50 var_pos instances, varying the wall, passenger, and destinations positions.

*

implies a dual-stage system with two baselines chained.

Method	Liveness	Safety
TSL f	$\mathbf{F}\,(\texttt{eq}\,x\,\texttt{DEST\_x}\land\texttt{eq}\,y\,\texttt{DEST\_y})$	$\mathbf{G}\,(\texttt{eq}\,x\,\texttt{YELLOW\_x}\land\texttt{eq}\,y\,\texttt{YELLOW\_y})$
	$\mathbf{F}\,((\texttt{eq}\,x\,\texttt{RED\_X}\land\texttt{eq}\,y\,\texttt{RED\_Y})\land\mathbf{F}\,(\texttt{eq}\,x\,\texttt{DEST\_X}\land\texttt{eq}\,y\,\texttt{DEST\_Y}))$	$\mathbf{G}\,((\texttt{eq}\,x\,\texttt{RED\_X}\land\texttt{eq}\,y\,\texttt{RED\_Y})\leftrightarrow(\texttt{eq}\,x\,\texttt{YELLOW\_X}\land\texttt{eq}\,y\,\texttt{YELLOW\_Y}))$
LTL-BB	$\mathbf{F}\,((\texttt{x\_b0})\leftrightarrow(\texttt{RED\_x\_b1}))$	$\mathbf{G}\,((\texttt{x\_b0})\leftrightarrow(\texttt{RED\_x\_b1}))$
	$\mathbf{F}\,((\texttt{DEST\_x\_b1})\leftrightarrow(((\texttt{DEST\_y\_b0})\leftrightarrow(\texttt{RED\_y\_b1}))\to(\texttt{DEST\_x\_b0})))$	$\mathbf{G}\,((\texttt{DEST\_x\_b1})\leftrightarrow(((\texttt{DEST\_y\_b0})\leftrightarrow(\texttt{RED\_y\_b1}))\to(\texttt{DEST\_x\_b0})))$

Table 6: Unique specifications mined by TSL f and LTL-BB on Taxi . LTL-BB mining times out for

n\geq 12

Method	Strategy	4	8	12	16	20
SpecMining(TSL f )	Threshold	50 (22)	50 (22)	50 (22)	50 (22)	50 (22)
	Conservative	50 (24)	40 (22)	50 (24)	50 (24)	50 (24)
	Basic	44 (22)	44 (22)	50 (25)	50 (25)	50 (25)
Alergia(SMM)	Threshold	50 (22)	50 (22)	50 (22)	50 (22)	50 (22)
	Conservative	50 (24)	50 (24)	50 (24)	50 (24)	50 (24)
	Basic	44 (22)	50 (25)	50 (25)	50 (25)	50 (25)

Table 7: Strategy adherence (win rate) on Blackjack for different training set sizes on 50 instances. As strategy becomes more complex, win rates improve.

Method	Strategy	Safety Specification
TSL f	Threshold	$\mathbf{G}\,\neg((\texttt{lt}\,\texttt{c}\,\texttt{sThresh})\leftrightarrow(\mathbf{X}\,\texttt{stood}))$
	Conservative	$\mathbf{G}\,((\texttt{lt}\,\texttt{c}\,\texttt{sThresh})\to(\mathbf{X}\,((\texttt{lt}\,\texttt{c}\,\texttt{sThresh})\leftrightarrow(((\texttt{gte}\,\texttt{dealer}\,\texttt{lo})\land(\texttt{lte}\,\texttt{dealer}\,\texttt{med}))\lor(\texttt{lt}\,\texttt{c}\,\texttt{sWeak})))))$
	Conservative	$\mathbf{G}\,\neg((\mathbf{X}\,\texttt{stood})\leftrightarrow((\texttt{lt}\,\texttt{c}\,\texttt{sThresh})\land(((\texttt{gte}\,\texttt{dealer}\,\texttt{lo})\land(\texttt{lte}\,\texttt{dealer}\,\texttt{med}))\to(\texttt{lt}\,\texttt{c}\,\texttt{sWeak}))))$
	Basic	$\mathbf{G}\,((\texttt{lt}\,\texttt{c}\,\texttt{sWeak})\lor(\mathbf{X}\,((\texttt{eq}\,\texttt{c}\,\texttt{sWeak})\leftrightarrow[\texttt{c}\leftarrow\texttt{c}])))$
	Basic	$\mathbf{G}\,\neg((\mathbf{X}\,\texttt{stood})\leftrightarrow((\texttt{lt}\,\texttt{c}\,\texttt{sThresh})\land(((\texttt{gte}\,\texttt{dealer}\,\texttt{lo})\land(\texttt{lte}\,\texttt{dealer}\,\texttt{med}))\to(\texttt{lt}\,\texttt{c}\,\texttt{sWeak}))))$
LTL-BB	Threshold	$\mathbf{G}\,((\texttt{c\_b4})\to(\mathbf{X}\,\texttt{stood}))$

Table 8: Specifications mined by TSL f and LTL-BB on Blackjack . Legend: c

=

player card total, lo

=

2, med

=

6, sThresh

=

17, sWeak

=

12.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Game	Method	4	8	12	16	20	50	100	500	1000
FrozenLake	TSL f	3.1	2.2	3.0	3.8	5.0	–	–	–	–
	Alergia	$<$ .01	$<$ .01	$<$ .01	$<$ .01	$<$ .01	.02	.03	.18	.27
	BehavClone	.23	.54	1.1	1.6	1.3	3.1	5.0	29	58
	CART	$<$ .01	$<$ .01	$<$ .01	$<$ .01	$<$ .01	$<$ .01	$<$ .01	.09	.13
CliffWalking	TSL f	14	8.9	9.8	12	11	–	–	–	–
	Alergia	$<$ .01	$<$ .01	$<$ .01	$<$ .01	$<$ .01	.05	.02	.09	.24

Appendix

Table 9: Training time (seconds) across all environments. Alergia and CART train in milliseconds; BehavClone scales linearly with

n

. TSL f requires 3–14s but achieves perfect generalization with 1–2 orders of magnitude fewer samples.

Linear Temporal Logic

Linear Temporal Logic (LTL) specifies how properties should hold over sequences of events, enabling verification, monitoring, and synthesis of system behavior.

See all 31 papers

On Synthesis of Metric Interval Temporal Logics
Sep 1, 2026Hsi-Ming Ho, Shankaranarayanan Krishna, Khushraj MadnaniFormal Verification
University of Sussex, Brighton, UK · IIT Bombay, Mumbai, India · IIT Guwahati, Guwahati, India
Learning Linear Temporal Specifications from Demonstrations with Uncertainty
Jul 12, 2026Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oesFormal Verification Learning from Demonstration
School of Electrical Engineering and Computer Science at The Pennsylvania State University, State College, USA
Efficient Temporal Datalog Materialisation for Composite Event Recognition
May 4, 2026Periklis MantenoglouLogical Reasoning Temporal Reasoning
Örebro University, Sweden

Sep 1, 2026J/K move · Enter open · S save

On Synthesis of Metric Interval Temporal Logics

Hsi-Ming Ho, Shankaranarayanan Krishna, Khushraj Madnani

University of Sussex, Brighton, UK · IIT Bombay, Mumbai, India · IIT Guwahati, Guwahati, India

Formal Verification

Open paper AskPDF arXiv

Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to tackle precise passive learning for an expressive timed logic, Metric Interval Temporal Logic (MITL) without relying on predefined templates or restricted logic fragments. Our approach formally reduces the timed learning problem into a scalable untimed one. By identifying quantitative timing differences between positive and negative traces, we synthesise precise timed constraints and inject them as new Boolean atomic propositions. This embeds timing into the alphabet, delegating the complex formula evaluation to highly optimised, off-the-shelf untimed LTL tools. Crucially, our framework is complete, guaranteeing a separating specification can always be found. We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.

Abstract

Linear Temporal Logic

Explore similar work

On Synthesis of Metric Interval Temporal Logics

Learning Linear Temporal Specifications from Demonstrations with Uncertainty

Efficient Temporal Datalog Materialisation for Composite Event Recognition