1 citations · 1 across the 3 of their papers we have counts for
6 papers · 1 filter
Pushdown Model Checking Above the Cubic Bottleneck
A. R. Balasubramanian, Dmitry Chistikov, Rupak Majumdar
Many problems in the verification of recursive programs can be reduced to pushdown model checking. In this problem, we are given as input a pushdown automaton (PDA) over a constant…
Algorithms and fine-grained complexity for nondeterministic and symmetric difference automata
Dmitry Chistikov, Radosław Piórkowski, Neha Rino +1
Symmetric difference automata (XNFA) are a variant of standard finite automata in which an input word is accepted iff the number of accepting runs is odd. Equivalently, these are w…
Intersecting Dense Automata
Dmitry Chistikov, Neha Rino
We observe that the classical Cartesian product construction for the intersection of (languages of) nondeterministic finite automata (NFA) is non-optimal in the worst case, if the…
The Tractability Border of Reachability in Simple Vector Addition Systems with States
Dmitry Chistikov, Wojciech Czerwiński, Filip Mazowiecki +3
Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability pro…
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.…
Acyclic Petri and Workflow Nets with Resets
Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman +2
In this paper we propose two new subclasses of Petri nets with resets, for which the reachability and coverability problems become tractable. Namely, we add an acyclicity condition…