C.7 Fluent Linear Temporal Logic (FLTL)

C.7.1 Linear Temporal Logic

Given a set of atomic propositions , a well-formed LTL formula is defined inductively using the standard Boolean operators ! (not), | | (or), && (and), and the temporal operators X (next) and U (strong until) as follows:

each member of is a formula,
if φ and ψ are formulae, then so are ! φ, φ || ψ, φ && ψ, X φ, φ U ψ.

An interpretation for an LTL formula is an infinite word w = x₀x₁x₂ ... over . In other words, an interpretation maps to each instant of time a set of propositions that hold at that instant. We write w_i for the suffix of w starting at x_i. LTL semantics is then defined inductively as follows:

w |= p iff p ∈ x₀, for p ∈
w |= ! φ iff not w| = φ
w |=φ || ψ iff (w| = φ) or (w| = ψ)
w |=φ && ψ iff (w| = φ) and (w| = ψ)
w |= X φ iff w₁| = φ
w |=φ U ψ iff i ≥ 0, such that: w_i| = ψ and ∀ 0 ≤ j < i, w_j| = φ

We introduce the abbreviations “true ≡ φ || ! φ” and “false ≡ ! true”. Implication -> and equivalence <-> are defined as:

Temporal operators <> (eventually),[] (always), and W (weak until) are defined in terms of the main temporal operators:

image from book

C.7.2 Fluents

We define a fluent Fl by a pair of sets, a set of initiating actions I_Fl and a set of terminating actions T_Fl:

In addition, a fluent Fl may initially be true or false at time zero as denoted by the attribute Initially_Fl.

The set of atomic propositions from which FLTL formulae are built is the set of fluents Φ. Therefore, an interpretation in FLTL is an infinite word over 2^Φ, which assigns to each time instant the set of fluents that hold at that time instant. An infinite word < a₀a₁a₂ ··· > over Act (i.e. an infinite trace of actions) also defines an FLTL interpretation < f₀f₁f₂ ··· > over 2^Φ as follows:

∀i ∈ N, ∀ Fl ∈ Φ, Fl ∈ f_i iff either of the following holds
– Initially_Fl (∀k ∈ N · 0 ≤ k ≤ i, a_kT_Fl)
–j ∈ N : ((j ≤ i) (a_j ∈ I_Fl) (∀k ∈ N · j < k ≤ i, a_k T_Fl))

In other words, a fluent holds at a time instant if and only if it holds initially or some initiating action has occurred, and, in both cases, no terminating action has yet occurred. Note that the interval over which a fluent holds is closed on the left and open on the right, since actions have immediate effect on the values of fluents. Since the sets of initiating and terminating actions are disjoint, the value of a fluent is always deterministic with respect to a system execution.

Every action a implicitly defines a fluent whose initial set of actions is the singleton {a} and whose terminating set contains all other actions in the alphabet of a process A Act :

Fluent(a) becomes true the instant a occurs and becomes false with the first occurrence of a different action. It is often more succinct in defining properties to declare a fluent implicitly for a set of actions as in:

This is equivalent to a₀ || a₁ || ... || a_n where a_i represents the implicitly defined Fluent(a_i).