The basic concepts of mathematical logic, starting from Boolean algebra and sentential logic, to first-order logic and Gödel’s incompleteness theorem, were discovered in the 19th and early 20th centuries, as a consequence of the need to reason about mathematics and codify logical thinking. The needs of the computing sciences to describe processes and events later gave rise to a newer type of analytical tool, called temporal logic, which, as the name suggests, allows for the analyses to include the time sequence of events, which is not possible in the classical logic. (Note that, in the propositional logic, A & B is the same as B & A, while in everyday understanding, “He showered and dressed” is not the same as “He dressed and showered.”)

Temporal logic formalisms have received a great deal of attention since the 1980s, and some of the better known ones among them include Misra’s UNITY, Lamport TLA, and duration calculus (DC). This book addresses the last, and is the first definitive monograph on DC, by two of the founders. DC models real-time systems using states and events, with the behavior of real-time systems being modeled using state durations. A state is simply a Boolean function over time, namely, a mapping from time (considered to be the continuous real line, the uncountable set of real numbers) to the set {0,1}. The duration of a state is considered to be the definite integral of the state function over its temporal end points.

The first chapter of the book introduces its topics and definitions, giving examples of real-time systems, and certain safety properties that are associated with them. These are a gas burner, a software-embedded system (required to meet the safety property of not leaking too long in proportion to a minute or more of use), and a deadline-driven real-time process scheduler, first studied by Liu and Layland [1]. (These two examples are revisited several times in the book.) The second chapter lays out a first-order, complete interval logic that is the basis of DC. The syntax and semantics of the DC are presented in chapter 3, using the gas burner example. This, and the previous chapter, consist in large part of various theorems and proofs, and cannot be understood easily. (It also appears to me that several of the proofs could use more detail, in the interest of clarity.) Chapter 4 gives a concrete example of the DC, by specifying and verifying the deadline-driven scheduler algorithm proposed by Liu and Layland. Chapter 5, a short one, proves a relative completeness result for the DC, and the next two chapters address subsets of DC formulas that are decidable and undecidable, considering time to be discrete or continuous. The final few chapters present certain advanced topics, and appear to be independent of one another.

The appearance of this monograph is a welcome development, as it collects, in one place, otherwise-scattered research results. However, although it is doubtless suited to graduate courses and researchers, as the publishers claim, there is little indication that it can be used by professionals, as also claimed, since the highly abstract results (and the gas burner and scheduler examples) shed little light on the problems involved in the design of practical, safety-critical systems. This, however, is the kind of remark that could be made of much current research, and is not a criticism of what is doubtless an excellent work.