Temporal logic

Temporal logic ( temporal logic ; English temporal logic ) - logic , in the statements of which the time aspect is taken into account. Used to describe sequences of phenomena and their relationship on a timeline.

In ancient times, the application of logic in the temporal aspect was studied by the philosophers of the Mega school , in particular Diodorus Kron , and the Stoics . Modern symbolic temporal logic, first conceptualized and formulated in the 1950s by ^[1] on the basis of modal logic , gained the greatest distribution and development in computer science thanks to the works of Turing Prize winner Amir Pnueli .

Content

Example

The meaning of the statement: “I am hungry” does not change with time, but its truth can change: at a particular moment in time it can be true or false, but not simultaneously. In contrast to non-temporal logics, where the values of statements do not change over time, in temporal logic, the value depends on when it is checked. Temporal logic allows us to express statements like “I am always hungry”, “I am sometimes hungry” or “I am hungry until I sing.”

Temporal Operators

There are two kinds of operators in temporal logics: logical and modal. As logical operators are usually used ( $\neg ,\lor ,\land ,\rightarrow$ ${\ displaystyle \ neg, \ lor, \ land, \ rightarrow}$ ). The modal operators used in linear time logic and computation tree logic are defined as follows.

Text designation	Symbol	Definition	Description
Binary operators
$\phi$ ${\ displaystyle \ phi}$ U $\psi$ ${\ displaystyle \ psi}$	$\phi ~{\mathcal {U}}~\psi$ ${\ displaystyle \ phi ~ {\ mathcal {U}} ~ \ psi}$	${\begin{matrix}(B\,{\mathcal {U}}\,C)(\phi )=\\(\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))\end{matrix}}$ ${\ displaystyle {\ begin {matrix} (B \, {\ mathcal {U}} \, C) (\ phi) = \\ (\ exists i: C (\ phi _ {i}) \ land (\ forall j <i: B (\ phi _ {j}))) \ end {matrix}}}$	U ntil (strong): $\psi$ ${\ displaystyle \ psi}$ should be executed in some state in the future (possibly in the current one), the property $\phi$ ${\ displaystyle \ phi}$ must be performed in all states up to the indicated (not inclusive).
$\phi$ ${\ displaystyle \ phi}$ R $\psi$ ${\ displaystyle \ psi}$ $\phi$ ${\ displaystyle \ phi}$ V $\psi$ ${\ displaystyle \ psi}$	$\phi ~{\mathcal {R}}~\psi$ ${\ displaystyle \ phi ~ {\ mathcal {R}} ~ \ psi}$ $\phi ~{\mathcal {V}}~\psi$ ${\ displaystyle \ phi ~ {\ mathcal {V}} ~ \ psi}$	${\begin{matrix}(B\,{\mathcal {R}}\,C)(\phi )=\\(\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))\end{matrix}}$ ${\ displaystyle {\ begin {matrix} (B \, {\ mathcal {R}} \, C) (\ phi) = \\ (\ forall i: C (\ phi _ {i}) \ lor (\ exists j <i: B (\ phi _ {j}))) \ end {matrix}}}$	R elease: $\phi$ ${\ displaystyle \ phi}$ frees up $\psi$ ${\ displaystyle \ psi}$ , if a $\psi$ ${\ displaystyle \ psi}$ true until a moment comes when $\phi$ ${\ displaystyle \ phi}$ the first time will become true (or always, if such a moment does not come). Otherwise $\phi$ ${\ displaystyle \ phi}$ should at least once become true, while $\psi$ ${\ displaystyle \ psi}$ did not become true the first time.
Unary operators
N $\phi$ ${\ displaystyle \ phi}$ X $\phi$ ${\ displaystyle \ phi}$	$\circ \phi$ ${\ displaystyle \ circ \ phi}$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$ ${\ displaystyle {\ mathcal {N}} B (\ phi _ {i}) = B (\ phi _ {i + 1})}$	N e X t: $\phi$ ${\ displaystyle \ phi}$ must be true in the state immediately following the data.
F $\phi$ ${\ displaystyle \ phi}$	$\Diamond \phi$ ${\ displaystyle \ Diamond \ phi}$	${\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )$ ${\ displaystyle {\ mathcal {F}} B (\ phi) = (true \, {\ mathcal {U}} \, B) (\ phi)}$	F uture: $\phi$ ${\ displaystyle \ phi}$ must become true in at least one state in the future.
G $\phi$ ${\ displaystyle \ phi}$	$\Box \phi$ ${\ displaystyle \ Box \ phi}$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$ ${\ displaystyle {\ mathcal {G}} B (\ phi) = \ neg {\ mathcal {F}} \ neg B (\ phi)}$	G lobally: $\phi$ ${\ displaystyle \ phi}$ must be true in all future states.
A $\phi$ ${\ displaystyle \ phi}$	${\mathcal {A}}\phi$ ${\ displaystyle {\ mathcal {A}} \ phi}$	${\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}$ ${\ displaystyle {\ begin {matrix} ({\ mathcal {A}} B) (\ psi) = \\ (\ forall \ phi: \ phi _ {0} = \ psi \ to B (\ phi)) \ end {matrix}}}$	A ll: $\phi$ ${\ displaystyle \ phi}$ should be executed on all branches starting with this one.
E $\phi$ ${\ displaystyle \ phi}$	${\mathcal {E}}\phi$ ${\ displaystyle {\ mathcal {E}} \ phi}$	${\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}$ ${\ displaystyle {\ begin {matrix} ({\ mathcal {E}} B) (\ psi) = \\ (\ exists \ phi: \ phi _ {0} = \ psi \ land B (\ phi)) \ end {matrix}}}$	E xists: there is at least one branch on which $\phi$ ${\ displaystyle \ phi}$ performed.

Other modal operators

Operator W , meaning W eak until : $f W g$ ${\ displaystyle fWg}$ equivalently $fUg\lor Gf$ ${\ displaystyle fUg \ lor Gf}$

Duality identities

Like de Morgan's rules, there are duality properties for temporal operators:

$\phi ~{\mathcal {U}}~\psi =\neg (\neg \phi ~{\mathcal {V}}~\neg \psi )$ ${\ displaystyle \ phi ~ {\ mathcal {U}} ~ \ psi = \ neg (\ neg \ phi ~ {\ mathcal {V}} ~ \ neg \ psi)}$
$\neg \Diamond \phi =\Box \neg \phi$ ${\ displaystyle \ neg \ Diamond \ phi = \ Box \ neg \ phi}$
$\neg {\mathcal {A}}\phi ={\mathcal {E}}\neg \phi$ ${\ displaystyle \ neg {\ mathcal {A}} \ phi = {\ mathcal {E}} \ neg \ phi}$

Applications

Temporal logics are often used to express the requirements of formal verification . For example, properties of the type “if a request is received, then an answer will surely come” or “a function is called no more than once per calculation” can be conveniently formulated using temporal logics. To check such properties, various automata are used, for example, Buchi automata for checking properties expressed by the linear time logic LTL .

Options

The main universal variant of temporal logic is the ( Scott - de Bakker , 1969); it as a subset includes the and , and the main variants used in computer science — linear time logic ( LTL ) and computation tree logic ( CTL ) —are fragments of CTL *.

In addition, there are other variations of temporal logic that cannot be reduced to modal μ-calculus, for example, and

Some practical options use combinations of temporal logic with other logics, in particular, such is the temporal logic of actions (created for the specification language TLA⁺ ), which combines temporal logic and logic of actions .

Notes

↑ Ricardo Caferra. Logic for Computer Science and Artificial Intelligence. - John Wiley & Sons, 2013 .-- 537 p. - ISBN 978-1-118-60426-7 .

Literature

Clark E. M., Gramberg O., Peled D. Verification of program models. Model Checking. M .: ICNMO. 2002. ISBN 5-94057-054-2

[Caferra-1] Ricardo Caferra. Logic for Computer Science and Artificial Intelligence. - John Wiley & Sons, 2013 .-- 537 p. - ISBN 978-1-118-60426-7 .