Space-bound discovery by exit reachability
ID: space-bound-discovery-by-exit-reachability
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 space, doubling stops at . Each budget test uses the Savitch theorem recursion and the storage is reused. The method discovers a sufficient bound without computing .
New to topics? Read the docs here!