O'Reilly logo

An Introduction to Practical Formal Methods using Temporal Logic by Michael Fisher

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Chapter 4

Deduction

The past is certain, the future obscure.

—Thales of Miletus.

In this Chapter, we will:

  • [INTRODUCTION] examine the idea of deciding on the truth of temporal formulae using formal rules and procedures (Section 4.1);
  • [TECHNIQUE] introduce the clausal temporal resolution method for proof in PTL (Section 4.2);
  • [SYSTEM] describe the TSPASS system which is one of those implementing the clausal temporal resolution approach (Section 4.3); and
  • [ADVANCED] highlight a selection of more advanced work including alternative methods and tools (Section 4.4).

Although fewer in number than in previous chapters, exercises will again be interspersed throughout the chapter with solutions provided in Appendix B.

4.1 Temporal Proof

As we saw in the last chapter, we often want to check whether one temporal formula implies another. For example, if we have specified a system using the temporal formula, ψ, then we can check whether a certain temporal property, say φ, follows from the specification of the system by establishing that φ is implied by ψ, that is, whether vdash ψ ⇒ φ. This can be achieved by proving that one temporal formula implies another.

There are a variety of mechanisms for deciding proof problems in temporal logic, some of which we will mention in this chapter. However, our main technique will be a variety of clausal resolution for PTL. Before proceeding, it is appropriate ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required