Today I gave the last lecture of my course “Logic and Model Checking”. In the past few weeks we have revised Computational Tree Logic (CTL) and I spent a bit of time explaining the difference between the semantics of the CTL operators AF and EF. The first one expresses the universal “eventually”: if you write AF p, this means that “for All paths”, “at some point in the Future”, the proposition p will be true. EF p, instead, means that “there Exists a path” such that “at some point in the Future”, the proposition p will be true.

The standard example I use the explain the difference is to set p equal to the proposition “find a mushroom”. So, “AF p” means: it doesn’t matter which path you take, just be patient and you will eventually find a mushroom. “EF p”, instead, means: there exists a path such that, if you follow that path, you will eventually find a mushroom. I then go on explaining that my only way of finding an edible mushroom is to be in a wood where AF p is true, because in “EF p” woods I will never find a mushroom (I am really unlucky at mushroom hunting).

I guess the students liked the analogy, this is what I got today at the end of the class:

It is now my turn to revise an old recipe I used to prepare: Portobello mushrooms with goat cheese.