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 inﬁnite 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 satisﬁability 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 inﬁnite trees falls into the area of convex optimisation.

Document Actions