Translating CTL* to µ-Calculus

Question

Students often wonder how one can translate general CTL* formulas to µ-calculus. Of course, there are algorithms that can do that for us, but we have not discussed them in VRS, since it would lead us to further topics like ω-tree automata and time is limited in a semester. Still, even without doing that in detail, the following may give some hints on how that could work in general, and might be useful for the one or the other case.

The general idea is to unroll temporal operators in a "now" and "next" case (you will find these rules on the slides of the temporal logic chapter), then I will drive in the path quantifiers, and hope that formulas will soon repeat in this unrolling process. From this, we can derive a µ-calculus formula. 

For example, the CTL* property EG[φ∨Xφ] cannot be translated to CTL (this is a proven fact!), but of course, we can express it in µ-calculus. Let's apply the above mentioned procedure and call our formula y:

1. y = EG[φ∨Xφ]
2. = E[(φ∨Xφ) ∧ XG[φ∨Xφ]]
3. = E[φ∧XG[φ∨Xφ] ∨ Xφ∧XG[φ∨Xφ]]
4. = E[φ∧XG[φ∨Xφ] ∨ X(φ∧G[φ∨Xφ])]
5. = φ∧EXEG[φ∨Xφ] ∨ EX(φ∧EG[φ∨Xφ])
6. = φ∧EXy ∨ EX(φ∧y)

So, in step 5, we find our original formula again, and can abbreviate it now by y. Thus, we see that y = φ∧EXy ∨ EX(φ∧y)] holds, and therefore y is a fixpoint of f(y) = φ∧EXy ∨ EX(φ∧y)]. Since y is an "EG", and "EG" is a greatest fixpoint, we therefore derive 

EG[φ∨Xφ] = νy. (φ∧<>y ∨ <>(φ∧y))

Now, can you do the same for the following formulas?

1. E[Fφ∧Gψ]
2. EG[φ∧XXφ]
3. EG[φ∨XXφ]

Warning: I was always hesitating to mention this technique, since applying it will generally make a lot of work. In most cases (we ask in the exam), simpler ways can be found, and I would therefore not recommend the above technique. It is just mentioned now to cure your curiosity. 

Comments

Hi, would you kindly explain how in transition 5, E has propagated to before the second G, making the part after the disjunction EG[/phi or X/phi]. Propagation of E can be done over conjunctions as well? I understand the first propagations but E to me seemed like to be able to propagate over disjunction only. Is my understanding incorrect?

---

Good point!

Yes, in general, E(φ ∧ ψ) and (Eφ) ∧ (Eψ) are not equivalent, so it is fine that you have doubts when you see that. But in the above case, I can do so since (well I should have said this!) φ is a state formula (and not a path formula). For a state formula φ, Eφ just means that the state s satisfying Eφ must have an infinite outgoing path and just on the first state of the path (which is s) φ must hold. This is the same as φ ∧ E1.

Now consider a formula E(φ ∧ ψ) where φ is a state formula, but ψ is a path formula. It holds on a state s iff s has an infinite outgoing path where φ and ψ hold on the path. Since φ is a state formula, it means that φ holds on the first state of the path (that is how the semantics is defined), i.e, that φ holds on s. Hence, if φ is a state formula, then we have E(φ ∧ ψ) = φ ∧ Eψ (the second part Eψ makes sure that there exists an outgoing infinite path).

In the example above, φ is assumed to be a state formula so I can rewrite E(φ∧XG[φ∨Xφ]) to φ∧EXG[φ∨Xφ] and then to φ∧EXEG[φ∨Xφ].

Answer 1

Okay, let's also give an answer to this open question: Translating E[Fφ∧Gψ] to µ-calculus with the mentioned technique can be done as follows for state formulas φ and ψ: 

y  
= E[Fφ∧Gψ]
= E[(φ∨XFφ)∧ψ∧XGψ]
= E[φ∧ψ∧XGψ ∨ ψ∧XFφ∧XGψ]
= φ∧ψ∧EXEGψ ∨ ψ∧EXE[Fφ∧Gψ]
= φ∧EGψ ∨ ψ∧EXE[Fφ∧Gψ]
= φ∧EGψ ∨ ψ∧EXy

Thus, y is a fixpoint of f(y) := φ∧EGψ ∨ ψ∧EXy, and in particular, it is the least fixpoint, i.e., E[Fφ∧Gψ] = µy.(φ∧EGψ ∨ ψ∧EXy). We may write that also in pure µ-calculus: E[Fφ∧Gψ] = µy.(φ∧(nu x.ψ∧<>x) ∨ ψ∧<>y) as well as in CTL E[ψ SU (φ∧EGψ)].

The translation of EG[φ∧XXφ] can be simplified, since G[φ∧XXφ] is equivalent to Gφ, so that EG[φ∧XXφ] = EGφ = nu z.φ∧EXz. Using the above technique will also work for state formulas φ: 

y 
= EG[φ∧XXφ] 
= E(φ∧XXφ∧XG[φ∧XXφ]) 
= E(φ∧XXφ∧XG[φ∧XXφ]) 
= φ∧EXE(Xφ∧G[φ∧XXφ]) 
= φ∧EXz 

It remains to translate E(Xφ∧G[φ∧XXφ]) to µ-calculus:

z
= E(Xφ∧G[φ∧XXφ])
= E(Xφ∧φ∧XXφ∧XG[φ∧XXφ])
= E(φ∧X(φ∧Xφ∧G[φ∧XXφ]))
= φ∧EX(φ∧z))

So, we get z = nu z.φ∧EX(φ∧z), and therefore EG[φ∧XXφ] = φ∧EX(nu z.φ∧EX(φ∧z))).

Finally, consider EG[φ∨XXφ] for state formulas φ:

y 
= EG[φ∨XXφ]
= E[(φ∨XXφ) ∧ XG[φ∨XXφ] ]
= E[φ∧XG[φ∨XXφ] ∨ XXφ∧XG[φ∨XXφ]]
= E[φ∧XG[φ∨XXφ] ∨ X(Xφ∧G[φ∨XXφ])]
= φ∧EXEG[φ∨XXφ] ∨ EX(Xφ∧G[φ∨XXφ])
= φ∧EXy ∨ EXz

and the translation of z = E(Xφ∧G[φ∨XXφ]) is done as follows:

z
= E(Xφ∧G[φ∨XXφ])
= E(Xφ∧(φ∨XXφ)∧XG[φ∨XXφ])
= E(Xφ∧φ∧XG[φ∨XXφ] ∨ Xφ∧XXφ∧XG[φ∨XXφ])
= E(φ∧X(φ∧G[φ∨XXφ]) ∨ X(φ∧Xφ∧G[φ∨XXφ]))
= φ∧EX(φ∧EG[φ∨XXφ]) ∨ EX(φ∧z))
= φ∧EX(φ∧y) ∨ EX(φ∧z))

So that we conclude that EG[φ∨XXφ] = nu y. φ∧EXy ∨ EX(nu z. φ∧EX(φ∧y) ∨ EX(φ∧z))).

As said, this is a general translation technique, which usually makes  a bigger effort than having a closer look at the formulas. Usually, formulas can be rewritten at first (like in the second example above) which can simplify the translation a lot. Think twice before going too deep in one direction.