Bounded Searches:
Bounded Depth-First Search (BDFS) works exactly like Depth-First Search, however avoids some of its drawbacks by imposing a maximum limit on the depth of the search. Even when the search is capable of exploring transitions to states beyond that depth, this will not do so and thereby it will not follow infinitely deep paths or get stuck in cycles. Therefore, it can find a solution only if it is within the depth limit. For essentially infinite-state systems (e.g., in our DEOS case study) limiting the depth is the only practical way to use DFS, but finding the proper depth can be difficult and large depths may result in extremely long counterexamples.
In practice, you can run the model checker with BDFS strategy multiple times, each and every time with ever-increasing depth limits (0, 1, 2, …). This is called Iterative Deepening Depth-First Search. This way we still have the advantage over BFS that space complexity is O(n), and we have the advantage over DFS that we are guaranteed to find the solution with the shortest path from the root. We can also show that the time complexity of iterative deepening is not much worse than for breadth-or depth-first search.
Similarly, a Bounded Breadth-First Search (BBFS) works exactly like Breadth-First Search, but it imposes a maximum limit on the number of neighboring states.