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 links zero-order logic and by LTL operators.

LTL temporal operators in Spin

LTL formulas are constructed using temporal operators that describe the behavior of variables over time - how 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 operator designations in Spin Alternative operator designations in Spin Operator Descriptions

Graphical notation (used in LTL literature)	Short operator designations in Spin	Alternative operator designations in Spin	Operator Descriptions
or G	`[]`	`always`	Formula `□φ` it reads like "the formula is always true" or "the formula is globally true." This means that `φ` It must be true at every step of the model simulation: initial, current, and all future ones.
◊ or F	`<>`	`eventually`	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`	Formula `φ U ψ` It reads like "the formula is true until one day the formula becomes true." This means that `ψ` it must become true either at the current step or in the future; before that `φ` It must be true.
W	`W`	`weakuntil`	Formula `φ W ψ` It reads like "the formula must remain true as long as the formula is false." This is the same as `φ U ψ` But `ψ` It doesn’t have to become true (then `φ` must always be executed): `φ W ψ = (φ U ψ) ∨ □φ`.
R	`V`	`release`	Formula `φ V ψ` it reads like "formula φ releases formula ψ". Formula `_V` is dual to the until formula (`U`): `¬(φ U ψ) = ¬φ V ¬ψ`. Meaning `φ V ψ`: `ψ` it must remain true either always or until the moment (including it) when `φ` it will become true.
◯	`X`	`next`	Formula `◯φ` it reads like "in the next step, the formula φ will become true."

or G

[]

always

Formula □φ it reads like "the formula is always true" or "the formula is globally true." This means that φ It must be true at every step of the model simulation: initial, current, and all future ones.

◊ or F

<>

eventually

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

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

W

weakuntil

Formula φ W ψ It reads like "the formula must remain true as long as the formula is false." This is the same as φ U ψ But ψ It doesn’t have to become true (then φ must always be executed): φ W ψ = (φ U ψ) ∨ □φ.

V

release

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

◯

X

next

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 LTL literature.

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

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

!

Denial.

∧

&&

/\

Conjunction (logical "And").

∨

\/

Disjunction (logical "OR").

⨁

^

The exclusive "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