Characterizing LTL Formulas by Examples

Balder ten Cate; Dana Fisman; Patrik Sestic; Roi Ohayon

arxiv: 2604.22097 · v1 · submitted 2026-04-23 · 💻 cs.LO

Characterizing LTL Formulas by Examples

Balder ten Cate , Dana Fisman , Roi Ohayon , Patrik Sestic This is my paper

Pith reviewed 2026-05-08 13:34 UTC · model grok-4.3

classification 💻 cs.LO

keywords LTLunique characterizationlabeled examplestransfinite wordsschematic examplesbasis-restricted fragmentsmonotone fragmentstemporal logic

0 comments

The pith

LTL formulas in certain restricted fragments can be uniquely characterized by finite sets of labeled examples, with transfinite words and schematic patterns expanding the reach.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper examines when LTL formulas can be singled out by a small collection of positive and negative examples. In the usual finite-word case it delivers a full classification of the basis-restricted fragments for which this is always possible. Allowing transfinite words as examples then yields finite unique characterizations for many monotone fragments. Schematic examples, which stand for whole families of finite words, further succeed on fragments where ordinary finite examples are insufficient. A reader would care because the results clarify the power and limits of example-driven methods for writing, debugging, and learning temporal specifications.

Core claim

We provide a complete classification of basis-restricted LTL fragments that admit unique characterizations by finite examples. We show that allowing transfinite words as examples enables finite unique characterizations for large monotone fragments of LTL. We introduce schematic examples that compactly represent families of finite words and show that these enable unique characterization results in the finite setting that were not possible with ordinary finite examples alone.

What carries the argument

Unique characterization by labeled examples, applied to basis-restricted and monotone fragments of LTL together with the new device of schematic examples.

If this is right

Basis-restricted fragments of LTL receive a complete classification for unique characterization by finite labeled examples.
Large monotone fragments of LTL admit finite unique characterizations once transfinite words are allowed as examples.
Schematic examples produce unique characterizations in the finite setting for fragments that resist ordinary finite examples.
The descriptive power of each example type is thereby mapped for the targeted fragments.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Designers of example-based learning algorithms for temporal properties can select example types according to the target fragment.
Debugging tools for reactive systems could exploit the classification to isolate the precise formula consistent with observed traces.
The same separation technique may apply to fragments of other temporal logics once analogous restrictions are identified.

Load-bearing premise

The chosen example types are rich enough to separate any two distinct formulas inside the fragments under study.

What would settle it

Two syntactically different formulas from a basis-restricted fragment that receive identical labels on every finite word would falsify the claimed classification.

read the original abstract

We investigate the extent to which Linear Temporal Logic (LTL) formulas can be uniquely characterized by a finite set of labeled examples. We consider different types of examples, ranging from finite words to transfinite words, as well as schematic examples. In the finite-word setting, we provide a complete classification of basis-restricted LTL fragments that admit such unique characterizations. Next, we show that allowing transfinite words as examples enables finite unique characterizations for large monotone fragments of LTL. Finally, we introduce schematic examples, i.e., patterns that compactly represent a family of finite words, and we show that these enable unique characterization results in the finite setting that were not possible with ordinary finite examples alone. Overall, the work provides a foundational account of the descriptive power of different example types for example-driven specification, debugging, and learning of temporal properties.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper classifies exactly which basis-restricted LTL fragments admit unique finite-example characterizations and shows concrete gains from transfinite words and schematic patterns for monotone fragments.

read the letter

The main thing to know is that this work delivers a complete classification of basis-restricted LTL fragments that can be uniquely pinned down by finite examples, then shows how transfinite words give finite unique characterizations for large monotone fragments and how schematic examples recover some of those results in the finite case alone. Those three pieces—the classification, the transfinite extension, and the schematic technique—are the actual new contributions and they are not just rephrasings of prior work on LTL learning. The abstract presents them in a straightforward sequence that stays inside ordinary LTL semantics with no circular definitions or free parameters. That structure is clean and the claims about descriptive power for specification mining and debugging follow directly from it. The restrictions to basis-restricted and monotone fragments are declared up front, so the results are tight inside those classes but do not claim to cover full LTL. If a reader needs arbitrary formulas or non-monotone behavior, the positive results stop applying and the paper simply marks the boundary rather than crossing it. The proofs themselves are not visible here, so the case analysis could still contain gaps, but nothing in the stated argument relies on unstated closure properties or post-hoc fitting. This is for people working on example-based inference of temporal properties in verification tools. A reader who already cares about the limits of trace-based learning will get precise boundaries and new example formats to consider. It deserves a serious referee because the classification is foundational within its scope and the technical moves on example types are substantive enough to warrant checking the details.

Referee Report

0 major / 0 minor

Summary. The paper investigates the extent to which LTL formulas can be uniquely characterized by finite sets of labeled examples. It provides a complete classification of basis-restricted LTL fragments admitting such characterizations in the finite-word setting, shows that transfinite words enable finite unique characterizations for large monotone fragments of LTL, and introduces schematic examples (patterns representing families of finite words) that yield unique characterizations in the finite setting beyond what ordinary finite examples allow. The work frames these results as a foundational account for example-driven specification, debugging, and learning of temporal properties.

Significance. If the classifications and existence results hold, the paper delivers a systematic account of the descriptive power of finite words, transfinite words, and schematic examples for LTL. The complete classification of basis-restricted fragments and the positive results for monotone fragments under transfinite examples constitute clear strengths, as does the demonstration that schematic patterns recover characterizations unavailable with plain finite words. These contributions advance the theoretical foundations of example-based approaches in temporal logic.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading and positive evaluation of our manuscript. The provided summary accurately captures the main results on unique characterizations of LTL formulas via finite examples, transfinite words, and schematic examples, as well as the complete classification for basis-restricted fragments. We are pleased with the recommendation to accept.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's claims consist of a complete classification of basis-restricted LTL fragments admitting unique characterizations by finite words, followed by positive results for transfinite words on monotone fragments and for schematic examples in the finite case. These rest on explicitly declared restrictions and standard LTL semantics rather than any self-definitional equations, fitted parameters presented as predictions, or load-bearing self-citations whose validity reduces to the current work. The derivation chain is therefore self-contained and classificatory, with no step reducing by construction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The abstract invokes standard LTL semantics over words and linear orders but introduces no fitted numerical parameters, no new physical or logical entities, and no ad-hoc axioms beyond the usual definitions of LTL fragments.

axioms (1)

standard math Standard semantics of LTL over finite and transfinite words
The paper relies on the usual inductive definition of LTL satisfaction on linear orders.

pith-pipeline@v0.9.0 · 5441 in / 1250 out tokens · 44050 ms · 2026-05-08T13:34:17.984912+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages

[1]

This follows immediately from the fact thatF(φ∨ψ)≡F(φ)∨F(ψ)and FFφ≡FφandF⊤≡⊤andF⊥≡⊥

There are only finitely many formulas up to equivalence in this fragment (in a given finite set AP). This follows immediately from the fact thatF(φ∨ψ)≡F(φ)∨F(ψ)and FFφ≡FφandF⊤≡⊤andF⊥≡⊥

work page
[2]

Recall that Gφis shorthand for¬F¬φ. By rewriting to negation normal form and applying the equivalencesF⊥≡⊥, G⊥≡⊥, F⊤≡⊤and G⊤≡⊤, every formula in this fragment can be written in the form 1.o 1...,onpor 2.o 1...,on¬por 3.⊤or 4.⊥ with oi∈{F,G}. Furthermore, we have thatFFp≡Fpand GGp≡Gp, and FGFp≡GFpand GFGp≡FGp. Thus, only finitely many possible formulas up ...

work page
[3]

Letφbe any formula of one of the above forms, with depthn

By applying the equivalencesFˆFp≡ˆFFp≡ˆFp and XFp≡FXp= ˆFp we can rewrite every formula in this fragment to a formula the form 1.X nFpor 2.X nF⊤or 3.X npor 4.X n⊤ Let us refer to the numbern as thedepthof the formula in question. Letφbe any formula of one of the above forms, with depthn. Letw = (AP)n+1. Thenw|=φand, for all formulas ψof the above forms of...

work page
[4]

φis true at the next timepoint or there is no next timepoint

Let X0φbe short for¬X¬φ, which means “φis true at the next timepoint or there is no next timepoint”. Then every formula in this fragment can be rewritten to the form o1...onα withoi∈{X,X0}(n≥0) andαof the formp or¬p. Such a formula is uniquely characterized by the following set of labeled examples: ∅k for k = 0...n−1labeled as positive/negative according ...

work page
[5]

Let ˆG be short for¬ˆF¬. By rewriting to negation normal form and applying the equivalences ˆGˆFφ≡G⊥and ˆFˆGφ≡ˆF⊤and ˆG⊤≡⊤and ˆF⊥≡⊥, we can rewrite all formulas in this fragment to one of the following forms:

work page
[6]

ˆF n α(n>0) withαof the formpor¬por⊤, or

work page
[7]

ˆG n β(n>0) withβof the formpor¬por⊥. 3.por¬p A formula of the first type is uniquely characterized by the examples∅n−1and APn−1labeled as a negative example, together with the examples∅n{p}and∅n+1 labeled according to whetherαis of the formp or¬por⊤. A formula of the second type is uniquely characterized XX:18 Characterizing LTL Formulas by Examples by t...

work page
[8]

3.The argument is similar to the one above: we cannot distinguish⊥from all formulas of the formXnp, respectively,ˆF n p, using only finitely many labeled examples

The formulap cannot be distinguished from all formulas of the formp∨Xnp, respectively, p∨ˆF n p(n>0) using only finitely many labeled examples. 3.The argument is similar to the one above: we cannot distinguish⊥from all formulas of the formXnp, respectively,ˆF n p, using only finitely many labeled examples

work page
[9]

ForLTLF,∧,¬[AP], we reason as follows: we can express⊥as p∧¬p

ForLTLX,∧,¬[AP]and LTLˆF,∧,¬[AP], the result follows from item 2 above (since disjunction is definable from conjunction and negation). ForLTLF,∧,¬[AP], we reason as follows: we can express⊥as p∧¬p. We cannot distinguish⊥from all formulas of the form p∧F(¬p∧F(p∧F(¬p...)))using only finitely many examples

work page
[10]

Thenφallows arbitrarily many alternations ofp and q before the first occurrence ofr, whereasψn bounds this number byn

Let φ:= (pUq)Ur, and defineψ0 :=r and ψn+1 :=pU(qUψn). Thenφallows arbitrarily many alternations ofp and q before the first occurrence ofr, whereasψn bounds this number byn. In particular,({p}{q})n+1{r}|=φbut̸|=ψn. Let S be any finite sample. For each positive examplew∈Swith w|=φ, fix a finite witness position ofr, and letm be the maximal number ofp/q-alt...

work page
[11]

Consider the formula¬ˆF¬ˆFp, it is equivalent to¬X⊤. We cannot distinguish this formula from¬X¬Xnp, for all n, using only finitely many finite examples: an example that distinguishes the two formulas needs to be a word of length at leastn

work page
[12]

Recall that Gφis short for¬F¬φ. Since GˆFφis equivalent, over finite words, to⊥, and we already know from item 3 above thatLTLˆF,⊥[AP]does not admit finite characterizations overWfin, it follows thatLTLF,ˆF,¬[AP]does not admit finite characterizations overWfin either. ◀ C Proofs for Section 5 ▶ Theorem 5.2.Let AP be any finite set of atomic propositions.L...

work page
[13]

We include, in our set of labeled examples, all words of length at mostn (labeled according toφ)

work page
[14]

We claim that the resulting set of labeled examples uniquely characterizesφwith respect to LTLX,∧,∨,⊤,⊥[AP]over Wall

In addition, for each word of lengthn, we include theω-wordsw·∅ωandw·APω(labeled according toφ). We claim that the resulting set of labeled examples uniquely characterizesφwith respect to LTLX,∧,∨,⊤,⊥[AP]over Wall. Indeed, if a formulaψ∈LTLX,∧,∨,⊤,⊥[AP]fits these examples, then it must agree withφon all examples. This is clearly so for words of length at ...

work page
[15]

every ui (i≥1) and everyvj (j≥1) appears exactly once ine, either alone or as part of a single merged letter. For two sets of finite wordsU,Vdefine:U ▷◁V={u▷◁v|u∈U,v∈V} ▶ Definition D.2(Canonical Examples).The set of canonical examplesEcan(φ)for a formula φ∈LTLˆF,∧,∨,⊤,⊥is defined by structural induction onφas follows: Ecan(⊥) :={}, Ecan(⊤) :={∅}, Ecan(p)...

work page

[1] [1]

This follows immediately from the fact thatF(φ∨ψ)≡F(φ)∨F(ψ)and FFφ≡FφandF⊤≡⊤andF⊥≡⊥

There are only finitely many formulas up to equivalence in this fragment (in a given finite set AP). This follows immediately from the fact thatF(φ∨ψ)≡F(φ)∨F(ψ)and FFφ≡FφandF⊤≡⊤andF⊥≡⊥

work page

[2] [2]

Recall that Gφis shorthand for¬F¬φ. By rewriting to negation normal form and applying the equivalencesF⊥≡⊥, G⊥≡⊥, F⊤≡⊤and G⊤≡⊤, every formula in this fragment can be written in the form 1.o 1...,onpor 2.o 1...,on¬por 3.⊤or 4.⊥ with oi∈{F,G}. Furthermore, we have thatFFp≡Fpand GGp≡Gp, and FGFp≡GFpand GFGp≡FGp. Thus, only finitely many possible formulas up ...

work page

[3] [3]

Letφbe any formula of one of the above forms, with depthn

By applying the equivalencesFˆFp≡ˆFFp≡ˆFp and XFp≡FXp= ˆFp we can rewrite every formula in this fragment to a formula the form 1.X nFpor 2.X nF⊤or 3.X npor 4.X n⊤ Let us refer to the numbern as thedepthof the formula in question. Letφbe any formula of one of the above forms, with depthn. Letw = (AP)n+1. Thenw|=φand, for all formulas ψof the above forms of...

work page

[4] [4]

φis true at the next timepoint or there is no next timepoint

Let X0φbe short for¬X¬φ, which means “φis true at the next timepoint or there is no next timepoint”. Then every formula in this fragment can be rewritten to the form o1...onα withoi∈{X,X0}(n≥0) andαof the formp or¬p. Such a formula is uniquely characterized by the following set of labeled examples: ∅k for k = 0...n−1labeled as positive/negative according ...

work page

[5] [5]

Let ˆG be short for¬ˆF¬. By rewriting to negation normal form and applying the equivalences ˆGˆFφ≡G⊥and ˆFˆGφ≡ˆF⊤and ˆG⊤≡⊤and ˆF⊥≡⊥, we can rewrite all formulas in this fragment to one of the following forms:

work page

[6] [6]

ˆF n α(n>0) withαof the formpor¬por⊤, or

work page

[7] [7]

ˆG n β(n>0) withβof the formpor¬por⊥. 3.por¬p A formula of the first type is uniquely characterized by the examples∅n−1and APn−1labeled as a negative example, together with the examples∅n{p}and∅n+1 labeled according to whetherαis of the formp or¬por⊤. A formula of the second type is uniquely characterized XX:18 Characterizing LTL Formulas by Examples by t...

work page

[8] [8]

3.The argument is similar to the one above: we cannot distinguish⊥from all formulas of the formXnp, respectively,ˆF n p, using only finitely many labeled examples

The formulap cannot be distinguished from all formulas of the formp∨Xnp, respectively, p∨ˆF n p(n>0) using only finitely many labeled examples. 3.The argument is similar to the one above: we cannot distinguish⊥from all formulas of the formXnp, respectively,ˆF n p, using only finitely many labeled examples

work page

[9] [9]

ForLTLF,∧,¬[AP], we reason as follows: we can express⊥as p∧¬p

ForLTLX,∧,¬[AP]and LTLˆF,∧,¬[AP], the result follows from item 2 above (since disjunction is definable from conjunction and negation). ForLTLF,∧,¬[AP], we reason as follows: we can express⊥as p∧¬p. We cannot distinguish⊥from all formulas of the form p∧F(¬p∧F(p∧F(¬p...)))using only finitely many examples

work page

[10] [10]

Thenφallows arbitrarily many alternations ofp and q before the first occurrence ofr, whereasψn bounds this number byn

Let φ:= (pUq)Ur, and defineψ0 :=r and ψn+1 :=pU(qUψn). Thenφallows arbitrarily many alternations ofp and q before the first occurrence ofr, whereasψn bounds this number byn. In particular,({p}{q})n+1{r}|=φbut̸|=ψn. Let S be any finite sample. For each positive examplew∈Swith w|=φ, fix a finite witness position ofr, and letm be the maximal number ofp/q-alt...

work page

[11] [11]

Consider the formula¬ˆF¬ˆFp, it is equivalent to¬X⊤. We cannot distinguish this formula from¬X¬Xnp, for all n, using only finitely many finite examples: an example that distinguishes the two formulas needs to be a word of length at leastn

work page

[12] [12]

Recall that Gφis short for¬F¬φ. Since GˆFφis equivalent, over finite words, to⊥, and we already know from item 3 above thatLTLˆF,⊥[AP]does not admit finite characterizations overWfin, it follows thatLTLF,ˆF,¬[AP]does not admit finite characterizations overWfin either. ◀ C Proofs for Section 5 ▶ Theorem 5.2.Let AP be any finite set of atomic propositions.L...

work page

[13] [13]

We include, in our set of labeled examples, all words of length at mostn (labeled according toφ)

work page

[14] [14]

We claim that the resulting set of labeled examples uniquely characterizesφwith respect to LTLX,∧,∨,⊤,⊥[AP]over Wall

In addition, for each word of lengthn, we include theω-wordsw·∅ωandw·APω(labeled according toφ). We claim that the resulting set of labeled examples uniquely characterizesφwith respect to LTLX,∧,∨,⊤,⊥[AP]over Wall. Indeed, if a formulaψ∈LTLX,∧,∨,⊤,⊥[AP]fits these examples, then it must agree withφon all examples. This is clearly so for words of length at ...

work page

[15] [15]

every ui (i≥1) and everyvj (j≥1) appears exactly once ine, either alone or as part of a single merged letter. For two sets of finite wordsU,Vdefine:U ▷◁V={u▷◁v|u∈U,v∈V} ▶ Definition D.2(Canonical Examples).The set of canonical examplesEcan(φ)for a formula φ∈LTLˆF,∧,∨,⊤,⊥is defined by structural induction onφas follows: Ecan(⊥) :={}, Ecan(⊤) :={∅}, Ecan(p)...

work page