Exam 2020 Question 6a) [closed]

Question

Can someone please explain the line marked in the image and how to derive it.

Answer 1

It is the standard translation that you find in the chapter on temporal logics.

The abbreviations are

•     q0 = a ∨ X a
•     q1 = b ∨ c ∧ Xq1
•     q2 = q1 ∧ X q2
•     q3 = q2 ∨ X q3

with the fairness constraints

•     GF[q0→a]
•     GF[c→q1]
•     GF[q1→q2]
•     GF[q3→q2]

Comments

Could you maybe tell me on which slide this is explained, because I have a really hard time understanding this? I understand the abbreviations but I don't know how to get to these acceptance conditions from this.

---

You find the rules to apply on slides 71-73, and their proof on the slides 62-70; example translations are given on slides 76-79 of chapter VRS-07-TemporalLogics

---

Fun Fact: There's tool support for that. Enter the LTL formula of your choice to the LTL validity checker and get the automate as a nice by-product https://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html