Chapter 2
Temporal Logic
Time flies like an arrow. Fruit flies like a banana.
—Groucho Marx
In this Chapter, we will:
- provide the basic intuition behind temporal logics (Section 2.1);
- define the syntax of a simple propositional temporal logic (Section 2.2);
- examine the formal semantics of this temporal logic (Section 2.3);
- explore some classes of temporal logic formulae that are useful in reactive system specification (Section 2.4);
- revisit the question ‘what is temporal logic’ (Section 2.5);
- introduce a normal form for our temporal logic that will be useful in Chapters 4 and 6 (Section 2.6);
- discuss the link between propositional temporal logic and finite state automata, something that will be essential in Chapter 5 (Section 2.7);
- provide pointers to some more advanced work in this area (Section 2.8); and
- give a final selection of exercises (Section 2.9), the solutions to which can be found in Appendix B.
To begin with we will only describe a simple propositional, discrete, temporal logic. However, much of the temporal framework we develop below is applicable to other variants of temporal logic we will see later.
2.1 Intuition
In classical propositional logic1, formulae are evaluated within a single fixed world (or state). For example, a proposition such as
is either true or false. Such propositions are then combined using constructs (or connectives) such as ‘’, ‘’, and ‘⇒’ ...
