Massachusetts Institute of Technology Lecture 9 6.042J/18.062J: Mathematics for Computer Science October 5, 2000 Professors Nancy Lynch and Shlomi Dolev

Proof Methods for State Machines

Reading: These notes. Rosen Section 3.5 (skim)

1 Invariants and the Invariant Theorem

Definition 1.1 An invariant of a state machine M = (Q, Q_{0}, δ) is a predicate P (q) that is true for all reachable states q.

Given: M = (Q, Q_{0}, δ) is a state machine. Prove: P is an invariant of M.

1. ∀q ∈ Q_{0}(P (q))

2. ∀(q, q′) ∈ δ(P (q) ⇒ P (q′)).

3. QED Invariant theorem

Theorem 1.2 (Invariant theorem) Suppose M = (Q, Q_{0}, δ) is a state machine, and P is a predicate of states in Q such that:

1. ∀q ∈ Q_{0}(P (q)), and

2. ∀(q, q′) ∈ δ(P (q) ⇒ P (q′)).

Then P is an invariant of M (that is, is true in all reachable states of M).

Given: M = (Q, Q_{0}, δ) is a state machine. Given: ∀q ∈ Q_{0}(P (q)) Given: ∀(q, q′) ∈ δ(P (q) ⇒ P (q′)). Prove: P is an invariant of M, that is, ∀q ∈ Q(q reachable ⇒ P (q))

1. Let P′(n) be the predicate ∀q, q a final state of an n-step execution (P (q)).

2. ∀n ≥ 0(P′(n))

1. (Base) P′(0) By the assumption about start states 2. (Inductive step) ∀n ≥ 0(P′(n) ⇒ P′(n + 1))

1. Fix n ≥ 0

2. Assume P′(n)

3. P′(n + 1), that is, P is true for all final states of n + 1-step executions. 1. Fix an n + 1-step execution q_{0}, q_{1}, …, q_{n}, q_{n+1}.

2. q_{n} is the final state of an n-step execution.

3. P (q_{n}) Inductive hypothesis (2.2.2)

4. (q_{n}, q_{n+1}) is a step of M.

5. P (q_{n+1}) By the assumption about steps preserving P 6. QED UG

4. QED

3. QED Induction

3. QED (P is an invariant of M) Definition of “reachable”

Prove: P is an invariant of the Die Hard state machine.

1. ∀q ∈ Q_{0}(P (q)) P true for start state (0, 0).

2. ∀(q, q′) ∈ δ(P (q) ⇒ P (q′)).

1. Fix (q, q′) ∈ δ

2. Assume P (q).

3. P (q′)

1. If (q, q′) fills the little jar, then P (q′).

2. If (q, q′) fills the big jar, then P (q′).

3. If (q, q′) empties the little jar, then P (q′).

4. If (q, q′) empties the big jar, then P (q′).

5. If (q, q′) pours from little to big, then P (q′).

6. If (q, q′) pours from big to little, then P (q′).

7. QED Cases 4. QED Implication, UG

3. QED Invariant theorem

2 Termination and Time Bound Theorems

Definition 2.1 Suppose M = (Q, Q_{0}, δ) is a state machine. Then a termination function for M is a function f mapping reachable states of M to N, such that for every reachable q and q′ with (q, q′) in δ, f(q′) < f(q).

Theorem 2.2 (Time bound theorem) Suppose M = (Q, Q_{0}, δ) is a state machine, and f : Q → N is a termination function for M. Then the number of steps in any execution starting from q ∈ Q_{0} is at most f(q).

Theorem 2.3 (Termination theorem) Suppose M = (Q, Q_{0}, δ) is a state machine, and f : Q → N is a termination function for M. Then every execution of M is finite.

Given: M = (Q, Q_{0}, δ) is a state machine. Given: e is an execution of M, k ∈ N. Prove: e has at most k steps.

1. f : Q → N is a termination function for M.

2. f(q) ≤ k, where q ∈ Q_{0} is the first state of e.

3. QED Time bound theorem

Given: M = (Q, Q_{0}, δ) is a state machine. Prove: Every execution of M has at most k steps.

1. f : Q → N is a termination function for M.

2. ∀q ∈ Q_{0}(f(q) ≤ k)

3. QED Time bound theorem

Given: M = (Q, Q_{0}, δ) is a state machine. Prove: Every execution of M is finite.

1. There exists a termination function for M.

2. QED Termination theorem