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

546 users

0 votes

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

closed with the note: well answered
in * TF "Emb. Sys. and Rob." by (800 points)
closed by

1 Answer

+1 vote
 
Best answer

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]

by (166k points)
selected by
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

Related questions

0 votes
1 answer
asked Jan 18, 2021 in * TF "Emb. Sys. and Rob." by MS (1.1k points)
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...