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

Appendix B

Solutions to Exercises

These Things Take Time.

—The Smiths

Solutions: Chapter 2

[2.1] Which of the following are not legal WFF of PTL, and why?

(a) images/b02_I0001.gif............................................not legal – left-hand side of ‘images/b02_I0002.gif’ is not a WFF

(b) images/b02_I0003.gif........................................legal

(c) images/b02_I0004.gif...............................not legal – binary operator expected between the propositional symbol ‘images/b02_I0005.gif’ and ‘(’

[2.2] How might we represent the following statements in PTL?

(a)In the next moment in time, running’ will be true and, at some time after that,images/b02_I0006.gifwill be true.”.........images/b02_I0007.gif

(b)There is a moment in the future where eitherimages/b02_I0008.gifis always true, or ‘’ is true in the next moment in time. ...

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