Para uma especificação mais rigorosa da semântica dos Guiões de Interacção foram utilizadas Petri Nets. A escolha deste formalismo ficou a dever-se fundamentalmente à facilidade com que possibilita a representação de processos concorrentes, dado possuir uma linguagem gráfica e uma semântica bem definida e estudada [Rei].
Descreve-se de seguida o tipo de redes utilizado, o modo como cada operador é especificado e como pode ser feita a composição dos diversos operadores para representar uma expressão mais complexa.