Temporal Logic

A program works now. But will it work in an hour? In a year? Will it deadlock? Classical logic describes static facts. But programs are dynamic systems. Temporal logic allows proving: 'this property will hold always'.

• **Protocol verification**: proving the absence of deadlock in distributed systems (Amazon, NASA)
• **Smart contracts**: formal verification that a contract will never lock funds
• **Medical devices**: proving that a pacemaker will always respond to arrhythmia

Temporal Logic

**Temporal logic** - a branch of modal logic that formalizes reasoning about **time**. Instead of 'necessarily' and 'possibly', it uses operators 'always', 'eventually', 'until'.

Temporal logic is the foundation of **program verification**. Model checking (Turing Award 2007) uses it to prove the correctness of systems.

Why do we need a logic of time? Many system properties cannot be expressed without it:

There are two main types of temporal logic: **LTL** (Linear Temporal Logic) - time as a linear sequence, and **CTL** (Computation Tree Logic) - time as a tree of possibilities.

Operator [] (Always / Globally)

The operator **□φ** (read 'box φ' or 'globally φ', written **G** in LTL) means: φ is **true now and at all future moments in time**.

**Safety properties** are expressed via □: 'nothing bad will ever happen'. Example: □¬crash - 'the system will never crash'.

Connection to modal logic: □ in temporal logic is similar to □ (necessity), but is interpreted as 'in all future states', not 'in all possible worlds'.

Operator <> (Eventually / Finally)

The operator **◇φ** (read 'diamond φ' or 'eventually φ', written **F** in LTL) means: φ **will become true at some point in the future** (including the present moment).

The relationship between □ and ◇ - duality, like ∀ and ∃:

**Liveness properties** are expressed via ◇: 'something good will eventually happen'. Example: ◇terminated - 'the program will eventually terminate'.

Operator U (Until)

The operator **φ U ψ** ('φ until ψ') means: φ **remains true until ψ becomes true**, and ψ is guaranteed to eventually become true.

Important: in **strong until** (φ U ψ), ψ must eventually occur. There is also **weak until** (φ W ψ), where ψ may not occur - in that case φ remains true forever.

U is the most powerful LTL operator. It allows expressing **event sequences**: 'first A, then B'. Without it, you can only say 'eventually', but not 'in the right order'.

Complete Operator System

LTL includes operators for **past** and **future**, as well as **next** (X) - 'at the next moment'. CTL adds quantifiers over paths.

CTL (Computation Tree Logic) adds path quantifiers:

**Model checking**: algorithms automatically verify whether a system (finite automaton) satisfies a temporal formula. NuSMV, SPIN, UPPAAL - verification tools.

Applications: verification of protocols, controllers, smart contracts, medical devices - wherever an error is critical.

Key Ideas

• **□φ (Always)** - φ is true now and in all future states. Expresses safety properties
• **◇φ (Eventually)** - φ will become true at some point. Expresses liveness properties
• **φ U ψ (Until)** - φ holds until ψ, and ψ must eventually occur. Primitive LTL operator
• **LTL vs CTL**: linear time (one path) vs branching time (tree of paths with A/E quantifiers)

Related Topics

Temporal logic is part of the family of modal logics:

• Modal Logic — Temporal operators are an interpretation of modal operators in terms of time
• Deontic Logic — Combination: 'obligation to fulfill eventually' - ◇Oφ

Вопросы для размышления

• Can you express 'infinitely often' using □ and ◇? (Hint: □◇φ)
• What is the practical difference between 'φ U ψ' and 'φ W ψ'? When does it matter that ψ must eventually occur?
• Why is model checking feasible for finite automata but difficult for infinite systems?

Связанные уроки

• fl-05-regex