41 citations · 41 across the 2 of their papers we have counts for
Showing 2006Show all
2 papers · 1 filter
cs.LO2006
LTL with the Freeze Quantifier and Register Automata
Stephane Demri, Ranko Lazic
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data…
cs.LO2006★ 41 cited
On the freeze quantifier in Constraint LTL: decidability and complexity
Stéphane Demri, Ranko Lazic, David Nowak
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze q…