Depth-First Search: With Depth-First Search (DFS), the model checker begins at the start state and explores each of its outgoing transitions to other states as far as possible along each branch before backtracking and selecting the next transition. DFS goes deeper and deeper until a goal state is reached (e.g., an error statesuch as a deadlock) or it hits a state with no outgoing or unexplored transition (e.g., an end state). The search backtracks, returning to the most recent state with unexplored transitions. A stack is usually used to hold the frontier (the set of states that are still in the process of being explored), and therefore the last state added to it is always selected first during the search.