# FSM to Kripke Q2 [closed]

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?

closed with the note: Answer solved

closed

+1 vote
see if this helps

https://q2a.cs.uni-kl.de/2361/vrs-sheet4-q2-fsm-to-kripke  somewhat similar.
by (290 points)
I couldn't understand this.
+1 vote

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).

by (170k points)
edited by
Thank you. This is clear now!