← All problems
Unverified

The time-complexity of coverability in unary 1-VASS

A 1-dimensional Vector Addition System with States (1-VASS) can be seen as an directed and integer weighted graph that is equipped with a non-negative integer counter. A configuration of a 1-VASS is a pair (q,x)(q, x) that is the current node qq and the current non-negative counter value xx. A run in a 1-VASS is a sequence of configurations (q0,x0),(q1,x1),…,(qk,xk)(q_0, x_0), (q_1, x_1), \ldots, (q_k, x_k) where for each i∈{1,…,k}i \in \{ 1, \ldots, k\}, there is an edge from xi−1x_{i-1} to xix_i with weight xi−xi−1x_i - x_{i-1}. Let nn the size of a 1-VASS, encoded in unary, that is the number of states plus the absolute value of all weights. The coverability problem asks whether there is a run from (p,0)(p, 0) to (q,x)(q, x) in V\mathcal{V}, where x≥0x \geq 0; the input consists of a 1-VASS V\mathcal{V}, an initial state pp, and a target state qq. There is a straightforward O(n2)\mathcal{O}(n^2)-time algorithm for coverability in 1-VASS. Is there an o(n2)o(n^2)-time algorithm for coverability in 1-VASS?

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu