DOC PREVIEW
MIT 6 042J - Invariants and Termination

This preview shows page 1-2-3-4-5 out of 15 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

State machinesBasic definitionsExamplesExecutions of state machinesReachability and InvariantsDie Hard Once and For AllThe RobotSequential algorithm examplesProving CorrectnessThe Euclidean AlgorithmPartial Correctness of GCDTermination of GCDThe Extended Euclidean AlgorithmDerived VariablesThe Stable Marriage ProblemThe ProblemThe Mating AlgorithmThe State Machine ModelTerminationThey All Live Happily Every After......And the Boys Live Especially HappilyMassachusetts Institute of Technology Course Notes, Week 76.042J/18.062J, Fall ’05: Mathematics for Computer Science October 21Prof. Albert R. Meyer and Prof. Ronitt Rubinfeld revised October 21, 2005, 364 minutesState Machines: Invariants and Termination1 State machinesState machines are an abstract model of step-by-step processes, and accordingly, they come up inmany areas of Computer Science. You may already have seen them in a digital logic course, acompiler course, or a a probability course.1.1 Basic definitionsA state machine is really nothing more than a digraph, except that the vertices are called “states”and the edges are called “transitions.” The transition (edge) from state p to state q will be writtenp → q.A state machine also comes equipped with a designated start state.State machines used in digital logic and compilers usually have only a finite number of states,but machines that model continuing computations typically have an infinite number of states. Inmany applications, the transitions in the state graphs are labelled with tokens indicating inputsor outputs, or numbers indicating costs, capacities or probabilities. In these Notes, we’ll stick tounlabelled transitions.1.2 ExamplesHere are some simple examples of state machines.Example 1.1. A bounded counter, which counts from 0 to 99 and overflows at 100. The state graphis shown in Figure 1, with start state zero.0 1 299 overflowstartstateFigure 1: The state graph of the 99-bounded counter.This machine isn’t much use once it overflows, since it has no way to get out of its overflow state.Copyright © 2005, Prof. Albert R. Meyer. All rights reserved.2 Course Notes, Week 7: State Machines: Invariants and TerminationExample 1.2. An unbounded counter is similar, but has an infinite state set, yielding an infinitedigraph. This is harder to draw :-)Example 1.3. The Die Hard 3 scenario with a 3 and a 5 gallon water jug could be modelled as astate machine. For states we could use pairs, (b, l) of real numbers such that 0 ≤ b ≤ 5, 0 ≤ l ≤ 3.We let b and l be arbitrary real numbers since Bruce could pour any amount of water into a bucket.The start state is (0, 0), since both jugs start empty.There are several kinds of transitions:1. Fill the little jug: (b, l) → (b, 3) for l < 3.2. Fill the big jug: (b, l) → (5, l) for b < 5.3. Empty the little jug: (b, l) → (b, 0) for l > 0.4. Empty the big jug: (b, l) → (0, l) for b > 0.5. Pour from the little jug into the big jug: for l > 0,(b, l) →((b + l, 0) if b + l ≤ 5,(5, l − (5 − b)) otherwise.6. Pour from big jug into little jug: for b > 0,(b, l) →((0, b + l) if b + l ≤ 3,(b − (3 − l), 3) otherwise.Note that in contrast to the 99-counter state machine, there is more than one possible transitionout of states in the Die Hard machine.Problem 1. Which states of the Die Hard 3 machine have direct transitions to exactly two states?1.3 Executions of state machinesThe Die Hard 3 machine models every possible way of pouring water among the jugs accordingto the rules. Die Hard properties that we want to verify can now be expressed and proved usingthe state machine model. For example, Bruce will disarm the bomb if he can reach some state ofthe form (4, l).In graph language, a (possibly infinite) path through the state machine graph beginning at thestart state corresponds to a possible system behavior; such a path is called an execution of the statemachine. A state is called reachable if there is a path to it starting from the start state, that is, if itappears in some execution.We observed that the state (4,3) was reachable, reflecting the fact that Bruce and Samuel success-fully disarmed the bomb in Die Hard 3.Course Notes, Week 7: State Machines: Invariants and Termination 32 Reachability and InvariantsA useful approach in analyzing state machine is to identify invariant properties of states.Definition 2.1. An invariant for a state machine is a predicate, P , on states, such that wheneverP (q) is true of a state, q, and q → r for some state, r, then P (r) holds.Now we can reformulate the Induction Axiom specially for state machines:Theorem 2.2 (Invariant Theorem). Let P be an invariant predicate for a state machine. If P holds forthe start state, then P holds for all reachable states.The truth of the Invariant Theorem is as obvious as the truth of the Induction Axiom. We couldprove it, of course, by induction on the length of finite executions, but we won’t bother.2.1 Die Hard Once and For AllNow back to Die Hard Once and For All. This time there is a 9 gallon jug instead of the 5 gallonjug. We can model this with a state machine whose states and transitions are specified the sameway as for the Die Hard 3 machine, with all occurrences of “5” replaced by “9.”Now reaching any state of the form (4, l) is impossible. We prove this using the Invariant Theorem.Namely, we define the invariant predicate, P ((b.l)), to be that b and l are nonnegative integermulitples of 3. So P obviously holds for the state state (0, 0).The proof that P is an invariant, we assume P ((b, l) holds for some state (b.l) and show that if(b, l) → (b0, l0), then P (b0, l0). The proof divides into cases, according to which transition ruleis used. For example, suppose the transition followed from the “fill the little jug” rule. Thismeans (b, l) → (b, 3). But P ((b, l) impiles that b is an integer multiple of 3, and of course 3 isan integer multiple of 3, so P still holds for the new state (b, 3). Another example is when thetransition rule used is “pour from big jug into little jug” for the subcase that b + l > 3. Then stateis (b, l) → (b − (3 − l), 3). But since b and l are integer multiples of 3, so is b − (3 − l). So in this casetoo, P holds after the transition.We won’t bother to crank out the remaining cases, which can all be checked with equal ease. Nowby the Invariant Theorem, we conclude that every reachable state satisifies P . But since no stateof the form (4, l) satisifies P ,


View Full Document

MIT 6 042J - Invariants and Termination

Documents in this Course
Counting

Counting

55 pages

Graphs

Graphs

19 pages

Proofs

Proofs

14 pages

Proofs

Proofs

18 pages

Proofs

Proofs

18 pages

Quiz 1

Quiz 1

9 pages

Quiz 2

Quiz 2

11 pages

Load more
Download Invariants and Termination
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Invariants and Termination and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Invariants and Termination 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?