Representation minimization

The algorithms implemented in Nancy are rooted in mathematical properties of the result of an operation which can be derived regardless of its shape, before the computation is performed. In particular, the parameters $T$, $d$ and $c$ that are necessary to have a finite the representation of the result. On one hand these are critical enablers for algorithms, on the other they may be pessimistic, and make us compute a larger representation than needed.

In turn, when this result is used as an operand of a following operation, these overestimated parameters are used to further overestimate the following result, and so on obtaining the effect often referred to as state-space explosion.

To contain this phenomenon, Nancy employs an efficient representation minimization algorithm to reduce a result to its minimal representation.

This is done in two ways: first, the periodic part is factorized to find the minimal period. The process is optimized by reducing the tested factorizations to only the prime numbers that fit the criteria to be feasible divisors.

A period which is divisible by 3.

Then, the transient part is reduced by anticipating the start of the periodic part, if that is possible.

A reducible transient.

For more details, checkout the paper [ZS23] or [Zippo23], Chapter 12.