Decision Diagrams , Bisimulation 2016 September exam paper

Question

Question 2)c) BDD

How is the propositional formula a ∧ ¬c ∨ c ∧ ¬b obtained for the given ROBDD diagram?

Question 3) Simulation

The state pair (s3, q0), (s3,q2) is written in step s0. I am not sure if it was written accidentally since there is not state s3.

Answer 1

First question: you have to enumerate the paths from the root node to the 1-leaf as conjuncts for a DNF. There are two paths c&!b and !c&a from the root node c.

Second question: yes, there is something wrong. As far as I can say, states Si should be Qi and Qi should be Si. But that is also mentioned in the solution.