Specifying with Temporal Logic

For a more explicit treatment of this topic see Berard et al. [34]:77ff.