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

For above problem trying solve b ^ vx. diamond(x), below is my solution , i didnt understand  how it is {S0,s4}

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

1 Answer

0 votes
It is b ∧ nu x. <>x, not b^… (^ is xor, ∧ is and).

I'm not sure whether I understand your notes correctly but you already wrote y = {s0, s4}.  First, we do nu y. <>y. y0 = all states, y1=all states except s7 because it as no successor hence, also none to y0, y2=y1. Now, we intersect it with the states satisfying b (s0, s4, s7). As we already kicked out s7, only s0, s4 are left.

To solve the outer mu, we just iteratively add predecessors that satisfy a. The iteration likes likes: s0,s4, then s0, s4, s5, then s0, s4, s5, then s0, s4, s5, s1, then s0, s4, s5, s1, s2, then fixpoint.
by (25.6k points)
Okay thank you so much. So, for inner bracket (b ∧ nu x. <>x), is it not required to reach the fix point?. And , what should be the order to consider while solving this problem. First, I need to solve for (nu x) and then (nu x . <>x) and then (b ∧ nu x. <>x).
The inner fixpoint is nu x. <>x. We do reach it. It is all states except for s2. We then compute b ∧ nu x. <>x by intersecting b and the fixpoints. We got {s0, s4}.

I don't understand the following problem.

Related questions

0 votes
1 answer
0 votes
1 answer
asked Aug 14, 2020 in * TF "Emb. Sys. and Rob." by maherin (370 points)
0 votes
1 answer
asked Aug 7, 2020 in * TF "Emb. Sys. and Rob." by ssripa (550 points)
0 votes
1 answer
asked Jun 25, 2020 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
Imprint | Privacy Policy
...