algorithm - BFS有向グラフトラバーサルアルゴリズムが終了可能であることを証明する方法は?

Question

BFS有向グラフトラバーサルアルゴリズムが終了可能であることを証明する方法は? (ここから疑似コードをコピーします) 入力: グラフ G と G のルート v

  procedure BFS(G,v):
      create a queue Q
      enqueue v onto Q
      mark v
      while Q is not empty:
          t ← Q.dequeue()
          if t is what we are looking for:
              return t
          for all edges e in G.incidentEdges(t) do
             o ← G.opposite(t,e)
             if o is not marked:
                  mark o
                  enqueue o onto Q

Answer 1

すべてのノードは最大で 1 回訪問 (マーク) されるため、最悪の場合、すべてのノードをマークすると、アルゴリズムが終了します。