1. FormalConjectures
  2. Paper
  3. BranchingVAS
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Decidability of reachability for branching vector addition systems

A branching vector addition system (BVAS) of dimension d is given by a finite list of axioms, a finite list of unary rules, and a finite list of binary rules, each of which is a vector in ℤ^d. A configuration is a vector in ℕ^d, which here is represented as a vector v ∈ ℤ^d subject to 0 ≤ v. The set of reachable configurations is defined inductively:

    every axiom that is a valid configuration (i.e. lies in ℕ^d) is reachable;

    if v is a reachable configuration, r is a unary rule and v + r ∈ ℕ^d, then v + r is reachable;

    if v₁, v₂ are both reachable configurations, r is a binary rule and v₁ + v₂ + r ∈ ℕ^d, then v₁ + v₂ + r is reachable.

Modelling axioms as vectors in ℤ^d and only counting the non-negative ones as reachable yields the same set of reachable configurations as the usual definition in which axioms are required to lie in ℕ^d.

Branching vector addition systems are distinguished from ordinary vector addition systems (VAS) by allowing binary rules. VAS reachability is known to be decidable.

References:

namespace BranchingVAS

A branching vector addition system of dimension d.

structure Bvas (d : ℕ) where axioms : List (Fin d → ℤ) unaryRules : List (Fin d → ℤ) binaryRules : List (Fin d → ℤ)instance {d : ℕ} : Primcodable (Bvas d) := .ofEquiv (List (Fin d → ℤ) × List (Fin d → ℤ) × List (Fin d → ℤ)) { toFun := fun b => (b.axioms, b.unaryRules, b.binaryRules) invFun := fun p => ⟨p.1, p.2.1, p.2.2⟩ left_inv := fun _ => rfl right_inv := fun _ => rfl }

The reachable configurations of a branching vector addition system.

inductive Bvas.Reachable {d : ℕ} (b : Bvas d) : (Fin d → ℤ) → Prop | base {v : Fin d → ℤ} (hmem : v ∈ b.axioms) (hcfg : 0 ≤ v) : b.Reachable v | unary {v r w : Fin d → ℤ} (hv : b.Reachable v) (hr : r ∈ b.unaryRules) (hcfg : 0 ≤ w) (hw : w = v + r) : b.Reachable w | binary {v₁ v₂ r w : Fin d → ℤ} (hv₁ : b.Reachable v₁) (hv₂ : b.Reachable v₂) (hr : r ∈ b.binaryRules) (hcfg : 0 ≤ w) (hw : w = v₁ + v₂ + r) : b.Reachable w

The reachability problem for branching vector addition systems is decidable.

That is, is the predicate taking a branching vector addition system b together with a target vector t and returning whether t is reachable in b is a computable predicate.

As of August 2026, the solution is quite recently announced and is not yet peer-reviewed.

@[category research solved, AMS 3 68] theorem reachability_decidable : ∀ {d : ℕ}, ComputablePred fun p : Bvas d × (Fin d → ℤ) => p.1.Reachable p.2 := ⊢ ∀ {d : ℕ}, ComputablePred fun p ↦ p.1.Reachable p.2 All goals completed! 🐙

Every axiom that is non-negative is reachable.

@[category test, AMS 3 68] theorem reachable_of_mem_axioms {d : ℕ} (b : Bvas d) {v : Fin d → ℤ} (hmem : v ∈ b.axioms) (hcfg : 0 ≤ v) : b.Reachable v := .base hmem hcfg

Reachable vectors are always non-negative.

@[category test, AMS 3 68] theorem reachable_imp_pos {d : ℕ} (v : Fin d → ℤ) (b : Bvas d) : b.Reachable v → 0 ≤ v := d:ℕv:Fin d → ℤb:Bvas d⊢ b.Reachable v → 0 ≤ v d:ℕv:Fin d → ℤb:Bvas dh:b.Reachable v⊢ 0 ≤ v; d:ℕv:Fin d → ℤb:Bvas dhmem✝:v ∈ b.axiomshcfg✝:0 ≤ v⊢ 0 ≤ vd:ℕv:Fin d → ℤb:Bvas dv✝:Fin d → ℤr✝:Fin d → ℤhv✝:b.Reachable v✝hr✝:r✝ ∈ b.unaryRuleshcfg✝:0 ≤ vhw✝:v = v✝ + r✝⊢ 0 ≤ vd:ℕv:Fin d → ℤb:Bvas dv₁✝:Fin d → ℤv₂✝:Fin d → ℤr✝:Fin d → ℤhv₁✝:b.Reachable v₁✝hv₂✝:b.Reachable v₂✝hr✝:r✝ ∈ b.binaryRuleshcfg✝:0 ≤ vhw✝:v = v₁✝ + v₂✝ + r✝⊢ 0 ≤ v; all_goals All goals completed! 🐙

A small BVAS of dimension 3 used for a test below.

def exampleBvas : Bvas 3 := { axioms := [![3,1,0], ![0,0,0]], unaryRules := [![1,-10,-10], ![-1,0,1]], binaryRules := [![-1,-1,10]], }

A small (indeed, degenerate, since it contains no binary rules) BVAS of dimension 2 used for a test below.

def exampleBvas2 : Bvas 2 := { axioms := [![10,0]], unaryRules := [![-1, 1]], binaryRules := [], }

The vector [0, 0, 12] is reachable in the first example BVAS.

@[category test, AMS 3 68] theorem reachable_example : exampleBvas.Reachable ![0,0,12] := have h1 : exampleBvas.Reachable ![3,1,0] := .base (⊢ ![3, 1, 0] ∈ exampleBvas.axioms All goals completed! 🐙) (⊢ 0 ≤ ![3, 1, 0] i:Fin 3⊢ 0 i ≤ ![3, 1, 0] i; ⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩)⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩)⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨2, ⋯⟩) ⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨0, ⋯⟩)⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨1, ⋯⟩)⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![3, 1, 0] ((fun i ↦ i) ⟨2, ⋯⟩) All goals completed! 🐙) have h2 : exampleBvas.Reachable ![0,0,0] := .base (h1:exampleBvas.Reachable ![3, 1, 0]⊢ ![0, 0, 0] ∈ exampleBvas.axioms All goals completed! 🐙) (h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ≤ ![0, 0, 0] h1:exampleBvas.Reachable ![3, 1, 0]i:Fin 3⊢ 0 i ≤ ![0, 0, 0] i; h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨2, ⋯⟩) h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 0] ((fun i ↦ i) ⟨2, ⋯⟩) All goals completed! 🐙) have h3 : exampleBvas.Reachable ![2,0,10] := h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ exampleBvas.Reachable ![2, 0, 10] refine .binary (r := ![-1, -1, 10]) h1 h2 (h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ ![-1, -1, 10] ∈ exampleBvas.binaryRules All goals completed! 🐙) ?_ (h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ ![2, 0, 10] = ![3, 1, 0] + ![0, 0, 0] + ![-1, -1, 10] All goals completed! 🐙) h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]i:Fin (Nat.succ 0).succ.succ⊢ 0 i ≤ ![2, 0, 10] i; h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨2, ⋯⟩) h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![2, 0, 10] ((fun i ↦ i) ⟨2, ⋯⟩) All goals completed! 🐙 have h4 : exampleBvas.Reachable ![1,0,11] := h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ exampleBvas.Reachable ![1, 0, 11] refine .unary (r := ![-1, 0, 1]) h3 (h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ ![-1, 0, 1] ∈ exampleBvas.unaryRules All goals completed! 🐙) ?_ (h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ ![1, 0, 11] = ![2, 0, 10] + ![-1, 0, 1] All goals completed! 🐙) h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]i:Fin (Nat.succ 0).succ.succ⊢ 0 i ≤ ![1, 0, 11] i; h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨2, ⋯⟩) h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![1, 0, 11] ((fun i ↦ i) ⟨2, ⋯⟩) All goals completed! 🐙 have h5 : exampleBvas.Reachable ![0,0,12] := h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ exampleBvas.Reachable ![0, 0, 12] refine .unary (r := ![-1, 0, 1]) h4 (h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ ![-1, 0, 1] ∈ exampleBvas.unaryRules All goals completed! 🐙) ?_ (h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ ![0, 0, 12] = ![1, 0, 11] + ![-1, 0, 1] All goals completed! 🐙) h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]i:Fin (Nat.succ 0).succ.succ⊢ 0 i ≤ ![0, 0, 12] i; h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨2, ⋯⟩) h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨0, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨0, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨1, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨1, ⋯⟩)h1:exampleBvas.Reachable ![3, 1, 0]h2:exampleBvas.Reachable ![0, 0, 0]h3:exampleBvas.Reachable ![2, 0, 10]h4:exampleBvas.Reachable ![1, 0, 11]⊢ 0 ((fun i ↦ i) ⟨2, ⋯⟩) ≤ ![0, 0, 12] ((fun i ↦ i) ⟨2, ⋯⟩) All goals completed! 🐙 h5

The vector [0, 0] is not reachable in the second example BVAS.

v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ (v✝ + ![-1, 1]) 0 + (v✝ + ![-1, 1]) 1 = 10 v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ v✝ 0 + -1 + (v✝ 1 + 1) = 10 v:Fin 2 → ℤv✝:Fin 2 → ℤhv:exampleBvas2.Reachable v✝hcfg:0 ≤ vhw:v = v✝ + ![-1, 1]⊢ v✝ 0 + v✝ 1 = 10 All goals completed! 🐙 v:Fin 2 → ℤv₁✝:Fin 2 → ℤv₂✝:Fin 2 → ℤr✝:Fin 2 → ℤhv₁✝:exampleBvas2.Reachable v₁✝hv₂✝:exampleBvas2.Reachable v₂✝hr:r✝ ∈ exampleBvas2.binaryRuleshcfg✝:0 ≤ vhw✝:v = v₁✝ + v₂✝ + r✝⊢ v 0 + v 1 = 10 v:Fin 2 → ℤv₁✝:Fin 2 → ℤv₂✝:Fin 2 → ℤr✝:Fin 2 → ℤhv₁✝:exampleBvas2.Reachable v₁✝hv₂✝:exampleBvas2.Reachable v₂✝hr:r✝ ∈ exampleBvas2.binaryRuleshcfg✝:0 ≤ vhw✝:v = v₁✝ + v₂✝ + r✝⊢ v 0 + v 1 = 10 All goals completed! 🐙 h:exampleBvas2.Reachable ![0, 0]⊢ False All goals completed! 🐙end BranchingVAS