Synthesis of max-plus quasi-interpretations

Abstract

Quasi-interpretations are a tool to bound the size of the values computed by a first-order functional program (or a term rewriting system) and thus a mean to extract bounds on its computational complexity. We study the synthesis of quasi-interpretations selected in the space of polynomials over the max-plus algebra. We prove that the synthesis problem is NP-hard under various conditions and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. We provide a polynomial time algorithm to synthesize homogeneous quasi-interpretations of bounded degree and show how to extend the algorithm to synthesize (general) quasi-interpretations. The resulting algorithm generalizes certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity.