You will be presented with the full text of a science research paper. Please write an abstract for this paper. Your response should include the abstract and no additional text.

Paper text:
before presenting details of this small contribution to the on - going investigation of complexity - theoretic properties of vector addition systems , their extensions and related logics on words and trees with unbounded data , we provide a brief overview of most - closely related research .
a diagrammatic summary is in figure  [ f:1 ] , where boldface and a thicker line indicate the new results .
[ [ vas . ] ] vas .
+ + + +    vector addition systems , or equivalently petri nets , are a fundamental and established model of concurrency .
they support an active and broad research community , with long - standing links to industry , where vas are an important modelling formalism and associated tools are extensively used .    in spite of several decades of research ,
the computational complexity of the reachability problem for vas remains one of the most well - known open questions in theoretical computer science .
while decidability was still unknown , lipton made initial progress on the problem by showing it expspace - hard @xcite , which is still the highest known lower bound .
a few years later , mayr showed the problem decidable @xcite .
although his proof was subsequently substantially simplified by kosaraju @xcite , lambert @xcite and in a remarkable recent series of articles by leroux @xcite , it is still unknown even whether there exists a primitive recursive algorithm for the problem .
[ [ branching - vas . ] ] branching vas .
+ + + + + + + + + + + + + +    whereas computations of vas are words of vectors of natural numbers , bvas are a natural generalisation whose computations are trees of such vectors .
although their reachability problem has been shown inter - reducible with the emptiness problem for multiple - valued linear index grammars @xcite , and with the provability problem for multiplicative exponential linear logic , the decidability status remains an open question .
however , curiously , a lower bound that is two notches above adding alternation to lipton s result , namely 2expspace - hardness , was recently shown  @xcite .    [ [ priority - vas . ] ] priority vas .
+ + + + + + + + + + + + +    equipping two counters ( in petri - speak , places ) with zero tests , of course , makes vas as powerful as minsky machines and the reachability problem undecidable .
it has turned out , though , that the mayr - kosaraju - lambert proof can be extended when only one counter may be tested for zero .
in fact , reinhardt has obtained a highly non - trivial proof of an even more general result : that reachability is decidable for _ pvas _ , where one may test whether all counters from any one of a series of sets @xmath0 are zero @xcite . so far with one zero - testable counter
, bonnet has succeeded in greatly simplifying reinhardt s proof along the lines of leroux @xcite .
let us say that pvas whose series of zero - testable sets of counters have length @xmath1 are of _ index _
@xmath1 .
[ [ stack - vas . ] ] stack vas .
+ + + + + + + + + +    another natural extension of vas is to allow them to use a stack over a finite alphabet .
equivalently to these systems , which we call svas and whose motivations include modelling software with integer variables and call - return procedures , one may consider intersections of vas languages and context - free languages . for an svas in that alternative presentation ,
let us say that it is of _ index _
@xmath1 if and only if the context - free language is of index @xmath1 , i.e.  there is a context - free grammar such that every word in the language has a derivation whose every step contains at most @xmath1 non - terminal symbols .
atig and ganty have recently shown that finite - index svas are essentially equivalent to pvas : every index-@xmath1 svas can be simulated by an index-@xmath1 pvas , and every index-@xmath1 pvas can be simulated by an index-@xmath2 svas @xcite .
incidentally , that seems to be the only interesting known relationship among bvas , pvas and svas .
the reachability problem for finite - index svas is consequently decidable since it is decidable for pvas .
although decidability for unrestricted svas remains an open question , we make some progress here in the opposite direction , obtaining that the problem is not elementary .
that puts svas in contrast to bvas , for which decidability is also unknown but so far there is only an elementary lower bound @xcite .
[ [ coverability . ] ] coverability .
+ + + + + + + + + + + + +    the well - known coverability problem for vas and their extensions corresponds to `` control - state reachability '' : it asks whether a given system can reach a configuration that is pointwise ( i.e. , for each counter ) greater than or equal to a given configuration .
lipton s and rackoff s classical results show that coverability for vas is expspace - complete @xcite , and by building on those works , demri et al .
have shown 2exptime - completeness of the problem for bvas @xcite .
unfortunately , for pvas and svas , there is no hope for such results , since for both classes of systems , there are straightforward reductions of reachability to coverability .
[ [ variable - fo - on - data - words - and - data - trees . ] ] 2-variable fo on data words and data trees .
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +    partly motivated by verification of concurrent systems and by querying of xml databases , in recent years there has been extensive research in logics on data words and data trees .
in addition to letters from a finite alphabet as classically , the latter structures have labels from an infinite domain , which are called _ data _ and on which only certain operations are available .
in fact , typically , the data can only be compared for equality , and that is the only operation we consider here .
remarkably , there are several connections between , on one hand , vas and their extensions that we have introduced , and on the other hand , two - variable first - order logics on data words and data trees . for positions @xmath3 and @xmath4 of a data word ,
the logics have navigational predicates @xmath5 and @xmath6 , as well as equality of data labels @xmath7 . on data trees , where variables range over nodes , navigational predicates are either vertical ( `` child '' and `` descendant '' ) , or horizontal ( `` next sibling '' and `` following sibling '' ) , or compare nodes for positions in the pre - traversal ( `` document order '' ) .    on data words ,
bojaczyk et al .
@xcite showed that the satisfiability problem for such a logic reduces in doubly - exponential time to the reachability problem for vas , and is therefore decidable .
moreover , they exhibited a polynomial - time converse reduction , and so lipton s lower bound carries over to the logic .
on data trees , the picture is more complicated .
already without document order , bojaczyk et al .
@xcite observed that the satisfiability problem is at least as hard as the reachability problem for bvas ( whose decidability is open ) , but obtained decidability by disallowing also the transitive navigational predicates ( `` descendant '' and `` following sibling '' ) .
another way of getting decidability was found by bjrklund and bojaczyk : no restrictions on the navigational predicates are required provided the depth of data trees is bounded . with that assumption , they showed how to reduce satisfiability to the reachability problem for pvas .
an alternative restriction on data trees suggests itself : that data labels be allowed only on leaf nodes .
although decidability of the full 2-variable fo on such structures remains open , we show that even without the `` descendant '' and `` following sibling '' predicates , satisfiability is at least as hard as the reachability problem for svas , and so is not elementary .
( 60,27)(0,-1 ) ( vas)(30,2.5 )    [ cols="^",options="header " , ]     ( vas , bvas ) ( vas , pvas ) ( pvas , svas ) ( vas , vas2 ) ( vas2,vas ) ( bvas , bvas2 ) ( pvas2,pvas ) ( svas , svas2 )
it is convenient for our purposes to formalise svas as programs which operate on non - negative counters and a finite - alphabet stack .
more precisely , we define them as finite sequences of commands which may be labelled , where a command is one of : an increment of a counter ( @xmath8 ) , a decrement of a counter ( @xmath9 ) , a push ( @xmath10 ) , a pop ( @xmath11 ) , a non - deterministic jump to one of two labelled commands ( @xmath12 ) , or termination ( @xmath13 ) . initially , all counters have value @xmath14 and the stack is empty . whenever a decrement of a counter with value @xmath14 or an erroneous pop is attempted , the program aborts . in every program ,
@xmath13 occurs only as the last command .
the reachability problem can now be stated as follows : given an svas , does it have a computation which reaches the @xmath13 command with all counters being @xmath14 and the stack being empty ?
the reachability problem for svas is not elementary .
the proof is by reducing from the @xmath15-bounded halting problem for _ counter programs _ with @xmath16 commands , where :    * for @xmath17 , the _ tetration _ operation @xmath18 is defined by @xmath19 and @xmath20 ; * the counter programs are defined like svas , except that they have no stack , have only deterministic jumps ( @xmath21 ) , but can test counters for zero ( @xmath22 ) ; * the @xmath15-bounded halting problem asks whether @xmath13 is reachable by a computation during which all counter values are at most @xmath23
.    given such a counter program @xmath24 , we construct in time polynomial in @xmath16 an svas @xmath25 which simulates @xmath24 as long as its counters do not exceed @xmath23 . as in stockmeyer s yardstick construction @xcite ,
the idea is to bootstrap the ability to simulate zero tests of counters that are bounded by @xmath26 , @xmath27 ,  , @xmath23 .
more precisely , for each counter @xmath3 of @xmath24 , @xmath25 has a pair of counters @xmath3 and @xmath28 , on which it maintains the invariant @xmath29 .
thus , every increment of @xmath3 in @xmath24 is translated to @xmath30 in @xmath25 , and similarly for decrements .
for every zero test of @xmath3 in @xmath24 , @xmath25 uses auxiliary counters @xmath31 and @xmath32 , for which it also maintains @xmath33 .
moreover , we assume that @xmath34 at the start of each zero - test simulation .
the simulation begins by @xmath25 transferring some part of @xmath28 to @xmath31 ( while preserving the invariants ) .
it then calls a procedure @xmath35 which decrements @xmath31 exactly @xmath23 times . for the latter to be possible ,
@xmath3 must have been @xmath14 .
otherwise , or in case not all of @xmath28 was transferred to @xmath31 , the procedure can only abort .
when @xmath35 succeeds , the initial values of @xmath3 and @xmath28 are reversed , so to finish the simulation , everything is repeated with @xmath3 and @xmath28 swapped .
the main part of the construction is implementing @xmath36 for @xmath37 . assuming that @xmath36 which decrements @xmath38 exactly @xmath39 times and maintains @xmath40 has been implemented for some @xmath41 , @xmath42 consists of performing the following by means of @xmath38 , @xmath43 and @xmath36 :    * push exactly @xmath39 zeros onto the stack ;
* keep incrementing the @xmath44-digit binary number that is on top of the stack until no longer possible , and decrement @xmath45 for each such increment ; * pop @xmath39 ones that are on top of the stack , and decrement @xmath45 once more .    by a similar pattern , starting with all counters having value @xmath14
, @xmath25 can initialise each auxiliary counter @xmath43 to @xmath39 , and each @xmath28 to @xmath23 , as required .
let _ leaf - data forests _ be data forests in which data labels are present only at leaf nodes .
more precisely , they are finite forests such that :    * the root nodes are linearly ordered ; * each node is either a leaf , or its children and their descendants form a leaf - data forest ; * each node has a label from a finite alphabet @xmath46 ; * each leaf node also has a label from an infinite domain ( say , @xmath47 )
.    now , let fo@xmath48 denote the two - variable first - order logic on leaf - data forests that has the following predicates :    * a unary predicate for each letter from @xmath46 ; * @xmath49 ( @xmath4 is a child of @xmath3 ) and @xmath50 ( @xmath4 is the next sibling of @xmath3 ) ; * @xmath51 ( @xmath3 and @xmath4 are leaves , and @xmath3 precedes @xmath4 in the document order ) ; * @xmath7 ( @xmath3 and @xmath4 are leaves with the same data label ) .
the reachability problem for svas is reducible in logarithmic space to the satisfiability problem for fo@xmath48 on leaf - data forests .
the proof is based on encoding svas computations as leaf - data forests . in the latter , their tree structure is used to represent the evolution of the stack , and data labels are employed for keeping track of counter values .    more concretely ,
suppose @xmath52 is an svas .
we show how to compute in logarithmic space a sentence @xmath53 of fo@xmath48 whose models are exactly leaf - data forests that encode in the following manner computations of @xmath52 that halt with all counters @xmath14 and the stack empty :    * the computation that such a leaf - data forest encodes can be obtained by traversing the forest so that each internal node is visited once before its children ( generating a push ) and for a second time after its children ( generating the corresponding pop ) ; * each leaf node is labelled either by a jump command , or by an increment or a decrement , and in the latter cases , mutually distinct data labels are used to distinguish among increments of the same counter and to match them to its decrements ; * each internal node is labelled by a pair consisting of a push command and the pop command that corresponds to it in the computation .
i am grateful to mikoaj bojaczyk and anca muscholl for outlining to me the reduction from svas reachability to fo@xmath48 satisfiability on leaf - data trees .
by adapting the iterative yardstick construction of stockmeyer , we show that the reachability problem for vector addition systems with a stack does not have elementary complexity . as a corollary , 
 the same lower bound holds for the satisfiability problem for a two - variable first - order logic on trees in which unbounded data may label only leaf nodes . 
 whether the two problems are decidable remains an open question .