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

I have doubt in LTL model checking questions of 31.08.2021 exam problem 6 . I am getting 3 GF equations while solving but in solution 2 GF equations are given how to solve these GF equations and in some solution only true is written , can you explain ?

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

1 Answer

+1 vote
We have to translate the negation of the formula to an omega-automaton. For the negation, all three occurrences of the temporal operators are negative. Negative occurrences of strong operators don't need a constraints, so we only need two constraints for the weak operators, in your case for q0 and q2. You should therefore have the constraints GF(!a->q0) and GF(q1->q2) and the third constraints GF(!q1->a) can be omitted. The reason for this is explained on slide 94 of VRS-07-TemporalLogic.
by (166k points)

Related questions

Imprint | Privacy Policy