LTL and CTL conversion

Question

In this problem, what is the correct way to solve this?. i mean same formula can have multiple form. right?. so, how can we decide we are in the end of the translation?. for eg. some formula can have both CTL and LTL form but once we reach the CTL form we might stop there. can you please give me any tricks/tips to solve this?

Answer 1

There are certain features of the formula that will tell you that the formula cannot be transformed to one of the logics. For example, if you can't get rid of an existential quantification, it is likely not to have an equivalent formula in LTL. Also, if it strictly relies on branching behavior, it is probably in CTL but not LTL. Similarly, if the formula looks at one isolated path, it might be difficult up to impossible to convert it to CTL.

There is no easy recipe how to tell whether the formula can be expressed in LTL/CTL. I typically simplify the formula a lot until I understand what it is doing. It doesn't harm to simplify a CTL/LTL formula further. Sometimes that gives the glue whether it is in another logic class.

Comments

can you please explain the steps 2 and 4 in this problem

---

In step 2, we just apply duality. (¬E something = A¬something and so on)
Step 4 is just the consequence of having SB encapsulated in G. If we want [a SB b] to hold in every step, we know that b can never occur. If b occurred, then in this step [a SB b] wouldn't be satisfied, thus G would be violated. That's why we add ¬b to the G. If we know that in this case [a SB b] may only be satisfied without satisfying b, then we can simplify it further. Since the before is a strong one, we need a after finite time. Hence, our [a SB b] boils down to F a. (Never forget the the context! Our [a SB b] is inside a G. That makes it stricter than a [a SB b] would normally be!