A linguagem de especificação de propriedades adoptada no STeP é a lógica temporal linear. Esta lógica é construída sobre uma lógica de primeira ordem que permite expressar fórmulas sobre as variáveis e marcas dos programas especificados.
