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.

  • $\begingroup$ 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? $\endgroup$
    – D.W.
    Jan 8, 2015 at 23:38
  • 1
    $\begingroup$ Is the PDF you linked to posted with permission on that site? We probably shouldn't be linking to copyright infringement. $\endgroup$ Jan 10, 2015 at 18:20
  • $\begingroup$ 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. $\endgroup$ Jan 12, 2015 at 16:08

1 Answer 1


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()  
while ~stack.isEmpty() {  
    current_state = stack.pop()  
    if current_state not in visited_states {  
        next_states = generate_next_states(current_state)  
        for each state in next_states {  

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.

  • $\begingroup$ Just finished reading page 48. I couldn't make much sense from it - is it basically saying that if 2 states exchange handshake actions then they are reachable from one another? The DFS pseudo-code makes sense, I just have to be clear first on what is considered a reachable state before I can give it a go. Thanks for the reply $\endgroup$ Jan 8, 2015 at 15:04
  • $\begingroup$ Product of 2 TS represents a super-system consists of two sub-systems. Handshake is a synchronization mechanism for sub-systems. Consider a sub-system wants to send data to another and there is no buffer, so the action of communication of these two should be of handshake type, it is done if both sub-systems perform it: the sender sends the data and receiver receives it. When two sub-systems handshake, each one goes from one state to another (s1->s2 and s'1->s'2) and super-system goes from state (s1,s'1) to (s2,s'2). So when two sub-systems handshake state (s2,s'2) is reachable from (s1,s'1). $\endgroup$ Jan 8, 2015 at 19:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.