88 citations · 281 across the 25 of their papers we have counts for
6 papers · 1 filter
Invariants for One-Counter Automata with Disequality Tests
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks +1
We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value.…
Reachability in fixed dimension vector addition systems with states
Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić +2
The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one…
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems
J. Leroux, M. Praveen, Ph. Schnoebelen +1
We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growi…
The Reachability Problem for Petri Nets is Not Elementary
Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic +2
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and datab…
On Boundedness Problems for Pushdown Vector Addition Systems
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
We study pushdown vector addition systems, which are synchronized products of pushdown automata with vector addition systems. The question of the boundedness of the reachability se…
On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension
Jérôme Leroux, Grégoire Sutre, Patrick Totzke
Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions invo…