Sciweavers

CORR
2008
Springer
141views Education» more  CORR 2008»
13 years 4 months ago
Model checking memoryful linear-time logics over one-counter automata
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL and written LTL ) and for first-order logic with data equality tests (written F...
Stéphane Demri, Ranko Lazic, Arnaud Sangnie...
FOSSACS
2008
Springer
13 years 6 months ago
Model Checking Freeze LTL over One-Counter Automata
We study complexity issues related to the model-checking problem for LTL with registers (a.k.a. freeze LTL) over one-counter automata. We consider several classes of one-counter au...
Stéphane Demri, Ranko Lazic, Arnaud Sangnie...
ICALP
2000
Springer
13 years 8 months ago
Efficient Verification Algorithms for One-Counter Processes
We study the problem of strong/weak bisimilarity between processes of one-counter automata and finite-state processes. We show that the problem of weak bisimilarity between process...
Antonín Kucera
CSL
2006
Springer
13 years 8 months ago
Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
Abstract. We investigate the possibility of (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses visibly BPA (Basi...
Jirí Srba
ICALP
2010
Springer
13 years 9 months ago
Model Checking Succinct and Parametric One-Counter Automata
We investigate the decidability and complexity of various model checking problems over one-counter automata. More specifically, we consider succinct one-counter automata, in which...
Stefan Göller, Christoph Haase, Joël Oua...
CONCUR
2009
Springer
13 years 11 months ago
Reachability in Succinct and Parametric One-Counter Automata
One-counter automata are a fundamental and widely-studied class of infinite-state systems. In this paper we consider one-counter automata with counter updates encoded in binary—...
Christoph Haase, Stephan Kreutzer, Joël Ouakn...