McNet : Loop Unrolling with Pivot being the Initial State

[ssoelvsten]

One can skip an entire relnext*() operation in the Chain algorithm by abusing the following insights:

• Consider the initial state the first pivot
• Here, the already computed set reachable is the entire forward set.
• Hence, the only thing still missing is the backwards set (relprev*()).

So, one can essentially do a loop-unrolling with the initial state as the pivot. This can potentially (in the best case) result in halving the number of symbolic steps.