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!