← All problems
Unverified

o(n^2)-time algorithm for coverability in 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: in a given 1-VASS, is there is a run from a given starting state that ends in a given target state (with any counter value). There is a straightforward O(n2)O(n 2 )-time algorithm for coverability in 1-VASS. Does 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