Modal Logic

1977: Amir Pnueli publishes his paper on temporal logic. The question: how to prove that a program will NEVER deadlock? Classical logic cannot answer this - it has no concept of "always" or "eventually". Classical logic sees a snapshot: true or false right now. Temporal logic sees a film: what happens at each step of an infinite execution. For this, Pnueli will receive the Turing Award in 1996.

• **Protocol verification:** NASA uses model checking (SPIN, LTL) to verify flight software - bugs in communication protocols cost missions, not just developer time.
• **Hardware verification:** after the Pentium FDIV bug (1994, $475 million in losses) Intel switched to formal verification of processor units using CTL model checking.
• **Epistemic logic in cryptography:** security protocols (TLS, Kerberos) are formally verified through knowledge logic - what the attacker knows, what the server knows, which worlds are accessible to each agent.

Предварительные знания

• Propositional logic - AND, OR, NOT operators, implication
• Predicate logic - quantifiers, formulas, interpretations
• Model theory - notion of a structure, truth of a formula in a model (ml-11)

• Model theory: structures, truth, Godel's completeness theorem

The Necessity Operator []

Classical logic describes what **is** - true or false. Modal logic describes what **must be** or **could be**. The **necessity** operator [] (read "box"): []phi means "phi is true in all possible worlds accessible from the current one". If phi is a law of nature, then []phi holds; if phi is a contingent fact, phi may be true but []phi need not be.

**Axiom K** (minimal system): [](p -> q) -> ([]p -> []q). Necessity distributes over implication: if it is necessary that p implies q, and p is necessary, then q is necessary. All extensions of modal logic include K as their base.

In system **S5**, necessity coincides with truth in all worlds without restriction: []p <-> p is true in all worlds. Mathematical theorems are necessarily true in S5: in any possible world, 2+2=4. The contingent fact "Napoleon lost at Waterloo" is true in our world but not in every possible one.

**History:** Modal logic traces back to Aristotle and was formalized by C.I. Lewis and Langford in *Symbolic Logic* (1932) through systems S1-S5. The modern possible-worlds semantics was given by Saul Kripke in 1959-1963 - see the next concept.

The Possibility Operator <> and Duality

The **possibility** operator <> (read "diamond"): <>phi means "phi is true in at least one possible world accessible from the current one". Formally: <>phi = -[]-phi. Possibility is the dual of necessity, just as existential quantification is the dual of universal quantification in predicate logic.

**Box-Diamond duality:** - []phi <-> -<>-phi (necessity = impossibility of the negation) - <>phi <-> -[]-phi (possibility = non-necessity of the negation) Analogy: (for all x) <-> (there is no x such that not), i.e. universal and existential quantifiers are duals.

**Epistemic logic** (Jaakko Hintikka, "Knowledge and Belief", 1962) was the first systematic application of possible-worlds semantics to knowledge. []_i phi reads "agent i knows phi". Axiom of knowledge: []_i phi -> phi (knowledge of a falsehood is impossible). This system became a foundation for game theory, cryptography, and protocol verification.

**Deontic logic** (logic of obligation): []phi = "phi is obligatory", <>phi = "phi is permitted". Applied in legal systems and ethics. Ross's paradox: from "mail the letter" we can derive "mail the letter or burn it" - a problem for standard deontic logic and an active research topic.

Kripke Semantics and Possible Worlds

In 1959, 18-year-old Saul Kripke published a paper giving complete semantics for modal logic. A **Kripke structure** (or Kripke frame) is a triple (W, R, V), where W is a non-empty set of possible worlds, R is a subset of W x W - the accessibility relation ("world v is accessible from world w"), and V: Prop x W -> {true, false} is a valuation function for atomic formulas.

**Correspondence between axioms and properties of R:** - Axiom T: []p -> p <-> R is reflexive (each world is accessible from itself) - Axiom 4: []p -> [][]p <-> R is transitive - Axiom B: p -> []<>p <-> R is symmetric - Axiom 5: <>p -> []<>p <-> R is Euclidean (from wRv and wRu it follows that vRu) S5 = K + T + 4 + 5 <-> R is an equivalence relation (reflexive + symmetric + transitive)

This correspondence is Kripke's central result: the **completeness theorem** for each standard system. For example, a formula phi is valid in S4 (true in every reflexive and transitive frame) if and only if phi is derivable in the S4 axiom system. This connects syntax (derivability) and semantics (truth in structures).

**Applications of Kripke semantics:** provability logic GL (Lob 1955; Kripke semantics via finite partial orders), intuitionistic logic (frames are partial orders, monotone valuation), epistemic logic in multi-agent systems (each agent has its own accessibility relation R_i).

Temporal Logic: LTL and CTL

In 1977, Amir Pnueli proposed **Linear Temporal Logic (LTL)** for reasoning about the behavior of reactive systems over time. LTL extends propositional logic with four operators: **X** (next - true at the next step), **F** (finally/eventually - true at some future step), **G** (globally/always - true at every step), **U** (until - p holds until q becomes true).

**CTL (Computation Tree Logic)** was proposed by Clarke and Emerson in 1981. Unlike LTL (linear time - a fixed path), CTL works with the **computation tree** - all possible paths from the current state. CTL adds path quantifiers: **A** (all paths) and **E** (there exists a path). Operators are written in pairs: AG, AF, EG, EF, AX, EX, AU, EU.

**Turing Award 2007:** Edmund Clarke, E. Allen Emerson, and Joseph Sifakis received it for creating **model checking** - automated verification of finite-state systems. Tools: SPIN (LTL, Bell Labs), NuSMV (CTL+LTL), PRISM (probabilistic MC). Intel has used model checking for hardware protocol verification since the 1990s - following the Pentium FDIV bug (1994), which cost the company $475 million.

Key Ideas

• **Modal operators:** [] (necessary - in all accessible worlds) and <> (possible - in at least one). They are dual: <>phi = -[]-phi. Different axioms (K, T, 4, B, 5) produce systems K, T, S4, S5 with different properties of the accessibility relation.
• **Kripke semantics (1963):** A frame (W, R, V) - set of worlds, accessibility relation, valuation of atoms. Axioms correspond to properties of R: T <-> reflexivity, 4 <-> transitivity, S5 <-> R is an equivalence relation.
• **LTL vs CTL:** LTL reasons about behavior on linear paths (G, F, X, U), CTL quantifies over paths in the computation tree (AG, EF, ...). They are incomparable in expressiveness. Model checking - automated verification: CTL in O(|S|*|phi|), LTL in PSPACE.

Related Topics

Modal logic runs through both mathematics and computer science:

• Model Theory and the Completeness Theorem — Kripke semantics is a special case of general model theory; Kripke's completeness theorem is analogous to Godel's theorem
• Algorithms and Verification — Model checking is an algorithmic problem on graphs: traversal of the state tree, checking LTL/CTL properties

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

• If free will is taken as a premise, which modal system describes it better - S4 (nested necessity) or S5 (all worlds equally accessible)? Why would determinism correspond to a system with an empty accessibility relation?
• Axiom of knowledge: []_i phi -> phi (knowledge of a falsehood is impossible). What happens to the logic when knowledge is replaced with belief? Which axiom must be dropped, and how does this change the structure of frames?
• The liveness property in LTL: AF phi (eventually phi). Why is it harder to verify than safety (AG -bad)? How does this difficulty relate to the notion of fairness in process scheduling?

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

• fl-01-intro