 The idea to apply temporal reasoning to the analysis of deterministic and stochastic transition systems was already present in the theory of processes and events in Rescher and Urquhart (1971, Chapter XIV). However, it was with the seminal paper of Pnueli (1977) that temporal logic became really prominent in computer science. Pnueli proposed the application of temporal logics to the specification and verification of reactive and concurrent programs and systems. In order to ensure correct behavior of a reactive program, in which computations are non-terminating (e.g. an operating system), it is necessary to formally specify and verify the acceptable infinite executions of that program. In addition, to ensure correctness of a concurrent program, where two or more processors are working in parallel, it is necessary to formally specify and verify their interaction and synchronization.