This fourth and last part of the book provides algorithmic methods for the main decision problems that come with temporal logics: satisfiability, validity and model checking. Model checking is typically easier, particularly for branching-time logics, and therefore admits simpler solutions that have been presented in the chapters of Part II already. Since temporal logics are usually closed under complementation, satisfiability and validity are very closely related and methods dealing with one of them can easily be used to solve the other, so we will not consider them separately. Indeed, in order to check a formula φ for validity, one can check ¬φ for satisfiability and invert the result since φ is valid iff ¬φ is unsatisfiable. Satisfiability is reducible to validity likewise. Furthermore, a satisfiability-checking procedure would typically yield not only the answer but also, in the positive case, a model witnessing the satisfiability of the input formula. Such an interpreted transition system would refute validity of ¬φ, i.e. be a countermodel for its validity. Hence, the focus of this part is on satisfiability checking.

The methods presented here are closely linked to Chapter 11, which provided lower bounds on the computational complexity of these decision problems, i.e. it explained how difficult these problems are from a computational perspective. The following chapters provide themissing halves to an exact analysis of temporal logics’ computational complexities: by estimating the time and space consumption that these methods need in order to check for satisfiability, satisfaction, etc., we obtain upper bounds on these decision problems. Thus, while Chapter 11 showed how hard at least these problems are, the following chapters show how hard they are at most, by presenting concrete algorithmic solutions for these decision problems.

The methods presented in the following three chapters are in fact methodologies in the sense that each chapter introduces a particular framework for obtaining methods for certain temporal logics. Each of these frameworks – tableaux, automata and games – has its own characteristics, strengths and weaknesses and may or may not be particularly suited for particular temporal logics. Axiomatic systems, presented in the respective chapters of Part II, provide an alternativemethodology that historically appeared first, but they can only be used to establish validity (resp. nonsatisfiability) when it is the case, and provide no answer otherwise, so they are not really decision methods.