Patterns in property specifications for finite-state verification | Synapse