Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

529 users

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 (166k 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, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Jan 27, 2021 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
0 votes
1 answer
asked Jan 13, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
Imprint | Privacy Policy
...