FSP notation


FSP stands for Finite State Process. It is the notation used to specify the behaviour of concurrent systems to LTSA. FSP specifications generate finite Labelled Transition Systems (see). The syntax and semantics owe much to both Hoare's CSP and Milner's CCS. FSP behaviour specifications contain (see semantics) two sorts of process definitions: primitive processes and composite processes. Safety properties are specified using property automata and liveness properties using Buchi automata.

Primitive Processes

Primitive processes are defined using action prefix, choice and recursion. Both action labels and local process names may be indexed which greatly increases the descriptive power of FSP.

Action Prefix "->"

Choice "|"


Alphabet extension "+{...}"


Conditionals and Guards


Composite Processes

Composite processes are defined using parallel composition, relabelling and hiding.

Parallel Composition "||"

Relabelling "/"

Hiding "\" and "@"

Prefixed labels

Conditionals and Recursion

Forall - process replication

Process labelling


LTSA provides different techniques for checking safety and properties. Correspondingly, FSP provides a way of specifying safety properties (using image automata) and a way of specifying liveness properties (using Buchi automata).

Safety properties and ERROR

Liveness properties

FSP Syntax reference

FSP Semantics