Zobrazeno 1 - 10
of 73 430
pro vyhledávání: '"Vass, A."'
The omega-regular separability problem for B\"uchi VASS coverability languages has recently been shown to be decidable, but with an EXPSPACE lower and a non-primitive recursive upper bound -- the exact complexity remained open. We close this gap and
Externí odkaz:
http://arxiv.org/abs/2406.01008
Autor:
Balasubramanian, A. R.
Vector addition system with states (VASS) is a popular model for the verification of concurrent systems. VASS consists of finitely many control states and a set of counters which can be incremented and decremented, but not tested for zero. VASS is a
Externí odkaz:
http://arxiv.org/abs/2405.11085
An $\mathsf{F}_{d}$ upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where $\mathsf{F}_d$ is the $d$-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm com
Externí odkaz:
http://arxiv.org/abs/2404.14781
Autor:
Keskin, Eren, Meyer, Roland
We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_{\omega}$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitab
Externí odkaz:
http://arxiv.org/abs/2401.16095
Autor:
Perez, Guillermo A., Rao, Shrisha
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer variables.
Externí odkaz:
http://arxiv.org/abs/2402.13237
The recent years have seen remarkable progress in establishing the complexity of the reachability problem for vector addition systems with states (VASS), equivalently known as Petri nets. Existing work primarily considers the case in which both the V
Externí odkaz:
http://arxiv.org/abs/2310.16740
Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero. Whether the reachability problem is decidable for
Externí odkaz:
http://arxiv.org/abs/2310.16798
Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackof
Externí odkaz:
http://arxiv.org/abs/2305.01581
Autor:
Ajdarów, Michal, Kučera, Antonín
The standard approach to analyzing the asymptotic complexity of probabilistic programs is based on studying the asymptotic growth of certain expected values (such as the expected termination time) for increasing input size. We argue that this approac
Externí odkaz:
http://arxiv.org/abs/2307.04707
We study extensions of Sem\"enov arithmetic, the first-order theory of the structure $(\mathbb{N}, +, 2^x)$. It is well-knonw that this theory becomes undecidable when extended with regular predicates over tuples of number strings, such as the B\"uch
Externí odkaz:
http://arxiv.org/abs/2306.14593