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


538 users

0 votes

Prove the LTL formula (FFGa↔ (FGato be valid by applying these steps: Translate the negation of the formula to a symbolic ω-automaton. 

In the solution's acceptance condition there are three GF's conjuncted. First one is GF[a -> q0], this one is clearly Ga's omega translation. The next GF[q1 -> q0] and GF[q2 -> q1] are Fa's translation.

My question is why did we only considered the first part FFGa although the problem asks to translate the negation of whole formula? (after negation of <-> it becomes xor)


Professor answered on

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

1 Answer

+1 vote
Best answer

When we make the abbreviations, we first get

  1. q0 := Ga with the rest (FFq0) ↔ (Fq0) 
  2. q1 := F q0 with the rest (Fq1) ↔ q1 
  3. q2 := F q1 with the rest q2 ↔ q1 
So, the answer is that the abbreviations take care of all occurrences of the sub formulas. 
by (166k points)
selected by

Related questions

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