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

Please check my expanded solution:

({p,q,r,s}, q|p|r|s, 
[q <-> (a&!b) | Xq &
p<->b | Xp &
r<-> c & Xr &
s<->a| Xs],
GF[q->(a&!b)] & GF[p] &GF[c->r]&GF[s->a])

I guessed: FG !b = G[p<->b | Xp], GF[p]

Is this correct?
 

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

1 Answer

0 votes
 
Best answer

I don't think that it is correct, even if you follow the example solution that explains that the given formula is equivalent to F(a∧¬b) ∨ FG¬b ∨ (Gc) ∧ (Fa), you should get another automaton. When I decompile your solution, I see

    q <-> (a&!b) | Xq   --> F(a&!b)
    p <-> b | Xp        --> F(b)
    r <-> c & Xr        --> G(c)
    s <-> a | Xs        --> F(a)

However, instead of F(b), there should be FGb which is not the same. Why do you believe that it is the same?

by (166k points)
selected by
I see. My interpretation of FG!b ended up the same as Fb.
Because I changed FG!b --> !GFb and then came up with the above automaton.

Would FG!b = p <-> !b & Xp be correct instead?
Or
Can I convert G!b first and then F() and take a conjunction after?
Yes, you need to first convert G!b and then F(..) so that two state variables are used. You cannot do that with just one.

Related questions

0 votes
1 answer
asked Jan 13, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Jan 18, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
Imprint | Privacy Policy
...