A Kripke kōan
From Spivey's Corner
A student came to Spivey and said, "Master, is it true that enlightenment, once achieved, is everlasting [ G (p → G p) ], and that enlightenment brings contentment [ G (p → q) ]?"
"What you say is true."
"Then will all attain enlightenment [ F (G p) ]?"
"No, but all will achieve everlasting contentment [ F (G q) ]."
"How can this be?"
"It is the search for enlightenment that brings discontent. Those who never seek it remain content, as do the beasts of the field."
"Then will all reach a condition where their contentment is secure [ AF (AG q) ]?"
"No, for the possibility of seeking enlightenment endlessly burdens the unenlightened with the risk of passing discontent [ EG (EF ¬q) ]."
"I ask again, how can this be?"
"My child, you must study diligently the writings of the master Kripke. For these truths cannot be written in the linear way."
The student left, more puzzled than before.
Analysis
In lecture notes, it is stated that F (G q) is an LTL formula without an equivalent CTL formula, and conversely that the CTL formula AF (AG q) has no equivalent in LTL. The question naturally arises of showing at least that these two formulas are not counterparts of each other.
To do this, consider the following Kripke structure:
Every infinite path from s0 either stays in state s0, 'never seeking enlightenment,' and therefore keeps q true forever, or it eventually reaches state s2, where q remains true. Thus the structure satisfies the LTL formula F (G q).
On the other hand, state s0 does not satisfy the CTL formula AG q, since there is a path 〈s0, s1, s2, s2, ...〉 on which q is momentarily false. Therefore state s0 does not satisfy AF (AG q), for there is a path 〈s0, s0, ...〉 on which AG q is never true.
[I found the counteraxample in a much-cited paper of Clarke and Draghicescu; indeed, most of the examples of mutual inexpressibility that appear online seem to be taken directly from that source.]
Disclaimer
Some people, on reading this page, have come to the conclusion that I rejoice in the obscurity of this corner of logic, and celebrate its inclusion in our first year logic course. Nothing could be further from truth, and in fact I think it is just plain daft in an introductory course to be discussing the relative expressive power of two variants of temporal logic when students hardly have the experience (e.g., of concurrent programming) to identify any properties of computer systems that are aptly expressible as temporal formulas, and there is no discussion in the course of properties of systems that are not expressible in this kind of temporal logic at all.
