Applying DFS algorithm to a transition system to find reachable states Currently working on a past exam question which tells me to compute the product of two transition systems and then use DFS to find the reachable states of the product. I learnt how to compute the product of transition systems by looking at pages 43 and 44 in the "Principles of Model Checking" book by Christel Baier and Joost-Pieter Katoen (if anyone has a copy). 

I understand that the way they found the reachable states in page 44 is by tracking the value of the variable y for each state and seeing if it holds, but in my particular question I'm not using a program graph; it's a transition system that uses only sigma and gamma (as handshake actions). My first question is how do I determine what is a reachable state and what is not in a product of transition systems?

Secondly, how would I show that I used DFS on paper? I couldn't find any useful articles online about it and our lecture notes don't cover it for some reason.
You can design an algorithm to traverse the product of two TSs.
With a simple DFS algorithm, start from start state and with rules for handshaking generate next states.
You need to keep the states that has been visited so far to avoid loop.
There may be more efficient ways but here is a sudo-code of a solution:

stack = new Stack()  
visited_states = new Array()  
stack.push(start_state)  
while ~stack.isEmpty() {  
    current_state = stack.pop()  
    if current_state not in visited_states {  
        visited_states.add(current_state)  
        next_states = generate_next_states(current_state)  
        for each state in next_states {  
            stack.push(state)  
        }  
    }  
}  


Where generate_next_states is a function that generates next states according to the rule in page 48, Figure 2.11.
Now the set of states in visited_states are reachable states.