A semântica da linguagem SPL baseia-se no conceito de Fair Transition System (FTS). Essencialmente, este modelo computacional acrescenta aos sistemas de transições normais uma noção de justiça que impede a existência de transições que, embora permanentemente prontas a executar, nunca são executadas. No STeP todas os programas SPL são primeiro traduzidos para o respectivo FTS que é depois usada nas provas de propriedades temporais. Embora seja possível trabalhar com o STeP sem nunca visionar os FTSs, é conveniente ter alguma noção de como são gerados por forma a compreender melhor o processo de prova. Neste capítulo será apresentada brevemente a notação utilizada em [6] e a respectiva equivalência na notação do STeP.