mu calculus to CTL model checking

Question

Que from Oct 2015 Prob 5 S3

IS this equal to nu.y  diamond(AF(y&b) ? And what is AF(y&b)?. AF(b) = all infinite paths of state should visit one of the state where b holds.But what does AF(yb) says?

Please help. Thanks

Answer 1

S3 is: νy. backward diamond (μx.(y∧b ∨ box x))

 The question whether they are equal is hard to answer. In general, there are no CTL operators within µ-calculus formulas. Besides that, the semantics are a bit different as CTL talks about infinite paths and the given µ-calculus formula is also happy with finite paths.

However, the idea is right. The inner formula means something like: There are only finitely many steps to a state satisfying y&b.

So what does y&b mean? It holds on all states that satisfy both y and b. The elementary formula b clearly represents all the states containing the label b. About y, it is a bit different. This is a variable over which we compute a fixpoint. So the outer ν computes the greatest fixpoint y so that y is equal to the result of backward_ diamond(innerformula) where the y in the innerformula is the same as the outer result.

Answer 2

Well, considering CTL operators as abbreviations of µ-calculus formulas, I would first agree with saying νy.<:>(μx.(y∧b∨[]x)) and νy.<:>AF(y∧b) are the same. Also, it is clear that AFφ are the states where either all infinite paths finally reach φ-states (or where there are no outgoing paths at all).

But your main question is which states satisfy νy.<:>AF(y∧b) in general, i.e., not just on the structure shown in the exam. Such questions are hard to answer in general. Clearly, all well-formed formulas in µ-calculus have a meaning in the sense that there is in every transition system a corresponding set of states. But to describe those sets of states with a property that is meaningful for humans is not always simple. There are soo many µ-calculus formulas that you will soon have no intuition anymore on what they might want to tell you. 

Still, let's have a little closer look on the formula that bothers you. For any transition system, its fixpoint iteration will start as follows:

1. y[0] := S
2. y[1] := [|<:>AF(y[0]∧b)|] = [|<:>AF(b)|]
3. y[2] := [|<:>AF(y[1]∧b)|] = [|<:>AF((<:>AF(b))∧b)|]

So, we should understand which states satisfy <:>AFφ in general since we compute the fixpoint of the function f(y) := [|<:>AF(y∧b)|] . By the semantics, those states s must have a predecessor state s1 which satisfies AFφ (see the figure below):

Now what are finally the states νy.<:>AF(y∧b) ? These belong to the set of states y where the above figure applies infinitely often, i.e., 

1. those states that have a predessor state that satisfies AF(y∧b) and when you ask what y is inside this AF(y∧b), the answer is 
2. those states that have a predessor state that satisfies AF(y∧b) and when you ask what y is inside this AF(y∧b), the answer is ...

So, the English sentences 1 and 2 read in a loop are the answer to your question, even though I doubt that is one that is a satisfying one. We could research more on this miraculous set of states, and I guess that we will find out that all there infinite paths will infinitely often visit b-states which comes very close to the more satisfying answer you want to hear, I guess. 

But as Martin wrote, these questions have in general no simple answer in human languages.