Linear tree constraints are given by pointwise linear inequalities between infinite trees labeled with nonnegative rational numbers. Satisfiability of such constraints is at least as hard as solving the Skolem-Mahler-Lech problem. We provide an interesting subcase, for which we prove that satisfiability is decidable. Our decision procedure is based on intricate arguments using automata and combinatorics of words.

Our subcase allows to construct an inference mechanism for resource bounds of object oriented Java-like programs: actual resource bounds can be read off from solutions of tree constraints. So far, only the case of degenerated tree constraints (i.e. lists) was known to be decidable which, however, is insufficient to generally solve the given resource analysis problem. The present paper therefore provides a generalisation to trees of higher degree in order to cover the entire range of constraints encountered by resource analysis.