56 citations · 231 across the 17 of their papers we have counts for
8 papers · 1 filter
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
Matthias Englert, Ranko Lazić, Patrick Totzke
Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial…
Non-Elementary Complexities for Branching VASS, MELL, and Extensions
Ranko Lazić, Sylvain Schmitz
We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments an…
Model checking memoryful linear-time logics over one-counter automata
Stephane Demri, Ranko Lazic, Arnaud Sangnier
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. W…
Alternating Automata on Data Trees and XPath Satisfiability
Marcin Jurdzinski, Ranko Lazic
A data tree is an unranked ordered tree whose every node is labelled by a letter from a finite alphabet and an element ("datum") from an infinite set, where the latter can only be…
Safety alternating automata on data words
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. Safety one-way altern…
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…
On model checking data-independent systems with arrays without reset
R. S. Lazic, T. C. Newcomb, A. W. Roscoe
A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store,…