NON-ELEMENTARY COMPLEXITIES FOR BRANCHING VASS, MELL, AND EXTENSIONS RANKO LAZIC´ AND SYLVAIN SCHMITZ Abstract. Westudythecomplexityofreachabilityproblemsonbranch- ing extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplica- 4 tiveexponentialfragmentisTower-hardalreadyintheaffinecase—and 1 hence non-elementary. We match this lower bound for the full propo- 0 sitional affine linear logic, proving its Tower-completeness. We also 2 showthatprovabilityinpropositionalcontractivelinearlogicisAcker- p mann-complete. e Key Words. Linearlogic,vectoradditionsystems,fast-growingcom- S plexity. 5 2 ] 1. Introduction O L The use of various classes of counter machines to provide computational s. counterparts to propositional substructural logics has been highly fruitful, c allowing to prove for instance: [ • the undecidability of provability in propositional linear logic (LL), 2 thanks to a reduction from the halting problem in Minsky machines v 5 provedbyLincoln,Mitchell,Scedrov,andShankar[18],whoinitiated 8 much of this line of work, 7 • the decidability of the !-Horn fragment of multiplicative exponential 6 . linear logic, proved by Kanovich [13] by reduction to reachability in 1 vector addition systems, 0 4 • the decidability of provability in affine linear logic, first shown by 1 Kopylov using a notion of vector addition games [14], v: • the Ackermann-completeness of provability in the conjunctive im- i plicative fragment of relevance logic, proved by Urquhart [30], using X reductions to and from expansive alternating vector addition sys- r a tems, and • the inter-reducibility between provability in multiplicative exponen- tial linear logic and reachability in a model of branching vector ad- dition systems, shown by de Groote, Guillaume, and Salvati [9]. 1.1. Alternating Branching VASS. In this paper, we revisit the corre- spondences between propositional linear logic and counter systems with a focus on computational complexity. In Section 3, we define a model of al- ternating branching vector addition systems (ABVASS) with full zero tests. While this model can be seen as an extension and repackaging of Kopylov’s vector games, its reachability problem enjoys very simple reductions to and Work partially supported by ANR grant ReacHard 11-BS02-001-01. 1 2 R.LAZIC´ ANDS.SCHMITZ from provability in LL, which are suitable for complexity statements (see Section 4). We prove that: • coverability in the top-down, root-to-leaves direction is Tower- complete, i.e. complete for the class of problems that can be solved with time or space resources bounded by a tower of exponentials whose height depends elementarily in the input size (see Section 5 for the upper bound and Section 6 for the lower bound), and • coverability in the bottom-up, leaves-to-root direction is complete for Ackermann, i.e. complete for resources bounded by the Acker- mann function of some primitive-recursive function of the input (see Section 7). 1.2. Provability in Substructural Logics. Our complexity bounds for ABVASS translate into the exact same bounds for provability in fragments and variants of LL: 1.2.1. Affine Linear Logic (LLW) was proved decidable by Kopylov [14] in 1995 using vector addition games; a model-theoretic proof was later pre- sented by Lafont [15].1 The best known complexity bounds for LLW are due to Urquhart [31]: by a reduction from coverability in vector addition systems [19], he derives an ExpSpace lower bound, very far from the Ackermann upper bound he obtains from length function theorems for Dickson’s Lemma [see e.g. 12]. 1.2.2. Contractive Linear Logic (LLC) was proved decidable by Okada and Terui [22] by model-theoretic methods. Urquhart [30] showed the Ackermann-completeness of provability in a fragment of relevance logic, which is also a fragment of intuitionistic multi- plicative additive LLC. To the best of our knowledge, there are no known complexity upper bounds for provability in LLC. 1.2.3. Multiplicative Exponential Linear Logic. The main open question in this area is whether the multiplicative exponential fragment (MELL) is de- cidable. It is related to many decision problems, for instance in computa- tional linguistics [24, 25], cryptographic protocol verification [32], the veri- fication of parallel programs [4], and data logics [3, 11]. Thanks to the reductions to and from the reachability problem in branch- ing vector addition systems with states (BVASS) [9] and to the bounds of Lazi´c [17], we know that provability in MELL is 2-ExpSpace-hard. 1.2.4. Summary of the Complexity Results: LLW: We improve both the lower bound and the upper bound of Urquhart[31],andprovethatLLWprovabilityiscompleteforTower. 1 Variants of LLW are popular in the literature on implicit complexity; for instance, light affine linear logic [2] is known to type exactly the class FP of polynomial time computable functions. In this paper we are however interested in the complexity of the provability problem (for the propositional fragment), rather than the complexity of nor- malisation. Intermsoftypedlambdacalculi,ourresultspertaintothecomplexityofthe type inhabitation problem. NON-ELEMENTARY COMPLEXITIES FOR BVASS, MELL, AND EXTENSIONS 3 LLC: We show that LLC provability is Ackermann-complete; the lower bound already holds for the multiplicative additive fragment MALLC. MELL: Our Tower-hardness result for LLW already holds for affine MELL and thus for MELL, which improves over the 2-ExpSpace lower bound of Lazi´c [17]. ILL: All of our complexity bounds also hold for provability in the intuitionistic versions of our calculi. See §4.1.2 for details. 2. Propositional Linear Logic 2.1. Classical Linear Logic. For convenience, we present here a sequent calculus for classical propositional linear logic that works with formulæ in negation normal form and considers one-sided sequents [see e.g. 29]. 2.1.1. Syntax. Propositionallinearlogicformulæaredefinedbytheabstract syntax A,B ::=a | a⊥ (atomic) | A`B | A⊗B | ⊥ | 1 (multiplicative) | A&B | A⊕B | (cid:62) | 0 (additive) | !A | ?A (exponential) wherearangesoveratomicformulæ. Wewrite“A⊥”forthenegationnormal form of A, where negations are pushed to the atoms using the dualities A⊥⊥ = A, (A`B)⊥ = A⊥⊗B⊥, ⊥⊥ = 1, (A&B)⊥ = A⊥⊕B⊥, (cid:62)⊥ = 0, and (?A)⊥ = !A⊥. We write “A (cid:40) B” for the linear implication A⊥`B. 2.1.2. Sequent Calculus. The rules of the sequent calculus manipulate mul- tisetsofformulæ, denotedbyΓ, ∆, ..., sothattheexchangeruleisimplicit; “?Γ” then denotes a multiset of formulæ all guarded by why-nots: ?Γ is of the form ?A ,...,?A . 1 n (cid:96) Γ,A (cid:96) ∆,A⊥ init cut (cid:96) A,A⊥ (cid:96) Γ,∆ (cid:96) Γ,A,B (cid:96) Γ,A (cid:96) ∆,B (cid:96) Γ ` ⊗ ⊥ 1 (cid:96) Γ,A`B (cid:96) Γ,∆,A⊗B (cid:96) Γ,⊥ (cid:96) 1 (cid:96) Γ,A (cid:96) Γ,B (cid:96) Γ,A (cid:96) Γ,B & ⊕ (cid:62) (cid:96) Γ,A&B (cid:96) Γ,A⊕B (cid:96) Γ,A⊕B (cid:96) Γ,(cid:62) (cid:96) Γ,A (cid:96) Γ (cid:96) Γ,?A,?A (cid:96) ?Γ,A ?D ?W ?C ?P (cid:96) Γ,?A (cid:96) Γ,?A (cid:96) Γ,?A (cid:96) ?Γ,!A Thelastfourrulesforexponentialformulæarecalleddereliction (?D),logical weakening (?W), logical contraction (?C), and promotion (?P). The cut rule can be eliminated in this calculus, which then enjoys the subformula property: in any rule except cut, the formulæ appearing in the premises are subformulæ of the formulæ appearing in the conclusion. 4 R.LAZIC´ ANDS.SCHMITZ 2.2. Fragments and Variants. Lincoln et al. [18] established most of the results on the decidability and complexity of provability in propositional linear logic. In particular, the full propositional linear logic (LL) is unde- cidable, while its multiplicative additive fragment (MALL, which excludes the exponential connectives and rules) is decidable in PSpace. As men- tioned in the introduction, the main open question in this area is whether themultiplicativeexponentialfragment(MELL,whichexcludestheadditive connectives and rules) is decidable. Regarding related logics, allowing respectively structural weakening (W) and structural contraction (C) (cid:96) Γ (cid:96) Γ,A,A W C (cid:96) Γ,A (cid:96) Γ,A instead of logical weakening and logical contraction gives rise to two decid- able variants, called respectively affine linear logic (LLW) and contractive linear logic (LLC). The sequent calculi for LLW and LLC also enjoy cut elimination and the subformula property for cut-free proofs. 2.2.1. Intuitionistic Linear Logic. Intuitionisticlinearlogicisessentiallyob- tainedfrom classicallinearlogic byrestrictingits two-sided sequentcalculus to consequents (the right sides of sequents) with at most one formula. We present here a variant of intuitionistic linear logic with bottom [29, Sec- tion 2.5], which we will refer to as ILZ: Γ (cid:96) A ∆,A (cid:96) B init cut A (cid:96) A Γ,∆ (cid:96) B Γ (cid:96) A ∆,B (cid:96) C Γ,A (cid:96) B Γ,∆,A (cid:40) B (cid:96) C L(cid:40) Γ (cid:96) A (cid:40) B R(cid:40) Γ,A,B (cid:96) C Γ (cid:96) A ∆ (cid:96) B L R Γ,A⊗B (cid:96) C ⊗ Γ,∆ (cid:96) A⊗B ⊗ Γ (cid:96) L R ⊥ (cid:96) ⊥ Γ (cid:96) ⊥ ⊥ Γ (cid:96) A L R Γ,1 (cid:96) A 1 (cid:96) 1 1 Γ,A (cid:96) C Γ,B (cid:96) C Γ (cid:96) A Γ (cid:96) B L R Γ,A⊕B (cid:96) C ⊕ Γ (cid:96) A⊕B Γ (cid:96) A⊕B ⊕ Γ,A (cid:96) C Γ,B (cid:96) C Γ (cid:96) A Γ (cid:96) B L R Γ,A&B (cid:96) C Γ,A&B (cid:96) C & Γ (cid:96) A&B & R Γ (cid:96) (cid:62) (cid:62) Γ,A (cid:96) B Γ (cid:96) B Γ,!A,!A (cid:96) B !Γ (cid:96) A !D !W !C !P Γ,!A (cid:96) B Γ,!A (cid:96) B Γ,!A (cid:96) B !Γ (cid:96) !A The fragment without ⊥ is better known as ILL. NON-ELEMENTARY COMPLEXITIES FOR BVASS, MELL, AND EXTENSIONS 5 2.2.2. Affine and Contractive Variants. Theintuitionisticversionswithbot- tomILZWandILZCandwithoutbottomILLWandILLCofLLWandLLC arerespectivelyobtainedbyaddingstructuralweakeningandstructuralcon- traction: Γ (cid:96) B Γ,A,A (cid:96) B W C Γ,A (cid:96) B Γ,A (cid:96) B As with the sequent calculi for LL, LLW, and LLC, the intuitionistic calculi forILZ,ILZW,andILZCenjoycuteliminationandthesubformulaproperty for cut-free proofs. 2.2.3. Relevance Logic. The sequent calculus LR+ considered by Urquhart [30] for a fragment of relevance logic is IMALLC without (cid:62), i.e. ILZC re- stricted to {(cid:40),⊗,1,⊕,&}. 3. Alternating Branching VASS Wedefinea“tree”extensionofvectoradditionsystemswithstates(VASS) thatcombinestwokindsofbranchingbehaviours: thoseofalternatingVASS (§3.3.1) and those of branching VASS (§3.3.2). With this combination, we obtain a reformulation of Kopylov’s vector addition games [14], for which he showed that (1) the game is inter-reducible with LL provability (2) the “lossy” version of the game is inter-reducible with LLW prov- ability. Wefurtheraddfull zero tests tothismodel,astheymakethereductionfrom LLprovabilitystraightforward(seeSection4)andcaneasilyberemoved(see §3.3.3). 3.1. Definitions. 3.1.1. Syntax. An alternating branching vector addition system with states andfullzerotests (ABVASS )issyntacticallyatupleA = (cid:104)Q,d,T ,T ,T ,T (cid:105) ¯0 u f s z where Q is a finite set of states, d is a dimension in N, and T ⊆ Q×Zd×Q, u T ⊆ Q3, T ⊆ Q3 and T ⊆ Q2 are respectively finite sets of unary, fork, f s z split and full zero test rules. We denote unary rules (q,u¯,q ) in T with u¯ 1 u in Zd by “q −→u¯ q ”, fork rules (q,q ,q ) in T by “q → q ∧q ”, split rules 1 1 2 f 1 2 (q,q ,q ) in T by “q → q + q ”, and full zero test rules (q,q ) in T by 1 2 s 1 2 1 z =?¯0 “q −−→ q ”. 1 3.1.2. Deduction Semantics. Given an ABVASS , its semantics is defined ¯0 by a deduction system over configurations (q,¯v) in Q×Nd: q,¯v unary q ,¯v+u¯ 1 where “+” denotes component-wise addition in Nd, if q −→u¯ q is a rule (and 1 implicitly ¯v+u¯ has no negative component, i.e. is in Nd), and q,¯v q,¯v +¯v q,¯0 1 2 fork split full-zero q ,¯v q ,¯v q ,¯v q ,¯v q ,¯0 1 2 1 1 2 2 1 6 R.LAZIC´ ANDS.SCHMITZ ++d q0 q1 q2 + q3 --c;--d;--d --d;++d(cid:48);++d(cid:48) --d(cid:48);++d q 4 Figure 1. An example BVASS. =?¯0 if q → q ∧q , q → q +q , and q −−→ q are rules of the system, respectively, 1 2 1 2 1 and“¯0”denotesthed-vector(cid:104)0,...,0(cid:105)withzeroesoneverycoordinate. Such a deduction system can be employed either top-down or bottom-up depend- ing on the decision problem at hand (as with tree automata); the top-down direction will correspond in a natural way to proof search in propositional linear logic, i.e. will correspond to the consequence to premises direction in the sequent calculus of §2.1.2. 3.1.3. Example. Let A be an ABVASS with five states (q ,q ,q ,q ,q ), of ¯0 0 1 2 3 4 dimension 3, with six unary rules: (cid:104)0,1,0(cid:105) (cid:104)0,−1,2(cid:105) (cid:104)0,0,0(cid:105) q −−−−→ q q −−−−−→ q q −−−−→ q 0 1 1 1 1 2 (cid:104)0,1,−1(cid:105) (cid:104)0,0,0(cid:105) (cid:104)−1,−2,0(cid:105) q −−−−−→ q q −−−−→ q q −−−−−−→ q , 2 2 3 0 3 4 and with one split rule q → q +q . There are no fork rules and no full zero 2 3 3 test rules in A, and so it is a BVASS (see §3.3.2). A depiction of A is in Figure 1, where we write c,d,d(cid:48) for vector indices 1,2,3 (respectively), and specify unary rules in terms of increments and decrements. From state q and with c,d,d(cid:48) initialised to 5,0,0 (i.e., from a root node 0 labelled by (q ,(cid:104)5,0,0(cid:105))), A can reach q with d,d(cid:48) having values 2,0, per- 0 2 form the split rule by dividing c and d almost equally (i.e., branch to two nodes labelled by (q ,(cid:104)3,1,0(cid:105)) and (q ,(cid:104)2,1,0(cid:105))), then in both threads reach 3 3 q again with d,d(cid:48) having values 4,0, perform the split rule as before, and 2 finally reach q with c,d,d(cid:48) having values 1,0,0 in one thread and 0,0,0 in 4 the remaining three threads. See Figure 2 for the corresponding deduction tree. Further reasoning, where we need to consider arbitrarily unequal splits, canshowthatAhasadeductiontreewhoserootislabelledby(q ,(cid:104)m,0,0(cid:105)) 0 and with the state label at every leaf being q if and only if m ≥ 4. In fact, 4 A is a slightly simplified version of the BVASS B in Section 6. 2 3.2. Decision Problems. Given an ABVASS A and a finite set of states ¯0 Q , we denote by a root judgement “A,Q (cid:46) q,¯v” the fact that there exists (cid:96) (cid:96) a deduction tree D in A with root label (q,¯v) and leaf labels in Q ×{¯0}. (cid:96) We call D a reachability witness for (q,¯v). Root judgements can be derived through the following deduction rules, which will be handy in proofs: A,Q(cid:96) (cid:46) q1,¯v+u¯ u¯ A,Q(cid:96) (cid:46) q1,¯0 =?¯0 A,Q (cid:46) q ,¯0 if q(cid:96) ∈ Q(cid:96) A,Q (cid:46) q,¯v if q −→ q1 A,Q (cid:46) q,¯0 if q −−→ q1 (cid:96) (cid:96) (cid:96) (cid:96) A,Q (cid:46) q ,¯v A,Q (cid:46) q ,¯v A,Q (cid:46) q ,¯v A,Q (cid:46) q ,¯v (cid:96) 1 (cid:96) 2 (cid:96) 1 1 (cid:96) 2 2 if q → q1∧q2 if q → q1+q2 A,Q (cid:46) q,¯v A,Q (cid:46) q,¯v +¯v (cid:96) (cid:96) 1 2 NON-ELEMENTARY COMPLEXITIES FOR BVASS, MELL, AND EXTENSIONS 7 q ,(cid:104)5,0,0(cid:105) 0 q ,(cid:104)5,1,0(cid:105) 1 q ,(cid:104)5,0,2(cid:105) 1 q ,(cid:104)5,0,2(cid:105) 2 q ,(cid:104)5,1,1(cid:105) 2 q ,(cid:104)5,2,0(cid:105) 2 q ,(cid:104)3,1,0(cid:105) q ,(cid:104)2,1,0(cid:105) 3 3 q ,(cid:104)3,1,0(cid:105) q ,(cid:104)2,1,0(cid:105) 0 0 q ,(cid:104)3,2,0(cid:105) q ,(cid:104)2,2,0(cid:105) 1 1 q ,(cid:104)3,1,2(cid:105) q ,(cid:104)2,1,2(cid:105) 1 1 q ,(cid:104)3,0,4(cid:105) q ,(cid:104)2,0,4(cid:105) 1 1 q ,(cid:104)3,0,4(cid:105) q ,(cid:104)2,0,4(cid:105) 2 2 q ,(cid:104)3,1,3(cid:105) q ,(cid:104)2,1,3(cid:105) 2 2 q ,(cid:104)3,2,2(cid:105) q ,(cid:104)2,2,2(cid:105) 2 2 q ,(cid:104)3,3,1(cid:105) q ,(cid:104)2,3,1(cid:105) 2 2 q ,(cid:104)3,4,0(cid:105) q ,(cid:104)2,4,0(cid:105) 2 2 q ,(cid:104)2,2,0(cid:105) q ,(cid:104)1,2,0(cid:105) q ,(cid:104)1,2,0(cid:105) q ,(cid:104)1,2,0(cid:105) 3 3 3 3 q ,(cid:104)1,0,0(cid:105) q ,(cid:104)0,0,0(cid:105) q ,(cid:104)0,0,0(cid:105) q ,(cid:104)0,0,0(cid:105) 4 4 4 4 Figure 2. A deduction tree in the BVASS of Figure 1. 3.2.1. Reachability. Given an ABVASS A, a finite set of states Q , and ¯0 (cid:96) a state q , the reachability problem asks whether A,Q (cid:46) q ,¯0; we call a r (cid:96) r reachability witness for (q ,¯0) more simply a reachability witness. r We will see in Section 4 that this reachability problem is equivalent to provability in LL; the problem is also related to games played over vectors of natural numbers, see Section 3.5. It is however undecidable: Fact 1. Reachability in ABVASS is undecidable. ¯0 Proof. Reachability is already undecidable in the more restricted model of AVASS, see Fact 2 below. (cid:3) 3.2.2. Lossy Reachability. In order to obtain decidability, we must weaken the ABVASS model or the decision problem. For the former, let us denote ¯0 by¯e theunitvectorinNd withoneoncoordinateiandzeroeverywhereelse. i Then a lossy ABVASS can be understood as featuring a rule q −−−¯e→i q for ¯0 every q in Q and 0 < i ≤ d. We rather define it by extending its deduction system with q,¯v loss q,¯v−¯e i foreveryqinQand0 < i ≤ d. Wewrite‘(cid:46) ’forrootjudgementswherelosses (cid:96) can occur. In terms of proof search in linear logic, losses will correspond to structural weakening, which is the distinguishing feature of affine linear logic. Top-Down Coverability. An alternative way to see the reachability problem in lossy ABVASS is to weaken the problem. Let us define a variant of ¯0 ABVASS that feature full resets instead of full zero tests: we denote in this ¯0 8 R.LAZIC´ ANDS.SCHMITZ :=¯0 case rules (q,q ) in T by q −−→ q and associate a different semantics: 1 z 1 q,¯v full-reset q ,¯0 1 We call the resulting model ABVASSr. Given an ABVASSr A, a state q , r and a finite set of states Q , the top-down coverability or leaf coverability (cid:96) problem asks whether there exists a deduction tree D with root label (q ,¯0) r and such that, for each leaf, there exists some q in Q and some ¯v in Nd (cid:96) (cid:96) such that the leaf label is (q ,¯v); we then call D a coverability witness. (cid:96) The reachability problem for lossy ABVASS is then equivalent to top- ¯0 down coverability for ABVASSr. Observe indeed that the unary, fork, and splitrulesaremonotone: if¯v ≤ w¯ fortheproductordering, i.e.if¯v(i) ≤ w¯(i) for all 0 < i ≤ d, and a configuration (q,¯v) allows to apply a rule and result in some configurations (q ,¯v ) and (possibly) (q ,¯v ), then (q,w¯) allows to 1 1 2 2 apply the same rule and to obtain some (q ,w¯ ) and (q ,w¯ ) with ¯v ≤ w¯ 1 1 2 2 1 1 and ¯v ≤ w¯ . This means that losses in an ABVASS can be applied as 2 2 ¯0 late as possible, either right before a full zero test or at the leaves—which corresponds exactly to top-down coverability for ABVASSr. 3.2.3. ExpansiveReachability. Inordertomodelstructuralcontractionsdur- ingproofsearch, itisnaturaltoconsideranothervariantofABVASS called ¯0 expansive ABVASS and equipped with the deduction rules ¯0 q,¯v+¯e i expansion q,¯v+2¯e i for every q in Q and 0 < i ≤ d. We write ‘(cid:46) ’ for root judgements where ex- e pansionscanoccur. ThisisarestrictionoverABVASS sinceexpansionscan ¯0 beemulatedthroughtwounaryrulesq −−−¯e→i q(cid:48) −2−¯e→i q. Expansivereachability is not quite dual to lossy reachability—we deal with increasing reachability in Section 7. 3.3. Restrictions. Note that ABVASS generalise vector addition systems ¯0 with states (VASS), which are ABVASS with only unary rules. They also ¯0 generalise two “branching” extensions of VASS, which have been defined in relation with propositional linear logic. Since these restrictions do not feature full zero tests, their lossy reachability problem is equivalent to their top-down coverability problem. 3.3.1. AlternatingVASS. wereoriginallycalled“and-branching”counterma- chinesbyLincolnetal.[18], andwereintroducedtoprovetheundecidability ofpropositionallinearlogic. Formally,anAVASSisanABVASS whichonly ¯0 features unary and fork rules, i.e. with T = T = ∅. s z Fact 2 (Lincoln et al. [18]). Reachability in AVASS is undecidable. Proof Idea. By a reduction from the halting problem in Minsky machines: ? note that a zero test q −c−=→0 q(cid:48) on a counter c can be emulated through a fork q → q(cid:48) ∧q , where unary rules q −−−¯e−→c(cid:48) q for all c(cid:48) (cid:54)= c allow to empty the c c c ¯0 counters different from c, and a last unary rule q →− q to the single target c (cid:96) state allows to check that c was indeed equal to zero. (cid:3) NON-ELEMENTARY COMPLEXITIES FOR BVASS, MELL, AND EXTENSIONS 9 AlternatingVASSdonotallowtomodelLLproofsearchinfull; Kanovich [13] identified the matching LL fragment, called the (!,⊕)-Horn fragment. The complexity of the other basic reachability problems on AVASS is known: • motivatedbythecomplexityoffragmentsofrelevancelogic,Urquhart [30]provedthatexpansivereachabilityiscompleteforAckermannian time, and • motivated by the complexity of vector addition games (see Sec- tion 3.5), Courtois and Schmitz [8] showed that lossy reachability is 2-ExpTime-complete. 3.3.2. BranchingVASS. Inspiredbythecorrespondencesbetweenthe!-Horn fragment of linear logic and VASS unearthed by Kanovich [13], de Groote et al. [9] defined BVASS—which they originally dubbed “vector addition tree automata”—as a model of counter machines that matches MELL. For- mally, a BVASS is an ABVASS with only unary and split rules, i.e. with ¯0 T = T = ∅. This model turned out to be equivalent to independently f z defined models in linguistics [24] and protocol verification [32]; see [25] for a survey. Whether BVASS reachability is decidable is an open problem, and is inter-reducible with MELL provability. Lazi´c [17] proved the best known lower bound to this day, which is 2-ExpSpace-hardness. Two related prob- lems were shown to be 2-ExpTime-complete by Demri et al. [10], namely increasing reachability (see Section 7) and boundedness. 3.3.3. Alternating Branching VASS. Kopylov [14] defined a one-player vec- tor game, which matches essentially the reachability problem in ABVASS, i.e. in ABVASS with T = ∅. The elementary fragment of ILL defined by ¯0 z Larchey-Wendling and Galmiche [16] is another counterpart to ABVASS. While allowing full zero tests is helpful in the reduction from LL provabil- ity, they can be dispensed with at little expense. Let us first introduce some notation. If node n is an ancestor of a node n(cid:48) in a deduction tree D, and the labels of n and n(cid:48) are the same, we write D[n ← n(cid:48)] for the shortening of D obtained by replacing the subtree of rule applications rooted at n by the one rooted at n(cid:48). Observe that, if D is a reachability witness (resp. a coverability witness), then D[n ← n(cid:48)] is also a reachability witness (resp. a coverability witness). Lemma 3. There is a logarithmic-space reduction from (lossy, resp. expan- sive)ABVASS reachabilityto(lossy, resp.expansive)ABVASSreachability, ¯0 andapolynomialtimeTuringreductionthatpreservesthesystemdimension. Proof. Suppose A is an ABVASS with set of states Q and dimension d. ¯0 For a logarithmic-space many-one reduction, the key observation is that, ifthereexistsawitnessforaninstanceof(lossy,resp.expansive)reachability forA, thenbyrepeatedshortenings, theremustbeoneinwhich, alongevery vertical path, the number of occurrences of full zero tests is at most |Q|−1. It therefore suffices to decide the problem for an ABVASS A† whose set of states is {1,...,|Q|}×Q, whose dimension is |Q|·d, and which simulates A up to |Q|−1 full zero tests along any vertical path. In any state (i,q), A† 10 R.LAZIC´ ANDS.SCHMITZ behaves like A in state q, but using the ith d-tuple of its vector components. To simulate a full zero test q −=−?→¯0 q(cid:48) in A, A† changes state from (i,q) to (i+1,q), postponing the check that the ith d-tuple of vector components are zero until the leaves of the deduction tree. For a polynomial time Turing reduction that preserves d, we define the set of root states relative to a subset X of Q by Root (X) d=ef {q ∈ Q | A,X (cid:46) q,¯0} (1) A as the set of states q such that there exists a deduction in A with root label (q,¯0) and leaf labels in X × {¯0}. The (lossy, resp. expansive) reachabil- ity problem for (cid:104)A,q ,Q (cid:105) then reduces to checking whether q belongs to r (cid:96) r Root (Q ). A (cid:96) LetA = (cid:104)Q,d,T ,T ,T ,T (cid:105). WritingA(cid:48)fortheABVASS(cid:104)Q,d,T ,T ,T ,∅(cid:105),we u f s z u f s can compute Root (X) using |Q| calls to an oracle for (lossy, resp. expan- A(cid:48) sive) ABVASS reachability. Moreover, since Root (X) ⊇ X is monotone, A(cid:48) wecanusealeastfixedpointcomputationthatdiscoversrootstatesaccord- ing to the number of full zero tests along the branches of their reachability witnesses: Root (Q ) = µX.Root (Q )∪Root (X ∪T−1(X)). (2) A (cid:96) A(cid:48) (cid:96) A(cid:48) z This computation converges after at most |Q| steps, and therefore works in polynomial time relative to the same oracle. (cid:3) 3.4. Computational Complexity. 3.4.1. Non-Elementary Complexity Classes. We will use in this paper two complexity classes [see 26]: Tower d=ef (cid:91) DTime(cid:0)tower(e(n))(cid:1) (3) e∈FElem is the class of problems that can be solved with a deterministic Turing machine in time tower of some elementary function e of the input, where tower(0) d=ef 1 and tower(n+1) d=ef 2tower(n) defines towers of exponentials. Similarly, Ackermann d=ef (cid:91) DTime(cid:0)Ack(p(n))(cid:1) (4) p∈FPR is the class of problems solvable in time Ack of some primitive recursive functionpoftheinputsize, where“Ack”denotestheAckermannfunction— any standard definition of Ack yields the same complexity class [26]. Completeness for Tower is understood relative to many-one elemen- tary reductions, and completeness for Ackermann relative to many-one primitive-recursive reductions. 3.4.2. ABVASS Complexity. ForasetT ofunaryrules,wewritemax−(T ) ¯0 u u (resp. max+(T )) for the largest absolute value of any negative (resp. posi- u tive) integer in a vector in T , and max(T ) for their overall maximum. We u u assume a binary encoding of the vectors in unary rules, thus max(T ) might u