FSM to Kripke Q2 [closed]

Question

Given a FSM: A={2Vin,2Vout,I,2Vstate,R}A={2Vin,2Vout,I,2Vstate,R}
where Vin={a}Vin={a}, Vout={o}Vout={o}, Vstate={p,q}Vstate={p,q}, I=I=!p,
R=R=next(q)&(next(p)|(p->q))&!(o|a)

a)

• label 0:; 1:p; 2:q; 3:p,q;
      i.e., node s0-s3 represent states !p&!q, p&!q, !p&q and p&q, respectively.
• inputs {a},{};
      i.e., two inputs represent a and !a, respectively.
• outputs {o},{};
      i.e., two outputs represent o and !o, respectively.
• init 0,1;
      i.e., s0 and s1 are initial states.
• transitions (0,{a},{o},1); (0,{},{o},2); (1,{a},{},3); (3,{},{},3);
• represents the following state transition diagram in an explicit form:

What is the process to solve this?

Answer 1

see if this helps

https://q2a.cs.uni-kl.de/2361/vrs-sheet4-q2-fsm-to-kripke  somewhat similar.

Comments

I couldn't understand this.

Answer 2

To get the transitions of the FSM which is given in a symbolic representation, you have to compute all satisfying assignments of its transition relation. 

The transition relation next(q)&(next(p)|(p->q))&!(o|a) has the following models that you can compute using BDDs, DNFs or simply the truth table (the latter is not recommended). Below is the formula given in DNF:

    !p&!q&!a&!o&!next_(p)&next_(q) | 
    !p&!q&!a&!o& next_(p)&next_(q) | 
    !p& q&!a&!o&!next_(p)&next_(q) | 
    !p& q&!a&!o& next_(p)&next_(q) |
     p&!q&!a&!o& next_(p)&next_(q) | 
     p& q&!a&!o& next_(p)&next_(q) | 
     p& q&!a&!o&!next_(p)&next_(q)  

Each satisfying assignment is a transition of the FSM that you should then submit as described with the example under part a).

Comments

Thank you. This is clear now!