Summary

The primitive propositions of the linear temporal logic we described in this chapter are termed “fluents”. A fluent is defined by a set of initiating actions and a set of terminating actions. At a particular instant, a fluent is true if and only if it was initially true or an initiating action has previously occurred and, in both cases, no terminating action has yet occurred. Using fluents, we can map the trace produced by a model into a sequence of sets. Each set in the sequence contains the fluents that are true at the point the corresponding action in the trace occurs. Fluent linear temporal logic (FLTL) is defined with respect to these sequences. For each action, we define a synonymous fluent which holds when the action occurs and becomes false immediately the following action occurs. We termed these actions “fluents” and they can be freely mixed with explicitly defined fluents in expressions. The following table summarizes the temporal operators used in FLTL (“iff” abbreviates “if and only if”):

next time X F	iff F holds in the next instant.
always F	iff F holds now and always in the future.
eventually <>F	iff F holds at some point in the future.
until P U Q	iff Q holds at some point in the future and P holds until then.
weak until P W Q	iff P holds indefinitely or P U Q.

The chapter outlined some typical ways of expressing safety and liveness properties. Using the database ring example, we also explained how to produce witness executions and how to deal with finite executions. In checking liveness properties, we make the same assumptions with respect to fair choice as those made in Chapter 7 and use the same action priority approach to generate adverse scheduling conditions.