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 
 
 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.
 
@@ -20,7 +19,7 @@ range N = 1..3
 fluent Ready[i:N] = <ready[i], reset[i]> initially False
 ```
 
-## Assertions in FLTL
+# 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).
 
@@ -30,7 +29,7 @@ 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
+# 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. 
 
@@ -42,7 +41,7 @@ ltl_property ONOFF = ([](on -> X off) && [](off -> X on) && on)
 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
+# 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.