I need a help with a formal definition of breadth first search algorithm for vertices traversal in case that a graph contains forbidden vertices. For example:
For a given graph G (V, E) and set of forbidden vertices F, define a set of traversed vertices T.
Algorithm starts e.g. from vertex s.
How to formally define a set of traversed vertices?
It sounds like you are looking for "the connect component of $G-F$ containing the vertex $s$". If we are just talking about (possibly edge-weighted) graphs, this is what you want. The notation $G-F$ means the graph $G$ with the vertices of $F$ and all edged incident to vertices in $F$ deleted. This could make the graph disconnected, and in a breadth first search we can only travel within the connected component we start.
If you are talking about directed graphs, the answer is not so clear, as there could be vertices in the connected component of $G-F$ containing $s$ that are not accessible from $s$. There may be no better term here than the graph induced in $G-F$ by the breadth first search tree starting at $s$ in $G-F$.