MTSA supports fluent linear temporal logic formulae FLTL 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 names or action names 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, select a composite process from the pulldown menu at the top of the application window, then use 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 = (ONOFF2 || 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 interpretation 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)

---

← End User