Chapter 8
Summary
I never think of the future; it comes soon enough.
—Albert Einstein
So, we are at the end. But, what have we seen?
It turns out that temporal logic (certainly the variety we have looked at here) is essentially quite a simple formalism. However, in spite of this simplicity, we have seen how temporal logics have very many potential applications, beginning with the formal specification of concurrent, interacting and communicating systems. Describing such reactive systems in a formal way clarifies their behaviour and formalizes our intuitive view of what this behaviour should comprise.
Although carrying out such formal specification is both an informative and useful process, if we cannot manipulate the resulting specifications in interesting and productive ways, then surely the logical framework itself would not be so appealing. Yet, as we have seen, this is not a problem with temporal specifications. A wide range of techniques has been developed for manipulating these descriptions, together with very many practical tools that implement these techniques.
Deductive techniques allow us to establish whether temporal statements are true or false, with the clausal temporal resolution approach specifically being the focus of our attention. Algorithmic techniques move towards analysing the detailed temporal properties of structures, something that is particularly important in model checking where the structures typically describe the runs of a particular system. Techniques ...
