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

925 questions

1k answers

1.4k comments

441 users

0 votes

Hi,  I was going through the Zielonka algorithm. I read the formula for finding Attr(Qh), which is "attrA(ϕ):⇔ µx.(ϕ ∨ <A>x)". What should be the <A> x, whether it's all states of player 1? Could you please help me solve this issue? [ How to find Attr(Qh)?] 

in # Study-Organisation (Master) by (1.1k points)

1 Answer

+1 vote
 
Best answer

The enforcement operator <A>phi is defined on page 63 and again on page 138. The definition is as follows: 

    ⟨A⟩φ := A ∧ <>φ ∨ B ∧ []φ = (A=><>φ|[]φ)

It holds on the states where player A can enforce that the next transition will reach a state where φ holds: Each state is either controlled by player A or player B, and if a state is controlled by player A, then it is sufficient to have a successor state where φ holds, since player A can choose that one. If the state is controlled by player B, we have to demand that []φ holds so that player B can only choose φ-states.

For computing the attractor attrA(p) := µx.(p ∨ <A>x) we relabel the state transition system such that the states controlled by player A and B are labeled with variables "a" and "b", respectively, and state s7 (the one with highest rank) is labeled with variable p. 

The computation of the attractor is then the computation of mu x. (p | a & <> x | b & [] x) which is done as follows: 

   〖p〗= {s7}
   〖a〗= {s3;s4;s5;s6}
   〖b〗= {s0;s1;s2;s7}
    step 0 : x = {}
        〖x〗= {}
        〖<> x〗 = {}
        〖a & <> x〗 = {}
        〖p | a & <> x〗 = {s7}
        〖x〗= {}
        〖[] x〗 = {}
        〖b & [] x〗 = {}
        〖p | a & <> x | b & [] x〗 = {s7}
    step 1 : x = {s7}
        〖x〗= {s7}
        〖<> x〗 = {s5;s6}
        〖a & <> x〗 = {s5;s6}
        〖p | a & <> x〗 = {s5;s6;s7}
        〖x〗= {s7}
        〖[] x〗 = {s5}
        〖b & [] x〗 = {}
        〖p | a & <> x | b & [] x〗 = {s5;s6;s7}
    step 2 : x = {s5;s6;s7}
        〖x〗= {s5;s6;s7}
        〖<> x〗 = {s1;s2;s5;s6;s7}
        〖a & <> x〗 = {s5;s6}
        〖p | a & <> x〗 = {s5;s6;s7}
        〖x〗= {s5;s6;s7}
        〖[] x〗 = {s5}
        〖b & [] x〗 = {}
        〖p | a & <> x | b & [] x〗 = {s5;s6;s7}
        〖x〗= {s5;s6;s7}
  fixpoint reached!
  〖mu x. (p | a & <> x | b & [] x)〗 = {s5;s6;s7}

The computation starts with p-states and adds the existential A-predecessors and the universal B-predecessors until a fixpoint is reached.

by (143k points)
selected by
Thank you, professor.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...