Temporal Logic

  • Hillel Wayne


So far everything we’ve done has been testing invariants: statements that must be true for all states in a behavior. In this chapter, we introduce Temporal Properties: statements about the behavior itself. Temporal properties considerably expand the kinds of things we can check, providing a range of techniques that few other formal methods tools can match. Some examples of temporal properties:
  • Does the algorithm always terminate?

  • Will all messages in the queue get processed?

  • If disrupted, will the system return to a stable state over time?

  • Is the database eventually consistent?

Copyright information

© Hillel Wayne 2018

Authors and Affiliations

  • Hillel Wayne
    • 1
  1. 1.ChicagoUSA

Personalised recommendations