Finite State Machine is a convenient formalism for explicit representation of a system's state space.