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.

Two-variable restriction: Only two registers: decidable. More registers: undecidable.

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

Symbols.

Symbol	Unicode	Name	Meaning
x↓	—	Freeze	Capture value
x↑	—	Match	Compare to frozen
x.	—	Bind	Position freeze
=	—	Equality	Data comparison

Metatheory. Decidability sensitive to restrictions. Two-variable: decidable. Relationship to register automata. Expressiveness hierarchy.

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

Limitations. Decidability fragile. Infinite data challenges. Complexity high. Restricted fragments practical.