Since the establishment of the decidability for the reachability problem for VASS Mayr (1981); Kosaraju (1982), very few works have been able to provide essential improvements, probably apart from Reutenauer (1990); Lambert (1992). Extensions of the problem have been shown decidable in Jan\vcar (1990) and Reinhardt (2005) by considering richer reachability properties or richer models, respectively. Still, the complexity of the reachability problem is an open problem, and the gap between the best known lower bound expspace, due to (Cardoza et al, 1976) and the upper bound (which has not been clearly characterized yet, but is at least non-primitive recursive) is very large. The most significant progress made recently have been done in (Leroux, 2010) when Leroux (2010) introduced a simple algorithm for deciding reachability. The algorithm is based on the existence of inductive invariants definable in Presburger arithmetic, that provide certificates of non reachability (Leroux, 2010). Whereas the existence of these invariants relies on the Lambert structures, recently a short direct proof of existence of these invariants was provided by Leroux (2011). This new proof is based on the central notion of asymptotically definable sets. These sets provide a simple way to overcome the classical examples of VASS with reachability sets that are not definable in the Presburger arithmetic and the undecidable problem of checking the equality of two reachability sets.

The new approach is based on the central concept of asymptotically definable sets. Asymptotically definable sets extend the class of Presburger sets. This extension is inspired by the semilinear decomposition of the Presburger sets introduced by Ginsburg and Spanier (1966). Intuitively, like a semilinear sets, an asymptotically definable set is a finite union of some ``simple'' sets. Whereas these ``simple'' sets are translations of finitely generated monoids in the case of semilinear sets, in the case of asymptotically definable sets they are translations of monoids with an asymptotic direction that can be denoted by a formula in a decidable logic. Asymptotically definable sets provide a simple way to overcome the difficulty of describing reachability sets of VASS. Thanks to them, it becomes possible to denote properties asymptotically satisfied by reachability sets with formulae in a decidable logic.