I have a finite automaton with these properties:
- Contains cycles
- It's a directed graph
- All the states/nodes are initialy reachable from the initial state
- It has final states but I guess it isn't relevant for my issue
- It's a random generated automaton, and the generation isn't meant to satisfy properties like strongly connected components or connected components
Let's suppose I have to delete an edge.
I need to know if there's a way to prove that the reached state by this edge is still reachable from the initial state without using a classical search (DFS or BFS); obviously, if there is any.