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

769 questions

886 answers

1.3k comments

424 users

0 votes

For above FSM constructed kripke structure and compute R',but my solution is incorrect.

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

1 Answer

0 votes

For the following FSM

    state var: p,q
    inp. var: a
    init q
    trans a&p&!q&next(p)&next(q) | a&q&!p&next(p)&next(q) | a&q&!next(p)&next(q) 

which looks as follows

we find this associated Kripke structure:

There are deadend states and unreachable states that we would like to remove from the set of transitions. The deadend states s0,s1,s2,s4,s6 are described by 

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

and the unreachable states s0,s1,s4,s5 by

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

so that our updated transition relation should be

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

and we also remove the deadends from the initial states

    I' := I & !(!p&!q&!a | !p&!q&a | !p&q&!a | p&!q&!a | p&q&!a)

which is the following structure

So, your result is missing a transition. 

by (117k points)
edited by
thanks updated.how to write for below question this part is confusing because  my solution is incorrect :
c) R1 is obtained by removing the transitions to deadends in R′. Construct a propositional logic formula for R1.Submit your solution in the form:a&p&q&next(p)&!next(q) | a&!p&!q&next(p)&next(q)

my solution:
after removing dead ends:
p&a&!q&next(p)&next(q)&next(a)| p&a&q&next(q)&!next(p)&!next(a) | q&a&!p&next(q)&!next(p)&next(a) |!p&a&q&next(q)&next(p)&next(a)

after removing unreachable nodes:
p&a&q&next(q)&!next(p)&!next(a) | q&a&!p&next(q)&!next(p)&next(a) |!p&a&q&next(q)&next(p)&next(a)
your solution after removing dead ends still contains s2:{q} which is a dead end
Imprint | Privacy Policy
...