If P requests access to r, eventually it will get the access. Let first use 
these abbreviations:

   rq : a state predicate which is true when P is requesting r
   u  : a state predicate which is true when P is accessing r

The solution proposed this LTL to express the above property:

(1)   [](~rq /\ ~u  W  rq)
   
The motivation was explained during the lecture. 

Now let's try to a different proposal. The requirement seems equivalent to
requiring any execution that **eventually** satisfyies this should not 
be accepted:

   ~rq UNTIL  ~rq /\ u
   
So, all executions must satisfy:
   
(2)   ~<>(~rq UNTIL  ~rq /\ u)
   
Let's do some calculation on (2):
  
      ~<>(~rq  UNTIL  ~rq /\ u)
    =
	  []~(~rq  UNTIL  ~rq /\ u) 
	  
	= // recall ~(a U b) = ~b W (~a /\ ~b) 
	
      [](~(~rq /\ u) WEAKUNTIL rq /\ ~(~rq /\ u))
	=
      [](rq \/ ~u WEAKUNTIL rq /\ (rq \/ ~u))
	  
    =  // a /\ (a\/b) = a
	
(3)   [](rq \/ ~u WEAKUNTIL rq)

Additionally, you can prove the following

    R1: any execution satisfies a W ~a
	
    R2: any execution satisfing a1 W b  and  a2 W b also satisfies (a1 /\ a2) W b

Using R1, we infer:

(4a)  [](~rq WEAKUNTIL rq)

Applying R2 on 3 and 4a gives:

(4b) 	[](~rq /\ (rq \/ ~u) WEAKUNTIL rq)

Which is equivalent to:

(5) 	[](~rq /\ ~u  WEAKUNTIL rq)

But this is just (1). Conclusion: (2) implies (1).

We can also prove the following:

    R3: any execution satisfying a1 W b  also satisfies a2 W b, if a2 is weaker than a1. 
	   (BUT the other way around is not always true!)
	  
It follows then, that (1) implies (3), which is equivalent to (2).