Closure properties for CTL*, CTL or LTL?

Question

Hi, as the title suggests are there any useful closure properties apart from the trivial ones for CTL*, CTL or LTL?

Answer 1

What do you mean with closure properties? These sets of formulas are all closed under boolean operations. LTL is complete with respect to the first order theory of linear orders, i.e., LTL = LO1; and that is also known as the non-counting fragment of the omega-automata. So, for LTL, there are a lot of equivalent formulations know. CTL is a bit ad hoc defined and does not have such strong equivalences, but CTL* inherits those from LTL for branching time, i.e., tree automata and second order monadic logic with many successors.

Comments

Maybe closure property was not the right word.I was thinking about  theorems of the kind like LeftCTL* can always be translated to CTL. If there exist similiar  things for CTL* and LTL or CTL and LTL.

---

There is this exercise on the past exams, where you should show that formulas can be rewritten in CTL or LTL and show why. The solutions all did translations of the formulas, but I was thinking maybe we could just say, the following formula is in LeftCTL* and by lecture can be translated to ctl?

---

Every LeftCTL* formula can be translated to CTL for sure and the size of the generated CTL formula may be exponential in the size of the given LeftCTL* formula. However, there are also CTL* formulas that are (syntactically) not LeftCTL* formulas but can still be translated to CTL (simply imagine (EGFa | !EGFa)). For CTL*, LTL, and CTL we can rather say that all of these logics are different.

---

If you can see that a formula belongs to LeftCTL* it is for sure that you can rewrite it to CTL, but I guess that the exercise wants that you also do that translation.