Extending Rackoff's EXPSPACE Technique

The covering problem (checking whether a configuration greater than a given one is reachable) and the boundedness problem (checking whether the reachability set is finite) for VASS were shown to lie in EXPSPACE by Rackoff (1978).

Rackoff's proof technique has been extended in (Praveen and Lodaya, 2009; Atig and Habermehl, 2009; Demri, 2010; Blockelet and Schmitz, 2011) to numerous other decision problems on VASS that can be answered by exhibiting witness runs of small lengths. All the works extend the scope of the proof by induction on the dimension of the VASS from (Rackoff, 1978).

Other results related to reachability problems for the branching extension of VASS () have been recently obtained (Demri et al, 2009; Schmitz, 2010; Lazić, 2010), providing new proof techniques to tackle the reachability problem for VASS.