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.