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

543 users

+1 vote
Hello,

the question is: why is AG(a ↔ Xa) = A(Ga ∨ G¬a) ?
The equivalence was used in the solution for the exam from 06.09.2016 in Task 7b).

I see that AG(a ↔ Xa) = A (G (¬a ∨ X a) & G (¬X a ∨ a)) but how does that translate to A(Ga ∨ G¬a) ?

Thank you!
in * TF "Emb. Sys. and Rob." by (220 points)

2 Answers

+2 votes
 
Best answer
a <-> Xa = aaaaa or neg(a) neg(a0......

hence I think G(a) V G(neg(a))....
by (870 points)
selected by
Absolutely right. Maybe I should add something about AG(a ↔ Xa).

It requires that all paths satisfy at any point in time that the next state in the path has an a if and only if the current one has one. This means, there cannot be any place where there is a change between ¬a and a or between a and ¬a. Hence, the only two paths satisfying this formula are a^omega and (¬a)^omega. And these are the paths described by Ga ∨ G¬a.
+2 votes
Forget about the A-quantifier, and consider G(a ↔ Xa) and let's find all of its models. Variable a may be initially either true or false. If it is false, then also ¬Xa must hold, since a ↔ Xa must be true at time 0. Same for time 1, and so on and by induction, we see that in that case G¬a holds.

If "a" would be initially true, the same arguments will prove that Ga holds.

Hence, G(a ↔ Xa) implies that we either have Ga or G¬a. Conversely, Ga and also G¬a imply G(a ↔ Xa).
by (166k points)
edited by

Related questions

+1 vote
1 answer
0 votes
1 answer
asked Jan 25 in * TF "Emb. Sys. and Rob." by A (360 points)
0 votes
1 answer
asked Jan 25 in * TF "Emb. Sys. and Rob." by A (360 points)
0 votes
1 answer
0 votes
1 answer
asked Aug 26, 2023 in * TF "Emb. Sys. and Rob." by calvet (250 points)
Imprint | Privacy Policy
...