Chapter 1
Introduction
Time is an illusion, lunchtime doubly so.
—Douglas Adams
Time plays a central role in our lives. In describing the world, or our activities within it, we naturally invoke temporal descriptions. Some of these are explicit, such as ‘next week’ or ‘in 5 minutes’, while others implicitly acknowledge the passing of time, for example ‘during’, ‘did’ or ‘will do’. Not surprisingly, it is also important to be able to describe temporal aspects within the world of Computer Science: computations naturally proceed through time, and so have a history of activity; computational processes take time to act; some processes must finish before others can start; and so on. Consequently, being able to understand, and reason about, temporal concepts is central to Computer Science.
In this book, we will explain how some of these temporal notions can be described and manipulated. This, in turn, will allow us to carry out a temporal analysis of certain aspects of computation. To be precise in our temporal descriptions, we will use formal logic. These not only provide a concise and unambiguous basis for our descriptions, but are supported by many well-developed tools, techniques and results that we can take advantage of.
This book will provide an introduction to work concerned with formal logic for capturing temporal notions, called temporal logic, together with some of its applications in the formal development and analysis of computational systems. The name ‘temporal logic’ may ...
