A.5 Fluent Linear Temporal Logic (FLTL)

Table A.5: Fluent Linear Temporal Logic
Open table as spreadsheet
Fluent fluent	fluent FL = <{s₁,...s_n}, {e₁..e_n}> initially B defines a fluent FL that is initially true if the expression B is true and initially false if the expression B is false. FL becomes true immediately any of the initiating actions {s₁,...s_n} occur and false immediately any of the terminating actions {e₁..e_n} occur. If the term initially B is omitted then FL is initially false.
Assertion assert	assert PF = FLTL_Expression defines an FLTL property.
&&	conjunction (and)
\|\|	disjunction (or)
!	negation (not)
->	implication ((A->B) ≡ (!A\|\|B))
<->	equivalence ((A<->B) ≡ (A->B)&&(B->A))
next time XF	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.
forall	forall[i:R] FL(i) conjunction of FL(i)
exists	exists[i:R] FL(i) disjunction of FL(i)