SNF for LTL state transition

Question

Thank you for answering the question and suggestión. I am able to gain some clarity.

I think the question is possible to solve using SNF. Can you please show me the SNF table for Sept 2022 Problem 6a for  for p,q,pq,{}.

Answer 1

Well, using the teaching tool,  I get the following SNF which is not as nice as the BDD since there are some sub-formulas that can be shared:

•     (q ? (b ? false
              : (Xq ? (a ? (Xp ? true
                               : false)
                         : (p ? (Xp ? true
                                    : false)
                              : (Xp ? false
                                    : true)))
                    : false))
         : (a ? (Xp ? true
                    : false)
              : (p ? (Xp ? true
                         : false)
                   : (Xp ? false
                         : true))))