Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

529 users

0 votes

Vin={a}Vout={o}Vstate={p,q}
I=q<->p, 
R=next(q)&!(q->a)&(next(p)|o|p)

How can I convert this to the FSM diagram and then to Kripke structure?

in * TF "Emb. Sys. and Rob." by (160 points)
I guess, this question is related to the Verification of Reactive Systems lecture. If so, would you please add the tag "vrs"?

1 Answer

+1 vote

The FSM may have four states {},{p},{q},{p,q} where {},{p,q} are the initial states. The transitions are the satisfying assignments of the transition relation R. Thus, we need to determine those. Looking at R, we can clearly see that next(q) must be true, and !(q->a) means q&!a so that q,a, and next(q) are already determined. Hence, there are no outgoing transitions from {} and neither from {p}. So, consider the remaining states {q},{p,q} which have the following transitions:

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

The FSM looks therefore as follows:

The Kripke structure has states that correspond with the above transitions. To list them, we first have to expand the don't care values of the output for the FSM:

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

The above are still the transitions of the FSM, just written without don't care values for the output. 

This leads to the following transitions of the Kripke structure where IO can be an arbitrary assignment to the input/output variables a and o (hence the seven transitions listed below lead to 28 transitions of the Kripke structure):

  •     {q} ----> {p,q}∪IO
  •   {q,o} ----> {p,q}∪IO
  •   {q,o} ----> {q}∪IO
  •   {p,q} ----> {q}∪IO
  • {p,q,o} ----> {q}∪IO
  •   {p,q} ----> {p,q}∪IO
  • {p,q,o} ----> {p,q}∪IO

by (166k points)
Thanks for the answer sir.
how did you come up with these lines in the beginning of the solution?
  {q} --!a --> {p,q}
  {q} --!a& o --> {q}
{p,q} --!a --> {q}
{p,q} --!a --> {p,q}
These are the state transitions of the FSM that you can find by enumerating all satisfying assignments of the transition relation R=next(q)&!(q->a)&(next(p)|o|p).
Yes, I am also not able to find out how you came up with these?
{q} --!a --> {p,q}
  {q} --!a& o --> {q}
{p,q} --!a --> {q}
{p,q} --!a --> {p,q}

It would be really helpful if you can please explain.

Also in this post, we solved transition relation by directly considering separately the & clause in relation, while in another post (its heading is 'Propositional formula to FSM to Kripke --->   https://q2a.cs.uni-kl.de/45/propositional-formula-to-fsm-to-kripke   ') we considered the solution by putting
1) p=0,q=0
2) p=0, q=1
3) p=1, q=0
4) p=1, q=1

Why we are using different methods to solve it? Is there any one generic method to get FSM from transition relation?
Well, in general, the transitions are the satisfying assignments of the translation relation. The simplest way would therefore by a truth table, but in many cases that is already too big to be calculated in reasonable time.

Thus, you can use any other method for computing the satisfying assignments, like computing a DNF or a BDD to enumerate the paths to the 1-leaf. Via BDDs, I computed the following

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

and this must be completed to all variables using q = !p&q | p&q etc.
    
        !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)
what order of variables should be considered? Since BDD is different for different order of variables. (next(q)<=next(p)<=o<=a<=q<=p)? or any order can be considered?
Any order can be considered. We need to expand the path to all variables anyway so good orderings are not of a big help here.
Thank you so much. Now I am able to solve with both DNF and BDD. Your explanation helped a lot.

Related questions

0 votes
1 answer
+1 vote
1 answer
asked Aug 18, 2018 in * TF "Emb. Sys. and Rob." by a_ (350 points)
0 votes
1 answer
Imprint | Privacy Policy
...