This chapter will describe the formal specification of behavioural properties in Linear Temporal Logic (LTL).
In the meantime, you can learn this topic from Section 3.2.3 of my PhD thesis (Letier 2001) or Chapter 17 of van Lamsweerde’s book (Lamsweerde 2009). Both cover LTL as presented by Manna and Pnueli (Manna and Pnueli 1992), along with Koymans’ extension to real-time properties using Metric Temporal Logic (MTL) (Koymans 1990).
Koymans, Ron. 1990. “Specifying Real-Time Properties with Metric Temporal Logic.” Real-Time Systems 2 (4): 255–99.
Lamsweerde, Axel van. 2009. Requirements Engineering: From System Goals to UML Models to Software Specifications. John Wiley & Sons.
Letier, Emmanuel. 2001.
“Reasoning about Agents in Goal-Oriented Requirements Engineering.” PhD thesis, Universit
é catholique de Louvain.
http://www0.cs.ucl.ac.uk/staff/e.letier/publications/letier-thesis.pdf.
Manna, Zohar, and Amir Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specifications. Vol. 1. Springer Science & Business Media.