LTL state transition

Question

Thank you for answering our questions

Sept 2022 Problem 6a

Can you please show me the truth table for p,q,pq,{}

  1.where p=0 and q =1. I m landing at (p' <-> a) & (!b & q). I am getting a transition from s1 to s2 on giving input 'a' (considering p' <-> a).

 2 where p=1 and q=0. I m landing at (p')&(!(!b&q)) = p'&(b|q). I m confused with drawing the transistion for p'&(b|q).

Answer 1

The truth table would have 64 entries for the variables p,q,a,b,Xp,Xq which is not recommended here. Instead, I show you a BDD with the optimal variable ordering which is quite small: 

We may also read a DNF from this diagram:

     !Xp&!p&!a&!q  |
     !Xp&!p&!a&Xq&!b&q |
      Xp&p&!a&!q |
      Xp&p&!a&Xq&!b&q |
      Xp&a&!q |
      Xp&a&Xq&!b&q

Comments

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,{}.