2025年10月24日¶

\(\newcommand{Cone}{\mathop{\operatorname{cone}}}\) \(\newcommand{Span}{\mathop{\operatorname{span}}}\) \(\newcommand{Supp}{\mathop{\operatorname{supp}}}\) \(\newcommand{BSeq}{\mathop{\operatorname{Seq'}}}\) \(\newcommand{Intr}{\mathop{\operatorname{int}}}\)

Towards Reachability in Max-Geometric Dimension 3¶

Wideness¶

Consider a sequence of strongly connected VASSes where each of them has geometric dimension 3.

\[ V_0 t_1 V_1 t_2 V_2 \cdots t_k V_k \]

We would like to define wideness to be the non-emptiness intersection of "forward cone of \(V_0\)" and "backward sequential cone of \(V_0\ldots V_k\)".

The backward sequential cone is defined to be:

\(\BSeq(V_k) = -\Cone(V_k) \cap \mathbb{Q}^d_{\ge 0}\), by \(\Cone\) we mean closed cones.
\(\BSeq(V_i t_{i+1} V_{i+1} \ldots) = (-\Cone(V_i) + \BSeq(V_{i+1} \ldots)) \cap \mathbb{Q}_{\ge 0}^d\).

For technical reasons wideness is defined to be

\[ \Intr(\Cone(V_0)) \cap \BSeq(V_0 \ldots V_k) \ne \emptyset \]

It can be proved that wideness is equivalent to that: there is a homogeneous solution to the characteristic system where every edge in \(V_0\) is used at least once.

Moreover, when wideness does not hold, we have

\[ \Intr(\Cone(V_0)) \cap \BSeq(V_0 \ldots V_k) = \emptyset \]

Note that at the end of \(V_0\) we cannot be too far from \(\BSeq(V_0 \ldots V_k)\). Thus, inside \(V_0\) we can only use those cycles from

\[ \Cone(V_0) \cap \BSeq(V_0 \ldots V_k) \]

From non-wideness this must be at most 2-dimensional, reducing the geometric dimension.

A structure for induction¶

We may assume at \(V_0\) we have a forward pumping run, otherwise its geometric dimension can be dropped. In this case we only need to care about \(\mathbb{Z}\)-runs inside \(V_0\). We can make \(V_0\) a \(\mathbb{Z}\)-component and not care it in the future.

Problem

After pumping we need to find cycles in later components to cancel to effect of difference between upward and downward pumps. However, the homogeneous solution may not touch every state in other components.

This may be solved by guessing which states will be touched and delete others?

Therefore, we define a sequence for induction as a sequence of VASSes, where the first \(k\) and last \(\ell\) components are \(\mathbb{Z}\)-VASSes where we do not care its dimension (but we require the configuration visited after leaving and before entering these components be non-negative).

We aim to reduce the number of \(\mathbb{N}\)-VASSes in the sequence. So for the first \(\mathbb{N}\)-component, we need to define its wideness and pumpability. Note that its source can be defined as the reachability set of the first \(\mathbb{Z}\)-VASSes, which is a linear set obtained from equations.