zbMATH — the first resource for mathematics

Decidable inequalities over infinite trees. (English) Zbl 1415.68059
Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 111-130 (2018).
Summary: Linear tree constraints are given by pointwise linear inequalities between infinite trees labeled with nonnegative rational numbers. Satisfiablity 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 satisfiablity 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.
For the entire collection see [Zbl 1407.68021].
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B25 Decidability of theories and sets of sentences
03D05 Automata and formal grammars in connection with logical questions
68R15 Combinatorics on words
Full Text: DOI