Abstract
Several logic-based decision problems have been shown to be reducible to the emptiness problem of automata. In a similar way, non-standard reasoning problems can be reduced to the computation of the behaviour of weighted automata. In this paper, we consider a variant of weighted Büchi automata working on (unlabeled) infinite trees, where the weights belong to a lattice. We analyse the complexity of computing the behaviour of this kind of automata if the underlying lattice is not distributive. We show that the decision version of this problem is in ExpTime and PSpace-hard in general, assuming that the lattice operations are polynomial-time computable. If the lattice is what we call "linear-space-computable-encoded", then the upper bound can be reduced to PSpace, but the lower bound also decreases to NP-hard and co-NP-hard. We conjecture that the upper bounds provided are in fact tight.