A Kripke kōan

From Spivey's Corner
Jump to: navigation, search

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.


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.]