Temporal logic of actions

This article or section needs to be revised. Details should be given on the talk page. Please help to improve it , and then remove this flag.

The temporal logic of actions (TLA) is a further development of the temporal logic (engl. Temporal logic) and the logic of actions (engl. Logic of actions). It was developed by Leslie Lamport .

The temporal logic of actions is part of the propositional logic (Engl. Propositional logic) and is used in computer science for specification, reasoning and verification of systems (z. B. programs) are used. A specification in TLA is a logical formula that describes all possible and correct behavior of a system. Using this logical formula, systems can be checked for undesired and desired properties.

Symbols

The symbols of Boolean algebra and other symbols apply

${\displaystyle {\hat {=}}}$	same by definition
${\displaystyle \models F}$	F is valid
${\displaystyle \Box }$	always
${\displaystyle \Diamond }$	finally, finally
${\displaystyle \lbrack A\rbrack }$	Action (stuttering step)
${\displaystyle \langle A\rangle }$	action

Syntax and semantics

${\displaystyle \langle Formel\rangle }$	${\displaystyle {\hat {=}}}$	${\displaystyle \langle Formel\rangle \land \langle Formel\rangle }$  ${\displaystyle \vert }$  ${\displaystyle \langle Formel\rangle \lor \langle Formel\rangle }$  ${\displaystyle \vert }$  ${\displaystyle \neg \langle Formel\rangle }$  ${\displaystyle \vert }$  ${\displaystyle \Box \langle Formel\rangle }$  ${\displaystyle \vert }$  ${\displaystyle \Diamond \langle Formel\rangle }$  ${\displaystyle \vert }$  ${\displaystyle \langle Pr{\ddot {a}}dikat\rangle }$  ${\displaystyle \vert }$  ${\displaystyle \Box {\lbrack \langle Aktion\rangle \rbrack }_{\langle Zustandsfunktion\rangle }}$
${\displaystyle \langle Aktion\rangle }$	${\displaystyle {\hat {=}}}$	Boolean expression consisting of constants, variables and primed variables. An action represents a relation between two states, with deleted variables referring to the new state. A pair of states that fulfill an action A is called A step.
${\displaystyle \langle Pr{\ddot {a}}dikat\rangle }$	${\displaystyle {\hat {=}}}$	${\displaystyle \langle Aktion\rangle }$without deleted variable     Enabled (action) ${\displaystyle \vert }$
${\displaystyle \langle Zustandsfunktion\rangle }$	${\displaystyle {\hat {=}}}$	Non-Boolean expression from constants, variables to describe a state
behavior	${\displaystyle {\hat {=}}}$	infinite sequence of states

The following are z, u states, f state functions, A actions, F, G formulas, p predicates, v variables and behavior. ${\displaystyle \sigma }$

Let f be a state function or a predicate, then f 'is the expression f in which all variables have been replaced by deleted variables.

${\displaystyle z\lbrack f\rbrack }$	${\displaystyle {\hat {=}}}$	${\displaystyle f(\forall 'v':z\lbrack v\rbrack /v)}$
${\displaystyle s\lbrack f\rbrack u}$	${\displaystyle {\hat {=}}}$	${\displaystyle f(\forall 'v':z\lbrack v\rbrack /v,u\lbrack v\rbrack /v')}$
${\displaystyle \models A}$	${\displaystyle {\hat {=}}}$	${\displaystyle \forall z,u:z\lbrack A\rbrack t}$
${\displaystyle \sigma \lbrack F\land G\rbrack }$	${\displaystyle {\hat {=}}}$	${\displaystyle \sigma \lbrack F\rbrack \land \sigma \lbrack G\rbrack }$
${\displaystyle \sigma \lbrack \neg F\rbrack }$	${\displaystyle {\hat {=}}}$	${\displaystyle \neg \sigma \lbrack F\rbrack }$
${\displaystyle \models F}$	${\displaystyle {\hat {=}}}$	${\displaystyle \forall \sigma :\sigma \lbrack F\rbrack }$
${\displaystyle {\lbrack A\rbrack }_{f}}$	${\displaystyle {\hat {=}}}$	${\displaystyle A\lor (f'=f)}$
${\displaystyle {\langle A\rangle }_{f}}$	${\displaystyle {\hat {=}}}$	${\displaystyle A\land (f'\neq f)}$

${\displaystyle {\lbrack A\rbrack }_{f}}$ is a stuttering step that leaves the value of the variable unchanged.

${\displaystyle {\langle A\rangle }_{f}}$ is a step that changes the state function.

For each action A, an Enabled A predicate is defined. It is only true in a state if it is possible to perform an A-step from this state. In other words, Enabled A is true in state z if a state u exists, so that A is step. In a behavior, a predicate is only true if it is true in the first state. ${\displaystyle \langle z,u\rangle }$

Behavioral characteristics

A security property guarantees that undesired states are never reached.

A liveliness property guarantees that desired states will be reached at some point.

In a concurrent system, a distinction is made between weak and strong fairness . Weak fairness (English weak fairness, justice) means that an action must be carried out infinitely often if it is always possible to carry out it from a certain point in time. In other words: If an action is only carried out finitely often, it cannot be carried out infinitely in a behavior. It guarantees that the action will eventually be carried out or that it will be impossible to carry out - even if only for a certain period of time.

Strong fairness (compassion) means that an action has to be carried out infinitely often if it is possible to carry it out indefinitely. In other words: If an action is only carried out finitely often, it can only be carried out finitely often in one behavior. It assures that the action will eventually be carried out or that it will eventually become impossible to carry out forever.

If behavior is strongly fair to an action, it is also weakly fair to that action.

Representation and example

var x = 0, y = 0

doParallel ({x: = x + 1}, {y: = y + 1})

The above program in pseudocode should add 1 to either x or y in parallel processing (non-deterministic).

So that a TLA specification can be specified, the status functions and actions must first be defined.

In this example, a state that is also the initial state is sufficient.

${\displaystyle Init_{\phi }=(x=0)\land (y=0)}$

The additions running in parallel can be described in two actions . ${\displaystyle M_{1},M_{2}}$

${\displaystyle M_{1}{\hat {=}}(x'=x+1)\land (y'=y),}$
${\displaystyle M_{2}{\hat {=}}(y'=y+1)\land (x'=x),}$
${\displaystyle M=M_{1}\lor M_{2}}$

Finally, fairness conditions are specified. SF as strong fairness and WF as weak fairness.

${\displaystyle SF_{\langle x,y\rangle }(M_{1})}$
${\displaystyle SF_{\langle x,y\rangle }(M_{2})}$

From these three components we get the following TLA formula:

${\displaystyle Init_{\phi }=(x=0)\land (y=0)}$
${\displaystyle M_{1}{\hat {=}}(x'=x+1)\land (y'=y)M_{2}{\hat {=}}(y'=y+1)\land (x'=x)}$
${\displaystyle M=M_{1}\lor M_{2}}$
${\displaystyle \phi {\hat {=}}Init_{\phi }\land \Box {\lbrack M\rbrack }_{\langle x,y\rangle }\land SF_{\langle x,y\rangle }(M_{1})\land SF_{\langle x,y\rangle }(M_{2})}$

See also

• Formal systems
• Formal semantics
• Formal language
• Mobile temporal logic of actions

Web links

• Temporal logic guide
• TLA + - The way to specify, community website on TLA + and PlusCal (English)
• TLA - The Temporal Logic of Actions by Leslie Lamport (English)