model to describe the behavior of systems digraphs where nodes represent states, and edges model transitions ■ state o the current color of a traffic light o the current values of all program variables the program counter o the value of register and output transition: ("state change o a switch from one color to another o the execution of a program statement o the change of the registers and output bits for a new input◼ model to describe the behavior of systems ◼ digraphs where nodes represent states, and edges model transitions ◼ state:  the current color of a traffic light  the current values of all program variables + the program counter  the value of register and output ◼ transition: (“state change”)  a switch from one color to another  the execution of a program statement  the change of the registers and output bits for a new input