We prove the decidability of the static fragment of ambient logic,
with composition adjunct and iteration, which corresponds to a kind
of regular expression language for semistructured data. The essence
of this result is a surprising connection between formulas in the
ambient logic and counting constraints on (nested) vectors of
integers.
Our proof method is based on a new class of tree automata for
unranked, unordered trees, which may result in practical algorithms
for deciding the satisfiability of a formula. A benefit of our
approach is to naturally lead to an extension of the logic with
recursive definitions, which is also decidable. Finally, we identify
a simple syntactic restriction that improves the effectiveness of
our algorithms on large examples.
