Breadth-First Search: With Breadth-First Search (BFS), the model checker again begins at the start state and explores all its outgoing transitions to the neighboring states. Then for each of those nearest states, it explores all of its outgoing transitions to its neighbor states, and so on, until it hits a goal state or a state with no outgoing or unexplored transition. A queue is usually used to hold the frontier, and therefore the first state added to it is always selected first during the search.