I'm studying CTL and I got stuck on the following problem:
Determine if the following operations are idempotent or not: AG, AF, EG or EF.
I have the following definitions: Let M = (S,→,L) be a model for CTL, s in S, φ a CTL formula. The relation M, s |– φ is defined by structural induction on φ:
- M,s |– AG φ holds iff for all paths s1 →s2 →s3 →...,where s1 equals s,and all si along the path, we have M, si |– φ. Mnemonically: for All computation paths beginning in s the property φ holds Globally. Note that ‘along the path’ includes the path’s initial state s.
- M,s |– AF φ holds iff for all paths s1 → s2 → ..., where s1 equals s, there is some si such that M, si |– φ. Mnemonically: for All computation paths beginning in s there will be some Future state where φ holds.
- M,s |– EG φ holds iff there is a path s1 →s2 →s3 →..., where s1 equals s, and for all si along the path, we have M, si |– φ. Mnemonically: there Exists a path beginning in s such that φ holds Globally along the path.
- M,s |– EF φ holds iff there is a path s1 →s2 →s3 →..., where s1 equals s, and for some si along the path, we have M, si |– φ. Mnemonically: there Exists a computation path beginning in s such that φ holds in some Future state.
When I just think about idempotency of the different operations, I feel like all of them are idempotent. E.g. If AG x holds, then AG( AG x) should also hold. Because if we know that M,s |– AG x holds, then x ∈ L(si) for all states i. Then AG( AG x) should obviously also hold.
But how am I supposed to determine/argue more rigorously that eg. AF is idempotent or not? Am I supposed to test them against some kind of generalised model? Figure out a countermodel?
Could someone explain how I should go about this? I feel lost.
Thanks!
This is how I would go about solving it for the $\mathrm{AG}$ operator (and for the other operators I would proceed similarly).
Direction $\mathrm{AG} \Rightarrow \mathrm{AG}\,\mathrm{AG}$:
Suppose that $\mathcal{M},s_0\vdash\mathrm{AG}\,\phi~$ (for ease, I have renamed the initial state from $s$ to $s_0$). By definition, this means that for every path $s_0\to s_1\to \cdots \to s_n$, it holds that $\mathcal{M},s_i\vdash\phi$, where $i\in\{0,\ldots,n\}$.
Now, we need to show that $\mathcal{M},s_0\vdash\mathrm{AG}\,(\mathrm{AG}\,\phi)$, which means that we need to show that for every path $s_0\to s_1\to \cdots \to s_n$, it holds that $\mathcal{M},s_i\vdash\mathrm{AG}\,\phi$. Again, following the definition, the latter means that for every path $s_i\to\cdots\to s_n$, we need to show that $\mathcal{M},s_j\vdash\phi$, where $i\in\{i,\ldots,n\}$. But, $s_i\to\cdots\to s_n$ is a subpath of $s_0\to \cdots \to s_n$. So, since by assumption $\mathcal{M},s_k\vdash\phi$ holds for any $k\in\{0,\ldots,n\}$, it also holds for any $k\in\{i,\ldots,n\}$. Thus, we have $\mathcal{M},s_0\vdash\mathrm{AG}\,(\mathrm{AG}\,\phi)$.
Direction $\mathrm{AG}\,\mathrm{AG} \Rightarrow \mathrm{AG}$:
Suppose that $\mathcal{M},s_0\vdash\mathrm{AG}\,(\mathrm{AG}\,\phi)$. By definition, for every path $s_0\to s_1\to \cdots \to s_n$, it holds that $\mathcal{M},s_i\vdash\mathrm{AG}\,\phi$, where $i\in\{0,\ldots,n\}$. Since the latter holds for every state on that path, it also holds for the state initial $s_0$. Thus, by setting $i=0$, we get the desideratum, $\mathcal{M},s_0\vdash\mathrm{AG}\,\phi$.