Freeze Quantifiers

Origin. Alur and Henzinger (1994). Freeze current time/value. Compare across positions. Real-time and data constraints. First-order temporal with data.

Models. Freeze x.φ: bind current position/value to x. Compare x with later positions. Enables data-aware temporal properties. Decidability varies.

Formalism.

Freeze operator: x.φ: bind current position to x, continue with φ. Uses x in φ to refer back.

Position freeze (timed): x.◇(t = x + 5): eventually at time x+5. Capture timestamp, compare later.

Data freeze: x↓.φ: capture current data value as x. Compare data across positions.

LTL with freeze: LTL↓: LTL + freeze for data. φ ::= p | x↓.φ | x ↑ | ¬φ | φ∧ψ | Xφ | φUψ x↑: current data equals frozen x.

Example: G(request → x↓.F(response ∧ x↑)) "Every request gets response with same ID."

Decidability: LTL↓ over finite alphabet: decidable. Over infinite data: depends on constraints. With arithmetic: often undecidable.

Register restriction: One register: satisfiability decidable over data words, but non-primitive-recursive (Demri–Lazić). Two or more registers: undecidable.

Timed automata connection: Clock freeze ≈ timed automata clocks. Reset and compare.

Symbols.

Symbol	Unicode	Name	Meaning
↓	U+2193	Freeze	x↓: capture the current value into register x
↑	U+2191	Match	x↑: current value equals the frozen one
x.	—	Bind	Position freeze, as in TPTL
=	—	Equality	Only comparison available on data
X	—	Next	Next position
U	—	Until	Until
G	—	Globally	Always
F	—	Finally	Eventually
⊨	U+22A8	Satisfaction	Truth at a position under a register valuation

Metatheory. The freeze quantifier arrived in the timed setting with Alur and Henzinger's TPTL ("A really temporal logic", JACM 1994), where x.φ binds the current timestamp and φ may compare it with later ones by linear constraints; over discrete time TPTL satisfiability is EXPSPACE-complete, matching MITL, and Bouyer, Chevalier, and Markey (2005) showed that in the pointwise semantics TPTL is strictly more expressive than MTL. Transposed to data words, the same device gives LTL↓, whose registers correspond exactly to the registers of the register automata of Kaminski and Francez (1994). Here the number of registers is the decisive parameter, established by Demri and Lazić (ToCL 2009): with one register, satisfiability over finite data words is decidable but non-primitive-recursive, by reduction to reachability in faulty counter machines; with two registers it is undecidable; and with one register over infinite data words it is Π⁰₁-complete, so decidable satisfiability does not survive the move to infinite models.

Applies to. Data-aware verification. XML processing. Database queries. Protocol verification. Runtime monitoring.

Limitations. The decidable region is one register wide. Two registers already give undecidability, so there is no graded tradeoff to tune, and the one-register case is decidable only at non-primitive-recursive cost, which puts no usable algorithm behind the decidability result. Over infinite data words even one register loses it. Data may be compared only for equality: an order, a successor function, or arithmetic on the frozen values pushes the logic back into undecidability, so aggregation, counting, and threshold properties are all out of reach. In the timed reading the freeze inherits punctuality, and since MTL embeds into TPTL in the pointwise semantics, TPTL over dense time with infinite models is undecidable as well. The binder also destroys the automaton-theoretic route that makes LTL practical, since alternating register automata have undecidable emptiness in general.