# 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.

• I can't understand what your problem is. If you know how to compute the product of two transition systems, and you know how to execute the DFS, what exactly is your issue? You first compute the product to get a new transition system, then do DFS on that. It doesn't need to be any more complicated than that. What specifically are you stuck on?
– D.W.
Jan 8, 2015 at 23:38
• Is the PDF you linked to posted with permission on that site? We probably shouldn't be linking to copyright infringement. Jan 10, 2015 at 18:20
• I'm really not sure, as the site is in Russian. Taking that into account though I'll edit the main post to get rid of the link. Jan 12, 2015 at 16:08

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 {