Synthesis of Quasi-interpretations

This paper presents complexity results by showing that the synthesis of MaxPoly quasi-interpretations over reals is decidable in exponential time with fixed polynomial degrees and fixed max-degree and that the synthesis ofMaxPlus quasi-interpretations over reals is NPtime-complete with fixed multiplicative degrees and fixed max-degree. Quasi-interpretations are a tool that allows to control resources like the runtime, the runspace or the size of a result in a program execution. Quasi-interpretations assign to each program symbol a numerical function which is compatible with the computational semantics and roughly speaking provide an upper bound on sizes of intermediate values computed