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. ...

Get An Introduction to Practical Formal Methods using Temporal Logic now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.