Safety properties are specified to LTSA as deterministic primitive processes which contains no silent (tau) transitions (no hiding). Safety property processes are denoted by the keyword property. Informally, a property process specifies a set of acceptable behaviours for the system it is composed with. A system S will satisfy a property P if S can only generate sequences of actions (traces) which when restricted to the alphabet of P, are acceptable to P. For example, the following property specifies that only behaviour in which knock occurs before enter is acceptable.

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

The systems specified below would generate property violations:

HESITANT = (knock->knock->enter->HESITANT).
IMPATIENT = (enter -> IMPATIENT).

||SysA = (HESITANT || POLITE).
||SysB = (IMPATIENT || POLITE).

Property processes do not constrain the operation of the systems they are composed with. They are compiled into "image" LTS, which accept all possible interleavings of their alphabets. However, violating sequences of actions lead to an error state (represented as -1) as shown in the LTS for POLITE.

The error state was generated implicitly above through the use of a safety property process. However, it can also be generated directly by using the predefined local process ERROR. ERROR behaves like STOP in that it does not engage in any further actions. However, it has an alphabet consisting of all the actions in the system. Consequently, ERROR will always bring the system to a halt. The following example is taken from the model of an Active Badge system. It is a model of the infrared transmitter, which can only process one command at a time. Consequently, it is an error if another command is received before the first is either acknowledged or cancelled.

const NBAD = 2

TX = (command[b:1..NBAD] -> (ack[b] -> TX 
			     | cancel[b] -> TX
			     | command[c:1..NBAD]->ERROR)).