Space-bound discovery by exit reachability (source code)

= Space-bound discovery by exit reachability
{title2=$m\leftarrow2m$}

For a bounded-space machine, start with a logarithmic work budget and test accepting reachability and reachability of a transition leaving the budget. Accept if acceptance is found, double the budget if an exit is reachable, and otherwise reject. If all paths use at most $Cs(n)$ space, doubling stops at $O(s(n))$. Each budget test uses the <Savitch theorem> recursion and the storage is reused. The method discovers a sufficient bound without computing $s(n)$.