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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

After generating the the kripke structure from the FSM shown above, i try to compute R' from the deadends in the kripke structure.

The deadends i got were !p&!q&!a | !p&!q&a | !p&q&a | p&!q&a | p&!q&a. Since 2 deadends satisfy our inital  condition i got R' as R & next(a).

I generated the kripke structure with the following new transition and i got the following.

After removing the deadends and computing the transitions, i get the following: 

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

But it is flagged as wrong, can you please tell me why ?

in * TF "Emb. Sys. and Rob." by (790 points)

1 Answer

+1 vote

You have an FSM with state variables p,q and input variable a and initial states p&q|!p&!q and the following transition relation

    R = p&    q&!next(q)&next(p)
      | p&!a&!q&!next(q)&next(p)
      | q&!a&!p&!next(q)&next(p)

Remark: It would be nice of you if you would type that in instead of making a screen shot where we have to type in the formulas. 

The FSM corresponds with the following Kripke structure:

The deadend states are computed as pre∀(false) which is !q&a|!p&a|!p&!q which can be written in full DNF as

   !p&!q&!a | !p&!q&a | !p&q&a | p&!q&a

Hence, we have four deadend states that you can also directly see in the above figure. You also have written a fifth one p&!q&a which is however the same as the fourth. 

Moreover, there is an unreachable state s2:{q} that we also have to eliminate. Thus, we replace the above transition relation with

    I1 = (p&q|!p&!q) & !(!p&!q&!a | !p&!q&a | !p&q&a | p&!q&a)
    R1 = R & !(!p&q&!a) & !(!next(q)&next(a)|!next(p)&next(a)|!next(p)&!next(q))

which is equivalent to

    I1 = p&q&a | p&q&!a

    R1 = p&!q&!a&next(p)&!next(q)&!next(a) 
       | p& q& a&next(p)&!next(q)&!next(a) 
       | p& q&!a&next(p)&!next(q)&!next(a)

This structure looks now as follows:

Your transition relation !a&p&q&next(p)&!next(q) | a&p&q&next(p)&!next(q) | !a&p&!q&next(p)&!next(q) produces however the following transitions, and you can now see where you go wrong:

by (170k points)
Imprint | Privacy Policy
...