O'Reilly logo

An Introduction to Practical Formal Methods using Temporal Logic by Michael Fisher

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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

images/c02_I0001.gif

is either true or false. Such propositions are then combined using constructs (or connectives) such as ‘’, ‘’, and ‘⇒’ ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required