This book represents the fruitful achievements of the authors’ outstanding accomplishments and cooperation in the field of temporal logic, providing a comprehensive mathematical and computational tool fo research and applications of the domain. The contents may be summarized as follows: Chapter 1 is an introductory survey review of the topic and of the contents of the book. Chapter 2 begins the semantical presentation of temporal connectives for propositional temporal logic, with its basic elements being the flow of time, the assignment to the atoms, and the temporal connectives. Chapter 3 approaches the axiomatic presentation of propositional temporal connectives: the Hilbert system \(K_t\) and some of its axiomatic variants. Chapter 4 introduces predicate temporal logic, while Chapter 5 points out the relationship between temporal logics as languages, and predicate calculi as metalanguages. Chapter 6 presents a general theory of axiomatization for propositional temporal logic. A survey on the technical aspects of many-dimensional temporal logics is provided in Chapter 7. Chapter 8 investigates the two related topics of propositional quantifiers and fixed-point operators. The next three chapters are devoted to the expressive power of various temporal logics, using as basic tools the separation theorems. One-dimensional temporal connectives are investigated in Chapter 9, the expressive completeness of “Since” and “Until” over integer and real time is considered in Chapter 10, and Stavi connectives over general linear time are analyzed in Chapter 11. Chapter 12 proves the main result of the previous chapter (i.e., the expressive completeness of Stavi connectives) not on the basis of the separation property but by using the technique of Ehrenfeucht-Fraïssé games. A fundamental property of of temporal flow, namely its Henkin dimension, and its relationship to the expressive completeness of temporal logics, are taken into account in Chapter 13. Interesting approaches are involved in the process of temporalizing an existing logic (Chapter 14), while decidability/undecidability, effectiveness, and complexity results are obtained in Chapter 15. An extensive bibliography of 666 basic titles in the field, and adequate indexes, add to the high quality and usefulness of the book.