0 votes

In Problem 7a) for translating LTL formula to an equivalent automaton formula, F[a B b] | [a U (Fc)], why does the solution not have 2 more acceptance conditions ?

GF[q0 | b] & GF[a --> q3]


Could someone please explain me the reason. 

in * TF "Emb. Sys. and Rob." by (130 points)

1 Answer

+1 vote

To translate F[a WB b] ∨ [a WU (F c)] to an equivalent omega-automaton, we will abbreviate 

  • q0 := [a WB b]
  • q1 := F q0
  • q2 := F c
  • q3 :=  [a WU q2]

Next, we replace these definitions by transition relations and fairness constraints. For each state variable, we would get one fairness constraint:

  • q0 yields GF[q0∨b]
  • q1 yields GF[q1->q0])
  • q2 yields GF[q2->c])
  • q3 yields GF[a->q3]

In the example solution, you find the fairness constraints for q1 and q2, but you miss the other two. You may safely add one or both of them if you want, the solution will be correct with them also. However, since they stem from weak operators with positive occurrences, you may omit them also if you want. See the slides of the related chapter that mentions this optimization after the unoptimized procedure has been explained. 

by (93k points)
edited by
Thank you for the explanation

Related questions

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