VRS Sheet4 Q2 - FSM to Kripke

Question

In the exercise sheet 4. Question 2.

Could you please give some insights as to how to solve the Q2 and Q3.

I am not getting how to proceed.

My understanding

+ the inputs are {},a

+ the outputs are o,{}

+the states are p,q,pq,{}

*Initial state = p&q (am I correct coz its given I =p&q&q)

Now what should I do next hoe to proceed please guide me. What should I do with R ?? How do I get the transitions?

Incase you have some materials which I can refer please share with me it will try looking into that and try to solve.

How to we compute the transitions from =R=next(q)&(next(p)|(q->p))&!(o|a)

Answer 1

To compute the state transition diagram of this FSM, we first note that there are the states {},{p},{q},{p,q} which may however not all be reachable. 

The only initial state is {p,q} since this is the only assignment that satisfies I = p&q&q. For the transitions, we start with the initial state and instantiate true for p and q in R so that we obtain the transitions starting in state {p,q} as those assignments that satisfy R[p<-true;q<-true] = next(q)&!(o|a). It is easy to see that R[p<-true;q<-true] = next(q)&!o&!a so that there are the transitions 

•     {p,q} -- !a/!o --> {q} 
•     {p,q} -- !a/!o --> {p,q} 

We proceed now the same way in the new state {q} that has been reached, i.e., we consider R[p<-false;q<-true] = next(q)&next(p)&!(o|a) which is equivalent to next(q)&next(p)&!o&!a. Hence, we have the following transition from state {q}

•     {q} -- !a/!o --> {p,q} 

These are all transitions of the reachable states, since the other two states {},{p} are not reachable. However, you also have to determine their transitions in the same way as shown above to see the entire state transition diagram of the FSM.

You can find the explanations as well as examples in the chapter on Transition systems; section "Kripke Structures vs. FSMs".

You can also use the tool https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html to check your computations for correctness.

Comments

regarding the tool, there is no field for the output variables, where in the questions there is output.
will that make a difference?

---

ohh ok.. now I get it.
Actually for R[p<-true;q<-true] = next(q)&!o&!a
I was considering only     {p,q} -- !a/!o --> {q}
and missed  {p,q} -- !a/!o --> {p,q}  for all the states.

so, for a var x,y
if we have R[x<-1;y<-1] = x'&!a&!o
then we shud consider both x'&!a&!o and also x'&y'!a&!o ? am I correct ?
i.e
{x,y} --!a/!o-->{x}
{x,y} --!a/!o-->{x,y}


so similarly R[x<-1;y<-1] = x'&!o
then will it be x'&!a&!o, x'&y'!a&!o, x'&a&!o and x'&y'a&!o ?
and the transition will be
{x,y} --!a/!o-->{x}
{x,y} --!a/!o-->{x,y}
{x,y} --a/!o-->{x}
{x,y} --a/!o-->{x,y}
have I understood it correct ?

---

Usually, the outputs are defined as functions that map the source state and the input to an output, so that it won't matter.

---

Yes, you have to rule out don't care values, i.e., if a variable like y' would not occur in the formula of the transition relation, you have to consider both the case where it is false and true. However, unlike you stated above, x'&!a&!o is then to be replaced with x'&!y'&!a&!o | x'&y'!a&!o to get all assignments without don't care values. You may also simply consider a truth table.