Update: Revised reference to Fages and Rizk time series paper — see below.
The slides for this lecture review Linear Temporal Logic (LTL), with several examples of LTL formulae for expressing properties of Petri Net behaviour.
Boardwork then gave the expansion from linear time to branching time, the syntax for CTL formulae, and some small discussion of their interpretation.
The final slide gives some further reading, reproduced below. All articles are linked to web pages where you should be able to download copies: you may be asked to log in with the EASE authentication service along the way.