To prove properties on Finite State Machines, we can construct a proof:
- stating an invariant
- proving that the invarient is true for all states
- for all transitions: assume invarient is true before transition and prove that its true after
So, essentially induction.