Posted on by rpicard92

Formal Methods 101: Induction


Introduction:

Induction is a mathematical technique used to prove a property of a system.

Intuitively, you can think of induction as a way of proving that all dominos will fall. If we know that the first domino falls, and we know that this domino causes the next domino to fall, we are assured that all dominos will fall.

Induction involves 4 steps:

  1. Base Case: Proof that a property holds for the base case (or state).
  2. Inductive Hyposysis: Assume that the property holds for a latter case (or state) satisfies the assumptions of a base case (i.e. assume symbolic base case).
  3. Inductive Step: Perform an inductive step (i.e. symbolic transition to the next state).
  4. Proof Step: Prove that a property holds after the inductive step (i.e. after the symbolic transition.)

Classic Example:

We will now explore a classic example. We will prove that the following formula holds out to N natural numbers; that is the sum of n natural numbers equals P(n).

P(n) = \frac{n(n+1)}{2} = 0 + 1 + 2 + ... + n

  • Step 1 – Base Case:
    • Test the base case, n=0.
    • P(0) = \frac{n(n+1)}{2} = \frac{0(0+1)}{2} = 0
    • The base case is proven true.
  • Step 2 – Inductive Hypothesis:
    • Assume P(n) holds for a latter case, n = k | n ∈ ℕ , which has the same properties as the base case. (i.e. symbolic base case)
    • P(k) = \frac{k(k+1)}{2} = (0 + 1 + 2 + ... + k)
  • Step 3 – Inductive Step:
    • Perform an inductive step by testing n = k+1. (i.e. symbolic execution from k to k+1)
    • Equation for P(k+1):
      • \frac{(k+1)((k+1)+1)}{2} = (0 + 1 + 2 + ... + k) + (k + 1)
    • Left Hand Side:
      • \frac{(k+1)((k+1)+1)}{2}
    • Right Hand Side:
      • (0 + 1 + 2 + ... + k) + (k + 1)
  • Step 4 – Proof Step:
    • Check if the property, P(n), still holds.
    • Simplify Left-Hand Side:
      • \frac{(k+1)((k+1)+1)}{2} = \frac{k^2+2k+2}{2}
    • Rewrite Right-Hand Side by Definition:
      • (0 + 1 + 2 + ... + k) + (k + 1) = \frac{k(k+1)}{2} + (k+1)
    • Rewrite Right Hand Side:
      • Step 1:
        • \frac{k(k+1)}{2} + (k+1) = \frac{k(k+1) + 2(k+1)}{2}
      • Step 2:
        • \frac{k(k+1) + 2(k+1)}{2} = \frac{(k+1)(k+2)}{2}
      • Step 3:
        • \frac{(k+1)(k+2)}{2} = \frac{(k+1)((k+1)+1)}{2}
    • Set Left Hand Side equal to Right Hand Side
      • \frac{(k+1)((k+1)+1)}{2}\ = \frac{(k+1)((k+1)+1)}{2}
    • Proof Complete: We have proved that for all n, P(n) holds

Types of Induction:

  • Weak Induction (or Simple Induction):
    • The classical example above was an example of weak induction; that is, we only assume a single base case (and therefore, symbolic base case) and an inductive step.
    • (\phi(0) \land (\forall n)(\phi(n) \rightarrow \phi(n+1))) \rightarrow (\forall n)\phi(n)
    • In natural language this is read: The property holds in the initial state and for all future states, if the property holds for some state, it holds for the next state; therefore, the property holds for all states.
  • Strong Induction(or Complete Induction, or K-Induction) :
    • Complete induction is when you make the property easier to prove by inductive strengthening the base case (and therefore, symbolic base case), also known as the inductive hypothesis.
    • (\phi(0) \land (\forall n)((\forall m \leq n)\phi(m) \rightarrow (\forall m \leq n + 1)\phi (m))) \rightarrow (\forall n)\phi(n)
    • In natural language this is read: The property holds in the initial state and for all future states, if the property holds for some amount of states, it holds for the next state; therefore, the property holds for all states.
  • K-Induction can be looked at from a different syntactic lense:
    • Consider the following set of equivalent formulas:
    • 1-Induction:
      • (\phi(0) \land (\forall n)(\phi(n) \rightarrow \phi(n+1))) \rightarrow (\forall n)\phi(n)
    • 2-Induction:
      • (\phi(0) \land \phi(1) \land (\forall n)((\phi(n) \land \phi(n+1)) \rightarrow \phi(n+2))) \rightarrow (\forall n)\phi(n)
    • K-Induction:
      • (\phi(0) \land \phi(1) \land ... \land \phi(k) \land (\forall n)(\phi(n) \land \phi(n+1) \land ... \land \phi(n+k) \rightarrow \phi(n+k))) \rightarrow (\forall n)\phi(n)
    • K-Induction (simplified):
      • ( \bigwedge_{i=0}^{k-1} \phi(i) \land (\forall n)(\bigwedge_{i=0}^{k-1} \phi(n+i) \rightarrow \phi(n+k))) \rightarrow (\forall n)\phi(n)

Induction for Extended-State Machines:

  • Induction may be applied to extended-state machines to prove invariant properties about systems.
  • Consider the following extended-state machine. This system is made up of two states, four transitions, one variable of type int, and one variable representing the current state (i.e. S1 or S2). The system initially states in the state S1 with variable x equal to 0. In the next transition (step), if x is less than 0, the system transitions to state S2 and increments x by one. While in state S2, the system increments x by one each transition (step) until x is greater than 9. When x is greater than 9, the system transitions back to state S1 and resets x to 0.
  • Consider the following property that we wish to prove is invariant by induction:
    • \phi = (x \leq 9)
    • That is, x can never be greater than 9. This is known as a static invariant; which is a property that is unchanging throughout the life of the system.
    • If the invariant can be proven by induction then we call this an inductive invariant. Note: there are invariants that cannot be proven by induction.
  • Notices how this extened-state machine can be written as the following SMT formula:
    • S:= ( (x < 9) \rightarrow ( x' = x + 1 \land state' = S2 ) ) \land ( (x \geq 9) \rightarrow (x' = 0 \land state' = S1) )
    • Note: x’ & state’ stand for the value of the x & state variables after the next transition.
  • We will now join this property to this SMT formula by an implication operator; indicating that where this system SMT formula is satisfied, the property is always satisfied.
    • S \rightarrow \phi := ( ( (x < 9) \rightarrow ( x' = x + 1 \land state' = S2 ) ) \land ( (x \geq 9) \rightarrow (x' = 0 \land state' = S1) ) ) \rightarrow ((x \leq 9) \land (x' \leq 9))

We will now attempt to prove this invariant via induction.

  • Step 1 – Base Case:
    • Test the base case (i.e. the initial value), x = 0 & state = S1.
    • S \rightarrow \phi := (( (0 < 9) \rightarrow ( x' = 0 + 1 \land state' = S2 ) ) \land ( (0 \geq 9) \rightarrow (x' = 0 \land state' = S1) )) \rightarrow ((x \leq 9) \land (x' \leq 9))
    • Simplify…
    • S \rightarrow \phi := (( (0 < 9) \rightarrow ( x' = 1 \land state' = S2 ) ) \land ( (0 \geq 9) \rightarrow (x' = 0 \land state' = S1) )) \rightarrow ((0 \leq 9) \land (1 \leq 9))
    • S \rightarrow \phi := TRUE \land TRUE) \rightarrow (TRUE \land TRUE
    • S \rightarrow \phi := TRUE \rightarrow TRUE
    • S \rightarrow \phi := TRUE
    • The base case is proven true.
  • Step 2 – Inductive Hypothesis:
    • Assume the property holds for a latter case, x = k (where k \leq 9)
    • S \rightarrow \phi := ( ((k < 9) \rightarrow ( x' = k + 1 \land state' = S2 ) ) \land ( (k \geq 9) \rightarrow (x' = k \land state' = S1) )) \rightarrow ((k \leq 9) \land (x' \leq 9))
    • S \rightarrow \phi := TRUE (assumed)
  • Step 3 – Inductive Step:
    • Perform and inductive step by testing n = k+1. (i.e. symbolic execution from k to k+1)
    • S \rightarrow \phi := ( ((k + 1) < 9) \rightarrow ( x' = (k + 1) + 1 \land state' = S2 ) ) \land ( ((k + 1) \geq 9) \rightarrow (x' = (k + 1) \land state' = S1) )) \rightarrow (((k+1) \leq 9) \land (x' \leq 9))
  • Step 4 – Proof Step:
    • Check if the implication, S \rightarrow \phi, still holds.
    • In order to do this, we much check is \phi holds for the two cases: the case when (k < 9) and the case when (k \geq 9). Note: only one of these can be true at one point time, and one of them must always be true.
    • Case 1: ((k + 1) < 9)
      • x' = k+2
      • \phi := ((k+1) \leq 9) \land ((k+2) \leq 9)
      • Since k+1 is less than 9, the highest k could be is 7.
      • \phi := ((7+1) \leq 9) \land ((7+2) \leq 9)
      • \phi := (8 \leq 9) \land (9 \leq 9)
      • \phi := TRUE
    • Case 2: ((k + 1) \geq 9)
      • x' = 0
      • Because (k + 1) \geq 9 , and our assumption from our inductive hypothesis is that (k + 1) \leq 9 where k is an integer, we can conclude that (k + 1) = 9. Therefore, k must equal 8.
      • \phi := ((8+1) \leq 9) \land (0 \leq 9)
      • \phi := (9 \leq 9) \land (0 \leq 9)
      • \phi := TRUE \land TRUE
      • \phi := TRUE
    • Proof Complete: We have proved that for all states the property \phi := x \leq 9 is held. Since we have proven \phi by induction, we call the property an inductive invariant of the system.