Abstract

We present an introductory survey of temporal and dynamic logics: logics for reasoning about how environments change over time, and how dynamic processes affect their environments.We begin by introducing the historical development of temporal and dynamic logic, starting with the seminal work of Prior. This leads to a discussion of the use of temporal and dynamic logic in computer science. We describe LTL, CTL, and PDL; three key formalisms used in computer science for reasoning about programs, and illustrate how these formalisms may be used in the formal specification and verification of computer systems.We then discuss interval temporal logics.We conclude with some pointers for further reading.