Logics of Repeating Values on Data Trees and Branching Counter Systems

We study connections between the satisfiability problem for logics on data trees and Branching Vector Addition Systems BVAS. We consider a natural temporal logic of "repeating values" LRV featuring an operator which tests whether a data value in the current node is repeated in some descendant node. On the one hand, we show that the satisfiability of a restricted version of LRV on ranked data trees can be reduced to the coverability problem for Branching Vector Addition Systems. This immediately gives elementary upper bounds for its satisfiability problem, showing that restricted LRV behaves much better than downward-XPath, which has a non-primitive-recursive satisfiability problem. On the other hand, satisfiability for LRV is shown to be reducible to the coverability for a novel branching model we introduce here, called Merging VASS MVASS. MVASS is an extension of Branching Vector Addition Systems with States BVASS allowing richer merging operations of the vectors. We show that the control-state reachability for MVASS, as well as its bottom-up coverability, are in 3ExpTime. This work can be seen as a natural continuation of the work initiated by Demri, D'Souza and Gascon for the case of data words, this time considering branching structures and counter systems, although, as we show, in the case of data trees more powerful models are needed to encode satisfiability.