MTSA Syntax

MTSA Syntax currently supports writing sequential and concurrent processes modelled as LTS using the Finite State Processes (FSP) language. It also supports writing formulae in Fluent Linear Temporal Logic for model checking and synthesis. There is additional syntax for modelling modal transition systems and markov decision processes.

Basic FSP syntax

MTSA preserves the full syntax supported by LTSA. Some references for its syntax are FSP-Syntax by Jeff Magee and Notes on FSP, Alan Williams, Donal Fellows, and Howard Barringer

Here we cover some aspects:

const, range, set

const declares a named integer constant, range a named integer interval, and set a named collection of labels.

const N = 3
range R = 1..N
set Colours = {red, green, blue}

SERVER = (request[i:R] -> reply[i] -> SERVER).

A set can be used wherever a similarly as a range — for example as a choice over its elements, or to extend a process alphabet with +:

set Colours = {red, green, blue}
LIGHT = (show[Colours] -> LIGHT).        // one branch per element of the set

set Ext = {pause, resume}
P = (run -> P) + Ext.                     // alphabet extension

Set size (`#`) and set element access (`@`)

The # operator gives the size (number of elements) of a set, as an integer, so it can be used anywhere an integer expression is expected — range bounds, constants, guards:

set Nodes = {n1, n2, n3, n4}
range Ids = 1..#Nodes
const NumNodes = #Nodes

The @(set, i) operator selects an element of a set by its 0-based index i, yielding that label. It is typically used to pass a set element as a process parameter, and combines naturally with # to instantiate one process per element:

set UID = {red, green, blue}
PROC(U=1) = (act[U] -> PROC).

||SYS = (forall[i:1..#UID] p[i]:PROC(@(UID, i-1))).

Here @(UID, 0), @(UID, 1) and @(UID, 2) are red, green and blue. An index outside 0 .. #set - 1 is a compile-time error.

when

A when guard makes a branch of a choice available only while its boolean condition holds. It is the standard way to encode state-dependent behaviour in an indexed process.

const Max = 2
BUFFER = COUNT[0],
COUNT[i:0..Max] = (when (i<Max) put -> COUNT[i+1]
                 | when (i>0)   get -> COUNT[i-1]).

if / then / else

Inside a process body, if (cond) then (P) else (Q) selects between two sub-behaviours according to a boolean condition over constants and indices.

A = (b -> if (1<2) then (a -> A) else (c -> A)).

forall

forall replicates a parallel composition over an index range: forall[i:R] ... composes one copy of the process per value of i. It is used in composite (||) definitions.

const N = 3
USER = (acquire -> use -> release -> USER).

||USERS = (forall[i:1..N] u[i]:USER).

The indexed-prefix shorthand (u[i:1..N]:USER) is equivalent.

foreach

Inside a process body, foreach[i:R] <choices> replicates the choice expression that follows once for each value of i in the range or set — a shorthand for a large | choice, and most useful combined with when guards or indexed labels.

range R = 0..2
P = (foreach[j:R] sel[j] -> P).
// equivalent to  P = (sel[0] -> P | sel[1] -> P | sel[2] -> P).

With an index-dependent guard:

const N = 2
range R = 1..N
SW = SW[1],
SW[cur:R] = (foreach[t:R] when (t!=cur) switch[t] -> SW[t]).

def

def NAME(p1, ...) = <expression> declares a parameterised expression macro: a named arithmetic expression over its parameters that is substituted wherever NAME(args) appears in another expression. It is handy for factoring out index arithmetic used by indexed processes.

const N = 3
def Next(i) = (i+1) % N

TOKEN = TOKEN[0],
TOKEN[i:0..N-1] = (use[i] -> pass -> TOKEN[Next(i)]).

Here Next(i) computes the next position in a ring of N, so the token passes 0 -> 1 -> 2 -> 0 -> .... Note def defines an expression, not a process.

rigid

rigid <expr> is a rigid (time-invariant) proposition, valid only inside an FLTL assertion (assert, ltl_property, constraint). The arithmetic expression over constants/parameters is evaluated once at compile time: it becomes true when <expr> > 0 and false otherwise. This lets a parameterised assertion switch on a compile-time condition. It is an advanced, rarely used feature inherited from LTSA.

const K = 1
fluent Fa = <a, b>
P = (a -> b -> P).

assert A = (rigid (K>0) -> []<> Fa)

Modifiers to process definitions

Deterministic

The deterministic keyword produces a deterministic LTS that preserves the traces of the original one. It can be used with sequential and composite processes.

Note that in composite processes the keyword takes precedence over hiding.

deterministic A = (a -> b -> A | a -> c -> A).

B = (a -> b -> B | a -> c -> B).
deterministic ||COMP = (B)\{a}.

C = (a -> b -> C | a -> c -> C)\{a}.
deterministic ||COMP2 = (C).

Closure

The closure keyword adds new transitions to the LTS resulting from compiling an FSP process according to the transitive closure of the transition relation over tau (silent) events. The keyword can be used with sequential and composite processes.

closure A = (a -> b -> A)\{b}.


B = (d -> a -> b -> B | d -> a -> c -> B).
closure ||COMP = (B)\{a}.

Property

The property keyword adds an error state and for every event and every other state it adds a transition to it if the event is not enabled in that state. It requires a deterministic LTS.

property POLITE
  = (knock->enter->POLITE).

Minimal keyword

The minimal keyword produces a minimal LTS, equivalent to the original one up to bisimulation. It can be used with sequential and composite processes.

As with deterministic, in composite processes hiding is applied before the minimisation.

minimal M = (a -> v -> M | a -> v -> M).

Compose

The compose keyword is supposed to force the parallel composition of a composite process to be computed explicitly, rather than kept in the deferred form. However the is not the MTSA. Thus, it makes not effect at all.

A = (a -> b -> A).
B = (b -> c -> B).
compose ||COMP = (A || B).

Other Keywords

Progress

The progress keyword declares a progress (liveness) property. It asserts that, in any infinite execution under fair choice, at least one of the actions in the given set occurs infinitely often.

progress HEADS = {heads}

progress HEADSorTAILS = {heads, tails}

The keyword also accepts a conditional if ... then ... which asserts that, in any infinite execution under fair choice, if at least one of the actions in the if happens infinitely then at least one of the actions in the then occurs infinitely often too.

progress P = if {enter} then {work}

Fluent Linear Temporal Logic (FLTL)

MTSA supports Fluent Linear Temporal Logic (FLTL) to express and check temporal properties over the traces of a system. A fluent is a boolean proposition defined by the actions that make it true and the actions that make it false. FLTL formulas are then written over fluents (and, directly, over action names) using the usual boolean and temporal operators.

Fluents

A fluent is declared with the set of actions that turn it on (initiating) and the set of actions that turn it off (terminating), plus an optional initial value 1 (true) or 0 (false, the default).

fluent LIGHT_ON = <switchOn, switchOff> initially 0

Either side may be a set of actions.

fluent LIGHT_ON = <{switchOn, turnOn}, {switchOff, turnOff}> initially 0

Fluents can be indexed meaning that various fluents are defined, each with its own index.

const N = 2
range R = 1..N
fluent HELD[i:R] = <acquire[i], release[i]>

The initially clause may be an expression over the indices.

const N = 3
range T = 0..N
fluent AT[i:T] = <arrive[i], {leave[i]}> initially (i==0)

Note that True and False are not built-in; to write initially False you must first declare the constants (const False = 0 and const True = 1).

const False = 0
const True = 1
fluent LIGHT_ON = <switchOn, switchOff> initially False

Temporal operators

FLTL formulas combine fluents and action names with the boolean connectives !, &&, ||, ->, <-> and the temporal operators:

[] f — always f (globally)
<> f — eventually f
X f — f holds in the next state
f U g — f holds until g (strong until)
f W g — f holds unless/weak until g
forall [i:R] f, exists [i:R] f — quantification over an index range

Assert

assert gives a name to an FLTL formula so it can be checked against a system (in the GUI: Check ▸ LTL Property).

LIGHT = (switchOn -> switchOff -> LIGHT).
fluent LIGHT_ON = <switchOn, switchOff> initially 0

assert ALWAYS_EVENTUALLY_ON = []<> LIGHT_ON
assert NO_DOUBLE_ON         = [](switchOn -> X(!switchOn W switchOff))

ltl_property

ltl_property compiles an FLTL safety formula into a property process (an LTS with an error state) that can be composed with a system to monitor it, analogous to a property definition but written in FLTL.


range R = 1..2
fluent In[i:R] = <enter[i], exit[i]>  initially 0

ltl_property MUTEX = [](!In[1] || !In[2])

constraint

constraint compiles an FLTL safety formula into a constraining process: unlike a property (which flags violations with an error state), a constraint only allows the behaviours that satisfy the formula. It is typically used to restrict a model or an environment.


range R = 1..2
fluent In[i:R] = <enter[i], exit[i]>  initially 0


constraint MUTEX = [](!In[1] || !In[2])

Unsupported

The keywords below are recognised by the parser but are not yet documented in this guide — and some are not currently functional. They are collected here as a working list to be documented and verified over time. The full index is in the MTSA Keyword Reference.

Animation / Visualisation

These keywords are related to the scenebeans animation capabilities developed originally for LTSA. This functionality has not received attention in many years and may not be fully functional.

menu — defines a menu
animation — animation specification
actions — action labelling
controls — control definition
target — inside an animation declaration, binds the XML scene to a composition.

Probabilistic

MTSA also supports some mdp model checking. This functionality has not received attention in many years and may not be fully functional.

probabilistic — marks a process/composition as probabilistic; transitions carry probability distributions, e.g. t -> {0.4:P1 + 0.6:P2}. Currently it must be paired with mdp.
mdp — selects the Markov Decision Process interpretation; composition builds an MDP abstraction. Written as probabilistic mdp ||C = (R || A).

Distribution

Splits a monolithic model into per-component models over given alphabets. Declared as a block: distribution C1, C2, ... = { distributedAlphabets = {A1, ...} systemModel = SYS [outputFileName = "..."] }.

distribution — opens the block; takes the comma-separated component names (needs exactly one alphabet per component).
distributedAlphabets — the alphabets (one per component) to project the system onto.
systemModel — the monolithic process to be distributed.
outputFileName — optional string path where the distribution result is written.

Miscellaneous

import — imports an external LTS from an Aldebaran .aut file as a named process, bypassing FSP compilation: import NAME = "file.aut".

← End User