# compute R' from the following FSM

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

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 (162k 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:
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)