# mu calculus to CTL model checking

+1 vote
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?

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.
by (25.6k points)
+1 vote

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.

by (166k points)

+1 vote