enduser/Fluents-and-LTL-properties.md

+# Fluents and LTL properties
+
+MTSA supports fluent linear temporal logic formulae [FLTL](https://doi.org/10.1145/949952.940106) to write properties that can be checked against models and also as a form of constructing models.
+
+
+## Fluents 
+
+Fluents are defined with an initiating and terminating set of actions that must be disjoint. Also an initial value can be set. The default value is false.
+
+```
+const True = 1
+fluent DoorOpen = <open, close> 
+fluent off = <{off, reset}, on > initially True
+```
+
+Fluents can be indexed:
+
+```
+range N = 1..3
+fluent Ready[i:N] = <ready[i], reset[i]> initially False
+```
+
+## Assertions in FLTL
+
+FLTL properties are constructed with the assert keyword using fluent or events as atoms, non-temporal operators  -- || (or), && (and), <-> (iff), -> (implication), !( (negation) --, quantifiers ----- forall, exists--, and temporal operators -- U (Until). W (weak until), X (next), <> (eventually), [] (always).
+
+```
+assert ALL_READY = forall[i:N] ([]<>Ready[i])
+```
+
+To check a behaviour model against a property, a composite process must be chosen from the pulldown menu at the top of the application window. Then Check->LTL from the menu.
+
+## Observers defined in FLTL
+
+It is possible to create a process that observes system behaviour and flags violations of safety properties defined by an FLTL formula. 
+
+```
+ltl_property ONOFF = ([](on -> X off) && [](off -> X on) && on)
+||MONITORED_SYS = (ONOFF || SYS).
+```
+
+The ltl_property keyword works similarly to the property keyword, except that the former takes a safety property expressed in FLTL and the latter a sequential process defined in FSP.
+
+
+## Constraints defined in FLTL
+
+The constraint keyword builds a process that constrains all behaviour that violates a given FLTL safety property. Where ltl_property flags an error, constraint impedes the event that would flag that error.
+
+```
+constraint ONOFF2 = ([](on -> X off) && [](off -> X on) && on)
+||CONSTRAINED_SYS = (ONOFF || SYS).
+```
+
+The alphabet of the resulting LTS contains exactly all events that appear
+in the formula or in fluent definitions used by the formula.
+This implies that the interpetation of the next operator (X) is of an alphabetised next.
+
+```
+constraint P = [] (p -> X q)
+
+fluent A = <a, c>
+fluent B = <b, c>
+
+constraint Q = [](A -> X B)
+```
\ No newline at end of file