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


543 users

+1 vote
The ques is from Sept 2016 prob 4 S2.

S = nu.y. diamond(y) & (mu.x (avb) V box(x))

Here i replace mu.x to AF(avb). And i have avb = {s1,s3,s6,s8} // s3 and s8 holds for all the formula.

And i have to check for all the infinite paths of the state, the path must visit  these states.

So i have AF(avb)  = {s4,s6,s5,s7,s3,s8} //s7 holds as it visits s1 initially, s3 and s8 holds for all the formulas.

Is my understanding right?

since Y is not dependent on x diamond(y) is same. And i compute    AF(avb) &diamond(y).

Is this the final states where i should check for all the initial states to satisfy the property?

Please help
in * TF "Emb. Sys. and Rob." by (870 points)

1 Answer

+1 vote

Yes, your thoughts are correct. But I think AF(avb) (or equivalently µx.(avbv[]x)) holds on states {s1;s3;s4;s6;s7;s8}. Anyway, after having computed these states, you can proceed with the outer fixpoint that does not mutually depend on the inner one.

The transition system is the following one:

and the computation goes like this:

  computing states of A F (a | b)

  i.e., computing states of mu Z. (a | b | [] Z)

  • 〖a〗= {s1;s8}
  • 〖b〗= {s1;s6}
  • 〖a | b〗 = {s1;s6;s8}

    step 0 : Z = {}

  • 〖Z〗= {}
  • 〖[] Z〗 = {s3;s8}
  • 〖a | b | [] Z〗 = {s1;s3;s6;s8}

    step 1 : Z = {s1;s3;s6;s8}

  • 〖Z〗= {s1;s3;s6;s8}
  • 〖[] Z〗 = {s3;s4;s7;s8}
  • 〖a | b | [] Z〗 = {s1;s3;s4;s6;s7;s8}

    step 2 : Z = {s1;s3;s4;s6;s7;s8}

  • 〖Z〗= {s1;s3;s4;s6;s7;s8}
  • 〖[] Z〗 = {s3;s4;s7;s8}
  • 〖a | b | [] Z〗 = {s1;s3;s4;s6;s7;s8}

    fixpoint reached!〖mu Z. (a | b | [] Z)〗 = {s1;s3;s4;s6;s7;s8}

by (166k points)
edited by
But why not s5? s5 has one outgoing infinite path that visits s6.
It also has an outgoing path that does never visit a state in a|b: Look at the path s5;(s2;s0)^omega. Note that we are checking AF and not EF.
Got it.Thank you

Related questions

+1 vote
2 answers
0 votes
1 answer
asked Aug 24, 2020 in * TF "Emb. Sys. and Rob." by nimteaj (770 points)
0 votes
1 answer
Imprint | Privacy Policy