ABSTRACT
In this chapter, we introduce temporal logic (TL), a logical formalism for reasoning about domains in which the truth or falsity of statements can vary over time. These statements could include formulae representing states of a dynamical system, which brings TL clearly within the scope of this handbook. Since TL is an extension of propositional logic, we believe that the reader will best be in a position to appreciate the former if we first provide a brief introduction to the latter; readers already familiar with propositional logic can skip directly to Section 20.2.
