Liveness properties in LTSA are specified as Buchi automata. In general, these are not obvious since it is necessary to specify the Buchi automata for the complement of the logical property being checked. However, the Template menu provides a set of LTL (Linear Temporal Logic) formulas. Selecting one of these generates the FSP text for the complement of the LTL property. For example the formula for always a implies eventually b:
[] (a => <> b)
has the following Buchi automata for its complement.
/* Liveness property - always (a implies eventually b) */
L1 = ({a,b}->L1 | a->L1A),
L1A@ = (a -> L1A | b -> L1F),
L1F = ({a,b} ->L1F)
/ {$$$/a, $$$/b}.
The user is required to substitute the relevant application action labels for a and b. The extra FSP syntax here is the marking of the acceptance state L1A using @. The following LTS is generated for the process L1.
