# Convert to LTL (Exam 2019.08.27)

In exercise 8 of exam 2019.08.27, we have to convert "A([¬aU0]∧F[aUb])" to LTL.

Why is "A([¬aU0]∧F[aUb])" not already a LTL formula? edited
The formula is syntactically in CTL* and in LTL.
Students who realized that and wrote that the formula itself is already an equivalent formula in LTL got full points.
The solution is there to show a possible but not required way to simplify the formula (third step). The fourth step (conversion to CTL) is purely educative and not required in a real submission.

+1 vote

You are right, that does not make sense. It is already a LTL formula, and the exercise should be to convert it to CTL. It has been fixed now.
by (162k points)
selected by
The formula is syntactically in CTL* and in LTL.
Students who realized that and wrote that the formula itself is already an equivalent formula in LTL got full points.
The solution is there to show a possible but not required way to simplify the formula (third step). The fourth step (conversion to CTL) is purely educative and not required in a real submission.