[Termtools] Complexity of ITSs

[Juergen Giesl]

Dear all,

as asked by Johannes, below I attach again the summary of our discussion
among the tool authors for complexity of integer transition systems. For
the category in Koat-syntax, the details of the input format are clear. For
the category in C-syntax, these details were not discussed yet. In
particular, there is a problem with non-deterministic values. As far as I
see, Loopus considers them as input, whereas all other tools (and the
translators) don't do that. So in contrast to Loopus, they would consider
the runtime as "unbounded" if it depends on such non-deterministic values.
Therefore, at the moment, the answers of the tools are not really
comparable.

Best Regards
Juergen

--------------------------------------------------------------------------------

After a long discussion, we reached a consensus among the authors of the
tools for complexity analysis of integer transition systems:

   - There will be 2 categories for complexity analysis of integer
   programs. In one category, the input are non-recursive (i.e., tail
   recursive) programs with single destination locations in Koat-syntax and in
   the other category, the input is given in C-syntax.
   - If a tool uses a translator from the input format to its own format,
   the runtime of this translator should not count towards the time limit of
   30 seconds.
   - The output format is similar to the output format for complexity of
   TRSs (see below for details).
   - In each of these categories, there will be a winner when considering
   only upper bounds, and a winner when considering both upper and lower
   (worst-case) bounds. See below for more details on scoring.

Most likely, the following tools will participate in both of these
categories: CoFloCo, Loopus, TCT, AProVE, and probably also RanK. So this
seems to be a real interesting competition!

For the output format, we use the same format as for complexity of term
rewriting:


> The output written to the first line of STDOUT shall be a complexity
> statement according to the following grammar:
>


S -> MAYBE | WORST_CASE(L,U) | WORST_CASE(?,U) | WORST_CASE(L,?)
> L -> Omega(n^Nat) | NON_POLY
> U -> O(1) | O(n^Nat) | POLY
>


where "Nat" is a non-zero natural number and WORST_CASE(L,U) means L (U) is
> a lower (upper) bound. Here "Omega(n^k)" is the usual Omega notation and
> "NON_POLY" refers to an unspecified exponential. On the other hand "O(n^k)"
> is the usual big-Oh notation and "POLY" indicates an unspecified
> polynomial. Either of the functions L, U (but not both) may be replaced by
> "don't know", indicated by ?.


When considering both upper and lower bounds, we use the same scoring
algorithm as for complexity of ITSs:

Scoring is for lower and upper bounds. We make use of two linear orders,
> one for upper bounds and one for lower bounds. The minimal element for
> upper bounds is "O(1)", the maximal "?". With respect to lower bounds the
> minimal element is "NON_POLY". Again the maximal element is "?". Trivial
> answers count as "?". The following scoring algorithm is used. Firstly,
> given k answers (low1,up1) … (low_k,up_k) on a specific program, two
> rankings are determined, for lower and upper bounds independently. For the
> lower bounds ranking, the best tool(s) get k points, the second best
> tool(s) get k-1 points, etc, where giving the trivial answer always gives 0
> points. Similarly, each tool gets the points for the upper bounds ranking.
> And the final score is just the sum of the points for upper and lower
> bounds.


When considering only upper bounds, the above algorithm is adapted by
ignoring lower bounds.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20160819/2897677f/attachment.html>