0 votes

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?

in * TF "Emb. Sys. and Rob." by (440 points)
edited 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.

1 Answer

+1 vote
 
Best answer
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 (91.8k 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.

Related questions

0 votes
1 answer
asked Feb 6 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
0 votes
1 answer
0 votes
2 answers
0 votes
1 answer
asked Aug 5, 2020 in * TF "Emb. Sys. and Rob." by ssripa (550 points)
Imprint | Privacy Policy
...