41 citations · 41 across the 2 of their papers we have counts for
4 papers
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…
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…
Reasoning about transfinite sequences
Stéphane Demri, David Nowak
We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequenc…
Deciding regular grammar logics with converse through first-order logic
Stephane Demri, Hans de Nivelle
We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variabl…