Links und Funktionen

You are here: Home / Publikationen / Linear Constraints over Infinite Trees


Martin Hofmann and Dulma Rodriguez (2012)

Linear Constraints over Infinite Trees

In: LPAR, pp. 343-358.

In this paper we consider linear arithmetic constraints over infinite trees whose nodes are labelled with nonnegative real numbers. These constraints arose in the context of resource inference for objectoriented programs but should be of independent interest. It is as yet open whether satisfiability of these constraint systems is at all decidable. For a restricted fragment motivated from the application to resource inference we are however able to provide a heuristic decision procedure based on regular trees. We also observe that the related problem of optimising linear objectives over these infinite trees falls into the area of convex optimisation.

Resource analysis, Infinite trees, Constraints

Document Actions