=================================================================================

Slightly different from Depth-First Search (DFS), Breadth-First Search (BFS) is a graph traversal algorithm that explores all the vertices of a graph in breadthward motion, i.e., it visits all the vertices at the same level before moving on to the next level. It starts from the source vertex and systematically explores the adjacent vertices. 

The basic steps of BFS are: 

     i) Start with the source vertex: 

Begin at the specified source vertex and mark it as visited. 

     ii) Explore neighbors at the current level: 

Visit all the neighbors (adjacent vertices) of the current vertex. Mark each neighbor as visited and enqueue them. 

     iii) Move to the next level: 

Move to the next level by dequeuing the current vertex and selecting the next vertex from the queue. 

     iv) Repeat until all vertices are visited: 

Continue this process until all vertices in the graph are visited or until a specific condition is met. 

BFS is commonly implemented using a queue data structure. In the algorithms and data structures, the queue is often implemented using arrays or linked lists. The queue is a first-in, first-out (FIFO) data structure.  The two primary operations on a queue are: 

     i) Enqueue (Push): Adds an element to the back of the queue.

     ii) Dequeue (Pop): Removes the element from the front of the queue. 

The queue helps maintain the order in which vertices are visited. The algorithm ensures that all vertices at the current level are visited before moving on to the vertices at the next level. One of the key applications of BFS is finding the shortest path between two nodes in an unweighted graph. The first time a vertex is visited during BFS, it is the shortest path to that vertex since the algorithm always expands the shallowest node in the frontier first. If the graph is weighted, a variation of BFS called Dijkstra's algorithm is often used for finding the shortest path. BFS has a time complexity of O(V + E), where V is the number of vertices and E is the number of edges in the graph.  

Figure 3646a demonstrates maze solving with BFS.

Figure 3646a. Demonstration of  maze solving with BFS (code). 

The breadth-first search algorithms can also be used  for Model Checking. For instance, this script here  is an example of Python scripts using breadth-first search for Model Checking.

Script explanation:

The deque class from the collections module is a deque (double-ended queue) which is used to efficiently implement a queue data structure with fast O(1) append and pop operations from both ends:

from collections import deque 

Defining breadth_first_search function: 

def breadth_first_search(graph, start, target): 

visited = set() 

queue = deque([start]) 

while queue: 

current = queue.popleft() 

if current == target: 

return True 

if current not in visited: 

visited.add(current) 

queue.extend(graph[current]) 

return False 

The property target is set to vertex 4. Model checking is performed by calling model_check with the graph, starting vertex (0), and the property target (4): 

g = Graph(vertices) 

g.add_edge(0, 1) 

g.add_edge(0, 2) 

g.add_edge(1, 3) 

g.add_edge(2, 4) 

Output from the script execution:

        

============================================