Imagine you have a system that can have a number of states, and "events" for state transitions.  Fluents are then the constructs that help to reason about state transitions.

Here is an example inspired by [Queins et. al. 2000] that got picked up by [Letier 2005]: Assume that you have the task of building a light controller.  By pushing a button, light is turned out and will switch off after some time.  pushing the button when the light is on will reset the timer.

In this example, we may have the state variables light ∈ {on, off} and timer ∈ {0..n}.  For now, the timer simply counts ticks.  To set these state variables, we may have the events "pushButton", "switchOn", "switchOff", and "tick".

A Fluent is a proposition defined by a pair of sets of events.  Events from the first set the fluent to true, the second to false, e.g.:

fluent LightOn = <switchOn, switchOff>

We can use the Fluent in  temporal logic (e.g. LTL):

â—» (pushButton X LightOn)

The box means "always", and X means "next". So the above means "When pushing the button, next the fluent LightOn must be true".

Quite a bit is fishy here.  For instance, what exactly does "next" mean?  This is where Letier’s contribution comes from: it could be the next event (which he calls asynchronous) or the next tick (which he calls synchronous).  Also check out how restrictive the statement is in the asqnchronous case: It is not allowed to insert any events after pushButton, which would make refinement through stuttering impossible.