Linear Time Time Logic (LTL) in Spin

Formulas of temporal or temporal logic of linear time (Linear Temporal Logic) are used as specifications (constraints, requirements) of the model in the Promela language.

Each such formula can consist of global names (and even local ones - special syntax <process name>[<process number>]:<variable name>) variables connected by logical connectives zero-order logic and by LTL operators.

LTL temporal Operators in Spin

LTL formulas are constructed using temporal operators usage, which describe the behavior of variables in time - how the values should change or remain unchanged at different simulation steps.

The table below shows the main LTL operators supported by the Spin tool.

Graphical notation (used in LTL literature) Short notation of operators in Spin Alternative notation of operators in Spin Operator descriptions

Graphical notation (used in LTL literature)	Short notation of operators in Spin	Alternative notation of operators in Spin	Operator descriptions
or G	`[]`	`always`	The formula `□φ` it is read as "the formula _ _ is always true" or "the formula _ _ is globally true". This means that `φ` It must be true at every step of the simulation of the model: initial, current and all future.
◊ or F	`<>`	`eventually`	The formula `◊φ` it reads like "the formula _ will someday become true." This means that `_φ` It must be true at least once — either at the current step or sometime in the future.
∪ or U	`U`	`until` or `stronguntil`	The formula `φ U ψ` It reads like "the formula is true until one day the formula becomes true." This means that `ψ` must become true either at the current step or in the future; before that `φ` must be true.
W	`W`	`weakuntil`	The formula `φ W ψ` It reads like "the formula must remain true as long as the formula is false." This is the same as `φ U ψ`, but `ψ` does not have to become true (then `φ` must always be executed): `φ W ψ = (φ U ψ) ∨ □φ`.
R	`V`	`release`	The formula `φ V ψ` it reads like "formula _ _ releases formula ". The formula `_V` is dual to the formula until (`U`): `¬(φ U ψ) = ¬φ V ¬ψ`. Meaning `φ V ψ`: `ψ` must remain true either always or until the moment (including it) when `φ` it will become true.
◯	`X`	`next`	The formula `◯φ` it reads like "in the next step, the formula __ will become true."

or G

[]

always

The formula □φ it is read as "the formula _ _ is always true" or "the formula _ _ is globally true". This means that φ It must be true at every step of the simulation of the model: initial, current and all future.

◊ or F

<>

eventually

The formula ◊φ it reads like "the formula _ will someday become true." This means that _φ It must be true at least once — either at the current step or sometime in the future.

∪ or U

U

until or stronguntil

The formula φ U ψ It reads like "the formula is true until one day the formula becomes true." This means that ψ must become true either at the current step or in the future; before that φ must be true.

W

weakuntil

The formula φ W ψ It reads like "the formula must remain true as long as the formula is false." This is the same as φ U ψ, but ψ does not have to become true (then φ must always be executed): φ W ψ = (φ U ψ) ∨ □φ.

V

release

The formula φ V ψ it reads like "formula _ _ releases formula ". The formula _V is dual to the formula until (U): ¬(φ U ψ) = ¬φ V ¬ψ. Meaning φ V ψ: ψ must remain true either always or until the moment (including it) when φ it will become true.

◯

X

next

The formula ◯φ it reads like "in the next step, the formula __ will become true."

Designations of logical connectives allowed in LTL Spin

In addition to temporal operators, LTL formulas use the usual logical connectives - negation, conjunction, disjunction, and others.

The table below shows their designations in Spin and in the literature on LTL.

Graphical notation (in the literature) Short notation in Spin Alternative notation in Spin Description

Graphical notation (in the literature)	Short notation in Spin	Alternative notation in Spin	Description
¬	`!`		Denial.
∧	`&&`	`/\`	Conjunction (logical "And").
∨	`		`
`\/`	Disjunction (logical "OR").	⨁	`^`
	Excluding "OR" (XOR).	⟹	`→`
`implies`	Implication ("if …, then …").	⟺	`<→`

!

Denial.

∧

&&

/\

Conjunction (logical "And").

∨

\/

Disjunction (logical "OR").

⨁

^

Excluding "OR" (XOR).

⟹

→

implies

Implication ("if …, then …").

⟺

<→

Linear Time Time Logic (LTL) in Spin

LTL temporal Operators in Spin

Designations of logical connectives allowed in LTL Spin

Useful links